Add simple parser

diff --git a/.gitignore b/.gitignore
new file mode 100644 (file)
index 0000000..bfb30ec
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/.lake

diff --git a/Temple.lean b/Temple.lean
new file mode 100644 (file)
index 0000000..8b015eb
--- /dev/null
+++ b/Temple.lean
@@ -0,0 +1 @@
+import «Temple».Syntax
\ No newline at end of file

diff --git a/Temple/Syntax.lean b/Temple/Syntax.lean
new file mode 100644 (file)
index 0000000..e4f2f68
--- /dev/null
+++ b/Temple/Syntax.lean
@@ -0,0 +1,130 @@
+import Parser
+
+namespace TempleSyntax
+
+inductive Term
+| text : String -> Term
+| var : String -> Term
+| op : String -> List String -> Term
+| forloop : String -> String -> List Term -> Term
+deriving BEq, Repr, Inhabited
+
+partial instance : ToString Term where
+  toString :=
+    let rec toStr x :=
+      have : ToString Term := ⟨toStr⟩
+      match x with
+      | .text t => t
+      | .var name => "{{ " ++ name ++ " }}"
+      | .op name args => "{% " ++ name ++ " " ++ (String.join (List.intersperse " " args)) ++ " %}"
+      | .forloop var collection body =>
+        "{% for " ++ var ++ " in " ++ collection ++ " %}\n"
+          ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body)))
+          ++ "\n{% endfor %}"
+    toStr
+
+abbrev TempleParser := SimpleParser Substring Char
+
+namespace TempleParser
+open Parser Char
+
+def spaces : TempleParser Unit :=
+  withErrorMessage "<spaces>" do
+    dropMany (char ' ')
+
+def spaces1 : TempleParser Unit :=
+  withErrorMessage "<spaces1>" do
+    dropMany1 (char ' ')
+
+partial def textInner (acc : String) : TempleParser String :=
+  withErrorMessage "<text>" do
+
+    try
+      let savePos <- getPosition
+      match <- option? (chars "{{" <|> chars "{%") with
+        | some _ => do
+          setPosition savePos false
+          return acc
+        | none => do
+          let c <- anyToken
+          textInner (String.push acc c)
+    catch _ => return acc
+
+partial def text : TempleParser Term :=
+  withErrorMessage "<text>" do
+    let t <- textInner ""
+    if t == "" then throwUnexpected else return Term.text t
+
+def name : TempleParser String :=
+  withErrorMessage "<name>" do
+    foldl String.push "" (ASCII.alphanum <|> char '_')
+
+def var : TempleParser Term :=
+  withErrorMessage "<var>" do
+    let n <- spaces *> chars "{{" *> spaces *> name <* spaces <* chars "}}"
+    return Term.var n
+
+def op : TempleParser Term :=
+  withErrorMessage "<op>" do
+    let n <- spaces *> chars "{%" *> spaces *> name
+    let firstArg <- spaces1 *> name
+    let args <- spaces1 *> (sepBy1 spaces1 name) <* spaces <* chars "%}"
+    return Term.op n ([firstArg] ++ List.filter (fun a => !String.isEmpty a) (Array.toList args))
+
+mutual
+  partial def forloop : TempleParser Term :=
+    withErrorMessage "<forloop>" do
+      let _ <- spaces *> chars "{%" *> spaces *> chars "for"
+      let v <- spaces1 *> name <* spaces1 <* chars "in"
+      let collection <- spaces1 *> name <* spaces <* chars "%}"
+
+      let terms <- spaces *> takeMany term
+
+      let _ <- spaces *> chars "{%" *> spaces *> chars "endfor" *> spaces <* chars "%}"
+      return Term.forloop v collection (Array.toList terms)
+
+  partial def term : TempleParser Term :=
+    withErrorMessage "<term>" do
+      let t <- withErrorMessage "<term>: expected term"
+        (forloop <|> op <|> var <|> text)
+      return t
+end
+
+end TempleParser
+
+def parse (input : String) : Except String Term :=
+  match (TempleParser.term <* Parser.endOfInput).run input.toSubstring with
+  | .ok _ t => .ok t
+  | .error e => .error ("error: " ++ toString e)
+
+section Test
+
+protected def term (input : String) : IO Term :=
+  match parse input with
+  | .ok t => IO.println t *> return t
+  | .error e => IO.println e *> return default
+
+#eval show IO Bool from do
+  let t <- TempleSyntax.term "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"
+  return t == Term.text "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"
+
+#eval show IO Bool from do
+ let t <- TempleSyntax.term "{{ myVariable }}"
+ return t == Term.var "myVariable"
+
+#eval show IO Bool from do
+ let t <- TempleSyntax.term "{% my_operator s   d %}"
+ return t == Term.op "my_operator" [ "s", "d" ]
+
+#eval show IO Bool from do
+  let t <- TempleSyntax.term "{% for    x     in      fruits %}sadasd{{hello}}{% endfor %}"
+  return t == Term.forloop "x" "fruits" [ Term.text "sadasd", Term.var "hello" ]
+
+#eval show IO Bool from do
+  let t <- TempleSyntax.term "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
+  return t == Term.forloop "x" "fruits"
+    [ Term.text "hello", Term.forloop "y" "fruits" [ Term.text "world", Term.var "x", Term.var "y" ], Term.text "good" ]
+
+end Test
+
+end TempleSyntax
\ No newline at end of file

diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644 (file)
index 0000000..0f1db72
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,32 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "6b203c31b414beb758ef9b7fdc71b01d144504ad",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-parser",
+   "type": "git",
+   "subDir": null,
+   "rev": "4ae54daeb1e7c1c0b1d34bf314338c49819599d9",
+   "name": "Parser",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "temple",
+ "lakeDir": ".lake"}

diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644 (file)
index 0000000..e32f6a7
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,15 @@
+import Lake
+open Lake DSL
+
+require std from git
+  "https://github.com/leanprover/std4" @ "main"
+
+require UnicodeBasic from git
+  "https://github.com/fgdorais/lean4-unicode-basic" @ "main"
+
+require Parser from git "https://github.com/fgdorais/lean4-parser" @ "main"
+
+package «temple»
+
+@[default_target]
+lean_lib «Temple»