Use RegionVarId and RegionId in a more consistent manner

7 files changed, 86 insertions, 37 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 64151a48..192638cf 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -28,8 +28,8 @@ type fun_sig = {
   region_params : region_var list;
   num_early_bound_regions : int;
   type_params : type_var list;
-  inputs : rty list;
-  output : rty;
+  inputs : sty list;
+  output : sty;
 }
 [@@deriving show]
 
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 0a7eeb78..3494f004 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -124,8 +124,8 @@ let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) :
         Ok (T.Ref (region, ty, ref_kind))
     | _ -> Error "")
 
-let rty_of_json (js : json) : (T.rty, string) result =
-  combine_error_msgs js "rty_of_json" (ty_of_json region_of_json js)
+let sty_of_json (js : json) : (T.sty, string) result =
+  combine_error_msgs js "sty_of_json" (ty_of_json region_of_json js)
 
 let ety_of_json (js : json) : (T.ety, string) result =
   combine_error_msgs js "ety_of_json" (ty_of_json erased_region_of_json js)
@@ -135,7 +135,7 @@ let field_of_json (js : json) : (T.field, string) result =
     (match js with
     | `Assoc [ ("name", name); ("ty", ty) ] ->
         let* name = string_of_json name in
-        let* ty = rty_of_json ty in
+        let* ty = sty_of_json ty in
         Ok { T.field_name = name; field_ty = ty }
     | _ -> Error "")
 
@@ -450,8 +450,8 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
         let* region_params = list_of_json region_var_of_json region_params in
         let* num_early_bound_regions = int_of_json num_early_bound_regions in
         let* type_params = list_of_json type_var_of_json type_params in
-        let* inputs = list_of_json rty_of_json inputs in
-        let* output = rty_of_json output in
+        let* inputs = list_of_json sty_of_json inputs in
+        let* output = sty_of_json output in
         Ok
           {
             A.region_params;
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 8b929b0f..9555b0ca 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -584,8 +584,12 @@ exception FoundOuter of outer_borrows_or_abs
     Note that the two abstractions have different views (in terms of regions)
     of the symbolic value (hence the two region types).
 *)
-let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty)
-    (rset2 : V.RegionId.set_t) : bool =
+let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t)
+    (ty2 : T.rty) (rset2 : T.RegionId.set_t) : bool =
+  let region_in_set (r : T.RegionId.id T.region) (rset : T.RegionId.set_t) :
+      bool =
+    match r with T.Static -> false | T.Var id -> T.RegionId.Set.mem id rset
+  in
   match (ty1, ty2) with
   | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false
   | T.Integer int_ty1, T.Integer int_ty2 ->
@@ -603,8 +607,7 @@ let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty)
       let regions = List.combine regions1 regions2 in
       let tys = List.combine tys1 tys2 in
       List.exists
-        (fun (r1, r2) ->
-          V.RegionId.Set.mem r1 rset1 && V.RegionId.Set.mem r2 rset2)
+        (fun (r1, r2) -> region_in_set r1 rset1 && region_in_set r2 rset2)
         regions
       || List.exists
            (fun (ty1, ty2) -> projections_intersect ty1 rset1 ty2 rset2)
@@ -616,7 +619,7 @@ let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty)
       assert (kind1 = kind2);
       (* The projections intersect if the borrows intersect or their contents
        * intersect *)
-      (V.RegionId.Set.mem r1 rset1 && V.RegionId.Set.mem r2 rset2)
+      (region_in_set r1 rset1 && region_in_set r2 rset2)
       || projections_intersect ty1 rset1 ty2 rset2
   | _ -> failwith "Unreachable"
 
@@ -628,7 +631,7 @@ let projections_intersect (ty1 : T.rty) (rset1 : V.RegionId.set_t) (ty2 : T.rty)
       map borrows to regions - or to interpret the borrows as belonging
       to some regions...)
 *)
-let apply_proj_borrows (regions : V.RegionId.set_t) (v : V.typed_value)
+let apply_proj_borrows (regions : T.RegionId.set_t) (v : V.typed_value)
     (ty : T.rty) : V.typed_avalue =
   (* Sanity check - TODO: move this elsewhere (here we perform the check at every
    * recursive call which is a bit overkill...) *)
diff --git a/src/Print.ml b/src/Print.ml
index e9ba4730..bf07e57e 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -16,6 +16,12 @@ module Types = struct
     | Some name -> name
     | None -> T.RegionVarId.to_string rv.index
 
+  let region_var_id_to_string (rid : T.RegionVarId.id) : string =
+    "rv@" ^ T.RegionVarId.to_string rid
+
+  let region_id_to_string (rid : T.RegionId.id) : string =
+    "r@" ^ T.RegionId.to_string rid
+
   let region_to_string (rid_to_string : 'rid -> string) (r : 'rid T.region) :
       string =
     match r with Static -> "'static" | Var rid -> rid_to_string rid
@@ -33,9 +39,11 @@ module Types = struct
     type_def_id_to_string : T.TypeDefId.id -> string;
   }
 
-  type etype_formatter = T.erased_region type_formatter
+  type stype_formatter = T.RegionVarId.id T.region type_formatter
 
-  type rtype_formatter = T.RegionVarId.id T.region type_formatter
+  type rtype_formatter = T.RegionId.id T.region type_formatter
+
+  type etype_formatter = T.erased_region type_formatter
 
   let integer_type_to_string = function
     | T.Isize -> "isize"
@@ -87,9 +95,14 @@ module Types = struct
     else if List.length regions + List.length types > 0 then "<" ^ params ^ ">"
     else ""
 
-  let rty_to_string fmt (ty : T.rty) : string = ty_to_string fmt ty
+  let sty_to_string (fmt : stype_formatter) (ty : T.sty) : string =
+    ty_to_string fmt ty
+
+  let rty_to_string (fmt : rtype_formatter) (ty : T.rty) : string =
+    ty_to_string fmt ty
 
-  let ety_to_string fmt (ty : T.ety) : string = ty_to_string fmt ty
+  let ety_to_string (fmt : etype_formatter) (ty : T.ety) : string =
+    ty_to_string fmt ty
 
   let field_to_string fmt (f : T.field) : string =
     f.field_name ^ " : " ^ ty_to_string fmt f.field_ty
@@ -148,7 +161,8 @@ module PT = Types (* local module *)
 (** Pretty-printing for values *)
 module Values = struct
   type value_formatter = {
-    r_to_string : T.RegionVarId.id -> string;
+    rvar_to_string : T.RegionVarId.id -> string;
+    r_to_string : T.RegionId.id -> string;
     type_var_id_to_string : T.TypeVarId.id -> string;
     type_def_id_to_string : T.TypeDefId.id -> string;
     adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
@@ -171,6 +185,13 @@ module Values = struct
       PT.type_def_id_to_string = fmt.type_def_id_to_string;
     }
 
+  let value_to_stype_formatter (fmt : value_formatter) : PT.stype_formatter =
+    {
+      PT.r_to_string = PT.region_to_string fmt.rvar_to_string;
+      PT.type_var_id_to_string = fmt.type_var_id_to_string;
+      PT.type_def_id_to_string = fmt.type_def_id_to_string;
+    }
+
   let var_id_to_string (id : V.VarId.id) : string =
     "var@" ^ V.VarId.to_string id
 
@@ -191,14 +212,11 @@ module Values = struct
 
   let symbolic_value_to_string (fmt : PT.rtype_formatter)
       (sv : V.symbolic_value) : string =
-    symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.ty_to_string fmt sv.sv_ty
-
-  let region_id_to_string (rid : V.RegionId.id) : string =
-    "r@" ^ V.RegionId.to_string rid
+    symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.rty_to_string fmt sv.sv_ty
 
   let symbolic_proj_comp_to_string (fmt : PT.rtype_formatter)
       (sp : V.symbolic_proj_comp) : string =
-    let regions = V.RegionId.set_to_string sp.rset_ended in
+    let regions = T.RegionId.set_to_string sp.rset_ended in
     "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")"
 
   let symbolic_value_proj_to_string (fmt : value_formatter)
@@ -411,7 +429,7 @@ module Values = struct
     ^ "{parents="
     ^ V.AbstractionId.set_to_string abs.parents
     ^ "}" ^ "{regions="
-    ^ V.RegionId.set_to_string abs.regions
+    ^ T.RegionId.set_to_string abs.regions
     ^ "}" ^ " {\n" ^ avs ^ "\n}"
 end
 
@@ -465,8 +483,10 @@ module Contexts = struct
     Some fields
 
   let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
-    (* We shouldn't use r_to_string *)
-    let r_to_string _ = failwith "Unexpected use of r_to_string" in
+    (* We shouldn't use rvar_to_string *)
+    let rvar_to_string r = failwith "Unexpected use of rvar_to_string" in
+    let r_to_string r = PT.region_id_to_string r in
+
     let type_var_id_to_string vid =
       let v = C.lookup_type_var ctx vid in
       v.name
@@ -484,6 +504,7 @@ module Contexts = struct
     in
     let adt_field_names = type_ctx_to_adt_field_names_fun ctx.C.type_context in
     {
+      rvar_to_string;
       r_to_string;
       type_var_id_to_string;
       type_def_id_to_string;
@@ -527,7 +548,8 @@ module PC = Contexts (* local module *)
 (** Pretty-printing for contexts (generic functions) *)
 module CfimAst = struct
   type ast_formatter = {
-    r_to_string : T.RegionVarId.id -> string;
+    rvar_to_string : T.RegionVarId.id -> string;
+    r_to_string : T.RegionId.id -> string;
     type_var_id_to_string : T.TypeVarId.id -> string;
     type_def_id_to_string : T.TypeDefId.id -> string;
     adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
@@ -541,6 +563,7 @@ module CfimAst = struct
 
   let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
     {
+      PV.rvar_to_string = fmt.rvar_to_string;
       PV.r_to_string = fmt.r_to_string;
       PV.type_var_id_to_string = fmt.type_var_id_to_string;
       PV.type_def_id_to_string = fmt.type_def_id_to_string;
@@ -563,6 +586,13 @@ module CfimAst = struct
       PT.type_def_id_to_string = fmt.type_def_id_to_string;
     }
 
+  let ast_to_stype_formatter (fmt : ast_formatter) : PT.stype_formatter =
+    {
+      PT.r_to_string = PT.region_to_string fmt.rvar_to_string;
+      PT.type_var_id_to_string = fmt.type_var_id_to_string;
+      PT.type_def_id_to_string = fmt.type_def_id_to_string;
+    }
+
   let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def list) :
       T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string =
    fun def_id opt_variant_id field_id ->
@@ -581,6 +611,7 @@ module CfimAst = struct
       PT.name_to_string def.name
     in
     {
+      rvar_to_string = ctx_fmt.PV.rvar_to_string;
       r_to_string = ctx_fmt.PV.r_to_string;
       type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string;
       type_def_id_to_string = ctx_fmt.PV.type_def_id_to_string;
@@ -790,6 +821,8 @@ module CfimAst = struct
       (indent_incr : string) (def : A.fun_def) : string =
     let rty_fmt = ast_to_rtype_formatter fmt in
     let rty_to_string = PT.rty_to_string rty_fmt in
+    let sty_fmt = ast_to_stype_formatter fmt in
+    let sty_to_string = PT.sty_to_string sty_fmt in
     let ety_fmt = ast_to_etype_formatter fmt in
     let ety_to_string = PT.ety_to_string ety_fmt in
     let sg = def.signature in
@@ -814,7 +847,7 @@ module CfimAst = struct
     let args = List.combine inputs sg.inputs in
     let args =
       List.map
-        (fun (var, rty) -> var_to_string var ^ " : " ^ rty_to_string rty)
+        (fun (var, rty) -> var_to_string var ^ " : " ^ sty_to_string rty)
         args
     in
     let args = String.concat ", " args in
@@ -822,7 +855,7 @@ module CfimAst = struct
     (* Return type *)
     let ret_ty = sg.output in
     let ret_ty =
-      if TU.ty_is_unit ret_ty then "" else " -> " ^ rty_to_string ret_ty
+      if TU.ty_is_unit ret_ty then "" else " -> " ^ sty_to_string ret_ty
     in
 
     (* All the locals (with erased regions) *)
@@ -863,10 +896,14 @@ module Module = struct
       with the variables local to a function's definition *)
   let def_ctx_to_ast_formatter (type_context : T.type_def list)
       (fun_context : A.fun_def list) (def : A.fun_def) : PA.ast_formatter =
-    let r_to_string vid =
+    let rvar_to_string vid =
       let var = T.RegionVarId.nth def.signature.region_params vid in
       PT.region_var_to_string var
     in
+    let r_to_string vid =
+      (* TODO: we might want something more informative *)
+      PT.region_id_to_string vid
+    in
     let type_var_id_to_string vid =
       let var = T.TypeVarId.nth def.signature.type_params vid in
       PT.type_var_to_string var
@@ -891,6 +928,7 @@ module Module = struct
     in
     let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_context in
     {
+      rvar_to_string;
       r_to_string;
       type_var_id_to_string;
       type_def_id_to_string;
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 78109913..9adbf4a6 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -37,8 +37,8 @@ let erase_regions (ty : T.rty) : T.ety =
 
 (** Erase the regions in a type and substitute the type variables *)
 let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
-    (ty : T.rty) : T.ety =
-  let rsubst (_ : T.RegionVarId.id T.region) : T.erased_region = T.Erased in
+    (ty : 'r T.region T.ty) : T.ety =
+  let rsubst (_ : 'r T.region) : T.erased_region = T.Erased in
   ty_substitute rsubst tsubst ty
 
 (** Create a type substitution from a list of type variable ids and a list of
diff --git a/src/Types.ml b/src/Types.ml
index 59a512eb..c9eeff7e 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -9,6 +9,10 @@ module VariantId = IdGen ()
 module FieldId = IdGen ()
 
 module RegionVarId = IdGen ()
+(** Region variable ids. Used in function signatures. *)
+
+module RegionId = IdGen ()
+(** Region ids. Used for symbolic executions. *)
 
 type ('id, 'name) indexed_var = {
   index : 'id;  (** Unique index identifying the variable *)
@@ -79,19 +83,25 @@ type 'r ty =
 [@@deriving show]
 (* TODO: group Bool, Char, etc. in Constant *)
 
-type rty = RegionVarId.id region ty [@@deriving show]
-(** Type with *R*egions.
+type sty = RegionVarId.id region ty [@@deriving show]
+(** *S*ignature types.
 
     Used in function signatures and type definitions.
  *)
 
+type rty = RegionId.id region ty [@@deriving show]
+(** Type with *R*egions.
+
+    Used during symbolic execution.
+ *)
+
 type ety = erased_region ty [@@deriving show]
 (** Type with *E*rased regions.
     
     Used in function bodies, "general" value types, etc.
  *)
 
-type field = { field_name : string; field_ty : rty } [@@deriving show]
+type field = { field_name : string; field_ty : sty } [@@deriving show]
 
 type variant = { variant_name : string; fields : field list } [@@deriving show]
 
diff --git a/src/Values.ml b/src/Values.ml
index 4b5b9b4e..96feb814 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -13,8 +13,6 @@ module SymbolicValueId = IdGen ()
 
 module AbstractionId = IdGen ()
 
-module RegionId = IdGen ()
-
 (** A variable *)
 
 type big_int = Z.t