diff options
Diffstat (limited to 'tests/coq')
| -rw-r--r-- | tests/coq/arrays/Arrays.v | 31 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 148 | ||||
| -rw-r--r-- | tests/coq/betree/_CoqProject | 2 | ||||
| -rw-r--r-- | tests/coq/demo/Demo.v | 50 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 30 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 36 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/_CoqProject | 2 | ||||
| -rw-r--r-- | tests/coq/misc/External_Funs.v | 6 | ||||
| -rw-r--r-- | tests/coq/misc/Loops.v | 61 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 9 | ||||
| -rw-r--r-- | tests/coq/misc/Paper.v | 2 | ||||
| -rw-r--r-- | tests/coq/misc/_CoqProject | 4 |
12 files changed, 182 insertions, 199 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v index 34d163b7..049d63cb 100644 --- a/tests/coq/arrays/Arrays.v +++ b/tests/coq/arrays/Arrays.v @@ -30,27 +30,25 @@ 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]: Source: 'src/arrays.rs', lines 25:0-25:40 *) Definition array_len (T : Type) (s : array T 32%usize) : result usize := - s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i + s1 <- array_to_slice T 32%usize s; Return (slice_len T s1) . (** [arrays::shared_array_len]: Source: 'src/arrays.rs', lines 29:0-29:48 *) Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize := - s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i + s1 <- array_to_slice T 32%usize s; Return (slice_len T s1) . (** [arrays::shared_slice_len]: Source: 'src/arrays.rs', lines 33:0-33:44 *) Definition shared_slice_len (T : Type) (s : slice T) : result usize := - let i := slice_len T s in Return i + Return (slice_len T s) . (** [arrays::index_array_shared]: @@ -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_]: @@ -334,8 +326,8 @@ Definition update_mut_slice (x : slice u32) : result (slice u32) := Definition update_all : result unit := _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - a <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]); - p <- array_to_slice_mut u32 2%usize a; + x <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + p <- array_to_slice_mut u32 2%usize x; let (s, to_slice_mut_back) := p in s1 <- update_mut_slice s; _ <- to_slice_mut_back s1; @@ -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..c2cca26d 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]: @@ -205,9 +201,9 @@ Definition betree_Leaf_split p1 <- betree_List_hd (u64 * u64) content1; let (pivot, _) := p1 in p2 <- betree_NodeIdCounter_fresh_id node_id_cnt; - let (id0, nic) := p2 in - p3 <- betree_NodeIdCounter_fresh_id nic; - let (id1, nic1) := p3 in + let (id0, node_id_cnt1) := p2 in + p3 <- betree_NodeIdCounter_fresh_id node_id_cnt1; + let (id1, node_id_cnt2) := p3 in p4 <- betree_store_leaf_node id0 content0 st; let (st1, _) := p4 in p5 <- betree_store_leaf_node id1 content1 st1; @@ -222,7 +218,8 @@ Definition betree_Leaf_split betree_Leaf_id := id1; betree_Leaf_size := params.(betree_Params_split_size) |} in - Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, nic1)) + Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, + node_id_cnt2)) . (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: @@ -290,22 +287,22 @@ Fixpoint betree_Node_apply_upserts if b then ( p <- betree_List_pop_front (u64 * betree_Message_t) msgs; - let (msg, l) := p in + let (msg, msgs1) := p in let (_, m) := msg in match m with | Betree_Message_Insert _ => Fail_ Failure | Betree_Message_Delete => Fail_ Failure | Betree_Message_Upsert s => v <- betree_upsert_update prev s; - betree_Node_apply_upserts n1 l (Some v) key st + betree_Node_apply_upserts n1 msgs1 (Some v) key st end) else ( p <- core_option_Option_unwrap u64 prev st; let (st1, v) := p in - l <- + msgs1 <- betree_List_push_front (u64 * betree_Message_t) msgs (key, Betree_Message_Insert v); - Return (st1, (v, l))) + Return (st1, (v, msgs1))) end . @@ -355,9 +352,9 @@ with betree_Node_lookup then ( p3 <- betree_Internal_lookup_in_children n1 node key st1; let (st2, p4) := p3 in - let (o, i) := p4 in + let (o, node1) := p4 in _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l); - Return (st2, (o, Betree_Node_Internal i))) + Return (st2, (o, Betree_Node_Internal node1))) else match msg with | Betree_Message_Insert v => @@ -373,23 +370,24 @@ with betree_Node_lookup | Betree_Message_Upsert ufs => p3 <- betree_Internal_lookup_in_children n1 node key st1; let (st2, p4) := p3 in - let (v, i) := p4 in + let (v, node1) := p4 in p5 <- betree_Node_apply_upserts n1 (Betree_List_Cons (k, Betree_Message_Upsert ufs) l) v key st2; let (st3, p6) := p5 in - let (v1, l1) := p6 in - msgs1 <- lookup_first_message_for_key_back l1; - p7 <- betree_store_internal_node i.(betree_Internal_id) msgs1 st3; + let (v1, pending1) := p6 in + msgs1 <- lookup_first_message_for_key_back pending1; + p7 <- + betree_store_internal_node node1.(betree_Internal_id) msgs1 st3; let (st4, _) := p7 in - Return (st4, (Some v1, Betree_Node_Internal i)) + Return (st4, (Some v1, Betree_Node_Internal node1)) end | Betree_List_Nil => p2 <- betree_Internal_lookup_in_children n1 node key st1; let (st2, p3) := p2 in - let (o, i) := p3 in + let (o, node1) := p3 in _ <- lookup_first_message_for_key_back Betree_List_Nil; - Return (st2, (o, Betree_Node_Internal i)) + Return (st2, (o, Betree_Node_Internal node1)) end | Betree_Node_Leaf node => p <- betree_load_leaf_node node.(betree_Leaf_id) st; @@ -417,8 +415,8 @@ Fixpoint betree_Node_filter_messages_for_key p1 <- betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k, m) l); - let (_, l1) := p1 in - betree_Node_filter_messages_for_key n1 key l1) + let (_, msgs1) := p1 in + betree_Node_filter_messages_for_key n1 key msgs1) else Return (Betree_List_Cons (k, m) l) | Betree_List_Nil => Return Betree_List_Nil end @@ -467,17 +465,17 @@ Definition betree_Node_apply_to_internal then match new_msg with | Betree_Message_Insert i => - l <- betree_Node_filter_messages_for_key n key msgs1; - l1 <- - betree_List_push_front (u64 * betree_Message_t) l (key, + msgs2 <- betree_Node_filter_messages_for_key n key msgs1; + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Insert i); - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete => - l <- betree_Node_filter_messages_for_key n key msgs1; - l1 <- - betree_List_push_front (u64 * betree_Message_t) l (key, + msgs2 <- betree_Node_filter_messages_for_key n key msgs1; + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Delete); - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert s => p1 <- betree_List_hd (u64 * betree_Message_t) msgs1; let (_, m) := p1 in @@ -485,32 +483,33 @@ Definition betree_Node_apply_to_internal | Betree_Message_Insert prev => v <- betree_upsert_update (Some prev) s; p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; - let (_, l) := p2 in - l1 <- - betree_List_push_front (u64 * betree_Message_t) l (key, + let (_, msgs2) := p2 in + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Insert v); - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Delete => p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; - let (_, l) := p2 in + let (_, msgs2) := p2 in v <- betree_upsert_update None s; - l1 <- - betree_List_push_front (u64 * betree_Message_t) l (key, + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Insert v); - lookup_first_message_for_key_back l1 + lookup_first_message_for_key_back msgs3 | Betree_Message_Upsert _ => p2 <- betree_Node_lookup_first_message_after_key n key msgs1; let (msgs2, lookup_first_message_after_key_back) := p2 in - l <- + msgs3 <- betree_List_push_front (u64 * betree_Message_t) msgs2 (key, Betree_Message_Upsert s); - msgs3 <- lookup_first_message_after_key_back l; - lookup_first_message_for_key_back msgs3 + msgs4 <- lookup_first_message_after_key_back msgs3; + lookup_first_message_for_key_back msgs4 end end else ( - l <- betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg); - lookup_first_message_for_key_back l) + msgs2 <- + betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg); + lookup_first_message_for_key_back msgs2) . (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: @@ -526,8 +525,8 @@ Fixpoint betree_Node_apply_messages_to_internal match new_msgs with | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in - l <- betree_Node_apply_to_internal n1 msgs i m; - betree_Node_apply_messages_to_internal n1 l new_msgs_tl + msgs1 <- betree_Node_apply_to_internal n1 msgs i m; + betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl | Betree_List_Nil => Return msgs end end @@ -574,28 +573,28 @@ Definition betree_Node_apply_to_leaf if b then ( p1 <- betree_List_pop_front (u64 * u64) bindings1; - let (hd, l) := p1 in + let (hd, bindings2) := p1 in match new_msg with | Betree_Message_Insert v => - l1 <- betree_List_push_front (u64 * u64) l (key, v); - lookup_mut_in_bindings_back l1 - | Betree_Message_Delete => lookup_mut_in_bindings_back l + bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v); + lookup_mut_in_bindings_back bindings3 + | Betree_Message_Delete => lookup_mut_in_bindings_back bindings2 | Betree_Message_Upsert s => let (_, i) := hd in v <- betree_upsert_update (Some i) s; - l1 <- betree_List_push_front (u64 * u64) l (key, v); - lookup_mut_in_bindings_back l1 + bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v); + lookup_mut_in_bindings_back bindings3 end) else match new_msg with | Betree_Message_Insert v => - l <- betree_List_push_front (u64 * u64) bindings1 (key, v); - lookup_mut_in_bindings_back l + bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); + lookup_mut_in_bindings_back bindings2 | Betree_Message_Delete => lookup_mut_in_bindings_back bindings1 | Betree_Message_Upsert s => v <- betree_upsert_update None s; - l <- betree_List_push_front (u64 * u64) bindings1 (key, v); - lookup_mut_in_bindings_back l + bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); + lookup_mut_in_bindings_back bindings2 end . @@ -612,8 +611,8 @@ Fixpoint betree_Node_apply_messages_to_leaf match new_msgs with | Betree_List_Cons new_msg new_msgs_tl => let (i, m) := new_msg in - l <- betree_Node_apply_to_leaf n1 bindings i m; - betree_Node_apply_messages_to_leaf n1 l new_msgs_tl + bindings1 <- betree_Node_apply_to_leaf n1 bindings i m; + betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl | Betree_List_Nil => Return bindings end end @@ -684,38 +683,39 @@ with betree_Node_apply_messages | Betree_Node_Internal node => p <- betree_load_internal_node node.(betree_Internal_id) st; let (st1, content) := p in - l <- betree_Node_apply_messages_to_internal n1 content msgs; - num_msgs <- betree_List_len (u64 * betree_Message_t) n1 l; + content1 <- betree_Node_apply_messages_to_internal n1 content msgs; + num_msgs <- betree_List_len (u64 * betree_Message_t) n1 content1; if num_msgs s>= params.(betree_Params_min_flush_size) then ( - p1 <- betree_Internal_flush n1 node params node_id_cnt l st1; + p1 <- betree_Internal_flush n1 node params node_id_cnt content1 st1; let (st2, p2) := p1 in - let (content1, p3) := p2 in + let (content2, p3) := p2 in let (node1, node_id_cnt1) := p3 in p4 <- - betree_store_internal_node node1.(betree_Internal_id) content1 st2; + betree_store_internal_node node1.(betree_Internal_id) content2 st2; let (st3, _) := p4 in Return (st3, (Betree_Node_Internal node1, node_id_cnt1))) else ( - p1 <- betree_store_internal_node node.(betree_Internal_id) l st1; + p1 <- + betree_store_internal_node node.(betree_Internal_id) content1 st1; let (st2, _) := p1 in Return (st2, (Betree_Node_Internal node, node_id_cnt))) | Betree_Node_Leaf node => p <- betree_load_leaf_node node.(betree_Leaf_id) st; let (st1, content) := p in - l <- betree_Node_apply_messages_to_leaf n1 content msgs; - len <- betree_List_len (u64 * u64) n1 l; + content1 <- betree_Node_apply_messages_to_leaf n1 content msgs; + len <- betree_List_len (u64 * u64) n1 content1; i <- u64_mul 2%u64 params.(betree_Params_split_size); if len s>= i then ( - p1 <- betree_Leaf_split n1 node l params node_id_cnt st1; + p1 <- betree_Leaf_split n1 node content1 params node_id_cnt st1; let (st2, p2) := p1 in - let (new_node, nic) := p2 in + let (new_node, node_id_cnt1) := p2 in p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2; let (st3, _) := p3 in - Return (st3, (Betree_Node_Internal new_node, nic))) + Return (st3, (Betree_Node_Internal new_node, node_id_cnt1))) else ( - p1 <- betree_store_leaf_node node.(betree_Leaf_id) l st1; + p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1; let (st2, _) := p1 in Return (st2, (Betree_Node_Leaf {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len @@ -748,7 +748,7 @@ Definition betree_BeTree_new := node_id_cnt <- betree_NodeIdCounter_new; p <- betree_NodeIdCounter_fresh_id node_id_cnt; - let (id, nic) := p in + let (id, node_id_cnt1) := p in p1 <- betree_store_leaf_node id Betree_List_Nil st; let (st1, _) := p1 in Return (st1, @@ -758,7 +758,7 @@ Definition betree_BeTree_new betree_Params_min_flush_size := min_flush_size; betree_Params_split_size := split_size |}; - betree_BeTree_node_id_cnt := nic; + betree_BeTree_node_id_cnt := node_id_cnt1; betree_BeTree_root := (Betree_Node_Leaf {| betree_Leaf_id := id; betree_Leaf_size := 0%u64 |}) 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 ec7ca29d..d5a6e535 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -34,8 +34,14 @@ Definition use_mul2_add1 (x : u32) (y : u32) : result u32 := Definition incr (x : u32) : result u32 := u32_add x 1%u32. +(** [demo::use_incr]: + Source: 'src/demo.rs', lines 25:0-25:17 *) +Definition use_incr : result unit := + x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Return tt +. + (** [demo::CList] - Source: 'src/demo.rs', lines 27:0-27:17 *) + Source: 'src/demo.rs', lines 34:0-34:17 *) Inductive CList_t (T : Type) := | CList_CCons : T -> CList_t T -> CList_t T | CList_CNil : CList_t T @@ -45,7 +51,7 @@ Arguments CList_CCons { _ }. Arguments CList_CNil { _ }. (** [demo::list_nth]: - Source: 'src/demo.rs', lines 32:0-32:56 *) + Source: 'src/demo.rs', lines 39:0-39:56 *) Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T := match n with | O => Fail_ OutOfFuel @@ -61,7 +67,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T := . (** [demo::list_nth_mut]: - Source: 'src/demo.rs', lines 47:0-47:68 *) + Source: 'src/demo.rs', lines 54:0-54:68 *) Fixpoint list_nth_mut (T : Type) (n : nat) (l : CList_t T) (i : u32) : result (T * (T -> result (CList_t T))) @@ -89,7 +95,7 @@ Fixpoint list_nth_mut . (** [demo::list_nth_mut1]: loop 0: - Source: 'src/demo.rs', lines 62:0-71:1 *) + Source: 'src/demo.rs', lines 69:0-78:1 *) Fixpoint list_nth_mut1_loop (T : Type) (n : nat) (l : CList_t T) (i : u32) : result (T * (T -> result (CList_t T))) @@ -116,16 +122,16 @@ Fixpoint list_nth_mut1_loop . (** [demo::list_nth_mut1]: - Source: 'src/demo.rs', lines 62:0-62:77 *) + Source: 'src/demo.rs', lines 69:0-69:77 *) 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]: - Source: 'src/demo.rs', lines 73:0-73:28 *) + Source: 'src/demo.rs', lines 80:0-80:28 *) Fixpoint i32_id (n : nat) (i : i32) : result i32 := match n with | O => Fail_ OutOfFuel @@ -136,8 +142,30 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 := end . +(** [demo::list_tail]: + Source: 'src/demo.rs', lines 88:0-88:64 *) +Fixpoint list_tail + (T : Type) (n : nat) (l : CList_t T) : + result ((CList_t T) * (CList_t T -> result (CList_t T))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match l with + | CList_CCons t tl => + p <- list_tail T n1 tl; + let (c, list_tail_back) := p in + let back_'a := + fun (ret : CList_t T) => + tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in + Return (c, back_'a) + | CList_CNil => Return (CList_CNil, Return) + end + end +. + (** Trait declaration: [demo::Counter] - Source: 'src/demo.rs', lines 83:0-83:17 *) + Source: 'src/demo.rs', lines 97:0-97:17 *) Record Counter_t (Self : Type) := mkCounter_t { Counter_t_incr : Self -> result (usize * Self); }. @@ -146,19 +174,19 @@ Arguments mkCounter_t { _ }. Arguments Counter_t_incr { _ }. (** [demo::{(demo::Counter for usize)}::incr]: - Source: 'src/demo.rs', lines 88:4-88:31 *) + Source: 'src/demo.rs', lines 102:4-102:31 *) Definition counterUsize_incr (self : usize) : result (usize * usize) := self1 <- usize_add self 1%usize; Return (self, self1) . (** Trait implementation: [demo::{(demo::Counter for usize)}] - Source: 'src/demo.rs', lines 87:0-87:22 *) + Source: 'src/demo.rs', lines 101:0-101:22 *) Definition CounterUsize : Counter_t usize := {| Counter_t_incr := counterUsize_incr; |}. (** [demo::use_counter]: - Source: 'src/demo.rs', lines 95:0-95:59 *) + Source: 'src/demo.rs', lines 109:0-109:59 *) Definition use_counter (T : Type) (counterInst : Counter_t T) (cnt : T) : result (usize * T) := counterInst.(Counter_t_incr) cnt diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 0478edbe..d709a8d5 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -26,9 +26,9 @@ Fixpoint hashMap_allocate_slots_loop | S n2 => if n1 s> 0%usize then ( - v <- alloc_vec_Vec_push (List_t T) slots List_Nil; + slots1 <- alloc_vec_Vec_push (List_t T) slots List_Nil; n3 <- usize_sub n1 1%usize; - hashMap_allocate_slots_loop T n2 v n3) + hashMap_allocate_slots_loop T n2 slots1 n3) else Return slots end . @@ -190,8 +190,8 @@ Fixpoint hashMap_move_elements_from_list_loop | S n1 => match ls with | List_Cons k v tl => - hm <- hashMap_insert_no_resize T n1 ntable k v; - hashMap_move_elements_from_list_loop T n1 hm tl + ntable1 <- hashMap_insert_no_resize T n1 ntable k v; + hashMap_move_elements_from_list_loop T n1 ntable1 tl | List_Nil => Return ntable end end @@ -224,12 +224,10 @@ Fixpoint hashMap_move_elements_loop (core_slice_index_SliceIndexUsizeSliceTInst (List_t T)) slots i; let (l, index_mut_back) := p in let (ls, l1) := core_mem_replace (List_t T) l List_Nil in - hm <- hashMap_move_elements_from_list T n1 ntable ls; + ntable1 <- hashMap_move_elements_from_list T n1 ntable ls; i2 <- usize_add i 1%usize; slots1 <- index_mut_back l1; - back_'a <- hashMap_move_elements_loop T n1 hm slots1 i2; - let (hm1, v) := back_'a in - Return (hm1, v)) + hashMap_move_elements_loop T n1 ntable1 slots1 i2) else Return (ntable, slots) end . @@ -241,9 +239,7 @@ Definition hashMap_move_elements (slots : alloc_vec_Vec (List_t T)) (i : usize) : result ((HashMap_t T) * (alloc_vec_Vec (List_t T))) := - back_'a <- hashMap_move_elements_loop T n ntable slots i; - let (hm, v) := back_'a in - Return (hm, v) + hashMap_move_elements_loop T n ntable slots i . (** [hashmap::{hashmap::HashMap<T>}::try_resize]: @@ -284,9 +280,11 @@ Definition hashMap_insert (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) : result (HashMap_t T) := - hm <- hashMap_insert_no_resize T n self key value; - i <- hashMap_len T hm; - if i s> hm.(hashMap_max_load) then hashMap_try_resize T n hm else Return hm + self1 <- hashMap_insert_no_resize T n self key value; + i <- hashMap_len T self1; + if i s> self1.(hashMap_max_load) + then hashMap_try_resize T n self1 + else Return self1 . (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0: @@ -398,9 +396,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..9fb3c482 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -29,9 +29,9 @@ Fixpoint hashmap_HashMap_allocate_slots_loop | S n2 => if n1 s> 0%usize then ( - v <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil; + slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil; n3 <- usize_sub n1 1%usize; - hashmap_HashMap_allocate_slots_loop T n2 v n3) + hashmap_HashMap_allocate_slots_loop T n2 slots1 n3) else Return slots end . @@ -204,8 +204,8 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop | S n1 => match ls with | Hashmap_List_Cons k v tl => - hm <- hashmap_HashMap_insert_no_resize T n1 ntable k v; - hashmap_HashMap_move_elements_from_list_loop T n1 hm tl + ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v; + hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl | Hashmap_List_Nil => Return ntable end end @@ -239,12 +239,10 @@ Fixpoint hashmap_HashMap_move_elements_loop i; let (l, index_mut_back) := p in let (ls, l1) := core_mem_replace (hashmap_List_t T) l Hashmap_List_Nil in - hm <- hashmap_HashMap_move_elements_from_list T n1 ntable ls; + ntable1 <- hashmap_HashMap_move_elements_from_list T n1 ntable ls; i2 <- usize_add i 1%usize; slots1 <- index_mut_back l1; - back_'a <- hashmap_HashMap_move_elements_loop T n1 hm slots1 i2; - let (hm1, v) := back_'a in - Return (hm1, v)) + hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2) else Return (ntable, slots) end . @@ -256,9 +254,7 @@ Definition hashmap_HashMap_move_elements (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T))) := - back_'a <- hashmap_HashMap_move_elements_loop T n ntable slots i; - let (hm, v) := back_'a in - Return (hm, v) + hashmap_HashMap_move_elements_loop T n ntable slots i . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]: @@ -304,11 +300,11 @@ Definition hashmap_HashMap_insert (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) : result (hashmap_HashMap_t T) := - hm <- hashmap_HashMap_insert_no_resize T n self key value; - i <- hashmap_HashMap_len T hm; - if i s> hm.(hashmap_HashMap_max_load) - then hashmap_HashMap_try_resize T n hm - else Return hm + self1 <- hashmap_HashMap_insert_no_resize T n self key value; + i <- hashmap_HashMap_len T self1; + if i s> self1.(hashmap_HashMap_max_load) + then hashmap_HashMap_try_resize T n self1 + else Return self1 . (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0: @@ -423,9 +419,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 +579,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/External_Funs.v b/tests/coq/misc/External_Funs.v index 91ea88c9..faf91fef 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -45,9 +45,9 @@ Definition custom_swap := p <- core_mem_swap T x y st; let (st1, p1) := p in - let (t, t1) := p1 in - let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, t1)) in - Return (st1, (t, back_'a)) + let (x1, y1) := p1 in + let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in + Return (st1, (x1, back_'a)) . (** [external::test_custom_swap]: diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index e235b60d..7c83a014 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -29,16 +29,16 @@ Definition sum (n : nat) (max : u32) : result u32 := (** [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 *) Fixpoint sum_with_mut_borrows_loop - (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 := + (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with | O => Fail_ OutOfFuel | S n1 => - if mi s< max + if i s< max then ( - ms1 <- u32_add ms mi; - mi1 <- u32_add mi 1%u32; - sum_with_mut_borrows_loop n1 max mi1 ms1) - else u32_mul ms 2%u32 + ms <- u32_add s i; + mi <- u32_add i 1%u32; + sum_with_mut_borrows_loop n1 max mi ms) + else u32_mul s 2%u32 end . @@ -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: @@ -245,10 +245,10 @@ Definition get_elem_mut p <- alloc_vec_Vec_index_mut (List_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize; - let (l, index_mut_back) := p in - p1 <- get_elem_mut_loop n x l; + let (ls, index_mut_back) := p in + p1 <- get_elem_mut_loop n x ls; let (i, back) := p1 in - let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in + let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in Return (i, back1) . @@ -273,10 +273,10 @@ Definition get_elem_shared (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) : result usize := - l <- + ls <- alloc_vec_Vec_index (List_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize; - get_elem_shared_loop n x l + get_elem_shared_loop n x ls . (** [loops::id_mut]: @@ -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/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 73c4ee58..76dc4cf6 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -475,9 +475,7 @@ Definition id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) := - let back_'a := fun (ret : (T1 * T2)) => let (t, t1) := ret in Return (t, t1) - in - Return ((x, y), back_'a) + Return ((x, y), Return) . (** [no_nested_borrows::id_mut_pair2]: @@ -486,10 +484,7 @@ Definition id_mut_pair2 (T1 T2 : Type) (p : (T1 * T2)) : result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2))) := - let (t, t1) := p in - let back_'a := - fun (ret : (T1 * T2)) => let (t2, t3) := ret in Return (t2, t3) in - Return ((t, t1), back_'a) + let (t, t1) := p in Return ((t, t1), Return) . (** [no_nested_borrows::id_mut_pair3]: diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 769cf34c..ad77fa2a 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 := (** [paper::test_incr]: Source: 'src/paper.rs', lines 8:0-8:18 *) Definition test_incr : result unit := - i <- ref_incr 0%i32; if negb (i s= 1%i32) then Fail_ Failure else Return tt + x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt . (** Unit test for [paper::test_incr] *) 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 |