Improve the value visitors and some substitution functions

3 files changed, 54 insertions, 23 deletions

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index cc8cdcff..e302ea41 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -11,7 +11,6 @@ open ValuesUtils
 module Inv = Invariants
 module S = SynthesizeSymbolic
 module UF = UnionFind
-open Utils
 open Cps
 open InterpreterUtils
 open InterpreterBorrows
@@ -1046,9 +1045,8 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id)
   with ValueMatchFailure _ -> raise (Failure "Unexpected")
 
 (** 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 join_ctxs (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
 
@@ -1209,7 +1207,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 loop_id old_ids !joined_ctx ctx with
+    match join_ctxs loop_id old_ids !joined_ctx ctx with
     | Ok nctx -> joined_ctx := nctx
     | Error err ->
         let ctx =
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 0978e078..415f4d59 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -400,13 +400,12 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
       inherit [_] V.map_abs
       method! visit_borrow_id _ bid = bsubst bid
       method! visit_loan_id _ bid = bsubst bid
-
-      method! visit_symbolic_value env sv =
-        let sv_id = ssubst sv.sv_id in
-        let sv_ty = subst_rty#visit_ty env sv.sv_ty in
-        { sv with V.sv_id; sv_ty }
-
       method! visit_ety _ ty = ty_substitute_ids tsubst ty
+      method! visit_rty env ty = subst_rty#visit_ty env ty
+      method! visit_symbolic_value_id _ id = ssubst id
+
+      (** We *do* visit meta-values *)
+      method! visit_msymbolic_value env sv = self#visit_symbolic_value env sv
 
       (** We *do* visit meta-values *)
       method! visit_mvalue env v = self#visit_typed_value env v
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 9c68ad4f..f6f4d1b6 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -15,6 +15,7 @@ module LoopId = IdGen ()
 type big_int = PrimitiveValues.big_int [@@deriving show, ord]
 type scalar_value = PrimitiveValues.scalar_value [@@deriving show, ord]
 type primitive_value = PrimitiveValues.primitive_value [@@deriving show, ord]
+type symbolic_value_id = SymbolicValueId.id [@@deriving show, ord]
 
 (** The kind of a symbolic value, which precises how the value was generated.
 
@@ -49,13 +50,54 @@ type sv_kind =
       (** The result of a loop join (when computing loop fixed points) *)
 [@@deriving show, ord]
 
+(** Ancestor for {!symbolic_value} iter visitor *)
+class ['self] iter_symbolic_value_base =
+  object (_self : 'self)
+    inherit [_] VisitorsRuntime.iter
+    method visit_sv_kind : 'env -> sv_kind -> unit = fun _ _ -> ()
+    method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
+
+    method visit_symbolic_value_id : 'env -> symbolic_value_id -> unit =
+      fun _ _ -> ()
+  end
+
+(** Ancestor for {!symbolic_value} map visitor for *)
+class ['self] map_symbolic_value_base =
+  object (_self : 'self)
+    inherit [_] VisitorsRuntime.map
+    method visit_sv_kind : 'env -> sv_kind -> sv_kind = fun _ x -> x
+    method visit_rty : 'env -> rty -> rty = fun _ x -> x
+
+    method visit_symbolic_value_id
+        : 'env -> symbolic_value_id -> symbolic_value_id =
+      fun _ x -> x
+  end
+
 (** A symbolic value *)
 type symbolic_value = {
   sv_kind : sv_kind;
-  sv_id : SymbolicValueId.id;
+  sv_id : symbolic_value_id;
   sv_ty : rty;
 }
-[@@deriving show, ord]
+[@@deriving
+  show,
+    ord,
+    visitors
+      {
+        name = "iter_symbolic_value";
+        variety = "iter";
+        ancestors = [ "iter_symbolic_value_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        concrete = true;
+      },
+    visitors
+      {
+        name = "map_symbolic_value";
+        variety = "map";
+        ancestors = [ "map_symbolic_value_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        concrete = true;
+      }]
 
 type borrow_id = BorrowId.id [@@deriving show, ord]
 type borrow_id_set = BorrowId.Set.t [@@deriving show, ord]
@@ -65,13 +107,12 @@ type loan_id_set = BorrowId.Set.t [@@deriving show, ord]
 (** Ancestor for {!typed_value} iter visitor *)
 class ['self] iter_typed_value_base =
   object (self : 'self)
-    inherit [_] VisitorsRuntime.iter
+    inherit [_] iter_symbolic_value
 
     method visit_primitive_value : 'env -> primitive_value -> unit =
       fun _ _ -> ()
 
     method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
-    method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> ()
     method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
     method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
     method visit_borrow_id : 'env -> borrow_id -> unit = fun _ _ -> ()
@@ -87,7 +128,7 @@ class ['self] iter_typed_value_base =
 (** Ancestor for {!typed_value} map visitor for *)
 class ['self] map_typed_value_base =
   object (self : 'self)
-    inherit [_] VisitorsRuntime.map
+    inherit [_] map_symbolic_value
 
     method visit_primitive_value : 'env -> primitive_value -> primitive_value =
       fun _ cv -> cv
@@ -95,9 +136,6 @@ class ['self] map_typed_value_base =
     method visit_erased_region : 'env -> erased_region -> erased_region =
       fun _ r -> r
 
-    method visit_symbolic_value : 'env -> symbolic_value -> symbolic_value =
-      fun _ sv -> sv
-
     method visit_ety : 'env -> ety -> ety = fun _ ty -> ty
     method visit_variant_id : 'env -> variant_id -> variant_id = fun _ x -> x
     method visit_borrow_id : 'env -> borrow_id -> borrow_id = fun _ id -> id
@@ -243,8 +281,6 @@ class ['self] iter_typed_value =
 
     method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
       fun _ _ -> ()
-
-    method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
   end
 
 class ['self] map_typed_value =
@@ -255,8 +291,6 @@ class ['self] map_typed_value =
         to ignore meta-values *)
     method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
 
-    method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
-
     method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
       fun _ m -> m
   end