repos / temple.lean4.git

commit

90f4f7a

parent

fe1d360

author

Evgenii Akentev

date

2024-03-29 00:22:20 +0400 +04

Fix operators

 1@@ -22,11 +22,20 @@ partial instance : ToString Value where
 2 
 3 structure UserContext where
 4   data : Lean.HashMap String Value := Lean.HashMap.ofList []
 5-  operators : Lean.HashMap String (Value -> IO Value) := Lean.HashMap.ofList []
 6+  operators : Lean.HashMap String (Value -> Except String Value) := Lean.HashMap.ofList []
 7+
 8+def defaultOperators : List (Prod String (Value -> Except String Value)) :=
 9+  let toUpper
10+    | .text t => return .text (String.toUpper t)
11+    | _ => throw "toUpper: list is not supported"
12+  let toLower
13+    | .text t => return .text (String.toLower t)
14+    | _ => throw "toLower: list is not supported"
15+  [ ("toUpper", toUpper), ("toLower", toLower) ]
16 
17 structure Context where
18-  data : Lean.HashMap String Value := Lean.HashMap.ofList []
19-  operators : Lean.HashMap String (Value -> IO Value) := Lean.HashMap.ofList []
20+  data : Lean.HashMap String Value
21+  operators : Lean.HashMap String (Value -> Except String Value)
22   binds : List Value := []
23 
24 private partial def eval' (ctx : Context) (t : Term) : IO String :=
25@@ -36,16 +45,18 @@ private partial def eval' (ctx : Context) (t : Term) : IO String :=
26     match (Lean.HashMap.find? ctx.operators name) with
27     | .some operator => do
28       let resolvedArgs <- args.mapM $ fun (Arg.var v) => eval' ctx $ .var v
29-      let result <- operator $ match resolvedArgs with
30+      let operatorResult := operator $ match resolvedArgs with
31         | [x] => .text x
32         | _ => .list $ resolvedArgs.map .text
33-      return toString result
34-    | _ => throw $ IO.userError $ "\"" ++ name ++ "\" operator is not provided"
35+      match operatorResult with
36+        | .ok r => return toString r
37+        | .error e => throw $ IO.userError s!"operator {name} execution result: {e}"
38+    | _ => throw $ IO.userError s!"\"{name}\" operator is not provided"
39   | .forloop v ts => do
40     let processVariable name o := match o with
41       | .some (.text t) => return t.toList.map $ fun c => .text ([c].asString)
42       | .some (.list vs) => return vs
43-      | .none => throw $ IO.userError $ "\"" ++ name ++ "\" is not provided"
44+      | .none => throw $ IO.userError s!"\"{name}\" is not provided"
45     let vals <- match v with
46       | .free n => processVariable n $ Lean.HashMap.find? ctx.data n
47       | .bound (i, n) => processVariable n ctx.binds[i]?
48@@ -54,13 +65,16 @@ private partial def eval' (ctx : Context) (t : Term) : IO String :=
49     return String.join (results.map String.join)
50   | .var (.free n) => match (Lean.HashMap.find? ctx.data n) with
51     | .some v => return toString v
52-    | .none => throw $ IO.userError $ "\"" ++ n ++ "\" is not provided"
53+    | .none => throw $ IO.userError s!"\"{n}\" is not provided"
54   | .var (.bound (i, n)) => match ctx.binds[i]? with
55     | .some v => return toString v
56-    | .none => throw $ IO.userError $ "\"" ++ n ++ "\" is not defined in this scope"
57+    | .none => throw $ IO.userError s!"\"{n}\" is not defined in this scope"
58 
59 partial def eval (userContext : UserContext) : Term -> IO String :=
60-  TempleDeBruijnEval.eval' { data := userContext.data, operators := userContext.operators }
61+  TempleDeBruijnEval.eval'
62+    { data := userContext.data
63+    , operators := Lean.HashMap.ofList $ defaultOperators ++ userContext.operators.toList
64+    }
65 
66 section Test
67 

 1@@ -71,11 +71,8 @@ section Test
 2         [ ("world", .text "world")
 3         , ("xs", .list [ .text "hello", .text "world"] )
 4         ]
 5-  let toUpper (v : TempleDeBruijnEval.Value) := match v with
 6-      | (TempleDeBruijnEval.Value.text t) => return TempleDeBruijnEval.Value.text (String.toUpper t)
 7-      | _ => throw $ IO.userError "upper: list is not supported"
 8 
 9-  runStringWith { data := dataItems, operators := Lean.HashMap.ofList [ ("toUpper", toUpper) ] }
10+  runStringWith { data := dataItems }
11     "hello {{ world }}
12 {% for x in xs %}
13   {% toUpper x %}

1@@ -94,7 +94,7 @@ end TempleParser
2 def parse (input : String) : IO (List Term) :=
3   match (TempleParser.terms <* Parser.endOfInput).run input.toSubstring with
4   | .ok _ t => return t
5-  | .error e => throw $ IO.userError $ "Parsing error: " ++ toString e
6+  | .error e => throw $ IO.userError s!"Parsing error: {e}"
7 
8 section Test
9