From 0fe449a4e535f30ef1d93a83a880e631e9015888 Mon Sep 17 00:00:00 2001 From: Evgenii Akentev Date: Sun, 24 Mar 2024 13:06:11 +0400 Subject: [PATCH] Add simple parser --- .gitignore | 1 + Temple.lean | 1 + Temple/Syntax.lean | 130 +++++++++++++++++++++++++++++++++++++++++++++ lake-manifest.json | 32 +++++++++++ lakefile.lean | 15 ++++++ 5 files changed, 179 insertions(+) create mode 100644 .gitignore create mode 100644 Temple.lean create mode 100644 Temple/Syntax.lean create mode 100644 lake-manifest.json create mode 100644 lakefile.lean diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/Temple.lean b/Temple.lean new file mode 100644 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 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 "" do + dropMany (char ' ') + +def spaces1 : TempleParser Unit := + withErrorMessage "" do + dropMany1 (char ' ') + +partial def textInner (acc : String) : TempleParser String := + withErrorMessage "" 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 "" do + let t <- textInner "" + if t == "" then throwUnexpected else return Term.text t + +def name : TempleParser String := + withErrorMessage "" do + foldl String.push "" (ASCII.alphanum <|> char '_') + +def var : TempleParser Term := + withErrorMessage "" do + let n <- spaces *> chars "{{" *> spaces *> name <* spaces <* chars "}}" + return Term.var n + +def op : TempleParser Term := + withErrorMessage "" 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 "" 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 "" do + let t <- withErrorMessage ": 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 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 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» -- 2.34.1