Update the deps

diff --git a/Temple/DeBruijnEval.lean b/Temple/DeBruijnEval.lean
index cb28416c2b0224f31edc00182733272fd0428ecc..9a969097776edcc210342071bd90c9c4534631b3 100644 (file)
--- a/Temple/DeBruijnEval.lean
+++ b/Temple/DeBruijnEval.lean
@@ -1,4 +1,4 @@
-import Lean.Data.HashMap
+import Std.Data.HashMap

 
 import Temple.DeBruijn
 
 
 import Temple.DeBruijn
 


@@ -21,8 +21,8 @@ partial instance : ToString Value where
     toStr
 
 structure UserContext where
     toStr
 
 structure UserContext where

-  data : Lean.HashMap String Value := Lean.HashMap.ofList []
-  operators : Lean.HashMap String (Value -> Except String Value) := Lean.HashMap.ofList []
+  data : Std.HashMap String Value := Std.HashMap.ofList []
+  operators : Std.HashMap String (Value -> Except String Value) := Std.HashMap.ofList []

 
 def defaultOperators : List (Prod String (Value -> Except String Value)) :=
   let toUpper
 
 def defaultOperators : List (Prod String (Value -> Except String Value)) :=
   let toUpper


@@ -34,15 +34,15 @@ def defaultOperators : List (Prod String (Value -> Except String Value)) :=
   [ ("toUpper", toUpper), ("toLower", toLower) ]
 
 structure Context where
   [ ("toUpper", toUpper), ("toLower", toLower) ]
 
 structure Context where

-  data : Lean.HashMap String Value
-  operators : Lean.HashMap String (Value -> Except String Value)
+  data : Std.HashMap String Value
+  operators : Std.HashMap String (Value -> Except String Value)

   binds : List Value := []
 
 private partial def eval' (ctx : Context) (t : Term) : IO String :=
   match t with
   | .text s => return s
   | .op name args =>
   binds : List Value := []
 
 private partial def eval' (ctx : Context) (t : Term) : IO String :=
   match t with
   | .text s => return s
   | .op name args =>

-    match (Lean.HashMap.find? ctx.operators name) with
+    match (Std.HashMap.get? ctx.operators name) with

     | .some operator => do
       let resolvedArgs <- args.mapM $ fun (Arg.var v) => eval' ctx $ .var v
       let operatorResult := operator $ match resolvedArgs with
     | .some operator => do
       let resolvedArgs <- args.mapM $ fun (Arg.var v) => eval' ctx $ .var v
       let operatorResult := operator $ match resolvedArgs with


@@ -58,12 +58,12 @@ private partial def eval' (ctx : Context) (t : Term) : IO String :=
       | .some (.list vs) => return vs
       | .none => throw $ IO.userError s!"\"{name}\" is not provided"
     let vals <- match v with
       | .some (.list vs) => return vs
       | .none => throw $ IO.userError s!"\"{name}\" is not provided"
     let vals <- match v with

-      | .free n => processVariable n $ Lean.HashMap.find? ctx.data n
+      | .free n => processVariable n $ Std.HashMap.get? ctx.data n

       | .bound (i, n) => processVariable n ctx.binds[i]?
     let processVal val := ts.mapM $ eval' {ctx with binds := List.cons val ctx.binds }
     let results <- vals.mapM processVal
     return String.join (results.map String.join)
       | .bound (i, n) => processVariable n ctx.binds[i]?
     let processVal val := ts.mapM $ eval' {ctx with binds := List.cons val ctx.binds }
     let results <- vals.mapM processVal
     return String.join (results.map String.join)

-  | .var (.free n) => match (Lean.HashMap.find? ctx.data n) with
+  | .var (.free n) => match (Std.HashMap.get? ctx.data n) with

     | .some v => return toString v
     | .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 s!"\"{n}\" is not provided"
   | .var (.bound (i, n)) => match ctx.binds[i]? with


@@ -73,7 +73,7 @@ private partial def eval' (ctx : Context) (t : Term) : IO String :=
 partial def eval (userContext : UserContext) : Term -> IO String :=
   TempleDeBruijnEval.eval'
     { data := userContext.data
 partial def eval (userContext : UserContext) : Term -> IO String :=
   TempleDeBruijnEval.eval'
     { data := userContext.data

-    , operators := Lean.HashMap.ofList $ defaultOperators ++ userContext.operators.toList
+    , operators := Std.HashMap.ofList $ defaultOperators ++ userContext.operators.toList

     }
 
 section Test
     }
 
 section Test


