Remove regions_hierarchy.rs

charon-ml/src/Collections.ml

@@ -112,6 +112,10 @@ module List = struct
       f ();
       iter_times (n - 1) f)
     else ()
+
+  let filter_mapi (f : int -> 'a -> 'b option) (l : 'a list) : 'b list =
+    let l = mapi f l in
+    filter_map (fun x -> x) l
 end
 
 module type OrderedType = sig
@@ -149,6 +153,7 @@ module type Map = sig
 
   val add_list : (key * 'a) list -> 'a t -> 'a t
   val of_list : (key * 'a) list -> 'a t
+  val keys : 'a t -> key list
   val values : 'a t -> 'a list
 
   (** "Simple" pretty printing function.
@@ -192,6 +197,7 @@ module MakeMap (Ord : OrderedType) : Map with type key = Ord.t = struct
 
   let add_list bl m = List.fold_left (fun s (key, e) -> add key e s) m bl
   let of_list bl = add_list bl empty
+  let keys m = List.map fst (bindings m)
   let values m = List.map snd (bindings m)
 
   let to_string indent_opt a_to_string m =

charon-ml/src/GAst.ml

@@ -32,14 +32,14 @@ type var = {
 class ['self] iter_ast_base =
   object (_self : 'self)
     inherit [_] iter_rvalue
-    method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
+    inherit! [_] iter_predicates
   end
 
 (** Ancestor the AST map visitors *)
 class ['self] map_ast_base =
   object (_self : 'self)
     inherit [_] map_rvalue
-    method visit_meta : 'env -> meta -> meta = fun _ x -> x
+    inherit! [_] map_predicates
   end
 
 (* Below: the types need not be mutually recursive, but it makes it easier
@@ -97,7 +97,6 @@ type fun_sig = {
   parent_params_info : params_info option;
   inputs : ty list;
   output : ty;
-  regions_hierarchy : region_groups;
 }
 [@@deriving show]
 

charon-ml/src/GAstOfJson.ml

@@ -495,8 +495,8 @@ let trait_clause_of_json (id_to_file : id_to_file_map) (js : json) :
         let* clause_id = T.TraitClauseId.id_of_json clause_id in
         let* meta = option_of_json (meta_of_json id_to_file) meta in
         let* trait_id = T.TraitDeclId.id_of_json trait_id in
-        let* generics = generic_args_of_json generics in
-        Ok ({ clause_id; meta; trait_id; generics } : T.trait_clause)
+        let* clause_generics = generic_args_of_json generics in
+        Ok ({ clause_id; meta; trait_id; clause_generics } : T.trait_clause)
     | _ -> Error "")
 
 let generic_params_of_json (id_to_file : id_to_file_map) (js : json) :
@@ -589,7 +589,6 @@ let type_decl_of_json (id_to_file : id_to_file_map) (js : json) :
           ("generics", generics);
           ("preds", preds);
           ("kind", kind);
-          ("regions_hierarchy", regions_hierarchy);
         ] ->
         let* def_id = T.TypeDeclId.id_of_json def_id in
         let* meta = meta_of_json id_to_file meta in
@@ -598,18 +597,7 @@ let type_decl_of_json (id_to_file : id_to_file_map) (js : json) :
         let* generics = generic_params_of_json id_to_file generics in
         let* preds = predicates_of_json preds in
         let* kind = type_decl_kind_of_json id_to_file kind in
-        let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
-        Ok
-          {
-            T.def_id;
-            meta;
-            is_local;
-            name;
-            generics;
-            preds;
-            kind;
-            regions_hierarchy;
-          }
+        Ok { T.def_id; meta; is_local; name; generics; preds; kind }
     | _ -> Error "")
 
 let var_of_json (js : json) : (A.var, string) result =
@@ -912,7 +900,6 @@ let fun_sig_of_json (id_to_file : id_to_file_map) (js : json) :
           ("parent_params_info", parent_params_info);
           ("inputs", inputs);
           ("output", output);
-          ("regions_hierarchy", regions_hierarchy);
         ] ->
         let* is_unsafe = bool_of_json is_unsafe in
         let* generics = generic_params_of_json id_to_file generics in
@@ -922,17 +909,7 @@ let fun_sig_of_json (id_to_file : id_to_file_map) (js : json) :
         in
         let* inputs = list_of_json ty_of_json inputs in
         let* output = ty_of_json output in
-        let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
-        Ok
-          {
-            A.is_unsafe;
-            generics;
-            preds;
-            parent_params_info;
-            inputs;
-            output;
-            regions_hierarchy;
-          }
+        Ok { A.is_unsafe; generics; preds; parent_params_info; inputs; output }
     | _ -> Error "")
 
 let call_of_json (js : json) : (A.call, string) result =

charon-ml/src/GAstUtils.ml

@@ -6,14 +6,14 @@ module T = Types
 
     This list *doesn't* include the current region.
  *)
-let rec list_ancestor_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) :
-    T.RegionGroupId.Set.t =
-  let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in
+let rec list_ancestor_region_groups (regions_hierarchy : T.region_groups)
+    (gid : T.RegionGroupId.id) : T.RegionGroupId.Set.t =
+  let rg = T.RegionGroupId.nth regions_hierarchy gid in
   let parents =
     List.fold_left
       (fun s gid ->
         (* Compute the parents *)
-        let parents = list_ancestor_region_groups sg gid in
+        let parents = list_ancestor_region_groups regions_hierarchy gid in
         (* Parents U current region *)
         let parents = T.RegionGroupId.Set.add gid parents in
         (* Make the union with the accumulator *)
@@ -23,13 +23,13 @@ let rec list_ancestor_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) :
   parents
 
 (** Small utility: same as {!list_ancestor_region_groups}, but returns an ordered list.  *)
-let list_ordered_ancestor_region_groups (sg : fun_sig)
+let list_ordered_ancestor_region_groups (regions_hierarchy : T.region_groups)
     (gid : T.RegionGroupId.id) : T.RegionGroupId.id list =
-  let pset = list_ancestor_region_groups sg gid in
+  let pset = list_ancestor_region_groups regions_hierarchy gid in
   let parents =
     List.filter
       (fun (rg : T.region_group) -> T.RegionGroupId.Set.mem rg.id pset)
-      sg.regions_hierarchy
+      regions_hierarchy
   in
   let parents = List.map (fun (rg : T.region_group) -> rg.id) parents in
   parents

charon-ml/src/LlbcOfJson.ml

@@ -142,7 +142,6 @@ let global_decl_of_json (id_to_file : id_to_file_map) (js : json)
          generics = TypesUtils.mk_empty_generic_params;
          preds = TypesUtils.mk_empty_predicates;
          parent_params_info = None;
-         regions_hierarchy = [];
          inputs = [];
          output = ty;
        }

charon-ml/src/PrintTypes.ml

@@ -171,7 +171,7 @@ let trait_clause_to_string (fmt : type_formatter) (clause : T.trait_clause) :
     string =
   let clause_id = fmt.trait_clause_id_to_string clause.clause_id in
   let trait_id = fmt.trait_decl_id_to_string clause.trait_id in
-  let generics = generic_args_to_string fmt clause.generics in
+  let generics = generic_args_to_string fmt clause.clause_generics in
   "[" ^ clause_id ^ "]: " ^ trait_id ^ generics
 
 let generic_params_to_strings (fmt : type_formatter)

charon-ml/src/Types.ml

@@ -237,7 +237,6 @@ type assumed_ty = TBox | TArray | TSlice | TStr
 *)
 and type_id = TAdtId of type_decl_id | TTuple | TAssumed of assumed_ty
 
-(* TODO: we should prefix the type variants with "T", this would avoid collisions *)
 and ty =
   | TAdt of type_id * generic_args
       (** {!Types.ty.TAdt} encodes ADTs, tuples and assumed types *)
@@ -330,24 +329,76 @@ and region =
         polymorphic = false;
       }]
 
