summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/InterpreterLoopsCore.ml20
-rw-r--r--compiler/InterpreterLoopsJoinCtxs.ml67
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml10
3 files changed, 53 insertions, 44 deletions
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 4149b19e..df808385 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -430,11 +430,11 @@ let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets =
in
ids
-(* Small utility: Add a projection marker to a typed avalue.
- This can be used in combination with List.map to add markers to an entire abstraction
-*)
-let add_marker_avalue (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker)
- (av : typed_avalue) : typed_avalue =
+(** Small utility: add a projection marker to a typed avalue.
+ This can be used in combination with List.map to add markers to an entire abstraction
+ *)
+let typed_avalue_add_marker (span : Meta.span) (ctx : eval_ctx)
+ (pm : proj_marker) (av : typed_avalue) : typed_avalue =
let obj =
object
inherit [_] map_typed_avalue as super
@@ -473,3 +473,13 @@ let add_marker_avalue (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker)
end
in
obj#visit_typed_avalue () av
+
+(** Small utility: add a projection marker to an abstraction.
+ This can be used in combination with List.map to add markers to an entire abstraction
+ *)
+let abs_add_marker (span : Meta.span) (ctx : eval_ctx) (pm : proj_marker)
+ (abs : abs) : abs =
+ {
+ abs with
+ avalues = List.map (typed_avalue_add_marker span ctx pm) abs.avalues;
+ }
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index d2f52781..b25ea0fc 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -67,20 +67,23 @@ let log = Logging.loops_join_ctxs_log
abs@4 { MB l0, ML l4 }
]}
- If [merge_funs] is [None], we check that there are no markers in the environments.
- This is the "reduce" operation.
- If [merge_funs] is [Some _], when merging abstractions together, we merge the pairs
- of borrows and the pairs of loans with complementary markers. This is useful to
- reuse the reduce operation to implement the collapse.
- For instance, when merging:
- {[
- abs@0 { ML l0, |MB l1| }
- abs@1 { MB l0, ︙MB l1︙ }
- ]}
- We get:
- {[
- abs@2 { MB l1 }
- ]}
+ - If [merge_funs] is [None], we check that there are no markers in the environments.
+ This is the "reduce" operation.
+ - If [merge_funs] is [Some _], when merging abstractions together, we merge the pairs
+ of borrows and the pairs of loans with the same markers **if this marker is not**
+ [PNone]. This is useful to reuse the reduce operation to implement the collapse.
+ Note that we ignore borrows/loans with the [PNone] marker: the goal of the collapse
+ operation is to *eliminate* markers, not to simplify the environment.
+
+ For instance, when merging:
+ {[
+ abs@0 { ML l0, |MB l1| }
+ abs@1 { MB l0, ︙MB l1︙ }
+ ]}
+ We get:
+ {[
+ abs@2 { MB l1 }
+ ]}
*)
let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option)
(span : Meta.span) (loop_id : LoopId.id) (old_ids : ids_sets)
@@ -92,7 +95,7 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option)
^ eval_ctx_to_string ~span:(Some span) ctx0
^ "\n\n"));
- let allow_markers = merge_funs <> None in
+ let with_markers = merge_funs <> None in
let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in
let can_end = true in
@@ -172,18 +175,27 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option)
let bids = MarkerBorrowId.Set.elements bids in
List.iter
(fun bid ->
- if not allow_markers then
+ if not with_markers then
sanity_check __FILE__ __LINE__ (fst bid = PNone) span;
- match MarkerBorrowId.Map.find_opt bid loan_to_abs with
- | None -> (* Nothing to do *) ()
- | Some abs_ids1 ->
- if allow_markers && fst bid = PNone then ()
- else
+ (* If we use markers: we are doing a collapse, which means we attempt
+ to eliminate markers (and this is the only goal of the operation).
+ We thus ignore the non-marked values (we merge non-marked values
+ when doing a "real" reduce, to simplify the environment in order
+ to converge to a fixed-point, for instance). *)
+ if with_markers && fst bid = PNone then ()
+ else
+ match MarkerBorrowId.Map.find_opt bid loan_to_abs with
+ | None -> (* Nothing to do *) ()
+ | Some abs_ids1 ->
AbstractionId.Set.iter
(fun abs_id1 ->
(* We need to merge - unless we have already merged *)
- (* First, find the representatives for the two abstractions (the
- representative is the abstraction into which we merged) *)
+ (* First, find the representatives for the two abstractions.
+
+ We may have merged some abstractions already, so maybe abs_id0
+ and abs_id1 don't exist anymore, because they may have been
+ merged into other abstractions: we look for the abstractions
+ resulting from such merged. *)
let abs_ref0 =
UnionFind.find (AbstractionId.Map.find abs_id0 merged_abs)
in
@@ -207,7 +219,7 @@ let reduce_ctx_with_markers (merge_funs : merge_duplicates_funcs option)
^ ":\n\n"
^ eval_ctx_to_string ~span:(Some span) !ctx));
- (* Update the environment - pay attention to the order: we
+ (* Update the environment - pay attention to the order:
we merge [abs_id1] *into* [abs_id0] *)
let nctx, abs_id =
merge_into_abstraction span abs_kind can_end merge_funs
@@ -672,12 +684,7 @@ let join_ctxs (span : Meta.span) (loop_id : LoopId.id) (fixed_ids : ids_sets)
(* Add projection marker to all abstractions in the left and right environments *)
let add_marker (pm : proj_marker) (ee : env_elem) : env_elem =
match ee with
- | EAbs abs ->
- EAbs
- {
- abs with
- avalues = List.map (add_marker_avalue span ctx0 pm) abs.avalues;
- }
+ | EAbs abs -> EAbs (abs_add_marker span ctx0 pm abs)
| x -> x
in
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index bc39d5ec..3f7c023e 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -837,15 +837,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
in
(* Add a marker to the abstraction indicating the provenance of the value *)
let pm = if value_is_left then PLeft else PRight in
- let absl =
- List.map
- (fun abs ->
- {
- abs with
- avalues = List.map (add_marker_avalue span ctx0 pm) abs.avalues;
- })
- absl
- in
+ let absl = List.map (abs_add_marker span ctx0 pm) absl in
push_absl absl;
(* Return [Bottom] *)
mk_bottom span v.ty