summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/AssociatedTypes.ml11
-rw-r--r--compiler/Assumed.ml14
-rw-r--r--compiler/Interpreter.ml2
-rw-r--r--compiler/Print.ml21
-rw-r--r--compiler/PrintPure.ml5
-rw-r--r--compiler/RegionsHierarchy.ml13
-rw-r--r--compiler/Substitute.ml2
-rw-r--r--compiler/SymbolicToPure.ml68
8 files changed, 63 insertions, 73 deletions
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 15:49:43 +0000