changes to extract_ty and related functions to use the right meta

4 files changed, 52 insertions, 60 deletions

diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 38615777..0ed46e8c 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -418,7 +418,6 @@ 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_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)
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 3d0fe75f..564ffafb 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -452,7 +452,7 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.for
             cassert (lp_id = None) trait_decl.meta "TODO: Error message";
             extract_trait_ref trait_decl.meta ctx fmt TypeDeclId.Set.empty true trait_ref;
             let fun_name =
-              ctx_get_trait_method trait_ref.trait_decl_ref.trait_decl_id
+              ctx_get_trait_method meta trait_ref.trait_decl_ref.trait_decl_id
                 method_name ctx
             in
             let add_brackets (s : string) =
@@ -2236,7 +2236,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
   let trans = A.FunDeclId.Map.find id ctx.trans_funs in
   (* Extract the items *)
   let f = trans.f in
-  let fun_name = ctx_get_trait_method decl.def_id item_name ctx in
+  let fun_name = ctx_get_trait_method decl.meta decl.def_id item_name ctx in
   let ty () =
     (* Extract the generics *)
     (* We need to add the generics specific to the method, by removing those
@@ -2252,7 +2252,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
        - we only generate trait clauses for the clauses we find in the
          pure generics *)
     let ctx, type_params, cg_params, trait_clauses =
