Update following some changes in Charon

4 files changed, 59 insertions, 57 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
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 688ed352..56290ab4 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1239,42 +1239,45 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
       F.pp_print_space fmt ();
       extract_rec false ret_ty;
       if inside then F.pp_print_string fmt ")"
-  | TraitType (trait_ref, generics, type_name) ->
+  | TraitType (trait_ref, generics, type_name) -> (
       if !parameterize_trait_types then raise (Failure "Unimplemented")
-      else if trait_ref.trait_id <> Self then (
-        (* HOL4 doesn't have 1st class types *)
-        assert (!backend <> HOL4);
-        let use_brackets = generics <> empty_generic_args in
-        if use_brackets then F.pp_print_string fmt "(";
-        extract_trait_ref ctx fmt no_params_tys false trait_ref;
-        extract_generic_args ctx fmt no_params_tys generics;
-        let name =
-          ctx_get_trait_type trait_ref.trait_decl_ref.trait_decl_id type_name
-            ctx
-        in
-        if use_brackets then F.pp_print_string fmt ")";
-        F.pp_print_string fmt ("." ^ name))
       else
-        (* There are two situations:
-           - we are extracting a declared item (typically a function signature)
-             for a trait declaration. We directly refer to the item (we extract
-             trait declarations as structures, so we can refer to their fields)
-           - we are extracting a provided method for a trait declaration. We
-             refer to the item in the self trait clause (see {!SelfTraitClauseId}).
-
-           Remark: we can't get there for trait *implementations* because then the
-           types should have been normalized.
-        *)
-        let trait_decl_id = Option.get ctx.trait_decl_id in
-        let item_name = ctx_get_trait_type trait_decl_id type_name ctx in
-        assert (generics = empty_generic_args);
-        if ctx.is_provided_method then
-          (* Provided method: use the trait self clause *)
-          let self_clause = ctx_get_trait_self_clause ctx in
-          F.pp_print_string fmt (self_clause ^ "." ^ item_name)
-        else
-          (* Declaration: directly refer to the item *)
-          F.pp_print_string fmt item_name
+        (* There may be a special treatment depending on the instance id *)
+        match trait_ref.trait_id with
+        | Self ->
+            (* There are two situations:
+               - we are extracting a declared item (typically a function signature)
+                 for a trait declaration. We directly refer to the item (we extract
+                 trait declarations as structures, so we can refer to their fields)
+               - we are extracting a provided method for a trait declaration. We
+                 refer to the item in the self trait clause (see {!SelfTraitClauseId}).
+
+               Remark: we can't get there for trait *implementations* because then the
+               types should have been normalized.
+            *)
+            let trait_decl_id = Option.get ctx.trait_decl_id in
+            let item_name = ctx_get_trait_type trait_decl_id type_name ctx in
+            assert (generics = empty_generic_args);
+            if ctx.is_provided_method then
+              (* Provided method: use the trait self clause *)
+              let self_clause = ctx_get_trait_self_clause ctx in
+              F.pp_print_string fmt (self_clause ^ "." ^ item_name)
+            else
+              (* Declaration: directly refer to the item *)
+              F.pp_print_string fmt item_name
+        | _ ->
+            (* HOL4 doesn't have 1st class types *)
+            assert (!backend <> HOL4);
+            let use_brackets = generics <> empty_generic_args in
+            if use_brackets then F.pp_print_string fmt "(";
+            extract_trait_ref ctx fmt no_params_tys false trait_ref;
+            extract_generic_args ctx fmt no_params_tys generics;
+            let name =
+              ctx_get_trait_type trait_ref.trait_decl_ref.trait_decl_id
+                type_name ctx
+            in
+            if use_brackets then F.pp_print_string fmt ")";
+            F.pp_print_string fmt ("." ^ name))
 
 and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_ref) : unit =
@@ -1342,7 +1345,9 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
   | Self ->
       (* This has specific treatment depending on the item we're extracting
          (associated type, etc.). We should have caught this elsewhere. *)
-      raise (Failure "Unexpected")
+      if !Config.extract_fail_hard then
+        raise (Failure "Unexpected occurrence of `Self`")
+      else F.pp_print_string fmt "ERROR(\"Unexpected Self\")"
   | TraitImpl id ->
       let name = ctx_get_trait_impl id ctx in
       F.pp_print_string fmt name
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 70653e57..c33a745c 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1013,6 +1013,7 @@ type trait_decl = {
   name : name;
   generics : generic_params;
   preds : predicates;
+  parent_clauses : trait_clause list;
   consts : (trait_item_name * (ty * global_decl_id option)) list;
   types : (trait_item_name * (trait_clause list * ty option)) list;
   required_methods : (trait_item_name * fun_decl_id) list;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index c629a96f..46aa3b83 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3096,6 +3096,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
     name;
     generics;
     preds;
+    parent_clauses;
     consts;
     types;
     required_methods;
@@ -3105,6 +3106,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
   in
   let generics = translate_generic_params generics in
   let preds = translate_predicates preds in
+  let parent_clauses = List.map translate_trait_clause parent_clauses in
   let consts =
     List.map
       (fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
@@ -3123,6 +3125,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
     name;
     generics;
     preds;
+    parent_clauses;
     consts;
     types;
     required_methods;