diff options
Diffstat (limited to 'tests/coq/misc/Paper.v')
| -rw-r--r-- | tests/coq/misc/Paper.v | 33 |
1 files changed, 22 insertions, 11 deletions
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index d3852e6b..4a49096f 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -9,11 +9,13 @@ Local Open Scope Primitives_scope. Module Paper. (** [paper::ref_incr]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) *) + (there is a single backward function, and the forward function returns ()) + Source: 'src/paper.rs', lines 4:0-4:28 *) Definition ref_incr (x : i32) : result i32 := i32_add x 1%i32. -(** [paper::test_incr]: forward function *) +(** [paper::test_incr]: forward function + Source: 'src/paper.rs', lines 8:0-8:18 *) Definition test_incr : result unit := x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt . @@ -21,18 +23,21 @@ Definition test_incr : result unit := (** Unit test for [paper::test_incr] *) Check (test_incr )%return. -(** [paper::choose]: forward function *) +(** [paper::choose]: forward function + Source: 'src/paper.rs', lines 15:0-15:70 *) Definition choose (T : Type) (b : bool) (x : T) (y : T) : result T := if b then Return x else Return y . -(** [paper::choose]: backward function 0 *) +(** [paper::choose]: backward function 0 + Source: 'src/paper.rs', lines 15:0-15:70 *) 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]: forward function *) +(** [paper::test_choose]: forward function + Source: 'src/paper.rs', lines 23:0-23:20 *) Definition test_choose : result unit := z <- choose i32 true 0%i32 0%i32; z0 <- i32_add z 1%i32; @@ -49,7 +54,8 @@ Definition test_choose : result unit := (** Unit test for [paper::test_choose] *) Check (test_choose )%return. -(** [paper::List] *) +(** [paper::List] + Source: 'src/paper.rs', lines 35:0-35:16 *) Inductive List_t (T : Type) := | List_Cons : T -> List_t T -> List_t T | List_Nil : List_t T @@ -58,7 +64,8 @@ Inductive List_t (T : Type) := Arguments List_Cons { _ }. Arguments List_Nil { _ }. -(** [paper::list_nth_mut]: forward function *) +(** [paper::list_nth_mut]: forward function + Source: 'src/paper.rs', lines 42:0-42:67 *) Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result T := match l with | List_Cons x tl => @@ -69,7 +76,8 @@ Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result T := end . -(** [paper::list_nth_mut]: backward function 0 *) +(** [paper::list_nth_mut]: backward function 0 + Source: 'src/paper.rs', lines 42:0-42:67 *) Fixpoint list_nth_mut_back (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) := match l with @@ -84,7 +92,8 @@ Fixpoint list_nth_mut_back end . -(** [paper::sum]: forward function *) +(** [paper::sum]: forward function + Source: 'src/paper.rs', lines 57:0-57:32 *) Fixpoint sum (l : List_t i32) : result i32 := match l with | List_Cons x tl => i <- sum tl; i32_add x i @@ -92,7 +101,8 @@ Fixpoint sum (l : List_t i32) : result i32 := end . -(** [paper::test_nth]: forward function *) +(** [paper::test_nth]: forward function + Source: 'src/paper.rs', lines 68:0-68:17 *) Definition test_nth : result unit := let l := List_Nil in let l0 := List_Cons 3%i32 l in @@ -107,7 +117,8 @@ Definition test_nth : result unit := (** Unit test for [paper::test_nth] *) Check (test_nth )%return. -(** [paper::call_choose]: forward function *) +(** [paper::call_choose]: forward function + Source: 'src/paper.rs', lines 76:0-76:44 *) Definition call_choose (p : (u32 * u32)) : result u32 := let (px, py) := p in pz <- choose u32 true px py; |