@@ -83,16 +83,16 @@ section Test
   return (t == "hello")
 
 #eval show IO Bool from do
   return (t == "hello")
 
 #eval show IO Bool from do

-  let t <- eval ({operators := Lean.HashMap.ofList [ ( "hello", fun _ => return (Value.text "world") ) ]}) (.op "hello" [])
+  let t <- eval ({operators := Std.HashMap.ofList [ ( "hello", fun _ => return (Value.text "world") ) ]}) (.op "hello" [])

   return (t == "world")
 
 #eval show IO Bool from do
   return (t == "world")
 
 #eval show IO Bool from do

-  let t <- eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
+  let t <- eval ({data := Std.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})

                 (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "0")) ])
   return (t == "hello worldhello land")
 
 #eval show IO Bool from do
                 (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "0")) ])
   return (t == "hello worldhello land")
 
 #eval show IO Bool from do

-  let t <- eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
+  let t <- eval ({data := Std.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])

                                                             , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
                 (.forloop (Var.free "fruits")
                   [ .text "got an ", .var (.bound (0, "0")), .text "\n"
                                                             , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
                 (.forloop (Var.free "fruits")
                   [ .text "got an ", .var (.bound (0, "0")), .text "\n"


@@ -100,7 +100,7 @@ section Test
   return (t == "got an apple\nsaladoniongot an orange\nsaladonion")
 
 #eval show IO String from
   return (t == "got an apple\nsaladoniongot an orange\nsaladonion")
 
 #eval show IO String from

-  eval ({data := Lean.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])
+  eval ({data := Std.HashMap.ofList [ ("fruits", .list [ .text "apple", .text "orange" ])

                                                             , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
                 (.forloop (Var.free "fruits")
                   [ .text "got an ", .var (.bound (0, "0")), .text "\n"
                                                             , ("vegetables", .list [ .text "salad", .text "onion" ] ) ]})
                 (.forloop (Var.free "fruits")
                   [ .text "got an ", .var (.bound (0, "0")), .text "\n"


@@ -108,22 +108,22 @@ section Test
 
 #eval show IO String from
   try
 
 #eval show IO String from
   try

-    eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
+    eval ({data := Std.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})

                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (1, "x")) ])
   catch e => pure s!"Caught exception: {e}"
 
 #eval show IO String from
   try
                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (1, "x")) ])
   catch e => pure s!"Caught exception: {e}"
 
 #eval show IO String from
   try

-    eval ({data := Lean.HashMap.ofList [ ]})
+    eval ({data := Std.HashMap.ofList [ ]})

                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "x")) ])
   catch e => pure s!"Caught exception: {e}"
 
 #eval show IO String from
   try
                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.bound (0, "x")) ])
   catch e => pure s!"Caught exception: {e}"
 
 #eval show IO String from
   try

-    eval ({data := Lean.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})
+    eval ({data := Std.HashMap.ofList [ ( "fruits", .list [ .text "world", .text "land" ] ) ]})

                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ])
   catch e => pure s!"Caught exception: {e}"
 
 end Test
 
                   (.forloop (Var.free "fruits") [ .text "hello ", .var (.free "free"), .var (.bound (0, "x")) ])
   catch e => pure s!"Caught exception: {e}"
 
 end Test
 

-end TempleDeBruijnEval
\ No newline at end of file
+end TempleDeBruijnEval

diff --git a/Temple/Eval.lean b/Temple/Eval.lean
index ff55392b5311ffc783d744d2ff19de8780cbe21c..7f4182e1428089df8df75985bafd3f6684b2d621 100644 (file)
--- a/Temple/Eval.lean
+++ b/Temple/Eval.lean
@@ -32,10 +32,10 @@ section Test
   runStringWith {} "hello"
 
 #eval show IO String from
   runStringWith {} "hello"
 
 #eval show IO String from

-  runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"
+  runStringWith { data := Std.HashMap.ofList [ ("world", .text "world") ] } "hello {{ world }}"

 
 #eval show IO String from
 
 #eval show IO String from

