Update the types and deserialization following charon's updates

9 files changed, 146 insertions, 152 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index ac66d1a4..6d8c03e4 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -5,8 +5,6 @@ open Expressions
 
 module FunDefId = IdGen ()
 
-module RegionGroupId = IdGen ()
-
 type var = {
   index : VarId.id;  (** Unique variable identifier *)
   name : string option;
@@ -26,28 +24,6 @@ type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id
 
 type assertion = { cond : operand; expected : bool } [@@deriving show]
 
-type ('id, 'r) g_region_group = {
-  id : 'id;
-  regions : 'r list;
-  parents : 'id list;
-}
-[@@deriving show]
-(** A group of regions.
-
-    Results from a lifetime analysis: we group the regions with the same
-    lifetime together, and compute the hierarchy between the regions.
-    This is necessary to introduce the proper abstraction with the
-    proper constraints, when evaluating a function call in symbolic mode.
-*)
-
-type ('r, 'id) g_region_groups = ('r, 'id) g_region_group list [@@deriving show]
-
-type region_var_group = (RegionGroupId.id, RegionVarId.id) g_region_group
-[@@deriving show]
-
-type region_var_groups = (RegionGroupId.id, RegionVarId.id) g_region_groups
-[@@deriving show]
-
 type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
 [@@deriving show]
 
@@ -182,7 +158,6 @@ type fun_def = {
   def_id : FunDefId.id;
   name : name;
   signature : fun_sig;
-  divergent : bool;
   arg_count : int;
   locals : var list;
   body : statement;
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index a1dd0ad1..dddfbd58 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -159,6 +159,21 @@ let type_def_kind_of_json (js : json) : (T.type_def_kind, string) result =
         Ok (T.Enum variants)
     | _ -> Error "")
 
+let region_var_group_of_json (js : json) : (T.region_var_group, string) result =
+  combine_error_msgs js "region_var_group_of_json"
+    (match js with
+    | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] ->
+        let* id = T.RegionGroupId.id_of_json id in
+        let* regions = list_of_json T.RegionVarId.id_of_json regions in
+        let* parents = list_of_json T.RegionGroupId.id_of_json parents in
+        Ok { T.id; regions; parents }
+    | _ -> Error "")
+
+let region_var_groups_of_json (js : json) : (T.region_var_groups, string) result
+    =
+  combine_error_msgs js "region_var_group_of_json"
+    (list_of_json region_var_group_of_json js)
+
 let type_def_of_json (js : json) : (T.type_def, string) result =
   combine_error_msgs js "type_def_of_json"
     (match js with
@@ -169,13 +184,23 @@ let type_def_of_json (js : json) : (T.type_def, string) result =
           ("region_params", region_params);
           ("type_params", type_params);
           ("kind", kind);
+          ("regions_hierarchy", regions_hierarchy);
         ] ->
         let* def_id = T.TypeDefId.id_of_json def_id in
         let* name = name_of_json name in
         let* region_params = list_of_json region_var_of_json region_params in
         let* type_params = list_of_json type_var_of_json type_params in
         let* kind = type_def_kind_of_json kind in
-        Ok { T.def_id; name; region_params; type_params; kind }
+        let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
+        Ok
+          {
+            T.def_id;
+            name;
+            region_params;
+            type_params;
+            kind;
+            regions_hierarchy;
+          }
     | _ -> Error "")
 
 let var_of_json (js : json) : (A.var, string) result =
@@ -436,21 +461,6 @@ let assertion_of_json (js : json) : (A.assertion, string) result =
         Ok { A.cond; expected }
     | _ -> Error "")
 
-let region_var_group_of_json (js : json) : (A.region_var_group, string) result =
-  combine_error_msgs js "region_var_group_of_json"
-    (match js with
-    | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] ->
-        let* id = A.RegionGroupId.id_of_json id in
-        let* regions = list_of_json T.RegionVarId.id_of_json regions in
-        let* parents = list_of_json A.RegionGroupId.id_of_json parents in
-        Ok { A.id; regions; parents }
-    | _ -> Error "")
-
-let region_var_groups_of_json (js : json) : (A.region_var_groups, string) result
-    =
-  combine_error_msgs js "region_var_group_of_json"
-    (list_of_json region_var_group_of_json js)
-
 let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
   combine_error_msgs js "fun_sig_of_json"
     (match js with
@@ -570,7 +580,6 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result =
           ("def_id", def_id);
           ("name", name);
           ("signature", signature);
-          ("divergent", divergent);
           ("arg_count", arg_count);
           ("locals", locals);
           ("body", body);
@@ -578,28 +587,44 @@ let fun_def_of_json (js : json) : (A.fun_def, string) result =
         let* def_id = A.FunDefId.id_of_json def_id in
         let* name = name_of_json name in
         let* signature = fun_sig_of_json signature in
-        let* divergent = bool_of_json divergent in
         let* arg_count = int_of_json arg_count in
         let* locals = list_of_json var_of_json locals in
         let* body = statement_of_json body in
-        Ok { A.def_id; name; signature; divergent; arg_count; locals; body }
+        Ok { A.def_id; name; signature; arg_count; locals; body }
     | _ -> Error "")
 
