diff options
Diffstat (limited to 'tests/coq/misc/External__Funs.v')
-rw-r--r-- | tests/coq/misc/External__Funs.v | 39 |
1 files changed, 20 insertions, 19 deletions
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v index cc9e9461..e7020040 100644 --- a/tests/coq/misc/External__Funs.v +++ b/tests/coq/misc/External__Funs.v @@ -4,11 +4,11 @@ Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Local Open Scope Primitives_scope. -Require Export External__Types . -Import External__Types . -Require Export External__Opaque . -Import External__Opaque . -Module External__Funs . +Require Export External__Types. +Import External__Types. +Require Export External__Opaque. +Import External__Opaque. +Module External__Funs. (** [external::swap] *) Definition swap_fwd @@ -20,7 +20,7 @@ Definition swap_fwd p1 <- core_mem_swap_back1 T x y st st1; let (st2, _) := p1 in Return (st2, tt) - . +. (** [external::swap] *) Definition swap_back @@ -34,7 +34,7 @@ Definition swap_back p1 <- core_mem_swap_back1 T x y st st2; let (_, y0) := p1 in Return (st0, (x0, y0)) - . +. (** [external::test_new_non_zero_u32] *) Definition test_new_non_zero_u32_fwd @@ -44,15 +44,15 @@ Definition test_new_non_zero_u32_fwd p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0; let (st1, nzu) := p0 in Return (st1, nzu) - . +. (** [external::test_vec] *) Definition test_vec_fwd : result unit := let v := vec_new u32 in - v0 <- vec_push_back u32 v (0 %u32); + v0 <- vec_push_back u32 v (0%u32); let _ := v0 in Return tt - . +. (** Unit test for [external::test_vec] *) Check (test_vec_fwd )%return. @@ -67,7 +67,7 @@ Definition custom_swap_fwd p1 <- core_mem_swap_back1 T x y st st1; let (st2, _) := p1 in Return (st2, x0) - . +. (** [external::custom_swap] *) Definition custom_swap_back @@ -81,33 +81,34 @@ Definition custom_swap_back p1 <- core_mem_swap_back1 T x y st st2; let (_, y0) := p1 in Return (st0, (ret, y0)) - . +. (** [external::test_custom_swap] *) 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) . + p <- custom_swap_fwd u32 x y st; let (st0, _) := p in Return (st0, tt) +. (** [external::test_custom_swap] *) Definition test_custom_swap_back (x : u32) (y : u32) (st : state) (st0 : state) : result (state * (u32 * u32)) := - p <- custom_swap_back u32 x y st (1 %u32) st0; + p <- custom_swap_back u32 x y st (1%u32) st0; let (st1, p0) := p in let (x0, y0) := p0 in Return (st1, (x0, y0)) - . +. (** [external::test_swap_non_zero] *) Definition test_swap_non_zero_fwd (x : u32) (st : state) : result (state * u32) := - p <- swap_fwd u32 x (0 %u32) st; + p <- swap_fwd u32 x (0%u32) st; let (st0, _) := p in - p0 <- swap_back u32 x (0 %u32) st st0; + p0 <- swap_back u32 x (0%u32) st st0; let (st1, p1) := p0 in let (x0, _) := p1 in - if x0 s= 0 %u32 then Fail_ Failure else Return (st1, x0) - . + if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0) +. End External__Funs . |