-  runStringWith { data := Lean.HashMap.ofList [ ("world", .text "world"), ("xs", .list $ [ "1", "2", "3" ].map .text ) ] }
+  runStringWith { data := Std.HashMap.ofList [ ("world", .text "world"), ("xs", .list $ [ "1", "2", "3" ].map .text ) ] }

     "hello {{ world }}
 
     {% for x in xs %}
     "hello {{ world }}
 
     {% for x in xs %}


@@ -44,7 +44,7 @@ section Test
     "
 
 #eval show IO String from
     "
 
 #eval show IO String from

-  let dataItems := Lean.HashMap.ofList
+  let dataItems := Std.HashMap.ofList

         [ ("world", .text "world")
         , ("xs", .list $ [ "1", "2", "3" ].map .text )
         , ("ys", .list $ [ "4", "5", "6" ].map .text )
         [ ("world", .text "world")
         , ("xs", .list $ [ "1", "2", "3" ].map .text )
         , ("ys", .list $ [ "4", "5", "6" ].map .text )


@@ -56,7 +56,7 @@ section Test
 {% endfor %}"
 
 #eval show IO String from
 {% endfor %}"
 
 #eval show IO String from

-  let dataItems := Lean.HashMap.ofList
+  let dataItems := Std.HashMap.ofList

         [ ("world", .text "world")
         , ("xs", .list $ [ .text "1", .list [ .text "2", .text "3"], .text "4" ] )
         ]
         [ ("world", .text "world")
         , ("xs", .list $ [ .text "1", .list [ .text "2", .text "3"], .text "4" ] )
         ]


@@ -67,7 +67,7 @@ section Test
 {% endfor %}"
 
 #eval show IO String from
 {% endfor %}"
 
 #eval show IO String from

-  let dataItems := Lean.HashMap.ofList
+  let dataItems := Std.HashMap.ofList

         [ ("world", .text "world")
         , ("xs", .list [ .text "hello", .text "world"] )
         ]
         [ ("world", .text "world")
         , ("xs", .list [ .text "hello", .text "world"] )
         ]

diff --git a/Temple/Syntax.lean b/Temple/Syntax.lean
index 3167ecab32098aad694584d35ca6e3998405024e..f93d5ec84c5572f29d44ce5037b398aedaf1fce1 100644 (file)
--- a/Temple/Syntax.lean
+++ b/Temple/Syntax.lean
@@ -42,7 +42,7 @@ partial def textInner (acc : String) : TempleParser String :=
       let savePos <- getPosition
       match <- option? (chars "{{" <|> chars "{%") with
         | some _ => do
       let savePos <- getPosition
       match <- option? (chars "{{" <|> chars "{%") with
         | some _ => do

-          setPosition savePos false
+          setPosition savePos

           return acc
         | none => do
           let c <- anyToken
           return acc
         | none => do
           let c <- anyToken


@@ -94,35 +94,35 @@ 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 s!"Parsing error: {e}"
+  | .error _ e => throw $ IO.userError s!"Parsing error: {e}"

 
 section Test
 
 
 section Test
 

-#eval show IO Bool from do
+#eval! show IO Bool from do

   let t <- parse "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"
   return t == [.text "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"]
 
   let t <- parse "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"
   return t == [.text "hello worl asd a{}s[]@#}!@#!@#SADsa][c«»»{»  æыв{ { {  }} { % { { {фыÔ¨ÍÓÎÓˆd"]
 

-#eval show IO Bool from do
+#eval! show IO Bool from do

   let t <- parse "{{ myVariable }}"
   return t == [.var "myVariable"]
 
   let t <- parse "{{ myVariable }}"
   return t == [.var "myVariable"]
 

-#eval show IO Bool from do
+#eval! show IO Bool from do

   let t <- parse "hello {{ myVariable }}"
   return t == [.text "hello ", .var "myVariable"]
 
   let t <- parse "hello {{ myVariable }}"
   return t == [.text "hello ", .var "myVariable"]
 

-#eval show IO Bool from do
+#eval! show IO Bool from do

   let t <- parse "{% my_operator s   d %}"
   return t == [.op "my_operator" [ "s", "d" ]]
 
   let t <- parse "{% my_operator s   d %}"
   return t == [.op "my_operator" [ "s", "d" ]]
 

-#eval show IO Bool from do
+#eval! show IO Bool from do

   let t <- parse "{% for    x     in      fruits %}sadasd{{hello}}{% endfor %}"
   return t == [.forloop "x" "fruits" [ .text "sadasd", .var "hello" ]]
 
   let t <- parse "{% for    x     in      fruits %}sadasd{{hello}}{% endfor %}"
   return t == [.forloop "x" "fruits" [ .text "sadasd", .var "hello" ]]
 

-#eval show IO Bool from do
+#eval! show IO Bool from do

   let t <- parse "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
   return t == [.forloop "x" "fruits"
     [ .text "hello", .forloop "y" "fruits" [ .text "world", .var "x", .var "y" ], .text "good" ]]
 
 end Test
 
   let t <- parse "{% for x in fruits %}hello{% for y in fruits %}world{{x}}{{y}}{% endfor %}good{% endfor %}"
   return t == [.forloop "x" "fruits"
     [ .text "hello", .forloop "y" "fruits" [ .text "world", .var "x", .var "y" ], .text "good" ]]
 
 end Test
 

-end TempleSyntax
\ No newline at end of file
+end TempleSyntax

diff --git a/lake-manifest.json b/lake-manifest.json
index 0f1db72e097fb2eeccce269c26fee9ff0bf837c1..d1e936c953a6785bc82c1e4be50c907066c71627 100644 (file)
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,32 +1,35 @@
-{"version": 7,
+{"version": "1.1.0",

  "packagesDir": ".lake/packages",
  "packages":
  "packagesDir": ".lake/packages",
  "packages":

- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/fgdorais/lean4-parser",

    "type": "git",
    "subDir": null,
    "type": "git",
    "subDir": null,

-   "rev": "6b203c31b414beb758ef9b7fdc71b01d144504ad",
-   "name": "std",
+   "scope": "",
+   "rev": "4155745b7e137396988a25f433807efc525ce135",
+   "name": "Parser",

    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,

-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},

   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,

-   "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9",
+   "scope": "",
+   "rev": "625c5900a5af52f192722b844ba2a440e0dfbd59",

    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},

-  {"url": "https://github.com/fgdorais/lean4-parser",
+  {"url": "https://github.com/leanprover-community/batteries",

    "type": "git",
    "subDir": null,
    "type": "git",
    "subDir": null,

-   "rev": "4ae54daeb1e7c1c0b1d34bf314338c49819599d9",
-   "name": "Parser",
+   "scope": "",
+   "rev": "47d41b04677e3e9b3d726b78ea5d7a9ba0577e79",
+   "name": "batteries",

    "manifestFile": "lake-manifest.json",
    "manifestFile": "lake-manifest.json",

-   "inputRev": "main",
+   "inputRev": "bump/nightly-2025-08-19",

    "inherited": false,
    "inherited": false,

-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],

  "name": "temple",
  "lakeDir": ".lake"}
  "name": "temple",
  "lakeDir": ".lake"}

diff --git a/lakefile.lean b/lakefile.lean
deleted file mode 100644 (file)
index e32f6a7..0000000
--- a/lakefile.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-import Lake
-open Lake DSL
-
-require std from git
-  "https://github.com/leanprover/std4" @ "main"
-
-require UnicodeBasic from git
-  "https://github.com/fgdorais/lean4-unicode-basic" @ "main"
-
-require Parser from git "https://github.com/fgdorais/lean4-parser" @ "main"
-
-package «temple»
-
-@[default_target]
-lean_lib «Temple»

diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644 (file)
index 0000000..de618e6
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,21 @@
+name = "temple"
+defaultTargets = ["Temple"]
+
+[[require]]
+name = "batteries"
+git = "https://github.com/leanprover-community/batteries"
+rev = "bump/nightly-2025-08-19"
+
+[[require]]
+name = "UnicodeBasic"
+git = "https://github.com/fgdorais/lean4-unicode-basic"
+rev = "main"
+
+[[require]]
+name = "Parser"
+git = "https://github.com/fgdorais/lean4-parser"
+rev = "main"
+
+[[lean_lib]]
+name = "Temple"
+

diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644 (file)
index 0000000..27770b5
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.23.0-rc2
\ No newline at end of file