-let declaration_of_json (js : json) : (M.declaration, string) result =
+let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
+    (js : json) : ('id M.g_declaration_group, string) result =
+  combine_error_msgs js "g_declaration_group_of_json"
+    (match js with
+    | `Assoc [ ("NonRec", `List [ id ]) ] ->
+        let* id = id_of_json id in
+        Ok (M.NonRec id)
+    | `Assoc [ ("Rec", `List [ ids ]) ] ->
+        let* ids = list_of_json id_of_json ids in
+        Ok (M.Rec ids)
+    | _ -> Error "")
+
+let type_declaration_group_of_json (js : json) :
+    (M.type_declaration_group, string) result =
+  combine_error_msgs js "type_declaration_group_of_json"
+    (g_declaration_group_of_json T.TypeDefId.id_of_json js)
+
+let fun_declaration_group_of_json (js : json) :
+    (M.fun_declaration_group, string) result =
+  combine_error_msgs js "fun_declaration_group_of_json"
+    (g_declaration_group_of_json A.FunDefId.id_of_json js)
+
+let declaration_group_of_json (js : json) : (M.declaration_group, string) result
+    =
   combine_error_msgs js "declaration_of_json"
     (match js with
-    | `Assoc [ ("Type", id) ] ->
-        let* id = T.TypeDefId.id_of_json id in
-        Ok (M.Type id)
-    | `Assoc [ ("Fun", id) ] ->
-        let* id = A.FunDefId.id_of_json id in
-        Ok (M.Fun id)
-    | `Assoc [ ("RecTypes", ids) ] ->
-        let* ids = list_of_json T.TypeDefId.id_of_json ids in
-        Ok (M.RecTypes ids)
-    | `Assoc [ ("RecFuns", ids) ] ->
-        let* ids = list_of_json A.FunDefId.id_of_json ids in
-        Ok (M.RecFuns ids)
+    | `Assoc [ ("Type", `List [ decl ]) ] ->
+        let* decl = type_declaration_group_of_json decl in
+        Ok (M.Type decl)
+    | `Assoc [ ("Fun", `List [ decl ]) ] ->
+        let* decl = fun_declaration_group_of_json decl in
+        Ok (M.Fun decl)
     | _ -> Error "")
 
 let cfim_module_of_json (js : json) : (M.cfim_module, string) result =
@@ -611,7 +636,9 @@ let cfim_module_of_json (js : json) : (M.cfim_module, string) result =
           ("types", types);
           ("functions", functions);
         ] ->
-        let* declarations = list_of_json declaration_of_json declarations in
+        let* declarations =
+          list_of_json declaration_group_of_json declarations
+        in
         let* types = list_of_json type_def_of_json types in
         let* functions = list_of_json fun_def_of_json functions in
         Ok { M.declarations; types; functions }
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 1a9dcfc8..f7a24d27 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -137,7 +137,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) :
   }
 
 type type_context = {
-  type_defs_groups : M.types_decl_group TypeDefId.Map.t;
+  type_defs_groups : M.type_declaration_group TypeDefId.Map.t;
   type_defs : type_def list;
 }
 [@@deriving show]
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 9d332543..9331d9f3 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -432,11 +432,14 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
 let give_back_symbolic_value (_config : C.config)
     (proj_regions : T.RegionId.Set.t) (proj_ty : T.rty) (sv : V.symbolic_value)
     (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx =
-  let subst local_regions local_ty =
+  let subst (abs : V.abs) abs_proj_ty =
+    (* TODO: check that we can consume this symbolic value - this is not
+     * a precondition, purely a sanity check *)
+    raise Errors.Unimplemented;
     let child_proj =
       if sv.sv_id = nsv.sv_id then None
       else
-        Some (mk_aproj_borrows_from_symbolic_value local_regions nsv local_ty)
+        Some (mk_aproj_borrows_from_symbolic_value abs.regions nsv abs_proj_ty)
     in
     V.AEndedProjLoans child_proj
   in
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 455d62c3..8f6827b3 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -831,19 +831,18 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t)
     Note that the new value [nv] with which to replace the proj_loans could
     be untyped: we request a typed value for sanity checking.
     
