summaryrefslogtreecommitdiff
path: root/tests/hol4/hashmap
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/hashmap')
-rw-r--r--tests/hol4/hashmap/Holmakefile5
-rw-r--r--tests/hol4/hashmap/hashmap_FunsScript.sml567
-rw-r--r--tests/hol4/hashmap/hashmap_FunsTheory.sig550
-rw-r--r--tests/hol4/hashmap/hashmap_TypesScript.sml24
-rw-r--r--tests/hol4/hashmap/hashmap_TypesTheory.sig494
5 files changed, 1640 insertions, 0 deletions
diff --git a/tests/hol4/hashmap/Holmakefile b/tests/hol4/hashmap/Holmakefile
new file mode 100644
index 00000000..3c4b8973
--- /dev/null
+++ b/tests/hol4/hashmap/Holmakefile
@@ -0,0 +1,5 @@
+# This file was automatically generated - modify ../Holmakefile.template instead
+INCLUDES = ../../../backends/hol4
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/tests/hol4/hashmap/hashmap_FunsScript.sml b/tests/hol4/hashmap/hashmap_FunsScript.sml
new file mode 100644
index 00000000..9ad497f5
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_FunsScript.sml
@@ -0,0 +1,567 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap]: function definitions *)
+open primitivesLib divDefLib
+open hashmap_TypesTheory
+
+val _ = new_theory "hashmap_Funs"
+
+
+val hash_key_fwd_def = Define ‘
+ (** [hashmap::hash_key] *)
+ hash_key_fwd (k : usize) : usize result =
+ Return k
+’
+
+val [hash_map_allocate_slots_loop_fwd_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::allocate_slots] *)
+ hash_map_allocate_slots_loop_fwd
+ (slots : 't list_t vec) (n : usize) : 't list_t vec result =
+ if usize_gt n (int_to_usize 0)
+ then (
+ do
+ slots0 <- vec_push_back slots ListNil;
+ n0 <- usize_sub n (int_to_usize 1);
+ hash_map_allocate_slots_loop_fwd slots0 n0
+ od)
+ else Return slots
+’
+
+val hash_map_allocate_slots_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::allocate_slots] *)
+ hash_map_allocate_slots_fwd
+ (slots : 't list_t vec) (n : usize) : 't list_t vec result =
+ hash_map_allocate_slots_loop_fwd slots n
+’
+
+val hash_map_new_with_capacity_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::new_with_capacity] *)
+ hash_map_new_with_capacity_fwd
+ (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) :
+ 't hash_map_t result
+ =
+ let v = vec_new in
+ do
+ slots <- hash_map_allocate_slots_fwd v capacity;
+ i <- usize_mul capacity max_load_dividend;
+ i0 <- usize_div i max_load_divisor;
+ Return
+ (<|
+ hash_map_num_entries := (int_to_usize 0);
+ hash_map_max_load_factor := (max_load_dividend, max_load_divisor);
+ hash_map_max_load := i0;
+ hash_map_slots := slots
+ |>)
+ od
+’
+
+val hash_map_new_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::new] *)
+ hash_map_new_fwd : 't hash_map_t result =
+ hash_map_new_with_capacity_fwd (int_to_usize 32) (int_to_usize 4)
+ (int_to_usize 5)
+’
+
+val [hash_map_clear_loop_fwd_back_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::clear] *)
+ hash_map_clear_loop_fwd_back
+ (slots : 't list_t vec) (i : usize) : 't list_t vec result =
+ let i0 = vec_len slots in
+ if usize_lt i i0
+ then (
+ do
+ i1 <- usize_add i (int_to_usize 1);
+ slots0 <- vec_index_mut_back slots i ListNil;
+ hash_map_clear_loop_fwd_back slots0 i1
+ od)
+ else Return slots
+’
+
+val hash_map_clear_fwd_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::clear] *)
+ hash_map_clear_fwd_back (self : 't hash_map_t) : 't hash_map_t result =
+ do
+ v <- hash_map_clear_loop_fwd_back self.hash_map_slots (int_to_usize 0);
+ Return
+ (self
+ with
+ <|
+ hash_map_num_entries := (int_to_usize 0); hash_map_slots := v
+ |>)
+ od
+’
+
+val hash_map_len_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::len] *)
+ hash_map_len_fwd (self : 't hash_map_t) : usize result =
+ Return self.hash_map_num_entries
+’
+
+val [hash_map_insert_in_list_loop_fwd_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::insert_in_list] *)
+ hash_map_insert_in_list_loop_fwd
+ (key : usize) (value : 't) (ls : 't list_t) : bool result =
+ (case ls of
+ | ListCons ckey cvalue tl =>
+ if ckey = key
+ then Return F
+ else hash_map_insert_in_list_loop_fwd key value tl
+ | ListNil => Return T)
+’
+
+val hash_map_insert_in_list_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::insert_in_list] *)
+ hash_map_insert_in_list_fwd
+ (key : usize) (value : 't) (ls : 't list_t) : bool result =
+ hash_map_insert_in_list_loop_fwd key value ls
+’
+
+val [hash_map_insert_in_list_loop_back_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::insert_in_list] *)
+ hash_map_insert_in_list_loop_back
+ (key : usize) (value : 't) (ls : 't list_t) : 't list_t result =
+ (case ls of
+ | ListCons ckey cvalue tl =>
+ if ckey = key
+ then Return (ListCons ckey value tl)
+ else (
+ do
+ tl0 <- hash_map_insert_in_list_loop_back key value tl;
+ Return (ListCons ckey cvalue tl0)
+ od)
+ | ListNil => let l = ListNil in Return (ListCons key value l))
+’
+
+val hash_map_insert_in_list_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::insert_in_list] *)
+ hash_map_insert_in_list_back
+ (key : usize) (value : 't) (ls : 't list_t) : 't list_t result =
+ hash_map_insert_in_list_loop_back key value ls
+’
+
+val hash_map_insert_no_resize_fwd_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::insert_no_resize] *)
+ hash_map_insert_no_resize_fwd_back
+ (self : 't hash_map_t) (key : usize) (value : 't) : 't hash_map_t result =
+ do
+ hash <- hash_key_fwd key;
+ let i = vec_len self.hash_map_slots in
+ do
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ inserted <- hash_map_insert_in_list_fwd key value l;
+ if inserted
+ then (
+ do
+ i0 <- usize_add self.hash_map_num_entries (int_to_usize 1);
+ l0 <- hash_map_insert_in_list_back key value l;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return (self with <| hash_map_num_entries := i0; hash_map_slots := v |>)
+ od)
+ else (
+ do
+ l0 <- hash_map_insert_in_list_back key value l;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return (self with <| hash_map_slots := v |>)
+ od)
+ od
+ od
+’
+
+(** [core::num::u32::{9}::MAX] *)
+Definition core_num_u32_max_body_def:
+ core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
+End
+Definition core_num_u32_max_c_def:
+ core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
+End
+
+val [hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::move_elements_from_list] *)
+ hash_map_move_elements_from_list_loop_fwd_back
+ (ntable : 't hash_map_t) (ls : 't list_t) : 't hash_map_t result =
+ (case ls of
+ | ListCons k v tl =>
+ do
+ ntable0 <- hash_map_insert_no_resize_fwd_back ntable k v;
+ hash_map_move_elements_from_list_loop_fwd_back ntable0 tl
+ od
+ | ListNil => Return ntable)
+’
+
+val hash_map_move_elements_from_list_fwd_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::move_elements_from_list] *)
+ hash_map_move_elements_from_list_fwd_back
+ (ntable : 't hash_map_t) (ls : 't list_t) : 't hash_map_t result =
+ hash_map_move_elements_from_list_loop_fwd_back ntable ls
+’
+
+val [hash_map_move_elements_loop_fwd_back_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::move_elements] *)
+ hash_map_move_elements_loop_fwd_back
+ (ntable : 't hash_map_t) (slots : 't list_t vec) (i : usize) :
+ ('t hash_map_t # 't list_t vec) result
+ =
+ let i0 = vec_len slots in
+ if usize_lt i i0
+ then (
+ do
+ l <- vec_index_mut_fwd slots i;
+ let ls = mem_replace_fwd l ListNil in
+ do
+ ntable0 <- hash_map_move_elements_from_list_fwd_back ntable ls;
+ i1 <- usize_add i (int_to_usize 1);
+ let l0 = mem_replace_back l ListNil in
+ do
+ slots0 <- vec_index_mut_back slots i l0;
+ hash_map_move_elements_loop_fwd_back ntable0 slots0 i1
+ od
+ od
+ od)
+ else Return (ntable, slots)
+’
+
+val hash_map_move_elements_fwd_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::move_elements] *)
+ hash_map_move_elements_fwd_back
+ (ntable : 't hash_map_t) (slots : 't list_t vec) (i : usize) :
+ ('t hash_map_t # 't list_t vec) result
+ =
+ hash_map_move_elements_loop_fwd_back ntable slots i
+’
+
+val hash_map_try_resize_fwd_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::try_resize] *)
+ hash_map_try_resize_fwd_back (self : 't hash_map_t) : 't hash_map_t result =
+ do
+ max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+ let capacity = vec_len self.hash_map_slots in
+ do
+ n1 <- usize_div max_usize (int_to_usize 2);
+ let (i, i0) = self.hash_map_max_load_factor in
+ do
+ i1 <- usize_div n1 i;
+ if usize_le capacity i1
+ then (
+ do
+ i2 <- usize_mul capacity (int_to_usize 2);
+ ntable <- hash_map_new_with_capacity_fwd i2 i i0;
+ (ntable0, _) <-
+ hash_map_move_elements_fwd_back ntable self.hash_map_slots
+ (int_to_usize 0);
+ Return
+ (ntable0
+ with
+ <|
+ hash_map_num_entries := self.hash_map_num_entries;
+ hash_map_max_load_factor := (i, i0)
+ |>)
+ od)
+ else Return (self with <| hash_map_max_load_factor := (i, i0) |>)
+ od
+ od
+ od
+’
+
+val hash_map_insert_fwd_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::insert] *)
+ hash_map_insert_fwd_back
+ (self : 't hash_map_t) (key : usize) (value : 't) : 't hash_map_t result =
+ do
+ self0 <- hash_map_insert_no_resize_fwd_back self key value;
+ i <- hash_map_len_fwd self0;
+ if usize_gt i self0.hash_map_max_load
+ then hash_map_try_resize_fwd_back self0
+ else Return self0
+ od
+’
+
+val [hash_map_contains_key_in_list_loop_fwd_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::contains_key_in_list] *)
+ hash_map_contains_key_in_list_loop_fwd
+ (key : usize) (ls : 't list_t) : bool result =
+ (case ls of
+ | ListCons ckey t tl =>
+ if ckey = key
+ then Return T
+ else hash_map_contains_key_in_list_loop_fwd key tl
+ | ListNil => Return F)
+’
+
+val hash_map_contains_key_in_list_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::contains_key_in_list] *)
+ hash_map_contains_key_in_list_fwd
+ (key : usize) (ls : 't list_t) : bool result =
+ hash_map_contains_key_in_list_loop_fwd key ls
+’
+
+val hash_map_contains_key_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::contains_key] *)
+ hash_map_contains_key_fwd
+ (self : 't hash_map_t) (key : usize) : bool result =
+ do
+ hash <- hash_key_fwd key;
+ let i = vec_len self.hash_map_slots in
+ do
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_fwd self.hash_map_slots hash_mod;
+ hash_map_contains_key_in_list_fwd key l
+ od
+ od
+’
+
+val [hash_map_get_in_list_loop_fwd_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::get_in_list] *)
+ hash_map_get_in_list_loop_fwd (key : usize) (ls : 't list_t) : 't result =
+ (case ls of
+ | ListCons ckey cvalue tl =>
+ if ckey = key
+ then Return cvalue
+ else hash_map_get_in_list_loop_fwd key tl
+ | ListNil => Fail Failure)
+’
+
+val hash_map_get_in_list_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::get_in_list] *)
+ hash_map_get_in_list_fwd (key : usize) (ls : 't list_t) : 't result =
+ hash_map_get_in_list_loop_fwd key ls
+’
+
+val hash_map_get_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::get] *)
+ hash_map_get_fwd (self : 't hash_map_t) (key : usize) : 't result =
+ do
+ hash <- hash_key_fwd key;
+ let i = vec_len self.hash_map_slots in
+ do
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_fwd self.hash_map_slots hash_mod;
+ hash_map_get_in_list_fwd key l
+ od
+ od
+’
+
+val [hash_map_get_mut_in_list_loop_fwd_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::get_mut_in_list] *)
+ hash_map_get_mut_in_list_loop_fwd
+ (ls : 't list_t) (key : usize) : 't result =
+ (case ls of
+ | ListCons ckey cvalue tl =>
+ if ckey = key
+ then Return cvalue
+ else hash_map_get_mut_in_list_loop_fwd tl key
+ | ListNil => Fail Failure)
+’
+
+val hash_map_get_mut_in_list_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::get_mut_in_list] *)
+ hash_map_get_mut_in_list_fwd (ls : 't list_t) (key : usize) : 't result =
+ hash_map_get_mut_in_list_loop_fwd ls key
+’
+
+val [hash_map_get_mut_in_list_loop_back_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::get_mut_in_list] *)
+ hash_map_get_mut_in_list_loop_back
+ (ls : 't list_t) (key : usize) (ret : 't) : 't list_t result =
+ (case ls of
+ | ListCons ckey cvalue tl =>
+ if ckey = key
+ then Return (ListCons ckey ret tl)
+ else (
+ do
+ tl0 <- hash_map_get_mut_in_list_loop_back tl key ret;
+ Return (ListCons ckey cvalue tl0)
+ od)
+ | ListNil => Fail Failure)
+’
+
+val hash_map_get_mut_in_list_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::get_mut_in_list] *)
+ hash_map_get_mut_in_list_back
+ (ls : 't list_t) (key : usize) (ret : 't) : 't list_t result =
+ hash_map_get_mut_in_list_loop_back ls key ret
+’
+
+val hash_map_get_mut_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::get_mut] *)
+ hash_map_get_mut_fwd (self : 't hash_map_t) (key : usize) : 't result =
+ do
+ hash <- hash_key_fwd key;
+ let i = vec_len self.hash_map_slots in
+ do
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ hash_map_get_mut_in_list_fwd l key
+ od
+ od
+’
+
+val hash_map_get_mut_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::get_mut] *)
+ hash_map_get_mut_back
+ (self : 't hash_map_t) (key : usize) (ret : 't) : 't hash_map_t result =
+ do
+ hash <- hash_key_fwd key;
+ let i = vec_len self.hash_map_slots in
+ do
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ l0 <- hash_map_get_mut_in_list_back l key ret;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return (self with <| hash_map_slots := v |>)
+ od
+ od
+’
+
+val [hash_map_remove_from_list_loop_fwd_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::remove_from_list] *)
+ hash_map_remove_from_list_loop_fwd
+ (key : usize) (ls : 't list_t) : 't option result =
+ (case ls of
+ | ListCons ckey t tl =>
+ if ckey = key
+ then
+ let mv_ls = mem_replace_fwd (ListCons ckey t tl) ListNil in
+ (case mv_ls of
+ | ListCons i cvalue tl0 => Return (SOME cvalue)
+ | ListNil => Fail Failure)
+ else hash_map_remove_from_list_loop_fwd key tl
+ | ListNil => Return NONE)
+’
+
+val hash_map_remove_from_list_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::remove_from_list] *)
+ hash_map_remove_from_list_fwd
+ (key : usize) (ls : 't list_t) : 't option result =
+ hash_map_remove_from_list_loop_fwd key ls
+’
+
+val [hash_map_remove_from_list_loop_back_def] = DefineDiv ‘
+ (** [hashmap::HashMap::{0}::remove_from_list] *)
+ hash_map_remove_from_list_loop_back
+ (key : usize) (ls : 't list_t) : 't list_t result =
+ (case ls of
+ | ListCons ckey t tl =>
+ if ckey = key
+ then
+ let mv_ls = mem_replace_fwd (ListCons ckey t tl) ListNil in
+ (case mv_ls of
+ | ListCons i cvalue tl0 => Return tl0
+ | ListNil => Fail Failure)
+ else (
+ do
+ tl0 <- hash_map_remove_from_list_loop_back key tl;
+ Return (ListCons ckey t tl0)
+ od)
+ | ListNil => Return ListNil)
+’
+
+val hash_map_remove_from_list_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::remove_from_list] *)
+ hash_map_remove_from_list_back
+ (key : usize) (ls : 't list_t) : 't list_t result =
+ hash_map_remove_from_list_loop_back key ls
+’
+
+val hash_map_remove_fwd_def = Define ‘
+ (** [hashmap::HashMap::{0}::remove] *)
+ hash_map_remove_fwd (self : 't hash_map_t) (key : usize) : 't option result =
+ do
+ hash <- hash_key_fwd key;
+ let i = vec_len self.hash_map_slots in
+ do
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ x <- hash_map_remove_from_list_fwd key l;
+ (case x of
+ | NONE => Return NONE
+ | SOME x0 =>
+ do
+ _ <- usize_sub self.hash_map_num_entries (int_to_usize 1);
+ Return (SOME x0)
+ od)
+ od
+ od
+’
+
+val hash_map_remove_back_def = Define ‘
+ (** [hashmap::HashMap::{0}::remove] *)
+ hash_map_remove_back
+ (self : 't hash_map_t) (key : usize) : 't hash_map_t result =
+ do
+ hash <- hash_key_fwd key;
+ let i = vec_len self.hash_map_slots in
+ do
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ x <- hash_map_remove_from_list_fwd key l;
+ (case x of
+ | NONE =>
+ do
+ l0 <- hash_map_remove_from_list_back key l;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return (self with <| hash_map_slots := v |>)
+ od
+ | SOME x0 =>
+ do
+ i0 <- usize_sub self.hash_map_num_entries (int_to_usize 1);
+ l0 <- hash_map_remove_from_list_back key l;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return (self with <| hash_map_num_entries := i0; hash_map_slots := v |>)
+ od)
+ od
+ od
+’
+
+val test1_fwd_def = Define ‘
+ (** [hashmap::test1] *)
+ test1_fwd : unit result =
+ do
+ hm <- hash_map_new_fwd;
+ hm0 <- hash_map_insert_fwd_back hm (int_to_usize 0) (int_to_u64 42);
+ hm1 <- hash_map_insert_fwd_back hm0 (int_to_usize 128) (int_to_u64 18);
+ hm2 <- hash_map_insert_fwd_back hm1 (int_to_usize 1024) (int_to_u64 138);
+ hm3 <- hash_map_insert_fwd_back hm2 (int_to_usize 1056) (int_to_u64 256);
+ i <- hash_map_get_fwd hm3 (int_to_usize 128);
+ if ~ (i = int_to_u64 18)
+ then Fail Failure
+ else (
+ do
+ hm4 <- hash_map_get_mut_back hm3 (int_to_usize 1024) (int_to_u64 56);
+ i0 <- hash_map_get_fwd hm4 (int_to_usize 1024);
+ if ~ (i0 = int_to_u64 56)
+ then Fail Failure
+ else (
+ do
+ x <- hash_map_remove_fwd hm4 (int_to_usize 1024);
+ (case x of
+ | NONE => Fail Failure
+ | SOME x0 =>
+ if ~ (x0 = int_to_u64 56)
+ then Fail Failure
+ else (
+ do
+ hm5 <- hash_map_remove_back hm4 (int_to_usize 1024);
+ i1 <- hash_map_get_fwd hm5 (int_to_usize 0);
+ if ~ (i1 = int_to_u64 42)
+ then Fail Failure
+ else (
+ do
+ i2 <- hash_map_get_fwd hm5 (int_to_usize 128);
+ if ~ (i2 = int_to_u64 18)
+ then Fail Failure
+ else (
+ do
+ i3 <- hash_map_get_fwd hm5 (int_to_usize 1056);
+ if ~ (i3 = int_to_u64 256) then Fail Failure else Return ()
+ od)
+ od)
+ od))
+ od)
+ od)
+ od
+’
+
+(** Unit test for [hashmap::test1] *)
+val _ = assert_return (“test1_fwd”)
+
+val _ = export_theory ()
diff --git a/tests/hol4/hashmap/hashmap_FunsTheory.sig b/tests/hol4/hashmap/hashmap_FunsTheory.sig
new file mode 100644
index 00000000..50482547
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_FunsTheory.sig
@@ -0,0 +1,550 @@
+signature hashmap_FunsTheory =
+sig
+ type thm = Thm.thm
+
+ (* Definitions *)
+ val core_num_u32_max_body_def : thm
+ val core_num_u32_max_c_def : thm
+ val hash_key_fwd_def : thm
+ val hash_map_allocate_slots_fwd_def : thm
+ val hash_map_allocate_slots_loop_fwd_def : thm
+ val hash_map_clear_fwd_back_def : thm
+ val hash_map_clear_loop_fwd_back_def : thm
+ val hash_map_contains_key_fwd_def : thm
+ val hash_map_contains_key_in_list_fwd_def : thm
+ val hash_map_contains_key_in_list_loop_fwd_def : thm
+ val hash_map_get_fwd_def : thm
+ val hash_map_get_in_list_fwd_def : thm
+ val hash_map_get_in_list_loop_fwd_def : thm
+ val hash_map_get_mut_back_def : thm
+ val hash_map_get_mut_fwd_def : thm
+ val hash_map_get_mut_in_list_back_def : thm
+ val hash_map_get_mut_in_list_fwd_def : thm
+ val hash_map_get_mut_in_list_loop_back_def : thm
+ val hash_map_get_mut_in_list_loop_fwd_def : thm
+ val hash_map_insert_fwd_back_def : thm
+ val hash_map_insert_in_list_back_def : thm
+ val hash_map_insert_in_list_fwd_def : thm
+ val hash_map_insert_in_list_loop_back_def : thm
+ val hash_map_insert_in_list_loop_fwd_def : thm
+ val hash_map_insert_no_resize_fwd_back_def : thm
+ val hash_map_len_fwd_def : thm
+ val hash_map_move_elements_from_list_fwd_back_def : thm
+ val hash_map_move_elements_from_list_loop_fwd_back_def : thm
+ val hash_map_move_elements_fwd_back_def : thm
+ val hash_map_move_elements_loop_fwd_back_def : thm
+ val hash_map_new_fwd_def : thm
+ val hash_map_new_with_capacity_fwd_def : thm
+ val hash_map_remove_back_def : thm
+ val hash_map_remove_from_list_back_def : thm
+ val hash_map_remove_from_list_fwd_def : thm
+ val hash_map_remove_from_list_loop_back_def : thm
+ val hash_map_remove_from_list_loop_fwd_def : thm
+ val hash_map_remove_fwd_def : thm
+ val hash_map_try_resize_fwd_back_def : thm
+ val test1_fwd_def : thm
+
+ val hashmap_Funs_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [hashmap_Types] Parent theory of "hashmap_Funs"
+
+ [core_num_u32_max_body_def] Definition
+
+ ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
+
+ [core_num_u32_max_c_def] Definition
+
+ ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
+
+ [hash_key_fwd_def] Definition
+
+ ⊢ ∀k. hash_key_fwd k = Return k
+
+ [hash_map_allocate_slots_fwd_def] Definition
+
+ ⊢ ∀slots n.
+ hash_map_allocate_slots_fwd slots n =
+ hash_map_allocate_slots_loop_fwd slots n
+
+ [hash_map_allocate_slots_loop_fwd_def] Definition
+
+ ⊢ ∀slots n.
+ hash_map_allocate_slots_loop_fwd slots n =
+ if usize_gt n (int_to_usize 0) then
+ do
+ slots0 <- vec_push_back slots ListNil;
+ n0 <- usize_sub n (int_to_usize 1);
+ hash_map_allocate_slots_loop_fwd slots0 n0
+ od
+ else Return slots
+
+ [hash_map_clear_fwd_back_def] Definition
+
+ ⊢ ∀self.
+ hash_map_clear_fwd_back self =
+ do
+ v <-
+ hash_map_clear_loop_fwd_back self.hash_map_slots
+ (int_to_usize 0);
+ Return
+ (self with
+ <|hash_map_num_entries := int_to_usize 0;
+ hash_map_slots := v|>)
+ od
+
+ [hash_map_clear_loop_fwd_back_def] Definition
+
+ ⊢ ∀slots i.
+ hash_map_clear_loop_fwd_back slots i =
+ (let
+ i0 = vec_len slots
+ in
+ if usize_lt i i0 then
+ do
+ i1 <- usize_add i (int_to_usize 1);
+ slots0 <- vec_index_mut_back slots i ListNil;
+ hash_map_clear_loop_fwd_back slots0 i1
+ od
+ else Return slots)
+
+ [hash_map_contains_key_fwd_def] Definition
+
+ ⊢ ∀self key.
+ hash_map_contains_key_fwd self key =
+ do
+ hash <- hash_key_fwd key;
+ i <<- vec_len self.hash_map_slots;
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_fwd self.hash_map_slots hash_mod;
+ hash_map_contains_key_in_list_fwd key l
+ od
+
+ [hash_map_contains_key_in_list_fwd_def] Definition
+
+ ⊢ ∀key ls.
+ hash_map_contains_key_in_list_fwd key ls =
+ hash_map_contains_key_in_list_loop_fwd key ls
+
+ [hash_map_contains_key_in_list_loop_fwd_def] Definition
+
+ ⊢ ∀key ls.
+ hash_map_contains_key_in_list_loop_fwd key ls =
+ case ls of
+ ListCons ckey t tl =>
+ if ckey = key then Return T
+ else hash_map_contains_key_in_list_loop_fwd key tl
+ | ListNil => Return F
+
+ [hash_map_get_fwd_def] Definition
+
+ ⊢ ∀self key.
+ hash_map_get_fwd self key =
+ do
+ hash <- hash_key_fwd key;
+ i <<- vec_len self.hash_map_slots;
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_fwd self.hash_map_slots hash_mod;
+ hash_map_get_in_list_fwd key l
+ od
+
+ [hash_map_get_in_list_fwd_def] Definition
+
+ ⊢ ∀key ls.
+ hash_map_get_in_list_fwd key ls =
+ hash_map_get_in_list_loop_fwd key ls
+
+ [hash_map_get_in_list_loop_fwd_def] Definition
+
+ ⊢ ∀key ls.
+ hash_map_get_in_list_loop_fwd key ls =
+ case ls of
+ ListCons ckey cvalue tl =>
+ if ckey = key then Return cvalue
+ else hash_map_get_in_list_loop_fwd key tl
+ | ListNil => Fail Failure
+
+ [hash_map_get_mut_back_def] Definition
+
+ ⊢ ∀self key ret.
+ hash_map_get_mut_back self key ret =
+ do
+ hash <- hash_key_fwd key;
+ i <<- vec_len self.hash_map_slots;
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ l0 <- hash_map_get_mut_in_list_back l key ret;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return (self with hash_map_slots := v)
+ od
+
+ [hash_map_get_mut_fwd_def] Definition
+
+ ⊢ ∀self key.
+ hash_map_get_mut_fwd self key =
+ do
+ hash <- hash_key_fwd key;
+ i <<- vec_len self.hash_map_slots;
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ hash_map_get_mut_in_list_fwd l key
+ od
+
+ [hash_map_get_mut_in_list_back_def] Definition
+
+ ⊢ ∀ls key ret.
+ hash_map_get_mut_in_list_back ls key ret =
+ hash_map_get_mut_in_list_loop_back ls key ret
+
+ [hash_map_get_mut_in_list_fwd_def] Definition
+
+ ⊢ ∀ls key.
+ hash_map_get_mut_in_list_fwd ls key =
+ hash_map_get_mut_in_list_loop_fwd ls key
+
+ [hash_map_get_mut_in_list_loop_back_def] Definition
+
+ ⊢ ∀ls key ret.
+ hash_map_get_mut_in_list_loop_back ls key ret =
+ case ls of
+ ListCons ckey cvalue tl =>
+ if ckey = key then Return (ListCons ckey ret tl)
+ else
+ do
+ tl0 <- hash_map_get_mut_in_list_loop_back tl key ret;
+ Return (ListCons ckey cvalue tl0)
+ od
+ | ListNil => Fail Failure
+
+ [hash_map_get_mut_in_list_loop_fwd_def] Definition
+
+ ⊢ ∀ls key.
+ hash_map_get_mut_in_list_loop_fwd ls key =
+ case ls of
+ ListCons ckey cvalue tl =>
+ if ckey = key then Return cvalue
+ else hash_map_get_mut_in_list_loop_fwd tl key
+ | ListNil => Fail Failure
+
+ [hash_map_insert_fwd_back_def] Definition
+
+ ⊢ ∀self key value.
+ hash_map_insert_fwd_back self key value =
+ do
+ self0 <- hash_map_insert_no_resize_fwd_back self key value;
+ i <- hash_map_len_fwd self0;
+ if usize_gt i self0.hash_map_max_load then
+ hash_map_try_resize_fwd_back self0
+ else Return self0
+ od
+
+ [hash_map_insert_in_list_back_def] Definition
+
+ ⊢ ∀key value ls.
+ hash_map_insert_in_list_back key value ls =
+ hash_map_insert_in_list_loop_back key value ls
+
+ [hash_map_insert_in_list_fwd_def] Definition
+
+ ⊢ ∀key value ls.
+ hash_map_insert_in_list_fwd key value ls =
+ hash_map_insert_in_list_loop_fwd key value ls
+
+ [hash_map_insert_in_list_loop_back_def] Definition
+
+ ⊢ ∀key value ls.
+ hash_map_insert_in_list_loop_back key value ls =
+ case ls of
+ ListCons ckey cvalue tl =>
+ if ckey = key then Return (ListCons ckey value tl)
+ else
+ do
+ tl0 <- hash_map_insert_in_list_loop_back key value tl;
+ Return (ListCons ckey cvalue tl0)
+ od
+ | ListNil => (let l = ListNil in Return (ListCons key value l))
+
+ [hash_map_insert_in_list_loop_fwd_def] Definition
+
+ ⊢ ∀key value ls.
+ hash_map_insert_in_list_loop_fwd key value ls =
+ case ls of
+ ListCons ckey cvalue tl =>
+ if ckey = key then Return F
+ else hash_map_insert_in_list_loop_fwd key value tl
+ | ListNil => Return T
+
+ [hash_map_insert_no_resize_fwd_back_def] Definition
+
+ ⊢ ∀self key value.
+ hash_map_insert_no_resize_fwd_back self key value =
+ do
+ hash <- hash_key_fwd key;
+ i <<- vec_len self.hash_map_slots;
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ inserted <- hash_map_insert_in_list_fwd key value l;
+ if inserted then
+ do
+ i0 <- usize_add self.hash_map_num_entries (int_to_usize 1);
+ l0 <- hash_map_insert_in_list_back key value l;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return
+ (self with
+ <|hash_map_num_entries := i0; hash_map_slots := v|>)
+ od
+ else
+ do
+ l0 <- hash_map_insert_in_list_back key value l;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return (self with hash_map_slots := v)
+ od
+ od
+
+ [hash_map_len_fwd_def] Definition
+
+ ⊢ ∀self. hash_map_len_fwd self = Return self.hash_map_num_entries
+
+ [hash_map_move_elements_from_list_fwd_back_def] Definition
+
+ ⊢ ∀ntable ls.
+ hash_map_move_elements_from_list_fwd_back ntable ls =
+ hash_map_move_elements_from_list_loop_fwd_back ntable ls
+
+ [hash_map_move_elements_from_list_loop_fwd_back_def] Definition
+
+ ⊢ ∀ntable ls.
+ hash_map_move_elements_from_list_loop_fwd_back ntable ls =
+ case ls of
+ ListCons k v tl =>
+ do
+ ntable0 <- hash_map_insert_no_resize_fwd_back ntable k v;
+ hash_map_move_elements_from_list_loop_fwd_back ntable0 tl
+ od
+ | ListNil => Return ntable
+
+ [hash_map_move_elements_fwd_back_def] Definition
+
+ ⊢ ∀ntable slots i.
+ hash_map_move_elements_fwd_back ntable slots i =
+ hash_map_move_elements_loop_fwd_back ntable slots i
+
+ [hash_map_move_elements_loop_fwd_back_def] Definition
+
+ ⊢ ∀ntable slots i.
+ hash_map_move_elements_loop_fwd_back ntable slots i =
+ (let
+ i0 = vec_len slots
+ in
+ if usize_lt i i0 then
+ do
+ l <- vec_index_mut_fwd slots i;
+ ls <<- mem_replace_fwd l ListNil;
+ ntable0 <-
+ hash_map_move_elements_from_list_fwd_back ntable ls;
+ i1 <- usize_add i (int_to_usize 1);
+ l0 <<- mem_replace_back l ListNil;
+ slots0 <- vec_index_mut_back slots i l0;
+ hash_map_move_elements_loop_fwd_back ntable0 slots0 i1
+ od
+ else Return (ntable,slots))
+
+ [hash_map_new_fwd_def] Definition
+
+ ⊢ hash_map_new_fwd =
+ hash_map_new_with_capacity_fwd (int_to_usize 32) (int_to_usize 4)
+ (int_to_usize 5)
+
+ [hash_map_new_with_capacity_fwd_def] Definition
+
+ ⊢ ∀capacity max_load_dividend max_load_divisor.
+ hash_map_new_with_capacity_fwd capacity max_load_dividend
+ max_load_divisor =
+ (let
+ v = vec_new
+ in
+ do
+ slots <- hash_map_allocate_slots_fwd v capacity;
+ i <- usize_mul capacity max_load_dividend;
+ i0 <- usize_div i max_load_divisor;
+ Return
+ <|hash_map_num_entries := int_to_usize 0;
+ hash_map_max_load_factor :=
+ (max_load_dividend,max_load_divisor);
+ hash_map_max_load := i0; hash_map_slots := slots|>
+ od)
+
+ [hash_map_remove_back_def] Definition
+
+ ⊢ ∀self key.
+ hash_map_remove_back self key =
+ do
+ hash <- hash_key_fwd key;
+ i <<- vec_len self.hash_map_slots;
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ x <- hash_map_remove_from_list_fwd key l;
+ case x of
+ NONE =>
+ do
+ l0 <- hash_map_remove_from_list_back key l;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return (self with hash_map_slots := v)
+ od
+ | SOME x0 =>
+ do
+ i0 <- usize_sub self.hash_map_num_entries (int_to_usize 1);
+ l0 <- hash_map_remove_from_list_back key l;
+ v <- vec_index_mut_back self.hash_map_slots hash_mod l0;
+ Return
+ (self with
+ <|hash_map_num_entries := i0; hash_map_slots := v|>)
+ od
+ od
+
+ [hash_map_remove_from_list_back_def] Definition
+
+ ⊢ ∀key ls.
+ hash_map_remove_from_list_back key ls =
+ hash_map_remove_from_list_loop_back key ls
+
+ [hash_map_remove_from_list_fwd_def] Definition
+
+ ⊢ ∀key ls.
+ hash_map_remove_from_list_fwd key ls =
+ hash_map_remove_from_list_loop_fwd key ls
+
+ [hash_map_remove_from_list_loop_back_def] Definition
+
+ ⊢ ∀key ls.
+ hash_map_remove_from_list_loop_back key ls =
+ case ls of
+ ListCons ckey t tl =>
+ if ckey = key then
+ (let
+ mv_ls = mem_replace_fwd (ListCons ckey t tl) ListNil
+ in
+ case mv_ls of
+ ListCons i cvalue tl0 => Return tl0
+ | ListNil => Fail Failure)
+ else
+ do
+ tl0 <- hash_map_remove_from_list_loop_back key tl;
+ Return (ListCons ckey t tl0)
+ od
+ | ListNil => Return ListNil
+
+ [hash_map_remove_from_list_loop_fwd_def] Definition
+
+ ⊢ ∀key ls.
+ hash_map_remove_from_list_loop_fwd key ls =
+ case ls of
+ ListCons ckey t tl =>
+ if ckey = key then
+ (let
+ mv_ls = mem_replace_fwd (ListCons ckey t tl) ListNil
+ in
+ case mv_ls of
+ ListCons i cvalue tl0 => Return (SOME cvalue)
+ | ListNil => Fail Failure)
+ else hash_map_remove_from_list_loop_fwd key tl
+ | ListNil => Return NONE
+
+ [hash_map_remove_fwd_def] Definition
+
+ ⊢ ∀self key.
+ hash_map_remove_fwd self key =
+ do
+ hash <- hash_key_fwd key;
+ i <<- vec_len self.hash_map_slots;
+ hash_mod <- usize_rem hash i;
+ l <- vec_index_mut_fwd self.hash_map_slots hash_mod;
+ x <- hash_map_remove_from_list_fwd key l;
+ case x of
+ NONE => Return NONE
+ | SOME x0 =>
+ monad_ignore_bind
+ (usize_sub self.hash_map_num_entries (int_to_usize 1))
+ (Return (SOME x0))
+ od
+
+ [hash_map_try_resize_fwd_back_def] Definition
+
+ ⊢ ∀self.
+ hash_map_try_resize_fwd_back self =
+ do
+ max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+ capacity <<- vec_len self.hash_map_slots;
+ n1 <- usize_div max_usize (int_to_usize 2);
+ (i,i0) <<- self.hash_map_max_load_factor;
+ i1 <- usize_div n1 i;
+ if usize_le capacity i1 then
+ do
+ i2 <- usize_mul capacity (int_to_usize 2);
+ ntable <- hash_map_new_with_capacity_fwd i2 i i0;
+ (ntable0,_) <-
+ hash_map_move_elements_fwd_back ntable
+ self.hash_map_slots (int_to_usize 0);
+ Return
+ (ntable0 with
+ <|hash_map_num_entries := self.hash_map_num_entries;
+ hash_map_max_load_factor := (i,i0)|>)
+ od
+ else Return (self with hash_map_max_load_factor := (i,i0))
+ od
+
+ [test1_fwd_def] Definition
+
+ ⊢ test1_fwd =
+ do
+ hm <- hash_map_new_fwd;
+ hm0 <-
+ hash_map_insert_fwd_back hm (int_to_usize 0) (int_to_u64 42);
+ hm1 <-
+ hash_map_insert_fwd_back hm0 (int_to_usize 128) (int_to_u64 18);
+ hm2 <-
+ hash_map_insert_fwd_back hm1 (int_to_usize 1024)
+ (int_to_u64 138);
+ hm3 <-
+ hash_map_insert_fwd_back hm2 (int_to_usize 1056)
+ (int_to_u64 256);
+ i <- hash_map_get_fwd hm3 (int_to_usize 128);
+ if i ≠ int_to_u64 18 then Fail Failure
+ else
+ do
+ hm4 <-
+ hash_map_get_mut_back hm3 (int_to_usize 1024)
+ (int_to_u64 56);
+ i0 <- hash_map_get_fwd hm4 (int_to_usize 1024);
+ if i0 ≠ int_to_u64 56 then Fail Failure
+ else
+ do
+ x <- hash_map_remove_fwd hm4 (int_to_usize 1024);
+ case x of
+ NONE => Fail Failure
+ | SOME x0 =>
+ if x0 ≠ int_to_u64 56 then Fail Failure
+ else
+ do
+ hm5 <- hash_map_remove_back hm4 (int_to_usize 1024);
+ i1 <- hash_map_get_fwd hm5 (int_to_usize 0);
+ if i1 ≠ int_to_u64 42 then Fail Failure
+ else
+ do
+ i2 <- hash_map_get_fwd hm5 (int_to_usize 128);
+ if i2 ≠ int_to_u64 18 then Fail Failure
+ else
+ do
+ i3 <-
+ hash_map_get_fwd hm5 (int_to_usize 1056);
+ if i3 ≠ int_to_u64 256 then Fail Failure
+ else Return ()
+ od
+ od
+ od
+ od
+ od
+ od
+
+
+*)
+end
diff --git a/tests/hol4/hashmap/hashmap_TypesScript.sml b/tests/hol4/hashmap/hashmap_TypesScript.sml
new file mode 100644
index 00000000..a0865956
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_TypesScript.sml
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap]: type definitions *)
+open primitivesLib divDefLib
+
+val _ = new_theory "hashmap_Types"
+
+
+Datatype:
+ (** [hashmap::List] *)
+ list_t = | ListCons usize 't list_t | ListNil
+End
+
+Datatype:
+ (** [hashmap::HashMap] *)
+ hash_map_t =
+ <|
+ hash_map_num_entries : usize;
+ hash_map_max_load_factor : (usize # usize);
+ hash_map_max_load : usize;
+ hash_map_slots : 't list_t vec;
+ |>
+End
+
+val _ = export_theory ()
diff --git a/tests/hol4/hashmap/hashmap_TypesTheory.sig b/tests/hol4/hashmap/hashmap_TypesTheory.sig
new file mode 100644
index 00000000..4ad77ac5
--- /dev/null
+++ b/tests/hol4/hashmap/hashmap_TypesTheory.sig
@@ -0,0 +1,494 @@
+signature hashmap_TypesTheory =
+sig
+ type thm = Thm.thm
+
+ (* Definitions *)
+ val hash_map_t_TY_DEF : thm
+ val hash_map_t_case_def : thm
+ val hash_map_t_size_def : thm
+ val list_t_TY_DEF : thm
+ val list_t_case_def : thm
+ val list_t_size_def : thm
+ val recordtype_hash_map_t_seldef_hash_map_max_load_def : thm
+ val recordtype_hash_map_t_seldef_hash_map_max_load_factor_def : thm
+ val recordtype_hash_map_t_seldef_hash_map_max_load_factor_fupd_def : thm
+ val recordtype_hash_map_t_seldef_hash_map_max_load_fupd_def : thm
+ val recordtype_hash_map_t_seldef_hash_map_num_entries_def : thm
+ val recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def : thm
+ val recordtype_hash_map_t_seldef_hash_map_slots_def : thm
+ val recordtype_hash_map_t_seldef_hash_map_slots_fupd_def : thm
+
+ (* Theorems *)
+ val EXISTS_hash_map_t : thm
+ val FORALL_hash_map_t : thm
+ val datatype_hash_map_t : thm
+ val datatype_list_t : thm
+ val hash_map_t_11 : thm
+ val hash_map_t_Axiom : thm
+ val hash_map_t_accessors : thm
+ val hash_map_t_accfupds : thm
+ val hash_map_t_case_cong : thm
+ val hash_map_t_case_eq : thm
+ val hash_map_t_component_equality : thm
+ val hash_map_t_fn_updates : thm
+ val hash_map_t_fupdcanon : thm
+ val hash_map_t_fupdcanon_comp : thm
+ val hash_map_t_fupdfupds : thm
+ val hash_map_t_fupdfupds_comp : thm
+ val hash_map_t_induction : thm
+ val hash_map_t_literal_11 : thm
+ val hash_map_t_literal_nchotomy : thm
+ val hash_map_t_nchotomy : thm
+ val hash_map_t_updates_eq_literal : thm
+ val list_t_11 : thm
+ val list_t_Axiom : thm
+ val list_t_case_cong : thm
+ val list_t_case_eq : thm
+ val list_t_distinct : thm
+ val list_t_induction : thm
+ val list_t_nchotomy : thm
+
+ val hashmap_Types_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [divDef] Parent theory of "hashmap_Types"
+
+ [hash_map_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0'.
+ ∀ $var$('hash_map_t').
+ (∀a0'.
+ (∃a0 a1 a2 a3.
+ a0' =
+ (λa0 a1 a2 a3.
+ ind_type$CONSTR 0 (a0,a1,a2,a3)
+ (λn. ind_type$BOTTOM)) a0 a1 a2 a3) ⇒
+ $var$('hash_map_t') a0') ⇒
+ $var$('hash_map_t') a0') rep
+
+ [hash_map_t_case_def] Definition
+
+ ⊢ ∀a0 a1 a2 a3 f.
+ hash_map_t_CASE (hash_map_t a0 a1 a2 a3) f = f a0 a1 a2 a3
+
+ [hash_map_t_size_def] Definition
+
+ ⊢ ∀f a0 a1 a2 a3.
+ hash_map_t_size f (hash_map_t a0 a1 a2 a3) =
+ 1 + pair_size (λv. 0) (λv. 0) a1
+
+ [list_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0'.
+ ∀ $var$('list_t').
+ (∀a0'.
+ (∃a0 a1 a2.
+ a0' =
+ (λa0 a1 a2.
+ ind_type$CONSTR 0 (a0,a1)
+ (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))
+ a0 a1 a2 ∧ $var$('list_t') a2) ∨
+ a0' =
+ ind_type$CONSTR (SUC 0) (ARB,ARB)
+ (λn. ind_type$BOTTOM) ⇒
+ $var$('list_t') a0') ⇒
+ $var$('list_t') a0') rep
+
+ [list_t_case_def] Definition
+
+ ⊢ (∀a0 a1 a2 f v. list_t_CASE (ListCons a0 a1 a2) f v = f a0 a1 a2) ∧
+ ∀f v. list_t_CASE ListNil f v = v
+
+ [list_t_size_def] Definition
+
+ ⊢ (∀f a0 a1 a2.
+ list_t_size f (ListCons a0 a1 a2) =
+ 1 + (f a1 + list_t_size f a2)) ∧ ∀f. list_t_size f ListNil = 0
+
+ [recordtype_hash_map_t_seldef_hash_map_max_load_def] Definition
+
+ ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load = u0
+
+ [recordtype_hash_map_t_seldef_hash_map_max_load_factor_def] Definition
+
+ ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load_factor = p
+
+ [recordtype_hash_map_t_seldef_hash_map_max_load_factor_fupd_def] Definition
+
+ ⊢ ∀f u p u0 v.
+ hash_map_t u p u0 v with hash_map_max_load_factor updated_by f =
+ hash_map_t u (f p) u0 v
+
+ [recordtype_hash_map_t_seldef_hash_map_max_load_fupd_def] Definition
+
+ ⊢ ∀f u p u0 v.
+ hash_map_t u p u0 v with hash_map_max_load updated_by f =
+ hash_map_t u p (f u0) v
+
+ [recordtype_hash_map_t_seldef_hash_map_num_entries_def] Definition
+
+ ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_num_entries = u
+
+ [recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def] Definition
+
+ ⊢ ∀f u p u0 v.
+ hash_map_t u p u0 v with hash_map_num_entries updated_by f =
+ hash_map_t (f u) p u0 v
+
+ [recordtype_hash_map_t_seldef_hash_map_slots_def] Definition
+
+ ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_slots = v
+
+ [recordtype_hash_map_t_seldef_hash_map_slots_fupd_def] Definition
+
+ ⊢ ∀f u p u0 v.
+ hash_map_t u p u0 v with hash_map_slots updated_by f =
+ hash_map_t u p u0 (f v)
+
+ [EXISTS_hash_map_t] Theorem
+
+ ⊢ ∀P. (∃h. P h) ⇔
+ ∃u0 p u v.
+ P
+ <|hash_map_num_entries := u0;
+ hash_map_max_load_factor := p; hash_map_max_load := u;
+ hash_map_slots := v|>
+
+ [FORALL_hash_map_t] Theorem
+
+ ⊢ ∀P. (∀h. P h) ⇔
+ ∀u0 p u v.
+ P
+ <|hash_map_num_entries := u0;
+ hash_map_max_load_factor := p; hash_map_max_load := u;
+ hash_map_slots := v|>
+
+ [datatype_hash_map_t] Theorem
+
+ ⊢ DATATYPE
+ (record hash_map_t hash_map_num_entries hash_map_max_load_factor
+ hash_map_max_load hash_map_slots)
+
+ [datatype_list_t] Theorem
+
+ ⊢ DATATYPE (list_t ListCons ListNil)
+
+ [hash_map_t_11] Theorem
+
+ ⊢ ∀a0 a1 a2 a3 a0' a1' a2' a3'.
+ hash_map_t a0 a1 a2 a3 = hash_map_t a0' a1' a2' a3' ⇔
+ a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3'
+
+ [hash_map_t_Axiom] Theorem
+
+ ⊢ ∀f. ∃fn. ∀a0 a1 a2 a3. fn (hash_map_t a0 a1 a2 a3) = f a0 a1 a2 a3
+
+ [hash_map_t_accessors] Theorem
+
+ ⊢ (∀u p u0 v. (hash_map_t u p u0 v).hash_map_num_entries = u) ∧
+ (∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load_factor = p) ∧
+ (∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load = u0) ∧
+ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_slots = v
+
+ [hash_map_t_accfupds] Theorem
+
+ ⊢ (∀h f.
+ (h with hash_map_max_load_factor updated_by f).
+ hash_map_num_entries =
+ h.hash_map_num_entries) ∧
+ (∀h f.
+ (h with hash_map_max_load updated_by f).hash_map_num_entries =
+ h.hash_map_num_entries) ∧
+ (∀h f.
+ (h with hash_map_slots updated_by f).hash_map_num_entries =
+ h.hash_map_num_entries) ∧
+ (∀h f.
+ (h with hash_map_num_entries updated_by f).
+ hash_map_max_load_factor =
+ h.hash_map_max_load_factor) ∧
+ (∀h f.
+ (h with hash_map_max_load updated_by f).hash_map_max_load_factor =
+ h.hash_map_max_load_factor) ∧
+ (∀h f.
+ (h with hash_map_slots updated_by f).hash_map_max_load_factor =
+ h.hash_map_max_load_factor) ∧
+ (∀h f.
+ (h with hash_map_num_entries updated_by f).hash_map_max_load =
+ h.hash_map_max_load) ∧
+ (∀h f.
+ (h with hash_map_max_load_factor updated_by f).hash_map_max_load =
+ h.hash_map_max_load) ∧
+ (∀h f.
+ (h with hash_map_slots updated_by f).hash_map_max_load =
+ h.hash_map_max_load) ∧
+ (∀h f.
+ (h with hash_map_num_entries updated_by f).hash_map_slots =
+ h.hash_map_slots) ∧
+ (∀h f.
+ (h with hash_map_max_load_factor updated_by f).hash_map_slots =
+ h.hash_map_slots) ∧
+ (∀h f.
+ (h with hash_map_max_load updated_by f).hash_map_slots =
+ h.hash_map_slots) ∧
+ (∀h f.
+ (h with hash_map_num_entries updated_by f).hash_map_num_entries =
+ f h.hash_map_num_entries) ∧
+ (∀h f.
+ (h with hash_map_max_load_factor updated_by f).
+ hash_map_max_load_factor =
+ f h.hash_map_max_load_factor) ∧
+ (∀h f.
+ (h with hash_map_max_load updated_by f).hash_map_max_load =
+ f h.hash_map_max_load) ∧
+ ∀h f.
+ (h with hash_map_slots updated_by f).hash_map_slots =
+ f h.hash_map_slots
+
+ [hash_map_t_case_cong] Theorem
+
+ ⊢ ∀M M' f.
+ M = M' ∧
+ (∀a0 a1 a2 a3.
+ M' = hash_map_t a0 a1 a2 a3 ⇒ f a0 a1 a2 a3 = f' a0 a1 a2 a3) ⇒
+ hash_map_t_CASE M f = hash_map_t_CASE M' f'
+
+ [hash_map_t_case_eq] Theorem
+
+ ⊢ hash_map_t_CASE x f = v ⇔
+ ∃u p u0 v'. x = hash_map_t u p u0 v' ∧ f u p u0 v' = v
+
+ [hash_map_t_component_equality] Theorem
+
+ ⊢ ∀h1 h2.
+ h1 = h2 ⇔
+ h1.hash_map_num_entries = h2.hash_map_num_entries ∧
+ h1.hash_map_max_load_factor = h2.hash_map_max_load_factor ∧
+ h1.hash_map_max_load = h2.hash_map_max_load ∧
+ h1.hash_map_slots = h2.hash_map_slots
+
+ [hash_map_t_fn_updates] Theorem
+
+ ⊢ (∀f u p u0 v.
+ hash_map_t u p u0 v with hash_map_num_entries updated_by f =
+ hash_map_t (f u) p u0 v) ∧
+ (∀f u p u0 v.
+ hash_map_t u p u0 v with hash_map_max_load_factor updated_by f =
+ hash_map_t u (f p) u0 v) ∧
+ (∀f u p u0 v.
+ hash_map_t u p u0 v with hash_map_max_load updated_by f =
+ hash_map_t u p (f u0) v) ∧
+ ∀f u p u0 v.
+ hash_map_t u p u0 v with hash_map_slots updated_by f =
+ hash_map_t u p u0 (f v)
+
+ [hash_map_t_fupdcanon] Theorem
+
+ ⊢ (∀h g f.
+ h with
+ <|hash_map_max_load_factor updated_by f;
+ hash_map_num_entries updated_by g|> =
+ h with
+ <|hash_map_num_entries updated_by g;
+ hash_map_max_load_factor updated_by f|>) ∧
+ (∀h g f.
+ h with
+ <|hash_map_max_load updated_by f;
+ hash_map_num_entries updated_by g|> =
+ h with
+ <|hash_map_num_entries updated_by g;
+ hash_map_max_load updated_by f|>) ∧
+ (∀h g f.
+ h with
+ <|hash_map_max_load updated_by f;
+ hash_map_max_load_factor updated_by g|> =
+ h with
+ <|hash_map_max_load_factor updated_by g;
+ hash_map_max_load updated_by f|>) ∧
+ (∀h g f.
+ h with
+ <|hash_map_slots updated_by f;
+ hash_map_num_entries updated_by g|> =
+ h with
+ <|hash_map_num_entries updated_by g;
+ hash_map_slots updated_by f|>) ∧
+ (∀h g f.
+ h with
+ <|hash_map_slots updated_by f;
+ hash_map_max_load_factor updated_by g|> =
+ h with
+ <|hash_map_max_load_factor updated_by g;
+ hash_map_slots updated_by f|>) ∧
+ ∀h g f.
+ h with
+ <|hash_map_slots updated_by f; hash_map_max_load updated_by g|> =
+ h with
+ <|hash_map_max_load updated_by g; hash_map_slots updated_by f|>
+
+ [hash_map_t_fupdcanon_comp] Theorem
+
+ ⊢ ((∀g f.
+ hash_map_max_load_factor_fupd f ∘ hash_map_num_entries_fupd g =
+ hash_map_num_entries_fupd g ∘ hash_map_max_load_factor_fupd f) ∧
+ ∀h g f.
+ hash_map_max_load_factor_fupd f ∘ hash_map_num_entries_fupd g ∘
+ h =
+ hash_map_num_entries_fupd g ∘ hash_map_max_load_factor_fupd f ∘
+ h) ∧
+ ((∀g f.
+ hash_map_max_load_fupd f ∘ hash_map_num_entries_fupd g =
+ hash_map_num_entries_fupd g ∘ hash_map_max_load_fupd f) ∧
+ ∀h g f.
+ hash_map_max_load_fupd f ∘ hash_map_num_entries_fupd g ∘ h =
+ hash_map_num_entries_fupd g ∘ hash_map_max_load_fupd f ∘ h) ∧
+ ((∀g f.
+ hash_map_max_load_fupd f ∘ hash_map_max_load_factor_fupd g =
+ hash_map_max_load_factor_fupd g ∘ hash_map_max_load_fupd f) ∧
+ ∀h g f.
+ hash_map_max_load_fupd f ∘ hash_map_max_load_factor_fupd g ∘ h =
+ hash_map_max_load_factor_fupd g ∘ hash_map_max_load_fupd f ∘ h) ∧
+ ((∀g f.
+ hash_map_slots_fupd f ∘ hash_map_num_entries_fupd g =
+ hash_map_num_entries_fupd g ∘ hash_map_slots_fupd f) ∧
+ ∀h g f.
+ hash_map_slots_fupd f ∘ hash_map_num_entries_fupd g ∘ h =
+ hash_map_num_entries_fupd g ∘ hash_map_slots_fupd f ∘ h) ∧
+ ((∀g f.
+ hash_map_slots_fupd f ∘ hash_map_max_load_factor_fupd g =
+ hash_map_max_load_factor_fupd g ∘ hash_map_slots_fupd f) ∧
+ ∀h g f.
+ hash_map_slots_fupd f ∘ hash_map_max_load_factor_fupd g ∘ h =
+ hash_map_max_load_factor_fupd g ∘ hash_map_slots_fupd f ∘ h) ∧
+ (∀g f.
+ hash_map_slots_fupd f ∘ hash_map_max_load_fupd g =
+ hash_map_max_load_fupd g ∘ hash_map_slots_fupd f) ∧
+ ∀h g f.
+ hash_map_slots_fupd f ∘ hash_map_max_load_fupd g ∘ h =
+ hash_map_max_load_fupd g ∘ hash_map_slots_fupd f ∘ h
+
+ [hash_map_t_fupdfupds] Theorem
+
+ ⊢ (∀h g f.
+ h with
+ <|hash_map_num_entries updated_by f;
+ hash_map_num_entries updated_by g|> =
+ h with hash_map_num_entries updated_by f ∘ g) ∧
+ (∀h g f.
+ h with
+ <|hash_map_max_load_factor updated_by f;
+ hash_map_max_load_factor updated_by g|> =
+ h with hash_map_max_load_factor updated_by f ∘ g) ∧
+ (∀h g f.
+ h with
+ <|hash_map_max_load updated_by f;
+ hash_map_max_load updated_by g|> =
+ h with hash_map_max_load updated_by f ∘ g) ∧
+ ∀h g f.
+ h with
+ <|hash_map_slots updated_by f; hash_map_slots updated_by g|> =
+ h with hash_map_slots updated_by f ∘ g
+
+ [hash_map_t_fupdfupds_comp] Theorem
+
+ ⊢ ((∀g f.
+ hash_map_num_entries_fupd f ∘ hash_map_num_entries_fupd g =
+ hash_map_num_entries_fupd (f ∘ g)) ∧
+ ∀h g f.
+ hash_map_num_entries_fupd f ∘ hash_map_num_entries_fupd g ∘ h =
+ hash_map_num_entries_fupd (f ∘ g) ∘ h) ∧
+ ((∀g f.
+ hash_map_max_load_factor_fupd f ∘
+ hash_map_max_load_factor_fupd g =
+ hash_map_max_load_factor_fupd (f ∘ g)) ∧
+ ∀h g f.
+ hash_map_max_load_factor_fupd f ∘
+ hash_map_max_load_factor_fupd g ∘ h =
+ hash_map_max_load_factor_fupd (f ∘ g) ∘ h) ∧
+ ((∀g f.
+ hash_map_max_load_fupd f ∘ hash_map_max_load_fupd g =
+ hash_map_max_load_fupd (f ∘ g)) ∧
+ ∀h g f.
+ hash_map_max_load_fupd f ∘ hash_map_max_load_fupd g ∘ h =
+ hash_map_max_load_fupd (f ∘ g) ∘ h) ∧
+ (∀g f.
+ hash_map_slots_fupd f ∘ hash_map_slots_fupd g =
+ hash_map_slots_fupd (f ∘ g)) ∧
+ ∀h g f.
+ hash_map_slots_fupd f ∘ hash_map_slots_fupd g ∘ h =
+ hash_map_slots_fupd (f ∘ g) ∘ h
+
+ [hash_map_t_induction] Theorem
+
+ ⊢ ∀P. (∀u p u0 v. P (hash_map_t u p u0 v)) ⇒ ∀h. P h
+
+ [hash_map_t_literal_11] Theorem
+
+ ⊢ ∀u01 p1 u1 v1 u02 p2 u2 v2.
+ <|hash_map_num_entries := u01; hash_map_max_load_factor := p1;
+ hash_map_max_load := u1; hash_map_slots := v1|> =
+ <|hash_map_num_entries := u02; hash_map_max_load_factor := p2;
+ hash_map_max_load := u2; hash_map_slots := v2|> ⇔
+ u01 = u02 ∧ p1 = p2 ∧ u1 = u2 ∧ v1 = v2
+
+ [hash_map_t_literal_nchotomy] Theorem
+
+ ⊢ ∀h. ∃u0 p u v.
+ h =
+ <|hash_map_num_entries := u0; hash_map_max_load_factor := p;
+ hash_map_max_load := u; hash_map_slots := v|>
+
+ [hash_map_t_nchotomy] Theorem
+
+ ⊢ ∀hh. ∃u p u0 v. hh = hash_map_t u p u0 v
+
+ [hash_map_t_updates_eq_literal] Theorem
+
+ ⊢ ∀h u0 p u v.
+ h with
+ <|hash_map_num_entries := u0; hash_map_max_load_factor := p;
+ hash_map_max_load := u; hash_map_slots := v|> =
+ <|hash_map_num_entries := u0; hash_map_max_load_factor := p;
+ hash_map_max_load := u; hash_map_slots := v|>
+
+ [list_t_11] Theorem
+
+ ⊢ ∀a0 a1 a2 a0' a1' a2'.
+ ListCons a0 a1 a2 = ListCons a0' a1' a2' ⇔
+ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
+
+ [list_t_Axiom] Theorem
+
+ ⊢ ∀f0 f1. ∃fn.
+ (∀a0 a1 a2. fn (ListCons a0 a1 a2) = f0 a0 a1 a2 (fn a2)) ∧
+ fn ListNil = f1
+
+ [list_t_case_cong] Theorem
+
+ ⊢ ∀M M' f v.
+ M = M' ∧
+ (∀a0 a1 a2. M' = ListCons a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ∧
+ (M' = ListNil ⇒ v = v') ⇒
+ list_t_CASE M f v = list_t_CASE M' f' v'
+
+ [list_t_case_eq] Theorem
+
+ ⊢ list_t_CASE x f v = v' ⇔
+ (∃u t l. x = ListCons u t l ∧ f u t l = v') ∨ x = ListNil ∧ v = v'
+
+ [list_t_distinct] Theorem
+
+ ⊢ ∀a2 a1 a0. ListCons a0 a1 a2 ≠ ListNil
+
+ [list_t_induction] Theorem
+
+ ⊢ ∀P. (∀l. P l ⇒ ∀t u. P (ListCons u t l)) ∧ P ListNil ⇒ ∀l. P l
+
+ [list_t_nchotomy] Theorem
+
+ ⊢ ∀ll. (∃u t l. ll = ListCons u t l) ∨ ll = ListNil
+
+
+*)
+end