summaryrefslogtreecommitdiff
path: root/tests/lean/Hashmap
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Hashmap')
-rw-r--r--tests/lean/Hashmap/Funs.lean62
-rw-r--r--tests/lean/Hashmap/Properties.lean14
2 files changed, 38 insertions, 38 deletions
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 363d751a..9cbd958c 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -9,7 +9,7 @@ namespace hashmap
/- [hashmap::hash_key]:
Source: 'src/hashmap.rs', lines 27:0-27:32 -/
def hash_key (k : Usize) : Result Usize :=
- Result.ret k
+ Result.ok k
/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
Source: 'src/hashmap.rs', lines 50:4-56:5 -/
@@ -23,7 +23,7 @@ divergent def HashMap.allocate_slots_loop
let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil
let n1 ← n - 1#usize
HashMap.allocate_slots_loop T slots1 n1
- else Result.ret slots
+ else Result.ok slots
/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
Source: 'src/hashmap.rs', lines 50:4-50:76 -/
@@ -44,7 +44,7 @@ def HashMap.new_with_capacity
let slots ← HashMap.allocate_slots T (alloc.vec.Vec.new (List T)) capacity
let i ← capacity * max_load_dividend
let i1 ← i / max_load_divisor
- Result.ret
+ Result.ok
{
num_entries := 0#usize,
max_load_factor := (max_load_dividend, max_load_divisor),
@@ -73,19 +73,19 @@ divergent def HashMap.clear_loop
let i2 ← i + 1#usize
let slots1 ← index_mut_back List.Nil
HashMap.clear_loop T slots1 i2
- else Result.ret slots
+ else Result.ok slots
/- [hashmap::{hashmap::HashMap<T>}::clear]:
Source: 'src/hashmap.rs', lines 80:4-80:27 -/
def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
let hm ← HashMap.clear_loop T self.slots 0#usize
- Result.ret { self with num_entries := 0#usize, slots := hm }
+ Result.ok { self with num_entries := 0#usize, slots := hm }
/- [hashmap::{hashmap::HashMap<T>}::len]:
Source: 'src/hashmap.rs', lines 90:4-90:30 -/
def HashMap.len (T : Type) (self : HashMap T) : Result Usize :=
- Result.ret self.num_entries
+ Result.ok self.num_entries
/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
Source: 'src/hashmap.rs', lines 97:4-114:5 -/
@@ -96,12 +96,12 @@ divergent def HashMap.insert_in_list_loop
match ls with
| List.Cons ckey cvalue tl =>
if ckey = key
- then Result.ret (false, List.Cons ckey value tl)
+ then Result.ok (false, List.Cons ckey value tl)
else
do
let (b, tl1) ← HashMap.insert_in_list_loop T key value tl
- Result.ret (b, List.Cons ckey cvalue tl1)
- | List.Nil => Result.ret (true, List.Cons key value List.Nil)
+ Result.ok (b, List.Cons ckey cvalue tl1)
+ | List.Nil => Result.ok (true, List.Cons key value List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
Source: 'src/hashmap.rs', lines 97:4-97:71 -/
@@ -130,10 +130,10 @@ def HashMap.insert_no_resize
do
let i1 ← self.num_entries + 1#usize
let v ← index_mut_back l1
- Result.ret { self with num_entries := i1, slots := v }
+ Result.ok { self with num_entries := i1, slots := v }
else do
let v ← index_mut_back l1
- Result.ret { self with slots := v }
+ Result.ok { self with slots := v }
/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 183:4-196:5 -/
@@ -144,7 +144,7 @@ divergent def HashMap.move_elements_from_list_loop
do
let ntable1 ← HashMap.insert_no_resize T ntable k v
HashMap.move_elements_from_list_loop T ntable1 tl
- | List.Nil => Result.ret ntable
+ | List.Nil => Result.ok ntable
/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
Source: 'src/hashmap.rs', lines 183:4-183:72 -/
@@ -171,7 +171,7 @@ divergent def HashMap.move_elements_loop
let i2 ← i + 1#usize
let slots1 ← index_mut_back l1
HashMap.move_elements_loop T ntable1 slots1 i2
- else Result.ret (ntable, slots)
+ else Result.ok (ntable, slots)
/- [hashmap::{hashmap::HashMap<T>}::move_elements]:
Source: 'src/hashmap.rs', lines 171:4-171:95 -/
@@ -198,13 +198,13 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
let ntable ← HashMap.new_with_capacity T i3 i i1
let p ← HashMap.move_elements T ntable self.slots 0#usize
let (ntable1, _) := p
- Result.ret
+ Result.ok
{
ntable1
with
num_entries := self.num_entries, max_load_factor := (i, i1)
}
- else Result.ret { self with max_load_factor := (i, i1) }
+ else Result.ok { self with max_load_factor := (i, i1) }
/- [hashmap::{hashmap::HashMap<T>}::insert]:
Source: 'src/hashmap.rs', lines 129:4-129:48 -/
@@ -217,7 +217,7 @@ def HashMap.insert
let i ← HashMap.len T self1
if i > self1.max_load
then HashMap.try_resize T self1
- else Result.ret self1
+ else Result.ok self1
/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
Source: 'src/hashmap.rs', lines 206:4-219:5 -/
@@ -226,9 +226,9 @@ divergent def HashMap.contains_key_in_list_loop
match ls with
| List.Cons ckey _ tl =>
if ckey = key
- then Result.ret true
+ then Result.ok true
else HashMap.contains_key_in_list_loop T key tl
- | List.Nil => Result.ret false
+ | List.Nil => Result.ok false
/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]:
Source: 'src/hashmap.rs', lines 206:4-206:68 -/
@@ -256,7 +256,7 @@ divergent def HashMap.get_in_list_loop
match ls with
| List.Cons ckey cvalue tl =>
if ckey = key
- then Result.ret cvalue
+ then Result.ok cvalue
else HashMap.get_in_list_loop T key tl
| List.Nil => Result.fail .panic
@@ -287,8 +287,8 @@ divergent def HashMap.get_mut_in_list_loop
| List.Cons ckey cvalue tl =>
if ckey = key
then
- let back := fun ret => Result.ret (List.Cons ckey ret tl)
- Result.ret (cvalue, back)
+ let back := fun ret => Result.ok (List.Cons ckey ret tl)
+ Result.ok (cvalue, back)
else
do
let (t, back) ← HashMap.get_mut_in_list_loop T tl key
@@ -296,8 +296,8 @@ divergent def HashMap.get_mut_in_list_loop
fun ret =>
do
let tl1 ← back ret
- Result.ret (List.Cons ckey cvalue tl1)
- Result.ret (t, back1)
+ Result.ok (List.Cons ckey cvalue tl1)
+ Result.ok (t, back1)
| List.Nil => Result.fail .panic
/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
@@ -327,8 +327,8 @@ def HashMap.get_mut
do
let l1 ← get_mut_in_list_back ret
let v ← index_mut_back l1
- Result.ret { self with slots := v }
- Result.ret (t, back)
+ Result.ok { self with slots := v }
+ Result.ok (t, back)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 265:4-291:5 -/
@@ -341,13 +341,13 @@ divergent def HashMap.remove_from_list_loop
let (mv_ls, _) :=
core.mem.replace (List T) (List.Cons ckey t tl) List.Nil
match mv_ls with
- | List.Cons _ cvalue tl1 => Result.ret (some cvalue, tl1)
+ | List.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1)
| List.Nil => Result.fail .panic
else
do
let (o, tl1) ← HashMap.remove_from_list_loop T key tl
- Result.ret (o, List.Cons ckey t tl1)
- | List.Nil => Result.ret (none, List.Nil)
+ Result.ok (o, List.Cons ckey t tl1)
+ | List.Nil => Result.ok (none, List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
Source: 'src/hashmap.rs', lines 265:4-265:69 -/
@@ -373,12 +373,12 @@ def HashMap.remove
| none =>
do
let v ← index_mut_back l1
- Result.ret (none, { self with slots := v })
+ Result.ok (none, { self with slots := v })
| some x1 =>
do
let i1 ← self.num_entries - 1#usize
let v ← index_mut_back l1
- Result.ret (some x1, { self with num_entries := i1, slots := v })
+ Result.ok (some x1, { self with num_entries := i1, slots := v })
/- [hashmap::test1]:
Source: 'src/hashmap.rs', lines 315:0-315:10 -/
@@ -422,6 +422,6 @@ def test1 : Result Unit :=
let i4 ← HashMap.get U64 hm6 1056#usize
if ¬ (i4 = 256#u64)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
end hashmap
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 4e0ca509..fcaf5806 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -59,7 +59,7 @@ def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x
def hash_mod_key (k : Usize) (l : Int) : Int :=
match hash_key k with
- | .ret k => k.val % l
+ | .ok k => k.val % l
| _ => 0
@[simp]
@@ -121,7 +121,7 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (
(hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
(hdk : distinct_keys l0.v) :
∃ b l1,
- insert_in_list α key value l0 = ret (b, l1) ∧
+ insert_in_list α key value l0 = ok (b, l1) ∧
-- The boolean is true ↔ we inserted a new binding
(b ↔ (l0.lookup key = none)) ∧
-- We update the binding
@@ -183,7 +183,7 @@ theorem insert_in_list_spec {α : Type} (l : Int) (key: Usize) (value: α) (l0:
(hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
(hdk : distinct_keys l0.v) :
∃ b l1,
- insert_in_list α key value l0 = ret (b, l1) ∧
+ insert_in_list α key value l0 = ok (b, l1) ∧
(b ↔ (l0.lookup key = none)) ∧
-- We update the binding
l1.lookup key = value ∧
@@ -240,7 +240,7 @@ set_option maxHeartbeats 2000000
theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
(hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
- ∃ nhm, hm.insert_no_resize α key value = ret nhm ∧
+ ∃ nhm, hm.insert_no_resize α key value = ok nhm ∧
-- We preserve the invariant
nhm.inv ∧
-- We updated the binding for key
@@ -253,7 +253,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
| some _ => nhm.len_s = hm.len_s) := by
rw [insert_no_resize]
-- Simplify. Note that this also simplifies some function calls, like array index
- simp [hash_key, bind_tc_ret]
+ simp [hash_key, bind_tc_ok]
have _ : (alloc.vec.Vec.len (List α) hm.slots).val ≠ 0 := by
intro
simp_all [inv]
@@ -281,7 +281,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
rw [if_update_eq] -- TODO: necessary because we don't have a join
-- TODO: progress to ...
have hipost :
- ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧
+ ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ok i0 ∧
i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val
:= by
if inserted then
@@ -328,7 +328,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
-- TODO: we want to automate this
simp only [k_hash_mod]
have h := Int.emod_lt_of_pos k.val hvpos
- simp_all only [ret.injEq, exists_eq_left', List.len_update, gt_iff_lt,
+ simp_all only [ok.injEq, exists_eq_left', List.len_update, gt_iff_lt,
List.index_update_eq, ne_eq, not_false_eq_true, neq_imp]
if h_hm : k_hash_mod = hash_mod.val then
simp_all only [k_hash_mod, List.len_update, gt_iff_lt, List.index_update_eq,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-30 20:24:51 +0000