diff options
Diffstat (limited to 'tests/lean/Hashmap/Funs.lean')
| -rw-r--r-- | tests/lean/Hashmap/Funs.lean | 62 |
1 files changed, 31 insertions, 31 deletions
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 3c244ee0..612e1848 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -18,11 +18,11 @@ divergent def HashMap.allocate_slots_loop (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) : Result (alloc.vec.Vec (List T)) := - if n > 0usize + if n > 0#usize then do let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil - let n1 ← n - 1usize + let n1 ← n - 1#usize HashMap.allocate_slots_loop T slots1 n1 else Result.ok slots @@ -47,7 +47,7 @@ def HashMap.new_with_capacity let i1 ← i / max_load_divisor Result.ok { - num_entries := 0usize, + num_entries := 0#usize, max_load_factor := (max_load_dividend, max_load_divisor), max_load := i1, slots := slots @@ -56,7 +56,7 @@ def HashMap.new_with_capacity /- [hashmap::{hashmap::HashMap<T>}::new]: Source: 'tests/src/hashmap.rs', lines 85:4-85:24 -/ def HashMap.new (T : Type) : Result (HashMap T) := - HashMap.new_with_capacity T 32usize 4usize 5usize + HashMap.new_with_capacity T 32#usize 4#usize 5#usize /- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0: Source: 'tests/src/hashmap.rs', lines 90:4-98:5 -/ @@ -71,7 +71,7 @@ divergent def HashMap.clear_loop let (_, index_mut_back) ← alloc.vec.Vec.index_mut (List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i - let i2 ← i + 1usize + let i2 ← i + 1#usize let slots1 ← index_mut_back List.Nil HashMap.clear_loop T slots1 i2 else Result.ok slots @@ -80,8 +80,8 @@ divergent def HashMap.clear_loop Source: 'tests/src/hashmap.rs', lines 90:4-90:27 -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do - let hm ← HashMap.clear_loop T self.slots 0usize - Result.ok { self with num_entries := 0usize, slots := hm } + let hm ← HashMap.clear_loop T self.slots 0#usize + Result.ok { self with num_entries := 0#usize, slots := hm } /- [hashmap::{hashmap::HashMap<T>}::len]: Source: 'tests/src/hashmap.rs', lines 100:4-100:30 -/ @@ -129,7 +129,7 @@ def HashMap.insert_no_resize if inserted then do - let i1 ← self.num_entries + 1usize + let i1 ← self.num_entries + 1#usize let v ← index_mut_back l1 Result.ok { self with num_entries := i1, slots := v } else do @@ -169,7 +169,7 @@ divergent def HashMap.move_elements_loop (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i let (ls, l1) := core.mem.replace (List T) l List.Nil let ntable1 ← HashMap.move_elements_from_list T ntable ls - let i2 ← i + 1usize + let i2 ← i + 1#usize let slots1 ← index_mut_back l1 HashMap.move_elements_loop T ntable1 slots1 i2 else Result.ok (ntable, slots) @@ -189,15 +189,15 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_u32_max let capacity := alloc.vec.Vec.len (List T) self.slots - let n1 ← max_usize / 2usize + let n1 ← max_usize / 2#usize let (i, i1) := self.max_load_factor let i2 ← n1 / i if capacity <= i2 then do - let i3 ← capacity * 2usize + let i3 ← capacity * 2#usize let ntable ← HashMap.new_with_capacity T i3 i i1 - let p ← HashMap.move_elements T ntable self.slots 0usize + let p ← HashMap.move_elements T ntable self.slots 0#usize let (ntable1, _) := p Result.ok { @@ -377,7 +377,7 @@ def HashMap.remove Result.ok (none, { self with slots := v }) | some x1 => do - let i1 ← self.num_entries - 1usize + let i1 ← self.num_entries - 1#usize let v ← index_mut_back l1 Result.ok (some x1, { self with num_entries := i1, slots := v }) @@ -395,37 +395,37 @@ def insert_on_disk def test1 : Result Unit := do let hm ← HashMap.new U64 - let hm1 ← HashMap.insert U64 hm 0usize 42u64 - let hm2 ← HashMap.insert U64 hm1 128usize 18u64 - let hm3 ← HashMap.insert U64 hm2 1024usize 138u64 - let hm4 ← HashMap.insert U64 hm3 1056usize 256u64 - let i ← HashMap.get U64 hm4 128usize - if i = 18u64 + let hm1 ← HashMap.insert U64 hm 0#usize 42#u64 + let hm2 ← HashMap.insert U64 hm1 128#usize 18#u64 + let hm3 ← HashMap.insert U64 hm2 1024#usize 138#u64 + let hm4 ← HashMap.insert U64 hm3 1056#usize 256#u64 + let i ← HashMap.get U64 hm4 128#usize + if i = 18#u64 then do - let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024usize - let hm5 ← get_mut_back 56u64 - let i1 ← HashMap.get U64 hm5 1024usize - if i1 = 56u64 + let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024#usize + let hm5 ← get_mut_back 56#u64 + let i1 ← HashMap.get U64 hm5 1024#usize + if i1 = 56#u64 then do - let (x, hm6) ← HashMap.remove U64 hm5 1024usize + let (x, hm6) ← HashMap.remove U64 hm5 1024#usize match x with | none => Result.fail .panic | some x1 => - if x1 = 56u64 + if x1 = 56#u64 then do - let i2 ← HashMap.get U64 hm6 0usize - if i2 = 42u64 + let i2 ← HashMap.get U64 hm6 0#usize + if i2 = 42#u64 then do - let i3 ← HashMap.get U64 hm6 128usize - if i3 = 18u64 + let i3 ← HashMap.get U64 hm6 128#usize + if i3 = 18#u64 then do - let i4 ← HashMap.get U64 hm6 1056usize - if i4 = 256u64 + let i4 ← HashMap.get U64 hm6 1056#usize + if i4 = 256#u64 then Result.ok () else Result.fail .panic else Result.fail .panic |