diff options
Diffstat (limited to 'tests/hol4')
| -rw-r--r-- | tests/hol4/betree/betreeMain_OpaqueScript.sml | 26 | ||||
| -rw-r--r-- | tests/hol4/betree/betreeMain_OpaqueTheory.sig | 11 | ||||
| -rw-r--r-- | tests/hol4/betree/betree_FunsScript.sml (renamed from tests/hol4/betree/betreeMain_FunsScript.sml) | 120 | ||||
| -rw-r--r-- | tests/hol4/betree/betree_FunsTheory.sig (renamed from tests/hol4/betree/betreeMain_FunsTheory.sig) | 6 | ||||
| -rw-r--r-- | tests/hol4/betree/betree_OpaqueScript.sml | 26 | ||||
| -rw-r--r-- | tests/hol4/betree/betree_OpaqueTheory.sig | 11 | ||||
| -rw-r--r-- | tests/hol4/betree/betree_TypesScript.sml (renamed from tests/hol4/betree/betreeMain_TypesScript.sml) | 22 | ||||
| -rw-r--r-- | tests/hol4/betree/betree_TypesTheory.sig (renamed from tests/hol4/betree/betreeMain_TypesTheory.sig) | 6 |
8 files changed, 114 insertions, 114 deletions
diff --git a/tests/hol4/betree/betreeMain_OpaqueScript.sml b/tests/hol4/betree/betreeMain_OpaqueScript.sml deleted file mode 100644 index 1d16db4c..00000000 --- a/tests/hol4/betree/betreeMain_OpaqueScript.sml +++ /dev/null @@ -1,26 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external function declarations *) -open primitivesLib divDefLib -open betreeMain_TypesTheory - -val _ = new_theory "betreeMain_Opaque" - - -(** [betree_main::betree_utils::load_internal_node]: forward function *)val _ = new_constant ("betree_utils_load_internal_node_fwd", - “:u64 -> state -> (state # (u64 # betree_message_t) betree_list_t) - result”) - -(** [betree_main::betree_utils::store_internal_node]: forward function *)val _ = new_constant ("betree_utils_store_internal_node_fwd", - “:u64 -> (u64 # betree_message_t) betree_list_t -> state -> (state # unit) - result”) - -(** [betree_main::betree_utils::load_leaf_node]: forward function *)val _ = new_constant ("betree_utils_load_leaf_node_fwd", - “:u64 -> state -> (state # (u64 # u64) betree_list_t) result”) - -(** [betree_main::betree_utils::store_leaf_node]: forward function *)val _ = new_constant ("betree_utils_store_leaf_node_fwd", - “:u64 -> (u64 # u64) betree_list_t -> state -> (state # unit) result”) - -(** [core::option::Option::{0}::unwrap]: forward function *)val _ = new_constant ("core_option_option_unwrap_fwd", - “:'t option -> state -> (state # 't) result”) - -val _ = export_theory () diff --git a/tests/hol4/betree/betreeMain_OpaqueTheory.sig b/tests/hol4/betree/betreeMain_OpaqueTheory.sig deleted file mode 100644 index da7559a0..00000000 --- a/tests/hol4/betree/betreeMain_OpaqueTheory.sig +++ /dev/null @@ -1,11 +0,0 @@ -signature betreeMain_OpaqueTheory = -sig - type thm = Thm.thm - - val betreeMain_Opaque_grammars : type_grammar.grammar * term_grammar.grammar -(* - [betreeMain_Types] Parent theory of "betreeMain_Opaque" - - -*) -end diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betree_FunsScript.sml index bd16c16c..49bcb446 100644 --- a/tests/hol4/betree/betreeMain_FunsScript.sml +++ b/tests/hol4/betree/betree_FunsScript.sml @@ -1,13 +1,13 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) +(** [betree]: function definitions *) open primitivesLib divDefLib -open betreeMain_TypesTheory betreeMain_OpaqueTheory +open betree_TypesTheory betree_OpaqueTheory -val _ = new_theory "betreeMain_Funs" +val _ = new_theory "betree_Funs" val betree_load_internal_node_fwd_def = Define ‘ - (** [betree_main::betree::load_internal_node]: forward function *) + (** [betree::betree::load_internal_node]: forward function *) betree_load_internal_node_fwd (id : u64) (st : state) : (state # (u64 # betree_message_t) betree_list_t) result @@ -16,7 +16,7 @@ val betree_load_internal_node_fwd_def = Define ‘ ’ val betree_store_internal_node_fwd_def = Define ‘ - (** [betree_main::betree::store_internal_node]: forward function *) + (** [betree::betree::store_internal_node]: forward function *) betree_store_internal_node_fwd (id : u64) (content : (u64 # betree_message_t) betree_list_t) (st : state) : @@ -29,14 +29,14 @@ val betree_store_internal_node_fwd_def = Define ‘ ’ val betree_load_leaf_node_fwd_def = Define ‘ - (** [betree_main::betree::load_leaf_node]: forward function *) + (** [betree::betree::load_leaf_node]: forward function *) betree_load_leaf_node_fwd (id : u64) (st : state) : (state # (u64 # u64) betree_list_t) result = betree_utils_load_leaf_node_fwd id st ’ val betree_store_leaf_node_fwd_def = Define ‘ - (** [betree_main::betree::store_leaf_node]: forward function *) + (** [betree::betree::store_leaf_node]: forward function *) betree_store_leaf_node_fwd (id : u64) (content : (u64 # u64) betree_list_t) (st : state) : (state # unit) result @@ -48,7 +48,7 @@ val betree_store_leaf_node_fwd_def = Define ‘ ’ val betree_fresh_node_id_fwd_def = Define ‘ - (** [betree_main::betree::fresh_node_id]: forward function *) + (** [betree::betree::fresh_node_id]: forward function *) betree_fresh_node_id_fwd (counter : u64) : u64 result = do _ <- u64_add counter (int_to_u64 1); @@ -57,19 +57,19 @@ val betree_fresh_node_id_fwd_def = Define ‘ ’ val betree_fresh_node_id_back_def = Define ‘ - (** [betree_main::betree::fresh_node_id]: backward function 0 *) + (** [betree::betree::fresh_node_id]: backward function 0 *) betree_fresh_node_id_back (counter : u64) : u64 result = u64_add counter (int_to_u64 1) ’ val betree_node_id_counter_new_fwd_def = Define ‘ - (** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *) + (** [betree::betree::NodeIdCounter::{0}::new]: forward function *) betree_node_id_counter_new_fwd : betree_node_id_counter_t result = Return (<| betree_node_id_counter_next_node_id := (int_to_u64 0) |>) ’ val betree_node_id_counter_fresh_id_fwd_def = Define ‘ - (** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *) + (** [betree::betree::NodeIdCounter::{0}::fresh_id]: forward function *) betree_node_id_counter_fresh_id_fwd (self : betree_node_id_counter_t) : u64 result = do @@ -79,7 +79,7 @@ val betree_node_id_counter_fresh_id_fwd_def = Define ‘ ’ val betree_node_id_counter_fresh_id_back_def = Define ‘ - (** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *) + (** [betree::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *) betree_node_id_counter_fresh_id_back (self : betree_node_id_counter_t) : betree_node_id_counter_t result = do @@ -89,7 +89,7 @@ val betree_node_id_counter_fresh_id_back_def = Define ‘ ’ val betree_upsert_update_fwd_def = Define ‘ - (** [betree_main::betree::upsert_update]: forward function *) + (** [betree::betree::upsert_update]: forward function *) betree_upsert_update_fwd (prev : u64 option) (st : betree_upsert_fun_state_t) : u64 result = (case prev of @@ -109,7 +109,7 @@ val betree_upsert_update_fwd_def = Define ‘ ’ val [betree_list_len_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::List::{1}::len]: forward function *) + (** [betree::betree::List::{1}::len]: forward function *) betree_list_len_fwd (self : 't betree_list_t) : u64 result = (case self of | BetreeListCons t tl => @@ -121,7 +121,7 @@ val [betree_list_len_fwd_def] = DefineDiv ‘ ’ val [betree_list_split_at_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::List::{1}::split_at]: forward function *) + (** [betree::betree::List::{1}::split_at]: forward function *) betree_list_split_at_fwd (self : 't betree_list_t) (n : u64) : ('t betree_list_t # 't betree_list_t) result @@ -140,7 +140,7 @@ val [betree_list_split_at_fwd_def] = DefineDiv ‘ ’ val betree_list_push_front_fwd_back_def = Define ‘ - (** [betree_main::betree::List::{1}::push_front]: merged forward/backward function + (** [betree::betree::List::{1}::push_front]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) betree_list_push_front_fwd_back (self : 't betree_list_t) (x : 't) : 't betree_list_t result = @@ -150,7 +150,7 @@ val betree_list_push_front_fwd_back_def = Define ‘ ’ val betree_list_pop_front_fwd_def = Define ‘ - (** [betree_main::betree::List::{1}::pop_front]: forward function *) + (** [betree::betree::List::{1}::pop_front]: forward function *) betree_list_pop_front_fwd (self : 't betree_list_t) : 't result = let ls = mem_replace_fwd self BetreeListNil in (case ls of @@ -159,7 +159,7 @@ val betree_list_pop_front_fwd_def = Define ‘ ’ val betree_list_pop_front_back_def = Define ‘ - (** [betree_main::betree::List::{1}::pop_front]: backward function 0 *) + (** [betree::betree::List::{1}::pop_front]: backward function 0 *) betree_list_pop_front_back (self : 't betree_list_t) : 't betree_list_t result = let ls = mem_replace_fwd self BetreeListNil in @@ -169,7 +169,7 @@ val betree_list_pop_front_back_def = Define ‘ ’ val betree_list_hd_fwd_def = Define ‘ - (** [betree_main::betree::List::{1}::hd]: forward function *) + (** [betree::betree::List::{1}::hd]: forward function *) betree_list_hd_fwd (self : 't betree_list_t) : 't result = (case self of | BetreeListCons hd l => Return hd @@ -177,7 +177,7 @@ val betree_list_hd_fwd_def = Define ‘ ’ val betree_list_head_has_key_fwd_def = Define ‘ - (** [betree_main::betree::List::{2}::head_has_key]: forward function *) + (** [betree::betree::List::{2}::head_has_key]: forward function *) betree_list_head_has_key_fwd (self : (u64 # 't) betree_list_t) (key : u64) : bool result = (case self of @@ -186,7 +186,7 @@ val betree_list_head_has_key_fwd_def = Define ‘ ’ val [betree_list_partition_at_pivot_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *) + (** [betree::betree::List::{2}::partition_at_pivot]: forward function *) betree_list_partition_at_pivot_fwd (self : (u64 # 't) betree_list_t) (pivot : u64) : ((u64 # 't) betree_list_t # (u64 # 't) betree_list_t) result @@ -207,7 +207,7 @@ val [betree_list_partition_at_pivot_fwd_def] = DefineDiv ‘ ’ val betree_leaf_split_fwd_def = Define ‘ - (** [betree_main::betree::Leaf::{3}::split]: forward function *) + (** [betree::betree::Leaf::{3}::split]: forward function *) betree_leaf_split_fwd (self : betree_leaf_t) (content : (u64 # u64) betree_list_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -249,7 +249,7 @@ val betree_leaf_split_fwd_def = Define ‘ ’ val betree_leaf_split_back_def = Define ‘ - (** [betree_main::betree::Leaf::{3}::split]: backward function 2 *) + (** [betree::betree::Leaf::{3}::split]: backward function 2 *) betree_leaf_split_back (self : betree_leaf_t) (content : (u64 # u64) betree_list_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -272,7 +272,7 @@ val betree_leaf_split_back_def = Define ‘ ’ val [betree_node_lookup_first_message_for_key_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *) + (** [betree::betree::Node::{5}::lookup_first_message_for_key]: forward function *) betree_node_lookup_first_message_for_key_fwd (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) : (u64 # betree_message_t) betree_list_t result @@ -287,7 +287,7 @@ val [betree_node_lookup_first_message_for_key_fwd_def] = DefineDiv ‘ ’ val [betree_node_lookup_first_message_for_key_back_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *) + (** [betree::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *) betree_node_lookup_first_message_for_key_back (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) (ret : (u64 # betree_message_t) betree_list_t) : @@ -308,7 +308,7 @@ val [betree_node_lookup_first_message_for_key_back_def] = DefineDiv ‘ ’ val [betree_node_apply_upserts_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::apply_upserts]: forward function *) + (** [betree::betree::Node::{5}::apply_upserts]: forward function *) betree_node_apply_upserts_fwd (msgs : (u64 # betree_message_t) betree_list_t) (prev : u64 option) (key : u64) (st : state) : @@ -341,7 +341,7 @@ val [betree_node_apply_upserts_fwd_def] = DefineDiv ‘ ’ val [betree_node_apply_upserts_back_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *) + (** [betree::betree::Node::{5}::apply_upserts]: backward function 0 *) betree_node_apply_upserts_back (msgs : (u64 # betree_message_t) betree_list_t) (prev : u64 option) (key : u64) (st : state) : @@ -373,7 +373,7 @@ val [betree_node_apply_upserts_back_def] = DefineDiv ‘ ’ val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *) + (** [betree::betree::Node::{5}::lookup_in_bindings]: forward function *) betree_node_lookup_in_bindings_fwd (key : u64) (bindings : (u64 # u64) betree_list_t) : u64 option result = (case bindings of @@ -389,7 +389,7 @@ val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘ ’ val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_children_back_def, betree_node_lookup_fwd_def, betree_node_lookup_back_def] = DefineDiv ‘ - (** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *) + (** [betree::betree::Internal::{4}::lookup_in_children]: forward function *) (betree_internal_lookup_in_children_fwd (self : betree_internal_t) (key : u64) (st : state) : (state # u64 option) result @@ -399,7 +399,7 @@ val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_child else betree_node_lookup_fwd self.betree_internal_right key st) /\ - (** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *) + (** [betree::betree::Internal::{4}::lookup_in_children]: backward function 0 *) (betree_internal_lookup_in_children_back (self : betree_internal_t) (key : u64) (st : state) : betree_internal_t result @@ -417,7 +417,7 @@ val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_child od)) /\ - (** [betree_main::betree::Node::{5}::lookup]: forward function *) + (** [betree::betree::Node::{5}::lookup]: forward function *) (betree_node_lookup_fwd (self : betree_node_t) (key : u64) (st : state) : (state # u64 option) result @@ -487,7 +487,7 @@ val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_child od)) /\ - (** [betree_main::betree::Node::{5}::lookup]: backward function 0 *) + (** [betree::betree::Node::{5}::lookup]: backward function 0 *) betree_node_lookup_back (self : betree_node_t) (key : u64) (st : state) : betree_node_t result = (case self of @@ -556,7 +556,7 @@ val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_child ’ val [betree_node_filter_messages_for_key_fwd_back_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function + (** [betree::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) betree_node_filter_messages_for_key_fwd_back (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) : @@ -576,7 +576,7 @@ val [betree_node_filter_messages_for_key_fwd_back_def] = DefineDiv ‘ ’ val [betree_node_lookup_first_message_after_key_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *) + (** [betree::betree::Node::{5}::lookup_first_message_after_key]: forward function *) betree_node_lookup_first_message_after_key_fwd (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) : (u64 # betree_message_t) betree_list_t result @@ -591,7 +591,7 @@ val [betree_node_lookup_first_message_after_key_fwd_def] = DefineDiv ‘ ’ val [betree_node_lookup_first_message_after_key_back_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *) + (** [betree::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *) betree_node_lookup_first_message_after_key_back (key : u64) (msgs : (u64 # betree_message_t) betree_list_t) (ret : (u64 # betree_message_t) betree_list_t) : @@ -612,7 +612,7 @@ val [betree_node_lookup_first_message_after_key_back_def] = DefineDiv ‘ ’ val betree_node_apply_to_internal_fwd_back_def = Define ‘ - (** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function + (** [betree::betree::Node::{5}::apply_to_internal]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) betree_node_apply_to_internal_fwd_back (msgs : (u64 # betree_message_t) betree_list_t) (key : u64) @@ -679,7 +679,7 @@ val betree_node_apply_to_internal_fwd_back_def = Define ‘ ’ val [betree_node_apply_messages_to_internal_fwd_back_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function + (** [betree::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) betree_node_apply_messages_to_internal_fwd_back (msgs : (u64 # betree_message_t) betree_list_t) @@ -697,7 +697,7 @@ val [betree_node_apply_messages_to_internal_fwd_back_def] = DefineDiv ‘ ’ val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *) + (** [betree::betree::Node::{5}::lookup_mut_in_bindings]: forward function *) betree_node_lookup_mut_in_bindings_fwd (key : u64) (bindings : (u64 # u64) betree_list_t) : (u64 # u64) betree_list_t result @@ -712,7 +712,7 @@ val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘ ’ val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *) + (** [betree::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *) betree_node_lookup_mut_in_bindings_back (key : u64) (bindings : (u64 # u64) betree_list_t) (ret : (u64 # u64) betree_list_t) : @@ -732,7 +732,7 @@ val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘ ’ val betree_node_apply_to_leaf_fwd_back_def = Define ‘ - (** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function + (** [betree::betree::Node::{5}::apply_to_leaf]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) betree_node_apply_to_leaf_fwd_back (bindings : (u64 # u64) betree_list_t) (key : u64) @@ -786,7 +786,7 @@ val betree_node_apply_to_leaf_fwd_back_def = Define ‘ ’ val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘ - (** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function + (** [betree::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) betree_node_apply_messages_to_leaf_fwd_back (bindings : (u64 # u64) betree_list_t) @@ -804,7 +804,7 @@ val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘ ’ val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def] = DefineDiv ‘ - (** [betree_main::betree::Internal::{4}::flush]: forward function *) + (** [betree::betree::Internal::{4}::flush]: forward function *) (betree_internal_flush_fwd (self : betree_internal_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -853,7 +853,7 @@ val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_ od) /\ - (** [betree_main::betree::Internal::{4}::flush]: backward function 0 *) + (** [betree::betree::Internal::{4}::flush]: backward function 0 *) (betree_internal_flush_back (self : betree_internal_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -901,7 +901,7 @@ val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_ od) /\ - (** [betree_main::betree::Node::{5}::apply_messages]: forward function *) + (** [betree::betree::Node::{5}::apply_messages]: forward function *) (betree_node_apply_messages_fwd (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -956,7 +956,7 @@ val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_ od)) /\ - (** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *) + (** [betree::betree::Node::{5}::apply_messages]: backward function 0 *) betree_node_apply_messages_back (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) @@ -1014,7 +1014,7 @@ val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_ ’ val betree_node_apply_fwd_def = Define ‘ - (** [betree_main::betree::Node::{5}::apply]: forward function *) + (** [betree::betree::Node::{5}::apply]: forward function *) betree_node_apply_fwd (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) (key : u64) @@ -1034,7 +1034,7 @@ val betree_node_apply_fwd_def = Define ‘ ’ val betree_node_apply_back_def = Define ‘ - (** [betree_main::betree::Node::{5}::apply]: backward function 0 *) + (** [betree::betree::Node::{5}::apply]: backward function 0 *) betree_node_apply_back (self : betree_node_t) (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t) (key : u64) @@ -1047,7 +1047,7 @@ val betree_node_apply_back_def = Define ‘ ’ val betree_be_tree_new_fwd_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::new]: forward function *) + (** [betree::betree::BeTree::{6}::new]: forward function *) betree_be_tree_new_fwd (min_flush_size : u64) (split_size : u64) (st : state) : (state # betree_be_tree_t) result @@ -1073,7 +1073,7 @@ val betree_be_tree_new_fwd_def = Define ‘ ’ val betree_be_tree_apply_fwd_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::apply]: forward function *) + (** [betree::betree::BeTree::{6}::apply]: forward function *) betree_be_tree_apply_fwd (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) : @@ -1091,7 +1091,7 @@ val betree_be_tree_apply_fwd_def = Define ‘ ’ val betree_be_tree_apply_back_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *) + (** [betree::betree::BeTree::{6}::apply]: backward function 0 *) betree_be_tree_apply_back (self : betree_be_tree_t) (key : u64) (msg : betree_message_t) (st : state) : @@ -1111,7 +1111,7 @@ val betree_be_tree_apply_back_def = Define ‘ ’ val betree_be_tree_insert_fwd_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::insert]: forward function *) + (** [betree::betree::BeTree::{6}::insert]: forward function *) betree_be_tree_insert_fwd (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) : (state # unit) result @@ -1125,7 +1125,7 @@ val betree_be_tree_insert_fwd_def = Define ‘ ’ val betree_be_tree_insert_back_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *) + (** [betree::betree::BeTree::{6}::insert]: backward function 0 *) betree_be_tree_insert_back (self : betree_be_tree_t) (key : u64) (value : u64) (st : state) : betree_be_tree_t result @@ -1134,7 +1134,7 @@ val betree_be_tree_insert_back_def = Define ‘ ’ val betree_be_tree_delete_fwd_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::delete]: forward function *) + (** [betree::betree::BeTree::{6}::delete]: forward function *) betree_be_tree_delete_fwd (self : betree_be_tree_t) (key : u64) (st : state) : (state # unit) result @@ -1147,7 +1147,7 @@ val betree_be_tree_delete_fwd_def = Define ‘ ’ val betree_be_tree_delete_back_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *) + (** [betree::betree::BeTree::{6}::delete]: backward function 0 *) betree_be_tree_delete_back (self : betree_be_tree_t) (key : u64) (st : state) : betree_be_tree_t result @@ -1156,7 +1156,7 @@ val betree_be_tree_delete_back_def = Define ‘ ’ val betree_be_tree_upsert_fwd_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::upsert]: forward function *) + (** [betree::betree::BeTree::{6}::upsert]: forward function *) betree_be_tree_upsert_fwd (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t) (st : state) : @@ -1170,7 +1170,7 @@ val betree_be_tree_upsert_fwd_def = Define ‘ ’ val betree_be_tree_upsert_back_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *) + (** [betree::betree::BeTree::{6}::upsert]: backward function 0 *) betree_be_tree_upsert_back (self : betree_be_tree_t) (key : u64) (upd : betree_upsert_fun_state_t) (st : state) : @@ -1180,7 +1180,7 @@ val betree_be_tree_upsert_back_def = Define ‘ ’ val betree_be_tree_lookup_fwd_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::lookup]: forward function *) + (** [betree::betree::BeTree::{6}::lookup]: forward function *) betree_be_tree_lookup_fwd (self : betree_be_tree_t) (key : u64) (st : state) : (state # u64 option) result @@ -1189,7 +1189,7 @@ val betree_be_tree_lookup_fwd_def = Define ‘ ’ val betree_be_tree_lookup_back_def = Define ‘ - (** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *) + (** [betree::betree::BeTree::{6}::lookup]: backward function 0 *) betree_be_tree_lookup_back (self : betree_be_tree_t) (key : u64) (st : state) : betree_be_tree_t result @@ -1201,12 +1201,12 @@ val betree_be_tree_lookup_back_def = Define ‘ ’ val main_fwd_def = Define ‘ - (** [betree_main::main]: forward function *) + (** [betree::main]: forward function *) main_fwd : unit result = Return () ’ -(** Unit test for [betree_main::main] *) +(** Unit test for [betree::main] *) val _ = assert_return (“main_fwd”) val _ = export_theory () diff --git a/tests/hol4/betree/betreeMain_FunsTheory.sig b/tests/hol4/betree/betree_FunsTheory.sig index c922ca9f..4127cba1 100644 --- a/tests/hol4/betree/betreeMain_FunsTheory.sig +++ b/tests/hol4/betree/betree_FunsTheory.sig @@ -1,4 +1,4 @@ -signature betreeMain_FunsTheory = +signature betree_FunsTheory = sig type thm = Thm.thm @@ -60,9 +60,9 @@ sig val betree_upsert_update_fwd_def : thm val main_fwd_def : thm - val betreeMain_Funs_grammars : type_grammar.grammar * term_grammar.grammar + val betree_Funs_grammars : type_grammar.grammar * term_grammar.grammar (* - [betreeMain_Opaque] Parent theory of "betreeMain_Funs" + [betree_Opaque] Parent theory of "betree_Funs" [betree_be_tree_apply_back_def] Definition diff --git a/tests/hol4/betree/betree_OpaqueScript.sml b/tests/hol4/betree/betree_OpaqueScript.sml new file mode 100644 index 00000000..d8fdf6b5 --- /dev/null +++ b/tests/hol4/betree/betree_OpaqueScript.sml @@ -0,0 +1,26 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree]: external function declarations *) +open primitivesLib divDefLib +open betree_TypesTheory + +val _ = new_theory "betree_Opaque" + + +(** [betree::betree_utils::load_internal_node]: forward function *)val _ = new_constant ("betree_utils_load_internal_node_fwd", + “:u64 -> state -> (state # (u64 # betree_message_t) betree_list_t) + result”) + +(** [betree::betree_utils::store_internal_node]: forward function *)val _ = new_constant ("betree_utils_store_internal_node_fwd", + “:u64 -> (u64 # betree_message_t) betree_list_t -> state -> (state # unit) + result”) + +(** [betree::betree_utils::load_leaf_node]: forward function *)val _ = new_constant ("betree_utils_load_leaf_node_fwd", + “:u64 -> state -> (state # (u64 # u64) betree_list_t) result”) + +(** [betree::betree_utils::store_leaf_node]: forward function *)val _ = new_constant ("betree_utils_store_leaf_node_fwd", + “:u64 -> (u64 # u64) betree_list_t -> state -> (state # unit) result”) + +(** [core::option::Option::{0}::unwrap]: forward function *)val _ = new_constant ("core_option_option_unwrap_fwd", + “:'t option -> state -> (state # 't) result”) + +val _ = export_theory () diff --git a/tests/hol4/betree/betree_OpaqueTheory.sig b/tests/hol4/betree/betree_OpaqueTheory.sig new file mode 100644 index 00000000..9452ff0f --- /dev/null +++ b/tests/hol4/betree/betree_OpaqueTheory.sig @@ -0,0 +1,11 @@ +signature betree_OpaqueTheory = +sig + type thm = Thm.thm + + val betree_Opaque_grammars : type_grammar.grammar * term_grammar.grammar +(* + [betree_Types] Parent theory of "betree_Opaque" + + +*) +end diff --git a/tests/hol4/betree/betreeMain_TypesScript.sml b/tests/hol4/betree/betree_TypesScript.sml index 779f6abb..93be2f46 100644 --- a/tests/hol4/betree/betreeMain_TypesScript.sml +++ b/tests/hol4/betree/betree_TypesScript.sml @@ -1,24 +1,24 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: type definitions *) +(** [betree]: type definitions *) open primitivesLib divDefLib -val _ = new_theory "betreeMain_Types" +val _ = new_theory "betree_Types" Datatype: - (** [betree_main::betree::List] *) + (** [betree::betree::List] *) betree_list_t = | BetreeListCons 't betree_list_t | BetreeListNil End Datatype: - (** [betree_main::betree::UpsertFunState] *) + (** [betree::betree::UpsertFunState] *) betree_upsert_fun_state_t = | BetreeUpsertFunStateAdd u64 | BetreeUpsertFunStateSub u64 End Datatype: - (** [betree_main::betree::Message] *) + (** [betree::betree::Message] *) betree_message_t = | BetreeMessageInsert u64 | BetreeMessageDelete @@ -26,12 +26,12 @@ Datatype: End Datatype: - (** [betree_main::betree::Leaf] *) + (** [betree::betree::Leaf] *) betree_leaf_t = <| betree_leaf_id : u64; betree_leaf_size : u64; |> End Datatype: - (** [betree_main::betree::Internal] *) + (** [betree::betree::Internal] *) betree_internal_t = <| betree_internal_id : u64; @@ -41,14 +41,14 @@ Datatype: |> ; - (** [betree_main::betree::Node] *) + (** [betree::betree::Node] *) betree_node_t = | BetreeNodeInternal betree_internal_t | BetreeNodeLeaf betree_leaf_t End Datatype: - (** [betree_main::betree::Params] *) + (** [betree::betree::Params] *) betree_params_t = <| betree_params_min_flush_size : u64; betree_params_split_size : u64; @@ -56,12 +56,12 @@ Datatype: End Datatype: - (** [betree_main::betree::NodeIdCounter] *) + (** [betree::betree::NodeIdCounter] *) betree_node_id_counter_t = <| betree_node_id_counter_next_node_id : u64; |> End Datatype: - (** [betree_main::betree::BeTree] *) + (** [betree::betree::BeTree] *) betree_be_tree_t = <| betree_be_tree_params : betree_params_t; diff --git a/tests/hol4/betree/betreeMain_TypesTheory.sig b/tests/hol4/betree/betree_TypesTheory.sig index cffe6afb..ee2ec4b5 100644 --- a/tests/hol4/betree/betreeMain_TypesTheory.sig +++ b/tests/hol4/betree/betree_TypesTheory.sig @@ -1,4 +1,4 @@ -signature betreeMain_TypesTheory = +signature betree_TypesTheory = sig type thm = Thm.thm @@ -185,9 +185,9 @@ sig val datatype_betree_params_t : thm val datatype_betree_upsert_fun_state_t : thm - val betreeMain_Types_grammars : type_grammar.grammar * term_grammar.grammar + val betree_Types_grammars : type_grammar.grammar * term_grammar.grammar (* - [divDef] Parent theory of "betreeMain_Types" + [divDef] Parent theory of "betree_Types" [betree_be_tree_t_TY_DEF] Definition |