diff options
| -rw-r--r-- | compiler/AssociatedTypes.ml | 57 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 1 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 6 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 2 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/RegionsHierarchy.ml | 1 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 2 |
8 files changed, 35 insertions, 38 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index cce5a082..38615777 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -102,6 +102,7 @@ let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool = but they should be applied to types without regions. *) type norm_ctx = { + meta : Meta.meta option; norm_trait_types : ty TraitTypeRefMap.t; type_decls : type_decl TypeDeclId.Map.t; fun_decls : fun_decl FunDeclId.Map.t; @@ -238,8 +239,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = match trait_ref.trait_id with | TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ } -> - let meta = (TraitImplId.Map.find impl_id ctx.trait_impls).meta in - cassert (ref_generics = empty_generic_args) meta "Higher order types are not supported yet TODO: error message"; + cassert_opt_meta (ref_generics = empty_generic_args) ctx.meta "Higher order types are not supported yet TODO: error message"; log#ldebug (lazy ("norm_ctx_normalize_ty: trait type: trait ref: " @@ -279,8 +279,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = ^ trait_ref_to_string ctx trait_ref ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); (* We can't project *) - let meta = (TraitDeclId.Map.find trait_ref.trait_decl_ref.trait_decl_id ctx.trait_decls).meta in - cassert (trait_instance_id_is_local_clause trait_ref.trait_id) meta "TODO: error message"; + cassert_opt_meta (trait_instance_id_is_local_clause trait_ref.trait_id) ctx.meta "TODO: error message"; TTraitType (trait_ref, type_name) in let tr : trait_type_ref = { trait_ref; type_name } in @@ -345,11 +344,10 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) | ParentClause (inst_id, decl_id, clause_id) -> ( let inst_id, impl = norm_ctx_normalize_trait_instance_id ctx inst_id in (* Check if the inst_id refers to a specific implementation, if yes project *) - let meta = (TraitDeclId.Map.find decl_id ctx.trait_decls).meta in match impl with | None -> (* This is actually a local clause *) - cassert (trait_instance_id_is_local_clause inst_id) meta "TODO: error message"; + cassert_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta "TODO: error message"; (ParentClause (inst_id, decl_id, clause_id), None) | Some impl -> (* We figure out the parent clause by doing the following: @@ -375,13 +373,12 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) let clause = norm_ctx_normalize_trait_ref ctx clause in (TraitRef clause, Some clause)) | ItemClause (inst_id, decl_id, item_name, clause_id) -> ( - let meta = (TraitDeclId.Map.find decl_id ctx.trait_decls).meta in let inst_id, impl = norm_ctx_normalize_trait_instance_id ctx inst_id in (* Check if the inst_id refers to a specific implementation, if yes project *) match impl with | None -> (* This is actually a local clause *) - cassert (trait_instance_id_is_local_clause inst_id) meta "Trait instance id is not a local clause"; + cassert_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta "Trait instance id is not a local clause"; (ItemClause (inst_id, decl_id, item_name, clause_id), None) | Some impl -> (* We figure out the item clause by doing the following: @@ -421,9 +418,9 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) | TraitRef trait_ref -> (* The trait instance id necessarily refers to a local sub-clause. We can't project over it and can only peel off the [TraitRef] wrapper *) - let meta = (TraitDeclId.Map.find trait_ref.trait_decl_ref.trait_decl_id ctx.trait_decls).meta in - cassert (trait_instance_id_is_local_clause trait_ref.trait_id) meta "Trait instance id is not a local sub-clause"; - cassert (trait_ref.generics = empty_generic_args) meta "TODO: error message"; +(* let meta = (TraitDeclId.Map.find trait_ref.trait_decl_ref.trait_decl_id ctx.trait_decls).meta in *) + cassert_opt_meta (trait_instance_id_is_local_clause trait_ref.trait_id) ctx.meta "Trait instance id is not a local sub-clause"; + cassert_opt_meta (trait_ref.generics = empty_generic_args) ctx.meta "TODO: error message"; (trait_ref.trait_id, None) | FnPointer ty -> let ty = norm_ctx_normalize_ty ctx ty in @@ -472,8 +469,7 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) : (lazy ("norm_ctx_normalize_trait_ref: normalized to: " ^ trait_ref_to_string ctx trait_ref)); - let meta = (TraitDeclId.Map.find trait_ref.trait_decl_ref.trait_decl_id ctx.trait_decls).meta in - cassert (generics = empty_generic_args) meta "TODO: error message"; + cassert_opt_meta (generics = empty_generic_args) ctx.meta "TODO: error message"; trait_ref (* Not sure this one is really necessary *) @@ -490,8 +486,9 @@ let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx) let ty = norm_ctx_normalize_ty ctx ty in { trait_ref; type_name; ty } -let mk_norm_ctx (ctx : eval_ctx) : norm_ctx = +let mk_norm_ctx (meta : Meta.meta) (ctx : eval_ctx) : norm_ctx = { + meta = Some meta; norm_trait_types = ctx.norm_trait_types; type_decls = ctx.type_ctx.type_decls; fun_decls = ctx.fun_ctx.fun_decls; @@ -502,17 +499,17 @@ let mk_norm_ctx (ctx : eval_ctx) : norm_ctx = const_generic_vars = ctx.const_generic_vars; } -let ctx_normalize_ty (ctx : eval_ctx) (ty : ty) : ty = - norm_ctx_normalize_ty (mk_norm_ctx ctx) ty +let ctx_normalize_ty (meta : Meta.meta) (ctx : eval_ctx) (ty : ty) : ty = + norm_ctx_normalize_ty (mk_norm_ctx meta ctx) ty (** Normalize a type and erase the regions at the same time *) -let ctx_normalize_erase_ty (ctx : eval_ctx) (ty : ty) : ty = - let ty = ctx_normalize_ty ctx ty in +let ctx_normalize_erase_ty (meta : Meta.meta) (ctx : eval_ctx) (ty : ty) : ty = + let ty = ctx_normalize_ty meta ctx ty in Subst.erase_regions ty -let ctx_normalize_trait_type_constraint (ctx : eval_ctx) +let ctx_normalize_trait_type_constraint (meta : Meta.meta) (ctx : eval_ctx) (ttc : trait_type_constraint) : trait_type_constraint = - norm_ctx_normalize_trait_type_constraint (mk_norm_ctx ctx) ttc + norm_ctx_normalize_trait_type_constraint (mk_norm_ctx meta ctx) ttc (** Same as [type_decl_get_instantiated_variants_fields_types] but normalizes the types *) let type_decl_get_inst_norm_variants_fields_rtypes (ctx : eval_ctx) @@ -523,7 +520,7 @@ let type_decl_get_inst_norm_variants_fields_rtypes (ctx : eval_ctx) in List.map (fun (variant_id, types) -> - (variant_id, List.map (ctx_normalize_ty ctx) types)) + (variant_id, List.map (ctx_normalize_ty def.meta ctx) types)) res (** Same as [type_decl_get_instantiated_field_types] but normalizes the types *) @@ -532,7 +529,7 @@ let type_decl_get_inst_norm_field_rtypes (ctx : eval_ctx) (def : type_decl) let types = Subst.type_decl_get_instantiated_field_types def opt_variant_id generics in - List.map (ctx_normalize_ty ctx) types + List.map (ctx_normalize_ty def.meta ctx) types (** Same as [ctx_adt_value_get_instantiated_field_rtypes] but normalizes the types *) let ctx_adt_value_get_inst_norm_field_rtypes (meta : Meta.meta) (ctx : eval_ctx) (adt : adt_value) @@ -540,7 +537,7 @@ let ctx_adt_value_get_inst_norm_field_rtypes (meta : Meta.meta) (ctx : eval_ctx) let types = Subst.ctx_adt_value_get_instantiated_field_types meta ctx adt id generics in - List.map (ctx_normalize_ty ctx) types + List.map (ctx_normalize_ty meta ctx) types (** Same as [ctx_adt_value_get_instantiated_field_types] but normalizes the types and erases the regions. *) @@ -549,22 +546,22 @@ let type_decl_get_inst_norm_field_etypes (ctx : eval_ctx) (def : type_decl) let types = Subst.type_decl_get_instantiated_field_types def opt_variant_id generics in - let types = List.map (ctx_normalize_ty ctx) types in + let types = List.map (ctx_normalize_ty def.meta ctx) types in List.map Subst.erase_regions types (** Same as [ctx_adt_get_instantiated_field_types] but normalizes the types and erases the regions. *) -let ctx_adt_get_inst_norm_field_etypes (ctx : eval_ctx) (def_id : TypeDeclId.id) +let ctx_adt_get_inst_norm_field_etypes (meta : Meta.meta) (ctx : eval_ctx) (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option) (generics : generic_args) : ty list = let types = Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id generics in - let types = List.map (ctx_normalize_ty ctx) types in + let types = List.map (ctx_normalize_ty meta ctx) types in List.map Subst.erase_regions types (** Same as [substitute_signature] but normalizes the types *) -let ctx_subst_norm_signature (ctx : eval_ctx) +let ctx_subst_norm_signature (meta : Meta.meta) (ctx : eval_ctx) (asubst : RegionGroupId.id -> AbstractionId.id) (r_subst : RegionVarId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty) (cg_subst : ConstGenericVarId.id -> const_generic) @@ -576,9 +573,9 @@ let ctx_subst_norm_signature (ctx : eval_ctx) sg regions_hierarchy in let { regions_hierarchy; inputs; output; trait_type_constraints } = sg in - let inputs = List.map (ctx_normalize_ty ctx) inputs in - let output = ctx_normalize_ty ctx output in + let inputs = List.map (ctx_normalize_ty meta ctx) inputs in + let output = ctx_normalize_ty meta ctx output in let trait_type_constraints = - List.map (ctx_normalize_trait_type_constraint ctx) trait_type_constraints + List.map (ctx_normalize_trait_type_constraint meta ctx) trait_type_constraints in { regions_hierarchy; inputs; output; trait_type_constraints } diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 71717b57..6e799bd9 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -748,7 +748,6 @@ let ctx_get_local_trait_clause (meta : Meta.meta) (id : TraitClauseId.id) (ctx : let ctx_get_field (meta : Meta.meta) (type_id : type_id) (field_id : FieldId.id) (ctx : extraction_ctx) : string = - (* let meta = (TypeDeclId.Map.find type_id ctx.trans_types).meta in TODO : check how to get meta *) ctx_get ~meta:(Some meta) (FieldId (type_id, field_id)) ctx let ctx_get_struct (meta : Meta.meta) (def_id : type_id) (ctx : extraction_ctx) : string = diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 6e2c15d7..2ac772ae 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -49,11 +49,11 @@ let compute_contexts (m : crate) : decls_ctx = to compute a normalization map (for the associated types) and that we added it in the context. *) -let normalize_inst_fun_sig (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig = +let normalize_inst_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig = let { regions_hierarchy = _; trait_type_constraints = _; inputs; output } = sg in - let norm = AssociatedTypes.ctx_normalize_ty ctx in + let norm = AssociatedTypes.ctx_normalize_ty meta ctx in let inputs = List.map norm inputs in let output = norm output in { sg with inputs; output } @@ -157,7 +157,7 @@ let symbolic_instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (sg : fun_s inst_sg.trait_type_constraints in (* Normalize the signature *) - let inst_sg = normalize_inst_fun_sig ctx inst_sg in + let inst_sg = normalize_inst_fun_sig meta ctx inst_sg in (* Return *) (ctx, inst_sg) diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index d74e0751..6c4f8af5 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -741,7 +741,7 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind : List.length type_decl.generics.regions = List.length generics.regions) meta "TODO: error message"; let expected_field_types = - AssociatedTypes.ctx_adt_get_inst_norm_field_etypes ctx def_id + AssociatedTypes.ctx_adt_get_inst_norm_field_etypes meta ctx def_id opt_variant_id generics in cassert ( diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 253d90cc..0d0fd0a5 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -309,7 +309,7 @@ let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx) (fid : Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self sg.output in - AssociatedTypes.ctx_normalize_erase_ty ctx ty + AssociatedTypes.ctx_normalize_erase_ty meta ctx ty let move_return_value (config : config) (meta : Meta.meta) (pop_return_value : bool) (cf : typed_value option -> m_fun) : m_fun = diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 48869739..b5402bb0 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -514,7 +514,7 @@ let instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (generics : generic_ in (* Substitute the signature *) let inst_sig = - AssociatedTypes.ctx_subst_norm_signature ctx asubst rsubst tsubst cgsubst + AssociatedTypes.ctx_subst_norm_signature meta ctx asubst rsubst tsubst cgsubst tr_subst tr_self sg regions_hierarchy in (* Return *) diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 4ebdd01a..0672a25f 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -55,6 +55,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty sg.preds.trait_type_constraints in { + meta = meta; norm_trait_types; type_decls; fun_decls; diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 63605b9c..b62966bd 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -973,7 +973,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta) (* Normalize the signature *) let sg = let ({ A.inputs; output; _ } : A.fun_sig) = sg in - let norm = AssociatedTypes.ctx_normalize_ty ctx in + let norm = AssociatedTypes.ctx_normalize_ty meta ctx in let inputs = List.map norm inputs in let output = norm output in { sg with A.inputs; output } |