diff options
Diffstat (limited to 'tests/coq/misc/Paper.v')
-rw-r--r-- | tests/coq/misc/Paper.v | 23 |
1 files changed, 10 insertions, 13 deletions
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 77276223..5995de15 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 := - x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt + x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Ok tt . (** Unit test for [paper::test_incr] *) @@ -27,8 +27,8 @@ Check (test_incr )%return. Definition choose (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) := if b - then let back := fun (ret : T) => Return (ret, y) in Return (x, back) - else let back := fun (ret : T) => Return (x, ret) in Return (y, back) + then let back := fun (ret : T) => Ok (ret, y) in Ok (x, back) + else let back := fun (ret : T) => Ok (x, ret) in Ok (y, back) . (** [paper::test_choose]: @@ -44,7 +44,7 @@ Definition test_choose : result unit := let (x, y) := p1 in if negb (x s= 1%i32) then Fail_ Failure - else if negb (y s= 0%i32) then Fail_ Failure else Return tt) + else if negb (y s= 0%i32) then Fail_ Failure else Ok tt) . (** Unit test for [paper::test_choose] *) @@ -69,17 +69,14 @@ Fixpoint list_nth_mut match l with | List_Cons x tl => if i s= 0%u32 - then - let back := fun (ret : T) => Return (List_Cons ret tl) in - Return (x, back) + then let back := fun (ret : T) => Ok (List_Cons ret tl) in Ok (x, back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut T tl i1; let (t, list_nth_mut_back) := p in let back := - fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1) - in - Return (t, back)) + fun (ret : T) => tl1 <- list_nth_mut_back ret; Ok (List_Cons x tl1) in + Ok (t, back)) | List_Nil => Fail_ Failure end . @@ -89,7 +86,7 @@ Fixpoint list_nth_mut Fixpoint sum (l : List_t i32) : result i32 := match l with | List_Cons x tl => i <- sum tl; i32_add x i - | List_Nil => Return 0%i32 + | List_Nil => Ok 0%i32 end . @@ -103,7 +100,7 @@ Definition test_nth : result unit := x1 <- i32_add x 1%i32; l2 <- list_nth_mut_back x1; i <- sum l2; - if negb (i s= 7%i32) then Fail_ Failure else Return tt + if negb (i s= 7%i32) then Fail_ Failure else Ok tt . (** Unit test for [paper::test_nth] *) @@ -118,7 +115,7 @@ Definition call_choose (p : (u32 * u32)) : result u32 := pz1 <- u32_add pz 1%u32; p2 <- choose_back pz1; let (px1, _) := p2 in - Return px1 + Ok px1 . End Paper. |