diff options
Diffstat (limited to 'tests/coq/misc')
| -rw-r--r-- | tests/coq/misc/Constants.v | 16 | ||||
| -rw-r--r-- | tests/coq/misc/External_Funs.v | 18 | ||||
| -rw-r--r-- | tests/coq/misc/External_Opaque.v | 12 | ||||
| -rw-r--r-- | tests/coq/misc/Loops.v | 124 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 112 | ||||
| -rw-r--r-- | tests/coq/misc/Paper.v | 21 | ||||
| -rw-r--r-- | tests/coq/misc/PoloniusList.v | 4 | ||||
| -rw-r--r-- | tests/coq/misc/_CoqProject | 6 |
8 files changed, 159 insertions, 154 deletions
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index 6a5f2696..14c05c61 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -22,7 +22,7 @@ Definition x1_c : u32 := x1_body%global. Definition x2_body : result u32 := Return 3%u32. Definition x2_c : u32 := x2_body%global. -(** [constants::incr] *) +(** [constants::incr]: forward function *) Definition incr_fwd (n : u32) : result u32 := u32_add n 1%u32. @@ -30,7 +30,7 @@ Definition incr_fwd (n : u32) : result u32 := Definition x3_body : result u32 := incr_fwd 32%u32. Definition x3_c : u32 := x3_body%global. -(** [constants::mk_pair0] *) +(** [constants::mk_pair0]: forward function *) Definition mk_pair0_fwd (x : u32) (y : u32) : result (u32 * u32) := Return (x, y) . @@ -42,7 +42,7 @@ Arguments mkPair_t {T1} {T2} _ _. Arguments Pair_x {T1} {T2}. Arguments Pair_y {T1} {T2}. -(** [constants::mk_pair1] *) +(** [constants::mk_pair1]: forward function *) Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) := Return {| Pair_x := x; Pair_y := y |} . @@ -71,7 +71,7 @@ Record Wrap_t (T : Type) := mkWrap_t { Wrap_val : T; }. Arguments mkWrap_t {T} _. Arguments Wrap_val {T}. -(** [constants::Wrap::{0}::new] *) +(** [constants::Wrap::{0}::new]: forward function *) Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) := Return {| Wrap_val := val |} . @@ -80,7 +80,7 @@ Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) := Definition y_body : result (Wrap_t i32) := wrap_new_fwd i32 2%i32. Definition y_c : Wrap_t i32 := y_body%global. -(** [constants::unwrap_y] *) +(** [constants::unwrap_y]: forward function *) Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val). @@ -92,11 +92,11 @@ Definition yval_c : i32 := yval_body%global. Definition get_z1_z1_body : result i32 := Return 3%i32. Definition get_z1_z1_c : i32 := get_z1_z1_body%global. -(** [constants::get_z1] *) +(** [constants::get_z1]: forward function *) Definition get_z1_fwd : result i32 := Return get_z1_z1_c. -(** [constants::add] *) +(** [constants::add]: forward function *) Definition add_fwd (a : i32) (b : i32) : result i32 := i32_add a b. @@ -112,7 +112,7 @@ Definition q2_c : i32 := q2_body%global. Definition q3_body : result i32 := add_fwd q2_c 3%i32. Definition q3_c : i32 := q3_body%global. -(** [constants::get_z2] *) +(** [constants::get_z2]: forward function *) Definition get_z2_fwd : result i32 := i <- get_z1_fwd; i0 <- add_fwd i q3_c; add_fwd q1_c i0 . diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index 05dd8f2e..f18bbd1f 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -10,7 +10,7 @@ Require Export External_Opaque. Import External_Opaque. Module External_Funs. -(** [external::swap] *) +(** [external::swap]: forward function *) Definition swap_fwd (T : Type) (x : T) (y : T) (st : state) : result (state * unit) := p <- core_mem_swap_fwd T x y st; @@ -22,7 +22,7 @@ Definition swap_fwd Return (st2, tt) . -(** [external::swap] *) +(** [external::swap]: backward function 0 *) Definition swap_back (T : Type) (x : T) (y : T) (st : state) (st0 : state) : result (state * (T * T)) @@ -36,7 +36,7 @@ Definition swap_back Return (st0, (x0, y0)) . -(** [external::test_new_non_zero_u32] *) +(** [external::test_new_non_zero_u32]: forward function *) Definition test_new_non_zero_u32_fwd (x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) := p <- core_num_nonzero_non_zero_u32_new_fwd x st; @@ -44,7 +44,7 @@ Definition test_new_non_zero_u32_fwd core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0 . -(** [external::test_vec] *) +(** [external::test_vec]: forward function *) Definition test_vec_fwd : result unit := let v := vec_new u32 in _ <- vec_push_back u32 v 0%u32; Return tt . @@ -52,7 +52,7 @@ Definition test_vec_fwd : result unit := (** Unit test for [external::test_vec] *) Check (test_vec_fwd )%return. -(** [external::custom_swap] *) +(** [external::custom_swap]: forward function *) Definition custom_swap_fwd (T : Type) (x : T) (y : T) (st : state) : result (state * T) := p <- core_mem_swap_fwd T x y st; @@ -64,7 +64,7 @@ Definition custom_swap_fwd Return (st2, x0) . -(** [external::custom_swap] *) +(** [external::custom_swap]: backward function 0 *) Definition custom_swap_back (T : Type) (x : T) (y : T) (st : state) (ret : T) (st0 : state) : result (state * (T * T)) @@ -78,13 +78,13 @@ Definition custom_swap_back Return (st0, (ret, y0)) . -(** [external::test_custom_swap] *) +(** [external::test_custom_swap]: forward function *) Definition test_custom_swap_fwd (x : u32) (y : u32) (st : state) : result (state * unit) := p <- custom_swap_fwd u32 x y st; let (st0, _) := p in Return (st0, tt) . -(** [external::test_custom_swap] *) +(** [external::test_custom_swap]: backward function 0 *) Definition test_custom_swap_back (x : u32) (y : u32) (st : state) (st0 : state) : result (state * (u32 * u32)) @@ -92,7 +92,7 @@ Definition test_custom_swap_back custom_swap_back u32 x y st 1%u32 st0 . -(** [external::test_swap_non_zero] *) +(** [external::test_swap_non_zero]: forward function *) Definition test_swap_non_zero_fwd (x : u32) (st : state) : result (state * u32) := p <- swap_fwd u32 x 0%u32 st; diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v index d60251e0..1224f426 100644 --- a/tests/coq/misc/External_Opaque.v +++ b/tests/coq/misc/External_Opaque.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [external]: opaque function definitions *) +(** [external]: external function declarations *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. @@ -8,27 +8,27 @@ Require Export External_Types. Import External_Types. Module External_Opaque. -(** [core::mem::swap] *) +(** [core::mem::swap]: forward function *) Axiom core_mem_swap_fwd : forall(T : Type), T -> T -> state -> result (state * unit) . -(** [core::mem::swap] *) +(** [core::mem::swap]: backward function 0 *) Axiom core_mem_swap_back0 : forall(T : Type), T -> T -> state -> state -> result (state * T) . -(** [core::mem::swap] *) +(** [core::mem::swap]: backward function 1 *) Axiom core_mem_swap_back1 : forall(T : Type), T -> T -> state -> state -> result (state * T) . -(** [core::num::nonzero::NonZeroU32::{14}::new] *) +(** [core::num::nonzero::NonZeroU32::{14}::new]: forward function *) Axiom core_num_nonzero_non_zero_u32_new_fwd : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t)) . -(** [core::option::Option::{0}::unwrap] *) +(** [core::option::Option::{0}::unwrap]: forward function *) Axiom core_option_option_unwrap_fwd : forall(T : Type), option T -> state -> result (state * T) . diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index a5cb3688..f17eb986 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -6,7 +6,7 @@ Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. Module Loops. -(** [loops::sum] *) +(** [loops::sum]: loop 0: forward function *) Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with | O => Fail_ OutOfFuel @@ -17,12 +17,12 @@ Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := end . -(** [loops::sum] *) +(** [loops::sum]: forward function *) Definition sum_fwd (n : nat) (max : u32) : result u32 := sum_loop_fwd n max 0%u32 0%u32 . -(** [loops::sum_with_mut_borrows] *) +(** [loops::sum_with_mut_borrows]: loop 0: forward function *) Fixpoint sum_with_mut_borrows_loop_fwd (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 := match n with @@ -37,12 +37,12 @@ Fixpoint sum_with_mut_borrows_loop_fwd end . -(** [loops::sum_with_mut_borrows] *) +(** [loops::sum_with_mut_borrows]: forward function *) Definition sum_with_mut_borrows_fwd (n : nat) (max : u32) : result u32 := sum_with_mut_borrows_loop_fwd n max 0%u32 0%u32 . -(** [loops::sum_with_shared_borrows] *) +(** [loops::sum_with_shared_borrows]: loop 0: forward function *) Fixpoint sum_with_shared_borrows_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with @@ -57,12 +57,13 @@ Fixpoint sum_with_shared_borrows_loop_fwd end . -(** [loops::sum_with_shared_borrows] *) +(** [loops::sum_with_shared_borrows]: forward function *) Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 := sum_with_shared_borrows_loop_fwd n max 0%u32 0%u32 . -(** [loops::clear] *) +(** [loops::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Fixpoint clear_loop_fwd_back (n : nat) (v : vec u32) (i : usize) : result (vec u32) := match n with @@ -78,7 +79,8 @@ Fixpoint clear_loop_fwd_back end . -(** [loops::clear] *) +(** [loops::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) := clear_loop_fwd_back n v 0%usize . @@ -92,7 +94,7 @@ Inductive List_t (T : Type) := Arguments ListCons {T} _ _. Arguments ListNil {T}. -(** [loops::list_mem] *) +(** [loops::list_mem]: loop 0: forward function *) Fixpoint list_mem_loop_fwd (n : nat) (x : u32) (ls : List_t u32) : result bool := match n with @@ -106,12 +108,12 @@ Fixpoint list_mem_loop_fwd end . -(** [loops::list_mem] *) +(** [loops::list_mem]: forward function *) Definition list_mem_fwd (n : nat) (x : u32) (ls : List_t u32) : result bool := list_mem_loop_fwd n x ls . -(** [loops::list_nth_mut_loop] *) +(** [loops::list_nth_mut_loop]: loop 0: forward function *) Fixpoint list_nth_mut_loop_loop_fwd (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := match n with @@ -127,13 +129,13 @@ Fixpoint list_nth_mut_loop_loop_fwd end . -(** [loops::list_nth_mut_loop] *) +(** [loops::list_nth_mut_loop]: forward function *) Definition list_nth_mut_loop_fwd (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := list_nth_mut_loop_loop_fwd T n ls i . -(** [loops::list_nth_mut_loop] *) +(** [loops::list_nth_mut_loop]: loop 0: backward function 0 *) Fixpoint list_nth_mut_loop_loop_back (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -154,7 +156,7 @@ Fixpoint list_nth_mut_loop_loop_back end . -(** [loops::list_nth_mut_loop] *) +(** [loops::list_nth_mut_loop]: backward function 0 *) Definition list_nth_mut_loop_back (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -162,7 +164,7 @@ Definition list_nth_mut_loop_back list_nth_mut_loop_loop_back T n ls i ret . -(** [loops::list_nth_shared_loop] *) +(** [loops::list_nth_shared_loop]: loop 0: forward function *) Fixpoint list_nth_shared_loop_loop_fwd (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := match n with @@ -178,13 +180,13 @@ Fixpoint list_nth_shared_loop_loop_fwd end . -(** [loops::list_nth_shared_loop] *) +(** [loops::list_nth_shared_loop]: forward function *) Definition list_nth_shared_loop_fwd (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := list_nth_shared_loop_loop_fwd T n ls i . -(** [loops::get_elem_mut] *) +(** [loops::get_elem_mut]: loop 0: forward function *) Fixpoint get_elem_mut_loop_fwd (n : nat) (x : usize) (ls : List_t usize) : result usize := match n with @@ -198,14 +200,14 @@ Fixpoint get_elem_mut_loop_fwd end . -(** [loops::get_elem_mut] *) +(** [loops::get_elem_mut]: forward function *) Definition get_elem_mut_fwd (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize := l <- vec_index_mut_fwd (List_t usize) slots 0%usize; get_elem_mut_loop_fwd n x l . -(** [loops::get_elem_mut] *) +(** [loops::get_elem_mut]: loop 0: backward function 0 *) Fixpoint get_elem_mut_loop_back (n : nat) (x : usize) (ls : List_t usize) (ret : usize) : result (List_t usize) @@ -223,7 +225,7 @@ Fixpoint get_elem_mut_loop_back end . -(** [loops::get_elem_mut] *) +(** [loops::get_elem_mut]: backward function 0 *) Definition get_elem_mut_back (n : nat) (slots : vec (List_t usize)) (x : usize) (ret : usize) : result (vec (List_t usize)) @@ -233,7 +235,7 @@ Definition get_elem_mut_back vec_index_mut_back (List_t usize) slots 0%usize l0 . -(** [loops::get_elem_shared] *) +(** [loops::get_elem_shared]: loop 0: forward function *) Fixpoint get_elem_shared_loop_fwd (n : nat) (x : usize) (ls : List_t usize) : result usize := match n with @@ -247,30 +249,30 @@ Fixpoint get_elem_shared_loop_fwd end . -(** [loops::get_elem_shared] *) +(** [loops::get_elem_shared]: forward function *) Definition get_elem_shared_fwd (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize := l <- vec_index_fwd (List_t usize) slots 0%usize; get_elem_shared_loop_fwd n x l . -(** [loops::id_mut] *) +(** [loops::id_mut]: forward function *) Definition id_mut_fwd (T : Type) (ls : List_t T) : result (List_t T) := Return ls . -(** [loops::id_mut] *) +(** [loops::id_mut]: backward function 0 *) Definition id_mut_back (T : Type) (ls : List_t T) (ret : List_t T) : result (List_t T) := Return ret . -(** [loops::id_shared] *) +(** [loops::id_shared]: forward function *) Definition id_shared_fwd (T : Type) (ls : List_t T) : result (List_t T) := Return ls . -(** [loops::list_nth_mut_loop_with_id] *) +(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *) Fixpoint list_nth_mut_loop_with_id_loop_fwd (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T := match n with @@ -287,13 +289,13 @@ Fixpoint list_nth_mut_loop_with_id_loop_fwd end . -(** [loops::list_nth_mut_loop_with_id] *) +(** [loops::list_nth_mut_loop_with_id]: forward function *) Definition list_nth_mut_loop_with_id_fwd (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := ls0 <- id_mut_fwd T ls; list_nth_mut_loop_with_id_loop_fwd T n i ls0 . -(** [loops::list_nth_mut_loop_with_id] *) +(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *) Fixpoint list_nth_mut_loop_with_id_loop_back (T : Type) (n : nat) (i : u32) (ls : List_t T) (ret : T) : result (List_t T) @@ -314,7 +316,7 @@ Fixpoint list_nth_mut_loop_with_id_loop_back end . -(** [loops::list_nth_mut_loop_with_id] *) +(** [loops::list_nth_mut_loop_with_id]: backward function 0 *) Definition list_nth_mut_loop_with_id_back (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -324,7 +326,7 @@ Definition list_nth_mut_loop_with_id_back id_mut_back T ls l . -(** [loops::list_nth_shared_loop_with_id] *) +(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *) Fixpoint list_nth_shared_loop_with_id_loop_fwd (T : Type) (n : nat) (i : u32) (ls : List_t T) : result T := match n with @@ -341,13 +343,13 @@ Fixpoint list_nth_shared_loop_with_id_loop_fwd end . -(** [loops::list_nth_shared_loop_with_id] *) +(** [loops::list_nth_shared_loop_with_id]: forward function *) Definition list_nth_shared_loop_with_id_fwd (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := ls0 <- id_shared_fwd T ls; list_nth_shared_loop_with_id_loop_fwd T n i ls0 . -(** [loops::list_nth_mut_loop_pair] *) +(** [loops::list_nth_mut_loop_pair]: loop 0: forward function *) Fixpoint list_nth_mut_loop_pair_loop_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -371,7 +373,7 @@ Fixpoint list_nth_mut_loop_pair_loop_fwd end . -(** [loops::list_nth_mut_loop_pair] *) +(** [loops::list_nth_mut_loop_pair]: forward function *) Definition list_nth_mut_loop_pair_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -379,7 +381,7 @@ Definition list_nth_mut_loop_pair_fwd list_nth_mut_loop_pair_loop_fwd T n ls0 ls1 i . -(** [loops::list_nth_mut_loop_pair] *) +(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *) Fixpoint list_nth_mut_loop_pair_loop_back'a (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -404,7 +406,7 @@ Fixpoint list_nth_mut_loop_pair_loop_back'a end . -(** [loops::list_nth_mut_loop_pair] *) +(** [loops::list_nth_mut_loop_pair]: backward function 0 *) Definition list_nth_mut_loop_pair_back'a (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -412,7 +414,7 @@ Definition list_nth_mut_loop_pair_back'a list_nth_mut_loop_pair_loop_back'a T n ls0 ls1 i ret . -(** [loops::list_nth_mut_loop_pair] *) +(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 *) Fixpoint list_nth_mut_loop_pair_loop_back'b (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -437,7 +439,7 @@ Fixpoint list_nth_mut_loop_pair_loop_back'b end . -(** [loops::list_nth_mut_loop_pair] *) +(** [loops::list_nth_mut_loop_pair]: backward function 1 *) Definition list_nth_mut_loop_pair_back'b (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -445,7 +447,7 @@ Definition list_nth_mut_loop_pair_back'b list_nth_mut_loop_pair_loop_back'b T n ls0 ls1 i ret . -(** [loops::list_nth_shared_loop_pair] *) +(** [loops::list_nth_shared_loop_pair]: loop 0: forward function *) Fixpoint list_nth_shared_loop_pair_loop_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -469,7 +471,7 @@ Fixpoint list_nth_shared_loop_pair_loop_fwd end . -(** [loops::list_nth_shared_loop_pair] *) +(** [loops::list_nth_shared_loop_pair]: forward function *) Definition list_nth_shared_loop_pair_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -477,7 +479,7 @@ Definition list_nth_shared_loop_pair_fwd list_nth_shared_loop_pair_loop_fwd T n ls0 ls1 i . -(** [loops::list_nth_mut_loop_pair_merge] *) +(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *) Fixpoint list_nth_mut_loop_pair_merge_loop_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -501,7 +503,7 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_fwd end . -(** [loops::list_nth_mut_loop_pair_merge] *) +(** [loops::list_nth_mut_loop_pair_merge]: forward function *) Definition list_nth_mut_loop_pair_merge_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -509,7 +511,7 @@ Definition list_nth_mut_loop_pair_merge_fwd list_nth_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i . -(** [loops::list_nth_mut_loop_pair_merge] *) +(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *) Fixpoint list_nth_mut_loop_pair_merge_loop_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : (T * T)) : @@ -536,7 +538,7 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_back end . -(** [loops::list_nth_mut_loop_pair_merge] *) +(** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *) Definition list_nth_mut_loop_pair_merge_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : (T * T)) : @@ -545,7 +547,7 @@ Definition list_nth_mut_loop_pair_merge_back list_nth_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret . -(** [loops::list_nth_shared_loop_pair_merge] *) +(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *) Fixpoint list_nth_shared_loop_pair_merge_loop_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -569,7 +571,7 @@ Fixpoint list_nth_shared_loop_pair_merge_loop_fwd end . -(** [loops::list_nth_shared_loop_pair_merge] *) +(** [loops::list_nth_shared_loop_pair_merge]: forward function *) Definition list_nth_shared_loop_pair_merge_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -577,7 +579,7 @@ Definition list_nth_shared_loop_pair_merge_fwd list_nth_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i . -(** [loops::list_nth_mut_shared_loop_pair] *) +(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *) Fixpoint list_nth_mut_shared_loop_pair_loop_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -601,7 +603,7 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_fwd end . -(** [loops::list_nth_mut_shared_loop_pair] *) +(** [loops::list_nth_mut_shared_loop_pair]: forward function *) Definition list_nth_mut_shared_loop_pair_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -609,7 +611,7 @@ Definition list_nth_mut_shared_loop_pair_fwd list_nth_mut_shared_loop_pair_loop_fwd T n ls0 ls1 i . -(** [loops::list_nth_mut_shared_loop_pair] *) +(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *) Fixpoint list_nth_mut_shared_loop_pair_loop_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -634,7 +636,7 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_back end . -(** [loops::list_nth_mut_shared_loop_pair] *) +(** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *) Definition list_nth_mut_shared_loop_pair_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -642,7 +644,7 @@ Definition list_nth_mut_shared_loop_pair_back list_nth_mut_shared_loop_pair_loop_back T n ls0 ls1 i ret . -(** [loops::list_nth_mut_shared_loop_pair_merge] *) +(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *) Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -666,7 +668,7 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd end . -(** [loops::list_nth_mut_shared_loop_pair_merge] *) +(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *) Definition list_nth_mut_shared_loop_pair_merge_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -674,7 +676,7 @@ Definition list_nth_mut_shared_loop_pair_merge_fwd list_nth_mut_shared_loop_pair_merge_loop_fwd T n ls0 ls1 i . -(** [loops::list_nth_mut_shared_loop_pair_merge] *) +(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *) Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -700,7 +702,7 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back end . -(** [loops::list_nth_mut_shared_loop_pair_merge] *) +(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *) Definition list_nth_mut_shared_loop_pair_merge_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -708,7 +710,7 @@ Definition list_nth_mut_shared_loop_pair_merge_back list_nth_mut_shared_loop_pair_merge_loop_back T n ls0 ls1 i ret . -(** [loops::list_nth_shared_mut_loop_pair] *) +(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *) Fixpoint list_nth_shared_mut_loop_pair_loop_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -732,7 +734,7 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_fwd end . -(** [loops::list_nth_shared_mut_loop_pair] *) +(** [loops::list_nth_shared_mut_loop_pair]: forward function *) Definition list_nth_shared_mut_loop_pair_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -740,7 +742,7 @@ Definition list_nth_shared_mut_loop_pair_fwd list_nth_shared_mut_loop_pair_loop_fwd T n ls0 ls1 i . -(** [loops::list_nth_shared_mut_loop_pair] *) +(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *) Fixpoint list_nth_shared_mut_loop_pair_loop_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -765,7 +767,7 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_back end . -(** [loops::list_nth_shared_mut_loop_pair] *) +(** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *) Definition list_nth_shared_mut_loop_pair_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -773,7 +775,7 @@ Definition list_nth_shared_mut_loop_pair_back list_nth_shared_mut_loop_pair_loop_back T n ls0 ls1 i ret . -(** [loops::list_nth_shared_mut_loop_pair_merge] *) +(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *) Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -797,7 +799,7 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd end . -(** [loops::list_nth_shared_mut_loop_pair_merge] *) +(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *) Definition list_nth_shared_mut_loop_pair_merge_fwd (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result (T * T) @@ -805,7 +807,7 @@ Definition list_nth_shared_mut_loop_pair_merge_fwd list_nth_shared_mut_loop_pair_merge_loop_fwd T n ls0 ls1 i . -(** [loops::list_nth_shared_mut_loop_pair_merge] *) +(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *) Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) @@ -831,7 +833,7 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back end . -(** [loops::list_nth_shared_mut_loop_pair_merge] *) +(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *) Definition list_nth_shared_mut_loop_pair_merge_back (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) : result (List_t T) diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 96d62711..470a2cde 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -45,47 +45,47 @@ Inductive Sum_t (T1 T2 : Type) := Arguments SumLeft {T1} {T2} _. Arguments SumRight {T1} {T2} _. -(** [no_nested_borrows::neg_test] *) +(** [no_nested_borrows::neg_test]: forward function *) Definition neg_test_fwd (x : i32) : result i32 := i32_neg x. -(** [no_nested_borrows::add_test] *) +(** [no_nested_borrows::add_test]: forward function *) Definition add_test_fwd (x : u32) (y : u32) : result u32 := u32_add x y. -(** [no_nested_borrows::subs_test] *) +(** [no_nested_borrows::subs_test]: forward function *) Definition subs_test_fwd (x : u32) (y : u32) : result u32 := u32_sub x y. -(** [no_nested_borrows::div_test] *) +(** [no_nested_borrows::div_test]: forward function *) Definition div_test_fwd (x : u32) (y : u32) : result u32 := u32_div x y. -(** [no_nested_borrows::div_test1] *) +(** [no_nested_borrows::div_test1]: forward function *) Definition div_test1_fwd (x : u32) : result u32 := u32_div x 2%u32. -(** [no_nested_borrows::rem_test] *) +(** [no_nested_borrows::rem_test]: forward function *) Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y. -(** [no_nested_borrows::cast_test] *) +(** [no_nested_borrows::cast_test]: forward function *) Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x. -(** [no_nested_borrows::test2] *) +(** [no_nested_borrows::test2]: forward function *) Definition test2_fwd : result unit := _ <- u32_add 23%u32 44%u32; Return tt. (** Unit test for [no_nested_borrows::test2] *) Check (test2_fwd )%return. -(** [no_nested_borrows::get_max] *) +(** [no_nested_borrows::get_max]: forward function *) Definition get_max_fwd (x : u32) (y : u32) : result u32 := if x s>= y then Return x else Return y . -(** [no_nested_borrows::test3] *) +(** [no_nested_borrows::test3]: forward function *) Definition test3_fwd : result unit := x <- get_max_fwd 4%u32 3%u32; y <- get_max_fwd 10%u32 11%u32; @@ -96,7 +96,7 @@ Definition test3_fwd : result unit := (** Unit test for [no_nested_borrows::test3] *) Check (test3_fwd )%return. -(** [no_nested_borrows::test_neg1] *) +(** [no_nested_borrows::test_neg1]: forward function *) Definition test_neg1_fwd : result unit := y <- i32_neg 3%i32; if negb (y s= (-3)%i32) then Fail_ Failure else Return tt . @@ -104,7 +104,7 @@ Definition test_neg1_fwd : result unit := (** Unit test for [no_nested_borrows::test_neg1] *) Check (test_neg1_fwd )%return. -(** [no_nested_borrows::refs_test1] *) +(** [no_nested_borrows::refs_test1]: forward function *) Definition refs_test1_fwd : result unit := if negb (1%i32 s= 1%i32) then Fail_ Failure else Return tt . @@ -112,7 +112,7 @@ Definition refs_test1_fwd : result unit := (** Unit test for [no_nested_borrows::refs_test1] *) Check (refs_test1_fwd )%return. -(** [no_nested_borrows::refs_test2] *) +(** [no_nested_borrows::refs_test2]: forward function *) Definition refs_test2_fwd : result unit := if negb (2%i32 s= 2%i32) then Fail_ Failure @@ -128,14 +128,14 @@ Definition refs_test2_fwd : result unit := (** Unit test for [no_nested_borrows::refs_test2] *) Check (refs_test2_fwd )%return. -(** [no_nested_borrows::test_list1] *) +(** [no_nested_borrows::test_list1]: forward function *) Definition test_list1_fwd : result unit := Return tt. (** Unit test for [no_nested_borrows::test_list1] *) Check (test_list1_fwd )%return. -(** [no_nested_borrows::test_box1] *) +(** [no_nested_borrows::test_box1]: forward function *) Definition test_box1_fwd : result unit := let b := 1%i32 in let x := b in @@ -145,21 +145,21 @@ Definition test_box1_fwd : result unit := (** Unit test for [no_nested_borrows::test_box1] *) Check (test_box1_fwd )%return. -(** [no_nested_borrows::copy_int] *) +(** [no_nested_borrows::copy_int]: forward function *) Definition copy_int_fwd (x : i32) : result i32 := Return x. -(** [no_nested_borrows::test_unreachable] *) +(** [no_nested_borrows::test_unreachable]: forward function *) Definition test_unreachable_fwd (b : bool) : result unit := if b then Fail_ Failure else Return tt . -(** [no_nested_borrows::test_panic] *) +(** [no_nested_borrows::test_panic]: forward function *) Definition test_panic_fwd (b : bool) : result unit := if b then Fail_ Failure else Return tt . -(** [no_nested_borrows::test_copy_int] *) +(** [no_nested_borrows::test_copy_int]: forward function *) Definition test_copy_int_fwd : result unit := y <- copy_int_fwd 0%i32; if negb (0%i32 s= y) then Fail_ Failure else Return tt @@ -168,12 +168,12 @@ Definition test_copy_int_fwd : result unit := (** Unit test for [no_nested_borrows::test_copy_int] *) Check (test_copy_int_fwd )%return. -(** [no_nested_borrows::is_cons] *) +(** [no_nested_borrows::is_cons]: forward function *) Definition is_cons_fwd (T : Type) (l : List_t T) : result bool := match l with | ListCons t l0 => Return true | ListNil => Return false end . -(** [no_nested_borrows::test_is_cons] *) +(** [no_nested_borrows::test_is_cons]: forward function *) Definition test_is_cons_fwd : result unit := let l := ListNil in b <- is_cons_fwd i32 (ListCons 0%i32 l); @@ -183,7 +183,7 @@ Definition test_is_cons_fwd : result unit := (** Unit test for [no_nested_borrows::test_is_cons] *) Check (test_is_cons_fwd )%return. -(** [no_nested_borrows::split_list] *) +(** [no_nested_borrows::split_list]: forward function *) Definition split_list_fwd (T : Type) (l : List_t T) : result (T * (List_t T)) := match l with @@ -192,7 +192,7 @@ Definition split_list_fwd end . -(** [no_nested_borrows::test_split_list] *) +(** [no_nested_borrows::test_split_list]: forward function *) Definition test_split_list_fwd : result unit := let l := ListNil in p <- split_list_fwd i32 (ListCons 0%i32 l); @@ -203,18 +203,18 @@ Definition test_split_list_fwd : result unit := (** Unit test for [no_nested_borrows::test_split_list] *) Check (test_split_list_fwd )%return. -(** [no_nested_borrows::choose] *) +(** [no_nested_borrows::choose]: forward function *) Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T := if b then Return x else Return y . -(** [no_nested_borrows::choose] *) +(** [no_nested_borrows::choose]: backward function 0 *) Definition choose_back (T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) := if b then Return (ret, y) else Return (x, ret) . -(** [no_nested_borrows::choose_test] *) +(** [no_nested_borrows::choose_test]: forward function *) Definition choose_test_fwd : result unit := z <- choose_fwd i32 true 0%i32 0%i32; z0 <- i32_add z 1%i32; @@ -231,7 +231,7 @@ Definition choose_test_fwd : result unit := (** Unit test for [no_nested_borrows::choose_test] *) Check (choose_test_fwd )%return. -(** [no_nested_borrows::test_char] *) +(** [no_nested_borrows::test_char]: forward function *) Definition test_char_fwd : result char := Return (char_of_byte Coq.Init.Byte.x61) . @@ -253,7 +253,7 @@ Arguments NodeElemNil {T}. Arguments TreeLeaf {T} _. Arguments TreeNode {T} _ _ _. -(** [no_nested_borrows::list_length] *) +(** [no_nested_borrows::list_length]: forward function *) Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 := match l with | ListCons t l1 => i <- list_length_fwd T l1; u32_add 1%u32 i @@ -261,7 +261,7 @@ Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 := end . -(** [no_nested_borrows::list_nth_shared] *) +(** [no_nested_borrows::list_nth_shared]: forward function *) Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T := match l with | ListCons x tl => @@ -272,7 +272,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T := end . -(** [no_nested_borrows::list_nth_mut] *) +(** [no_nested_borrows::list_nth_mut]: forward function *) Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := match l with | ListCons x tl => @@ -283,7 +283,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := end . -(** [no_nested_borrows::list_nth_mut] *) +(** [no_nested_borrows::list_nth_mut]: backward function 0 *) Fixpoint list_nth_mut_back (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) := match l with @@ -298,7 +298,7 @@ Fixpoint list_nth_mut_back end . -(** [no_nested_borrows::list_rev_aux] *) +(** [no_nested_borrows::list_rev_aux]: forward function *) Fixpoint list_rev_aux_fwd (T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) := match li with @@ -307,13 +307,14 @@ Fixpoint list_rev_aux_fwd end . -(** [no_nested_borrows::list_rev] *) +(** [no_nested_borrows::list_rev]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition list_rev_fwd_back (T : Type) (l : List_t T) : result (List_t T) := let li := mem_replace_fwd (List_t T) l ListNil in list_rev_aux_fwd T li ListNil . -(** [no_nested_borrows::test_list_functions] *) +(** [no_nested_borrows::test_list_functions]: forward function *) Definition test_list_functions_fwd : result unit := let l := ListNil in let l0 := ListCons 2%i32 l in @@ -350,61 +351,61 @@ Definition test_list_functions_fwd : result unit := (** Unit test for [no_nested_borrows::test_list_functions] *) Check (test_list_functions_fwd )%return. -(** [no_nested_borrows::id_mut_pair1] *) +(** [no_nested_borrows::id_mut_pair1]: forward function *) Definition id_mut_pair1_fwd (T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) := Return (x, y) . -(** [no_nested_borrows::id_mut_pair1] *) +(** [no_nested_borrows::id_mut_pair1]: backward function 0 *) Definition id_mut_pair1_back (T1 T2 : Type) (x : T1) (y : T2) (ret : (T1 * T2)) : result (T1 * T2) := let (t, t0) := ret in Return (t, t0) . -(** [no_nested_borrows::id_mut_pair2] *) +(** [no_nested_borrows::id_mut_pair2]: forward function *) Definition id_mut_pair2_fwd (T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) := let (t, t0) := p in Return (t, t0) . -(** [no_nested_borrows::id_mut_pair2] *) +(** [no_nested_borrows::id_mut_pair2]: backward function 0 *) Definition id_mut_pair2_back (T1 T2 : Type) (p : (T1 * T2)) (ret : (T1 * T2)) : result (T1 * T2) := let (t, t0) := ret in Return (t, t0) . -(** [no_nested_borrows::id_mut_pair3] *) +(** [no_nested_borrows::id_mut_pair3]: forward function *) Definition id_mut_pair3_fwd (T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) := Return (x, y) . -(** [no_nested_borrows::id_mut_pair3] *) +(** [no_nested_borrows::id_mut_pair3]: backward function 0 *) Definition id_mut_pair3_back'a (T1 T2 : Type) (x : T1) (y : T2) (ret : T1) : result T1 := Return ret . -(** [no_nested_borrows::id_mut_pair3] *) +(** [no_nested_borrows::id_mut_pair3]: backward function 1 *) Definition id_mut_pair3_back'b (T1 T2 : Type) (x : T1) (y : T2) (ret : T2) : result T2 := Return ret . -(** [no_nested_borrows::id_mut_pair4] *) +(** [no_nested_borrows::id_mut_pair4]: forward function *) Definition id_mut_pair4_fwd (T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) := let (t, t0) := p in Return (t, t0) . -(** [no_nested_borrows::id_mut_pair4] *) +(** [no_nested_borrows::id_mut_pair4]: backward function 0 *) Definition id_mut_pair4_back'a (T1 T2 : Type) (p : (T1 * T2)) (ret : T1) : result T1 := Return ret . -(** [no_nested_borrows::id_mut_pair4] *) +(** [no_nested_borrows::id_mut_pair4]: backward function 1 *) Definition id_mut_pair4_back'b (T1 T2 : Type) (p : (T1 * T2)) (ret : T2) : result T2 := Return ret @@ -420,17 +421,17 @@ mkStruct_with_tuple_t { Arguments mkStruct_with_tuple_t {T1} {T2} _. Arguments Struct_with_tuple_p {T1} {T2}. -(** [no_nested_borrows::new_tuple1] *) +(** [no_nested_borrows::new_tuple1]: forward function *) Definition new_tuple1_fwd : result (Struct_with_tuple_t u32 u32) := Return {| Struct_with_tuple_p := (1%u32, 2%u32) |} . -(** [no_nested_borrows::new_tuple2] *) +(** [no_nested_borrows::new_tuple2]: forward function *) Definition new_tuple2_fwd : result (Struct_with_tuple_t i16 i16) := Return {| Struct_with_tuple_p := (1%i16, 2%i16) |} . -(** [no_nested_borrows::new_tuple3] *) +(** [no_nested_borrows::new_tuple3]: forward function *) Definition new_tuple3_fwd : result (Struct_with_tuple_t u64 i64) := Return {| Struct_with_tuple_p := (1%u64, 2%i64) |} . @@ -445,12 +446,12 @@ mkStruct_with_pair_t { Arguments mkStruct_with_pair_t {T1} {T2} _. Arguments Struct_with_pair_p {T1} {T2}. -(** [no_nested_borrows::new_pair1] *) +(** [no_nested_borrows::new_pair1]: forward function *) Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) := Return {| Struct_with_pair_p := {| Pair_x := 1%u32; Pair_y := 2%u32 |} |} . -(** [no_nested_borrows::test_constants] *) +(** [no_nested_borrows::test_constants]: forward function *) Definition test_constants_fwd : result unit := swt <- new_tuple1_fwd; let (i, _) := swt.(Struct_with_tuple_p) in @@ -476,34 +477,35 @@ Definition test_constants_fwd : result unit := (** Unit test for [no_nested_borrows::test_constants] *) Check (test_constants_fwd )%return. -(** [no_nested_borrows::test_weird_borrows1] *) +(** [no_nested_borrows::test_weird_borrows1]: forward function *) Definition test_weird_borrows1_fwd : result unit := Return tt. (** Unit test for [no_nested_borrows::test_weird_borrows1] *) Check (test_weird_borrows1_fwd )%return. -(** [no_nested_borrows::test_mem_replace] *) +(** [no_nested_borrows::test_mem_replace]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition test_mem_replace_fwd_back (px : u32) : result u32 := let y := mem_replace_fwd u32 px 1%u32 in if negb (y s= 0%u32) then Fail_ Failure else Return 2%u32 . -(** [no_nested_borrows::test_shared_borrow_bool1] *) +(** [no_nested_borrows::test_shared_borrow_bool1]: forward function *) Definition test_shared_borrow_bool1_fwd (b : bool) : result u32 := if b then Return 0%u32 else Return 1%u32 . -(** [no_nested_borrows::test_shared_borrow_bool2] *) +(** [no_nested_borrows::test_shared_borrow_bool2]: forward function *) Definition test_shared_borrow_bool2_fwd : result u32 := Return 0%u32. -(** [no_nested_borrows::test_shared_borrow_enum1] *) +(** [no_nested_borrows::test_shared_borrow_enum1]: forward function *) Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 := match l with | ListCons i l0 => Return 1%u32 | ListNil => Return 0%u32 end . -(** [no_nested_borrows::test_shared_borrow_enum2] *) +(** [no_nested_borrows::test_shared_borrow_enum2]: forward function *) Definition test_shared_borrow_enum2_fwd : result u32 := Return 0%u32. diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 513bc749..0f854f31 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -6,11 +6,12 @@ Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. Module Paper. -(** [paper::ref_incr] *) +(** [paper::ref_incr]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) Definition ref_incr_fwd_back (x : i32) : result i32 := i32_add x 1%i32. -(** [paper::test_incr] *) +(** [paper::test_incr]: forward function *) Definition test_incr_fwd : result unit := x <- ref_incr_fwd_back 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt @@ -19,18 +20,18 @@ Definition test_incr_fwd : result unit := (** Unit test for [paper::test_incr] *) Check (test_incr_fwd )%return. -(** [paper::choose] *) +(** [paper::choose]: forward function *) Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T := if b then Return x else Return y . -(** [paper::choose] *) +(** [paper::choose]: backward function 0 *) Definition choose_back (T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) := if b then Return (ret, y) else Return (x, ret) . -(** [paper::test_choose] *) +(** [paper::test_choose]: forward function *) Definition test_choose_fwd : result unit := z <- choose_fwd i32 true 0%i32 0%i32; z0 <- i32_add z 1%i32; @@ -56,7 +57,7 @@ Inductive List_t (T : Type) := Arguments ListCons {T} _ _. Arguments ListNil {T}. -(** [paper::list_nth_mut] *) +(** [paper::list_nth_mut]: forward function *) Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := match l with | ListCons x tl => @@ -67,7 +68,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := end . -(** [paper::list_nth_mut] *) +(** [paper::list_nth_mut]: backward function 0 *) Fixpoint list_nth_mut_back (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) := match l with @@ -82,7 +83,7 @@ Fixpoint list_nth_mut_back end . -(** [paper::sum] *) +(** [paper::sum]: forward function *) Fixpoint sum_fwd (l : List_t i32) : result i32 := match l with | ListCons x tl => i <- sum_fwd tl; i32_add x i @@ -90,7 +91,7 @@ Fixpoint sum_fwd (l : List_t i32) : result i32 := end . -(** [paper::test_nth] *) +(** [paper::test_nth]: forward function *) Definition test_nth_fwd : result unit := let l := ListNil in let l0 := ListCons 3%i32 l in @@ -105,7 +106,7 @@ Definition test_nth_fwd : result unit := (** Unit test for [paper::test_nth] *) Check (test_nth_fwd )%return. -(** [paper::call_choose] *) +(** [paper::call_choose]: forward function *) Definition call_choose_fwd (p : (u32 * u32)) : result u32 := let (px, py) := p in pz <- choose_fwd u32 true px py; diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v index bd6df02e..e94b6dcb 100644 --- a/tests/coq/misc/PoloniusList.v +++ b/tests/coq/misc/PoloniusList.v @@ -15,7 +15,7 @@ Inductive List_t (T : Type) := Arguments ListCons {T} _ _. Arguments ListNil {T}. -(** [polonius_list::get_list_at_x] *) +(** [polonius_list::get_list_at_x]: forward function *) Fixpoint get_list_at_x_fwd (ls : List_t u32) (x : u32) : result (List_t u32) := match ls with | ListCons hd tl => @@ -24,7 +24,7 @@ Fixpoint get_list_at_x_fwd (ls : List_t u32) (x : u32) : result (List_t u32) := end . -(** [polonius_list::get_list_at_x] *) +(** [polonius_list::get_list_at_x]: backward function 0 *) Fixpoint get_list_at_x_back (ls : List_t u32) (x : u32) (ret : List_t u32) : result (List_t u32) := match ls with diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index 87dea3e6..db6c2742 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -3,12 +3,12 @@ -arg -w -arg all -Constants.v -External_Types.v -Primitives.v Loops.v +Primitives.v External_Funs.v +Constants.v PoloniusList.v +External_Types.v NoNestedBorrows.v External_Opaque.v Paper.v |