summaryrefslogtreecommitdiff
path: root/tests/lean/Hashmap
diff options
context:
space:
mode:
authorSon HO2024-03-20 06:48:08 +0100
committerGitHub2024-03-20 06:48:08 +0100
commit0d52c3fe35d0b24de729bdfb917ad6c7104d0c6e (patch)
tree7748d3c19a0993edc710690491a2dc6ea3a2b58f /tests/lean/Hashmap
parent8111c970fcae9d609961eba2ad6716e8c9fc1046 (diff)
parent34850eed3c66f7f2c432294e4c589be53ad5d37b (diff)
Merge pull request #93 from AeneasVerif/son/examples
Add some examples and improve the shape of the generated code
Diffstat (limited to '')
-rw-r--r--tests/lean/Hashmap/Funs.lean33
-rw-r--r--tests/lean/HashmapMain/Funs.lean36
2 files changed, 27 insertions, 42 deletions
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index f0706725..1c95f7c9 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -20,9 +20,9 @@ divergent def HashMap.allocate_slots_loop
if n > 0#usize
then
do
- let v ← alloc.vec.Vec.push (List T) slots List.Nil
+ let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil
let n1 ← n - 1#usize
- HashMap.allocate_slots_loop T v n1
+ HashMap.allocate_slots_loop T slots1 n1
else Result.ret slots
/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
@@ -142,8 +142,8 @@ divergent def HashMap.move_elements_from_list_loop
match ls with
| List.Cons k v tl =>
do
- let hm ← HashMap.insert_no_resize T ntable k v
- HashMap.move_elements_from_list_loop T hm tl
+ let ntable1 ← HashMap.insert_no_resize T ntable k v
+ HashMap.move_elements_from_list_loop T ntable1 tl
| List.Nil => Result.ret ntable
/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
@@ -167,12 +167,10 @@ divergent def HashMap.move_elements_loop
alloc.vec.Vec.index_mut (List T) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i
let (ls, l1) := core.mem.replace (List T) l List.Nil
- let hm ← HashMap.move_elements_from_list T ntable ls
+ let ntable1 ← HashMap.move_elements_from_list T ntable ls
let i2 ← i + 1#usize
let slots1 ← index_mut_back l1
- let back_'a ← HashMap.move_elements_loop T hm slots1 i2
- let (hm1, v) := back_'a
- Result.ret (hm1, v)
+ HashMap.move_elements_loop T ntable1 slots1 i2
else Result.ret (ntable, slots)
/- [hashmap::{hashmap::HashMap<T>}::move_elements]:
@@ -182,10 +180,7 @@ def HashMap.move_elements
:
Result ((HashMap T) × (alloc.vec.Vec (List T)))
:=
- do
- let back_'a ← HashMap.move_elements_loop T ntable slots i
- let (hm, v) := back_'a
- Result.ret (hm, v)
+ HashMap.move_elements_loop T ntable slots i
/- [hashmap::{hashmap::HashMap<T>}::try_resize]:
Source: 'src/hashmap.rs', lines 140:4-140:28 -/
@@ -218,11 +213,11 @@ def HashMap.insert
Result (HashMap T)
:=
do
- let hm ← HashMap.insert_no_resize T self key value
- let i ← HashMap.len T hm
- if i > hm.max_load
- then HashMap.try_resize T hm
- else Result.ret hm
+ let self1 ← HashMap.insert_no_resize T self key value
+ let i ← HashMap.len T self1
+ if i > self1.max_load
+ then HashMap.try_resize T self1
+ else Result.ret self1
/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
Source: 'src/hashmap.rs', lines 206:4-219:5 -/
@@ -311,9 +306,7 @@ def HashMap.get_mut_in_list
(T : Type) (ls : List T) (key : Usize) :
Result (T × (T → Result (List T)))
:=
- do
- let (t, back_'a) ← HashMap.get_mut_in_list_loop T ls key
- Result.ret (t, back_'a)
+ HashMap.get_mut_in_list_loop T ls key
/- [hashmap::{hashmap::HashMap<T>}::get_mut]:
Source: 'src/hashmap.rs', lines 257:4-257:67 -/
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 31441b4a..6a6934b8 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -21,9 +21,9 @@ divergent def hashmap.HashMap.allocate_slots_loop
if n > 0#usize
then
do
- let v ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
+ let slots1 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
let n1 ← n - 1#usize
- hashmap.HashMap.allocate_slots_loop T v n1
+ hashmap.HashMap.allocate_slots_loop T slots1 n1
else Result.ret slots
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]:
@@ -150,8 +150,8 @@ divergent def hashmap.HashMap.move_elements_from_list_loop
match ls with
| hashmap.List.Cons k v tl =>
do
- let hm ← hashmap.HashMap.insert_no_resize T ntable k v
- hashmap.HashMap.move_elements_from_list_loop T hm tl
+ let ntable1 ← hashmap.HashMap.insert_no_resize T ntable k v
+ hashmap.HashMap.move_elements_from_list_loop T ntable1 tl
| hashmap.List.Nil => Result.ret ntable
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]:
@@ -177,12 +177,10 @@ divergent def hashmap.HashMap.move_elements_loop
alloc.vec.Vec.index_mut (hashmap.List T) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i
let (ls, l1) := core.mem.replace (hashmap.List T) l hashmap.List.Nil
- let hm ← hashmap.HashMap.move_elements_from_list T ntable ls
+ let ntable1 ← hashmap.HashMap.move_elements_from_list T ntable ls
let i2 ← i + 1#usize
let slots1 ← index_mut_back l1
- let back_'a ← hashmap.HashMap.move_elements_loop T hm slots1 i2
- let (hm1, v) := back_'a
- Result.ret (hm1, v)
+ hashmap.HashMap.move_elements_loop T ntable1 slots1 i2
else Result.ret (ntable, slots)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]:
@@ -192,10 +190,7 @@ def hashmap.HashMap.move_elements
(slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T)))
:=
- do
- let back_'a ← hashmap.HashMap.move_elements_loop T ntable slots i
- let (hm, v) := back_'a
- Result.ret (hm, v)
+ hashmap.HashMap.move_elements_loop T ntable slots i
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
Source: 'src/hashmap.rs', lines 140:4-140:28 -/
@@ -229,11 +224,11 @@ def hashmap.HashMap.insert
Result (hashmap.HashMap T)
:=
do
- let hm ← hashmap.HashMap.insert_no_resize T self key value
- let i ← hashmap.HashMap.len T hm
- if i > hm.max_load
- then hashmap.HashMap.try_resize T hm
- else Result.ret hm
+ let self1 ← hashmap.HashMap.insert_no_resize T self key value
+ let i ← hashmap.HashMap.len T self1
+ if i > self1.max_load
+ then hashmap.HashMap.try_resize T self1
+ else Result.ret self1
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
Source: 'src/hashmap.rs', lines 206:4-219:5 -/
@@ -326,9 +321,7 @@ def hashmap.HashMap.get_mut_in_list
(T : Type) (ls : hashmap.List T) (key : Usize) :
Result (T × (T → Result (hashmap.List T)))
:=
- do
- let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T ls key
- Result.ret (t, back_'a)
+ hashmap.HashMap.get_mut_in_list_loop T ls key
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
Source: 'src/hashmap.rs', lines 257:4-257:67 -/
@@ -460,8 +453,7 @@ def insert_on_disk
do
let (st1, hm) ← hashmap_utils.deserialize st
let hm1 ← hashmap.HashMap.insert U64 hm key value
- let (st2, _) ← hashmap_utils.serialize hm1 st1
- Result.ret (st2, ())
+ hashmap_utils.serialize hm1 st1
/- [hashmap_main::main]:
Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/