diff options
Diffstat (limited to 'tests/lean')
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 35 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain.lean | 2 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 55 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Types.lean | 5 |
4 files changed, 73 insertions, 24 deletions
diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index 3b1d39fc..dc2314fc 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean @@ -1,3 +1,5 @@ +import Lean + ------------- -- PRELUDE -- ------------- @@ -10,14 +12,14 @@ inductive error where | arrayOutOfBounds: error | maximumSizeExceeded: error | panic: error -deriving Repr +deriving Repr, BEq open error inductive result (α : Type u) where | ret (v: α): result α | fail (e: error): result α -deriving Repr +deriving Repr, BEq open result @@ -48,7 +50,9 @@ instance : Pure result where def massert (b:Bool) : result Unit := if b then return () else fail assertionFailure --- Machine integers +---------------------- +-- MACHINE INTEGERS -- +---------------------- -- NOTE: we reuse the USize type from prelude.lean, because at least we know -- it's defined in an idiomatic style that is going to make proofs easy (and @@ -123,13 +127,16 @@ macro_rules #eval UInt32.ofNatCore 0 (by intlit) -- Test behavior... -#eval USize.checked_sub 10 20 +#eval assert! USize.checked_sub 10 20 == fail integerOverflow; 0 + #eval USize.checked_sub 20 10 -- NOTE: compare with concrete behavior here, which I do not think we want #eval USize.sub 0 1 #eval UInt8.add 255 255 --- Vectors +------------- +-- VECTORS -- +------------- def vec (α : Type u) := { l : List α // List.length l < USize.size } @@ -176,3 +183,21 @@ def vec_push_back (α : Type u) (v : vec α) (x : α) : { res: result (vec α) / -- TODO: strengthen post-condition above and do a demo to show that we can -- safely eliminate the `fail` case return (vec_len Nat x) + +-------------------- +-- ASSERT COMMAND -- +-------------------- + +open Lean Elab Command Term Meta + +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) + +#assert (2 == 2) diff --git a/tests/lean/hashmap_on_disk/HashmapMain.lean b/tests/lean/hashmap_on_disk/HashmapMain.lean index e99d3a6f..99415d9d 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain.lean @@ -1 +1 @@ -def hello := "world"
\ No newline at end of file +def hello := "world" diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index eb72cc97..0dcb6450 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -3,6 +3,7 @@ import Base.Primitives import HashmapMain.Types import HashmapMain.Opaque +import HashmapMain.Clauses.Template /- [hashmap_main::hashmap::hash_key] -/ def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k @@ -14,12 +15,18 @@ def hashmap_hash_map_allocate_slots_loop_fwd := if n > (USize.ofNatCore 0 (by intlit)) then + match h: (vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil).val with + | result.fail e => result.fail e + | result.ret slots0 => do - let slots0 <- - vec_push_back (hashmap_list_t T) slots hashmap_list_t.HashmapListNil let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else result.ret slots + termination_by hashmap_hash_map_allocate_slots_loop_fwd T slots n => n + decreasing_by + simp_wf + sorry + /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ def hashmap_hash_map_allocate_slots_fwd @@ -56,7 +63,8 @@ def hashmap_hash_map_new_fwd (T : Type) : result (hashmap_hash_map_t T) := /- [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)) + Tot (result (vec (hashmap_list_t T))) + (decreases (hashmap_hash_map_clear_slots_loop_decreases T slots i)) := let i0 := vec_len (hashmap_list_t T) slots if i < i0 @@ -98,7 +106,10 @@ def hashmap_hash_map_len_fwd /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_loop_fwd - (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : result Bool := + (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : + Tot (result Bool) + (decreases (hashmap_hash_map_insert_in_list_loop_decreases T key value ls)) + := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key @@ -115,7 +126,8 @@ def hashmap_hash_map_insert_in_list_fwd /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ def hashmap_hash_map_insert_in_list_loop_back (T : Type) (key : USize) (value : T) (ls : hashmap_list_t T) : - result (hashmap_list_t T) + Tot (result (hashmap_list_t T)) + (decreases (hashmap_hash_map_insert_in_list_loop_decreases T key value ls)) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => @@ -187,7 +199,9 @@ def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ def hashmap_hash_map_move_elements_from_list_loop_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) : - result (hashmap_hash_map_t T) + Tot (result (hashmap_hash_map_t T)) + (decreases ( + hashmap_hash_map_move_elements_from_list_loop_decreases T ntable ls)) := match ls with | hashmap_list_t.HashmapListCons k v tl => @@ -208,7 +222,8 @@ def hashmap_hash_map_move_elements_from_list_fwd_back def hashmap_hash_map_move_elements_loop_fwd_back (T : Type) (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) (i : USize) : - result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T))) + Tot (result ((hashmap_hash_map_t T) × (vec (hashmap_list_t T)))) + (decreases (hashmap_hash_map_move_elements_loop_decreases T ntable slots i)) := let i0 := vec_len (hashmap_list_t T) slots if i < i0 @@ -283,7 +298,10 @@ def hashmap_hash_map_insert_fwd_back /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ def hashmap_hash_map_contains_key_in_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result Bool := + (T : Type) (key : USize) (ls : hashmap_list_t T) : + Tot (result Bool) + (decreases (hashmap_hash_map_contains_key_in_list_loop_decreases T key ls)) + := match ls with | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key @@ -310,7 +328,10 @@ def hashmap_hash_map_contains_key_fwd /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ def hashmap_hash_map_get_in_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result T := + (T : Type) (key : USize) (ls : hashmap_list_t T) : + Tot (result T) + (decreases (hashmap_hash_map_get_in_list_loop_decreases T key ls)) + := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key @@ -337,7 +358,10 @@ def hashmap_hash_map_get_fwd /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_loop_fwd - (T : Type) (ls : hashmap_list_t T) (key : USize) : result T := + (T : Type) (ls : hashmap_list_t T) (key : USize) : + Tot (result T) + (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases T ls key)) + := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => if ckey = key @@ -354,7 +378,8 @@ def hashmap_hash_map_get_mut_in_list_fwd /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ def hashmap_hash_map_get_mut_in_list_loop_back (T : Type) (ls : hashmap_list_t T) (key : USize) (ret0 : T) : - result (hashmap_list_t T) + Tot (result (hashmap_list_t T)) + (decreases (hashmap_hash_map_get_mut_in_list_loop_decreases T ls key)) := match ls with | hashmap_list_t.HashmapListCons ckey cvalue tl => @@ -410,7 +435,10 @@ def hashmap_hash_map_get_mut_back /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_loop_fwd - (T : Type) (key : USize) (ls : hashmap_list_t T) : result (Option T) := + (T : Type) (key : USize) (ls : hashmap_list_t T) : + Tot (result (Option T)) + (decreases (hashmap_hash_map_remove_from_list_loop_decreases T key ls)) + := match ls with | hashmap_list_t.HashmapListCons ckey t tl => if ckey = key @@ -435,7 +463,8 @@ def hashmap_hash_map_remove_from_list_fwd /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ def hashmap_hash_map_remove_from_list_loop_back (T : Type) (key : USize) (ls : hashmap_list_t T) : - result (hashmap_list_t T) + Tot (result (hashmap_list_t T)) + (decreases (hashmap_hash_map_remove_from_list_loop_decreases T key ls)) := match ls with | hashmap_list_t.HashmapListCons ckey t tl => diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean index 1b8f8954..d1cd9579 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean @@ -16,11 +16,6 @@ structure hashmap_hash_map_t (T : Type) where hashmap_hash_map_slots : vec (hashmap_list_t T) -/- [core::num::u32::{9}::MAX] -/ -def core_num_u32_max_body : result UInt32 := - result.ret (UInt32.ofNatCore 4294967295 (by intlit)) -def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp) - /- The state type used in the state-error monad -/ axiom state : Type |