-    [subst]: takes as parameters the projection regions and the projection type
+    [subst]: takes as parameters the abstraction and the projection type
     where we perform the substitution.
  *)
 let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
     (proj_ty : T.rty) (sv : V.symbolic_value)
-    (subst : T.RegionId.Set.t -> T.rty -> V.aproj) (ctx : C.eval_ctx) :
-    C.eval_ctx =
+    (subst : V.abs -> T.rty -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
   (* Small helpers for sanity checks *)
   let updated = ref false in
-  let update local_regions local_proj_ty : V.aproj =
+  let update abs local_proj_ty : V.aproj =
     assert (not !updated);
     updated := true;
-    subst local_regions local_proj_ty
+    subst abs local_proj_ty
   in
   (* The visitor *)
   let obj =
@@ -864,7 +863,7 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
               if
                 projections_intersect proj_ty proj_regions sv'.V.sv_ty
                   abs.regions
-              then update abs.regions sv'.V.sv_ty
+              then update abs sv'.V.sv_ty
               else super#visit_aproj (Some abs) sproj)
             else super#visit_aproj (Some abs) sproj
     end
@@ -875,47 +874,3 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
   assert !updated;
   (* Return *)
   ctx
-
-(*
-let proj_loans_intersect (proj_loans : T.RegionId.Set.t * V.symbolic_value)
-    (proj_loans' : T.RegionId.Set.t * V.symbolic_value) : bool =
-  let regions, sv = proj_loans in
-  let regions', sv' = proj_loans' in
-  if same_symbolic_id sv sv' then
-    projections_intersect sv.V.sv_ty regions sv'.V.sv_ty regions'
-  else false
-
-*)
-(*(** Substitute the proj_loans based an a symbolic id *)
-  let substitute_aproj_loans_with_id (sv : V.symbolic_value)
-      (subst : T.RegionId.Set.t -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
-    (* Small helpers for sanity checks *)
-    let updated = ref false in
-    let update regions : V.aproj =
-      updated := true;
-      subst regions
-    in
-    (* The visitor *)
-    let obj =
-      object
-        inherit [_] C.map_eval_ctx as super
-
-        method! visit_abs _ abs = super#visit_abs (Some abs) abs
-
-        method! visit_aproj abs sproj =
-          match sproj with
-          | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows
-          | AIgnoredProjBorrows ->
-              super#visit_aproj abs sproj
-          | AProjLoans sv' ->
-              let abs = Option.get abs in
-              if same_symbolic_id sv sv' then update abs.regions
-              else super#visit_aproj (Some abs) sproj
-      end
-    in
-    (* Apply *)
-    let ctx = obj#visit_eval_ctx None ctx in
-    (* Check that we updated the context at least once *)
-    assert !updated;
-    (* Return *)
-  ctx*)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index aaf7a707..85c3acb4 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -406,7 +406,7 @@ let eval_box_deref_mut_or_shared_inst_sig (region_params : T.erased_region list)
 
       let output = mk_ref_ty r ty_param ref_kind in
 
-      let regions = { A.id = abs_id; regions = [ rid ]; parents = [] } in
+      let regions = { T.id = abs_id; regions = [ rid ]; parents = [] } in
 
       let inst_sg =
         { A.regions_hierarchy = [ regions ]; inputs = [ input ]; output }
@@ -509,16 +509,16 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig)
     List.fold_left_map
       (fun ctx rg ->
         let abs_id = C.fresh_abstraction_id () in
-        (ctx, (rg.A.id, abs_id)))
+        (ctx, (rg.T.id, abs_id)))
       ctx sg.regions_hierarchy
   in
-  let asubst_map : V.AbstractionId.id A.RegionGroupId.Map.t =
+  let asubst_map : V.AbstractionId.id T.RegionGroupId.Map.t =
     List.fold_left
-      (fun mp (rg_id, abs_id) -> A.RegionGroupId.Map.add rg_id abs_id mp)
-      A.RegionGroupId.Map.empty rg_abs_ids_bindings
+      (fun mp (rg_id, abs_id) -> T.RegionGroupId.Map.add rg_id abs_id mp)
+      T.RegionGroupId.Map.empty rg_abs_ids_bindings
   in
-  let asubst (rg_id : A.RegionGroupId.id) : V.AbstractionId.id =
-    A.RegionGroupId.Map.find rg_id asubst_map
+  let asubst (rg_id : T.RegionGroupId.id) : V.AbstractionId.id =
+    T.RegionGroupId.Map.find rg_id asubst_map
   in
   (* Generate fresh regions and their substitutions *)
   let _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params in
@@ -559,23 +559,23 @@ let create_empty_abstractions_from_abs_region_groups (kind : V.abs_kind)
   in
   (* Auxiliary function to create one abstraction *)
   let create_abs (rg : A.abs_region_group) : V.abs =
-    let abs_id = rg.A.id in
+    let abs_id = rg.T.id in
     let parents =
       List.fold_left
         (fun s pid -> V.AbstractionId.Set.add pid s)
-        V.AbstractionId.Set.empty rg.A.parents
+        V.AbstractionId.Set.empty rg.parents
     in
     let regions =
       List.fold_left
         (fun s rid -> T.RegionId.Set.add rid s)
-        T.RegionId.Set.empty rg.A.regions
+        T.RegionId.Set.empty rg.regions
     in
     let ancestors_regions =
       List.fold_left
         (fun acc parent_id ->
           T.RegionId.Set.union acc
             (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
-        T.RegionId.Set.empty rg.A.parents
+        T.RegionId.Set.empty rg.parents
     in
     let ancestors_regions_union_current_regions =
       T.RegionId.Set.union ancestors_regions regions
@@ -800,9 +800,10 @@ and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) :
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
 and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
-    (fid : A.FunDefId.id) (_region_params : T.erased_region list)
+    (fid : A.FunDefId.id) (region_params : T.erased_region list)
     (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
     C.eval_ctx eval_result list =
+  assert (region_params = []);
   (* Retrieve the (correctly instantiated) body *)
   let def = C.ctx_lookup_fun_def ctx fid in
   let tsubst =
@@ -883,6 +884,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     (ctx : C.eval_ctx) (fid : A.fun_id) (inst_sg : A.inst_fun_sig)
     (region_params : T.erased_region list) (type_params : T.ety list)
     (args : E.operand list) (dest : E.place) : C.eval_ctx =
+  assert (region_params = []);
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.A.output in
   let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in
@@ -899,6 +901,11 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
       (fun ((arg, rty) : V.typed_value * T.rty) ->
         arg.V.ty = Subst.erase_regions rty)
       args_with_rtypes);
+  (* Check that the input arguments don't contain symbolic values that can't 
+   * be fed to functions (i.e., symbolic values output from function return
+   * values and which contain borrows of borrows can't be used as function
+   * inputs *)
+  raise Errors.Unimplemented;
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let empty_absl =
     create_empty_abstractions_from_abs_region_groups V.FunCall
diff --git a/src/Modules.ml b/src/Modules.ml
index e4cb06c1..e437ad0a 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -1,55 +1,55 @@
 open Types
 open CfimAst
 
+type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
+[@@deriving show]
+
+type type_declaration_group = TypeDefId.id g_declaration_group [@@deriving show]
+
+type fun_declaration_group = FunDefId.id g_declaration_group [@@deriving show]
+
 (** Module declaration *)
-type declaration =
-  | Type of TypeDefId.id
-  | Fun of FunDefId.id
-  | RecTypes of TypeDefId.id list
-  | RecFuns of FunDefId.id list
+type declaration_group =
+  | Type of type_declaration_group
+  | Fun of fun_declaration_group
+[@@deriving show]
 
 type cfim_module = {
-  declarations : declaration list;
+  declarations : declaration_group list;
   types : type_def list;
   functions : fun_def list;
 }
 (** CFIM module *)
 
-type 'id decl_group = NonRec of 'id | Rec of 'id list [@@deriving show]
-
-type types_decl_group = TypeDefId.id decl_group [@@deriving show]
-
-type funs_decl_group = FunDefId.id decl_group [@@deriving show]
-
 (** Split a module's declarations between types and functions *)
-let split_declarations (decls : declaration list) :
-    types_decl_group list * funs_decl_group list =
+let split_declarations (decls : declaration_group list) :
+    type_declaration_group list * fun_declaration_group list =
   let rec split decls =
     match decls with
     | [] -> ([], [])
     | d :: decls' -> (
         let types, funs = split decls' in
         match d with
-        | Type id -> (NonRec id :: types, funs)
-        | Fun id -> (types, NonRec id :: funs)
-        | RecTypes ids -> (Rec ids :: types, funs)
-        | RecFuns ids -> (types, Rec ids :: funs))
+        | Type decl -> (decl :: types, funs)
+        | Fun decl -> (types, decl :: funs))
   in
   split decls
 
 (** Split a module's declarations into two maps from type/fun ids to
     declaration groups.
  *)
-let split_declarations_to_group_maps (decls : declaration list) :
-    types_decl_group TypeDefId.Map.t * funs_decl_group FunDefId.Map.t =
+let split_declarations_to_group_maps (decls : declaration_group list) :
+    type_declaration_group TypeDefId.Map.t
+    * fun_declaration_group FunDefId.Map.t =
   let module G (M : Map.S) = struct
-    let add_group (map : M.key decl_group M.t) (group : M.key decl_group) :
-        M.key decl_group M.t =
+    let add_group (map : M.key g_declaration_group M.t)
+        (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
       match group with
       | NonRec id -> M.add id group map
       | Rec ids -> List.fold_left (fun map id -> M.add id group map) map ids
 
-    let create_map (groups : M.key decl_group list) : M.key decl_group M.t =
+    let create_map (groups : M.key g_declaration_group list) :
+        M.key g_declaration_group M.t =
       List.fold_left add_group M.empty groups
   end in
   let types, funs = split_declarations decls in
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 62a737ad..9db58812 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -323,7 +323,7 @@ let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
   (locals, body)
 
 (** Substitute a function signature *)
-let substitute_signature (asubst : A.RegionGroupId.id -> V.AbstractionId.id)
+let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
     (rsubst : T.RegionVarId.id -> T.RegionId.id)
     (tsubst : T.TypeVarId.id -> T.rty) (sg : A.fun_sig) : A.inst_fun_sig =
   let rsubst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region =
@@ -331,11 +331,11 @@ let substitute_signature (asubst : A.RegionGroupId.id -> V.AbstractionId.id)
   in
   let inputs = List.map (ty_substitute rsubst' tsubst) sg.A.inputs in
   let output = ty_substitute rsubst' tsubst sg.A.output in
-  let subst_region_group (rg : A.region_var_group) : A.abs_region_group =
-    let id = asubst rg.A.id in
-    let regions = List.map rsubst rg.A.regions in
-    let parents = List.map asubst rg.A.parents in
-    { A.id; regions; parents }
+  let subst_region_group (rg : T.region_var_group) : A.abs_region_group =
+    let id = asubst rg.id in
+    let regions = List.map rsubst rg.regions in
+    let parents = List.map asubst rg.parents in
+    { id; regions; parents }
   in
   let regions_hierarchy = List.map subst_region_group sg.A.regions_hierarchy in
   { A.regions_hierarchy; inputs; output }
diff --git a/src/Types.ml b/src/Types.ml
index b410c5a6..44855eb2 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -14,6 +14,8 @@ module RegionVarId = IdGen ()
 module RegionId = IdGen ()
 (** Region ids. Used for symbolic executions. *)
 
+module RegionGroupId = IdGen ()
+
 type ('id, 'name) indexed_var = {
   index : 'id;  (** Unique index identifying the variable *)
   name : 'name;  (** Variable name *)
@@ -46,6 +48,28 @@ type 'rid region =
  *)
 type erased_region = Erased [@@deriving show]
 
+type ('id, 'r) g_region_group = {
+  id : 'id;
+  regions : 'r list;
+  parents : 'id list;
+}
+[@@deriving show]
+(** A group of regions.
+
+    Results from a lifetime analysis: we group the regions with the same
+    lifetime together, and compute the hierarchy between the regions.
+    This is necessary to introduce the proper abstraction with the
+    proper constraints, when evaluating a function call in symbolic mode.
+*)
+
+type ('r, 'id) g_region_groups = ('r, 'id) g_region_group list [@@deriving show]
+
+type region_var_group = (RegionGroupId.id, RegionVarId.id) g_region_group
+[@@deriving show]
+
+type region_var_groups = (RegionGroupId.id, RegionVarId.id) g_region_groups
+[@@deriving show]
+
 type integer_type =
   | Isize
   | I8
@@ -174,5 +198,8 @@ type type_def = {
   region_params : region_var list;
   type_params : type_var list;
   kind : type_def_kind;
+  regions_hierarchy : region_var_groups;
+      (** Stored the hierarchy between the regions (which regions have the same lifetime,
+          what is the hierarchy between the lifetimes) *)
 }
 [@@deriving show]