+(** Ancestor for iter visitor for {!type: Types.predicates} *)
+class ['self] iter_predicates_base =
+  object (self : 'self)
+    inherit [_] iter_ty
+    method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
+
+    method visit_type_var : 'env -> type_var -> unit =
+      fun env x ->
+        let { index; name } : type_var = x in
+        self#visit_type_var_id env index;
+        self#visit_string env name
+
+    method visit_region_var : 'env -> region_var -> unit =
+      fun env x ->
+        let { index; name } : region_var = x in
+        self#visit_region_id env index;
+        self#visit_option self#visit_string env name
+
+    method visit_const_generic_var : 'env -> const_generic_var -> unit =
+      fun env x ->
+        let { index; name; ty } : const_generic_var = x in
+        self#visit_const_generic_var_id env index;
+        self#visit_string env name;
+        self#visit_literal_type env ty
+  end
+
+(** Ancestor for map visitor for {!type: Types.ty} *)
+class virtual ['self] map_predicates_base =
+  object (self : 'self)
+    inherit [_] map_ty
+    method visit_meta : 'env -> meta -> meta = fun _ x -> x
+
+    method visit_region_var : 'env -> region_var -> region_var =
+      fun env x ->
+        let { index; name } : region_var = x in
+        let index = self#visit_region_id env index in
+        let name = self#visit_option self#visit_string env name in
+        { index; name }
+
+    method visit_type_var : 'env -> type_var -> type_var =
+      fun env x ->
+        let { index; name } : type_var = x in
+        let index = self#visit_type_var_id env index in
+        let name = self#visit_string env name in
+        { index; name }
+
+    method visit_const_generic_var
+        : 'env -> const_generic_var -> const_generic_var =
+      fun env x ->
+        let { index; name; ty } : const_generic_var = x in
+        let index = self#visit_const_generic_var_id env index in
+        let name = self#visit_string env name in
+        let ty = self#visit_literal_type env ty in
+        { index; name; ty }
+  end
+
 (** Type with erased regions (this only has an informative purpose) *)
-type ety = ty [@@deriving show, ord]
+type ety = ty
 
 (** Type with non-erased regions (this only has an informative purpose) *)
-type rty = ty [@@deriving show, ord]
-
-type field = { meta : meta; field_name : string option; field_ty : ty }
-[@@deriving show]
+and rty = ty
 
-type trait_clause = {
+and trait_clause = {
   clause_id : trait_clause_id;
   meta : meta option;
   trait_id : trait_decl_id;
-  generics : generic_args;
+  clause_generics : generic_args;
 }
-[@@deriving show]
 
-type generic_params = {
+and generic_params = {
   regions : region_var list;
   types : type_var list;
       (** The type parameters can be indexed with {!Types.TypeVarId.id}.
@@ -361,25 +412,45 @@ type generic_params = {
        *)
   trait_clauses : trait_clause list;
 }
-[@@deriving show]
 
-type region_outlives = region * region [@@deriving show]
-type type_outlives = ty * region [@@deriving show]
+(** ('long, 'short) means that 'long outlives 'short *)
+and region_outlives = region * region
+
+(** (T, 'a) means that T outlives 'a *)
+and type_outlives = ty * region
 
-type trait_type_constraint = {
+and trait_type_constraint = {
   trait_ref : trait_ref;
   generics : generic_args;
   type_name : trait_item_name;
   ty : ty;
 }
-[@@deriving show]
 
-type predicates = {
+and predicates = {
   regions_outlive : region_outlives list;
   types_outlive : type_outlives list;
   trait_type_constraints : trait_type_constraint list;
 }
-[@@deriving show]
+[@@deriving
+  show,
+    visitors
+      {
+        name = "iter_predicates";
+        variety = "iter";
+        ancestors = [ "iter_predicates_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        concrete = true;
+        polymorphic = false;
+      },
+    visitors
+      {
+        name = "map_predicates";
+        variety = "map";
+        ancestors = [ "map_predicates_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.map} *);
+        concrete = false;
+        polymorphic = false;
+      }]
 
 (** A group of regions.
 
@@ -398,6 +469,9 @@ type 'id g_region_group = {
 type region_group = RegionGroupId.id g_region_group [@@deriving show]
 type region_groups = region_group list [@@deriving show]
 
+type field = { meta : meta; field_name : string option; field_ty : ty }
+[@@deriving show]
+
 type variant = {
   meta : meta;
   variant_name : string;
@@ -432,9 +506,5 @@ type type_decl = {
   generics : generic_params;
   preds : predicates;
   kind : type_decl_kind;
-  regions_hierarchy : region_groups;
-      (** Stores the hierarchy between the regions (which regions have the
-          same lifetime, which lifetime should end before which other lifetime,
-          etc.) *)
 }
 [@@deriving show]

charon-ml/src/TypesUtils.ml

@@ -1,6 +1,19 @@
+open Collections
 open Types
 open Utils
 
+module RegionOrderedType : OrderedType with type t = region = struct
+  type t = region
+
+  let compare = compare_region
+  let to_string = show_region
+  let pp_t = pp_region
+  let show_t = show_region
+end
+
+module RegionMap = Collections.MakeMap (RegionOrderedType)
+module RegionSet = Collections.MakeSet (RegionOrderedType)
+
 let type_decl_is_opaque (d : type_decl) : bool =
   match d.kind with Struct _ | Enum _ -> false | Opaque -> true
 

charon/src/driver.rs

@@ -7,7 +7,6 @@ use crate::index_to_function_calls;
 use crate::insert_assign_return_unit;
 use crate::ops_to_function_calls;
 use crate::reconstruct_asserts;
-use crate::regions_hierarchy;
 use crate::remove_drop_never;
 use crate::remove_dynamic_checks;
 use crate::remove_read_discriminant;
@@ -169,10 +168,6 @@ pub fn translate(sess: &Session, tcx: TyCtxt, internal: &CharonCallbacks) -> Res
     // - group the mutually recursive definitions
     let ordered_decls = reorder_decls::reorder_declarations(&ctx)?;
 
-    // # Compute the regions hierarchies for the types and the function signatures
-    // TODO: move to Aeneas
-    regions_hierarchy::compute(&mut ctx, &ordered_decls);
-
     //
     // =================
     // **Micro-passes**:

charon/src/lib.rs

@@ -69,7 +69,6 @@ pub mod names;
 pub mod names_utils;
 pub mod ops_to_function_calls;
 pub mod reconstruct_asserts;
-pub mod regions_hierarchy;
 pub mod remove_drop_never;
 pub mod remove_dynamic_checks;
 pub mod remove_read_discriminant;