diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 39 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 132 | ||||
| -rw-r--r-- | tests/coq/misc/Paper.v | 24 |
3 files changed, 94 insertions, 101 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 9aaf753e..13c02bca 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1476,25 +1476,34 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_open_hovbox fmt ctx.indent_incr; let then_or_else = if is_then then "then" else "else" in F.pp_print_string fmt then_or_else; - F.pp_print_space fmt (); - (* Open a box for the branch *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the [begin] if necessary *) let parenth = PureUtils.let_group_requires_parentheses e_branch in - let left_delim, right_delim = - match !backend with FStar -> ("begin", "end") | Coq -> ("(", ")") - in - if parenth then ( - F.pp_print_string fmt left_delim; - F.pp_print_space fmt ()); + (* Open a box for the branch - we do this only if it is not a parenthesized + group of nested let bindings. + *) + if not parenth then ( + F.pp_print_space fmt (); + F.pp_open_hovbox fmt ctx.indent_incr); + (* Open the parenthesized expression *) + (if parenth then + match !backend with + | FStar -> + F.pp_print_space fmt (); + F.pp_print_string fmt "begin"; + F.pp_print_space fmt () + | Coq -> + F.pp_print_string fmt " ("; + F.pp_print_cut fmt ()); (* Print the branch expression *) extract_texpression ctx fmt false e_branch; - (* Close the [begin ... end ] *) - if parenth then ( - F.pp_print_space fmt (); - F.pp_print_string fmt right_delim); + (* Close the parenthesized expression *) + (if parenth then + match !backend with + | FStar -> + F.pp_print_space fmt (); + F.pp_print_string fmt "end" + | Coq -> F.pp_print_string fmt ")"); (* Close the box for the branch *) - F.pp_close_box fmt (); + if not parenth then F.pp_close_box fmt (); (* Close the box for the then/else+branch *) F.pp_close_box fmt () in diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 9075d01d..774b8a1e 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -210,13 +210,12 @@ Definition choose_test_fwd : result unit := z0 <- i32_add z 1 %i32; if negb (z0 s= 1 %i32) then Fail_ - else - ( - p <- choose_back i32 true (0 %i32) (0 %i32) z0; - let (x, y) := p in - if negb (x s= 1 %i32) - then Fail_ - else if negb (y s= 0 %i32) then Fail_ else Return tt ) + else ( + p <- choose_back i32 true (0 %i32) (0 %i32) z0; + let (x, y) := p in + if negb (x s= 1 %i32) + then Fail_ + else if negb (y s= 0 %i32) then Fail_ else Return tt) . (** Unit test for [no_nested_borrows::choose_test] *) @@ -258,7 +257,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T := | ListCons x tl => if i s= 0 %u32 then Return x - else ( i0 <- u32_sub i 1 %u32; t <- list_nth_shared_fwd T tl i0; Return t ) + else (i0 <- u32_sub i 1 %u32; t <- list_nth_shared_fwd T tl i0; Return t) | ListNil => Fail_ end . @@ -269,7 +268,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := | ListCons x tl => 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_ end . @@ -281,11 +280,10 @@ Fixpoint list_nth_mut_back | ListCons x tl => if i s= 0 %u32 then Return (ListCons ret tl) - else - ( - i0 <- u32_sub i 1 %u32; - tl0 <- list_nth_mut_back T tl i0 ret; - Return (ListCons x tl0) ) + else ( + i0 <- u32_sub i 1 %u32; + tl0 <- list_nth_mut_back T tl i0 ret; + Return (ListCons x tl0)) | ListNil => Fail_ end . @@ -314,39 +312,30 @@ Definition test_list_functions_fwd : result unit := i <- list_length_fwd i32 (ListCons (0 %i32) l1); if negb (i s= 3 %u32) then Fail_ - else - ( - i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32); - if negb (i0 s= 0 %i32) + else ( + i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32); + if negb (i0 s= 0 %i32) + then Fail_ + else ( + i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32); + if negb (i1 s= 1 %i32) then Fail_ - else - ( - i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32); - if negb (i1 s= 1 %i32) + else ( + i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32); + if negb (i2 s= 2 %i32) + then Fail_ + else ( + ls <- list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3 %i32); + i3 <- list_nth_shared_fwd i32 ls (0 %u32); + if negb (i3 s= 0 %i32) then Fail_ - else - ( - i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32); - if negb (i2 s= 2 %i32) - then Fail_ - else - ( - ls <- - list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3 - %i32); - i3 <- list_nth_shared_fwd i32 ls (0 %u32); - if negb (i3 s= 0 %i32) - then Fail_ - else - ( - i4 <- list_nth_shared_fwd i32 ls (1 %u32); - if negb (i4 s= 3 %i32) - then Fail_ - else - ( - i5 <- list_nth_shared_fwd i32 ls (2 %u32); - if negb (i5 s= 2 %i32) then Fail_ else Return tt ) ) - ) ) ) ) + else ( + i4 <- list_nth_shared_fwd i32 ls (1 %u32); + if negb (i4 s= 3 %i32) + then Fail_ + else ( + i5 <- list_nth_shared_fwd i32 ls (2 %u32); + if negb (i5 s= 2 %i32) then Fail_ else Return tt)))))) . (** Unit test for [no_nested_borrows::test_list_functions] *) @@ -448,34 +437,31 @@ Definition test_constants_fwd : result unit := let (i, _) := p in if negb (i s= 1 %u32) then Fail_ - else - ( - swt0 <- new_tuple2_fwd; - match swt0 with - | mkStruct_with_tuple_t p0 => - let (i0, _) := p0 in - if negb (i0 s= 1 %i16) - then Fail_ - else - ( - swt1 <- new_tuple3_fwd; - match swt1 with - | mkStruct_with_tuple_t p1 => - let (i1, _) := p1 in - if negb (i1 s= 1 %u64) - then Fail_ - else - ( - swp <- new_pair1_fwd; - match swp with - | mkStruct_with_pair_t p2 => - match p2 with - | mkPair_t i2 i3 => - if negb (i2 s= 1 %u32) then Fail_ else Return tt - end - end ) - end ) - end ) + else ( + swt0 <- new_tuple2_fwd; + match swt0 with + | mkStruct_with_tuple_t p0 => + let (i0, _) := p0 in + if negb (i0 s= 1 %i16) + then Fail_ + else ( + swt1 <- new_tuple3_fwd; + match swt1 with + | mkStruct_with_tuple_t p1 => + let (i1, _) := p1 in + if negb (i1 s= 1 %u64) + then Fail_ + else ( + swp <- new_pair1_fwd; + match swp with + | mkStruct_with_pair_t p2 => + match p2 with + | mkPair_t i2 i3 => + if negb (i2 s= 1 %u32) then Fail_ else Return tt + end + end) + end) + end) end . diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index e15e0dc1..25c01d7b 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -34,13 +34,12 @@ Definition test_choose_fwd : result unit := z0 <- i32_add z 1 %i32; if negb (z0 s= 1 %i32) then Fail_ - else - ( - p <- choose_back i32 true (0 %i32) (0 %i32) z0; - let (x, y) := p in - if negb (x s= 1 %i32) - then Fail_ - else if negb (y s= 0 %i32) then Fail_ else Return tt ) + else ( + p <- choose_back i32 true (0 %i32) (0 %i32) z0; + let (x, y) := p in + if negb (x s= 1 %i32) + then Fail_ + else if negb (y s= 0 %i32) then Fail_ else Return tt) . (** Unit test for [paper::test_choose] *) @@ -61,7 +60,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := | ListCons x tl => 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_ end . @@ -73,11 +72,10 @@ Fixpoint list_nth_mut_back | ListCons x tl => if i s= 0 %u32 then Return (ListCons ret tl) - else - ( - i0 <- u32_sub i 1 %u32; - tl0 <- list_nth_mut_back T tl i0 ret; - Return (ListCons x tl0) ) + else ( + i0 <- u32_sub i 1 %u32; + tl0 <- list_nth_mut_back T tl i0 ret; + Return (ListCons x tl0)) | ListNil => Fail_ end . |