Merge pull request #253 from Nadrieril/merge-preds-into-params

10 files changed, 67 insertions, 77 deletions

diff --git a/charon-pin b/charon-pin
index 082212e1..838e423c 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-28dc4f9b826031754fcd32c82355f6d0be05faca
+81c0edf20eefb55a0b2f2bc5ab029ec96e75a82c
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 1c335d8d..4de5382a 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -122,11 +122,14 @@ let norm_ctx_to_fmt_env (ctx : norm_ctx) : Print.fmt_env =
     global_decls = ctx.global_decls;
     trait_decls = ctx.trait_decls;
     trait_impls = ctx.trait_impls;
-    types = ctx.type_vars;
-    const_generics = ctx.const_generic_vars;
     regions = [];
-    trait_clauses = [];
-    preds = empty_predicates;
+    generics =
+      {
+        TypesUtils.empty_generic_params with
+        types = ctx.type_vars;
+        const_generics = ctx.const_generic_vars;
+        trait_clauses = [];
+      };
     locals = [];
   }
 
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 1807add5..1720b132 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -66,7 +66,15 @@ module Sig = struct
     { regions; types; const_generics; trait_refs = [] }
 
   let mk_generic_params regions types const_generics : generic_params =
-    { regions; types; const_generics; trait_clauses = [] }
+    {
+      regions;
+      types;
+      const_generics;
+      trait_clauses = [];
+      regions_outlive = [];
+      types_outlive = [];
+      trait_type_constraints = [];
+    }
 
   let mk_ref_ty (r : region) (ty : ty) (is_mut : bool) : ty =
     let ref_kind = if is_mut then RMut else RShared in
@@ -79,15 +87,11 @@ module Sig = struct
     TAdt (TAssumed TSlice, mk_generic_args [] [ ty ] [])
 
   let mk_sig generics inputs output : fun_sig =
-    let preds : predicates =
-      { regions_outlive = []; types_outlive = []; trait_type_constraints = [] }
-    in
     {
       is_unsafe = false;
       is_closure = false;
       closure_info = None;
       generics;
-      preds;
       parent_params_info = None;
       inputs;
       output;
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index b2e55841..7e292906 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -78,7 +78,7 @@ let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
     | TraitItemDecl _ | TraitItemProvided _ -> Self
   in
   let generics =
-    let { regions; types; const_generics; trait_clauses } = sg.generics in
+    let { regions; types; const_generics; trait_clauses; _ } = sg.generics in
     let regions = List.map (fun _ -> RErased) regions in
     let types = List.map (fun (v : type_var) -> TVar v.index) types in
     let const_generics =
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 8bd709d0..76793548 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -426,7 +426,6 @@ module Contexts = struct
     let global_decls = ctx.global_ctx.global_decls in
     let trait_decls = ctx.trait_decls_ctx.trait_decls in
     let trait_impls = ctx.trait_impls_ctx.trait_impls in
-    let preds = TypesUtils.empty_predicates in
     {
       type_decls;
       fun_decls;
@@ -434,10 +433,7 @@ module Contexts = struct
       trait_decls;
       trait_impls;
       regions = [];
-      types = [];
-      const_generics = [];
-      trait_clauses = [];
-      preds;
+      generics = TypesUtils.empty_generic_params;
       locals = [];
     }
 
@@ -450,8 +446,6 @@ module Contexts = struct
     (* Below: it is always safe to omit fields - if an id can't be found at
        printing time, we print the id (in raw form) instead of the name it
        designates. *)
-    (* We don't need the predicates so we initialize them to empty *)
-    let preds = empty_predicates in
     (* For the locals: we retrieve the information from the environment.
        Note that the locals don't need to be ordered based on their indices.
     *)
@@ -469,13 +463,16 @@ module Contexts = struct
       global_decls;
       trait_decls;
       trait_impls;
-      types = ctx.type_vars;
       (* The regions have been transformed to region groups *)
       regions = [];
-      const_generics = ctx.const_generic_vars;
-      (* We don't need the trait clauses so we initialize them to empty *)
-      trait_clauses = [];
-      preds;
+      generics =
+        {
+          TypesUtils.empty_generic_params with
+          types = ctx.type_vars;
+          const_generics = ctx.const_generic_vars;
+          (* We don't need the trait clauses so we initialize them to empty *)
+          trait_clauses = [];
+        };
       locals;
     }
 
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index fe7c1234..413f7f0d 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -58,10 +58,7 @@ let fmt_env_to_llbc_fmt_env (env : fmt_env) : Print.fmt_env =
     trait_decls = env.trait_decls;
     trait_impls = env.trait_impls;
     regions = [];
-    types = [];
-    const_generics = [];
-    trait_clauses = [];
-    preds = TypesUtils.empty_predicates;
+    generics = TypesUtils.empty_generic_params;
     locals = [];
   }
 
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index 3ec42f5d..c608c02e 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -53,7 +53,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
   let norm_ctx : AssociatedTypes.norm_ctx =
     let norm_trait_types =
       AssociatedTypes.compute_norm_trait_types_from_preds span
-        sg.preds.trait_type_constraints
+        sg.generics.trait_type_constraints
     in
     {
       span;
@@ -130,7 +130,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
 
   (* Explore the clauses - we only explore the "region outlives" clause,
      not the "type outlives" clauses *)
-  List.iter add_edge_from_region_constraint sg.preds.regions_outlive;
+  List.iter add_edge_from_region_constraint sg.generics.regions_outlive;
 
   (* Explore the types in the signature to add the edges *)
   let rec explore_ty (outer : region list) (ty : ty) =
@@ -148,7 +148,9 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
             let subst =
               Subst.make_subst_from_generics decl.generics generics tr_self
             in
-            let predicates = Subst.predicates_substitute subst decl.preds in
+            let predicates =
+              Subst.generic_params_substitute subst decl.generics
+            in
             (* Note that because we also explore the generics below, we may
                explore several times the same type - this is ok *)
             List.iter
@@ -312,10 +314,7 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t)
       trait_decls;
       trait_impls;
       regions = [];
-      types = [];
-      const_generics = [];
-      trait_clauses = [];
-      preds = empty_predicates;
+      generics = empty_generic_params;
       locals = [];
     }
   in
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 6ea460db..203bfac3 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -119,7 +119,7 @@ let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id)
   let trait_type_constraints =
     List.map
       (trait_type_constraint_substitute subst)
