Make more progress on the joins

1 files changed, 127 insertions, 142 deletions

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 85174aaf..cc8cdcff 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -20,15 +20,6 @@ open InterpreterExpressions
 (** The local logger *)
 let log = L.loops_log
 
-(* TODO: some fields are actually useless *)
-type cnt_thresholds = {
-  aid : V.AbstractionId.id;
-  sid : V.SymbolicValueId.id;
-  bid : V.BorrowId.id;
-  did : C.DummyVarId.id;
-  rid : T.RegionId.id;
-}
-
 type updt_env_kind =
   | AbsInLeft of V.AbstractionId.id
   | LoanInLeft of V.BorrowId.id
@@ -1054,116 +1045,139 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id)
   try collapse_ctx loop_id (Some merge_funcs) old_ids ctx
   with ValueMatchFailure _ -> raise (Failure "Unexpected")
 
-(*(** Apply substitutions in the first abstraction, then join the abstractions together.
-
-    TODO: remove?
- *)
-let subst_join_abstractions (loop_id : V.LoopId.id) (thresh : cnt_thresholds)
-    (rid_map : T.RegionId.InjSubst.t) (bid_map : V.BorrowId.InjSubst.t)
-    (sid_map : V.SymbolicValueId.InjSubst.t) (ctx : C.eval_ctx) (abs0 : V.abs)
-    (abs1 : V.abs) : V.abs =
-  (* Apply the substitutions in the first abstraction *)
-  let rsubst id =
-    assert (T.RegionId.Ord.compare id thresh.rid >= 0);
-    T.RegionId.InjSubst.find_with_default id id rid_map
-  in
-  let rvsubst id = id in
-  let tsubst id = id in
-  let ssubst id =
-    assert (V.SymbolicValueId.Ord.compare id thresh.sid >= 0);
-    V.SymbolicValueId.InjSubst.find_with_default id id sid_map
-  in
-  let bsubst id =
-    assert (V.BorrowId.Ord.compare id thresh.bid >= 0);
-    V.BorrowId.InjSubst.find_with_default id id bid_map
-  in
-  let asubst id = id in
-  let abs0 =
-    Substitute.abs_subst_ids rsubst rvsubst tsubst ssubst bsubst asubst abs0
-  in
-
-  (* Merge the two abstractions *)
-  let abs_kind = V.Loop loop_id in
-  let can_end = false in
-merge_abstractions abs_kind can_end None ctx abs0 abs1*)
-
-(*
-(** Merge a borrow with the abstraction containing the associated loan, where
-    the abstraction must be a *loop abstraction* (we don't synthesize code during
-    the operation).
+(** Join two contexts *)
+let join_ctxs (config : C.config) (loop_id : V.LoopId.id)
+    (old_ids : InterpreterBorrowsCore.ctx_ids) (ctx0 : C.eval_ctx)
+    (ctx1 : C.eval_ctx) : ctx_or_update =
+  let env0 = List.rev ctx0.env in
+  let env1 = List.rev ctx1.env in
+
+  (* We need to pick a context for some functions like [match_typed_values]:
+     the context is only used to lookup module data, so we can pick whichever
+     we want.
+     TODO: this is not very clean. Maybe we should just carry this data around.
+  *)
+  let ctx = ctx0 in
 
-    For instance:
-    {[
-      abs'0 { mut_loan l0 }
-      x -> mut_borrow l0 sx
+  let nabs = ref [] in
 
-            ~~>
+  (* Explore the environments.
 
-      abs'0 {}
-      x -> ⊥
-    ]}
- *)
-let merge_borrow_with_parent_loop_abs (config : C.config) (bid : V.BorrowId.id)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* TODO: use the function from InterpreterBorrows *)
-  failwith "Unimplemented"
-(* (* Lookup the borrow *)
-     let ek =
-       { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false }
-     in
-     (* TODO: use [end_borrow_get_borrow]? *)
-     match lookup_borrow ek bid ctx with
-     | None -> ctx
-   | Some b -> failwith "Unimplemented"*)
-
-(** See {!merge_borrow_with_parent_loop_abs} *)
-let rec merge_borrows_with_parent_loop_abs (config : C.config)
-    (bids : V.BorrowId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
-  V.BorrowId.Set.fold
-    (fun id ctx -> merge_borrow_with_parent_loop_abs config id ctx)
-    bids ctx
- *)
+     Note that they should have the same prefixes (they should start with
+     old dummy values, old abstractions and bindings which have the same ids).
+     Those old values and abstractions should actually be equal between the
+     two environments.
 
-(*
-(* TODO: we probably don't need an [match_ctx], and actually we might not use
-   the bounds propertly.
-   TODO: remove
-*)
-let match_ctx_with_target_old (config : C.config) (tgt_ctx : C.eval_ctx) :
-    cm_fun =
- fun cf src_ctx ->
-  (* We first reorganize [ctx] so that we can match it with [tgt_ctx] *)
-  (* First, collect all the borrows and abstractions which are in [ctx]
-     and not in [tgt_ctx]: we need to end them *)
-  let src_ids = InterpreterBorrowsCore.compute_context_ids src_ctx in
-  let tgt_ids = InterpreterBorrowsCore.compute_context_ids tgt_ctx in
-  let bids = V.BorrowId.Set.diff src_ids.bids tgt_ids.bids in
-  let aids = V.AbstractionId.Set.diff src_ids.aids tgt_ids.aids in
-  (* End those borrows and abstractions *)
-  let cc = InterpreterBorrows.end_borrows config bids in
-  let cc = comp cc (InterpreterBorrows.end_abstractions config aids) in
-  (* In the target context, merge all the borrows introduced by the loop with
-     their parent abstractions
+     Rem.: this is important to make the match easy (we take care of preserving
+     the structure of the environments, and ending the proper borrows/abstractions,
+     etc.). We could also implement a more general join.
   *)
-  let tgt_ctx =
-    merge_borrows_with_parent_loop_abs config
-      (V.BorrowId.Set.diff tgt_ids.bids src_ids.bids)
-      tgt_ctx
+  let join_suffixes (env0 : C.env) (env1 : C.env) : C.env =
+    (* Sanity check: there are no values/abstractions which should be in the prefix *)
+    let check_valid (ee : C.env_elem) : unit =
+      match ee with
+      | C.Var (C.VarBinder _, _) ->
+          (* Variables are necessarily in the prefix *)
+          raise (Failure "Unreachable")
+      | Var (C.DummyBinder did, _) ->
+          assert (not (C.DummyVarId.Set.mem did old_ids.dids))
+      | Abs abs ->
+          assert (not (V.AbstractionId.Set.mem abs.abs_id old_ids.aids))
+      | Frame -> ()
+    in
+    List.iter check_valid env0;
+    List.iter check_valid env1;
+    (* Concatenate the suffixes and append the abstractions introduced while
+       joining the prefixes *)
+    let absl = List.map (fun abs -> C.Abs abs) !nabs in
+    List.concat [ env0; env1; absl ]
   in
-  (* Replace the source context with the target context - TODO: explain
-     why this works *)
-  let cf_apply_match : cm_fun = fun cf _ -> cf tgt_ctx in
-  let cc = comp cc cf_apply_match in
-  (* Sanity check on the resulting context *)
-  let cc = comp_check_ctx cc Inv.check_invariants in
-  (* Apply and continue *)
-  cc cf src_ctx
-*)
 
-(** Join two contexts *)
-let join_ctxs (_config : C.config) (_old_ids : InterpreterBorrowsCore.ctx_ids)
-    (_ctx0 : C.eval_ctx) (_ctx1 : C.eval_ctx) : ctx_or_update =
-  raise (Failure "Unimplemented")
+  let module S : MatchJoinState = struct
+    (* The context is only used to lookup module data: we can pick whichever we want *)
+    let ctx = ctx
+    let loop_id = loop_id
+    let nabs = nabs
+  end in
+  let module JM = MakeJoinMatcher (S) in
+  let module M = Match (JM) in
+  (* Rem.: this function raises exceptions *)
+  let rec join_prefixes (env0 : C.env) (env1 : C.env) : C.env =
+    match (env0, env1) with
+    | ( (C.Var (C.DummyBinder b0, v0) as var) :: env0',
+        C.Var (C.DummyBinder b1, v1) :: env1' ) ->
+        (* Two cases: the dummy value is an old value, in which case the bindings
+           must be the same and we must join their values. Otherwise, it means we
+           are not in the prefix anymore *)
+        if C.DummyVarId.Set.mem b0 old_ids.dids then (
+          (* Still in the prefix: the values must match *)
+          assert (b0 = b1);
+          assert (v0 = v1);
+          (* Continue *)
+          var :: join_prefixes env0' env1')
+        else (* Not in the prefix anymore *)
+          join_suffixes env0 env1
+    | C.Var (C.VarBinder b0, v0) :: env0', C.Var (C.VarBinder b1, v1) :: env1'
+      ->
+        (* Variable bindings *must* be in the prefix and consequently their
+           ids must be the same *)
+        assert (b0 = b1);
+        (* Match the values *)
+        let b = b0 in
+        let v = M.match_typed_values ctx v0 v1 in
+        let var = C.Var (C.VarBinder b, v) in
+        (* Continue *)
+        var :: join_prefixes env0' env1'
+    | (C.Abs abs0 as abs) :: env0', C.Abs abs1 :: env1' ->
+        (* Same as for the dummy values: there are two cases *)
+        if V.AbstractionId.Set.mem abs0.abs_id old_ids.aids then (
+          (* Still in the prefix: the abstractions must be the same *)
+          assert (abs0 = abs1);
+          (* Continue *)
+          abs :: join_suffixes env0' env1')
+        else (* Not in the prefix anymore *)
+          join_suffixes env0 env1
+    | _ ->
+        (* The elements don't match: we are not in the prefix anymore *)
+        join_suffixes env0 env1
+  in
+
+  try
+    let env = List.rev (join_prefixes env0 env1) in
+
+    (* Construct the joined context - of course, the type, fun, etc. contexts
+     * should be the same in the two contexts *)
+    let {
+      C.type_context;
+      fun_context;
+      global_context;
+      type_vars;
+      env = _;
+      ended_regions = ended_regions0;
+    } =
+      ctx0
+    in
+    let {
+      C.type_context = _;
+      fun_context = _;
+      global_context = _;
+      type_vars = _;
+      env = _;
+      ended_regions = ended_regions1;
+    } =
+      ctx1
+    in
+    let ended_regions = T.RegionId.Set.union ended_regions0 ended_regions1 in
+    Ok
+      {
+        C.type_context;
+        fun_context;
+        global_context;
+        type_vars;
+        env;
+        ended_regions;
+      }
+  with ValueMatchFailure e -> Error e
 
 (** Join the context at the entry of the loop with the contexts upon reentry
     (upon reaching the [Continue] statement - the goal is to compute a fixed
@@ -1195,7 +1209,7 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
   *)
   let joined_ctx = ref old_ctx in
   let rec join_one_aux (ctx : C.eval_ctx) : unit =
-    match join_ctxs config old_ids !joined_ctx ctx with
+    match join_ctxs config loop_id old_ids !joined_ctx ctx with
     | Ok nctx -> joined_ctx := nctx
     | Error err ->
         let ctx =
@@ -1229,28 +1243,6 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
   (* # Return *)
   !joined_ctx
 
-(*
-(** Join a context at the entry of a loop with a context upon reaching
-    a continue in this loop.
- *)
-let loop_join_entry_ctx_with_continue_ctx (_ctx0 : C.eval_ctx)
-    (_ctx1 : C.eval_ctx) : ctx_or_update =
-  failwith "Unimplemented"
-
-(** See {!loop_join_entry_ctx_with_continue_ctx} *)
-let rec loop_join_entry_ctx_with_continue_ctxs (ctx0 : C.eval_ctx)
-    (ctxs : C.eval_ctx list) : ctx_or_update =
-  match ctxs with
-  | [] -> Ok ctx0
-  | ctx1 :: ctxs -> (
-      let res = loop_join_entry_ctx_with_continue_ctx ctx0 ctx1 in
-      match res with
-      | Error _ ->
-          (* TODO: apply the error *)
-          raise (Failure "Unimplemented")
-      | Ok ctx0 -> loop_join_entry_ctx_with_continue_ctxs ctx0 ctxs)
- *)
-
 let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
     (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : C.eval_ctx =
   (* The continuation for when we exit the loop - we register the
@@ -1276,13 +1268,6 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
         raise (Failure "Nested loops are not supported for now")
   in
   (* Join the contexts at the loop entry *)
-  (* TODO: return result:
-   * - end borrows in ctx0
-   * - ok: return joined env
-   * TODO: keep initial env somewhere?
-   * TODO: the returned env is an eval_ctx or smth else?
-   * Maybe simply keep track of existentially quantified variables?
-   *)
   let join_ctxs (ctx0 : C.eval_ctx) : C.eval_ctx =
     let ctx1 = loop_join_origin_with_continue_ctxs config loop_id ctx0 !ctxs in
     ctxs := [];