diff options
author | Son Ho | 2022-11-15 15:25:47 +0100 |
---|---|---|
committer | Son HO | 2022-11-16 15:45:32 +0100 |
commit | fa6dcd3ebbdc7a508157ff2a12f91e70d2012a86 (patch) | |
tree | b72055ef976459079c0f1352a3928bd8a1481f76 /tests | |
parent | bd5706896dec0a1aef1accdf51f93af00c5dc6fe (diff) |
Change the name of the generated Coq modules
Diffstat (limited to 'tests')
-rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v (renamed from tests/coq/betree/BetreeMain__Funs.v) | 12 | ||||
-rw-r--r-- | tests/coq/betree/BetreeMain_Opaque.v (renamed from tests/coq/betree/BetreeMain__Opaque.v) | 8 | ||||
-rw-r--r-- | tests/coq/betree/BetreeMain_Types.v (renamed from tests/coq/betree/BetreeMain__Types.v) | 4 | ||||
-rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v (renamed from tests/coq/hashmap/Hashmap__Funs.v) | 8 | ||||
-rw-r--r-- | tests/coq/hashmap/Hashmap_Types.v (renamed from tests/coq/hashmap/Hashmap__Types.v) | 4 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v (renamed from tests/coq/hashmap_on_disk/HashmapMain__Funs.v) | 12 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Opaque.v (renamed from tests/coq/hashmap_on_disk/HashmapMain__Opaque.v) | 8 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Types.v (renamed from tests/coq/hashmap_on_disk/HashmapMain__Types.v) | 4 | ||||
-rw-r--r-- | tests/coq/misc/External_Funs.v (renamed from tests/coq/misc/External__Funs.v) | 12 | ||||
-rw-r--r-- | tests/coq/misc/External_Opaque.v (renamed from tests/coq/misc/External__Opaque.v) | 8 | ||||
-rw-r--r-- | tests/coq/misc/External_Types.v (renamed from tests/coq/misc/External__Types.v) | 4 |
11 files changed, 42 insertions, 42 deletions
diff --git a/tests/coq/betree/BetreeMain__Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 3ce86f6b..3129614c 100644 --- a/tests/coq/betree/BetreeMain__Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -4,11 +4,11 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export BetreeMain__Types. -Import BetreeMain__Types. -Require Export BetreeMain__Opaque. -Import BetreeMain__Opaque. -Module BetreeMain__Funs. +Require Export BetreeMain_Types. +Import BetreeMain_Types. +Require Export BetreeMain_Opaque. +Import BetreeMain_Opaque. +Module BetreeMain_Funs. (** [betree_main::betree::load_internal_node] *) Definition betree_load_internal_node_fwd @@ -1394,4 +1394,4 @@ Definition betree_be_tree_lookup_back (** [betree_main::main] *) Definition main_fwd : result unit := Return tt. -End BetreeMain__Funs . +End BetreeMain_Funs . diff --git a/tests/coq/betree/BetreeMain__Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v index cbd8cfb3..08ab530a 100644 --- a/tests/coq/betree/BetreeMain__Opaque.v +++ b/tests/coq/betree/BetreeMain_Opaque.v @@ -4,9 +4,9 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export BetreeMain__Types. -Import BetreeMain__Types. -Module BetreeMain__Opaque. +Require Export BetreeMain_Types. +Import BetreeMain_Types. +Module BetreeMain_Opaque. (** [betree_main::betree_utils::load_internal_node] *) Axiom betree_utils_load_internal_node_fwd @@ -35,4 +35,4 @@ Axiom core_option_option_unwrap_fwd : forall(T : Type), option T -> state -> result (state * T) . -End BetreeMain__Opaque . +End BetreeMain_Opaque . diff --git a/tests/coq/betree/BetreeMain__Types.v b/tests/coq/betree/BetreeMain_Types.v index 2ed0d324..672b2ebd 100644 --- a/tests/coq/betree/BetreeMain__Types.v +++ b/tests/coq/betree/BetreeMain_Types.v @@ -4,7 +4,7 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Module BetreeMain__Types. +Module BetreeMain_Types. (** [betree_main::betree::List] *) Inductive Betree_list_t (T : Type) := @@ -82,4 +82,4 @@ Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global. (** The state type used in the state-error monad *) Axiom state : Type. -End BetreeMain__Types . +End BetreeMain_Types . diff --git a/tests/coq/hashmap/Hashmap__Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 7d897c8a..912b7fe2 100644 --- a/tests/coq/hashmap/Hashmap__Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -4,9 +4,9 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export Hashmap__Types. -Import Hashmap__Types. -Module Hashmap__Funs. +Require Export Hashmap_Types. +Import Hashmap_Types. +Module Hashmap_Funs. (** [hashmap::hash_key] *) Definition hash_key_fwd (k : usize) : result usize := Return k. @@ -538,4 +538,4 @@ Definition test1_fwd (n : nat) : result unit := end . -End Hashmap__Funs . +End Hashmap_Funs . diff --git a/tests/coq/hashmap/Hashmap__Types.v b/tests/coq/hashmap/Hashmap_Types.v index e1add060..a3b68f9a 100644 --- a/tests/coq/hashmap/Hashmap__Types.v +++ b/tests/coq/hashmap/Hashmap_Types.v @@ -4,7 +4,7 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Module Hashmap__Types. +Module Hashmap_Types. (** [hashmap::List] *) Inductive List_t (T : Type) := @@ -35,4 +35,4 @@ Arguments Hash_map_slots {T}. Definition core_num_u32_max_body : result u32 := Return (4294967295%u32). Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. -End Hashmap__Types . +End Hashmap_Types . diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 249adbe9..b4351dc3 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain__Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -4,11 +4,11 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export HashmapMain__Types. -Import HashmapMain__Types. -Require Export HashmapMain__Opaque. -Import HashmapMain__Opaque. -Module HashmapMain__Funs. +Require Export HashmapMain_Types. +Import HashmapMain_Types. +Require Export HashmapMain_Opaque. +Import HashmapMain_Opaque. +Module HashmapMain_Funs. (** [hashmap_main::hashmap::hash_key] *) Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k. @@ -595,4 +595,4 @@ Definition main_fwd : result unit := Return tt. (** Unit test for [hashmap_main::main] *) Check (main_fwd )%return. -End HashmapMain__Funs . +End HashmapMain_Funs . diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v index 4b6db927..6152b94b 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain__Opaque.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v @@ -4,9 +4,9 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export HashmapMain__Types. -Import HashmapMain__Types. -Module HashmapMain__Opaque. +Require Export HashmapMain_Types. +Import HashmapMain_Types. +Module HashmapMain_Opaque. (** [hashmap_main::hashmap_utils::deserialize] *) Axiom hashmap_utils_deserialize_fwd @@ -18,4 +18,4 @@ Axiom hashmap_utils_serialize_fwd : Hashmap_hash_map_t u64 -> state -> result (state * unit) . -End HashmapMain__Opaque . +End HashmapMain_Opaque . diff --git a/tests/coq/hashmap_on_disk/HashmapMain__Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v index 5d609937..01243baf 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain__Types.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v @@ -4,7 +4,7 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Module HashmapMain__Types. +Module HashmapMain_Types. (** [hashmap_main::hashmap::List] *) Inductive Hashmap_list_t (T : Type) := @@ -38,4 +38,4 @@ Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global. (** The state type used in the state-error monad *) Axiom state : Type. -End HashmapMain__Types . +End HashmapMain_Types . diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External_Funs.v index e7020040..3ddc1cf3 100644 --- a/tests/coq/misc/External__Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -4,11 +4,11 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export External__Types. -Import External__Types. -Require Export External__Opaque. -Import External__Opaque. -Module External__Funs. +Require Export External_Types. +Import External_Types. +Require Export External_Opaque. +Import External_Opaque. +Module External_Funs. (** [external::swap] *) Definition swap_fwd @@ -111,4 +111,4 @@ Definition test_swap_non_zero_fwd if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0) . -End External__Funs . +End External_Funs . diff --git a/tests/coq/misc/External__Opaque.v b/tests/coq/misc/External_Opaque.v index 93652450..d60251e0 100644 --- a/tests/coq/misc/External__Opaque.v +++ b/tests/coq/misc/External_Opaque.v @@ -4,9 +4,9 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export External__Types. -Import External__Types. -Module External__Opaque. +Require Export External_Types. +Import External_Types. +Module External_Opaque. (** [core::mem::swap] *) Axiom core_mem_swap_fwd : @@ -33,4 +33,4 @@ Axiom core_option_option_unwrap_fwd : forall(T : Type), option T -> state -> result (state * T) . -End External__Opaque . +End External_Opaque . diff --git a/tests/coq/misc/External__Types.v b/tests/coq/misc/External_Types.v index f4f74272..cec5b88e 100644 --- a/tests/coq/misc/External__Types.v +++ b/tests/coq/misc/External_Types.v @@ -4,7 +4,7 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Module External__Types. +Module External_Types. (** [core::num::nonzero::NonZeroU32] *) Axiom Core_num_nonzero_non_zero_u32_t : Type. @@ -12,4 +12,4 @@ Axiom Core_num_nonzero_non_zero_u32_t : Type. (** The state type used in the state-error monad *) Axiom state : Type. -End External__Types . +End External_Types . |