diff options
author | Son Ho | 2023-03-07 17:49:03 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 4db56fe2c963a4052f8415b3985c8765407fccbc (patch) | |
tree | 53c5f05469bb3946547c418176f35d840dbe6012 /tests/lean/hashmap | |
parent | 051e2a19f3268d272a0acd0425d2107ebea020c5 (diff) |
Update the extraction of Lean files
Diffstat (limited to '')
-rw-r--r-- | tests/lean/hashmap/Hashmap.lean | 1 | ||||
-rw-r--r-- | tests/lean/hashmap/Hashmap/Types.lean | 2 | ||||
-rw-r--r-- | tests/lean/hashmap/lake-manifest.json | 27 | ||||
-rw-r--r-- | tests/lean/hashmap/lakefile.lean | 14 | ||||
-rw-r--r-- | tests/lean/hashmap/lean-toolchain | 1 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain.lean | 2 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean | 18 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 23 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Types.lean | 4 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/lake-manifest.json | 8 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/lakefile.lean | 14 |
11 files changed, 69 insertions, 45 deletions
diff --git a/tests/lean/hashmap/Hashmap.lean b/tests/lean/hashmap/Hashmap.lean new file mode 100644 index 00000000..41630205 --- /dev/null +++ b/tests/lean/hashmap/Hashmap.lean @@ -0,0 +1 @@ +import Hashmap.Funs diff --git a/tests/lean/hashmap/Hashmap/Types.lean b/tests/lean/hashmap/Hashmap/Types.lean index 750bf6de..dd2be633 100644 --- a/tests/lean/hashmap/Hashmap/Types.lean +++ b/tests/lean/hashmap/Hashmap/Types.lean @@ -9,10 +9,8 @@ inductive list_t (T : Type) := /- [hashmap::HashMap] -/ structure hash_map_t (T : Type) where - hash_map_num_entries : USize hash_map_max_load_factor : (USize × USize) hash_map_max_load : USize hash_map_slots : Vec (list_t T) - diff --git a/tests/lean/hashmap/lake-manifest.json b/tests/lean/hashmap/lake-manifest.json new file mode 100644 index 00000000..57b071ca --- /dev/null +++ b/tests/lean/hashmap/lake-manifest.json @@ -0,0 +1,27 @@ +{"version": 4, + "packagesDir": "./lake-packages", + "packages": + [{"git": + {"url": "https://github.com/leanprover-community/mathlib4.git", + "subDir?": null, + "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece", + "name": "mathlib", + "inputRev?": null}}, + {"git": + {"url": "https://github.com/gebner/quote4", + "subDir?": null, + "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa", + "name": "Qq", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/JLimperg/aesop", + "subDir?": null, + "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690", + "name": "aesop", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee", + "name": "std", + "inputRev?": "main"}}]} diff --git a/tests/lean/hashmap/lakefile.lean b/tests/lean/hashmap/lakefile.lean index c7d79306..713785f6 100644 --- a/tests/lean/hashmap/lakefile.lean +++ b/tests/lean/hashmap/lakefile.lean @@ -4,15 +4,9 @@ open Lake DSL require mathlib from git "https://github.com/leanprover-community/mathlib4.git" -package «hashmap» { - -- add package configuration options here -} +package «hashmap» {} -lean_lib «Base» { - -- add library configuration options here -} - -lean_lib «Hashmap» { - -- add library configuration options here -} +lean_lib «Base» {} +@[default_target] +lean_lib «Hashmap» {} diff --git a/tests/lean/hashmap/lean-toolchain b/tests/lean/hashmap/lean-toolchain new file mode 100644 index 00000000..bbf57f10 --- /dev/null +++ b/tests/lean/hashmap/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2023-01-21 diff --git a/tests/lean/hashmap_on_disk/HashmapMain.lean b/tests/lean/hashmap_on_disk/HashmapMain.lean index 99415d9d..1a4e7f82 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain.lean @@ -1 +1 @@ -def hello := "world" +import HashmapMain.Funs diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean index 16a4ea4c..a514c58a 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean @@ -1,11 +1,12 @@ --- [hashmap_main]: decreases clauses +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: templates for the decreases clauses import Base.Primitives import HashmapMain.Types /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: termination measure -/ @[simp] def hashmap_hash_map_allocate_slots_loop_terminates (T : Type) - (slots : vec (hashmap_list_t T)) (n : USize) := + (slots : Vec (hashmap_list_t T)) (n : USize) := (slots, n) syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic @@ -14,16 +15,17 @@ macro_rules | `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) => `(tactic| sorry) -/- [hashmap_main::hashmap::HashMap::{0}::clear]: termination measure -/ +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/ @[simp] -def hashmap_hash_map_clear_loop_terminates (T : Type) - (slots : vec (hashmap_list_t T)) (i : USize) := +def hashmap_hash_map_clear_slots_loop_terminates (T : Type) + (slots : Vec (hashmap_list_t T)) (i : USize) := (slots, i) -syntax "hashmap_hash_map_clear_loop_decreases" term+ : tactic +syntax "hashmap_hash_map_clear_slots_loop_decreases" term+ : tactic macro_rules -| `(tactic| hashmap_hash_map_clear_loop_decreases $slots $i) =>`(tactic| sorry) +| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) => + `(tactic| sorry) /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/ @[simp] @@ -52,7 +54,7 @@ $ls) =>`(tactic| sorry) /- [hashmap_main::hashmap::HashMap::{0}::move_elements]: termination measure -/ @[simp] def hashmap_hash_map_move_elements_loop_terminates (T : Type) - (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) (i : USize) + (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) (i : USize) := (ntable, slots, i) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index c85d14f4..392c8816 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -60,8 +60,8 @@ def hashmap_hash_map_new_fwd (T : Type) : Result (hashmap_hash_map_t T) := hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit)) (USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit)) -/- [hashmap_main::hashmap::HashMap::{0}::clear] -/ -def hashmap_hash_map_clear_loop_fwd_back +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ +def hashmap_hash_map_clear_slots_loop_fwd_back (T : Type) (slots : Vec (hashmap_list_t T)) (i : USize) : (Result (Vec (hashmap_list_t T))) := @@ -73,19 +73,26 @@ def hashmap_hash_map_clear_loop_fwd_back let slots0 ← vec_index_mut_back (hashmap_list_t T) slots i hashmap_list_t.HashmapListNil - hashmap_hash_map_clear_loop_fwd_back T slots0 i1 + hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1 else Result.ret slots -termination_by hashmap_hash_map_clear_loop_fwd_back slots i => - hashmap_hash_map_clear_loop_terminates T slots i -decreasing_by hashmap_hash_map_clear_loop_decreases slots i +termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i => + hashmap_hash_map_clear_slots_loop_terminates T slots i +decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i + +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/ +def hashmap_hash_map_clear_slots_fwd_back + (T : Type) (slots : Vec (hashmap_list_t T)) : + Result (Vec (hashmap_list_t T)) + := + hashmap_hash_map_clear_slots_loop_fwd_back T slots + (USize.ofNatCore 0 (by intlit)) /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ def hashmap_hash_map_clear_fwd_back (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) := do let v ← - hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots - (USize.ofNatCore 0 (by intlit)) + hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots Result.ret { hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)), diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index 40f9b7e9..fbab1bcd 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -9,11 +9,11 @@ inductive hashmap_list_t (T : Type) := /- [hashmap_main::hashmap::HashMap] -/ structure hashmap_hash_map_t (T : Type) where - hashmap_hash_map_num_entries : USize hashmap_hash_map_max_load_factor : (USize × USize) hashmap_hash_map_max_load : USize hashmap_hash_map_slots : Vec (hashmap_list_t T) -/- The state type used in the state-error monad -/ axiom State : Type +/- The state type used in the state-error monad -/ +axiom State : Type diff --git a/tests/lean/hashmap_on_disk/lake-manifest.json b/tests/lean/hashmap_on_disk/lake-manifest.json index 8ac53836..57b071ca 100644 --- a/tests/lean/hashmap_on_disk/lake-manifest.json +++ b/tests/lean/hashmap_on_disk/lake-manifest.json @@ -4,24 +4,24 @@ [{"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "583f6cfa4bced545c797216b32600d6211b753f9", + "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece", "name": "mathlib", "inputRev?": null}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, - "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf", + "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa", "name": "Qq", "inputRev?": "master"}}, {"git": {"url": "https://github.com/JLimperg/aesop", "subDir?": null, - "rev": "ccff5d4ae7411c5fe741f3139950e8bddf353dea", + "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690", "name": "aesop", "inputRev?": "master"}}, {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "cda27d551340756d5ed6f9b83716a9db799c5537", + "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee", "name": "std", "inputRev?": "main"}}]} diff --git a/tests/lean/hashmap_on_disk/lakefile.lean b/tests/lean/hashmap_on_disk/lakefile.lean index bdb614cd..70daf427 100644 --- a/tests/lean/hashmap_on_disk/lakefile.lean +++ b/tests/lean/hashmap_on_disk/lakefile.lean @@ -4,15 +4,9 @@ open Lake DSL require mathlib from git "https://github.com/leanprover-community/mathlib4.git" -package «hashmap_main» { - -- add package configuration options here -} +package «hashmap_main» {} -lean_lib «Base» { - -- add library configuration options here -} - -lean_lib «HashmapMain» { - -- add library configuration options here -} +lean_lib «Base» {} +@[default_target] +lean_lib «HashmapMain» {} |