From 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jul 2023 14:52:23 +0200 Subject: Start using namespaces in the Lean backend --- tests/coq/hashmap_on_disk/HashmapMain_Opaque.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests/coq/hashmap_on_disk') diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v index 6152b94b..e1e7fe2b 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: opaque function definitions *) +(** [hashmap_main]: external function declarations *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. -- cgit v1.2.3 From 7c95800cefc87fad894f8bf855cfc047e713b3a7 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jul 2023 12:20:28 +0200 Subject: Improve the generated comments --- tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 89 ++++++++++++++------------ tests/coq/hashmap_on_disk/HashmapMain_Opaque.v | 4 +- 2 files changed, 51 insertions(+), 42 deletions(-) (limited to 'tests/coq/hashmap_on_disk') diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 2d1bcda6..1b7304cc 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -10,11 +10,11 @@ Require Export HashmapMain_Opaque. Import HashmapMain_Opaque. Module HashmapMain_Funs. -(** [hashmap_main::hashmap::hash_key] *) +(** [hashmap_main::hashmap::hash_key]: forward function *) Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k. -(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) +(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function *) Fixpoint hashmap_hash_map_allocate_slots_loop_fwd (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) : result (vec (Hashmap_list_t T)) @@ -31,7 +31,7 @@ Fixpoint hashmap_hash_map_allocate_slots_loop_fwd end . -(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *) +(** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: forward function *) Definition hashmap_hash_map_allocate_slots_fwd (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) : result (vec (Hashmap_list_t T)) @@ -39,7 +39,7 @@ Definition hashmap_hash_map_allocate_slots_fwd hashmap_hash_map_allocate_slots_loop_fwd T n slots n0 . -(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *) +(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity]: forward function *) Definition hashmap_hash_map_new_with_capacity_fwd (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : @@ -58,13 +58,14 @@ Definition hashmap_hash_map_new_with_capacity_fwd |} . -(** [hashmap_main::hashmap::HashMap::{0}::new] *) +(** [hashmap_main::hashmap::HashMap::{0}::new]: forward function *) Definition hashmap_hash_map_new_fwd (T : Type) (n : nat) : result (Hashmap_hash_map_t T) := hashmap_hash_map_new_with_capacity_fwd T n 32%usize 4%usize 5%usize . -(** [hashmap_main::hashmap::HashMap::{0}::clear] *) +(** [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Fixpoint hashmap_hash_map_clear_loop_fwd_back (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) : result (vec (Hashmap_list_t T)) @@ -82,7 +83,8 @@ Fixpoint hashmap_hash_map_clear_loop_fwd_back end . -(** [hashmap_main::hashmap::HashMap::{0}::clear] *) +(** [hashmap_main::hashmap::HashMap::{0}::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition hashmap_hash_map_clear_fwd_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) : result (Hashmap_hash_map_t T) @@ -100,13 +102,13 @@ Definition hashmap_hash_map_clear_fwd_back |} . -(** [hashmap_main::hashmap::HashMap::{0}::len] *) +(** [hashmap_main::hashmap::HashMap::{0}::len]: forward function *) Definition hashmap_hash_map_len_fwd (T : Type) (self : Hashmap_hash_map_t T) : result usize := Return self.(Hashmap_hash_map_num_entries) . -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function *) Fixpoint hashmap_hash_map_insert_in_list_loop_fwd (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) : result bool @@ -124,7 +126,7 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_fwd end . -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: forward function *) Definition hashmap_hash_map_insert_in_list_fwd (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) : result bool @@ -132,7 +134,7 @@ Definition hashmap_hash_map_insert_in_list_fwd hashmap_hash_map_insert_in_list_loop_fwd T n key value ls . -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: backward function 0 *) Fixpoint hashmap_hash_map_insert_in_list_loop_back (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) : result (Hashmap_list_t T) @@ -153,7 +155,7 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_back end . -(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: backward function 0 *) Definition hashmap_hash_map_insert_in_list_back (T : Type) (n : nat) (key : usize) (value : T) (ls : Hashmap_list_t T) : result (Hashmap_list_t T) @@ -161,7 +163,8 @@ Definition hashmap_hash_map_insert_in_list_back hashmap_hash_map_insert_in_list_loop_back T n key value ls . -(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize] *) +(** [hashmap_main::hashmap::HashMap::{0}::insert_no_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition hashmap_hash_map_insert_no_resize_fwd_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T) : @@ -207,7 +210,8 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back 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_main::hashmap::HashMap::{0}::move_elements_from_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) : @@ -225,7 +229,8 @@ Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back end . -(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition hashmap_hash_map_move_elements_from_list_fwd_back (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) : @@ -234,7 +239,8 @@ Definition hashmap_hash_map_move_elements_from_list_fwd_back hashmap_hash_map_move_elements_from_list_loop_fwd_back T n ntable ls . -(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) +(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Fixpoint hashmap_hash_map_move_elements_loop_fwd_back (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (slots : vec (Hashmap_list_t T)) (i : usize) : @@ -258,7 +264,8 @@ Fixpoint hashmap_hash_map_move_elements_loop_fwd_back end . -(** [hashmap_main::hashmap::HashMap::{0}::move_elements] *) +(** [hashmap_main::hashmap::HashMap::{0}::move_elements]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition hashmap_hash_map_move_elements_fwd_back (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (slots : vec (Hashmap_list_t T)) (i : usize) : @@ -267,7 +274,8 @@ Definition hashmap_hash_map_move_elements_fwd_back hashmap_hash_map_move_elements_loop_fwd_back T n ntable slots i . -(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) +(** [hashmap_main::hashmap::HashMap::{0}::try_resize]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition hashmap_hash_map_try_resize_fwd_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) : result (Hashmap_hash_map_t T) @@ -302,7 +310,8 @@ Definition hashmap_hash_map_try_resize_fwd_back |} . -(** [hashmap_main::hashmap::HashMap::{0}::insert] *) +(** [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition hashmap_hash_map_insert_fwd_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (value : T) : @@ -315,7 +324,7 @@ Definition hashmap_hash_map_insert_fwd_back else Return self0 . -(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: loop 0: forward function *) Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool := match n with @@ -331,13 +340,13 @@ Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd end . -(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: forward function *) Definition hashmap_hash_map_contains_key_in_list_fwd (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool := hashmap_hash_map_contains_key_in_list_loop_fwd T n key ls . -(** [hashmap_main::hashmap::HashMap::{0}::contains_key] *) +(** [hashmap_main::hashmap::HashMap::{0}::contains_key]: forward function *) Definition hashmap_hash_map_contains_key_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result bool @@ -349,7 +358,7 @@ Definition hashmap_hash_map_contains_key_fwd hashmap_hash_map_contains_key_in_list_fwd T n key l . -(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function *) Fixpoint hashmap_hash_map_get_in_list_loop_fwd (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T := match n with @@ -365,13 +374,13 @@ Fixpoint hashmap_hash_map_get_in_list_loop_fwd end . -(** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: forward function *) Definition hashmap_hash_map_get_in_list_fwd (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T := hashmap_hash_map_get_in_list_loop_fwd T n key ls . -(** [hashmap_main::hashmap::HashMap::{0}::get] *) +(** [hashmap_main::hashmap::HashMap::{0}::get]: forward function *) Definition hashmap_hash_map_get_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result T @@ -383,7 +392,7 @@ Definition hashmap_hash_map_get_fwd hashmap_hash_map_get_in_list_fwd T n key l . -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function *) Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T := match n with @@ -399,13 +408,13 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd end . -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: forward function *) Definition hashmap_hash_map_get_mut_in_list_fwd (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) : result T := hashmap_hash_map_get_mut_in_list_loop_fwd T n ls key . -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: backward function 0 *) Fixpoint hashmap_hash_map_get_mut_in_list_loop_back (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) : result (Hashmap_list_t T) @@ -425,7 +434,7 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back end . -(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: backward function 0 *) Definition hashmap_hash_map_get_mut_in_list_back (T : Type) (n : nat) (ls : Hashmap_list_t T) (key : usize) (ret : T) : result (Hashmap_list_t T) @@ -433,7 +442,7 @@ Definition hashmap_hash_map_get_mut_in_list_back hashmap_hash_map_get_mut_in_list_loop_back T n ls key ret . -(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) +(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: forward function *) Definition hashmap_hash_map_get_mut_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result T @@ -446,7 +455,7 @@ Definition hashmap_hash_map_get_mut_fwd hashmap_hash_map_get_mut_in_list_fwd T n l key . -(** [hashmap_main::hashmap::HashMap::{0}::get_mut] *) +(** [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 *) Definition hashmap_hash_map_get_mut_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) (ret : T) : result (Hashmap_hash_map_t T) @@ -470,7 +479,7 @@ Definition hashmap_hash_map_get_mut_back |} . -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function *) Fixpoint hashmap_hash_map_remove_from_list_loop_fwd (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result (option T) @@ -495,7 +504,7 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_fwd end . -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: forward function *) Definition hashmap_hash_map_remove_from_list_fwd (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result (option T) @@ -503,7 +512,7 @@ Definition hashmap_hash_map_remove_from_list_fwd hashmap_hash_map_remove_from_list_loop_fwd T n key ls . -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: backward function 1 *) Fixpoint hashmap_hash_map_remove_from_list_loop_back (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result (Hashmap_list_t T) @@ -530,7 +539,7 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back end . -(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *) +(** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: backward function 1 *) Definition hashmap_hash_map_remove_from_list_back (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result (Hashmap_list_t T) @@ -538,7 +547,7 @@ Definition hashmap_hash_map_remove_from_list_back hashmap_hash_map_remove_from_list_loop_back T n key ls . -(** [hashmap_main::hashmap::HashMap::{0}::remove] *) +(** [hashmap_main::hashmap::HashMap::{0}::remove]: forward function *) Definition hashmap_hash_map_remove_fwd (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result (option T) @@ -557,7 +566,7 @@ Definition hashmap_hash_map_remove_fwd end . -(** [hashmap_main::hashmap::HashMap::{0}::remove] *) +(** [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 *) Definition hashmap_hash_map_remove_back (T : Type) (n : nat) (self : Hashmap_hash_map_t T) (key : usize) : result (Hashmap_hash_map_t T) @@ -599,7 +608,7 @@ Definition hashmap_hash_map_remove_back end . -(** [hashmap_main::hashmap::test1] *) +(** [hashmap_main::hashmap::test1]: forward function *) Definition hashmap_test1_fwd (n : nat) : result unit := hm <- hashmap_hash_map_new_fwd u64 n; hm0 <- hashmap_hash_map_insert_fwd_back u64 n hm 0%usize 42%u64; @@ -636,7 +645,7 @@ Definition hashmap_test1_fwd (n : nat) : result unit := end)) . -(** [hashmap_main::insert_on_disk] *) +(** [hashmap_main::insert_on_disk]: forward function *) Definition insert_on_disk_fwd (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) := p <- hashmap_utils_deserialize_fwd st; @@ -647,7 +656,7 @@ Definition insert_on_disk_fwd Return (st1, tt) . -(** [hashmap_main::main] *) +(** [hashmap_main::main]: forward function *) Definition main_fwd : result unit := Return tt. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v index e1e7fe2b..1ad9c697 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v @@ -8,12 +8,12 @@ Require Export HashmapMain_Types. Import HashmapMain_Types. Module HashmapMain_Opaque. -(** [hashmap_main::hashmap_utils::deserialize] *) +(** [hashmap_main::hashmap_utils::deserialize]: forward function *) Axiom hashmap_utils_deserialize_fwd : state -> result (state * (Hashmap_hash_map_t u64)) . -(** [hashmap_main::hashmap_utils::serialize] *) +(** [hashmap_main::hashmap_utils::serialize]: forward function *) Axiom hashmap_utils_serialize_fwd : Hashmap_hash_map_t u64 -> state -> result (state * unit) . -- cgit v1.2.3