Fix operators

diff --git a/Temple/DeBruijnEval.lean b/Temple/DeBruijnEval.lean
index acfd0bfcf337d93eccfcbd0a33c7ed4e5d49b8c0..cb28416c2b0224f31edc00182733272fd0428ecc 100644 (file)
--- 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 []
 
 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
 
 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 :=
   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
     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
         | [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
   | .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]?
     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
     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
   | .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 :=
 
 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
 
 
 section Test
 

diff --git a/Temple/Eval.lean b/Temple/Eval.lean
index 2b2b4d4e825bc4cd47eb3ccd03d4e95676eca12e..ff55392b5311ffc783d744d2ff19de8780cbe21c 100644 (file)
--- a/Temple/Eval.lean
+++ b/Temple/Eval.lean
@@ -71,11 +71,8 @@ section Test
         [ ("world", .text "world")
         , ("xs", .list [ .text "hello", .text "world"] )
         ]
         [ ("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 %}
     "hello {{ world }}
 {% for x in xs %}
   {% toUpper x %}

diff --git a/Temple/Syntax.lean b/Temple/Syntax.lean
index a8ed32ca55d415668b9e1f2d406674cb6864cef7..3167ecab32098aad694584d35ca6e3998405024e 100644 (file)
--- 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
 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
 
 
 section Test