From 6b3cf1826116f70f6114798125f6edeb711cf4ec Mon Sep 17 00:00:00 2001 From: Evgenii Akentev Date: Wed, 27 Mar 2024 01:26:05 +0400 Subject: [PATCH] Small improvements --- Temple/DeBruijn.lean | 10 +++---- Temple/DeBruijnEval.lean | 27 ++++++++--------- Temple/Eval.lean | 64 +++++++++++++++++++++++++++++++++++++--- Temple/Syntax.lean | 1 - 4 files changed, 77 insertions(+), 25 deletions(-) diff --git a/Temple/DeBruijn.lean b/Temple/DeBruijn.lean index 16569dd..5fd93cb 100644 --- a/Temple/DeBruijn.lean +++ b/Temple/DeBruijn.lean @@ -29,24 +29,24 @@ partial instance : ToString Term where | .op name args => "{% " ++ name ++ " " ++ (String.join $ List.intersperse " " args) ++ " %}" | .forloop name body => "{% for " ++ toString name ++ " %}\n" - ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body))) + ++ (String.join $ List.intersperse "\n" $ body.map toStr) ++ "\n{% endfor %}" toStr -@[inline] def index (v : String) (binds : List String) : Option Nat := List.lookup v (List.zip binds (List.range (List.length binds))) +@[inline] def index (v : String) (binds : List String) : Option Nat := (binds.zip $ List.range binds.length).lookup v -partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax.Term) : Term := +private partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax.Term) : Term := match t with | .text t => Term.text t | .var n => match (index n binds) with | .some i => .var (Var.bound (i, n)) | .none => .var (Var.free n) | .op n args => Term.op n args - | .forloop v collection ts => + | .forloop v collection terms => let range_bind := match (index collection binds) with | .some i => (Var.bound (i, collection)) | .none => Var.free collection - Term.forloop range_bind (List.map (fromSyntaxTermInner ([v] ++ binds)) ts) + Term.forloop range_bind $ terms.map (fromSyntaxTermInner $ [v] ++ binds) @[inline] def fromSyntaxTerm (t : TempleSyntax.Term) : Term := fromSyntaxTermInner [] t diff --git a/Temple/DeBruijnEval.lean b/Temple/DeBruijnEval.lean index 1272a0a..0b4d759 100644 --- a/Temple/DeBruijnEval.lean +++ b/Temple/DeBruijnEval.lean @@ -17,15 +17,13 @@ partial instance : ToString Value where have : ToString Value := ⟨toStr⟩ match x with | .text s => s - | .list s => ", ".intercalate (s.map toStr) + | .list s => "[" ++ ",".intercalate (s.map toStr) ++ "]" toStr structure Context where - data : Lean.HashMap String Value - operators : Lean.HashMap String Value - binds : List Value - -def emptyCtx : Context := { binds := [], data := Lean.HashMap.ofList [], operators := Lean.HashMap.ofList []} + data : Lean.HashMap String Value := Lean.HashMap.ofList [] + operators : Lean.HashMap String Value := Lean.HashMap.ofList [] + binds : List Value := [] partial def eval (ctx : Context) (t : Term) : Except String String := match t with @@ -55,20 +53,20 @@ partial def eval (ctx : Context) (t : Term) : Except String String := section Test #eval show Bool from - let t := eval emptyCtx (.text "hello") + let t := eval {} (.text "hello") t.toOption == some "hello" #eval show Bool from - let t := eval ({emptyCtx with operators := Lean.HashMap.ofList [ ( "hello", .text "world" ) ]}) (.op "hello" []) + let t := eval ({operators := Lean.HashMap.ofList [ ( "hello", .text "world" ) ]}) (.op "hello" []) t.toOption == some "world" #eval show Bool from - let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]}) + let t := eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]}) (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "0")) ]) t.toOption == some "hello worldhello land" #eval show Bool from - let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ]) + let t := eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ]) , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]}) (.forloop (Var.free "fruits") [ .text "got an ", .var (.bound (0, "0")), .text "\n" @@ -76,28 +74,27 @@ section Test t.toOption == some "got an apple\nsaladoniongot an orange\nsaladonion" #eval show Except String String from - let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ]) + eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ]) , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]}) (.forloop (Var.free "fruits") [ .text "got an ", .var (.bound (0, "0")), .text "\n" , .forloop (Var.free "vegetables") [ .var (.bound (1, "1")) ] ]) - t #eval show Except String String from try - eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]}) + eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]}) (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (1, "x")) ]) catch e => pure s!"Caught exception: {e}" #eval show Except String String from try - eval ({emptyCtx with data := Lean.HashMap.ofList [ ]}) + eval ({data := Lean.HashMap.ofList [ ]}) (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "x")) ]) catch e => pure s!"Caught exception: {e}" #eval show Except String String from try - eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]}) + eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]}) (.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ]) catch e => pure s!"Caught exception: {e}" diff --git a/Temple/Eval.lean b/Temple/Eval.lean index 3105f55..c6d5533 100644 --- a/Temple/Eval.lean +++ b/Temple/Eval.lean @@ -1,21 +1,77 @@ +import Init.System.IO + import Temple.Syntax import Temple.DeBruijn import Temple.DeBruijnEval namespace TempleEval -open TempleDeBruijnEval +open IO.FS + +open TempleDeBruijnEval (Context) -def eval (c : Context) (s : String) : Except String String := do +structure UserContext where + data : Lean.HashMap String Value + operators : Lean.HashMap String Value + +def runStringWith (c : Context) (s : String) : Except String String := do let terms <- TempleSyntax.parse s let deBruijnTerms := List.map TempleDeBruijn.fromSyntaxTerm terms let results <- deBruijnTerms.mapM $ TempleDeBruijnEval.eval c return String.join results +@[inline] def runString (s : String) : Except String String := runStringWith { } s + +@[inline] def runWith (c : Context) (fn : System.FilePath) : IO (Except String String) := do + let s <- IO.FS.readFile fn + return runStringWith c s + +@[inline] def run (fn : System.FilePath) : IO (Except String String) := do + let s <- IO.FS.readFile fn + return runString s + +section Test + #eval show Except String String from - eval emptyCtx "hello" + runStringWith {} "hello" #eval show Except String String from - eval {emptyCtx with data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}" + runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}" + +#eval show Except String String from + runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world"), ("xs", .list $ [ "1", "2", "3" ].map .text ) ] } + "hello {{ world }} + + {% for x in xs %} + #{{ x }} + {% endfor %} + " + +#eval show IO Unit from + let dataItems := Lean.HashMap.ofList + [ ("world", .text "world") + , ("xs", .list $ [ "1", "2", "3" ].map .text ) + , ("ys", .list $ [ "4", "5", "6" ].map .text ) + ] + let t := runStringWith { data := dataItems } + "hello {{ world }} +{% for x in xs %} + {% for y in ys %}#{{ x }} {{y}} {% endfor %} +{% endfor %}" + IO.println t + +#eval show IO Unit from + let dataItems := Lean.HashMap.ofList + [ ("world", .text "world") + , ("xs", .list $ [ .text "1", .list [ .text "2", .text "3"], .text "4" ] ) + ] + let t := runStringWith { data := dataItems } + "hello {{ world }} +{% for x in xs %} + {% for y in x %}#{{ x }}{{y}} {% endfor %} +{% endfor %}" + IO.println t + +end Test end TempleEval diff --git a/Temple/Syntax.lean b/Temple/Syntax.lean index ef8b505..7456eb8 100644 --- a/Temple/Syntax.lean +++ b/Temple/Syntax.lean @@ -38,7 +38,6 @@ open Parser Char partial def textInner (acc : String) : TempleParser String := withErrorMessage "" do - try let savePos <- getPosition match <- option? (chars "{{" <|> chars "{%") with -- 2.34.1