repos / temple.lean4.git

commit

6b3cf18

parent

426ef43

author

Evgenii Akentev

date

2024-03-27 01:26:05 +0400 +04

Small improvements

 1@@ -29,24 +29,24 @@ partial instance : ToString Term where
 2       | .op name args => "{% " ++ name ++ " " ++ (String.join $ List.intersperse " " args) ++ " %}"
 3       | .forloop name body =>
 4         "{% for " ++ toString name ++ " %}\n"
 5-          ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body)))
 6+          ++ (String.join $ List.intersperse "\n" $ body.map toStr)
 7           ++ "\n{% endfor %}"
 8     toStr
 9 
10-@[inline] def index (v : String) (binds : List String) : Option Nat := List.lookup v (List.zip binds (List.range (List.length binds)))
11+@[inline] def index (v : String) (binds : List String) : Option Nat := (binds.zip $ List.range binds.length).lookup v
12 
13-partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax.Term) : Term :=
14+private partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax.Term) : Term :=
15   match t with
16   | .text t => Term.text t
17   | .var n => match (index n binds) with
18     | .some i => .var (Var.bound (i, n))
19     | .none => .var (Var.free n)
20   | .op n args => Term.op n args
21-  | .forloop v collection ts =>
22+  | .forloop v collection terms =>
23     let range_bind := match (index collection binds) with
24       | .some i => (Var.bound (i, collection))
25       | .none => Var.free collection
26-    Term.forloop range_bind (List.map (fromSyntaxTermInner ([v] ++ binds)) ts)
27+    Term.forloop range_bind $ terms.map (fromSyntaxTermInner $ [v] ++ binds)
28 
29 @[inline] def fromSyntaxTerm (t : TempleSyntax.Term) : Term := fromSyntaxTermInner [] t
30 

 1@@ -17,15 +17,13 @@ partial instance : ToString Value where
 2       have : ToString Value := ⟨toStr⟩
 3       match x with
 4       | .text s => s
 5-      | .list s => ", ".intercalate (s.map toStr)
 6+      | .list s => "[" ++ ",".intercalate (s.map toStr) ++ "]"
 7     toStr
 8 
 9 structure Context where
10-  data : Lean.HashMap String Value
11-  operators : Lean.HashMap String Value
12-  binds : List Value
13-
14-def emptyCtx : Context := { binds := [], data := Lean.HashMap.ofList [], operators := Lean.HashMap.ofList []}
15+  data : Lean.HashMap String Value := Lean.HashMap.ofList []
16+  operators : Lean.HashMap String Value := Lean.HashMap.ofList []
17+  binds : List Value := []
18 
19 partial def eval (ctx : Context) (t : Term) : Except String String :=
20   match t with
21@@ -55,20 +53,20 @@ partial def eval (ctx : Context) (t : Term) : Except String String :=
22 section Test
23 
24 #eval show Bool from
25-  let t := eval emptyCtx (.text "hello")
26+  let t := eval {} (.text "hello")
27   t.toOption == some "hello"
28 
29 #eval show Bool from
30-  let t := eval ({emptyCtx with operators := Lean.HashMap.ofList [ ( "hello", .text "world" ) ]}) (.op "hello" [])
31+  let t := eval ({operators := Lean.HashMap.ofList [ ( "hello", .text "world" ) ]}) (.op "hello" [])
32   t.toOption == some "world"
33 
34 #eval show Bool from
35-  let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
36+  let t := eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
37                 (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "0")) ])
38   t.toOption == some "hello worldhello land"
39 
40 #eval show Bool from
41-  let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
42+  let t := eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
43                                                             , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
44                 (.forloop (Var.free "fruits")
45                   [ .text "got an ", .var (.bound (0, "0")), .text "\n"
46@@ -76,28 +74,27 @@ section Test
47   t.toOption == some "got an apple\nsaladoniongot an orange\nsaladonion"
48 
49 #eval show Except String String from
50-  let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
51+  eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
52                                                             , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
53                 (.forloop (Var.free "fruits")
54                   [ .text "got an ", .var (.bound (0, "0")), .text "\n"
55                   , .forloop (Var.free "vegetables") [ .var (.bound (1, "1")) ] ])
56-  t
57 
58 #eval show Except String String from
59   try
60-    eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
61+    eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
62                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (1, "x")) ])
63   catch e => pure s!"Caught exception: {e}"
64 
65 #eval show Except String String from
66   try
67-    eval ({emptyCtx with data := Lean.HashMap.ofList [ ]})
68+    eval ({data := Lean.HashMap.ofList [ ]})
69                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "x")) ])
70   catch e => pure s!"Caught exception: {e}"
71 
72 #eval show Except String String from
73   try
74-    eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
75+    eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
76                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ])
77   catch e => pure s!"Caught exception: {e}"
78 

 1@@ -1,21 +1,77 @@
 2+import Init.System.IO
 3+
 4 import Temple.Syntax
 5 import Temple.DeBruijn
 6 import Temple.DeBruijnEval
 7 
 8 namespace TempleEval
 9 
