Update following some changes in Charon

1 files changed, 15 insertions, 22 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 574602c7..a73bf0fd 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1808,7 +1808,6 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
     (trait_decl : trait_decl)
     (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
     extraction_ctx =
-  let generics = trait_decl.generics in
   (* Compute the clause names *)
   let clause_names =
     match builtin_info with
@@ -1822,11 +1821,11 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
               else ctx.fmt.trait_decl_name trait_decl ^ name
             in
             (c.clause_id, name))
-          generics.trait_clauses
+          trait_decl.parent_clauses
     | Some info ->
         List.map
           (fun (c, name) -> (c.clause_id, name))
-          (List.combine generics.trait_clauses info.parent_clauses)
+          (List.combine trait_decl.parent_clauses info.parent_clauses)
   in
   (* Register the names *)
   List.fold_left
@@ -2113,12 +2112,15 @@ let extract_trait_impl_item (ctx : extraction_ctx) (fmt : F.formatter)
   extract_trait_item ctx fmt item_name assign ty
 
 (** Small helper - TODO: move *)
-let generic_params_drop_prefix (g1 : generic_params) (g2 : generic_params) :
-    generic_params =
+let generic_params_drop_prefix ~(drop_trait_clauses : bool)
+    (g1 : generic_params) (g2 : generic_params) : generic_params =
   let open Collections.List in
   let types = drop (length g1.types) g2.types in
   let const_generics = drop (length g1.const_generics) g2.const_generics in
-  let trait_clauses = drop (length g1.trait_clauses) g2.trait_clauses in
+  let trait_clauses =
+    if drop_trait_clauses then drop (length g1.trait_clauses) g2.trait_clauses
+    else g2.trait_clauses
+  in
   { types; const_generics; trait_clauses }
 
 (** Small helper.
@@ -2139,7 +2141,9 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
       (* We need to add the generics specific to the method, by removing those
          which actually apply to the trait decl *)
       let generics =
-        generic_params_drop_prefix decl.generics f.signature.generics
+        let drop_trait_clauses = false in
+        generic_params_drop_prefix ~drop_trait_clauses decl.generics
+          f.signature.generics
       in
       let ctx, type_params, cg_params, trait_clauses =
         ctx_add_generic_params generics ctx
@@ -2189,8 +2193,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_print_space fmt ();
   F.pp_print_string fmt decl_name;
   (* Print the generics *)
-  (* We ignore the trait clauses, which we extract as *fields* *)
-  let generics = { decl.generics with trait_clauses = [] } in
+  let generics = decl.generics in
   (* Add the type and const generic params - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx, type_params, cg_params, trait_clauses =
@@ -2199,17 +2202,6 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   extract_generic_params ctx fmt TypeDeclId.Set.empty generics type_params
     cg_params trait_clauses;
 
-  (* Add the parent clauses as local clauses, so that we can refer to them *)
-  let ctx =
-    List.fold_left
-      (fun ctx clause ->
-        let item_name =
-          ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx
-        in
-        ctx_add (LocalTraitClauseId clause.clause_id) item_name ctx)
-      ctx decl.generics.trait_clauses
-  in
-
   F.pp_print_space fmt ();
   (match !backend with
   | Lean -> F.pp_print_string fmt "where"
@@ -2233,7 +2225,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
         extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause
       in
       extract_trait_decl_item ctx fmt item_name ty)
-    decl.generics.trait_clauses;
+    decl.parent_clauses;
 
   (* The constants *)
   List.iter
@@ -2330,7 +2322,8 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
          are specific to the method, and call it will all the generics
          (trait impl + method generics) *)
       let f_generics =
-        generic_params_drop_prefix
+        let drop_trait_clauses = true in
+        generic_params_drop_prefix ~drop_trait_clauses
           { impl.generics with types = impl_types }
           f_generics
       in