summaryrefslogtreecommitdiff
path: root/tests/lean/Hashmap
diff options
context:
space:
mode:
authorSon Ho2023-07-04 18:09:36 +0200
committerSon Ho2023-07-04 18:09:36 +0200
commitb643bd00747e75d69b6066c55a1798b61277c4b6 (patch)
tree84bbebe82964efc0d779ea782f3ae4b946ca3483 /tests/lean/Hashmap
parent74b3ce71b0e3794853aa1413afaaaa05c8cc5a84 (diff)
Regenerate the Lean test files
Diffstat (limited to 'tests/lean/Hashmap')
-rw-r--r--tests/lean/Hashmap/Funs.lean31
-rw-r--r--tests/lean/Hashmap/Types.lean5
2 files changed, 21 insertions, 15 deletions
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 26742d5d..b4254726 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -4,6 +4,8 @@ import Base
import Hashmap.Types
open Primitives
+namespace Hashmap
+
/- [hashmap::hash_key] -/
def hash_key_fwd (k : Usize) : Result Usize :=
Result.ret k
@@ -82,7 +84,7 @@ def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result Usize :=
/- [hashmap::HashMap::{0}::insert_in_list] -/
divergent def hash_map_insert_in_list_loop_fwd
(T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret false
@@ -97,7 +99,7 @@ def hash_map_insert_in_list_fwd
/- [hashmap::HashMap::{0}::insert_in_list] -/
divergent def hash_map_insert_in_list_loop_back
(T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret (list_t.Cons ckey value tl)
@@ -146,7 +148,7 @@ def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
/- [hashmap::HashMap::{0}::move_elements_from_list] -/
divergent def hash_map_move_elements_from_list_loop_fwd_back
(T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons k v tl =>
do
let ntable0 ← hash_map_insert_no_resize_fwd_back T ntable k v
@@ -224,7 +226,7 @@ def hash_map_insert_fwd_back
/- [hashmap::HashMap::{0}::contains_key_in_list] -/
divergent def hash_map_contains_key_in_list_loop_fwd
(T : Type) (key : Usize) (ls : list_t T) : Result Bool :=
- match h: ls with
+ match ls with
| list_t.Cons ckey t tl =>
if ckey = key
then Result.ret true
@@ -249,7 +251,7 @@ def hash_map_contains_key_fwd
/- [hashmap::HashMap::{0}::get_in_list] -/
divergent def hash_map_get_in_list_loop_fwd
(T : Type) (key : Usize) (ls : list_t T) : Result T :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret cvalue
@@ -274,7 +276,7 @@ def hash_map_get_fwd
/- [hashmap::HashMap::{0}::get_mut_in_list] -/
divergent def hash_map_get_mut_in_list_loop_fwd
(T : Type) (ls : list_t T) (key : Usize) : Result T :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret cvalue
@@ -289,7 +291,7 @@ def hash_map_get_mut_in_list_fwd
/- [hashmap::HashMap::{0}::get_mut_in_list] -/
divergent def hash_map_get_mut_in_list_loop_back
(T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons ckey cvalue tl =>
if ckey = key
then Result.ret (list_t.Cons ckey ret0 tl)
@@ -331,13 +333,13 @@ def hash_map_get_mut_back
/- [hashmap::HashMap::{0}::remove_from_list] -/
divergent def hash_map_remove_from_list_loop_fwd
(T : Type) (key : Usize) (ls : list_t T) : Result (Option T) :=
- match h: ls with
+ match ls with
| list_t.Cons ckey t tl =>
if ckey = key
then
let mv_ls :=
mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil
- match h: mv_ls with
+ match mv_ls with
| list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue)
| list_t.Nil => Result.fail Error.panic
else hash_map_remove_from_list_loop_fwd T key tl
@@ -351,13 +353,13 @@ def hash_map_remove_from_list_fwd
/- [hashmap::HashMap::{0}::remove_from_list] -/
divergent def hash_map_remove_from_list_loop_back
(T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) :=
- match h: ls with
+ match ls with
| list_t.Cons ckey t tl =>
if ckey = key
then
let mv_ls :=
mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil
- match h: mv_ls with
+ match mv_ls with
| list_t.Cons i cvalue tl0 => Result.ret tl0
| list_t.Nil => Result.fail Error.panic
else
@@ -380,7 +382,7 @@ def hash_map_remove_fwd
let hash_mod ← hash % i
let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
let x ← hash_map_remove_from_list_fwd T key l
- match h: x with
+ match x with
| Option.none => Result.ret Option.none
| Option.some x0 =>
do
@@ -396,7 +398,7 @@ def hash_map_remove_back
let hash_mod ← hash % i
let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
let x ← hash_map_remove_from_list_fwd T key l
- match h: x with
+ match x with
| Option.none =>
do
let l0 ← hash_map_remove_from_list_back T key l
@@ -441,7 +443,7 @@ def test1_fwd : Result Unit :=
do
let x ←
hash_map_remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit))
- match h: x with
+ match x with
| Option.none => Result.fail Error.panic
| Option.some x0 =>
if not (x0 = (U64.ofInt 56 (by intlit)))
@@ -472,3 +474,4 @@ def test1_fwd : Result Unit :=
/- Unit test for [hashmap::test1] -/
#assert (test1_fwd == .ret ())
+end Hashmap
diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean
index af26f363..0aec6acf 100644
--- a/tests/lean/Hashmap/Types.lean
+++ b/tests/lean/Hashmap/Types.lean
@@ -3,9 +3,11 @@
import Base
open Primitives
+namespace Hashmap
+
/- [hashmap::List] -/
inductive list_t (T : Type) :=
-| Cons : Usize -> T -> list_t T -> list_t T
+| Cons : Usize → T → list_t T → list_t T
| Nil : list_t T
/- [hashmap::HashMap] -/
@@ -15,3 +17,4 @@ structure hash_map_t (T : Type) where
hash_map_max_load : Usize
hash_map_slots : Vec (list_t T)
+end Hashmap