added a meta option field to norm_ctx and changed the meta used by some assert to the norm_ctx one

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 }