From 90f4f7ab7d745736de55703a4fdded3d388017cf Mon Sep 17 00:00:00 2001 From: Evgenii Akentev Date: Fri, 29 Mar 2024 00:22:20 +0400 Subject: [PATCH] Fix operators --- Temple/DeBruijnEval.lean | 34 ++++++++++++++++++++++++---------- Temple/Eval.lean | 5 +---- Temple/Syntax.lean | 2 +- 3 files changed, 26 insertions(+), 15 deletions(-) diff --git a/Temple/DeBruijnEval.lean b/Temple/DeBruijnEval.lean index acfd0bf..cb28416 100644 --- a/Temple/DeBruijnEval.lean +++ b/Temple/DeBruijnEval.lean @@ -22,11 +22,20 @@ partial instance : ToString Value where structure UserContext where data : Lean.HashMap String Value := Lean.HashMap.ofList [] - operators : Lean.HashMap String (Value -> IO Value) := Lean.HashMap.ofList [] + operators : Lean.HashMap String (Value -> Except String Value) := Lean.HashMap.ofList [] + +def defaultOperators : List (Prod String (Value -> Except String Value)) := + let toUpper + | .text t => return .text (String.toUpper t) + | _ => throw "toUpper: list is not supported" + let toLower + | .text t => return .text (String.toLower t) + | _ => throw "toLower: list is not supported" + [ ("toUpper", toUpper), ("toLower", toLower) ] structure Context where - data : Lean.HashMap String Value := Lean.HashMap.ofList [] - operators : Lean.HashMap String (Value -> IO Value) := Lean.HashMap.ofList [] + data : Lean.HashMap String Value + operators : Lean.HashMap String (Value -> Except String Value) binds : List Value := [] private partial def eval' (ctx : Context) (t : Term) : IO String := @@ -36,16 +45,18 @@ private partial def eval' (ctx : Context) (t : Term) : IO String := match (Lean.HashMap.find? ctx.operators name) with | .some operator => do let resolvedArgs <- args.mapM $ fun (Arg.var v) => eval' ctx $ .var v - let result <- operator $ match resolvedArgs with + let operatorResult := operator $ match resolvedArgs with | [x] => .text x | _ => .list $ resolvedArgs.map .text - return toString result - | _ => throw $ IO.userError $ "\"" ++ name ++ "\" operator is not provided" + match operatorResult with + | .ok r => return toString r + | .error e => throw $ IO.userError s!"operator {name} execution result: {e}" + | _ => throw $ IO.userError s!"\"{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 $ IO.userError $ "\"" ++ name ++ "\" is not provided" + | .none => throw $ IO.userError s!"\"{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]? @@ -54,13 +65,16 @@ private partial def eval' (ctx : Context) (t : Term) : IO String := 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 $ IO.userError $ "\"" ++ n ++ "\" is not provided" + | .none => throw $ IO.userError s!"\"{n}\" is not provided" | .var (.bound (i, n)) => match ctx.binds[i]? with | .some v => return toString v - | .none => throw $ IO.userError $ "\"" ++ n ++ "\" is not defined in this scope" + | .none => throw $ IO.userError s!"\"{n}\" is not defined in this scope" partial def eval (userContext : UserContext) : Term -> IO String := - TempleDeBruijnEval.eval' { data := userContext.data, operators := userContext.operators } + TempleDeBruijnEval.eval' + { data := userContext.data + , operators := Lean.HashMap.ofList $ defaultOperators ++ userContext.operators.toList + } section Test diff --git a/Temple/Eval.lean b/Temple/Eval.lean index 2b2b4d4..ff55392 100644 --- a/Temple/Eval.lean +++ b/Temple/Eval.lean @@ -71,11 +71,8 @@ section Test [ ("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) ] } + runStringWith { data := dataItems } "hello {{ world }} {% for x in xs %} {% toUpper x %} diff --git a/Temple/Syntax.lean b/Temple/Syntax.lean index a8ed32c..3167eca 100644 --- a/Temple/Syntax.lean +++ b/Temple/Syntax.lean @@ -94,7 +94,7 @@ end TempleParser def parse (input : String) : IO (List Term) := match (TempleParser.terms <* Parser.endOfInput).run input.toSubstring with | .ok _ t => return t - | .error e => throw $ IO.userError $ "Parsing error: " ++ toString e + | .error e => throw $ IO.userError s!"Parsing error: {e}" section Test -- 2.34.1