From: Evgenii Akentev Date: Tue, 26 Mar 2024 22:58:33 +0000 (+0400) Subject: Add operators support. X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=fe1d3606a50d7aeaf3d1b3fca5d82a47bb9e5770;p=temple.lean.git Add operators support. --- diff --git a/Temple/DeBruijn.lean b/Temple/DeBruijn.lean index 5fd93cb..274f08d 100644 --- a/Temple/DeBruijn.lean +++ b/Temple/DeBruijn.lean @@ -12,9 +12,18 @@ instance : ToString Var where | .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 @@ -26,7 +35,7 @@ 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.map toString) ++ " %}" | .forloop name body => "{% for " ++ toString name ++ " %}\n" ++ (String.join $ List.intersperse "\n" $ body.map toStr) @@ -41,7 +50,10 @@ private partial def fromSyntaxTermInner (binds : List String) (t : TempleSyntax. | .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)) @@ -62,7 +74,7 @@ section Test #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" ]) diff --git a/Temple/DeBruijnEval.lean b/Temple/DeBruijnEval.lean index 0b4d759..acfd0bf 100644 --- a/Temple/DeBruijnEval.lean +++ b/Temple/DeBruijnEval.lean @@ -20,79 +20,91 @@ partial instance : ToString Value where | .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")) ]) diff --git a/Temple/Eval.lean b/Temple/Eval.lean index c6d5533..2b2b4d4 100644 --- a/Temple/Eval.lean +++ b/Temple/Eval.lean @@ -8,37 +8,33 @@ namespace TempleEval 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 }} @@ -47,30 +43,43 @@ section Test {% 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 diff --git a/Temple/Syntax.lean b/Temple/Syntax.lean index 7456eb8..a8ed32c 100644 --- a/Temple/Syntax.lean +++ b/Temple/Syntax.lean @@ -91,40 +91,35 @@ end 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" ]]