diff options
author | Son Ho | 2022-11-14 09:27:24 +0100 |
---|---|---|
committer | Son HO | 2022-11-14 14:21:04 +0100 |
commit | 1af63cade04325eb32a62ca23125eea75810822f (patch) | |
tree | 3aa1a74d5f59a8c197154ea48e7cf0b8da3f0f68 /tests/coq/misc/External__Funs.v | |
parent | 3eba613a9ff9d5c265fbe2676f6bd324728d9ca4 (diff) |
Improve the formatting of the generated code
Diffstat (limited to '')
-rw-r--r-- | tests/coq/misc/External__Funs.v | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v index 021acd6e..e8ecfab8 100644 --- a/tests/coq/misc/External__Funs.v +++ b/tests/coq/misc/External__Funs.v @@ -18,7 +18,8 @@ Definition swap_fwd p0 <- core_mem_swap_back0 T x y st st0; let (st1, _) := p0 in p1 <- core_mem_swap_back1 T x y st st1; - let (st2, _) := p1 in Return (st2, tt) + let (st2, _) := p1 in + Return (st2, tt) . (** [external::swap] *) @@ -31,7 +32,8 @@ Definition swap_back p0 <- core_mem_swap_back0 T x y st st1; let (st2, x0) := p0 in p1 <- core_mem_swap_back1 T x y st st2; - let (_, y0) := p1 in Return (st0, (x0, y0)) + let (_, y0) := p1 in + Return (st0, (x0, y0)) . (** [external::test_new_non_zero_u32] *) @@ -40,13 +42,16 @@ Definition test_new_non_zero_u32_fwd p <- core_num_nonzero_non_zero_u32_new_fwd x st; let (st0, opt) := p in p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0; - let (st1, nzu) := p0 in Return (st1, nzu) + 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); let _ := v0 in Return tt + v0 <- vec_push_back u32 v (0 %u32); + let _ := v0 in + Return tt . (** [external::custom_swap] *) @@ -57,7 +62,8 @@ Definition custom_swap_fwd p0 <- core_mem_swap_back0 T x y st st0; let (st1, x0) := p0 in p1 <- core_mem_swap_back1 T x y st st1; - let (st2, _) := p1 in Return (st2, x0) + let (st2, _) := p1 in + Return (st2, x0) . (** [external::custom_swap] *) @@ -70,7 +76,8 @@ Definition custom_swap_back p0 <- core_mem_swap_back0 T x y st st1; let (st2, _) := p0 in p1 <- core_mem_swap_back1 T x y st st2; - let (_, y0) := p1 in Return (st0, (ret, y0)) + let (_, y0) := p1 in + Return (st0, (ret, y0)) . (** [external::test_custom_swap] *) @@ -84,7 +91,9 @@ Definition test_custom_swap_back result (state * (u32 * u32)) := 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)) + let (st1, p0) := p in + let (x0, y0) := p0 in + Return (st1, (x0, y0)) . (** [external::test_swap_non_zero] *) @@ -94,7 +103,8 @@ Definition test_swap_non_zero_fwd let (st0, _) := p in 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_ else Return (st1, x0) + let (x0, _) := p1 in + if x0 s= 0 %u32 then Fail_ else Return (st1, x0) . End External__Funs . |