diff options
| -rw-r--r-- | flake.nix | 4 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_Funs.v (renamed from tests/coq/betree/BetreeMain_Funs.v) | 92 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_FunsExternal.v (renamed from tests/coq/betree/BetreeMain_FunsExternal.v) | 8 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_FunsExternal_Template.v (renamed from tests/coq/betree/BetreeMain_FunsExternal_Template.v) | 18 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_Types.v (renamed from tests/coq/betree/BetreeMain_Types.v) | 28 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_TypesExternal.v (renamed from tests/coq/betree/BetreeMain_TypesExternal.v) | 4 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_TypesExternal_Template.v (renamed from tests/coq/betree/BetreeMain_TypesExternal_Template.v) | 6 | ||||
| -rw-r--r-- | tests/coq/betree/_CoqProject | 12 | ||||
| -rw-r--r-- | tests/fstar/betree/Betree.Clauses.Template.fst (renamed from tests/fstar/betree/BetreeMain.Clauses.Template.fst) | 36 | ||||
| -rw-r--r-- | tests/fstar/betree/Betree.Clauses.fst (renamed from tests/fstar/betree/BetreeMain.Clauses.fst) | 4 | ||||
| -rw-r--r-- | tests/fstar/betree/Betree.Funs.fst (renamed from tests/fstar/betree/BetreeMain.Funs.fst) | 88 | ||||
| -rw-r--r-- | tests/fstar/betree/Betree.FunsExternal.fsti (renamed from tests/fstar/betree/BetreeMain.FunsExternal.fsti) | 14 | ||||
| -rw-r--r-- | tests/fstar/betree/Betree.Types.fst (renamed from tests/fstar/betree/BetreeMain.Types.fst) | 24 | ||||
| -rw-r--r-- | tests/fstar/betree/Betree.TypesExternal.fsti (renamed from tests/fstar/betree/BetreeMain.TypesExternal.fsti) | 4 | ||||
| -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 | ||||
| -rw-r--r-- | tests/lean/Betree/Funs.lean (renamed from tests/lean/BetreeMain/Funs.lean) | 88 | ||||
| -rw-r--r-- | tests/lean/Betree/FunsExternal.lean (renamed from tests/lean/BetreeMain/FunsExternal.lean) | 14 | ||||
| -rw-r--r-- | tests/lean/Betree/FunsExternal_Template.lean (renamed from tests/lean/BetreeMain/FunsExternal_Template.lean) | 14 | ||||
| -rw-r--r-- | tests/lean/Betree/Types.lean (renamed from tests/lean/BetreeMain/Types.lean) | 26 | ||||
| -rw-r--r-- | tests/lean/Betree/TypesExternal.lean (renamed from tests/lean/BetreeMain/TypesExternal.lean) | 2 | ||||
| -rw-r--r-- | tests/lean/Betree/TypesExternal_Template.lean (renamed from tests/lean/BetreeMain/TypesExternal_Template.lean) | 2 | ||||
| -rw-r--r-- | tests/lean/BetreeMain.lean | 1 | ||||
| -rw-r--r-- | tests/lean/lakefile.lean | 2 | ||||
| -rw-r--r-- | tests/test_runner/run_test.ml | 7 |
31 files changed, 361 insertions, 365 deletions
@@ -90,7 +90,7 @@ betree-llbc = charon.extractCrateWithCharon.${system} { name = "betree"; src = ./tests/src/betree; - charonFlags = "--polonius --opaque=betree_utils --crate betree_main"; + charonFlags = "--polonius --opaque=betree_utils"; craneExtraArgs.checkPhaseCargoCommand = '' cargo rustc -- --test -Zpolonius ./target/debug/betree @@ -125,7 +125,7 @@ mkdir tests/llbc export LLBC_DIR=tests/llbc # Copy over the llbc file we can't generate ourselves. - cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR + cp ${betree-llbc}/llbc/betree.llbc $LLBC_DIR # Run the tests with extra sanity checks enabled IN_CI=1 make test-all -j $NIX_BUILD_CORES diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/Betree_Funs.v index e0a1d8a2..b965d423 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/Betree_Funs.v @@ -1,18 +1,18 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) +(** [betree]: function definitions *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Import BetreeMain_Types. -Include BetreeMain_Types. -Require Import BetreeMain_FunsExternal. -Include BetreeMain_FunsExternal. -Module BetreeMain_Funs. +Require Import Betree_Types. +Include Betree_Types. +Require Import Betree_FunsExternal. +Include Betree_FunsExternal. +Module Betree_Funs. -(** [betree_main::betree::load_internal_node]: +(** [betree::betree::load_internal_node]: Source: 'src/betree.rs', lines 36:0-36:52 *) Definition betree_load_internal_node (id : u64) (st : state) : @@ -21,7 +21,7 @@ Definition betree_load_internal_node betree_utils_load_internal_node id st . -(** [betree_main::betree::store_internal_node]: +(** [betree::betree::store_internal_node]: Source: 'src/betree.rs', lines 41:0-41:60 *) Definition betree_store_internal_node (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) : @@ -30,14 +30,14 @@ Definition betree_store_internal_node betree_utils_store_internal_node id content st . -(** [betree_main::betree::load_leaf_node]: +(** [betree::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 *) Definition betree_load_leaf_node (id : u64) (st : state) : result (state * (betree_List_t (u64 * u64))) := betree_utils_load_leaf_node id st . -(** [betree_main::betree::store_leaf_node]: +(** [betree::betree::store_leaf_node]: Source: 'src/betree.rs', lines 51:0-51:52 *) Definition betree_store_leaf_node (id : u64) (content : betree_List_t (u64 * u64)) (st : state) : @@ -46,19 +46,19 @@ Definition betree_store_leaf_node betree_utils_store_leaf_node id content st . -(** [betree_main::betree::fresh_node_id]: +(** [betree::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 *) Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) := counter1 <- u64_add counter 1%u64; Ok (counter, counter1) . -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: +(** [betree::betree::{betree::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 *) Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t := Ok {| betree_NodeIdCounter_next_node_id := 0%u64 |} . -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: +(** [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 *) Definition betree_NodeIdCounter_fresh_id (self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) := @@ -67,7 +67,7 @@ Definition betree_NodeIdCounter_fresh_id {| betree_NodeIdCounter_next_node_id := i |}) . -(** [betree_main::betree::upsert_update]: +(** [betree::betree::upsert_update]: Source: 'src/betree.rs', lines 234:0-234:70 *) Definition betree_upsert_update (prev : option u64) (st : betree_UpsertFunState_t) : result u64 := @@ -88,7 +88,7 @@ Definition betree_upsert_update end . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: +(** [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 *) Fixpoint betree_List_len (T : Type) (n : nat) (self : betree_List_t T) : result u64 := @@ -102,7 +102,7 @@ Fixpoint betree_List_len end . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: Source: 'src/betree.rs', lines 284:4-284:51 *) Fixpoint betree_List_split_at (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) : @@ -125,7 +125,7 @@ Fixpoint betree_List_split_at end . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: +(** [betree::betree::{betree::betree::List<T>#1}::push_front]: Source: 'src/betree.rs', lines 299:4-299:34 *) Definition betree_List_push_front (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) := @@ -133,7 +133,7 @@ Definition betree_List_push_front Ok (Betree_List_Cons x tl) . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: +(** [betree::betree::{betree::betree::List<T>#1}::pop_front]: Source: 'src/betree.rs', lines 306:4-306:32 *) Definition betree_List_pop_front (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) := @@ -144,7 +144,7 @@ Definition betree_List_pop_front end . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: +(** [betree::betree::{betree::betree::List<T>#1}::hd]: Source: 'src/betree.rs', lines 318:4-318:22 *) Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := match self with @@ -153,7 +153,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := end . -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: Source: 'src/betree.rs', lines 327:4-327:44 *) Definition betree_ListPairU64T_head_has_key (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool := @@ -163,7 +163,7 @@ Definition betree_ListPairU64T_head_has_key end . -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: Source: 'src/betree.rs', lines 339:4-339:73 *) Fixpoint betree_ListPairU64T_partition_at_pivot (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) : @@ -186,7 +186,7 @@ Fixpoint betree_ListPairU64T_partition_at_pivot end . -(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: +(** [betree::betree::{betree::betree::Leaf#3}::split]: Source: 'src/betree.rs', lines 359:4-364:17 *) Definition betree_Leaf_split (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64)) @@ -222,7 +222,7 @@ Definition betree_Leaf_split node_id_cnt2)) . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 *) Fixpoint betree_Node_lookup_first_message_for_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : @@ -250,7 +250,7 @@ Fixpoint betree_Node_lookup_first_message_for_key end . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: Source: 'src/betree.rs', lines 636:4-636:80 *) Fixpoint betree_Node_lookup_in_bindings (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : @@ -271,7 +271,7 @@ Fixpoint betree_Node_lookup_in_bindings end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: Source: 'src/betree.rs', lines 819:4-819:90 *) Fixpoint betree_Node_apply_upserts (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) @@ -303,7 +303,7 @@ Fixpoint betree_Node_apply_upserts end . -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: +(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) Fixpoint betree_Internal_lookup_in_children (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : @@ -327,7 +327,7 @@ Fixpoint betree_Internal_lookup_in_children self.(betree_Internal_pivot) self.(betree_Internal_left) n2))) end -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: +(** [betree::betree::{betree::betree::Node#5}::lookup]: Source: 'src/betree.rs', lines 709:4-709:58 *) with betree_Node_lookup (n : nat) (self : betree_Node_t) (key : u64) (st : state) : @@ -394,7 +394,7 @@ with betree_Node_lookup end . -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: Source: 'src/betree.rs', lines 674:4-674:77 *) Fixpoint betree_Node_filter_messages_for_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : @@ -419,7 +419,7 @@ Fixpoint betree_Node_filter_messages_for_key end . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: Source: 'src/betree.rs', lines 689:4-692:34 *) Fixpoint betree_Node_lookup_first_message_after_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : @@ -447,7 +447,7 @@ Fixpoint betree_Node_lookup_first_message_after_key end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: +(** [betree::betree::{betree::betree::Node#5}::apply_to_internal]: Source: 'src/betree.rs', lines 521:4-521:89 *) Definition betree_Node_apply_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64) @@ -508,7 +508,7 @@ Definition betree_Node_apply_to_internal lookup_first_message_for_key_back msgs2) . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 *) Fixpoint betree_Node_apply_messages_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) @@ -528,7 +528,7 @@ Fixpoint betree_Node_apply_messages_to_internal end . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: Source: 'src/betree.rs', lines 653:4-656:32 *) Fixpoint betree_Node_lookup_mut_in_bindings (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : @@ -556,7 +556,7 @@ Fixpoint betree_Node_lookup_mut_in_bindings end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: +(** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: Source: 'src/betree.rs', lines 460:4-460:87 *) Definition betree_Node_apply_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64) @@ -594,7 +594,7 @@ Definition betree_Node_apply_to_leaf end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 *) Fixpoint betree_Node_apply_messages_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) @@ -614,7 +614,7 @@ Fixpoint betree_Node_apply_messages_to_leaf end . -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: +(** [betree::betree::{betree::betree::Internal#4}::flush]: Source: 'src/betree.rs', lines 410:4-415:26 *) Fixpoint betree_Internal_flush (n : nat) (self : betree_Internal_t) (params : betree_Params_t) @@ -664,7 +664,7 @@ Fixpoint betree_Internal_flush node_id_cnt1)))) end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages]: Source: 'src/betree.rs', lines 588:4-593:5 *) with betree_Node_apply_messages (n : nat) (self : betree_Node_t) (params : betree_Params_t) @@ -720,7 +720,7 @@ with betree_Node_apply_messages end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: +(** [betree::betree::{betree::betree::Node#5}::apply]: Source: 'src/betree.rs', lines 576:4-582:5 *) Definition betree_Node_apply (n : nat) (self : betree_Node_t) (params : betree_Params_t) @@ -736,7 +736,7 @@ Definition betree_Node_apply Ok (st1, (self1, node_id_cnt1)) . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: +(** [betree::betree::{betree::betree::BeTree#6}::new]: Source: 'src/betree.rs', lines 849:4-849:60 *) Definition betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : @@ -761,7 +761,7 @@ Definition betree_BeTree_new |}) . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: +(** [betree::betree::{betree::betree::BeTree#6}::apply]: Source: 'src/betree.rs', lines 868:4-868:47 *) Definition betree_BeTree_apply (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) @@ -781,7 +781,7 @@ Definition betree_BeTree_apply |}) . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: +(** [betree::betree::{betree::betree::BeTree#6}::insert]: Source: 'src/betree.rs', lines 874:4-874:52 *) Definition betree_BeTree_insert (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : @@ -790,7 +790,7 @@ Definition betree_BeTree_insert betree_BeTree_apply n self key (Betree_Message_Insert value) st . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: +(** [betree::betree::{betree::betree::BeTree#6}::delete]: Source: 'src/betree.rs', lines 880:4-880:38 *) Definition betree_BeTree_delete (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : @@ -799,7 +799,7 @@ Definition betree_BeTree_delete betree_BeTree_apply n self key Betree_Message_Delete st . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: +(** [betree::betree::{betree::betree::BeTree#6}::upsert]: Source: 'src/betree.rs', lines 886:4-886:59 *) Definition betree_BeTree_upsert (n : nat) (self : betree_BeTree_t) (key : u64) @@ -809,7 +809,7 @@ Definition betree_BeTree_upsert betree_BeTree_apply n self key (Betree_Message_Upsert upd) st . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: +(** [betree::betree::{betree::betree::BeTree#6}::lookup]: Source: 'src/betree.rs', lines 895:4-895:62 *) Definition betree_BeTree_lookup (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : @@ -826,12 +826,12 @@ Definition betree_BeTree_lookup |})) . -(** [betree_main::main]: +(** [betree::main]: Source: 'src/main.rs', lines 4:0-4:9 *) Definition main : result unit := Ok tt. -(** Unit test for [betree_main::main] *) +(** Unit test for [betree::main] *) Check (main )%return. -End BetreeMain_Funs. +End Betree_Funs. diff --git a/tests/coq/betree/BetreeMain_FunsExternal.v b/tests/coq/betree/Betree_FunsExternal.v index 099a2e8f..0263c272 100644 --- a/tests/coq/betree/BetreeMain_FunsExternal.v +++ b/tests/coq/betree/Betree_FunsExternal.v @@ -6,9 +6,9 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Export BetreeMain_Types. -Import BetreeMain_Types. -Module BetreeMain_FunsExternal. +Require Export Betree_Types. +Import Betree_Types. +Module Betree_FunsExternal. (** [betree_main::betree_utils::load_internal_node]: forward function Source: 'src/betree_utils.rs', lines 98:0-98:63 *) @@ -36,4 +36,4 @@ Axiom betree_utils_store_leaf_node : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) . -End BetreeMain_FunsExternal. +End Betree_FunsExternal. diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/Betree_FunsExternal_Template.v index 58be2733..2a2fddfc 100644 --- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v +++ b/tests/coq/betree/Betree_FunsExternal_Template.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external functions. +(** [betree]: external functions. -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) Require Import Primitives. Import Primitives. @@ -7,17 +7,17 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Import BetreeMain_Types. -Include BetreeMain_Types. -Module BetreeMain_FunsExternal_Template. +Require Import Betree_Types. +Include Betree_Types. +Module Betree_FunsExternal_Template. -(** [betree_main::betree_utils::load_internal_node]: +(** [betree::betree_utils::load_internal_node]: Source: 'src/betree_utils.rs', lines 98:0-98:63 *) Axiom betree_utils_load_internal_node : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t))) . -(** [betree_main::betree_utils::store_internal_node]: +(** [betree::betree_utils::store_internal_node]: Source: 'src/betree_utils.rs', lines 115:0-115:71 *) Axiom betree_utils_store_internal_node : @@ -25,16 +25,16 @@ Axiom betree_utils_store_internal_node unit) . -(** [betree_main::betree_utils::load_leaf_node]: +(** [betree::betree_utils::load_leaf_node]: Source: 'src/betree_utils.rs', lines 132:0-132:55 *) Axiom betree_utils_load_leaf_node : u64 -> state -> result (state * (betree_List_t (u64 * u64))) . -(** [betree_main::betree_utils::store_leaf_node]: +(** [betree::betree_utils::store_leaf_node]: Source: 'src/betree_utils.rs', lines 145:0-145:63 *) Axiom betree_utils_store_leaf_node : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) . -End BetreeMain_FunsExternal_Template. +End Betree_FunsExternal_Template. diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/Betree_Types.v index acbc2085..aa39d8e4 100644 --- a/tests/coq/betree/BetreeMain_Types.v +++ b/tests/coq/betree/Betree_Types.v @@ -1,16 +1,16 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: type definitions *) +(** [betree]: type definitions *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Import BetreeMain_TypesExternal. -Include BetreeMain_TypesExternal. -Module BetreeMain_Types. +Require Import Betree_TypesExternal. +Include Betree_TypesExternal. +Module Betree_Types. -(** [betree_main::betree::List] +(** [betree::betree::List] Source: 'src/betree.rs', lines 17:0-17:23 *) Inductive betree_List_t (T : Type) := | Betree_List_Cons : T -> betree_List_t T -> betree_List_t T @@ -20,14 +20,14 @@ Inductive betree_List_t (T : Type) := Arguments Betree_List_Cons { _ }. Arguments Betree_List_Nil { _ }. -(** [betree_main::betree::UpsertFunState] +(** [betree::betree::UpsertFunState] Source: 'src/betree.rs', lines 63:0-63:23 *) Inductive betree_UpsertFunState_t := | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t . -(** [betree_main::betree::Message] +(** [betree::betree::Message] Source: 'src/betree.rs', lines 69:0-69:23 *) Inductive betree_Message_t := | Betree_Message_Insert : u64 -> betree_Message_t @@ -35,7 +35,7 @@ Inductive betree_Message_t := | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t . -(** [betree_main::betree::Leaf] +(** [betree::betree::Leaf] Source: 'src/betree.rs', lines 167:0-167:11 *) Record betree_Leaf_t := mkbetree_Leaf_t { @@ -43,7 +43,7 @@ mkbetree_Leaf_t { } . -(** [betree_main::betree::Internal] +(** [betree::betree::Internal] Source: 'src/betree.rs', lines 156:0-156:15 *) Inductive betree_Internal_t := | mkbetree_Internal_t : @@ -53,7 +53,7 @@ Inductive betree_Internal_t := betree_Node_t -> betree_Internal_t -(** [betree_main::betree::Node] +(** [betree::betree::Node] Source: 'src/betree.rs', lines 179:0-179:9 *) with betree_Node_t := | Betree_Node_Internal : betree_Internal_t -> betree_Node_t @@ -89,7 +89,7 @@ Notation "x2 .(betree_Internal_right)" := (betree_Internal_right x2) (at level 9) . -(** [betree_main::betree::Params] +(** [betree::betree::Params] Source: 'src/betree.rs', lines 187:0-187:13 *) Record betree_Params_t := mkbetree_Params_t { @@ -97,7 +97,7 @@ mkbetree_Params_t { } . -(** [betree_main::betree::NodeIdCounter] +(** [betree::betree::NodeIdCounter] Source: 'src/betree.rs', lines 201:0-201:20 *) Record betree_NodeIdCounter_t := mkbetree_NodeIdCounter_t { @@ -105,7 +105,7 @@ mkbetree_NodeIdCounter_t { } . -(** [betree_main::betree::BeTree] +(** [betree::betree::BeTree] Source: 'src/betree.rs', lines 218:0-218:17 *) Record betree_BeTree_t := mkbetree_BeTree_t { @@ -115,4 +115,4 @@ mkbetree_BeTree_t { } . -End BetreeMain_Types. +End Betree_Types. diff --git a/tests/coq/betree/BetreeMain_TypesExternal.v b/tests/coq/betree/Betree_TypesExternal.v index 870d2601..37487d6d 100644 --- a/tests/coq/betree/BetreeMain_TypesExternal.v +++ b/tests/coq/betree/Betree_TypesExternal.v @@ -6,9 +6,9 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Module BetreeMain_TypesExternal. +Module Betree_TypesExternal. (** The state type used in the state-error monad *) Axiom state : Type. -End BetreeMain_TypesExternal. +End Betree_TypesExternal. diff --git a/tests/coq/betree/BetreeMain_TypesExternal_Template.v b/tests/coq/betree/Betree_TypesExternal_Template.v index 651de2b7..a40811cb 100644 --- a/tests/coq/betree/BetreeMain_TypesExternal_Template.v +++ b/tests/coq/betree/Betree_TypesExternal_Template.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external types. +(** [betree]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) Require Import Primitives. Import Primitives. @@ -7,9 +7,9 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Module BetreeMain_TypesExternal_Template. +Module Betree_TypesExternal_Template. (** The state type used in the state-error monad *) Axiom state : Type. -End BetreeMain_TypesExternal_Template. +End Betree_TypesExternal_Template. diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject index b14bed66..9fb7fe64 100644 --- a/tests/coq/betree/_CoqProject +++ b/tests/coq/betree/_CoqProject @@ -3,10 +3,10 @@ -arg -w -arg all -BetreeMain_TypesExternal_Template.v -BetreeMain_Types.v +Betree_TypesExternal_Template.v +Betree_Types.v Primitives.v -BetreeMain_FunsExternal_Template.v -BetreeMain_Funs.v -BetreeMain_TypesExternal.v -BetreeMain_FunsExternal.v +Betree_FunsExternal_Template.v +Betree_Funs.v +Betree_TypesExternal.v +Betree_FunsExternal.v diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst index b317dca4..fad8c5ba 100644 --- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree/Betree.Clauses.Template.fst @@ -1,46 +1,46 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: templates for the decreases clauses *) -module BetreeMain.Clauses.Template +(** [betree]: templates for the decreases clauses *) +module Betree.Clauses.Template open Primitives -open BetreeMain.Types +open Betree.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause +(** [betree::betree::{betree::betree::List<T>#1}::len]: decreases clause Source: 'src/betree.rs', lines 276:4-276:24 *) unfold let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat = admit () -(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause Source: 'src/betree.rs', lines 284:4-284:51 *) unfold let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) (n : u64) : nat = admit () -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause Source: 'src/betree.rs', lines 339:4-339:73 *) unfold let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: decreases clause Source: 'src/betree.rs', lines 789:4-792:34 *) unfold let betree_Node_lookup_first_message_for_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: decreases clause Source: 'src/betree.rs', lines 636:4-636:80 *) unfold let betree_Node_lookup_in_bindings_decreases (key : u64) (bindings : betree_List_t (u64 & u64)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: decreases clause Source: 'src/betree.rs', lines 819:4-819:90 *) unfold let betree_Node_apply_upserts_decreases @@ -48,35 +48,35 @@ let betree_Node_apply_upserts_decreases (key : u64) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause +(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: decreases clause Source: 'src/betree.rs', lines 395:4-395:63 *) unfold let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t) (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup]: decreases clause Source: 'src/betree.rs', lines 709:4-709:58 *) unfold let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: decreases clause Source: 'src/betree.rs', lines 674:4-674:77 *) unfold let betree_Node_filter_messages_for_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: decreases clause Source: 'src/betree.rs', lines 689:4-692:34 *) unfold let betree_Node_lookup_first_message_after_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: decreases clause Source: 'src/betree.rs', lines 502:4-505:5 *) unfold let betree_Node_apply_messages_to_internal_decreases @@ -84,14 +84,14 @@ let betree_Node_apply_messages_to_internal_decreases (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: decreases clause Source: 'src/betree.rs', lines 653:4-656:32 *) unfold let betree_Node_lookup_mut_in_bindings_decreases (key : u64) (bindings : betree_List_t (u64 & u64)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: decreases clause Source: 'src/betree.rs', lines 444:4-447:5 *) unfold let betree_Node_apply_messages_to_leaf_decreases @@ -99,7 +99,7 @@ let betree_Node_apply_messages_to_leaf_decreases (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause +(** [betree::betree::{betree::betree::Internal#4}::flush]: decreases clause Source: 'src/betree.rs', lines 410:4-415:26 *) unfold let betree_Internal_flush_decreases (self : betree_Internal_t) @@ -107,7 +107,7 @@ let betree_Internal_flush_decreases (self : betree_Internal_t) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::apply_messages]: decreases clause Source: 'src/betree.rs', lines 588:4-593:5 *) unfold let betree_Node_apply_messages_decreases (self : betree_Node_t) diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/Betree.Clauses.fst index b95d4c7e..ae201cee 100644 --- a/tests/fstar/betree/BetreeMain.Clauses.fst +++ b/tests/fstar/betree/Betree.Clauses.fst @@ -1,7 +1,7 @@ (** [betree_main]: templates for the decreases clauses *) -module BetreeMain.Clauses +module Betree.Clauses open Primitives -open BetreeMain.Types +open Betree.Types #set-options "--z3rlimit 50 --fuel 0 --ifuel 1" diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/Betree.Funs.fst index 9942ef68..07f561f5 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/Betree.Funs.fst @@ -1,14 +1,14 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) -module BetreeMain.Funs +(** [betree]: function definitions *) +module Betree.Funs open Primitives -include BetreeMain.Types -include BetreeMain.FunsExternal -include BetreeMain.Clauses +include Betree.Types +include Betree.FunsExternal +include Betree.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::load_internal_node]: +(** [betree::betree::load_internal_node]: Source: 'src/betree.rs', lines 36:0-36:52 *) let betree_load_internal_node (id : u64) (st : state) : @@ -16,7 +16,7 @@ let betree_load_internal_node = betree_utils_load_internal_node id st -(** [betree_main::betree::store_internal_node]: +(** [betree::betree::store_internal_node]: Source: 'src/betree.rs', lines 41:0-41:60 *) let betree_store_internal_node (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : @@ -24,13 +24,13 @@ let betree_store_internal_node = betree_utils_store_internal_node id content st -(** [betree_main::betree::load_leaf_node]: +(** [betree::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 *) let betree_load_leaf_node (id : u64) (st : state) : result (state & (betree_List_t (u64 & u64))) = betree_utils_load_leaf_node id st -(** [betree_main::betree::store_leaf_node]: +(** [betree::betree::store_leaf_node]: Source: 'src/betree.rs', lines 51:0-51:52 *) let betree_store_leaf_node (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : @@ -38,24 +38,24 @@ let betree_store_leaf_node = betree_utils_store_leaf_node id content st -(** [betree_main::betree::fresh_node_id]: +(** [betree::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 *) let betree_fresh_node_id (counter : u64) : result (u64 & u64) = let* counter1 = u64_add counter 1 in Ok (counter, counter1) -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: +(** [betree::betree::{betree::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 *) let betree_NodeIdCounter_new : result betree_NodeIdCounter_t = Ok { next_node_id = 0 } -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: +(** [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 *) let betree_NodeIdCounter_fresh_id (self : betree_NodeIdCounter_t) : result (u64 & betree_NodeIdCounter_t) = let* i = u64_add self.next_node_id 1 in Ok (self.next_node_id, { next_node_id = i }) -(** [betree_main::betree::upsert_update]: +(** [betree::betree::upsert_update]: Source: 'src/betree.rs', lines 234:0-234:70 *) let betree_upsert_update (prev : option u64) (st : betree_UpsertFunState_t) : result u64 = @@ -75,7 +75,7 @@ let betree_upsert_update end end -(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: +(** [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 *) let rec betree_List_len (t : Type0) (self : betree_List_t t) : @@ -86,7 +86,7 @@ let rec betree_List_len | Betree_List_Nil -> Ok 0 end -(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: Source: 'src/betree.rs', lines 284:4-284:51 *) let rec betree_List_split_at (t : Type0) (self : betree_List_t t) (n : u64) : @@ -105,14 +105,14 @@ let rec betree_List_split_at | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: +(** [betree::betree::{betree::betree::List<T>#1}::push_front]: Source: 'src/betree.rs', lines 299:4-299:34 *) let betree_List_push_front (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) = let (tl, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in Ok (Betree_List_Cons x tl) -(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: +(** [betree::betree::{betree::betree::List<T>#1}::pop_front]: Source: 'src/betree.rs', lines 306:4-306:32 *) let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) = @@ -122,7 +122,7 @@ let betree_List_pop_front | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: +(** [betree::betree::{betree::betree::List<T>#1}::hd]: Source: 'src/betree.rs', lines 318:4-318:22 *) let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = begin match self with @@ -130,7 +130,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = | Betree_List_Nil -> Fail Failure end -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: Source: 'src/betree.rs', lines 327:4-327:44 *) let betree_ListPairU64T_head_has_key (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool = @@ -139,7 +139,7 @@ let betree_ListPairU64T_head_has_key | Betree_List_Nil -> Ok false end -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: Source: 'src/betree.rs', lines 339:4-339:73 *) let rec betree_ListPairU64T_partition_at_pivot (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : @@ -158,7 +158,7 @@ let rec betree_ListPairU64T_partition_at_pivot | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil) end -(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: +(** [betree::betree::{betree::betree::Leaf#3}::split]: Source: 'src/betree.rs', lines 359:4-364:17 *) let betree_Leaf_split (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) @@ -179,7 +179,7 @@ let betree_Leaf_split Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, node_id_cnt2)) -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 *) let rec betree_Node_lookup_first_message_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : @@ -203,7 +203,7 @@ let rec betree_Node_lookup_first_message_for_key | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) end -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: Source: 'src/betree.rs', lines 636:4-636:80 *) let rec betree_Node_lookup_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : @@ -219,7 +219,7 @@ let rec betree_Node_lookup_in_bindings | Betree_List_Nil -> Ok None end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: Source: 'src/betree.rs', lines 819:4-819:90 *) let rec betree_Node_apply_upserts (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) @@ -246,7 +246,7 @@ let rec betree_Node_apply_upserts Betree_Message_Insert v) in Ok (v, msgs1) -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: +(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) let rec betree_Internal_lookup_in_children (self : betree_Internal_t) (key : u64) (st : state) : @@ -261,7 +261,7 @@ let rec betree_Internal_lookup_in_children let* (st1, (o, n)) = betree_Node_lookup self.right key st in Ok (st1, (o, { self with right = n })) -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: +(** [betree::betree::{betree::betree::Node#5}::lookup]: Source: 'src/betree.rs', lines 709:4-709:58 *) and betree_Node_lookup (self : betree_Node_t) (key : u64) (st : state) : @@ -317,7 +317,7 @@ and betree_Node_lookup Ok (st1, (o, Betree_Node_Leaf node)) end -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: Source: 'src/betree.rs', lines 674:4-674:77 *) let rec betree_Node_filter_messages_for_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : @@ -337,7 +337,7 @@ let rec betree_Node_filter_messages_for_key | Betree_List_Nil -> Ok Betree_List_Nil end -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: Source: 'src/betree.rs', lines 689:4-692:34 *) let rec betree_Node_lookup_first_message_after_key (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : @@ -361,7 +361,7 @@ let rec betree_Node_lookup_first_message_after_key | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: +(** [betree::betree::{betree::betree::Node#5}::apply_to_internal]: Source: 'src/betree.rs', lines 521:4-521:89 *) let betree_Node_apply_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64) @@ -421,7 +421,7 @@ let betree_Node_apply_to_internal betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in lookup_first_message_for_key_back msgs2 -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 *) let rec betree_Node_apply_messages_to_internal (msgs : betree_List_t (u64 & betree_Message_t)) @@ -437,7 +437,7 @@ let rec betree_Node_apply_messages_to_internal | Betree_List_Nil -> Ok msgs end -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: Source: 'src/betree.rs', lines 653:4-656:32 *) let rec betree_Node_lookup_mut_in_bindings (key : u64) (bindings : betree_List_t (u64 & u64)) : @@ -461,7 +461,7 @@ let rec betree_Node_lookup_mut_in_bindings | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: +(** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: Source: 'src/betree.rs', lines 460:4-460:87 *) let betree_Node_apply_to_leaf (bindings : betree_List_t (u64 & u64)) (key : u64) @@ -497,7 +497,7 @@ let betree_Node_apply_to_leaf lookup_mut_in_bindings_back bindings2 end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 *) let rec betree_Node_apply_messages_to_leaf (bindings : betree_List_t (u64 & u64)) @@ -513,7 +513,7 @@ let rec betree_Node_apply_messages_to_leaf | Betree_List_Nil -> Ok bindings end -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: +(** [betree::betree::{betree::betree::Internal#4}::flush]: Source: 'src/betree.rs', lines 410:4-415:26 *) let rec betree_Internal_flush (self : betree_Internal_t) (params : betree_Params_t) @@ -550,7 +550,7 @@ let rec betree_Internal_flush let (n, node_id_cnt1) = p1 in Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1))) -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages]: Source: 'src/betree.rs', lines 588:4-593:5 *) and betree_Node_apply_messages (self : betree_Node_t) (params : betree_Params_t) @@ -591,7 +591,7 @@ and betree_Node_apply_messages Ok (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: +(** [betree::betree::{betree::betree::Node#5}::apply]: Source: 'src/betree.rs', lines 576:4-582:5 *) let betree_Node_apply (self : betree_Node_t) (params : betree_Params_t) @@ -605,7 +605,7 @@ let betree_Node_apply let (self1, node_id_cnt1) = p in Ok (st1, (self1, node_id_cnt1)) -(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: +(** [betree::betree::{betree::betree::BeTree#6}::new]: Source: 'src/betree.rs', lines 849:4-849:60 *) let betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : @@ -621,7 +621,7 @@ let betree_BeTree_new root = (Betree_Node_Leaf { id = id; size = 0 }) }) -(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: +(** [betree::betree::{betree::betree::BeTree#6}::apply]: Source: 'src/betree.rs', lines 868:4-868:47 *) let betree_BeTree_apply (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : @@ -632,7 +632,7 @@ let betree_BeTree_apply let (n, nic) = p in Ok (st1, { self with node_id_cnt = nic; root = n }) -(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: +(** [betree::betree::{betree::betree::BeTree#6}::insert]: Source: 'src/betree.rs', lines 874:4-874:52 *) let betree_BeTree_insert (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : @@ -640,7 +640,7 @@ let betree_BeTree_insert = betree_BeTree_apply self key (Betree_Message_Insert value) st -(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: +(** [betree::betree::{betree::betree::BeTree#6}::delete]: Source: 'src/betree.rs', lines 880:4-880:38 *) let betree_BeTree_delete (self : betree_BeTree_t) (key : u64) (st : state) : @@ -648,7 +648,7 @@ let betree_BeTree_delete = betree_BeTree_apply self key Betree_Message_Delete st -(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: +(** [betree::betree::{betree::betree::BeTree#6}::upsert]: Source: 'src/betree.rs', lines 886:4-886:59 *) let betree_BeTree_upsert (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) @@ -657,7 +657,7 @@ let betree_BeTree_upsert = betree_BeTree_apply self key (Betree_Message_Upsert upd) st -(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: +(** [betree::betree::{betree::betree::BeTree#6}::lookup]: Source: 'src/betree.rs', lines 895:4-895:62 *) let betree_BeTree_lookup (self : betree_BeTree_t) (key : u64) (st : state) : @@ -666,11 +666,11 @@ let betree_BeTree_lookup let* (st1, (o, n)) = betree_Node_lookup self.root key st in Ok (st1, (o, { self with root = n })) -(** [betree_main::main]: +(** [betree::main]: Source: 'src/main.rs', lines 4:0-4:9 *) let main : result unit = Ok () -(** Unit test for [betree_main::main] *) +(** Unit test for [betree::main] *) let _ = assert_norm (main = Ok ()) diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/Betree.FunsExternal.fsti index 8be98acf..db96eead 100644 --- a/tests/fstar/betree/BetreeMain.FunsExternal.fsti +++ b/tests/fstar/betree/Betree.FunsExternal.fsti @@ -1,29 +1,29 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external function declarations *) -module BetreeMain.FunsExternal +(** [betree]: external function declarations *) +module Betree.FunsExternal open Primitives -include BetreeMain.Types +include Betree.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree_utils::load_internal_node]: +(** [betree::betree_utils::load_internal_node]: Source: 'src/betree_utils.rs', lines 98:0-98:63 *) val betree_utils_load_internal_node : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t))) -(** [betree_main::betree_utils::store_internal_node]: +(** [betree::betree_utils::store_internal_node]: Source: 'src/betree_utils.rs', lines 115:0-115:71 *) val betree_utils_store_internal_node : u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state & unit) -(** [betree_main::betree_utils::load_leaf_node]: +(** [betree::betree_utils::load_leaf_node]: Source: 'src/betree_utils.rs', lines 132:0-132:55 *) val betree_utils_load_leaf_node : u64 -> state -> result (state & (betree_List_t (u64 & u64))) -(** [betree_main::betree_utils::store_leaf_node]: +(** [betree::betree_utils::store_leaf_node]: Source: 'src/betree_utils.rs', lines 145:0-145:63 *) val betree_utils_store_leaf_node : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) diff --git a/tests/fstar/betree/BetreeMain.Types.fst b/tests/fstar/betree/Betree.Types.fst index b87219b2..6b8e063b 100644 --- a/tests/fstar/betree/BetreeMain.Types.fst +++ b/tests/fstar/betree/Betree.Types.fst @@ -1,56 +1,56 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: type definitions *) -module BetreeMain.Types +(** [betree]: type definitions *) +module Betree.Types open Primitives -include BetreeMain.TypesExternal +include Betree.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::List] +(** [betree::betree::List] Source: 'src/betree.rs', lines 17:0-17:23 *) type betree_List_t (t : Type0) = | Betree_List_Cons : t -> betree_List_t t -> betree_List_t t | Betree_List_Nil : betree_List_t t -(** [betree_main::betree::UpsertFunState] +(** [betree::betree::UpsertFunState] Source: 'src/betree.rs', lines 63:0-63:23 *) type betree_UpsertFunState_t = | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t -(** [betree_main::betree::Message] +(** [betree::betree::Message] Source: 'src/betree.rs', lines 69:0-69:23 *) type betree_Message_t = | Betree_Message_Insert : u64 -> betree_Message_t | Betree_Message_Delete : betree_Message_t | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t -(** [betree_main::betree::Leaf] +(** [betree::betree::Leaf] Source: 'src/betree.rs', lines 167:0-167:11 *) type betree_Leaf_t = { id : u64; size : u64; } -(** [betree_main::betree::Internal] +(** [betree::betree::Internal] Source: 'src/betree.rs', lines 156:0-156:15 *) type betree_Internal_t = { id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t; } -(** [betree_main::betree::Node] +(** [betree::betree::Node] Source: 'src/betree.rs', lines 179:0-179:9 *) and betree_Node_t = | Betree_Node_Internal : betree_Internal_t -> betree_Node_t | Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t -(** [betree_main::betree::Params] +(** [betree::betree::Params] Source: 'src/betree.rs', lines 187:0-187:13 *) type betree_Params_t = { min_flush_size : u64; split_size : u64; } -(** [betree_main::betree::NodeIdCounter] +(** [betree::betree::NodeIdCounter] Source: 'src/betree.rs', lines 201:0-201:20 *) type betree_NodeIdCounter_t = { next_node_id : u64; } -(** [betree_main::betree::BeTree] +(** [betree::betree::BeTree] Source: 'src/betree.rs', lines 218:0-218:17 *) type betree_BeTree_t = { diff --git a/tests/fstar/betree/BetreeMain.TypesExternal.fsti b/tests/fstar/betree/Betree.TypesExternal.fsti index 1b2c53a6..39e53ec9 100644 --- a/tests/fstar/betree/BetreeMain.TypesExternal.fsti +++ b/tests/fstar/betree/Betree.TypesExternal.fsti @@ -1,6 +1,6 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external type declarations *) -module BetreeMain.TypesExternal +(** [betree]: external type declarations *) +module Betree.TypesExternal open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" 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 diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/Betree/Funs.lean index f6fda6db..8612ccbc 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -1,13 +1,13 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: function definitions +-- [betree]: function definitions import Base -import BetreeMain.Types -import BetreeMain.FunsExternal +import Betree.Types +import Betree.FunsExternal open Primitives -namespace betree_main +namespace betree -/- [betree_main::betree::load_internal_node]: +/- [betree::betree::load_internal_node]: Source: 'src/betree.rs', lines 36:0-36:52 -/ def betree.load_internal_node (id : U64) (st : State) : @@ -15,7 +15,7 @@ def betree.load_internal_node := betree_utils.load_internal_node id st -/- [betree_main::betree::store_internal_node]: +/- [betree::betree::store_internal_node]: Source: 'src/betree.rs', lines 41:0-41:60 -/ def betree.store_internal_node (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) : @@ -23,13 +23,13 @@ def betree.store_internal_node := betree_utils.store_internal_node id content st -/- [betree_main::betree::load_leaf_node]: +/- [betree::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 -/ def betree.load_leaf_node (id : U64) (st : State) : Result (State × (betree.List (U64 × U64))) := betree_utils.load_leaf_node id st -/- [betree_main::betree::store_leaf_node]: +/- [betree::betree::store_leaf_node]: Source: 'src/betree.rs', lines 51:0-51:52 -/ def betree.store_leaf_node (id : U64) (content : betree.List (U64 × U64)) (st : State) : @@ -37,19 +37,19 @@ def betree.store_leaf_node := betree_utils.store_leaf_node id content st -/- [betree_main::betree::fresh_node_id]: +/- [betree::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 -/ def betree.fresh_node_id (counter : U64) : Result (U64 × U64) := do let counter1 ← counter + 1#u64 Result.ok (counter, counter1) -/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: +/- [betree::betree::{betree::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 -/ def betree.NodeIdCounter.new : Result betree.NodeIdCounter := Result.ok { next_node_id := 0#u64 } -/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: +/- [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 -/ def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) := @@ -57,7 +57,7 @@ def betree.NodeIdCounter.fresh_id let i ← self.next_node_id + 1#u64 Result.ok (self.next_node_id, { next_node_id := i }) -/- [betree_main::betree::upsert_update]: +/- [betree::betree::upsert_update]: Source: 'src/betree.rs', lines 234:0-234:70 -/ def betree.upsert_update (prev : Option U64) (st : betree.UpsertFunState) : Result U64 := @@ -79,7 +79,7 @@ def betree.upsert_update then prev1 - v else Result.ok 0#u64 -/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: +/- [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 -/ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 := match self with @@ -88,7 +88,7 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 := 1#u64 + i | betree.List.Nil => Result.ok 0#u64 -/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: +/- [betree::betree::{betree::betree::List<T>#1}::split_at]: Source: 'src/betree.rs', lines 284:4-284:51 -/ divergent def betree.List.split_at (T : Type) (self : betree.List T) (n : U64) : @@ -106,14 +106,14 @@ divergent def betree.List.split_at Result.ok (betree.List.Cons hd ls0, ls1) | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: +/- [betree::betree::{betree::betree::List<T>#1}::push_front]: Source: 'src/betree.rs', lines 299:4-299:34 -/ def betree.List.push_front (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) := let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil Result.ok (betree.List.Cons x tl) -/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: +/- [betree::betree::{betree::betree::List<T>#1}::pop_front]: Source: 'src/betree.rs', lines 306:4-306:32 -/ def betree.List.pop_front (T : Type) (self : betree.List T) : Result (T × (betree.List T)) := @@ -122,14 +122,14 @@ def betree.List.pop_front | betree.List.Cons x tl => Result.ok (x, tl) | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: +/- [betree::betree::{betree::betree::List<T>#1}::hd]: Source: 'src/betree.rs', lines 318:4-318:22 -/ def betree.List.hd (T : Type) (self : betree.List T) : Result T := match self with | betree.List.Cons hd _ => Result.ok hd | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: +/- [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: Source: 'src/betree.rs', lines 327:4-327:44 -/ def betree.ListPairU64T.head_has_key (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool := @@ -138,7 +138,7 @@ def betree.ListPairU64T.head_has_key Result.ok (i = key) | betree.List.Nil => Result.ok false -/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: +/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: Source: 'src/betree.rs', lines 339:4-339:73 -/ divergent def betree.ListPairU64T.partition_at_pivot (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : @@ -156,7 +156,7 @@ divergent def betree.ListPairU64T.partition_at_pivot Result.ok (betree.List.Cons (i, t) ls0, ls1) | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil) -/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: +/- [betree::betree::{betree::betree::Leaf#3}::split]: Source: 'src/betree.rs', lines 359:4-364:17 -/ def betree.Leaf.split (self : betree.Leaf) (content : betree.List (U64 × U64)) @@ -176,7 +176,7 @@ def betree.Leaf.split let n1 := betree.Node.Leaf { id := id1, size := params.split_size } Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2)) -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 -/ divergent def betree.Node.lookup_first_message_for_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : @@ -200,7 +200,7 @@ divergent def betree.Node.lookup_first_message_for_key Result.ok (l, back) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: +/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: Source: 'src/betree.rs', lines 636:4-636:80 -/ divergent def betree.Node.lookup_in_bindings (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := @@ -215,7 +215,7 @@ divergent def betree.Node.lookup_in_bindings else betree.Node.lookup_in_bindings key tl | betree.List.Nil => Result.ok none -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: +/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: Source: 'src/betree.rs', lines 819:4-819:90 -/ divergent def betree.Node.apply_upserts (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) @@ -244,7 +244,7 @@ divergent def betree.Node.apply_upserts betree.Message.Insert v) Result.ok (v, msgs1) -/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: +/- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 -/ mutual divergent def betree.Internal.lookup_in_children (self : betree.Internal) (key : U64) (st : State) : @@ -260,7 +260,7 @@ mutual divergent def betree.Internal.lookup_in_children let (st1, (o, n)) ← betree.Node.lookup self.right key st Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n)) -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: +/- [betree::betree::{betree::betree::Node#5}::lookup]: Source: 'src/betree.rs', lines 709:4-709:58 -/ divergent def betree.Node.lookup (self : betree.Node) (key : U64) (st : State) : @@ -320,7 +320,7 @@ divergent def betree.Node.lookup end -/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: +/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: Source: 'src/betree.rs', lines 674:4-674:77 -/ divergent def betree.Node.filter_messages_for_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : @@ -339,7 +339,7 @@ divergent def betree.Node.filter_messages_for_key else Result.ok (betree.List.Cons (k, m) l) | betree.List.Nil => Result.ok betree.List.Nil -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: Source: 'src/betree.rs', lines 689:4-692:34 -/ divergent def betree.Node.lookup_first_message_after_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : @@ -363,7 +363,7 @@ divergent def betree.Node.lookup_first_message_after_key else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: +/- [betree::betree::{betree::betree::Node#5}::apply_to_internal]: Source: 'src/betree.rs', lines 521:4-521:89 -/ def betree.Node.apply_to_internal (msgs : betree.List (U64 × betree.Message)) (key : U64) @@ -427,7 +427,7 @@ def betree.Node.apply_to_internal betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) lookup_first_message_for_key_back msgs2 -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 -/ divergent def betree.Node.apply_messages_to_internal (msgs : betree.List (U64 × betree.Message)) @@ -442,7 +442,7 @@ divergent def betree.Node.apply_messages_to_internal betree.Node.apply_messages_to_internal msgs1 new_msgs_tl | betree.List.Nil => Result.ok msgs -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: +/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: Source: 'src/betree.rs', lines 653:4-656:32 -/ divergent def betree.Node.lookup_mut_in_bindings (key : U64) (bindings : betree.List (U64 × U64)) : @@ -466,7 +466,7 @@ divergent def betree.Node.lookup_mut_in_bindings Result.ok (l, back) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: +/- [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: Source: 'src/betree.rs', lines 460:4-460:87 -/ def betree.Node.apply_to_leaf (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message) @@ -506,7 +506,7 @@ def betree.Node.apply_to_leaf let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) lookup_mut_in_bindings_back bindings2 -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 -/ divergent def betree.Node.apply_messages_to_leaf (bindings : betree.List (U64 × U64)) @@ -521,7 +521,7 @@ divergent def betree.Node.apply_messages_to_leaf betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl | betree.List.Nil => Result.ok bindings -/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: +/- [betree::betree::{betree::betree::Internal#4}::flush]: Source: 'src/betree.rs', lines 410:4-415:26 -/ mutual divergent def betree.Internal.flush (self : betree.Internal) (params : betree.Params) @@ -562,7 +562,7 @@ mutual divergent def betree.Internal.flush Result.ok (st1, (msgs_left, (betree.Internal.mk self.id self.pivot self.left n, node_id_cnt1))) -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: +/- [betree::betree::{betree::betree::Node#5}::apply_messages]: Source: 'src/betree.rs', lines 588:4-593:5 -/ divergent def betree.Node.apply_messages (self : betree.Node) (params : betree.Params) @@ -609,7 +609,7 @@ divergent def betree.Node.apply_messages end -/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: +/- [betree::betree::{betree::betree::Node#5}::apply]: Source: 'src/betree.rs', lines 576:4-582:5 -/ def betree.Node.apply (self : betree.Node) (params : betree.Params) @@ -624,7 +624,7 @@ def betree.Node.apply let (self1, node_id_cnt1) := p Result.ok (st1, (self1, node_id_cnt1)) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: +/- [betree::betree::{betree::betree::BeTree#6}::new]: Source: 'src/betree.rs', lines 849:4-849:60 -/ def betree.BeTree.new (min_flush_size : U64) (split_size : U64) (st : State) : @@ -641,7 +641,7 @@ def betree.BeTree.new root := (betree.Node.Leaf { id := id, size := 0#u64 }) }) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: +/- [betree::betree::{betree::betree::BeTree#6}::apply]: Source: 'src/betree.rs', lines 868:4-868:47 -/ def betree.BeTree.apply (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : @@ -653,7 +653,7 @@ def betree.BeTree.apply let (n, nic) := p Result.ok (st1, { self with node_id_cnt := nic, root := n }) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: +/- [betree::betree::{betree::betree::BeTree#6}::insert]: Source: 'src/betree.rs', lines 874:4-874:52 -/ def betree.BeTree.insert (self : betree.BeTree) (key : U64) (value : U64) (st : State) : @@ -661,7 +661,7 @@ def betree.BeTree.insert := betree.BeTree.apply self key (betree.Message.Insert value) st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: +/- [betree::betree::{betree::betree::BeTree#6}::delete]: Source: 'src/betree.rs', lines 880:4-880:38 -/ def betree.BeTree.delete (self : betree.BeTree) (key : U64) (st : State) : @@ -669,7 +669,7 @@ def betree.BeTree.delete := betree.BeTree.apply self key betree.Message.Delete st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: +/- [betree::betree::{betree::betree::BeTree#6}::upsert]: Source: 'src/betree.rs', lines 886:4-886:59 -/ def betree.BeTree.upsert (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) @@ -678,7 +678,7 @@ def betree.BeTree.upsert := betree.BeTree.apply self key (betree.Message.Upsert upd) st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: +/- [betree::betree::{betree::betree::BeTree#6}::lookup]: Source: 'src/betree.rs', lines 895:4-895:62 -/ def betree.BeTree.lookup (self : betree.BeTree) (key : U64) (st : State) : @@ -688,12 +688,12 @@ def betree.BeTree.lookup let (st1, (o, n)) ← betree.Node.lookup self.root key st Result.ok (st1, (o, { self with root := n })) -/- [betree_main::main]: +/- [betree::main]: Source: 'src/main.rs', lines 4:0-4:9 -/ def main : Result Unit := Result.ok () -/- Unit test for [betree_main::main] -/ +/- Unit test for [betree::main] -/ #assert (main == Result.ok ()) -end betree_main +end betree diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/Betree/FunsExternal.lean index d26177fb..859cbd68 100644 --- a/tests/lean/BetreeMain/FunsExternal.lean +++ b/tests/lean/Betree/FunsExternal.lean @@ -1,30 +1,30 @@ --- [betree_main]: external functions. +-- [betree]: external functions. import Base -import BetreeMain.Types +import Betree.Types open Primitives -open betree_main +open betree -- TODO: fill those bodies -/- [betree_main::betree_utils::load_internal_node] -/ +/- [betree::betree_utils::load_internal_node] -/ def betree_utils.load_internal_node : U64 → State → Result (State × (betree.List (U64 × betree.Message))) := fun _ _ => .fail .panic -/- [betree_main::betree_utils::store_internal_node] -/ +/- [betree::betree_utils::store_internal_node] -/ def betree_utils.store_internal_node : U64 → betree.List (U64 × betree.Message) → State → Result (State × Unit) := fun _ _ _ => .fail .panic -/- [betree_main::betree_utils::load_leaf_node] -/ +/- [betree::betree_utils::load_leaf_node] -/ def betree_utils.load_leaf_node : U64 → State → Result (State × (betree.List (U64 × U64))) := fun _ _ => .fail .panic -/- [betree_main::betree_utils::store_leaf_node] -/ +/- [betree::betree_utils::store_leaf_node] -/ def betree_utils.store_leaf_node : U64 → betree.List (U64 × U64) → State → Result (State × Unit) := fun _ _ _ => .fail .panic diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/Betree/FunsExternal_Template.lean index 0dcce5ca..014f0d83 100644 --- a/tests/lean/BetreeMain/FunsExternal_Template.lean +++ b/tests/lean/Betree/FunsExternal_Template.lean @@ -1,29 +1,29 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: external functions. +-- [betree]: external functions. -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. import Base -import BetreeMain.Types +import Betree.Types open Primitives -open betree_main +open betree -/- [betree_main::betree_utils::load_internal_node]: +/- [betree::betree_utils::load_internal_node]: Source: 'src/betree_utils.rs', lines 98:0-98:63 -/ axiom betree_utils.load_internal_node : U64 → State → Result (State × (betree.List (U64 × betree.Message))) -/- [betree_main::betree_utils::store_internal_node]: +/- [betree::betree_utils::store_internal_node]: Source: 'src/betree_utils.rs', lines 115:0-115:71 -/ axiom betree_utils.store_internal_node : U64 → betree.List (U64 × betree.Message) → State → Result (State × Unit) -/- [betree_main::betree_utils::load_leaf_node]: +/- [betree::betree_utils::load_leaf_node]: Source: 'src/betree_utils.rs', lines 132:0-132:55 -/ axiom betree_utils.load_leaf_node : U64 → State → Result (State × (betree.List (U64 × U64))) -/- [betree_main::betree_utils::store_leaf_node]: +/- [betree::betree_utils::store_leaf_node]: Source: 'src/betree_utils.rs', lines 145:0-145:63 -/ axiom betree_utils.store_leaf_node : U64 → betree.List (U64 × U64) → State → Result (State × Unit) diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/Betree/Types.lean index e79da43f..3b46c00c 100644 --- a/tests/lean/BetreeMain/Types.lean +++ b/tests/lean/Betree/Types.lean @@ -1,31 +1,31 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: type definitions +-- [betree]: type definitions import Base -import BetreeMain.TypesExternal +import Betree.TypesExternal open Primitives -namespace betree_main +namespace betree -/- [betree_main::betree::List] +/- [betree::betree::List] Source: 'src/betree.rs', lines 17:0-17:23 -/ inductive betree.List (T : Type) := | Cons : T → betree.List T → betree.List T | Nil : betree.List T -/- [betree_main::betree::UpsertFunState] +/- [betree::betree::UpsertFunState] Source: 'src/betree.rs', lines 63:0-63:23 -/ inductive betree.UpsertFunState := | Add : U64 → betree.UpsertFunState | Sub : U64 → betree.UpsertFunState -/- [betree_main::betree::Message] +/- [betree::betree::Message] Source: 'src/betree.rs', lines 69:0-69:23 -/ inductive betree.Message := | Insert : U64 → betree.Message | Delete : betree.Message | Upsert : betree.UpsertFunState → betree.Message -/- [betree_main::betree::Leaf] +/- [betree::betree::Leaf] Source: 'src/betree.rs', lines 167:0-167:11 -/ structure betree.Leaf where id : U64 @@ -33,12 +33,12 @@ structure betree.Leaf where mutual -/- [betree_main::betree::Internal] +/- [betree::betree::Internal] Source: 'src/betree.rs', lines 156:0-156:15 -/ inductive betree.Internal := | mk : U64 → U64 → betree.Node → betree.Node → betree.Internal -/- [betree_main::betree::Node] +/- [betree::betree::Node] Source: 'src/betree.rs', lines 179:0-179:9 -/ inductive betree.Node := | Internal : betree.Internal → betree.Node @@ -62,22 +62,22 @@ def betree.Internal.left (x : betree.Internal) := def betree.Internal.right (x : betree.Internal) := match x with | betree.Internal.mk _ _ _ x1 => x1 -/- [betree_main::betree::Params] +/- [betree::betree::Params] Source: 'src/betree.rs', lines 187:0-187:13 -/ structure betree.Params where min_flush_size : U64 split_size : U64 -/- [betree_main::betree::NodeIdCounter] +/- [betree::betree::NodeIdCounter] Source: 'src/betree.rs', lines 201:0-201:20 -/ structure betree.NodeIdCounter where next_node_id : U64 -/- [betree_main::betree::BeTree] +/- [betree::betree::BeTree] Source: 'src/betree.rs', lines 218:0-218:17 -/ structure betree.BeTree where params : betree.Params node_id_cnt : betree.NodeIdCounter root : betree.Node -end betree_main +end betree diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/Betree/TypesExternal.lean index 1701eaaf..34170271 100644 --- a/tests/lean/BetreeMain/TypesExternal.lean +++ b/tests/lean/Betree/TypesExternal.lean @@ -1,4 +1,4 @@ --- [betree_main]: external types. +-- [betree]: external types. import Base open Primitives diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/Betree/TypesExternal_Template.lean index bbac7e99..12fce657 100644 --- a/tests/lean/BetreeMain/TypesExternal_Template.lean +++ b/tests/lean/Betree/TypesExternal_Template.lean @@ -1,5 +1,5 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: external types. +-- [betree]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. import Base open Primitives diff --git a/tests/lean/BetreeMain.lean b/tests/lean/BetreeMain.lean deleted file mode 100644 index 5f307877..00000000 --- a/tests/lean/BetreeMain.lean +++ /dev/null @@ -1 +0,0 @@ -import BetreeMain.Funs diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean index bb13ddf2..ba336a4a 100644 --- a/tests/lean/lakefile.lean +++ b/tests/lean/lakefile.lean @@ -9,7 +9,7 @@ require base from "../../backends/lean" package «tests» {} @[default_target] lean_lib Tutorial -@[default_target] lean_lib BetreeMain +@[default_target] lean_lib Betree @[default_target] lean_lib Constants @[default_target] lean_lib External @[default_target] lean_lib Hashmap diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 1c885d4b..a7b83e88 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -122,8 +122,7 @@ let aeneas_options_for_test backend test_name = (* File-specific options *) let charon_options_for_test test_name = match test_name with - | "betree" -> - [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] + | "betree" -> [ "--polonius"; "--opaque=betree_utils" ] | _ -> [] (* The data for a specific test input *) @@ -257,10 +256,8 @@ end (* Run Aeneas on a specific input with the given options *) let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) = - (* FIXME: remove this special case *) let backend_str = Backend.to_string backend in - let test_name = if case.name = "betree" then "betree_main" else case.name in - let input_file = concat_path [ env.llbc_dir; test_name ] ^ ".llbc" in + let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in let output_file = Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out" in |