-      ctx_add_generic_params f.meta f.llbc_name f.signature.llbc_generics generics ctx (* TODO: confirm it's the right meta*)
+      ctx_add_generic_params decl.meta f.llbc_name f.signature.llbc_generics generics ctx (* TODO: confirm it's the right meta*)
     in
     let backend_uses_forall =
       match !backend with Coq | Lean -> true | FStar | HOL4 -> false
@@ -2261,7 +2261,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
     let use_forall = generics_not_empty && backend_uses_forall in
     let use_arrows = generics_not_empty && not backend_uses_forall in
     let use_forall_use_sep = false in
-    extract_generic_params f.meta ctx fmt TypeDeclId.Set.empty ~use_forall
+    extract_generic_params decl.meta ctx fmt TypeDeclId.Set.empty ~use_forall
       ~use_forall_use_sep ~use_arrows generics type_params cg_params
       trait_clauses; (* TODO: confirm it's the right meta*)
     if use_forall then F.pp_print_string fmt ",";
@@ -2275,7 +2275,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
 let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (decl : trait_decl) : unit =
   (* Retrieve the trait name *)
-  let decl_name = ctx_get_trait_decl decl.def_id ctx in
+  let decl_name = ctx_get_trait_decl decl.meta decl.def_id ctx in
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
@@ -2331,7 +2331,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_close_box fmt ())
   else if is_empty && !backend = Coq then (
     (* Coq is not very good at infering constructors *)
-    let cons = ctx_get_trait_constructor decl.def_id ctx in
+    let cons = ctx_get_trait_constructor decl.meta decl.def_id ctx in
     F.pp_print_string fmt (":= " ^ cons ^ "{}.");
     (* Outer box *)
     F.pp_close_box fmt ())
@@ -2340,7 +2340,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     | Lean -> F.pp_print_string fmt "where"
     | FStar -> F.pp_print_string fmt "= {"
     | Coq ->
-        let cons = ctx_get_trait_constructor decl.def_id ctx in
+        let cons = ctx_get_trait_constructor decl.meta decl.def_id ctx in
         F.pp_print_string fmt (":= " ^ cons ^ " {")
     | _ -> F.pp_print_string fmt "{");
 
@@ -2354,7 +2354,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (* The constants *)
     List.iter
       (fun (name, (ty, _)) ->
-        let item_name = ctx_get_trait_const decl.def_id name ctx in
+        let item_name = ctx_get_trait_const decl.meta decl.def_id name ctx in
         let ty () =
           let inside = false in
           F.pp_print_space fmt ();
@@ -2367,7 +2367,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     List.iter
       (fun (name, (clauses, _)) ->
         (* Extract the type *)
-        let item_name = ctx_get_trait_type decl.def_id name ctx in
+        let item_name = ctx_get_trait_type decl.meta decl.def_id name ctx in
         let ty () =
           F.pp_print_space fmt ();
           F.pp_print_string fmt (type_keyword decl.meta)
@@ -2377,11 +2377,11 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
         List.iter
           (fun clause ->
             let item_name =
-              ctx_get_trait_item_clause decl.def_id name clause.clause_id ctx
+              ctx_get_trait_item_clause decl.meta decl.def_id name clause.clause_id ctx
             in
             let ty () =
               F.pp_print_space fmt ();
-              extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause
+              extract_trait_clause_type decl.meta ctx fmt TypeDeclId.Set.empty clause
             in
             extract_trait_decl_item ctx fmt item_name ty)
           clauses)
@@ -2392,11 +2392,11 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     List.iter
       (fun clause ->
         let item_name =
-          ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx
+          ctx_get_trait_parent_clause decl.meta decl.def_id clause.clause_id ctx
         in
         let ty () =
           F.pp_print_space fmt ();
-          extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause
+          extract_trait_clause_type decl.meta ctx fmt TypeDeclId.Set.empty clause
         in
         extract_trait_decl_item ctx fmt item_name ty)
       decl.parent_clauses;
@@ -2433,25 +2433,25 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
   in
   if num_params > 0 then (
     (* The constructor *)
-    let cons_name = ctx_get_trait_constructor decl.def_id ctx in
+    let cons_name = ctx_get_trait_constructor decl.meta decl.def_id ctx in
     extract_coq_arguments_instruction ctx fmt cons_name num_params;
     (* The constants *)
     List.iter
       (fun (name, _) ->
-        let item_name = ctx_get_trait_const decl.def_id name ctx in
+        let item_name = ctx_get_trait_const decl.meta decl.def_id name ctx in
         extract_coq_arguments_instruction ctx fmt item_name num_params)
       decl.consts;
     (* The types *)
     List.iter
       (fun (name, (clauses, _)) ->
         (* The type *)
-        let item_name = ctx_get_trait_type decl.def_id name ctx in
+        let item_name = ctx_get_trait_type decl.meta decl.def_id name ctx in
         extract_coq_arguments_instruction ctx fmt item_name num_params;
         (* The type clauses *)
         List.iter
           (fun clause ->
             let item_name =
-              ctx_get_trait_item_clause decl.def_id name clause.clause_id ctx
+              ctx_get_trait_item_clause decl.meta decl.def_id name clause.clause_id ctx
             in
             extract_coq_arguments_instruction ctx fmt item_name num_params)
           clauses)
@@ -2460,7 +2460,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
     List.iter
       (fun clause ->
         let item_name =
-          ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx
+          ctx_get_trait_parent_clause decl.meta decl.def_id clause.clause_id ctx
         in
         extract_coq_arguments_instruction ctx fmt item_name num_params)
       decl.parent_clauses;
@@ -2468,7 +2468,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
     List.iter
       (fun (item_name, _) ->
         (* Extract the items *)
-        let item_name = ctx_get_trait_method decl.def_id item_name ctx in
+        let item_name = ctx_get_trait_method decl.meta decl.def_id item_name ctx in
         extract_coq_arguments_instruction ctx fmt item_name num_params)
       decl.required_methods;
     (* Add a space *)
@@ -2493,7 +2493,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
   let trans = A.FunDeclId.Map.find id ctx.trans_funs in
   (* Extract the items *)
   let f = trans.f in
-  let fun_name = ctx_get_trait_method trait_decl_id item_name ctx in
+  let fun_name = ctx_get_trait_method impl.meta trait_decl_id item_name ctx in
   let ty () =
     (* Filter the generics if the method is a builtin *)
     let i_tys, _, _ = impl_generics in
@@ -2533,16 +2533,16 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
        - we only generate trait clauses for the clauses we find in the
          pure generics *)
     let ctx, f_tys, f_cgs, f_tcs =
-      ctx_add_generic_params f.meta f.llbc_name f.signature.llbc_generics f_generics
+      ctx_add_generic_params impl.meta f.llbc_name f.signature.llbc_generics f_generics
         ctx
     in
     let use_forall = f_generics <> empty_generic_params in
-    extract_generic_params f.meta ctx fmt TypeDeclId.Set.empty ~use_forall f_generics
+    extract_generic_params impl.meta ctx fmt TypeDeclId.Set.empty ~use_forall f_generics
       f_tys f_cgs f_tcs;
     if use_forall then F.pp_print_string fmt ",";
     (* Extract the function call *)
     F.pp_print_space fmt ();
-    let fun_name = ctx_get_local_function f.meta f.def_id None ctx in
+    let fun_name = ctx_get_local_function impl.meta f.def_id None ctx in
     F.pp_print_string fmt fun_name;
     let all_generics =
       let _, i_cgs, i_tcs = impl_generics in
@@ -2565,7 +2565,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     (impl : trait_impl) : unit =
   log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name));
   (* Retrieve the impl name *)
