diff options
author | Jonathan Protzenko | 2023-02-02 23:36:14 -0800 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 40e7df701d246faa453003374206014606ca6b6d (patch) | |
tree | 4f4a199c90ce53937eae8ec4ecb9e0d1f7564a2c /tests/lean/hashmap_on_disk | |
parent | dad646759a3ab9175c8797f144dec9d8e07b54b3 (diff) |
WIP
Diffstat (limited to 'tests/lean/hashmap_on_disk')
-rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 76 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean | 113 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 8 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 18 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Types.lean | 4 | ||||
-rw-r--r-- | tests/lean/hashmap_on_disk/lake-manifest.json | 27 |
6 files changed, 206 insertions, 40 deletions
diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index 0a51aacd..79958d94 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -1,4 +1,5 @@ import Lean +import Lean.Meta.Tactic.Simp import Init.Data.List.Basic import Mathlib.Tactic.RunCmd @@ -75,7 +76,7 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem => -- Silly example of the kind of reasoning that this notation enables #eval do let h: y <-- .ret (0: Nat) - let _: y = 0 := by cases h; simp + let _: y = 0 := by cases h; decide let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ .ret r @@ -111,6 +112,23 @@ macro "let" h:ident " : " e:term " <-- " f:term : doElem => -- library_search." Try to settle this with a Lean expert on what is the most -- productive way to go about this? +-- One needs to perform a little bit of reasoning in order to successfully +-- inject constants into USize, so we provide a general-purpose macro + +syntax "intlit" : tactic + +macro_rules + | `(tactic| intlit) => `(tactic| + match USize.size, usize_size_eq with + | _, Or.inl rfl => decide + | _, Or.inr rfl => decide) + +-- This is how the macro is expected to be used +#eval USize.ofNatCore 0 (by intlit) + +-- Also works for other integer types (at the expense of a needless disjunction) +#eval UInt32.ofNatCore 0 (by intlit) + -- Further thoughts: look at what has been done here: -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean -- and @@ -133,7 +151,12 @@ def USize.checked_sub (n: USize) (m: USize): result USize := fail integerOverflow def USize.checked_add (n: USize) (m: USize): result USize := - if h: n.val + m.val < USize.size then + if h: n.val.val + m.val.val <= 4294967295 then + .ret ⟨ n.val.val + m.val.val, by + have h': 4294967295 < USize.size := by intlit + apply Nat.lt_of_le_of_lt h h' + ⟩ + else if h: n.val + m.val < USize.size then .ret ⟨ n.val + m.val, h ⟩ else .fail integerOverflow @@ -149,7 +172,12 @@ def USize.checked_rem (n: USize) (m: USize): result USize := .fail integerOverflow def USize.checked_mul (n: USize) (m: USize): result USize := - if h: n.val * m.val < USize.size then + if h: n.val.val * m.val.val <= 4294967295 then + .ret ⟨ n.val.val * m.val.val, by + have h': 4294967295 < USize.size := by intlit + apply Nat.lt_of_le_of_lt h h' + ⟩ + else if h: n.val * m.val < USize.size then .ret ⟨ n.val * m.val, h ⟩ else .fail integerOverflow @@ -187,22 +215,6 @@ def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineIntege else .fail integerOverflow --- One needs to perform a little bit of reasoning in order to successfully --- inject constants into USize, so we provide a general-purpose macro - -syntax "intlit" : tactic - -macro_rules - | `(tactic| intlit) => `(tactic| - match USize.size, usize_size_eq with - | _, Or.inl rfl => decide - | _, Or.inr rfl => decide) - --- This is how the macro is expected to be used -#eval USize.ofNatCore 0 (by intlit) - --- Also works for other integer types (at the expense of a needless disjunction) -#eval UInt32.ofNatCore 0 (by intlit) -- Test behavior... #eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0 @@ -267,7 +279,14 @@ def vec_push_back_old (α : Type u) (v : vec α) (x : α) : { res: result (vec def vec_push_back (α : Type u) (v : vec α) (x : α) : result (vec α) := - if h : List.length v.val + 1 < USize.size then + if h : List.length v.val + 1 <= 4294967295 then + return ⟨ List.concat v.val x, + by + rw [List.length_concat] + have h': 4294967295 < USize.size := by intlit + apply Nat.lt_of_le_of_lt h h' + ⟩ + else if h: List.length v.val + 1 < USize.size then return ⟨List.concat v.val x, by rw [List.length_concat] @@ -340,10 +359,15 @@ syntax (name := assert) "#assert" term: command @[command_elab assert] def assertImpl : CommandElab := fun (_stx: Syntax) => do - logInfo "Hello World" - -def ignore (a: Prop) (_x: a) := () - -#eval ignore (2 == 2) (by simp) - + logInfo "Reducing and asserting: " + logInfo _stx[1] + runTermElabM (fun _ => do + let e ← Term.elabTerm _stx[1] none + logInfo (Expr.dbgToString e) + -- How to evaluate the term and compare the result to true? + pure ()) + -- logInfo (Expr.dbgToString (``true)) + -- throwError "TODO: assert" + +#eval 2 == 2 #assert (2 == 2) diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean new file mode 100644 index 00000000..bf331d6e --- /dev/null +++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean @@ -0,0 +1,113 @@ +-- 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, n) + +syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/ +@[simp] +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_slots_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_insert_in_list_loop_terminates (T : Type) (key : USize) + (value : T) (ls : hashmap_list_t T) := + (key, value, ls) + +syntax "hashmap_hash_map_insert_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_insert_in_list_loop_decreases $key $value $ls) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: termination measure -/ +@[simp] +def hashmap_hash_map_move_elements_from_list_loop_terminates (T : Type) + (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) := + (ntable, ls) + +syntax "hashmap_hash_map_move_elements_from_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_move_elements_from_list_loop_decreases $ntable +$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, slots, i) + +syntax "hashmap_hash_map_move_elements_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_move_elements_loop_decreases $ntable $slots $i) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_contains_key_in_list_loop_terminates (T : Type) + (key : USize) (ls : hashmap_list_t T) := + (key, ls) + +syntax "hashmap_hash_map_contains_key_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_contains_key_in_list_loop_decreases $key $ls) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_get_in_list_loop_terminates (T : Type) (key : USize) + (ls : hashmap_list_t T) := + (key, ls) + +syntax "hashmap_hash_map_get_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_get_in_list_loop_decreases $key $ls) =>`(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: termination measure -/ +@[simp] +def hashmap_hash_map_get_mut_in_list_loop_terminates (T : Type) + (ls : hashmap_list_t T) (key : USize) := + (ls, key) + +syntax "hashmap_hash_map_get_mut_in_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_get_mut_in_list_loop_decreases $ls $key) => + `(tactic| sorry) + +/- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: termination measure -/ +@[simp] +def hashmap_hash_map_remove_from_list_loop_terminates (T : Type) (key : USize) + (ls : hashmap_list_t T) := + (key, ls) + +syntax "hashmap_hash_map_remove_from_list_loop_decreases" term+ : tactic + +macro_rules +| `(tactic| hashmap_hash_map_remove_from_list_loop_decreases $key $ls) => + `(tactic| sorry) + diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 5e78d9cf..ffe3416a 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -5,6 +5,8 @@ import HashmapMain.Types import HashmapMain.Opaque import HashmapMain.Clauses.Template +section variable (opaque_defs: OpaqueDecls) + /- [hashmap_main::hashmap::hash_key] -/ def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k @@ -637,15 +639,15 @@ def hashmap_test1_fwd : result Unit := /- Unit test for [hashmap_main::hashmap::test1] -/ -#assert (hashmap_test1_fwd = ret ()) +#assert (hashmap_test1_fwd = .ret ()) /- [hashmap_main::insert_on_disk] -/ def insert_on_disk_fwd (key : USize) (value : UInt64) (st : state) : result (state × Unit) := do - let (st0, hm) <- hashmap_utils_deserialize_fwd st + let (st0, hm) <- opaque_defs.hashmap_utils_deserialize_fwd st let hm0 <- hashmap_hash_map_insert_fwd_back UInt64 hm key value - let (st1, _) <- hashmap_utils_serialize_fwd hm0 st0 + let (st1, _) <- opaque_defs.hashmap_utils_serialize_fwd hm0 st0 result.ret (st1, ()) /- [hashmap_main::main] -/ diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean index 87b10c59..8b41934d 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean @@ -3,11 +3,13 @@ import Base.Primitives import HashmapMain.Types -/- [hashmap_main::hashmap_utils::deserialize] -/ -axiom hashmap_utils_deserialize_fwd - : state -> result (state × (hashmap_hash_map_t UInt64)) - -/- [hashmap_main::hashmap_utils::serialize] -/ -axiom hashmap_utils_serialize_fwd - : hashmap_hash_map_t UInt64 -> state -> result (state × Unit) - +structure OpaqueDecls where + + /- [hashmap_main::hashmap_utils::deserialize] -/ + hashmap_utils_deserialize_fwd + : state -> result (state × (hashmap_hash_map_t UInt64)) + + /- [hashmap_main::hashmap_utils::serialize] -/ + hashmap_utils_serialize_fwd + : hashmap_hash_map_t UInt64 -> state -> result (state × Unit) + diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index d1cd9579..2a3ea462 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -15,7 +15,5 @@ structure hashmap_hash_map_t (T : Type) where 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 new file mode 100644 index 00000000..8ac53836 --- /dev/null +++ b/tests/lean/hashmap_on_disk/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": "583f6cfa4bced545c797216b32600d6211b753f9", + "name": "mathlib", + "inputRev?": null}}, + {"git": + {"url": "https://github.com/gebner/quote4", + "subDir?": null, + "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf", + "name": "Qq", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/JLimperg/aesop", + "subDir?": null, + "rev": "ccff5d4ae7411c5fe741f3139950e8bddf353dea", + "name": "aesop", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "cda27d551340756d5ed6f9b83716a9db799c5537", + "name": "std", + "inputRev?": "main"}}]} |