- commit
- fe1d360
- parent
- 6b3cf18
- author
- Evgenii Akentev
- date
- 2024-03-27 02:58:33 +0400 +04
Add operators support.
4 files changed,
+90,
-62
+16,
-4
1@@ -12,9 +12,18 @@ instance : ToString Var where
2 | .bound (_ , n) => n
3 | .free n => n
4
5+inductive Arg
6+-- TODO: support strings and other types of arguments
7+| var : Var -> Arg
8+deriving BEq, Repr, Inhabited
9+
10+instance : ToString Arg where
11+ toString
12+ | .var v => toString v
13+
14 inductive Term
15 | text : String -> Term
16-| op : String -> List String -> Term
17+| op : String -> List Arg -> Term
18 | var : Var -> Term
19 | forloop : Var -> List Term -> Term
20 deriving BEq, Repr, Inhabited
21@@ -26,7 +35,7 @@ partial instance : ToString Term where
22 match x with
23 | .text t => t
24 | .var v => "{{ " ++ toString v ++ " }}"
25- | .op name args => "{% " ++ name ++ " " ++ (String.join $ List.intersperse " " args) ++ " %}"
26+ | .op name args => "{% " ++ name ++ " " ++ (String.join $ List.intersperse " " $ args.map toString) ++ " %}"
27 | .forloop name body =>
28 "{% for " ++ toString name ++ " %}\n"
29 ++ (String.join $ List.intersperse "\n" $ body.map toStr)
30@@ -41,7 +50,10 @@ private partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax.
31 | .var n => match (index n binds) with
32 | .some i => .var (Var.bound (i, n))
33 | .none => .var (Var.free n)
34- | .op n args => Term.op n args
35+ | .op n args => Term.op n $ args.map $ fun n => Arg.var $
36+ match (index n binds) with
37+ | .some i => (Var.bound (i, n))
38+ | .none => Var.free n
39 | .forloop v collection terms =>
40 let range_bind := match (index collection binds) with
41 | .some i => (Var.bound (i, collection))
42@@ -62,7 +74,7 @@ section Test
43
44 #eval show Bool from
45 let t := fromSyntaxTerm (.op "hello" [ "world" ])
46- t == .op "hello" [ "world" ]
47+ t == .op "hello" [ Arg.var ( .free "world") ]
48
49 #eval show IO Bool from do
50 let t := fromSyntaxTerm (.forloop "x" "fruits" [ .text "world", .var "x" ])
+37,
-25
1@@ -20,79 +20,91 @@ partial instance : ToString Value where
2 | .list s => "[" ++ ",".intercalate (s.map toStr) ++ "]"
3 toStr
4
5+structure UserContext where
6+ data : Lean.HashMap String Value := Lean.HashMap.ofList []
7+ operators : Lean.HashMap String (Value -> IO Value) := Lean.HashMap.ofList []
8+
9 structure Context where
10 data : Lean.HashMap String Value := Lean.HashMap.ofList []
11- operators : Lean.HashMap String Value := Lean.HashMap.ofList []
12+ operators : Lean.HashMap String (Value -> IO Value) := Lean.HashMap.ofList []
13 binds : List Value := []
14
15-partial def eval (ctx : Context) (t : Term) : Except String String :=
16+private partial def eval' (ctx : Context) (t : Term) : IO String :=
17 match t with
18 | .text s => return s
19- | .op name _ =>
20+ | .op name args =>
21 match (Lean.HashMap.find? ctx.operators name) with
22- | .some (.text t) => return t
23- | _ => throw $ "\"" ++ name ++ "\" operator is not provided"
24+ | .some operator => do
25+ let resolvedArgs <- args.mapM $ fun (Arg.var v) => eval' ctx $ .var v
26+ let result <- operator $ match resolvedArgs with
27+ | [x] => .text x
28+ | _ => .list $ resolvedArgs.map .text
29+ return toString result
30+ | _ => throw $ IO.userError $ "\"" ++ name ++ "\" operator is not provided"
31 | .forloop v ts => do
32 let processVariable name o := match o with
33 | .some (.text t) => return t.toList.map $ fun c => .text ([c].asString)
34 | .some (.list vs) => return vs
35- | .none => throw $ "\"" ++ name ++ "\" is not provided"
36+ | .none => throw $ IO.userError $ "\"" ++ name ++ "\" is not provided"
37 let vals <- match v with
38 | .free n => processVariable n $ Lean.HashMap.find? ctx.data n
39 | .bound (i, n) => processVariable n ctx.binds[i]?
40- let processVal val := ts.mapM $ eval {ctx with binds := List.cons val ctx.binds }
41+ let processVal val := ts.mapM $ eval' {ctx with binds := List.cons val ctx.binds }
42 let results <- vals.mapM processVal
43 return String.join (results.map String.join)
44 | .var (.free n) => match (Lean.HashMap.find? ctx.data n) with
45 | .some v => return toString v
46- | .none => throw $ "\"" ++ n ++ "\" is not provided"
47+ | .none => throw $ IO.userError $ "\"" ++ n ++ "\" is not provided"
48 | .var (.bound (i, n)) => match ctx.binds[i]? with
49 | .some v => return toString v
50- | .none => throw $ "\"" ++ n ++ "\" is not defined in this scope"
51+ | .none => throw $ IO.userError $ "\"" ++ n ++ "\" is not defined in this scope"
52+
53+partial def eval (userContext : UserContext) : Term -> IO String :=
54+ TempleDeBruijnEval.eval' { data := userContext.data, operators := userContext.operators }
55
56 section Test
57
58-#eval show Bool from
59- let t := eval {} (.text "hello")
60- t.toOption == some "hello"
61+#eval show IO Bool from do
62+ let t <- eval {} (.text "hello")
63+ return (t == "hello")
64
65-#eval show Bool from
66- let t := eval ({operators := Lean.HashMap.ofList [ ( "hello", .text "world" ) ]}) (.op "hello" [])
67- t.toOption == some "world"
68+#eval show IO Bool from do
69+ let t <- eval ({operators := Lean.HashMap.ofList [ ( "hello", fun _ => return (Value.text "world") ) ]}) (.op "hello" [])
70+ return (t == "world")
71
72-#eval show Bool from
73- let t := eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
74+#eval show IO Bool from do
75+ let t <- eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
76 (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "0")) ])
77- t.toOption == some "hello worldhello land"
78+ return (t == "hello worldhello land")
79
80-#eval show Bool from
81- let t := eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
82+#eval show IO Bool from do
83+ let t <- eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
84 , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
85 (.forloop (Var.free "fruits")
86 [ .text "got an ", .var (.bound (0, "0")), .text "\n"
87 , .forloop (Var.free "vegetables") [ .var (.bound (0, "0")) ] ])
88- t.toOption == some "got an apple\nsaladoniongot an orange\nsaladonion"
89+ return (t == "got an apple\nsaladoniongot an orange\nsaladonion")
90
91-#eval show Except String String from
92+#eval show IO String from
93 eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
94 , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
95 (.forloop (Var.free "fruits")
96 [ .text "got an ", .var (.bound (0, "0")), .text "\n"
97 , .forloop (Var.free "vegetables") [ .var (.bound (1, "1")) ] ])
98
99-#eval show Except String String from
100+#eval show IO String from
101 try
102 eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
103 (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (1, "x")) ])
104 catch e => pure s!"Caught exception: {e}"
105
106-#eval show Except String String from
107+#eval show IO String from
108 try
109 eval ({data := Lean.HashMap.ofList [ ]})
110 (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "x")) ])
111 catch e => pure s!"Caught exception: {e}"
112
113-#eval show Except String String from
114+#eval show IO String from
115 try
116 eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
117 (.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ])
+29,
-20
1@@ -8,37 +8,33 @@ namespace TempleEval
2
3 open IO.FS
4
5-open TempleDeBruijnEval (Context)
6+open TempleDeBruijnEval
7
8-structure UserContext where
9- data : Lean.HashMap String Value
10- operators : Lean.HashMap String Value
11-
12-def runStringWith (c : Context) (s : String) : Except String String := do
13+def runStringWith (c : UserContext) (s : String) : IO String := do
14 let terms <- TempleSyntax.parse s
15 let deBruijnTerms := List.map TempleDeBruijn.fromSyntaxTerm terms
16 let results <- deBruijnTerms.mapM $ TempleDeBruijnEval.eval c
17 return String.join results
18
19-@[inline] def runString (s : String) : Except String String := runStringWith { } s
20+@[inline] def runString (s : String) : IO String := runStringWith { } s
21
22-@[inline] def runWith (c : Context) (fn : System.FilePath) : IO (Except String String) := do
23+@[inline] def runWith (c : UserContext) (fn : System.FilePath) : IO String := do
24 let s <- IO.FS.readFile fn
25- return runStringWith c s
26+ runStringWith c s
27
28-@[inline] def run (fn : System.FilePath) : IO (Except String String) := do
29+@[inline] def run (fn : System.FilePath) : IO String := do
30 let s <- IO.FS.readFile fn
31- return runString s
32+ runString s
33
34 section Test
35
36-#eval show Except String String from
37+#eval show IO String from
38 runStringWith {} "hello"
39
40-#eval show Except String String from
41+#eval show IO String from
42 runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"
43
44-#eval show Except String String from
45+#eval show IO String from
46 runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world"), ("xs", .list $ [ "1", "2", "3" ].map .text ) ] }
47 "hello {{ world }}
48
49@@ -47,30 +43,43 @@ section Test
50 {% endfor %}
51 "
52
53-#eval show IO Unit from
54+#eval show IO String from
55 let dataItems := Lean.HashMap.ofList
56 [ ("world", .text "world")
57 , ("xs", .list $ [ "1", "2", "3" ].map .text )
58 , ("ys", .list $ [ "4", "5", "6" ].map .text )
59 ]
60- let t := runStringWith { data := dataItems }
61+ 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+#eval show IO String from
70 let dataItems := Lean.HashMap.ofList
71 [ ("world", .text "world")
72 , ("xs", .list $ [ .text "1", .list [ .text "2", .text "3"], .text "4" ] )
73 ]
74- let t := runStringWith { data := dataItems }
75+ runStringWith { data := dataItems }
76 "hello {{ world }}
77 {% for x in xs %}
78 {% for y in x %}#{{ x }}{{y}} {% endfor %}
79 {% endfor %}"
80- IO.println t
81+
82+#eval show IO String from
83+ let dataItems := Lean.HashMap.ofList
84+ [ ("world", .text "world")
85+ , ("xs", .list [ .text "hello", .text "world"] )
86+ ]
87+ let toUpper (v : TempleDeBruijnEval.Value) := match v with
88+ | (TempleDeBruijnEval.Value.text t) => return TempleDeBruijnEval.Value.text (String.toUpper t)
89+ | _ => throw $ IO.userError "upper: list is not supported"
90+
91+ runStringWith { data := dataItems, operators := Lean.HashMap.ofList [ ("toUpper", toUpper) ] }
92+ "hello {{ world }}
93+{% for x in xs %}
94+ {% toUpper x %}
95+{% endfor %}"
96
97 end Test
98
+8,
-13
1@@ -91,40 +91,35 @@ end
2
3 end TempleParser
4
5-def parse (input : String) : Except String (List Term) :=
6+def parse (input : String) : IO (List Term) :=
7 match (TempleParser.terms <* Parser.endOfInput).run input.toSubstring with
8 | .ok _ t => return t
9- | .error e => throw $ "error: " ++ toString e
10+ | .error e => throw $ IO.userError $ "Parsing error: " ++ toString e
11
12 section Test
13
14-def terms (input : String) : IO (List Term) :=
15- match parse input with
16- | .ok t => IO.println t *> return t
17- | .error e => IO.println e *> return default
18-
19 #eval show IO Bool from do
20- let t <- terms "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"
21+ let t <- parse "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"
22 return t == [.text "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"]
23
24 #eval show IO Bool from do
25- let t <- terms "{{ myVariable }}"
26+ let t <- parse "{{ myVariable }}"
27 return t == [.var "myVariable"]
28
29 #eval show IO Bool from do
30- let t <- terms "hello {{ myVariable }}"
31+ let t <- parse "hello {{ myVariable }}"
32 return t == [.text "hello ", .var "myVariable"]
33
34 #eval show IO Bool from do
35- let t <- terms "{% my_operator s d %}"
36+ let t <- parse "{% my_operator s d %}"
37 return t == [.op "my_operator" [ "s", "d" ]]
38
39 #eval show IO Bool from do
40- let t <- terms "{% for x in fruits %}sadasd{{hello}}{% endfor %}"
41+ let t <- parse "{% for x in fruits %}sadasd{{hello}}{% endfor %}"
42 return t == [.forloop "x" "fruits" [ .text "sadasd", .var "hello" ]]
43
44 #eval show IO Bool from do
45- let t <- terms "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
46+ let t <- parse "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
47 return t == [.forloop "x" "fruits"
48 [ .text "hello", .forloop "y" "fruits" [ .text "world", .var "x", .var "y" ], .text "good" ]]
49