From bd5706896dec0a1aef1accdf51f93af00c5dc6fe Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 15 Nov 2022 15:23:16 +0100 Subject: Improve formatting --- tests/coq/hashmap/Hashmap__Funs.v | 130 ++++++++++++++++++------------------- tests/coq/hashmap/Hashmap__Types.v | 23 ++++--- 2 files changed, 76 insertions(+), 77 deletions(-) (limited to 'tests/coq/hashmap') diff --git a/tests/coq/hashmap/Hashmap__Funs.v b/tests/coq/hashmap/Hashmap__Funs.v index 93aa389b..7d897c8a 100644 --- a/tests/coq/hashmap/Hashmap__Funs.v +++ b/tests/coq/hashmap/Hashmap__Funs.v @@ -4,12 +4,12 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export Hashmap__Types . -Import Hashmap__Types . -Module Hashmap__Funs . +Require Export Hashmap__Types. +Import Hashmap__Types. +Module Hashmap__Funs. (** [hashmap::hash_key] *) -Definition hash_key_fwd (k : usize) : result usize := Return k . +Definition hash_key_fwd (k : usize) : result usize := Return k. (** [hashmap::HashMap::{0}::allocate_slots] *) Fixpoint hash_map_allocate_slots_fwd @@ -19,15 +19,15 @@ Fixpoint hash_map_allocate_slots_fwd match n with | O => Fail_ OutOfFuel | S n1 => - if n0 s= 0 %usize + if n0 s= 0%usize then Return slots else ( slots0 <- vec_push_back (List_t T) slots ListNil; - i <- usize_sub n0 1 %usize; + i <- usize_sub n0 1%usize; v <- hash_map_allocate_slots_fwd T n1 slots0 i; Return v) end - . +. (** [hashmap::HashMap::{0}::new_with_capacity] *) Definition hash_map_new_with_capacity_fwd @@ -42,21 +42,20 @@ Definition hash_map_new_with_capacity_fwd slots <- hash_map_allocate_slots_fwd T n0 v capacity; i <- usize_mul capacity max_load_dividend; i0 <- usize_div i max_load_divisor; - Return (mkHash_map_t (0 %usize) (max_load_dividend, max_load_divisor) i0 + Return (mkHash_map_t (0%usize) (max_load_dividend, max_load_divisor) i0 slots) end - . +. (** [hashmap::HashMap::{0}::new] *) Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) := match n with | O => Fail_ OutOfFuel | S n0 => - hm <- - hash_map_new_with_capacity_fwd T n0 (32 %usize) (4 %usize) (5 %usize); + hm <- hash_map_new_with_capacity_fwd T n0 (32%usize) (4%usize) (5%usize); Return hm end - . +. (** [hashmap::HashMap::{0}::clear_slots] *) Fixpoint hash_map_clear_slots_fwd_back @@ -70,12 +69,12 @@ Fixpoint hash_map_clear_slots_fwd_back if i s< i0 then ( slots0 <- vec_index_mut_back (List_t T) slots i ListNil; - i1 <- usize_add i 1 %usize; + i1 <- usize_add i 1%usize; slots1 <- hash_map_clear_slots_fwd_back T n0 slots0 i1; Return slots1) else Return slots end - . +. (** [hashmap::HashMap::{0}::clear] *) Definition hash_map_clear_fwd_back @@ -85,15 +84,16 @@ Definition hash_map_clear_fwd_back | S n0 => match self with | mkHash_map_t i p i0 v => - v0 <- hash_map_clear_slots_fwd_back T n0 v (0 %usize); - Return (mkHash_map_t (0 %usize) p i0 v0) + v0 <- hash_map_clear_slots_fwd_back T n0 v (0%usize); + Return (mkHash_map_t (0%usize) p i0 v0) end end - . +. (** [hashmap::HashMap::{0}::len] *) Definition hash_map_len_fwd (T : Type) (self : Hash_map_t T) : result usize := - match self with | mkHash_map_t i p i0 v => Return i end . + match self with | mkHash_map_t i p i0 v => Return i end +. (** [hashmap::HashMap::{0}::insert_in_list] *) Fixpoint hash_map_insert_in_list_fwd @@ -111,7 +111,7 @@ Fixpoint hash_map_insert_in_list_fwd | ListNil => Return true end end - . +. (** [hashmap::HashMap::{0}::insert_in_list] *) Fixpoint hash_map_insert_in_list_back @@ -131,7 +131,7 @@ Fixpoint hash_map_insert_in_list_back | ListNil => let l := ListNil in Return (ListCons key value l) end end - . +. (** [hashmap::HashMap::{0}::insert_no_resize] *) Definition hash_map_insert_no_resize_fwd_back @@ -150,7 +150,7 @@ Definition hash_map_insert_no_resize_fwd_back inserted <- hash_map_insert_in_list_fwd T n0 key value l; if inserted then ( - i2 <- usize_add i 1 %usize; + i2 <- usize_add i 1%usize; l0 <- hash_map_insert_in_list_back T n0 key value l; v0 <- vec_index_mut_back (List_t T) v hash_mod l0; Return (mkHash_map_t i2 p i0 v0)) @@ -160,11 +160,11 @@ Definition hash_map_insert_no_resize_fwd_back Return (mkHash_map_t i p i0 v0)) end end - . +. (** [core::num::u32::{9}::MAX] *) -Definition core_num_u32_max_body : result u32 := Return (4294967295 %u32) . -Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global . +Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). +Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** [hashmap::HashMap::{0}::move_elements_from_list] *) Fixpoint hash_map_move_elements_from_list_fwd_back @@ -182,7 +182,7 @@ Fixpoint hash_map_move_elements_from_list_fwd_back | ListNil => Return ntable end end - . +. (** [hashmap::HashMap::{0}::move_elements] *) Fixpoint hash_map_move_elements_fwd_back @@ -201,13 +201,13 @@ Fixpoint hash_map_move_elements_fwd_back ntable0 <- hash_map_move_elements_from_list_fwd_back T n0 ntable ls; let l0 := mem_replace_back (List_t T) l ListNil in slots0 <- vec_index_mut_back (List_t T) slots i l0; - i1 <- usize_add i 1 %usize; + i1 <- usize_add i 1%usize; p <- hash_map_move_elements_fwd_back T n0 ntable0 slots0 i1; let (ntable1, slots1) := p in Return (ntable1, slots1)) else Return (ntable, slots) end - . +. (** [hashmap::HashMap::{0}::try_resize] *) Definition hash_map_try_resize_fwd_back @@ -219,14 +219,14 @@ Definition hash_map_try_resize_fwd_back match self with | mkHash_map_t i p i0 v => let capacity := vec_len (List_t T) v in - n1 <- usize_div max_usize 2 %usize; + n1 <- usize_div max_usize 2%usize; let (i1, i2) := p in i3 <- usize_div n1 i1; if capacity s<= i3 then ( - i4 <- usize_mul capacity 2 %usize; + i4 <- usize_mul capacity 2%usize; ntable <- hash_map_new_with_capacity_fwd T n0 i4 i1 i2; - p0 <- hash_map_move_elements_fwd_back T n0 ntable v (0 %usize); + p0 <- hash_map_move_elements_fwd_back T n0 ntable v (0%usize); let (ntable0, _) := p0 in match ntable0 with | mkHash_map_t i5 p1 i6 v0 => Return (mkHash_map_t i (i1, i2) i6 v0) @@ -234,7 +234,7 @@ Definition hash_map_try_resize_fwd_back else Return (mkHash_map_t i (i1, i2) i0 v) end end - . +. (** [hashmap::HashMap::{0}::insert] *) Definition hash_map_insert_fwd_back @@ -255,7 +255,7 @@ Definition hash_map_insert_fwd_back else Return (mkHash_map_t i0 p i1 v) end end - . +. (** [hashmap::HashMap::{0}::contains_key_in_list] *) Fixpoint hash_map_contains_key_in_list_fwd @@ -271,7 +271,7 @@ Fixpoint hash_map_contains_key_in_list_fwd | ListNil => Return false end end - . +. (** [hashmap::HashMap::{0}::contains_key] *) Definition hash_map_contains_key_fwd @@ -289,7 +289,7 @@ Definition hash_map_contains_key_fwd Return b end end - . +. (** [hashmap::HashMap::{0}::get_in_list] *) Fixpoint hash_map_get_in_list_fwd @@ -305,7 +305,7 @@ Fixpoint hash_map_get_in_list_fwd | ListNil => Fail_ Failure end end - . +. (** [hashmap::HashMap::{0}::get] *) Definition hash_map_get_fwd @@ -323,7 +323,7 @@ Definition hash_map_get_fwd Return t end end - . +. (** [hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hash_map_get_mut_in_list_fwd @@ -339,7 +339,7 @@ Fixpoint hash_map_get_mut_in_list_fwd | ListNil => Fail_ Failure end end - . +. (** [hashmap::HashMap::{0}::get_mut_in_list] *) Fixpoint hash_map_get_mut_in_list_back @@ -359,7 +359,7 @@ Fixpoint hash_map_get_mut_in_list_back | ListNil => Fail_ Failure end end - . +. (** [hashmap::HashMap::{0}::get_mut] *) Definition hash_map_get_mut_fwd @@ -377,7 +377,7 @@ Definition hash_map_get_mut_fwd Return t end end - . +. (** [hashmap::HashMap::{0}::get_mut] *) Definition hash_map_get_mut_back @@ -398,7 +398,7 @@ Definition hash_map_get_mut_back Return (mkHash_map_t i p i0 v0) end end - . +. (** [hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hash_map_remove_from_list_fwd @@ -419,7 +419,7 @@ Fixpoint hash_map_remove_from_list_fwd | ListNil => Return None end end - . +. (** [hashmap::HashMap::{0}::remove_from_list] *) Fixpoint hash_map_remove_from_list_back @@ -442,7 +442,7 @@ Fixpoint hash_map_remove_from_list_back | ListNil => Return ListNil end end - . +. (** [hashmap::HashMap::{0}::remove] *) Definition hash_map_remove_fwd @@ -461,11 +461,11 @@ Definition hash_map_remove_fwd x <- hash_map_remove_from_list_fwd T n0 key l; match x with | None => Return None - | Some x0 => i2 <- usize_sub i 1 %usize; let _ := i2 in Return (Some x0) + | Some x0 => i2 <- usize_sub i 1%usize; let _ := i2 in Return (Some x0) end end end - . +. (** [hashmap::HashMap::{0}::remove] *) Definition hash_map_remove_back @@ -488,14 +488,14 @@ Definition hash_map_remove_back v0 <- vec_index_mut_back (List_t T) v hash_mod l0; Return (mkHash_map_t i p i0 v0) | Some x0 => - i2 <- usize_sub i 1 %usize; + i2 <- usize_sub i 1%usize; l0 <- hash_map_remove_from_list_back T n0 key l; v0 <- vec_index_mut_back (List_t T) v hash_mod l0; Return (mkHash_map_t i2 p i0 v0) end end end - . +. (** [hashmap::test1] *) Definition test1_fwd (n : nat) : result unit := @@ -503,39 +503,39 @@ Definition test1_fwd (n : nat) : result unit := | O => Fail_ OutOfFuel | S n0 => hm <- hash_map_new_fwd u64 n0; - hm0 <- hash_map_insert_fwd_back u64 n0 hm (0 %usize) (42 %u64); - hm1 <- hash_map_insert_fwd_back u64 n0 hm0 (128 %usize) (18 %u64); - hm2 <- hash_map_insert_fwd_back u64 n0 hm1 (1024 %usize) (138 %u64); - hm3 <- hash_map_insert_fwd_back u64 n0 hm2 (1056 %usize) (256 %u64); - i <- hash_map_get_fwd u64 n0 hm3 (128 %usize); - if negb (i s= 18 %u64) + hm0 <- hash_map_insert_fwd_back u64 n0 hm (0%usize) (42%u64); + hm1 <- hash_map_insert_fwd_back u64 n0 hm0 (128%usize) (18%u64); + hm2 <- hash_map_insert_fwd_back u64 n0 hm1 (1024%usize) (138%u64); + hm3 <- hash_map_insert_fwd_back u64 n0 hm2 (1056%usize) (256%u64); + i <- hash_map_get_fwd u64 n0 hm3 (128%usize); + if negb (i s= 18%u64) then Fail_ Failure else ( - hm4 <- hash_map_get_mut_back u64 n0 hm3 (1024 %usize) (56 %u64); - i0 <- hash_map_get_fwd u64 n0 hm4 (1024 %usize); - if negb (i0 s= 56 %u64) + hm4 <- hash_map_get_mut_back u64 n0 hm3 (1024%usize) (56%u64); + i0 <- hash_map_get_fwd u64 n0 hm4 (1024%usize); + if negb (i0 s= 56%u64) then Fail_ Failure else ( - x <- hash_map_remove_fwd u64 n0 hm4 (1024 %usize); + x <- hash_map_remove_fwd u64 n0 hm4 (1024%usize); match x with | None => Fail_ Failure | Some x0 => - if negb (x0 s= 56 %u64) + if negb (x0 s= 56%u64) then Fail_ Failure else ( - hm5 <- hash_map_remove_back u64 n0 hm4 (1024 %usize); - i1 <- hash_map_get_fwd u64 n0 hm5 (0 %usize); - if negb (i1 s= 42 %u64) + hm5 <- hash_map_remove_back u64 n0 hm4 (1024%usize); + i1 <- hash_map_get_fwd u64 n0 hm5 (0%usize); + if negb (i1 s= 42%u64) then Fail_ Failure else ( - i2 <- hash_map_get_fwd u64 n0 hm5 (128 %usize); - if negb (i2 s= 18 %u64) + i2 <- hash_map_get_fwd u64 n0 hm5 (128%usize); + if negb (i2 s= 18%u64) then Fail_ Failure else ( - i3 <- hash_map_get_fwd u64 n0 hm5 (1056 %usize); - if negb (i3 s= 256 %u64) then Fail_ Failure else Return tt))) + i3 <- hash_map_get_fwd u64 n0 hm5 (1056%usize); + if negb (i3 s= 256%u64) then Fail_ Failure else Return tt))) end)) end - . +. End Hashmap__Funs . diff --git a/tests/coq/hashmap/Hashmap__Types.v b/tests/coq/hashmap/Hashmap__Types.v index b665179e..e1add060 100644 --- a/tests/coq/hashmap/Hashmap__Types.v +++ b/tests/coq/hashmap/Hashmap__Types.v @@ -4,7 +4,7 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Module Hashmap__Types . +Module Hashmap__Types. (** [hashmap::List] *) Inductive List_t (T : Type) := @@ -12,13 +12,12 @@ Inductive List_t (T : Type) := | ListNil : List_t T . -Arguments ListCons {T} _ _ _ . -Arguments ListNil {T} . +Arguments ListCons {T} _ _ _. +Arguments ListNil {T}. (** [hashmap::HashMap] *) Record Hash_map_t (T : Type) := -mkHash_map_t -{ +mkHash_map_t { Hash_map_num_entries : usize; Hash_map_max_load_factor : (usize * usize); Hash_map_max_load : usize; @@ -26,14 +25,14 @@ mkHash_map_t } . -Arguments mkHash_map_t {T} _ _ _ _ . -Arguments Hash_map_num_entries {T} . -Arguments Hash_map_max_load_factor {T} . -Arguments Hash_map_max_load {T} . -Arguments Hash_map_slots {T} . +Arguments mkHash_map_t {T} _ _ _ _. +Arguments Hash_map_num_entries {T}. +Arguments Hash_map_max_load_factor {T}. +Arguments Hash_map_max_load {T}. +Arguments Hash_map_slots {T}. (** [core::num::u32::{9}::MAX] *) -Definition core_num_u32_max_body : result u32 := Return (4294967295 %u32) . -Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global . +Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). +Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. End Hashmap__Types . -- cgit v1.2.3