From 426ef4330ca9f055507f916495e74a2662848d08 Mon Sep 17 00:00:00 2001 From: Evgenii Akentev Date: Sun, 24 Mar 2024 22:24:08 +0400 Subject: [PATCH] It works. --- Temple.lean | 4 +- Temple/DeBruijn.lean | 35 +++++++------ Temple/DeBruijnEval.lean | 106 +++++++++++++++++++++++++++++++++++++++ Temple/Eval.lean | 21 ++++++++ Temple/Syntax.lean | 76 +++++++++++++++------------- 5 files changed, 187 insertions(+), 55 deletions(-) create mode 100644 Temple/DeBruijnEval.lean create mode 100644 Temple/Eval.lean diff --git a/Temple.lean b/Temple.lean index 81fe868..9cafd03 100644 --- a/Temple.lean +++ b/Temple.lean @@ -1,2 +1,4 @@ import Temple.Syntax -import Temple.DeBruijn \ No newline at end of file +import Temple.DeBruijn +import Temple.DeBruijnEval +import Temple.Eval \ No newline at end of file diff --git a/Temple/DeBruijn.lean b/Temple/DeBruijn.lean index f761fad..16569dd 100644 --- a/Temple/DeBruijn.lean +++ b/Temple/DeBruijn.lean @@ -3,14 +3,14 @@ import Temple.Syntax namespace TempleDeBruijn inductive Var -| bound : Int -> Var +| bound : Prod Nat String -> Var | free : String -> Var deriving BEq, Repr, Inhabited instance : ToString Var where toString - | .bound i => toString i - | .free s => s + | .bound (_ , n) => n + | .free n => n inductive Term | text : String -> Term @@ -26,30 +26,29 @@ partial instance : ToString Term where match x with | .text t => t | .var v => "{{ " ++ toString v ++ " }}" - | .op name args => "{% " ++ name ++ " " ++ (String.join (List.intersperse " " args)) ++ " %}" + | .op name args => "{% " ++ name ++ " " ++ (String.join $ List.intersperse " " args) ++ " %}" | .forloop name body => "{% for " ++ toString name ++ " %}\n" ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body))) ++ "\n{% endfor %}" toStr -def index (v : String) (binds : List String) : Option Nat := - List.lookup v (List.zip binds (List.range (List.length binds))) +@[inline] def index (v : String) (binds : List String) : Option Nat := List.lookup v (List.zip binds (List.range (List.length binds))) partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax.Term) : Term := match t with | .text t => Term.text t - | .var v => match (index v binds) with - | .some i => .var (Var.bound i) - | .none => .var (Var.free v) + | .var n => match (index n binds) with + | .some i => .var (Var.bound (i, n)) + | .none => .var (Var.free n) | .op n args => Term.op n args - | .forloop v range ts => - let range_bind := match (index range binds) with - | .some i => Var.bound i - | .none => Var.free range + | .forloop v collection ts => + let range_bind := match (index collection binds) with + | .some i => (Var.bound (i, collection)) + | .none => Var.free collection Term.forloop range_bind (List.map (fromSyntaxTermInner ([v] ++ binds)) ts) -def fromSyntaxTerm (t : TempleSyntax.Term) : Term := fromSyntaxTermInner [] t +@[inline] def fromSyntaxTerm (t : TempleSyntax.Term) : Term := fromSyntaxTermInner [] t section Test @@ -67,19 +66,19 @@ section Test #eval show IO Bool from do let t := fromSyntaxTerm (.forloop "x" "fruits" [ .text "world", .var "x" ]) - return t == .forloop (Var.free "fruits") [ .text "world", .var (.bound 0) ] + return t == .forloop (Var.free "fruits") [ .text "world", .var (.bound (0, "x")) ] #eval show IO Bool from do let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "vegetables" [ .var "x", .var "y" ] ]) - return t == .forloop (.free "fruits") [ .forloop (.free "vegetables") [ .var (.bound 1), .var (.bound 0) ] ] + return t == .forloop (.free "fruits") [ .forloop (.free "vegetables") [ .var (.bound (1, "x")), .var (.bound (0, "y")) ] ] #eval show IO Bool from do let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "x" [ .var "x", .var "y" ] ]) - return t == .forloop (.free "fruits") [ .forloop (.bound 0) [ .var (.bound 1), .var (.bound 0) ] ] + return t == .forloop (.free "fruits") [ .forloop (.bound (0, "x")) [ .var (.bound (1, "x")), .var (.bound (0, "y")) ] ] #eval show IO Bool from do let t := fromSyntaxTerm (.forloop "x" "fruits" [ .forloop "y" "x" [ .var "hello", .var "y" ] ]) - return t == .forloop (.free "fruits") [ .forloop (.bound 0) [ .var (.free "hello"), .var (.bound 0) ] ] + return t == .forloop (.free "fruits") [ .forloop (.bound (0, "x")) [ .var (.free "hello"), .var (.bound (0, "y")) ] ] end Test diff --git a/Temple/DeBruijnEval.lean b/Temple/DeBruijnEval.lean new file mode 100644 index 0000000..1272a0a --- /dev/null +++ b/Temple/DeBruijnEval.lean @@ -0,0 +1,106 @@ +import Lean.Data.HashMap + +import Temple.DeBruijn + +open TempleDeBruijn + +namespace TempleDeBruijnEval + +inductive Value where +| text : String -> Value +| list : List Value -> Value +deriving BEq, Repr, Inhabited + +partial instance : ToString Value where + toString := + let rec toStr x := + have : ToString Value := ⟨toStr⟩ + match x with + | .text s => s + | .list s => ", ".intercalate (s.map toStr) + toStr + +structure Context where + data : Lean.HashMap String Value + operators : Lean.HashMap String Value + binds : List Value + +def emptyCtx : Context := { binds := [], data := Lean.HashMap.ofList [], operators := Lean.HashMap.ofList []} + +partial def eval (ctx : Context) (t : Term) : Except String String := + match t with + | .text s => return s + | .op name _ => + match (Lean.HashMap.find? ctx.operators name) with + | .some (.text t) => return t + | _ => throw $ "\"" ++ name ++ "\" operator is not provided" + | .forloop v ts => do + let processVariable name o := match o with + | .some (.text t) => return t.toList.map $ fun c => .text ([c].asString) + | .some (.list vs) => return vs + | .none => throw $ "\"" ++ name ++ "\" is not provided" + let vals <- match v with + | .free n => processVariable n $ Lean.HashMap.find? ctx.data n + | .bound (i, n) => processVariable n ctx.binds[i]? + let processVal val := ts.mapM $ eval {ctx with binds := List.cons val ctx.binds } + let results <- vals.mapM processVal + return String.join (results.map String.join) + | .var (.free n) => match (Lean.HashMap.find? ctx.data n) with + | .some v => return toString v + | .none => throw $ "\"" ++ n ++ "\" is not provided" + | .var (.bound (i, n)) => match ctx.binds[i]? with + | .some v => return toString v + | .none => throw $ "\"" ++ n ++ "\" is not defined in this scope" + +section Test + +#eval show Bool from + let t := eval emptyCtx (.text "hello") + t.toOption == some "hello" + +#eval show Bool from + let t := eval ({emptyCtx with operators := Lean.HashMap.ofList [ ( "hello", .text "world" ) ]}) (.op "hello" []) + t.toOption == some "world" + +#eval show Bool from + let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]}) + (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "0")) ]) + t.toOption == some "hello worldhello land" + +#eval show Bool from + let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ]) + , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]}) + (.forloop (Var.free "fruits") + [ .text "got an ", .var (.bound (0, "0")), .text "\n" + , .forloop (Var.free "vegetables") [ .var (.bound (0, "0")) ] ]) + t.toOption == some "got an apple\nsaladoniongot an orange\nsaladonion" + +#eval show Except String String from + let t := eval ({emptyCtx with data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ]) + , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]}) + (.forloop (Var.free "fruits") + [ .text "got an ", .var (.bound (0, "0")), .text "\n" + , .forloop (Var.free "vegetables") [ .var (.bound (1, "1")) ] ]) + t + +#eval show Except String String from + try + eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]}) + (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (1, "x")) ]) + catch e => pure s!"Caught exception: {e}" + +#eval show Except String String from + try + eval ({emptyCtx with data := Lean.HashMap.ofList [ ]}) + (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "x")) ]) + catch e => pure s!"Caught exception: {e}" + +#eval show Except String String from + try + eval ({emptyCtx with data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]}) + (.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ]) + catch e => pure s!"Caught exception: {e}" + +end Test + +end TempleDeBruijnEval \ No newline at end of file diff --git a/Temple/Eval.lean b/Temple/Eval.lean new file mode 100644 index 0000000..3105f55 --- /dev/null +++ b/Temple/Eval.lean @@ -0,0 +1,21 @@ +import Temple.Syntax +import Temple.DeBruijn +import Temple.DeBruijnEval + +namespace TempleEval + +open TempleDeBruijnEval + +def eval (c : Context) (s : String) : Except String String := do + let terms <- TempleSyntax.parse s + let deBruijnTerms := List.map TempleDeBruijn.fromSyntaxTerm terms + let results <- deBruijnTerms.mapM $ TempleDeBruijnEval.eval c + return String.join results + +#eval show Except String String from + eval emptyCtx "hello" + +#eval show Except String String from + eval {emptyCtx with data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}" + +end TempleEval diff --git a/Temple/Syntax.lean b/Temple/Syntax.lean index e4f2f68..ef8b505 100644 --- a/Temple/Syntax.lean +++ b/Temple/Syntax.lean @@ -14,12 +14,12 @@ partial instance : ToString Term where let rec toStr x := have : ToString Term := ⟨toStr⟩ match x with - | .text t => t + | .text t => "\"" ++ t ++ "\"" | .var name => "{{ " ++ name ++ " }}" - | .op name args => "{% " ++ name ++ " " ++ (String.join (List.intersperse " " args)) ++ " %}" + | .op name args => "{% " ++ name ++ " " ++ (String.join $ args.intersperse " ") ++ " %}" | .forloop var collection body => "{% for " ++ var ++ " in " ++ collection ++ " %}\n" - ++ (String.join (List.intersperse "\n" (List.map (fun a => toStr a) body))) + ++ (String.join $ List.intersperse "\n" $ body.map toStr) ++ "\n{% endfor %}" toStr @@ -28,11 +28,11 @@ abbrev TempleParser := SimpleParser Substring Char namespace TempleParser open Parser Char -def spaces : TempleParser Unit := +@[inline] def spaces : TempleParser Unit := withErrorMessage "" do dropMany (char ' ') -def spaces1 : TempleParser Unit := +@[inline] def spaces1 : TempleParser Unit := withErrorMessage "" do dropMany1 (char ' ') @@ -47,83 +47,87 @@ partial def textInner (acc : String) : TempleParser String := return acc | none => do let c <- anyToken - textInner (String.push acc c) + textInner $ String.push acc c catch _ => return acc -partial def text : TempleParser Term := +@[inline] partial def text : TempleParser Term := withErrorMessage "" do let t <- textInner "" if t == "" then throwUnexpected else return Term.text t -def name : TempleParser String := +@[inline] def name : TempleParser String := withErrorMessage "" do - foldl String.push "" (ASCII.alphanum <|> char '_') + foldl String.push "" $ ASCII.alphanum <|> char '_' -def var : TempleParser Term := +@[inline] def var : TempleParser Term := withErrorMessage "" do let n <- spaces *> chars "{{" *> spaces *> name <* spaces <* chars "}}" return Term.var n -def op : TempleParser Term := +@[inline] 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)) + return Term.op n (List.cons firstArg $ args.toList.filter (fun a => !a.isEmpty)) mutual partial def forloop : TempleParser Term := withErrorMessage "" do - let _ <- spaces *> chars "{%" *> spaces *> chars "for" + let _ <- chars "{%" *> spaces *> chars "for" let v <- spaces1 *> name <* spaces1 <* chars "in" let collection <- spaces1 *> name <* spaces <* chars "%}" - let terms <- spaces *> takeMany term + let parsedTerms <- terms - let _ <- spaces *> chars "{%" *> spaces *> chars "endfor" *> spaces <* chars "%}" - return Term.forloop v collection (Array.toList terms) + let _ <- chars "{%" *> spaces *> chars "endfor" *> spaces <* chars "%}" + return Term.forloop v collection parsedTerms - partial def term : TempleParser Term := + partial def terms : TempleParser (List Term) := withErrorMessage "" do - let t <- withErrorMessage ": expected term" - (forloop <|> op <|> var <|> text) - return t + let t <- withErrorMessage ": expected terms" + $ takeMany $ forloop <|> op <|> var <|> text + return t.toList 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) +def parse (input : String) : Except String (List Term) := + match (TempleParser.terms <* Parser.endOfInput).run input.toSubstring with + | .ok _ t => return t + | .error e => throw $ "error: " ++ toString e section Test -protected def term (input : String) : IO Term := +def terms (input : String) : IO (List 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" + let t <- terms "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd" + return t == [.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" + let t <- terms "{{ myVariable }}" + return t == [.var "myVariable"] #eval show IO Bool from do - let t <- TempleSyntax.term "{% my_operator s d %}" - return t == Term.op "my_operator" [ "s", "d" ] + let t <- terms "hello {{ myVariable }}" + return t == [.text "hello ", .var "myVariable"] #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" ] + let t <- terms "{% my_operator s d %}" + return t == [.op "my_operator" [ "s", "d" ]] #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" ] + let t <- terms "{% for x in fruits %}sadasd{{hello}}{% endfor %}" + return t == [.forloop "x" "fruits" [ .text "sadasd", .var "hello" ]] + +#eval show IO Bool from do + let t <- terms "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}" + return t == [.forloop "x" "fruits" + [ .text "hello", .forloop "y" "fruits" [ .text "world", .var "x", .var "y" ], .text "good" ]] end Test -- 2.34.1