-      sg.preds.trait_type_constraints
+      sg.generics.trait_type_constraints
   in
   { inputs; output; regions_hierarchy; trait_type_constraints }
 
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 1b5da858..7aa5c558 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -294,10 +294,7 @@ let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
   let global_decls = ctx.global_ctx.llbc_global_decls in
   let trait_decls = ctx.trait_decls_ctx in
   let trait_impls = ctx.trait_impls_ctx in
-  let { regions; types; const_generics; trait_clauses } : T.generic_params =
-    ctx.fun_decl.signature.generics
-  in
-  let preds = ctx.fun_decl.signature.preds in
+  let { regions; _ } : T.generic_params = ctx.fun_decl.signature.generics in
   {
     type_decls;
     fun_decls;
@@ -305,10 +302,7 @@ let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
     trait_decls;
     trait_impls;
     regions = [ regions ];
-    types;
-    const_generics;
-    trait_clauses;
-    preds;
+    generics = ctx.fun_decl.signature.generics;
     locals = [];
   }
 
@@ -527,20 +521,23 @@ let translate_strait_type_constraint (span : Meta.span)
   let ty = translate_sty span ty in
   { trait_ref; type_name; ty }
 
-let translate_predicates (span : Meta.span) (preds : T.predicates) : predicates
-    =
-  let trait_type_constraints =
-    List.map
-      (translate_strait_type_constraint span)
-      preds.trait_type_constraints
-  in
-  { trait_type_constraints }
-
 let translate_generic_params (span : Meta.span) (generics : T.generic_params) :
-    generic_params =
-  let { T.regions = _; types; const_generics; trait_clauses } = generics in
+    generic_params * predicates =
+  let {
+    T.regions = _;
+    types;
+    const_generics;
+    trait_clauses;
+    trait_type_constraints;
+    _;
+  } =
+    generics
+  in
   let trait_clauses = List.map (translate_trait_clause span) trait_clauses in
-  { types; const_generics; trait_clauses }
+  let trait_type_constraints =
+    List.map (translate_strait_type_constraint span) trait_type_constraints
+  in
+  ({ types; const_generics; trait_clauses }, { trait_type_constraints })
 
 let translate_field (span : Meta.span) (f : T.field) : field =
   let field_name = f.field_name in
