| .bound (_ , n) => n
| .free n => n
+inductive Arg
+-- TODO: support strings and other types of arguments
+| var : Var -> Arg
+deriving BEq, Repr, Inhabited
+
+instance : ToString Arg where
+ toString
+ | .var v => toString v
+
inductive Term
| text : String -> Term
-| op : String -> List String -> Term
+| op : String -> List Arg -> Term
| var : Var -> Term
| forloop : Var -> List Term -> Term
deriving BEq, Repr, Inhabited
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.map toString) ++ " %}"
| .forloop name body =>
"{% for " ++ toString name ++ " %}\n"
++ (String.join $ List.intersperse "\n" $ body.map toStr)
| .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
+ | .op n args => Term.op n $ args.map $ fun n => Arg.var $
+ match (index n binds) with
+ | .some i => (Var.bound (i, n))
+ | .none => Var.free n
| .forloop v collection terms =>
let range_bind := match (index collection binds) with
| .some i => (Var.bound (i, collection))
#eval show Bool from
let t := fromSyntaxTerm (.op "hello" [ "world" ])
- t == .op "hello" [ "world" ]
+ t == .op "hello" [ Arg.var ( .free "world") ]
#eval show IO Bool from do
let t := fromSyntaxTerm (.forloop "x" "fruits" [ .text "world", .var "x" ])
| .list s => "[" ++ ",".intercalate (s.map toStr) ++ "]"
toStr
+structure UserContext where
+ data : Lean.HashMap String Value := Lean.HashMap.ofList []
+ operators : Lean.HashMap String (Value -> IO Value) := Lean.HashMap.ofList []
+
structure Context where
data : Lean.HashMap String Value := Lean.HashMap.ofList []
- operators : Lean.HashMap String Value := Lean.HashMap.ofList []
+ operators : Lean.HashMap String (Value -> IO Value) := Lean.HashMap.ofList []
binds : List Value := []
-partial def eval (ctx : Context) (t : Term) : Except String String :=
+private partial def eval' (ctx : Context) (t : Term) : IO String :=
match t with
| .text s => return s
- | .op name _ =>
+ | .op name args =>
match (Lean.HashMap.find? ctx.operators name) with
- | .some (.text t) => return t
- | _ => throw $ "\"" ++ name ++ "\" operator is not provided"
+ | .some operator => do
+ let resolvedArgs <- args.mapM $ fun (Arg.var v) => eval' ctx $ .var v
+ let result <- operator $ match resolvedArgs with
+ | [x] => .text x
+ | _ => .list $ resolvedArgs.map .text
+ return toString result
+ | _ => throw $ IO.userError $ "\"" ++ 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"
+ | .none => throw $ IO.userError $ "\"" ++ 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 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"
+ | .none => throw $ IO.userError $ "\"" ++ 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"
+ | .none => throw $ IO.userError $ "\"" ++ n ++ "\" is not defined in this scope"
+
+partial def eval (userContext : UserContext) : Term -> IO String :=
+ TempleDeBruijnEval.eval' { data := userContext.data, operators := userContext.operators }
section Test
-#eval show Bool from
- let t := eval {} (.text "hello")
- t.toOption == some "hello"
+#eval show IO Bool from do
+ let t <- eval {} (.text "hello")
+ return (t == "hello")
-#eval show Bool from
- let t := eval ({operators := Lean.HashMap.ofList [ ( "hello", .text "world" ) ]}) (.op "hello" [])
- t.toOption == some "world"
+#eval show IO Bool from do
+ let t <- eval ({operators := Lean.HashMap.ofList [ ( "hello", fun _ => return (Value.text "world") ) ]}) (.op "hello" [])
+ return (t == "world")
-#eval show Bool from
- let t := eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
+#eval show IO Bool from do
+ let t <- eval ({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"
+ return (t == "hello worldhello land")
-#eval show Bool from
- let t := eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
+#eval show IO Bool from do
+ let t <- eval ({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"
+ return (t == "got an apple\nsaladoniongot an orange\nsaladonion")
-#eval show Except String String from
+#eval show IO String from
eval ({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")) ] ])
-#eval show Except String String from
+#eval show IO String from
try
eval ({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
+#eval show IO String from
try
eval ({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
+#eval show IO String from
try
eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
(.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ])
open IO.FS
-open TempleDeBruijnEval (Context)
+open TempleDeBruijnEval
-structure UserContext where
- data : Lean.HashMap String Value
- operators : Lean.HashMap String Value
-
-def runStringWith (c : Context) (s : String) : Except String String := do
+def runStringWith (c : UserContext) (s : String) : IO 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
-@[inline] def runString (s : String) : Except String String := runStringWith { } s
+@[inline] def runString (s : String) : IO String := runStringWith { } s
-@[inline] def runWith (c : Context) (fn : System.FilePath) : IO (Except String String) := do
+@[inline] def runWith (c : UserContext) (fn : System.FilePath) : IO String := do
let s <- IO.FS.readFile fn
- return runStringWith c s
+ runStringWith c s
-@[inline] def run (fn : System.FilePath) : IO (Except String String) := do
+@[inline] def run (fn : System.FilePath) : IO String := do
let s <- IO.FS.readFile fn
- return runString s
+ runString s
section Test
-#eval show Except String String from
+#eval show IO String from
runStringWith {} "hello"
-#eval show Except String String from
+#eval show IO String from
runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"
-#eval show Except String String from
+#eval show IO String from
runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world"), ("xs", .list $ [ "1", "2", "3" ].map .text ) ] }
"hello {{ world }}
{% endfor %}
"
-#eval show IO Unit from
+#eval show IO String from
let dataItems := Lean.HashMap.ofList
[ ("world", .text "world")
, ("xs", .list $ [ "1", "2", "3" ].map .text )
, ("ys", .list $ [ "4", "5", "6" ].map .text )
]
- let t := runStringWith { data := dataItems }
+ runStringWith { data := dataItems }
"hello {{ world }}
{% for x in xs %}
{% for y in ys %}#{{ x }} {{y}} {% endfor %}
{% endfor %}"
- IO.println t
-#eval show IO Unit from
+#eval show IO String from
let dataItems := Lean.HashMap.ofList
[ ("world", .text "world")
, ("xs", .list $ [ .text "1", .list [ .text "2", .text "3"], .text "4" ] )
]
- let t := runStringWith { data := dataItems }
+ runStringWith { data := dataItems }
"hello {{ world }}
{% for x in xs %}
{% for y in x %}#{{ x }}{{y}} {% endfor %}
{% endfor %}"
- IO.println t
+
+#eval show IO String from
+ let dataItems := Lean.HashMap.ofList
+ [ ("world", .text "world")
+ , ("xs", .list [ .text "hello", .text "world"] )
+ ]
+ let toUpper (v : TempleDeBruijnEval.Value) := match v with
+ | (TempleDeBruijnEval.Value.text t) => return TempleDeBruijnEval.Value.text (String.toUpper t)
+ | _ => throw $ IO.userError "upper: list is not supported"
+
+ runStringWith { data := dataItems, operators := Lean.HashMap.ofList [ ("toUpper", toUpper) ] }
+ "hello {{ world }}
+{% for x in xs %}
+ {% toUpper x %}
+{% endfor %}"
end Test
end TempleParser
-def parse (input : String) : Except String (List Term) :=
+def parse (input : String) : IO (List Term) :=
match (TempleParser.terms <* Parser.endOfInput).run input.toSubstring with
| .ok _ t => return t
- | .error e => throw $ "error: " ++ toString e
+ | .error e => throw $ IO.userError $ "Parsing error: " ++ toString e
section Test
-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 <- terms "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{» æыв{ { { }} { % { { {фыÔ¨ÍÓÎÓˆd"
+ let t <- parse "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 <- terms "{{ myVariable }}"
+ let t <- parse "{{ myVariable }}"
return t == [.var "myVariable"]
#eval show IO Bool from do
- let t <- terms "hello {{ myVariable }}"
+ let t <- parse "hello {{ myVariable }}"
return t == [.text "hello ", .var "myVariable"]
#eval show IO Bool from do
- let t <- terms "{% my_operator s d %}"
+ let t <- parse "{% my_operator s d %}"
return t == [.op "my_operator" [ "s", "d" ]]
#eval show IO Bool from do
- let t <- terms "{% for x in fruits %}sadasd{{hello}}{% endfor %}"
+ let t <- parse "{% 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 %}"
+ let t <- parse "{% 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" ]]
projects / temple.lean.git / commitdiff