From 90f4f7ab7d745736de55703a4fdded3d388017cf Mon Sep 17 00:00:00 2001
From: Evgenii Akentev <i@ak3n.com>
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