@@ -588,16 +585,14 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let def_id = def.T.def_id in
   let llbc_name = def.name in
   let name = Print.Types.name_to_string env def.name in
-  let { T.regions; types; const_generics; trait_clauses } = def.generics in
   (* Can't translate types with regions for now *)
-  cassert __FILE__ __LINE__ (regions = []) def.item_meta.span
-    "ADTs containing borrows are not supported yet";
-  let trait_clauses =
-    List.map (translate_trait_clause def.item_meta.span) trait_clauses
+  cassert __FILE__ __LINE__
+    (def.generics.regions = [])
+    def.item_meta.span "ADTs containing borrows are not supported yet";
+  let generics, preds =
+    translate_generic_params def.item_meta.span def.generics
   in
-  let generics = { types; const_generics; trait_clauses } in
   let kind = translate_type_decl_kind def.item_meta.span def.T.kind in
-  let preds = translate_predicates def.item_meta.span def.preds in
   let is_local = def.is_local in
   let item_meta = def.item_meta in
   {
@@ -1019,7 +1014,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (span : Meta.span)
     in
     (* Compute the normalization map for the *sty* types and add it to the context *)
     AssociatedTypes.ctx_add_norm_trait_types_from_preds span ctx
-      sg.preds.trait_type_constraints
+      sg.generics.trait_type_constraints
   in
 
   (* Normalize the signature *)
@@ -1247,10 +1242,9 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (span : Meta.span)
   in
 
   (* Generic parameters *)
-  let generics = translate_generic_params span sg.generics in
+  let generics, preds = translate_generic_params span sg.generics in
 
   (* Return *)
-  let preds = translate_predicates span sg.preds in
   {
     generics;
     llbc_generics = sg.generics;
@@ -3943,7 +3937,6 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     name = llbc_name;
     item_meta;
     generics = llbc_generics;
-    preds;
     parent_clauses = llbc_parent_clauses;
     consts;
     types;
@@ -3958,10 +3951,9 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics =
+  let generics, preds =
     translate_generic_params trait_decl.item_meta.span llbc_generics
   in
-  let preds = translate_predicates trait_decl.item_meta.span preds in
   let parent_clauses =
     List.map
       (translate_trait_clause trait_decl.item_meta.span)
@@ -4011,7 +4003,6 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     item_meta;
     impl_trait = llbc_impl_trait;
     generics = llbc_generics;
-    preds;
     parent_trait_refs;
     consts;
     types;
@@ -4031,10 +4022,9 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics =
+  let generics, preds =
     translate_generic_params trait_impl.item_meta.span llbc_generics
   in
-  let preds = translate_predicates trait_impl.item_meta.span preds in
   let parent_trait_refs =
     List.map (translate_strait_ref trait_impl.item_meta.span) parent_trait_refs
   in
@@ -4080,7 +4070,6 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
     is_local;
     name = llbc_name;
     generics = llbc_generics;
-    preds;
     ty;
     kind;
     body = body_id;
@@ -4092,8 +4081,9 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
       (Print.Contexts.decls_ctx_to_fmt_env ctx)
       llbc_name
   in
-  let generics = translate_generic_params decl.item_meta.span llbc_generics in
-  let preds = translate_predicates decl.item_meta.span preds in
+  let generics, preds =
+    translate_generic_params decl.item_meta.span llbc_generics
+  in
   let ty = translate_fwd_ty decl.item_meta.span ctx.type_ctx.type_infos ty in
   {
     span = item_meta.span;
diff --git a/flake.lock b/flake.lock
index 56f4c386..948d25d2 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1718717065,
-        "narHash": "sha256-ZkoUvx9HMBKTKDh7MnMEEocAGZaLkQqVApB0IlfxRYk=",
+        "lastModified": 1718897879,
+        "narHash": "sha256-sRbyKlrsEgx7FYDjlYeQpT8wLUgfBiNnMqEQ5029K14=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "28dc4f9b826031754fcd32c82355f6d0be05faca",
+        "rev": "81c0edf20eefb55a0b2f2bc5ab029ec96e75a82c",
         "type": "github"
       },
       "original": {