Small improvements

diff --git a/Temple/DeBruijn.lean b/Temple/DeBruijn.lean
index 16569ddf456e3e9ef8e50f95c17d410cec542fb5..5fd93cbeed4a882ecb4027c7a51fc6dfae44f05d 100644 (file)
--- 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 1272a0a50041cc70ddad84bed38844df4281655b..0b4d759ca2ce165f3332f07e4efb7531a6e43800 100644 (file)
--- 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 3105f55aedfe2666c5f4bf16ca04d402ad4dad96..c6d553358726760237797a869df9b25558ea3890 100644 (file)
--- 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 ef8b5056eb81745da9167e95d0605a883874bc1f..7456eb8d0aef8c813a80cf16517a218c8be77b94 100644 (file)
--- a/Temple/Syntax.lean
+++ b/Temple/Syntax.lean
@@ -38,7 +38,6 @@ open Parser Char
 
 partial def textInner (acc : String) : TempleParser String :=
   withErrorMessage "<text>" do
-
     try
       let savePos <- getPosition
       match <- option? (chars "{{" <|> chars "{%") with