-  let impl_name = ctx_get_trait_impl impl.def_id ctx in
+  let impl_name = ctx_get_trait_impl impl.meta impl.def_id ctx in
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
@@ -2629,7 +2629,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_close_box fmt ())
   else if is_empty && !Config.backend = Coq then (
     (* Coq is not very good at infering constructors *)
-    let cons = ctx_get_trait_constructor impl.impl_trait.trait_decl_id ctx in
+    let cons = ctx_get_trait_constructor impl.meta impl.impl_trait.trait_decl_id ctx in
     F.pp_print_string fmt (":= " ^ cons ^ ".");
     (* Outer box *)
     F.pp_close_box fmt ())
@@ -2653,7 +2653,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     (* The constants *)
     List.iter
       (fun (provided_id, (name, (_, id))) ->
-        let item_name = ctx_get_trait_const trait_decl_id name ctx in
+        let item_name = ctx_get_trait_const impl.meta trait_decl_id name ctx in
         (* The parameters are not the same depending on whether the constant
            is a provided constant or not *)
         let print_params () =
@@ -2683,7 +2683,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     List.iter
       (fun (name, (trait_refs, ty)) ->
         (* Extract the type *)
-        let item_name = ctx_get_trait_type trait_decl_id name ctx in
+        let item_name = ctx_get_trait_type impl.meta trait_decl_id name ctx in
         let ty () =
           F.pp_print_space fmt ();
           extract_ty impl.meta ctx fmt TypeDeclId.Set.empty false ty
@@ -2693,7 +2693,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
         TraitClauseId.iteri
           (fun clause_id trait_ref ->
             let item_name =
-              ctx_get_trait_item_clause trait_decl_id name clause_id ctx
+              ctx_get_trait_item_clause impl.meta trait_decl_id name clause_id ctx
             in
             let ty () =
               F.pp_print_space fmt ();
@@ -2707,7 +2707,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
     TraitClauseId.iteri
       (fun clause_id trait_ref ->
         let item_name =
-          ctx_get_trait_parent_clause trait_decl_id clause_id ctx
+          ctx_get_trait_parent_clause impl.meta trait_decl_id clause_id ctx
         in
         let ty () =
           F.pp_print_space fmt ();
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 6e799bd9..c2e3e35f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -688,48 +688,41 @@ let ctx_get_local_type (meta : Meta.meta) (id : TypeDeclId.id) (ctx : extraction
 let ctx_get_assumed_type ?(meta = None) (id : assumed_ty) (ctx : extraction_ctx) : string =
   ctx_get_type ~meta:meta (TAssumed id) ctx
 
-let ctx_get_trait_constructor (id : trait_decl_id) (ctx : extraction_ctx) :
+let ctx_get_trait_constructor (meta : Meta.meta) (id : trait_decl_id) (ctx : extraction_ctx) :
     string =
-  let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
   ctx_get ~meta:(Some meta) (TraitDeclConstructorId id) ctx
 
 let ctx_get_trait_self_clause (meta : Meta.meta) (ctx : extraction_ctx) : string =
   ctx_get ~meta:(Some meta) TraitSelfClauseId ctx
 
-let ctx_get_trait_decl (id : trait_decl_id) (ctx : extraction_ctx) : string =
-  let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
+let ctx_get_trait_decl (meta : Meta.meta) (id : trait_decl_id) (ctx : extraction_ctx) : string =
   ctx_get ~meta:(Some meta) (TraitDeclId id) ctx
 
-let ctx_get_trait_impl (id : trait_impl_id) (ctx : extraction_ctx) : string =
-  let meta = (TraitImplId.Map.find id ctx.trans_trait_impls).meta in
+let ctx_get_trait_impl (meta : Meta.meta) (id : trait_impl_id) (ctx : extraction_ctx) : string =
   ctx_get ~meta:(Some meta) (TraitImplId id) ctx
 
-let ctx_get_trait_item (id : trait_decl_id) (item_name : string)
+let ctx_get_trait_item (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
     (ctx : extraction_ctx) : string =
-    let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
     ctx_get ~meta:(Some meta) (TraitItemId (id, item_name)) ctx
 
-let ctx_get_trait_const (id : trait_decl_id) (item_name : string)
+let ctx_get_trait_const (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
     (ctx : extraction_ctx) : string =
-  ctx_get_trait_item id item_name ctx
+  ctx_get_trait_item meta id item_name ctx
 
-let ctx_get_trait_type (id : trait_decl_id) (item_name : string)
+let ctx_get_trait_type (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
     (ctx : extraction_ctx) : string =
-  ctx_get_trait_item id item_name ctx
+  ctx_get_trait_item meta id item_name ctx
 
-let ctx_get_trait_method (id : trait_decl_id) (item_name : string)
+let ctx_get_trait_method (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
     (ctx : extraction_ctx) : string =
-    let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
   ctx_get ~meta:(Some meta) (TraitMethodId (id, item_name)) ctx
 
-let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id)
+let ctx_get_trait_parent_clause (meta : Meta.meta) (id : trait_decl_id) (clause : trait_clause_id)
     (ctx : extraction_ctx) : string =
-    let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
   ctx_get ~meta:(Some meta) (TraitParentClauseId (id, clause)) ctx
 
-let ctx_get_trait_item_clause (id : trait_decl_id) (item : string)
+let ctx_get_trait_item_clause (meta : Meta.meta) (id : trait_decl_id) (item : string)
     (clause : trait_clause_id) (ctx : extraction_ctx) : string =
-    let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
   ctx_get ~meta:(Some meta) (TraitItemClauseId (id, item, clause)) ctx
 
 let ctx_get_var (meta : Meta.meta) (id : VarId.id) (ctx : extraction_ctx) : string =
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 0329d968..b26704ce 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -533,7 +533,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
       if !parameterize_trait_types then craise meta "Unimplemented"
       else
         let type_name =
-          ctx_get_trait_type trait_ref.trait_decl_ref.trait_decl_id type_name
+          ctx_get_trait_type meta trait_ref.trait_decl_ref.trait_decl_id type_name
             ctx
         in
         let add_brackets (s : string) =
@@ -548,7 +548,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
         *)
         match trait_ref.trait_id with
         | Self ->
-            assert (trait_ref.generics = empty_generic_args);
+            cassert (trait_ref.generics = empty_generic_args) "TODO: Error message";
             extract_trait_instance_id_with_dot meta ctx fmt no_params_tys false
               trait_ref.trait_id;
             F.pp_print_string fmt type_name
@@ -587,7 +587,7 @@ and extract_trait_decl_ref (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.fo
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_decl_ref) :
     unit =
   let use_brackets = tr.decl_generics <> empty_generic_args && inside in
-  let name = ctx_get_trait_decl tr.trait_decl_id ctx in
+  let name = ctx_get_trait_decl meta tr.trait_decl_id ctx in
   if use_brackets then F.pp_print_string fmt "(";
   F.pp_print_string fmt name;
   (* There is something subtle here: the trait obligations for the implemented
@@ -665,19 +665,19 @@ and extract_trait_instance_id (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F
         craise meta "Unexpected occurrence of `Self`"
       else F.pp_print_string fmt "ERROR(\"Unexpected Self\")"
   | TraitImpl id ->
-      let name = ctx_get_trait_impl id ctx in
+      let name = ctx_get_trait_impl meta id ctx in
       F.pp_print_string fmt name
   | Clause id ->
       let name = ctx_get_local_trait_clause meta id ctx in
       F.pp_print_string fmt name
   | ParentClause (inst_id, decl_id, clause_id) ->
       (* Use the trait decl id to lookup the name *)
-      let name = ctx_get_trait_parent_clause decl_id clause_id ctx in
+      let name = ctx_get_trait_parent_clause meta decl_id clause_id ctx in
       extract_trait_instance_id_with_dot meta ctx fmt no_params_tys true inst_id;
       F.pp_print_string fmt (add_brackets name)
   | ItemClause (inst_id, decl_id, item_name, clause_id) ->
       (* Use the trait decl id to lookup the name *)
-      let name = ctx_get_trait_item_clause decl_id item_name clause_id ctx in
+      let name = ctx_get_trait_item_clause meta decl_id item_name clause_id ctx in
       extract_trait_instance_id_with_dot meta ctx fmt no_params_tys true inst_id;
       F.pp_print_string fmt (add_brackets name)
   | TraitRef trait_ref ->
@@ -1130,12 +1130,12 @@ let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
   in
   extract_comment fmt (sl @ [ span ] @ name)
 
-let extract_trait_clause_type (* (meta : Meta.meta) TODO check if right meta*) (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_trait_clause_type (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
-  let trait_name = ctx_get_trait_decl clause.trait_id ctx in
+  let trait_name = ctx_get_trait_decl meta clause.trait_id ctx in
   F.pp_print_string fmt trait_name;
-  let meta = (TraitDeclId.Map.find clause.trait_id ctx.trans_trait_decls).meta in
-  extract_generic_args meta ctx fmt no_params_tys clause.generics
+  (* let meta = (TraitDeclId.Map.find clause.trait_id ctx.trans_trait_decls).meta in
+   *)extract_generic_args meta ctx fmt no_params_tys clause.generics
 
 (** Insert a space, if necessary *)
 let insert_req_space (fmt : F.formatter) (space : bool ref) : unit =
@@ -1155,7 +1155,7 @@ let extract_trait_self_clause (insert_req_space : unit -> unit)
   F.pp_print_space fmt ();
   F.pp_print_string fmt ":";
   F.pp_print_space fmt ();
-  let trait_id = ctx_get_trait_decl trait_decl.def_id ctx in
+  let trait_id = ctx_get_trait_decl trait_decl.meta trait_decl.def_id ctx in
   F.pp_print_string fmt trait_id;
   List.iter
     (fun p ->
@@ -1258,7 +1258,7 @@ let extract_generic_params (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.fo
           F.pp_print_space fmt ();
           F.pp_print_string fmt ":";
           F.pp_print_space fmt ();
-          extract_trait_clause_type ctx fmt no_params_tys clause;
+          extract_trait_clause_type meta ctx fmt no_params_tys clause;
           (* ) *)
           right_bracket as_implicits;
           if use_arrows then (