- commit
- 0fe449a
- parent
- 0fe449a
- author
- Evgenii Akentev
- date
- 2024-03-24 13:06:11 +0400 +04
Add simple parser
5 files changed,
+179,
-0
+1,
-0
1@@ -0,0 +1 @@
2+/.lake
+1,
-0
1@@ -0,0 +1 @@
2+import «Temple».Syntax
+130,
-0
1@@ -0,0 +1,130 @@
2+import Parser
3+
4+namespace TempleSyntax
5+
6+inductive Term
7+| text : String -> Term
8+| var : String -> Term
9+| op : String -> List String -> Term
10+| forloop : String -> String -> List Term -> Term
11+deriving BEq, Repr, Inhabited
12+
13+partial instance : ToString Term where
14+ toString :=
15+ let rec toStr x :=
16+ have : ToString Term := ⟨toStr⟩
17+ match x with
18+ | .text t => t
19+ | .var name => "{{ " ++ name ++ " }}"
20+ | .op name args => "{% " ++ name ++ " " ++ (String.join (List.intersperse " " args)) ++ " %}"
21+ | .forloop var collection body =>
22+ "{% for " ++ var ++ " in " ++ collection ++ " %}\n"
23+ ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body)))
24+ ++ "\n{% endfor %}"
25+ toStr
26+
27+abbrev TempleParser := SimpleParser Substring Char
28+
29+namespace TempleParser
30+open Parser Char
31+
32+def spaces : TempleParser Unit :=
33+ withErrorMessage "<spaces>" do
34+ dropMany (char ' ')
35+
36+def spaces1 : TempleParser Unit :=
37+ withErrorMessage "<spaces1>" do
38+ dropMany1 (char ' ')
39+
40+partial def textInner (acc : String) : TempleParser String :=
41+ withErrorMessage "<text>" do
42+
43+ try
44+ let savePos <- getPosition
45+ match <- option? (chars "{{" <|> chars "{%") with
46+ | some _ => do
47+ setPosition savePos false
48+ return acc
49+ | none => do
50+ let c <- anyToken
51+ textInner (String.push acc c)
52+ catch _ => return acc
53+
54+partial def text : TempleParser Term :=
55+ withErrorMessage "<text>" do
56+ let t <- textInner ""
57+ if t == "" then throwUnexpected else return Term.text t
58+
59+def name : TempleParser String :=
60+ withErrorMessage "<name>" do
61+ foldl String.push "" (ASCII.alphanum <|> char '_')
62+
63+def var : TempleParser Term :=
64+ withErrorMessage "<var>" do
65+ let n <- spaces *> chars "{{" *> spaces *> name <* spaces <* chars "}}"
66+ return Term.var n
67+
68+def op : TempleParser Term :=
69+ withErrorMessage "<op>" do
70+ let n <- spaces *> chars "{%" *> spaces *> name
71+ let firstArg <- spaces1 *> name
72+ let args <- spaces1 *> (sepBy1 spaces1 name) <* spaces <* chars "%}"
73+ return Term.op n ([firstArg] ++ List.filter (fun a => !String.isEmpty a) (Array.toList args))
74+
75+mutual
76+ partial def forloop : TempleParser Term :=
77+ withErrorMessage "<forloop>" do
78+ let _ <- spaces *> chars "{%" *> spaces *> chars "for"
79+ let v <- spaces1 *> name <* spaces1 <* chars "in"
80+ let collection <- spaces1 *> name <* spaces <* chars "%}"
81+
82+ let terms <- spaces *> takeMany term
83+
84+ let _ <- spaces *> chars "{%" *> spaces *> chars "endfor" *> spaces <* chars "%}"
85+ return Term.forloop v collection (Array.toList terms)
86+
87+ partial def term : TempleParser Term :=
88+ withErrorMessage "<term>" do
89+ let t <- withErrorMessage "<term>: expected term"
90+ (forloop <|> op <|> var <|> text)
91+ return t
92+end
93+
94+end TempleParser
95+
96+def parse (input : String) : Except String Term :=
97+ match (TempleParser.term <* Parser.endOfInput).run input.toSubstring with
98+ | .ok _ t => .ok t
99+ | .error e => .error ("error: " ++ toString e)
100+
101+section Test
102+
103+protected def term (input : String) : IO Term :=
104+ match parse input with
105+ | .ok t => IO.println t *> return t
106+ | .error e => IO.println e *> return default
107+
108+#eval show IO Bool from do
109+ let t <- TempleSyntax.term "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"
110+ return t == Term.text "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"
111+
112+#eval show IO Bool from do
113+ let t <- TempleSyntax.term "{{ myVariable }}"
114+ return t == Term.var "myVariable"
115+
116+#eval show IO Bool from do
117+ let t <- TempleSyntax.term "{% my_operator s d %}"
118+ return t == Term.op "my_operator" [ "s", "d" ]
119+
120+#eval show IO Bool from do
121+ let t <- TempleSyntax.term "{% for x in fruits %}sadasd{{hello}}{% endfor %}"
122+ return t == Term.forloop "x" "fruits" [ Term.text "sadasd", Term.var "hello" ]
123+
124+#eval show IO Bool from do
125+ let t <- TempleSyntax.term "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
126+ return t == Term.forloop "x" "fruits"
127+ [ Term.text "hello", Term.forloop "y" "fruits" [ Term.text "world", Term.var "x", Term.var "y" ], Term.text "good" ]
128+
129+end Test
130+
131+end TempleSyntax
+32,
-0
1@@ -0,0 +1,32 @@
2+{"version": 7,
3+ "packagesDir": ".lake/packages",
4+ "packages":
5+ [{"url": "https://github.com/leanprover/std4",
6+ "type": "git",
7+ "subDir": null,
8+ "rev": "6b203c31b414beb758ef9b7fdc71b01d144504ad",
9+ "name": "std",
10+ "manifestFile": "lake-manifest.json",
11+ "inputRev": "main",
12+ "inherited": false,
13+ "configFile": "lakefile.lean"},
14+ {"url": "https://github.com/fgdorais/lean4-unicode-basic",
15+ "type": "git",
16+ "subDir": null,
17+ "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9",
18+ "name": "UnicodeBasic",
19+ "manifestFile": "lake-manifest.json",
20+ "inputRev": "main",
21+ "inherited": false,
22+ "configFile": "lakefile.lean"},
23+ {"url": "https://github.com/fgdorais/lean4-parser",
24+ "type": "git",
25+ "subDir": null,
26+ "rev": "4ae54daeb1e7c1c0b1d34bf314338c49819599d9",
27+ "name": "Parser",
28+ "manifestFile": "lake-manifest.json",
29+ "inputRev": "main",
30+ "inherited": false,
31+ "configFile": "lakefile.lean"}],
32+ "name": "temple",
33+ "lakeDir": ".lake"}
+15,
-0
1@@ -0,0 +1,15 @@
2+import Lake
3+open Lake DSL
4+
5+require std from git
6+ "https://github.com/leanprover/std4" @ "main"
7+
8+require UnicodeBasic from git
9+ "https://github.com/fgdorais/lean4-unicode-basic" @ "main"
10+
11+require Parser from git "https://github.com/fgdorais/lean4-parser" @ "main"
12+
13+package «temple»
14+
15+@[default_target]
16+lean_lib «Temple»