diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/arrays/Arrays.v | 21 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 8 | ||||
| -rw-r--r-- | tests/coq/betree/_CoqProject | 2 | ||||
| -rw-r--r-- | tests/coq/demo/Demo.v | 2 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 4 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 8 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/_CoqProject | 2 | ||||
| -rw-r--r-- | tests/coq/misc/Loops.v | 39 | ||||
| -rw-r--r-- | tests/coq/misc/_CoqProject | 4 |
9 files changed, 26 insertions, 64 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v index 34d163b7..580e72f0 100644 --- a/tests/coq/arrays/Arrays.v +++ b/tests/coq/arrays/Arrays.v @@ -30,9 +30,7 @@ Definition array_to_mut_slice_ (T : Type) (s : array T 32%usize) : result ((slice T) * (slice T -> result (array T 32%usize))) := - p <- array_to_slice_mut T 32%usize s; - let (s1, to_slice_mut_back) := p in - Return (s1, to_slice_mut_back) + array_to_slice_mut T 32%usize s . (** [arrays::array_len]: @@ -78,9 +76,7 @@ Definition index_mut_array (T : Type) (s : array T 32%usize) (i : usize) : result (T * (T -> result (array T 32%usize))) := - p <- array_index_mut_usize T 32%usize s i; - let (t, index_mut_back) := p in - Return (t, index_mut_back) + array_index_mut_usize T 32%usize s i . (** [arrays::index_slice]: @@ -95,9 +91,7 @@ Definition index_mut_slice (T : Type) (s : slice T) (i : usize) : result (T * (T -> result (slice T))) := - p <- slice_index_mut_usize T s i; - let (t, index_mut_back) := p in - Return (t, index_mut_back) + slice_index_mut_usize T s i . (** [arrays::slice_subslice_shared_]: @@ -136,9 +130,7 @@ Definition array_to_slice_mut_ (x : array u32 32%usize) : result ((slice u32) * (slice u32 -> result (array u32 32%usize))) := - p <- array_to_slice_mut u32 32%usize x; - let (s, to_slice_mut_back) := p in - Return (s, to_slice_mut_back) + array_to_slice_mut u32 32%usize x . (** [arrays::array_subslice_shared_]: @@ -381,7 +373,7 @@ Definition take_array_t (a : array AB_t 2%usize) : result unit := (** [arrays::non_copyable_array]: Source: 'src/arrays.rs', lines 229:0-229:27 *) Definition non_copyable_array : result unit := - _ <- take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]); Return tt + take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]) . (** [arrays::sum]: loop 0: @@ -548,8 +540,7 @@ Fixpoint iter_mut_slice_loop | O => Fail_ OutOfFuel | S n1 => if i s< len - then ( - i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt) + then (i1 <- usize_add i 1%usize; iter_mut_slice_loop n1 len i1) else Return tt end . diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 3863a90f..a0338557 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -27,9 +27,7 @@ Definition betree_store_internal_node (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) : result (state * unit) := - p <- betree_utils_store_internal_node id content st; - let (st1, _) := p in - Return (st1, tt) + betree_utils_store_internal_node id content st . (** [betree_main::betree::load_leaf_node]: @@ -45,9 +43,7 @@ Definition betree_store_leaf_node (id : u64) (content : betree_List_t (u64 * u64)) (st : state) : result (state * unit) := - p <- betree_utils_store_leaf_node id content st; - let (st1, _) := p in - Return (st1, tt) + betree_utils_store_leaf_node id content st . (** [betree_main::betree::fresh_node_id]: diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject index 13e4b9c1..b14bed66 100644 --- a/tests/coq/betree/_CoqProject +++ b/tests/coq/betree/_CoqProject @@ -3,8 +3,8 @@ -arg -w -arg all -BetreeMain_Types.v BetreeMain_TypesExternal_Template.v +BetreeMain_Types.v Primitives.v BetreeMain_FunsExternal_Template.v BetreeMain_Funs.v diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index 48067c02..2fccf6c0 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -127,7 +127,7 @@ Definition list_nth_mut1 (T : Type) (n : nat) (l : CList_t T) (i : u32) : result (T * (T -> result (CList_t T))) := - p <- list_nth_mut1_loop T n l i; let (t, back_'a) := p in Return (t, back_'a) + list_nth_mut1_loop T n l i . (** [demo::i32_id]: diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 0478edbe..ab424e42 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -398,9 +398,7 @@ Definition hashMap_get_mut_in_list (T : Type) (n : nat) (ls : List_t T) (key : usize) : result (T * (T -> result (List_t T))) := - p <- hashMap_get_mut_in_list_loop T n ls key; - let (t, back_'a) := p in - Return (t, back_'a) + hashMap_get_mut_in_list_loop T n ls key . (** [hashmap::{hashmap::HashMap<T>}::get_mut]: diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 6a7eeb2d..aff4995f 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -423,9 +423,7 @@ Definition hashmap_HashMap_get_mut_in_list (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) : result (T * (T -> result (hashmap_List_t T))) := - p <- hashmap_HashMap_get_mut_in_list_loop T n ls key; - let (t, back_'a) := p in - Return (t, back_'a) + hashmap_HashMap_get_mut_in_list_loop T n ls key . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: @@ -585,9 +583,7 @@ Definition insert_on_disk p <- hashmap_utils_deserialize st; let (st1, hm) := p in hm1 <- hashmap_HashMap_insert u64 n hm key value; - p1 <- hashmap_utils_serialize hm1 st1; - let (st2, _) := p1 in - Return (st2, tt) + hashmap_utils_serialize hm1 st1 . (** [hashmap_main::main]: diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject index 41945494..d73541d9 100644 --- a/tests/coq/hashmap_on_disk/_CoqProject +++ b/tests/coq/hashmap_on_disk/_CoqProject @@ -4,9 +4,9 @@ -arg all HashmapMain_Types.v +HashmapMain_FunsExternal_Template.v Primitives.v HashmapMain_Funs.v HashmapMain_TypesExternal.v -HashmapMain_FunsExternal_Template.v HashmapMain_FunsExternal.v HashmapMain_TypesExternal_Template.v diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index e235b60d..85b54510 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -183,7 +183,7 @@ Definition list_nth_mut_loop (T : Type) (n : nat) (ls : List_t T) (i : u32) : result (T * (T -> result (List_t T))) := - p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back) + list_nth_mut_loop_loop T n ls i . (** [loops::list_nth_shared_loop]: loop 0: @@ -400,9 +400,7 @@ Definition list_nth_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T))) := - t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i; - let '(p, back_'a, back_'b) := t in - Return (p, back_'a, back_'b) + list_nth_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_shared_loop_pair]: loop 0: @@ -481,9 +479,7 @@ Definition list_nth_mut_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T)))) := - p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_shared_loop_pair_merge]: loop 0: @@ -557,9 +553,7 @@ Definition list_nth_mut_shared_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: @@ -599,9 +593,7 @@ Definition list_nth_mut_shared_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair]: loop 0: @@ -641,9 +633,7 @@ Definition list_nth_shared_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i; - let (p1, back_'b) := p in - Return (p1, back_'b) + list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: @@ -683,9 +673,7 @@ Definition list_nth_shared_mut_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::ignore_input_mut_borrow]: loop 0: @@ -695,8 +683,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | O => Fail_ OutOfFuel | S n1 => if i s> 0%u32 - then ( - i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt) + then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1) else Return tt end . @@ -715,10 +702,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | O => Fail_ OutOfFuel | S n1 => if i s> 0%u32 - then ( - i1 <- u32_sub i 1%u32; - _ <- incr_ignore_input_mut_borrow_loop n1 i1; - Return tt) + then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1) else Return tt end . @@ -737,10 +721,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit := | O => Fail_ OutOfFuel | S n1 => if i s> 0%u32 - then ( - i1 <- u32_sub i 1%u32; - _ <- ignore_input_shared_borrow_loop n1 i1; - Return tt) + then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1) else Return tt end . diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index 869cdb4d..308de4f4 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -3,6 +3,7 @@ -arg -w -arg all +External_FunsExternal_Template.v Loops.v External_Types.v Primitives.v @@ -10,9 +11,8 @@ External_Funs.v External_TypesExternal.v Constants.v PoloniusList.v -Paper.v NoNestedBorrows.v External_FunsExternal.v Bitwise.v External_TypesExternal_Template.v -External_FunsExternal_Template.v +Paper.v |