- commit
- 426ef43
- parent
- 001063c
- author
- Evgenii Akentev
- date
- 2024-03-24 22:24:08 +0400 +04
It works.
5 files changed,
+187,
-55
+3,
-1
1@@ -1,2 +1,4 @@
2 import Temple.Syntax
3-import Temple.DeBruijn
4+import Temple.DeBruijn
5+import Temple.DeBruijnEval
6+import Temple.Eval
+17,
-18
1@@ -3,14 +3,14 @@ import Temple.Syntax
2 namespace TempleDeBruijn
3
4 inductive Var
5-| bound : Int -> Var
6+| bound : Prod Nat String -> Var
7 | free : String -> Var
8 deriving BEq, Repr, Inhabited
9
10 instance : ToString Var where
11 toString
12- | .bound i => toString i
13- | .free s => s
14+ | .bound (_ , n) => n
15+ | .free n => n
16
17 inductive Term
18 | text : String -> Term
19@@ -26,30 +26,29 @@ partial instance : ToString Term where
20 match x with
21 | .text t => t
22 | .var v => "{{ " ++ toString v ++ " }}"
23- | .op name args => "{% " ++ name ++ " " ++ (String.join (List.intersperse " " args)) ++ " %}"
24+ | .op name args => "{% " ++ name ++ " " ++ (String.join $ List.intersperse " " args) ++ " %}"
25 | .forloop name body =>
26 "{% for " ++ toString name ++ " %}\n"
27 ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body)))
28 ++ "\n{% endfor %}"
29 toStr
30
31-def index (v : String) (binds : List String) : Option Nat :=
32- List.lookup v (List.zip binds (List.range (List.length binds)))
33+@[inline] def index (v : String) (binds : List String) : Option Nat := List.lookup v (List.zip binds (List.range (List.length binds)))
34
35 partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax.Term) : Term :=
36 match t with
37 | .text t => Term.text t
38- | .var v => match (index v binds) with
39- | .some i => .var (Var.bound i)
40- | .none => .var (Var.free v)
41+ | .var n => match (index n binds) with
42+ | .some i => .var (Var.bound (i, n))
43+ | .none => .var (Var.free n)
44 | .op n args => Term.op n args
45- | .forloop v range ts =>
46- let range_bind := match (index range binds) with
47- | .some i => Var.bound i
48- | .none => Var.free range
49+ | .forloop v collection ts =>
50+ let range_bind := match (index collection binds) with
51+ | .some i => (Var.bound (i, collection))
52+ | .none => Var.free collection
53 Term.forloop range_bind (List.map (fromSyntaxTermInner ([v] ++ binds)) ts)
54
55-def fromSyntaxTerm (t : TempleSyntax.Term) : Term := fromSyntaxTermInner [] t
56+@[inline] def fromSyntaxTerm (t : TempleSyntax.Term) : Term := fromSyntaxTermInner [] t
57
58 section Test
59
60@@ -67,19 +66,19 @@ section Test
61
62 #eval show IO Bool from do
63 let t := fromSyntaxTerm (.forloop "x" "fruits" [ .text "world", .var "x" ])
64- return t == .forloop (Var.free "fruits") [ .text "world", .var (.bound 0) ]
65+ return t == .forloop (Var.free "fruits") [ .text "world", .var (.bound (0, "x")) ]
66
67 #eval show IO Bool from do
68 let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "vegetables" [ .var "x", .var "y" ] ])
69- return t == .forloop (.free "fruits") [ .forloop (.free "vegetables") [ .var (.bound 1), .var (.bound 0) ] ]
70+ return t == .forloop (.free "fruits") [ .forloop (.free "vegetables") [ .var (.bound (1, "x")), .var (.bound (0, "y")) ] ]
71
72 #eval show IO Bool from do
73 let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "x" [ .var "x", .var "y" ] ])
74- return t == .forloop (.free "fruits") [ .forloop (.bound 0) [ .var (.bound 1), .var (.bound 0) ] ]
75+ return t == .forloop (.free "fruits") [ .forloop (.bound (0, "x")) [ .var (.bound (1, "x")), .var (.bound (0, "y")) ] ]
76
77 #eval show IO Bool from do
78 let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "x" [ .var "hello", .var "y" ] ])
79- return t == .forloop (.free "fruits") [ .forloop (.bound 0) [ .var (.free "hello"), .var (.bound 0) ] ]
80+ return t == .forloop (.free "fruits") [ .forloop (.bound (0, "x")) [ .var (.free "hello"), .var (.bound (0, "y")) ] ]
81
82 end Test
83
+106,
-0
1@@ -0,0 +1,106 @@
2+import Lean.Data.HashMap
3+
4+import Temple.DeBruijn
5+
6+open TempleDeBruijn
7+
8+namespace TempleDeBruijnEval
9+
10+inductive Value where
11+| text : String -> Value
12+| list : List Value -> Value
13+deriving BEq, Repr, Inhabited
14+
15+partial instance : ToString Value where
16+ toString :=
17+ let rec toStr x :=
18+ have : ToString Value := ⟨toStr⟩
19+ match x with
20+ | .text s => s
21+ | .list s => ", ".intercalate (s.map toStr)
22+ toStr
23+
24+structure Context where
25+ data : Lean.HashMap String Value
26+ operators : Lean.HashMap String Value
27+ binds : List Value
28+
29+def emptyCtx : Context := { binds := [], data := Lean.HashMap.ofList [], operators := Lean.HashMap.ofList []}
30+
31+partial def eval (ctx : Context) (t : Term) : Except String String :=
32+ match t with
33+ | .text s => return s
34+ | .op name _ =>
35+ match (Lean.HashMap.find? ctx.operators name) with
36+ | .some (.text t) => return t
37+ | _ => throw $ "\"" ++ name ++ "\" operator is not provided"
38+ | .forloop v ts => do
39+ let processVariable name o := match o with
40+ | .some (.text t) => return t.toList.map $ fun c => .text ([c].asString)
41+ | .some (.list vs) => return vs
42+ | .none => throw $ "\"" ++ name ++ "\" is not provided"
43+ let vals <- match v with
44+ | .free n => processVariable n $ Lean.HashMap.find? ctx.data n
45+ | .bound (i, n) => processVariable n ctx.binds[i]?
46+ let processVal val := ts.mapM $ eval {ctx with binds := List.cons val ctx.binds }
47+ let results <- vals.mapM processVal
48+ return String.join (results.map String.join)
49+ | .var (.free n) => match (Lean.HashMap.find? ctx.data n) with
50+ | .some v => return toString v
51+ | .none => throw $ "\"" ++ n ++ "\" is not provided"
52+ | .var (.bound (i, n)) => match ctx.binds[i]? with
53+ | .some v => return toString v
54+ | .none => throw $ "\"" ++ n ++ "\" is not defined in this scope"
55+
56+section Test
57+
58+#eval show Bool from
59+ let t := eval emptyCtx (.text "hello")
60+ t.toOption == some "hello"
61+
62+#eval show Bool from
63+ let t := eval ({emptyCtx with operators := Lean.HashMap.ofList [ ( "hello", .text "world" ) ]}) (.op "hello" [])
64+ t.toOption == some "world"
65+
66+#eval show Bool from
67+ let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
68+ (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "0")) ])
69+ t.toOption == some "hello worldhello land"
70+
71+#eval show Bool from
72+ let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
73+ , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
74+ (.forloop (Var.free "fruits")
75+ [ .text "got an ", .var (.bound (0, "0")), .text "\n"
76+ , .forloop (Var.free "vegetables") [ .var (.bound (0, "0")) ] ])
77+ t.toOption == some "got an apple\nsaladoniongot an orange\nsaladonion"
78+
79+#eval show Except String String from
80+ let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
81+ , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
82+ (.forloop (Var.free "fruits")
83+ [ .text "got an ", .var (.bound (0, "0")), .text "\n"
84+ , .forloop (Var.free "vegetables") [ .var (.bound (1, "1")) ] ])
85+ t
86+
87+#eval show Except String String from
88+ try
89+ eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
90+ (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (1, "x")) ])
91+ catch e => pure s!"Caught exception: {e}"
92+
93+#eval show Except String String from
94+ try
95+ eval ({emptyCtx with data := Lean.HashMap.ofList [ ]})
96+ (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "x")) ])
97+ catch e => pure s!"Caught exception: {e}"
98+
99+#eval show Except String String from
100+ try
101+ eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
102+ (.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ])
103+ catch e => pure s!"Caught exception: {e}"
104+
105+end Test
106+
107+end TempleDeBruijnEval
+21,
-0
1@@ -0,0 +1,21 @@
2+import Temple.Syntax
3+import Temple.DeBruijn
4+import Temple.DeBruijnEval
5+
6+namespace TempleEval
7+
8+open TempleDeBruijnEval
9+
10+def eval (c : Context) (s : String) : Except String String := do
11+ let terms <- TempleSyntax.parse s
12+ let deBruijnTerms := List.map TempleDeBruijn.fromSyntaxTerm terms
13+ let results <- deBruijnTerms.mapM $ TempleDeBruijnEval.eval c
14+ return String.join results
15+
16+#eval show Except String String from
17+ eval emptyCtx "hello"
18+
19+#eval show Except String String from
20+ eval {emptyCtx with data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"
21+
22+end TempleEval
+40,
-36
1@@ -14,12 +14,12 @@ partial instance : ToString Term where
2 let rec toStr x :=
3 have : ToString Term := ⟨toStr⟩
4 match x with
5- | .text t => t
6+ | .text t => "\"" ++ t ++ "\""
7 | .var name => "{{ " ++ name ++ " }}"
8- | .op name args => "{% " ++ name ++ " " ++ (String.join (List.intersperse " " args)) ++ " %}"
9+ | .op name args => "{% " ++ name ++ " " ++ (String.join $ args.intersperse " ") ++ " %}"
10 | .forloop var collection body =>
11 "{% for " ++ var ++ " in " ++ collection ++ " %}\n"
12- ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body)))
13+ ++ (String.join $ List.intersperse "\n" $ body.map toStr)
14 ++ "\n{% endfor %}"
15 toStr
16
17@@ -28,11 +28,11 @@ abbrev TempleParser := SimpleParser Substring Char
18 namespace TempleParser
19 open Parser Char
20
21-def spaces : TempleParser Unit :=
22+@[inline] def spaces : TempleParser Unit :=
23 withErrorMessage "<spaces>" do
24 dropMany (char ' ')
25
26-def spaces1 : TempleParser Unit :=
27+@[inline] def spaces1 : TempleParser Unit :=
28 withErrorMessage "<spaces1>" do
29 dropMany1 (char ' ')
30
31@@ -47,83 +47,87 @@ partial def textInner (acc : String) : TempleParser String :=
32 return acc
33 | none => do
34 let c <- anyToken
35- textInner (String.push acc c)
36+ textInner $ String.push acc c
37 catch _ => return acc
38
39-partial def text : TempleParser Term :=
40+@[inline] partial def text : TempleParser Term :=
41 withErrorMessage "<text>" do
42 let t <- textInner ""
43 if t == "" then throwUnexpected else return Term.text t
44
45-def name : TempleParser String :=
46+@[inline] def name : TempleParser String :=
47 withErrorMessage "<name>" do
48- foldl String.push "" (ASCII.alphanum <|> char '_')
49+ foldl String.push "" $ ASCII.alphanum <|> char '_'
50
51-def var : TempleParser Term :=
52+@[inline] def var : TempleParser Term :=
53 withErrorMessage "<var>" do
54 let n <- spaces *> chars "{{" *> spaces *> name <* spaces <* chars "}}"
55 return Term.var n
56
57-def op : TempleParser Term :=
58+@[inline] def op : TempleParser Term :=
59 withErrorMessage "<op>" do
60 let n <- spaces *> chars "{%" *> spaces *> name
61 let firstArg <- spaces1 *> name
62 let args <- spaces1 *> (sepBy1 spaces1 name) <* spaces <* chars "%}"
63- return Term.op n ([firstArg] ++ List.filter (fun a => !String.isEmpty a) (Array.toList args))
64+ return Term.op n (List.cons firstArg $ args.toList.filter (fun a => !a.isEmpty))
65
66 mutual
67 partial def forloop : TempleParser Term :=
68 withErrorMessage "<forloop>" do
69- let _ <- spaces *> chars "{%" *> spaces *> chars "for"
70+ let _ <- chars "{%" *> spaces *> chars "for"
71 let v <- spaces1 *> name <* spaces1 <* chars "in"
72 let collection <- spaces1 *> name <* spaces <* chars "%}"
73
74- let terms <- spaces *> takeMany term
75+ let parsedTerms <- terms
76
77- let _ <- spaces *> chars "{%" *> spaces *> chars "endfor" *> spaces <* chars "%}"
78- return Term.forloop v collection (Array.toList terms)
79+ let _ <- chars "{%" *> spaces *> chars "endfor" *> spaces <* chars "%}"
80+ return Term.forloop v collection parsedTerms
81
82- partial def term : TempleParser Term :=
83+ partial def terms : TempleParser (List Term) :=
84 withErrorMessage "<term>" do
85- let t <- withErrorMessage "<term>: expected term"
86- (forloop <|> op <|> var <|> text)
87- return t
88+ let t <- withErrorMessage "<term>: expected terms"
89+ $ takeMany $ forloop <|> op <|> var <|> text
90+ return t.toList
91 end
92
93 end TempleParser
94
95-def parse (input : String) : Except String Term :=
96- match (TempleParser.term <* Parser.endOfInput).run input.toSubstring with
97- | .ok _ t => .ok t
98- | .error e => .error ("error: " ++ toString e)
99+def parse (input : String) : Except String (List Term) :=
100+ match (TempleParser.terms <* Parser.endOfInput).run input.toSubstring with
101+ | .ok _ t => return t
102+ | .error e => throw $ "error: " ++ toString e
103
104 section Test
105
106-protected def term (input : String) : IO Term :=
107+def terms (input : String) : IO (List Term) :=
108 match parse input with
109 | .ok t => IO.println t *> return t
110 | .error e => IO.println e *> return default
111
112 #eval show IO Bool from do
113- let t <- TempleSyntax.term "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"
114- return t == Term.text "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"
115+ let t <- terms "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"
116+ return t == [.text "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"]
117
118 #eval show IO Bool from do
119- let t <- TempleSyntax.term "{{ myVariable }}"
120- return t == Term.var "myVariable"
121+ let t <- terms "{{ myVariable }}"
122+ return t == [.var "myVariable"]
123
124 #eval show IO Bool from do
125- let t <- TempleSyntax.term "{% my_operator s d %}"
126- return t == Term.op "my_operator" [ "s", "d" ]
127+ let t <- terms "hello {{ myVariable }}"
128+ return t == [.text "hello ", .var "myVariable"]
129
130 #eval show IO Bool from do
131- let t <- TempleSyntax.term "{% for x in fruits %}sadasd{{hello}}{% endfor %}"
132- return t == Term.forloop "x" "fruits" [ Term.text "sadasd", Term.var "hello" ]
133+ let t <- terms "{% my_operator s d %}"
134+ return t == [.op "my_operator" [ "s", "d" ]]
135
136 #eval show IO Bool from do
137- let t <- TempleSyntax.term "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
138- return t == Term.forloop "x" "fruits"
139- [ Term.text "hello", Term.forloop "y" "fruits" [ Term.text "world", Term.var "x", Term.var "y" ], Term.text "good" ]
140+ let t <- terms "{% for x in fruits %}sadasd{{hello}}{% endfor %}"
141+ return t == [.forloop "x" "fruits" [ .text "sadasd", .var "hello" ]]
142+
143+#eval show IO Bool from do
144+ let t <- terms "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
145+ return t == [.forloop "x" "fruits"
146+ [ .text "hello", .forloop "y" "fruits" [ .text "world", .var "x", .var "y" ], .text "good" ]]
147
148 end Test
149