summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/ExtractToFStar.ml47
-rw-r--r--src/PureMicroPasses.ml15
-rw-r--r--tests/hashmap/Hashmap.Funs.fst140
-rw-r--r--tests/misc/NoNestedBorrows.fst42
-rw-r--r--tests/misc/Paper.fst17
5 files changed, 138 insertions, 123 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index a1b3f4d4..50a98093 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -766,7 +766,11 @@ let extract_place (ctx : extraction_ctx) (fmt : F.formatter) (p : place) : unit
F.pp_print_string fmt ".";
F.pp_print_string fmt field_name
in
- extract_projection p.projection
+ (* We allow to break where "." appears, but we try to prevent that by
+ * wrapping in a box *)
+ F.pp_open_hovbox fmt ctx.indent_incr;
+ extract_projection p.projection;
+ F.pp_close_box fmt ()
(** [inside]: see [extract_ty] *)
let rec extract_typed_rvalue (ctx : extraction_ctx) (fmt : F.formatter)
@@ -783,20 +787,33 @@ let rec extract_typed_rvalue (ctx : extraction_ctx) (fmt : F.formatter)
extract_adt_g_value extract_value fmt ctx inside av.variant_id
av.field_values v.ty
-(** [inside]: see [extract_ty] *)
+(** [inner]: "inner-expression": controls how we break *value* expressions over
+ several lines. If `false`, we wrap the expression in an hovbox. Otherwise,
+ we don't wrap.
+ This is important when we have an expression like `Return (...)`: we want
+ to wrap it in an hovbox. However, when formatting function arguments, we
+ to want to introduce any additional box (because the whole function call
+ itself is in a box).
+
+ [inside]: controls the introduction of parentheses. See [extract_ty]
+ *)
let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
- (inside : bool) (e : texpression) : unit =
+ (inner : bool) (inside : bool) (e : texpression) : unit =
match e.e with
| Value (rv, _) ->
+ if not inner then F.pp_open_hovbox fmt ctx.indent_incr;
let _ = extract_typed_rvalue ctx fmt inside rv in
+ if not inner then F.pp_close_box fmt ();
()
| Call call -> (
match (call.func, call.args) with
| Unop unop, [ arg ] ->
- ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
+ ctx.fmt.extract_unop
+ (extract_texpression ctx fmt true)
+ fmt inside unop arg
| Binop (binop, int_ty), [ arg0; arg1 ] ->
ctx.fmt.extract_binop
- (extract_texpression ctx fmt)
+ (extract_texpression ctx fmt true)
fmt inside binop int_ty arg0 arg1
| Regular (fun_id, rg_id), _ ->
if inside then F.pp_print_string fmt "(";
@@ -815,7 +832,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun ve ->
F.pp_print_space fmt ();
- extract_texpression ctx fmt true ve)
+ extract_texpression ctx fmt true true ve)
call.args;
(* Close the box for the function call *)
F.pp_close_box fmt ();
@@ -833,7 +850,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "<--";
F.pp_print_space fmt ();
- extract_texpression ctx fmt false re;
+ extract_texpression ctx fmt true false re;
F.pp_print_string fmt ";";
ctx)
else (
@@ -843,7 +860,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "=";
F.pp_print_space fmt ();
- extract_texpression ctx fmt false re;
+ extract_texpression ctx fmt true false re;
F.pp_print_space fmt ();
F.pp_print_string fmt "in";
ctx)
@@ -852,7 +869,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ();
(* Print the next expression *)
F.pp_print_space fmt ();
- extract_texpression ctx fmt inside next_e
+ extract_texpression ctx fmt inner inside next_e
| Switch (scrut, body) -> (
match body with
| If (e_then, e_else) ->
@@ -862,7 +879,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hovbox fmt ctx.indent_incr;
F.pp_print_string fmt "if";
F.pp_print_space fmt ();
- extract_texpression ctx fmt false scrut;
+ extract_texpression ctx fmt true false scrut;
(* Close the box for the `if` *)
F.pp_close_box fmt ();
(* Extract the branches *)
@@ -881,7 +898,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "begin";
F.pp_print_space fmt ());
(* Print the branch expression *)
- extract_texpression ctx fmt false e_branch;
+ extract_texpression ctx fmt false false e_branch;
(* Close the `begin ... end ` *)
if parenth then (
F.pp_print_space fmt ();
@@ -904,7 +921,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
(* Print the `match ... with` *)
F.pp_print_string fmt "begin match";
F.pp_print_space fmt ();
- extract_texpression ctx fmt false scrut;
+ extract_texpression ctx fmt true false scrut;
F.pp_print_space fmt ();
F.pp_print_string fmt "with";
(* Close the box for the `match ... with` *)
@@ -925,7 +942,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the branch *)
F.pp_open_hvbox fmt 0;
(* Print the branch itself *)
- extract_texpression ctx fmt false br.branch;
+ extract_texpression ctx fmt false false br.branch;
(* Close the box for the branch *)
F.pp_close_box fmt ();
(* Close the box for the pattern+branch *)
@@ -939,7 +956,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "end";
(* Close the box for the whole match *)
F.pp_close_box fmt ())
- | Meta (_, e) -> extract_texpression ctx fmt inside e
+ | Meta (_, e) -> extract_texpression ctx fmt inner inside e
(** A small utility to print the parameters of a function signature.
@@ -1164,7 +1181,7 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the body *)
F.pp_open_hvbox fmt 0;
(* Extract the body *)
- let _ = extract_texpression ctx_body fmt false def.body in
+ let _ = extract_texpression ctx_body fmt false false def.body in
(* Close the box for the body *)
F.pp_close_box fmt ();
(* Close the box for the definition *)
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 9b9107d1..40a4be56 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -429,7 +429,20 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
else if p.projection = [] then self#visit_expression env ne.e
else super#visit_Value env v mp)
| _ -> (* No substitution *) super#visit_Value env v mp
- (** Visit the places used as rvalues, to substitute them if necessary *)
+ (** Visit the values, to substitute them if possible *)
+
+ method! visit_RvPlace env p =
+ if p.projection = [] then
+ match VarId.Map.find_opt p.var env with
+ | None -> (* No substitution *) super#visit_RvPlace env p
+ | Some ne -> (
+ (* Substitute if the new expression is a value *)
+ match ne.e with
+ | Value (nv, _) -> super#visit_rvalue env nv.value
+ | _ -> (* Not a value *) super#visit_RvPlace env p)
+ else (* TODO: project *)
+ super#visit_RvPlace env p
+ (** Visit the places used as rvalues, to substitute them if possible *)
end
in
let body = obj#visit_texpression VarId.Map.empty def.body in
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 4aa6f02c..318b0cf4 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -8,7 +8,7 @@ include Hashmap.Clauses
#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
(** [hashmap::hash_key] *)
-let hash_key_fwd (k : usize) : result usize = let i = k in Return i
+let hash_key_fwd (k : usize) : result usize = Return k
(** [hashmap::HashMap::allocate_slots] *)
let rec hash_map_allocate_slots_fwd
@@ -78,25 +78,25 @@ let rec hash_map_clear_slots_fwd_back
| Return i1 ->
begin match hash_map_clear_slots_fwd_back t v i1 with
| Fail -> Fail
- | Return v0 -> let slots0 = v0 in Return slots0
+ | Return v0 -> Return v0
end
end
end
- else let slots0 = slots in Return slots0
+ else Return slots
(** [hashmap::HashMap::clear] *)
let hash_map_clear_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
- let p = self.hash_map_max_load_factor in
- let i = self.hash_map_max_load in
begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with
| Fail -> Fail
- | Return v -> let self0 = Mkhash_map_t 0 p i v in Return self0
+ | Return v ->
+ Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load
+ v)
end
(** [hashmap::HashMap::len] *)
let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
- let i = self.hash_map_num_entries in Return i
+ Return self.hash_map_num_entries
(** [hashmap::HashMap::insert_in_list] *)
let rec hash_map_insert_in_list_fwd
@@ -125,13 +125,13 @@ let rec hash_map_insert_in_list_back
begin match ls with
| ListCons ckey cvalue ls0 ->
if ckey = key
- then let ls1 = ListCons ckey value ls0 in Return ls1
+ then Return (ListCons ckey value ls0)
else
begin match hash_map_insert_in_list_back t key value ls0 with
| Fail -> Fail
- | Return l -> let ls1 = ListCons ckey cvalue l in Return ls1
+ | Return l -> Return (ListCons ckey cvalue l)
end
- | ListNil -> let l = ListNil in let ls0 = ListCons key value l in Return ls0
+ | ListNil -> let l = ListNil in Return (ListCons key value l)
end
(** [hashmap::HashMap::insert_no_resize] *)
@@ -142,11 +142,8 @@ let hash_map_insert_no_resize_fwd_back
begin match hash_key_fwd key with
| Fail -> Fail
| Return i ->
- let i0 = self.hash_map_num_entries in
- let p = self.hash_map_max_load_factor in
- let i1 = self.hash_map_max_load in
- let i2 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i2 with
+ let i0 = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem i i0 with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
@@ -160,7 +157,7 @@ let hash_map_insert_no_resize_fwd_back
then
begin match usize_add self.hash_map_num_entries 1 with
| Fail -> Fail
- | Return i3 ->
+ | Return i1 ->
begin match hash_map_insert_in_list_back t key value l with
| Fail -> Fail
| Return l0 ->
@@ -169,7 +166,8 @@ let hash_map_insert_no_resize_fwd_back
with
| Fail -> Fail
| Return v ->
- let self0 = Mkhash_map_t i3 p i1 v in Return self0
+ Return (Mkhash_map_t i1 self.hash_map_max_load_factor
+ self.hash_map_max_load v)
end
end
end
@@ -181,7 +179,10 @@ let hash_map_insert_no_resize_fwd_back
vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
with
| Fail -> Fail
- | Return v -> let self0 = Mkhash_map_t i0 p i1 v in Return self0
+ | Return v ->
+ Return (Mkhash_map_t self.hash_map_num_entries
+ self.hash_map_max_load_factor self.hash_map_max_load
+ v)
end
end
end
@@ -202,10 +203,10 @@ let rec hash_map_move_elements_from_list_fwd_back
| Return h ->
begin match hash_map_move_elements_from_list_fwd_back t h tl with
| Fail -> Fail
- | Return h0 -> let ntable0 = h0 in Return ntable0
+ | Return h0 -> Return h0
end
end
- | ListNil -> let ntable0 = ntable in Return ntable0
+ | ListNil -> Return ntable
end
(** [hashmap::HashMap::move_elements] *)
@@ -233,51 +234,46 @@ let rec hash_map_move_elements_fwd_back
| Return i1 ->
begin match hash_map_move_elements_fwd_back t h v i1 with
| Fail -> Fail
- | Return (h0, v0) ->
- let ntable0 = h0 in let slots0 = v0 in Return (ntable0, slots0)
+ | Return (h0, v0) -> Return (h0, v0)
end
end
end
end
end
- else let ntable0 = ntable in let slots0 = slots in Return (ntable0, slots0)
+ else Return (ntable, slots)
(** [hashmap::HashMap::try_resize] *)
let hash_map_try_resize_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
- let i = self.hash_map_num_entries in
- let i0 = self.hash_map_max_load in
- let v = self.hash_map_slots in
- let i1 = vec_len (list_t t) self.hash_map_slots in
+ let i = vec_len (list_t t) self.hash_map_slots in
begin match usize_div 4294967295 2 with
| Fail -> Fail
| Return n1 ->
- let (i2, i3) = self.hash_map_max_load_factor in
- begin match usize_div n1 i2 with
+ let (i0, i1) = self.hash_map_max_load_factor in
+ begin match usize_div n1 i0 with
| Fail -> Fail
- | Return i4 ->
- if i1 <= i4
+ | Return i2 ->
+ if i <= i2
then
- begin match usize_mul i1 2 with
+ begin match usize_mul i 2 with
| Fail -> Fail
- | Return i5 ->
- begin match hash_map_new_with_capacity_fwd t i5 i2 i3 with
+ | Return i3 ->
+ begin match hash_map_new_with_capacity_fwd t i3 i0 i1 with
| Fail -> Fail
| Return h ->
begin match
hash_map_move_elements_fwd_back t h self.hash_map_slots 0 with
| Fail -> Fail
- | Return (h0, v0) ->
- let i6 = h0.hash_map_max_load in
- let v1 = mem_replace_back (vec (list_t t)) v0 h0.hash_map_slots
- in
- let self0 = Mkhash_map_t i (i2, i3) i6 v1 in
- Return
- self0
+ | Return (h0, v) ->
+ let v0 = mem_replace_back (vec (list_t t)) v h0.hash_map_slots in
+ Return (Mkhash_map_t self.hash_map_num_entries (i0, i1)
+ h0.hash_map_max_load v0)
end
end
end
- else let self0 = Mkhash_map_t i (i2, i3) i0 v in Return self0
+ else
+ Return (Mkhash_map_t self.hash_map_num_entries (i0, i1)
+ self.hash_map_max_load self.hash_map_slots)
end
end
@@ -292,18 +288,18 @@ let hash_map_insert_fwd_back
begin match hash_map_len_fwd t h with
| Fail -> Fail
| Return i ->
- let i0 = h.hash_map_num_entries in
- let p = h.hash_map_max_load_factor in
- let i1 = h.hash_map_max_load in
- let v = h.hash_map_slots in
if i > h.hash_map_max_load
then
- begin match hash_map_try_resize_fwd_back t (Mkhash_map_t i0 p i1 v)
+ begin match
+ hash_map_try_resize_fwd_back t (Mkhash_map_t h.hash_map_num_entries
+ h.hash_map_max_load_factor h.hash_map_max_load h.hash_map_slots)
with
| Fail -> Fail
- | Return h0 -> let self0 = h0 in Return self0
+ | Return h0 -> Return h0
end
- else let self0 = Mkhash_map_t i0 p i1 v in Return self0
+ else
+ Return (Mkhash_map_t h.hash_map_num_entries h.hash_map_max_load_factor
+ h.hash_map_max_load h.hash_map_slots)
end
end
@@ -358,7 +354,7 @@ let rec hash_map_get_in_list_fwd
else
begin match hash_map_get_in_list_fwd t key ls0 with
| Fail -> Fail
- | Return x -> let x0 = x in Return x0
+ | Return x -> Return x
end
| ListNil -> Fail
end
@@ -378,7 +374,7 @@ let hash_map_get_fwd
| Return l ->
begin match hash_map_get_in_list_fwd t key l with
| Fail -> Fail
- | Return x -> let x0 = x in Return x0
+ | Return x -> Return x
end
end
end
@@ -396,7 +392,7 @@ let rec hash_map_get_mut_in_list_fwd
else
begin match hash_map_get_mut_in_list_fwd t key ls0 with
| Fail -> Fail
- | Return x -> let x0 = x in Return x0
+ | Return x -> Return x
end
| ListNil -> Fail
end
@@ -410,11 +406,11 @@ let rec hash_map_get_mut_in_list_back
begin match ls with
| ListCons ckey cvalue ls0 ->
if ckey = key
- then let x = ret in let ls1 = ListCons ckey x ls0 in Return ls1
+ then Return (ListCons ckey ret ls0)
else
begin match hash_map_get_mut_in_list_back t key ls0 ret with
| Fail -> Fail
- | Return l -> let ls1 = ListCons ckey cvalue l in Return ls1
+ | Return l -> Return (ListCons ckey cvalue l)
end
| ListNil -> Fail
end
@@ -435,7 +431,7 @@ let hash_map_get_mut_fwd
| Return l ->
begin match hash_map_get_mut_in_list_fwd t key l with
| Fail -> Fail
- | Return x -> let x0 = x in Return x0
+ | Return x -> Return x
end
end
end
@@ -449,11 +445,8 @@ let hash_map_get_mut_back
begin match hash_key_fwd key with
| Fail -> Fail
| Return i ->
- let i0 = self.hash_map_num_entries in
- let p = self.hash_map_max_load_factor in
- let i1 = self.hash_map_max_load in
- let i2 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i2 with
+ let i0 = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem i i0 with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
@@ -466,7 +459,9 @@ let hash_map_get_mut_back
begin match
vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with
| Fail -> Fail
- | Return v -> let self0 = Mkhash_map_t i0 p i1 v in Return self0
+ | Return v ->
+ Return (Mkhash_map_t self.hash_map_num_entries
+ self.hash_map_max_load_factor self.hash_map_max_load v)
end
end
end
@@ -508,15 +503,15 @@ let rec hash_map_remove_from_list_back
then
let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
begin match mv_ls with
- | ListCons i cvalue tl0 -> let ls0 = tl0 in Return ls0
+ | ListCons i cvalue tl0 -> Return tl0
| ListNil -> Fail
end
else
begin match hash_map_remove_from_list_back t key tl with
| Fail -> Fail
- | Return l -> let ls0 = ListCons ckey x l in Return ls0
+ | Return l -> Return (ListCons ckey x l)
end
- | ListNil -> let ls0 = ListNil in Return ls0
+ | ListNil -> Return ListNil
end
(** [hashmap::HashMap::remove] *)
@@ -555,11 +550,8 @@ let hash_map_remove_back
begin match hash_key_fwd key with
| Fail -> Fail
| Return i ->
- let i0 = self.hash_map_num_entries in
- let p = self.hash_map_max_load_factor in
- let i1 = self.hash_map_max_load in
- let i2 = vec_len (list_t t) self.hash_map_slots in
- begin match usize_rem i i2 with
+ let i0 = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_rem i i0 with
| Fail -> Fail
| Return hash_mod ->
begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
@@ -578,13 +570,16 @@ let hash_map_remove_back
vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
with
| Fail -> Fail
- | Return v -> let self0 = Mkhash_map_t i0 p i1 v in Return self0
+ | Return v ->
+ Return (Mkhash_map_t self.hash_map_num_entries
+ self.hash_map_max_load_factor self.hash_map_max_load
+ v)
end
end
| Some x0 ->
begin match usize_sub self.hash_map_num_entries 1 with
| Fail -> Fail
- | Return i3 ->
+ | Return i1 ->
begin match hash_map_remove_from_list_back t key l with
| Fail -> Fail
| Return l0 ->
@@ -593,7 +588,8 @@ let hash_map_remove_back
with
| Fail -> Fail
| Return v ->
- let self0 = Mkhash_map_t i3 p i1 v in Return self0
+ Return (Mkhash_map_t i1 self.hash_map_max_load_factor
+ self.hash_map_max_load v)
end
end
end
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index 505dfc73..9bcbaec5 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -157,10 +157,7 @@ let _ = assert_norm (test_is_cons_fwd = Return ())
(** [no_nested_borrows::split_list] *)
let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) =
- begin match l with
- | ListCons hd tl -> let l0 = tl in Return (hd, l0)
- | ListNil -> Fail
- end
+ begin match l with | ListCons hd tl -> Return (hd, tl) | ListNil -> Fail end
(** [no_nested_borrows::test_split_list] *)
let test_split_list_fwd : result unit =
@@ -175,14 +172,12 @@ let _ = assert_norm (test_split_list_fwd = Return ())
(** [no_nested_borrows::get_elem] *)
let get_elem_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t =
- let x0 = y in let x1 = x in if b then Return x1 else Return x0
+ if b then Return x else Return y
(** [no_nested_borrows::get_elem] *)
let get_elem_back
(t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
- if b
- then let x0 = ret in let y0 = y in Return (x0, y0)
- else let x0 = x in let y0 = ret in Return (x0, y0)
+ if b then Return (ret, y) else Return (x, ret)
(** [no_nested_borrows::get_elem_test] *)
let get_elem_test_fwd : result unit =
@@ -300,7 +295,7 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
| Return i0 ->
begin match list_nth_shared_fwd t tl i0 with
| Fail -> Fail
- | Return x0 -> let x1 = x0 in Return x1
+ | Return x0 -> Return x0
end
end
end
@@ -319,7 +314,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
| Return i0 ->
begin match list_nth_mut_fwd t tl i0 with
| Fail -> Fail
- | Return x0 -> let x1 = x0 in Return x1
+ | Return x0 -> Return x0
end
end
end
@@ -332,14 +327,14 @@ let rec list_nth_mut_back
begin match l with
| ListCons x tl ->
begin match i with
- | 0 -> let x0 = ret in let l0 = ListCons x0 tl in Return l0
+ | 0 -> Return (ListCons ret tl)
| _ ->
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
begin match list_nth_mut_back t tl i0 ret with
| Fail -> Fail
- | Return l0 -> let l1 = ListCons x l0 in Return l1
+ | Return l0 -> Return (ListCons x l0)
end
end
end
@@ -408,49 +403,49 @@ let _ = assert_norm (test_list_functions_fwd = Return ())
(** [no_nested_borrows::id_mut_pair1] *)
let id_mut_pair1_fwd (t1 t2 : Type0) (x : t1) (y : t2) : result (t1 & t2) =
- let x0 = y in let x1 = x in Return (x1, x0)
+ Return (x, y)
(** [no_nested_borrows::id_mut_pair1] *)
let id_mut_pair1_back
(t1 t2 : Type0) (x : t1) (y : t2) (ret : (t1 & t2)) : result (t1 & t2) =
- let (x0, x1) = ret in let x2 = x0 in let y0 = x1 in Return (x2, y0)
+ let (x0, x1) = ret in Return (x0, x1)
(** [no_nested_borrows::id_mut_pair2] *)
let id_mut_pair2_fwd (t1 t2 : Type0) (p : (t1 & t2)) : result (t1 & t2) =
- let (x, x0) = p in let x1 = x in let x2 = x0 in Return (x1, x2)
+ let (x, x0) = p in Return (x, x0)
(** [no_nested_borrows::id_mut_pair2] *)
let id_mut_pair2_back
(t1 t2 : Type0) (p : (t1 & t2)) (ret : (t1 & t2)) : result (t1 & t2) =
- let (x, x0) = ret in let p0 = (x, x0) in Return p0
+ let (x, x0) = ret in Return (x, x0)
(** [no_nested_borrows::id_mut_pair3] *)
let id_mut_pair3_fwd (t1 t2 : Type0) (x : t1) (y : t2) : result (t1 & t2) =
- let x0 = y in let x1 = x in Return (x1, x0)
+ Return (x, y)
(** [no_nested_borrows::id_mut_pair3] *)
let id_mut_pair3_back'a
(t1 t2 : Type0) (x : t1) (y : t2) (ret : t1) : result t1 =
- let x0 = ret in Return x0
+ Return ret
(** [no_nested_borrows::id_mut_pair3] *)
let id_mut_pair3_back'b
(t1 t2 : Type0) (x : t1) (y : t2) (ret : t2) : result t2 =
- let y0 = ret in Return y0
+ Return ret
(** [no_nested_borrows::id_mut_pair4] *)
let id_mut_pair4_fwd (t1 t2 : Type0) (p : (t1 & t2)) : result (t1 & t2) =
- let (x, x0) = p in let x1 = x in let x2 = x0 in Return (x1, x2)
+ let (x, x0) = p in Return (x, x0)
(** [no_nested_borrows::id_mut_pair4] *)
let id_mut_pair4_back'a
(t1 t2 : Type0) (p : (t1 & t2)) (ret : t1) : result t1 =
- let p0 = ret in Return p0
+ Return ret
(** [no_nested_borrows::id_mut_pair4] *)
let id_mut_pair4_back'b
(t1 t2 : Type0) (p : (t1 & t2)) (ret : t2) : result t2 =
- let p0 = ret in Return p0
+ Return ret
(** [no_nested_borrows::StructWithTuple] *)
type struct_with_tuple_t (t1 t2 : Type0) = { struct_with_tuple_p : (t1 & t2); }
@@ -521,6 +516,5 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ())
(** [no_nested_borrows::test_mem_replace] *)
let test_mem_replace_fwd_back (px : u32) : result u32 =
- let i = mem_replace_fwd u32 px 1 in
- if not (i = 0) then Fail else let px0 = 2 in Return px0
+ let i = mem_replace_fwd u32 px 1 in if not (i = 0) then Fail else Return 2
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index 1ab42726..be4326d7 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -7,10 +7,7 @@ open Primitives
(** [paper::ref_incr] *)
let ref_incr_fwd_back (x : i32) : result i32 =
- begin match i32_add x 1 with
- | Fail -> Fail
- | Return x0 -> let x1 = x0 in Return x1
- end
+ begin match i32_add x 1 with | Fail -> Fail | Return x0 -> Return x0 end
(** [paper::test_incr] *)
let test_incr_fwd : result unit =
@@ -24,14 +21,12 @@ let _ = assert_norm (test_incr_fwd = Return ())
(** [paper::choose] *)
let choose_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t =
- let x0 = y in let x1 = x in if b then Return x1 else Return x0
+ if b then Return x else Return y
(** [paper::choose] *)
let choose_back
(t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
- if b
- then let x0 = ret in let y0 = y in Return (x0, y0)
- else let x0 = x in let y0 = ret in Return (x0, y0)
+ if b then Return (ret, y) else Return (x, ret)
(** [paper::test_choose] *)
let test_choose_fwd : result unit =
@@ -74,7 +69,7 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
| Return i0 ->
begin match list_nth_mut_fwd t tl i0 with
| Fail -> Fail
- | Return x0 -> let x1 = x0 in Return x1
+ | Return x0 -> Return x0
end
end
end
@@ -87,14 +82,14 @@ let rec list_nth_mut_back
begin match l with
| ListCons x tl ->
begin match i with
- | 0 -> let x0 = ret in let l0 = ListCons x0 tl in Return l0
+ | 0 -> Return (ListCons ret tl)
| _ ->
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
begin match list_nth_mut_back t tl i0 ret with
| Fail -> Fail
- | Return l0 -> let l1 = ListCons x l0 in Return l1
+ | Return l0 -> Return (ListCons x l0)
end
end
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 01:31:13 +0000