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
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
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
#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
--- /dev/null
+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
--- /dev/null
+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
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
namespace TempleParser
open Parser Char
-def spaces : TempleParser Unit :=
+@[inline] def spaces : TempleParser Unit :=
withErrorMessage "<spaces>" do
dropMany (char ' ')
-def spaces1 : TempleParser Unit :=
+@[inline] def spaces1 : TempleParser Unit :=
withErrorMessage "<spaces1>" do
dropMany1 (char ' ')
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 "<text>" do
let t <- textInner ""
if t == "" then throwUnexpected else return Term.text t
-def name : TempleParser String :=
+@[inline] def name : TempleParser String :=
withErrorMessage "<name>" do
- foldl String.push "" (ASCII.alphanum <|> char '_')
+ foldl String.push "" $ ASCII.alphanum <|> char '_'
-def var : TempleParser Term :=
+@[inline] def var : TempleParser Term :=
withErrorMessage "<var>" do
let n <- spaces *> chars "{{" *> spaces *> name <* spaces <* chars "}}"
return Term.var n
-def op : TempleParser Term :=
+@[inline] 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))
+ return Term.op n (List.cons firstArg $ args.toList.filter (fun a => !a.isEmpty))
mutual
partial def forloop : TempleParser Term :=
withErrorMessage "<forloop>" 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 "<term>" do
- let t <- withErrorMessage "<term>: expected term"
- (forloop <|> op <|> var <|> text)
- return t
+ let t <- withErrorMessage "<term>: 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
projects / temple.lean4.git / commitdiff