From e703f208d28bab041c92e852750a26cb55eaec85 Mon Sep 17 00:00:00 2001 From: Evgenii Akentev Date: Tue, 19 Aug 2025 23:17:33 +0400 Subject: [PATCH] Update the deps --- Temple/DeBruijnEval.lean | 34 +++++++++++++++++----------------- Temple/Eval.lean | 10 +++++----- Temple/Syntax.lean | 18 +++++++++--------- lake-manifest.json | 25 ++++++++++++++----------- lakefile.lean | 15 --------------- lakefile.toml | 21 +++++++++++++++++++++ lean-toolchain | 1 + 7 files changed, 67 insertions(+), 57 deletions(-) delete mode 100644 lakefile.lean create mode 100644 lakefile.toml create mode 100644 lean-toolchain diff --git a/Temple/DeBruijnEval.lean b/Temple/DeBruijnEval.lean index cb28416..9a96909 100644 --- a/Temple/DeBruijnEval.lean +++ b/Temple/DeBruijnEval.lean @@ -1,4 +1,4 @@ -import Lean.Data.HashMap +import Std.Data.HashMap import Temple.DeBruijn @@ -21,8 +21,8 @@ partial instance : ToString Value 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 @@ -34,15 +34,15 @@ def defaultOperators : List (Prod String (Value -> Except String Value)) := [ ("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 => - 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 @@ -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 - | .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) - | .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 @@ -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 - , operators := Lean.HashMap.ofList $ defaultOperators ++ userContext.operators.toList + , operators := Std.HashMap.ofList $ defaultOperators ++ userContext.operators.toList } section Test @@ -83,16 +83,16 @@ section Test 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 - 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 - 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" @@ -100,7 +100,7 @@ section Test 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" @@ -108,22 +108,22 @@ section Test #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 - 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 - 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 -end TempleDeBruijnEval \ No newline at end of file +end TempleDeBruijnEval diff --git a/Temple/Eval.lean b/Temple/Eval.lean index ff55392..7f4182e 100644 --- a/Temple/Eval.lean +++ b/Temple/Eval.lean @@ -32,10 +32,10 @@ section Test 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 - 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 %} @@ -44,7 +44,7 @@ section Test " #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 ) @@ -56,7 +56,7 @@ section Test {% 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" ] ) ] @@ -67,7 +67,7 @@ section Test {% 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"] ) ] diff --git a/Temple/Syntax.lean b/Temple/Syntax.lean index 3167eca..f93d5ec 100644 --- 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 - setPosition savePos false + setPosition savePos 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 - | .error e => throw $ IO.userError s!"Parsing error: {e}" + | .error _ e => throw $ IO.userError s!"Parsing error: {e}" 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"] -#eval show IO Bool from do +#eval! show IO Bool from do 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"] -#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" ]] -#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" ]] -#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 -end TempleSyntax \ No newline at end of file +end TempleSyntax diff --git a/lake-manifest.json b/lake-manifest.json index 0f1db72..d1e936c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,32 +1,35 @@ -{"version": 7, +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/std4", + [{"url": "https://github.com/fgdorais/lean4-parser", "type": "git", "subDir": null, - "rev": "6b203c31b414beb758ef9b7fdc71b01d144504ad", - "name": "std", + "scope": "", + "rev": "4155745b7e137396988a25f433807efc525ce135", + "name": "Parser", "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, - "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9", + "scope": "", + "rev": "625c5900a5af52f192722b844ba2a440e0dfbd59", "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, - "rev": "4ae54daeb1e7c1c0b1d34bf314338c49819599d9", - "name": "Parser", + "scope": "", + "rev": "47d41b04677e3e9b3d726b78ea5d7a9ba0577e79", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "bump/nightly-2025-08-19", "inherited": false, - "configFile": "lakefile.lean"}], + "configFile": "lakefile.toml"}], "name": "temple", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean deleted file mode 100644 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 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 index 0000000..27770b5 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.23.0-rc2 \ No newline at end of file -- 2.51.0