diff options
author | Son Ho | 2022-11-15 15:23:16 +0100 |
---|---|---|
committer | Son HO | 2022-11-16 15:45:32 +0100 |
commit | bd5706896dec0a1aef1accdf51f93af00c5dc6fe (patch) | |
tree | 09dd5431d351c8ef894092ea25fd9d2af54d3d6e /tests/coq/misc/Paper.v | |
parent | dbb5d549176edd60440e689fd28c529944bc6e51 (diff) |
Improve formatting
Diffstat (limited to '')
-rw-r--r-- | tests/coq/misc/Paper.v | 69 |
1 files changed, 36 insertions, 33 deletions
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index d0c99883..616eed37 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -4,43 +4,46 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Module Paper . +Module Paper. (** [paper::ref_incr] *) Definition ref_incr_fwd_back (x : i32) : result i32 := - x0 <- i32_add x 1 %i32; Return x0 . + x0 <- i32_add x 1%i32; Return x0 +. (** [paper::test_incr] *) 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 - . + x <- ref_incr_fwd_back (0%i32); + if negb (x s= 1%i32) then Fail_ Failure else Return tt +. (** Unit test for [paper::test_incr] *) Check (test_incr_fwd )%return. (** [paper::choose] *) Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T := - if b then Return x else Return y . + if b then Return x else Return y +. (** [paper::choose] *) 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) . + if b then Return (ret, y) else Return (x, ret) +. (** [paper::test_choose] *) Definition test_choose_fwd : result unit := - z <- choose_fwd i32 true (0 %i32) (0 %i32); - z0 <- i32_add z 1 %i32; - if negb (z0 s= 1 %i32) + z <- choose_fwd i32 true (0%i32) (0%i32); + z0 <- i32_add z 1%i32; + if negb (z0 s= 1%i32) then Fail_ Failure else ( - p <- choose_back i32 true (0 %i32) (0 %i32) z0; + p <- choose_back i32 true (0%i32) (0%i32) z0; let (x, y) := p in - if negb (x s= 1 %i32) + 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 Return tt) +. (** Unit test for [paper::test_choose] *) Check (test_choose_fwd )%return. @@ -51,54 +54,54 @@ Inductive List_t (T : Type) := | ListNil : List_t T . -Arguments ListCons {T} _ _ . -Arguments ListNil {T} . +Arguments ListCons {T} _ _. +Arguments ListNil {T}. (** [paper::list_nth_mut] *) Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := match l with | ListCons x tl => - if i s= 0 %u32 + if i s= 0%u32 then Return x - else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t) + else (i0 <- u32_sub i 1%u32; t <- list_nth_mut_fwd T tl i0; Return t) | ListNil => Fail_ Failure end - . +. (** [paper::list_nth_mut] *) Fixpoint list_nth_mut_back (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) := match l with | ListCons x tl => - if i s= 0 %u32 + if i s= 0%u32 then Return (ListCons ret tl) else ( - i0 <- u32_sub i 1 %u32; + i0 <- u32_sub i 1%u32; tl0 <- list_nth_mut_back T tl i0 ret; Return (ListCons x tl0)) | ListNil => Fail_ Failure end - . +. (** [paper::sum] *) Fixpoint sum_fwd (l : List_t i32) : result i32 := match l with | ListCons x tl => i <- sum_fwd tl; i0 <- i32_add x i; Return i0 - | ListNil => Return (0 %i32) + | ListNil => Return (0%i32) end - . +. (** [paper::test_nth] *) Definition test_nth_fwd : result unit := let l := ListNil in - let l0 := ListCons (3 %i32) l in - let l1 := ListCons (2 %i32) l0 in - x <- list_nth_mut_fwd i32 (ListCons (1 %i32) l1) (2 %u32); - x0 <- i32_add x 1 %i32; - l2 <- list_nth_mut_back i32 (ListCons (1 %i32) l1) (2 %u32) x0; + let l0 := ListCons (3%i32) l in + let l1 := ListCons (2%i32) l0 in + x <- list_nth_mut_fwd i32 (ListCons (1%i32) l1) (2%u32); + x0 <- i32_add x 1%i32; + l2 <- list_nth_mut_back i32 (ListCons (1%i32) l1) (2%u32) x0; i <- sum_fwd l2; - if negb (i s= 7 %i32) then Fail_ Failure else Return tt - . + if negb (i s= 7%i32) then Fail_ Failure else Return tt +. (** Unit test for [paper::test_nth] *) Check (test_nth_fwd )%return. @@ -107,10 +110,10 @@ Check (test_nth_fwd )%return. Definition call_choose_fwd (p : (u32 * u32)) : result u32 := let (px, py) := p in pz <- choose_fwd u32 true px py; - pz0 <- u32_add pz 1 %u32; + pz0 <- u32_add pz 1%u32; p0 <- choose_back u32 true px py pz0; let (px0, _) := p0 in Return px0 - . +. End Paper . |