repos / temple.lean4.git

commit

e703f20

parent

90f4f7a

author

Evgenii Akentev

date

2025-08-19 23:17:33 +0400 +04

Update the deps

  1@@ -1,4 +1,4 @@
  2-import Lean.Data.HashMap
  3+import Std.Data.HashMap
  4 
  5 import Temple.DeBruijn
  6 
  7@@ -21,8 +21,8 @@ partial instance : ToString Value where
  8     toStr
  9 
 10 structure UserContext where
 11-  data : Lean.HashMap String Value := Lean.HashMap.ofList []
 12-  operators : Lean.HashMap String (Value -> Except String Value) := Lean.HashMap.ofList []
 13+  data : Std.HashMap String Value := Std.HashMap.ofList []
 14+  operators : Std.HashMap String (Value -> Except String Value) := Std.HashMap.ofList []
 15 
 16 def defaultOperators : List (Prod String (Value -> Except String Value)) :=
 17   let toUpper
 18@@ -34,15 +34,15 @@ def defaultOperators : List (Prod String (Value -> Except String Value)) :=
 19   [ ("toUpper", toUpper), ("toLower", toLower) ]
 20 
 21 structure Context where
 22-  data : Lean.HashMap String Value
 23-  operators : Lean.HashMap String (Value -> Except String Value)
 24+  data : Std.HashMap String Value
 25+  operators : Std.HashMap String (Value -> Except String Value)
 26   binds : List Value := []
 27 
 28 private partial def eval' (ctx : Context) (t : Term) : IO String :=
 29   match t with
 30   | .text s => return s
 31   | .op name args =>
 32-    match (Lean.HashMap.find? ctx.operators name) with
 33+    match (Std.HashMap.get? ctx.operators name) with
 34     | .some operator => do
 35       let resolvedArgs <- args.mapM $ fun (Arg.var v) => eval' ctx $ .var v
 36       let operatorResult := operator $ match resolvedArgs with
 37@@ -58,12 +58,12 @@ private partial def eval' (ctx : Context) (t : Term) : IO String :=
 38       | .some (.list vs) => return vs
 39       | .none => throw $ IO.userError s!"\"{name}\" is not provided"
 40     let vals <- match v with
 41-      | .free n => processVariable n $ Lean.HashMap.find? ctx.data n
 42+      | .free n => processVariable n $ Std.HashMap.get? ctx.data n
 43       | .bound (i, n) => processVariable n ctx.binds[i]?
 44     let processVal val := ts.mapM $ eval' {ctx with binds := List.cons val ctx.binds }
 45     let results <- vals.mapM processVal
 46     return String.join (results.map String.join)
 47-  | .var (.free n) => match (Lean.HashMap.find? ctx.data n) with
 48+  | .var (.free n) => match (Std.HashMap.get? ctx.data n) with
 49     | .some v => return toString v
 50     | .none => throw $ IO.userError s!"\"{n}\" is not provided"
 51   | .var (.bound (i, n)) => match ctx.binds[i]? with
 52@@ -73,7 +73,7 @@ private partial def eval' (ctx : Context) (t : Term) : IO String :=
 53 partial def eval (userContext : UserContext) : Term -> IO String :=
 54   TempleDeBruijnEval.eval'
 55     { data := userContext.data
 56-    , operators := Lean.HashMap.ofList $ defaultOperators ++ userContext.operators.toList
 57+    , operators := Std.HashMap.ofList $ defaultOperators ++ userContext.operators.toList
 58     }
 59 
 60 section Test
 61@@ -83,16 +83,16 @@ section Test
 62   return (t == "hello")
 63 
 64 #eval show IO Bool from do
 65-  let t <- eval ({operators := Lean.HashMap.ofList [ ( "hello", fun _ => return (Value.text "world") ) ]}) (.op "hello" [])
 66+  let t <- eval ({operators := Std.HashMap.ofList [ ( "hello", fun _ => return (Value.text "world") ) ]}) (.op "hello" [])
 67   return (t == "world")
 68 
 69 #eval show IO Bool from do
 70-  let t <- eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
 71+  let t <- eval ({data := Std.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
 72                 (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "0")) ])
 73   return (t == "hello worldhello land")
 74 
 75 #eval show IO Bool from do
 76-  let t <- eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
 77+  let t <- eval ({data := Std.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
 78                                                             , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
 79                 (.forloop (Var.free "fruits")
 80                   [ .text "got an ", .var (.bound (0, "0")), .text "\n"
 81@@ -100,7 +100,7 @@ section Test
 82   return (t == "got an apple\nsaladoniongot an orange\nsaladonion")
 83 
 84 #eval show IO String from
 85-  eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
 86+  eval ({data := Std.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
 87                                                             , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
 88                 (.forloop (Var.free "fruits")
 89                   [ .text "got an ", .var (.bound (0, "0")), .text "\n"
 90@@ -108,22 +108,22 @@ section Test
 91 
 92 #eval show IO String from
 93   try
 94-    eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
 95+    eval ({data := Std.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
 96                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (1, "x")) ])
 97   catch e => pure s!"Caught exception: {e}"
 98 
 99 #eval show IO String from
100   try
101-    eval ({data := Lean.HashMap.ofList [ ]})
102+    eval ({data := Std.HashMap.ofList [ ]})
103                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "x")) ])
104   catch e => pure s!"Caught exception: {e}"
105 
106 #eval show IO String from
107   try
108-    eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
109+    eval ({data := Std.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
110                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ])
111   catch e => pure s!"Caught exception: {e}"
112 
113 end Test
114 
115-end TempleDeBruijnEval
116+end TempleDeBruijnEval

 1@@ -32,10 +32,10 @@ section Test
 2   runStringWith {} "hello"
 3 
 4 #eval show IO String from
 5-  runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"
 6+  runStringWith { data := Std.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"
 7 
 8 #eval show IO String from
 9-  runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world"), ("xs", .list $ [ "1", "2", "3" ].map .text ) ] }
10+  runStringWith { data := Std.HashMap.ofList [ ("world", .text "world"), ("xs", .list $ [ "1", "2", "3" ].map .text ) ] }
11     "hello {{ world }}
12 
13     {% for x in xs %}
14@@ -44,7 +44,7 @@ section Test
15     "
16 
17 #eval show IO String from
18-  let dataItems := Lean.HashMap.ofList
19+  let dataItems := Std.HashMap.ofList
20         [ ("world", .text "world")
21         , ("xs", .list $ [ "1", "2", "3" ].map .text )
22         , ("ys", .list $ [ "4", "5", "6" ].map .text )
23@@ -56,7 +56,7 @@ section Test
24 {% endfor %}"
25 
26 #eval show IO String from
27-  let dataItems := Lean.HashMap.ofList
28+  let dataItems := Std.HashMap.ofList
29         [ ("world", .text "world")
30         , ("xs", .list $ [ .text "1", .list [ .text "2", .text "3"], .text "4" ] )
31         ]
32@@ -67,7 +67,7 @@ section Test
33 {% endfor %}"
34 
35 #eval show IO String from
36-  let dataItems := Lean.HashMap.ofList
37+  let dataItems := Std.HashMap.ofList
38         [ ("world", .text "world")
39         , ("xs", .list [ .text "hello", .text "world"] )
40         ]

 1@@ -42,7 +42,7 @@ partial def textInner (acc : String) : TempleParser String :=
 2       let savePos <- getPosition
 3       match <- option? (chars "{{" <|> chars "{%") with
 4         | some _ => do
 5-          setPosition savePos false
 6+          setPosition savePos
 7           return acc
 8         | none => do
 9           let c <- anyToken
10@@ -94,35 +94,35 @@ end TempleParser
11 def parse (input : String) : IO (List Term) :=
12   match (TempleParser.terms <* Parser.endOfInput).run input.toSubstring with
13   | .ok _ t => return t
14-  | .error e => throw $ IO.userError s!"Parsing error: {e}"
15+  | .error _ e => throw $ IO.userError s!"Parsing error: {e}"
16 
17 section Test
18 
19-#eval show IO Bool from do
20+#eval! show IO Bool from do
21   let t <- parse "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"
22   return t == [.text "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"]
23 
24-#eval show IO Bool from do
25+#eval! show IO Bool from do
26   let t <- parse "{{ myVariable }}"
27   return t == [.var "myVariable"]
28 
29-#eval show IO Bool from do
30+#eval! show IO Bool from do
31   let t <- parse "hello {{ myVariable }}"
32   return t == [.text "hello ", .var "myVariable"]
33 
34-#eval show IO Bool from do
35+#eval! show IO Bool from do
36   let t <- parse "{% my_operator s   d %}"
37   return t == [.op "my_operator" [ "s", "d" ]]
38 
39-#eval show IO Bool from do
40+#eval! show IO Bool from do
41   let t <- parse "{% for    x     in      fruits %}sadasd{{hello}}{% endfor %}"
42   return t == [.forloop "x" "fruits" [ .text "sadasd", .var "hello" ]]
43 
44-#eval show IO Bool from do
45+#eval! show IO Bool from do
46   let t <- parse "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
47   return t == [.forloop "x" "fruits"
48     [ .text "hello", .forloop "y" "fruits" [ .text "world", .var "x", .var "y" ], .text "good" ]]
49 
50 end Test
51 
52-end TempleSyntax
53+end TempleSyntax

 1@@ -1,32 +1,35 @@
 2-{"version": 7,
 3+{"version": "1.1.0",
 4  "packagesDir": ".lake/packages",
 5  "packages":
 6- [{"url": "https://github.com/leanprover/std4",
 7+ [{"url": "https://github.com/fgdorais/lean4-parser",
 8    "type": "git",
 9    "subDir": null,
10-   "rev": "6b203c31b414beb758ef9b7fdc71b01d144504ad",
11-   "name": "std",
12+   "scope": "",
13+   "rev": "4155745b7e137396988a25f433807efc525ce135",
14+   "name": "Parser",
15    "manifestFile": "lake-manifest.json",
16    "inputRev": "main",
17    "inherited": false,
18-   "configFile": "lakefile.lean"},
19+   "configFile": "lakefile.toml"},
20   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
21    "type": "git",
22    "subDir": null,
23-   "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9",
24+   "scope": "",
25+   "rev": "625c5900a5af52f192722b844ba2a440e0dfbd59",
26    "name": "UnicodeBasic",
27    "manifestFile": "lake-manifest.json",
28    "inputRev": "main",
29    "inherited": false,
30    "configFile": "lakefile.lean"},
31-  {"url": "https://github.com/fgdorais/lean4-parser",
32+  {"url": "https://github.com/leanprover-community/batteries",
33    "type": "git",
34    "subDir": null,
35-   "rev": "4ae54daeb1e7c1c0b1d34bf314338c49819599d9",
36-   "name": "Parser",
37+   "scope": "",
38+   "rev": "47d41b04677e3e9b3d726b78ea5d7a9ba0577e79",
39+   "name": "batteries",
40    "manifestFile": "lake-manifest.json",
41-   "inputRev": "main",
42+   "inputRev": "bump/nightly-2025-08-19",
43    "inherited": false,
44-   "configFile": "lakefile.lean"}],
45+   "configFile": "lakefile.toml"}],
46  "name": "temple",
47  "lakeDir": ".lake"}

 1@@ -1,15 +0,0 @@
 2-import Lake
 3-open Lake DSL
 4-
 5-require std from git
 6-  "https://github.com/leanprover/std4" @ "main"
 7-
 8-require UnicodeBasic from git
 9-  "https://github.com/fgdorais/lean4-unicode-basic" @ "main"
10-
11-require Parser from git "https://github.com/fgdorais/lean4-parser" @ "main"
12-
13-package «temple»
14-
15-@[default_target]
16-lean_lib «Temple»

 1@@ -0,0 +1,21 @@
 2+name = "temple"
 3+defaultTargets = ["Temple"]
 4+
 5+[[require]]
 6+name = "batteries"
 7+git = "https://github.com/leanprover-community/batteries"
 8+rev = "bump/nightly-2025-08-19"
 9+
10+[[require]]
11+name = "UnicodeBasic"
12+git = "https://github.com/fgdorais/lean4-unicode-basic"
13+rev = "main"
14+
15+[[require]]
16+name = "Parser"
17+git = "https://github.com/fgdorais/lean4-parser"
18+rev = "main"
19+
20+[[lean_lib]]
21+name = "Temple"
22+

1@@ -0,0 +1 @@
2+leanprover/lean4:v4.23.0-rc2