10-open TempleDeBruijnEval
11+open IO.FS
12+
13+open TempleDeBruijnEval (Context)
14 
15-def eval (c : Context) (s : String) : Except String String := do
16+structure UserContext where
17+  data : Lean.HashMap String Value
18+  operators : Lean.HashMap String Value
19+
20+def runStringWith (c : Context) (s : String) : Except String String := do
21   let terms <- TempleSyntax.parse s
22   let deBruijnTerms := List.map TempleDeBruijn.fromSyntaxTerm terms
23   let results <- deBruijnTerms.mapM $ TempleDeBruijnEval.eval c
24   return String.join results
25 
26+@[inline] def runString (s : String) : Except String String := runStringWith { } s
27+
28+@[inline] def runWith (c : Context) (fn : System.FilePath) : IO (Except String String) := do
29+  let s <- IO.FS.readFile fn
30+  return runStringWith c s
31+
32+@[inline] def run (fn : System.FilePath) : IO (Except String String) := do
33+  let s <- IO.FS.readFile fn
34+  return runString s
35+
36+section Test
37+
38 #eval show Except String String from
39-  eval emptyCtx "hello"
40+  runStringWith {} "hello"
41 
42 #eval show Except String String from
43-  eval {emptyCtx with data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"
44+  runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"
45+
46+#eval show Except String String from
47+  runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world"), ("xs", .list $ [ "1", "2", "3" ].map .text ) ] }
48+    "hello {{ world }}
49+
50+    {% for x in xs %}
51+      #{{ x }}
52+    {% endfor %}
53+    "
54+
55+#eval show IO Unit from
56+  let dataItems := Lean.HashMap.ofList
57+        [ ("world", .text "world")
58+        , ("xs", .list $ [ "1", "2", "3" ].map .text )
59+        , ("ys", .list $ [ "4", "5", "6" ].map .text )
60+        ]
61+  let t := runStringWith { data := dataItems }
62+    "hello {{ world }}
63+{% for x in xs %}
64+  {% for y in ys %}#{{ x }} {{y}} {% endfor %}
65+{% endfor %}"
66+  IO.println t
67+
68+#eval show IO Unit from
69+  let dataItems := Lean.HashMap.ofList
70+        [ ("world", .text "world")
71+        , ("xs", .list $ [ .text "1", .list [ .text "2", .text "3"], .text "4" ] )
72+        ]
73+  let t := runStringWith { data := dataItems }
74+    "hello {{ world }}
75+{% for x in xs %}
76+  {% for y in x %}#{{ x }}{{y}} {% endfor %}
77+{% endfor %}"
78+  IO.println t
79+
80+end Test
81 
82 end TempleEval

1@@ -38,7 +38,6 @@ open Parser Char
2 
3 partial def textInner (acc : String) : TempleParser String :=
4   withErrorMessage "<text>" do
5-
6     try
7       let savePos <- getPosition
8       match <- option? (chars "{{" <|> chars "{%") with