diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 20 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 2 |
2 files changed, 20 insertions, 2 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 0b7b4be5..a1cb4ec3 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -1862,7 +1862,10 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool) in push_abs r_id avl; fv) - adt.field_values + (* Slightly tricky: pay attention to the order in which the + abstractions are pushed (i.e.: the [List.rev] is important + to get a "good" environment, and a nice translation) *) + (List.rev adt.field_values) in ([], field_values) in @@ -2430,6 +2433,21 @@ let merge_abstractions_aux (abs_kind : V.abs_kind) (can_end : bool) new values at the beggining of the stack of avalues) *) let avalues = List.rev !avalues in + (* Reorder the avalues. We want the avalues to have the borrows first, then + the loans (this structure is more stable when we merge abstractions together, + meaning it is easier to find fixed points). + *) + let avalues = + let is_borrow (av : V.typed_avalue) : bool = + match av.V.value with + | ABorrow _ -> true + | ALoan _ -> false + | _ -> raise (Failure "Unexpected") + in + let aborrows, aloans = List.partition is_borrow avalues in + List.append aborrows aloans + in + (* Filter the regions *) (* Create the new abstraction *) diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index a2a1cfde..9e407399 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -197,7 +197,7 @@ type merge_duplicates_funcs = { *) } -(** Merge two abstractions together. +(** Merge an abstraction into another abstraction. We insert the result of the merge in place of the first abstraction (this helps preserving the structure of the environment, when computing loop |