Lift clauses on associated types to be clauses on the whole trait

charon-ml/src/GAst.ml

@@ -159,7 +159,7 @@ type trait_decl = {
   generics : generic_params;
   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;
+  types : (trait_item_name * ty option) list;
   required_methods : (trait_item_name * fun_decl_id) list;
   provided_methods : (trait_item_name * fun_decl_id option) list;
 }
@@ -172,7 +172,7 @@ type trait_impl = {
   generics : generic_params;
   parent_trait_refs : trait_ref list;
   consts : (trait_item_name * (ty * global_decl_id)) list;
-  types : (trait_item_name * (trait_ref list * ty)) list;
+  types : (trait_item_name * ty) list;
   required_methods : (trait_item_name * fun_decl_id) list;
   provided_methods : (trait_item_name * fun_decl_id) list;
 }

charon-ml/src/GAstOfJson.ml

@@ -459,12 +459,6 @@ and trait_instance_id_of_json (js : json) : (trait_instance_id, string) result =
         let* x1 = trait_decl_id_of_json x1 in
         let* x2 = trait_clause_id_of_json x2 in
         Ok (ParentClause (x0, x1, x2))
-    | `Assoc [ ("ItemClause", `List [ x0; x1; x2; x3 ]) ] ->
-        let* x0 = trait_instance_id_of_json x0 in
-        let* x1 = trait_decl_id_of_json x1 in
-        let* x2 = trait_item_name_of_json x2 in
-        let* x3 = trait_clause_id_of_json x3 in
-        Ok (ItemClause (x0, x1, x2, x3))
     | `String "SelfId" -> Ok Self
     | `Assoc [ ("BuiltinOrAuto", builtin_or_auto) ] ->
         let* builtin_or_auto = trait_decl_ref_of_json builtin_or_auto in
@@ -1241,6 +1235,7 @@ let gglobal_decl_of_json (bodies : 'body gexpr_body option list)
         Ok global
     | _ -> Error "")
 
+(* Defined by hand because we discard the empty list of item clauses *)
 and trait_decl_of_json (id_to_file : id_to_file_map) (js : json) :
     (trait_decl, string) result =
   combine_error_msgs js __FUNCTION__
@@ -1279,6 +1274,7 @@ and trait_decl_of_json (id_to_file : id_to_file_map) (js : json) :
                   (option_of_json ty_of_json)))
             types
         in
+        let types = List.map (fun (name, (_, ty)) -> (name, ty)) types in
         let* required_methods =
           list_of_json
             (pair_of_json trait_item_name_of_json fun_decl_id_of_json)
@@ -1303,6 +1299,7 @@ and trait_decl_of_json (id_to_file : id_to_file_map) (js : json) :
           }
     | _ -> Error "")
 
+(* Defined by hand because we discard the empty list of item clauses *)
 and trait_impl_of_json (id_to_file : id_to_file_map) (js : json) :
     (trait_impl, string) result =
   combine_error_msgs js __FUNCTION__
@@ -1339,6 +1336,7 @@ and trait_impl_of_json (id_to_file : id_to_file_map) (js : json) :
                (pair_of_json (list_of_json trait_ref_of_json) ty_of_json))
             types
         in
+        let types = List.map (fun (name, (_, ty)) -> (name, ty)) types in
         let* required_methods =
           list_of_json
             (pair_of_json trait_item_name_of_json fun_decl_id_of_json)

charon-ml/src/PrintGAst.ml

@@ -176,14 +176,10 @@ let trait_decl_to_string (env : ('a, 'b) fmt_env) (indent : string)
     in
     let types =
       List.map
-        (fun (name, (clauses, opt_ty)) ->
-          let clauses = List.map (trait_clause_to_string env) clauses in
-          let clauses = clauses_to_string indent1 indent_incr 0 clauses in
+        (fun (name, opt_ty) ->
           match opt_ty with
-          | None -> indent1 ^ "type " ^ name ^ clauses ^ "\n"
-          | Some ty ->
-              indent1 ^ "type " ^ name ^ " = " ^ ty_to_string ty ^ clauses
-              ^ "\n")
+          | None -> indent1 ^ "type " ^ name ^ "\n"
+          | Some ty -> indent1 ^ "type " ^ name ^ " = " ^ ty_to_string ty ^ "\n")
         def.types
     in
     let required_methods =
@@ -261,16 +257,8 @@ let trait_impl_to_string (env : ('a, 'b) fmt_env) (indent : string)
     in
     let types =
       List.map
-        (fun (name, (trait_refs, ty)) ->
-          let trait_refs =
-            if trait_refs <> [] then
-              " where ["
-              ^ String.concat ", "
-                  (List.map (trait_ref_to_string env) trait_refs)
-              ^ "]"
-            else ""
-          in
-          indent1 ^ "type " ^ name ^ " = " ^ ty_to_string ty ^ trait_refs ^ "\n")
+        (fun (name, ty) ->
+          indent1 ^ "type " ^ name ^ " = " ^ ty_to_string ty ^ "\n")
         def.types
     in
     let env_method (name, f) =

charon-ml/src/PrintTypes.ml

@@ -230,10 +230,6 @@ and trait_instance_id_to_string (env : ('a, 'b) fmt_env)
       let inst_id = trait_instance_id_to_string env inst_id in
       let clause_id = trait_clause_id_to_string env clause_id in
       "parent(" ^ inst_id ^ ")::" ^ clause_id
-  | ItemClause (inst_id, _decl_id, item_name, clause_id) ->
-      let inst_id = trait_instance_id_to_string env inst_id in
-      let clause_id = trait_clause_id_to_string env clause_id in
-      "(" ^ inst_id ^ ")::" ^ item_name ^ "::[" ^ clause_id ^ "]"
   | FnPointer ty -> "fn_ptr(" ^ ty_to_string env ty ^ ")"
   | Closure (fid, generics) ->
       "closure("

charon-ml/src/Types.ml

@@ -318,8 +318,6 @@ and trait_instance_id =
   | BuiltinOrAuto of trait_decl_ref
   | Clause of trait_clause_id
   | ParentClause of trait_instance_id * trait_decl_id * trait_clause_id
-  | ItemClause of
-      trait_instance_id * trait_decl_id * trait_item_name * trait_clause_id
   | FnPointer of ty
   | Closure of fun_decl_id * generic_args
   | Dyn of trait_decl_ref

charon/src/ast/gast.rs

@@ -238,7 +238,10 @@ pub struct TraitDecl {
     ///
     /// The optional id is for the default value.
     pub consts: Vec<(TraitItemName, (Ty, Option<GlobalDeclId>))>,
-    /// The associated types declared in the trait.
+    /// The associated types declared in the trait. The `Vector` is a list of trait clauses that
+    /// apply to this item. This is used during translation, but the `lift_associated_item_clauses`
+    /// pass moves them to be parent clauses later. Hence this is empty after that pass.
+    /// TODO: Do this as we translate to avoid the need to store this vector.
     pub types: Vec<(
         TraitItemName,
         (Vector<TraitClauseId, TraitClause>, Option<Ty>),
@@ -287,7 +290,9 @@ pub struct TraitImpl {
     pub parent_trait_refs: Vector<TraitClauseId, TraitRef>,
     /// The associated constants declared in the trait.
     pub consts: Vec<(TraitItemName, (Ty, GlobalDeclId))>,
-    /// The associated types declared in the trait.
+    /// The associated types declared in the trait. The `Vec` corresponds to the same `Vector` in
+    /// `TraitDecl.types`. In the same way, this is empty after the `lift_associated_item_clauses`
+    /// pass.
     pub types: Vec<(TraitItemName, (Vec<TraitRef>, Ty))>,
     /// The implemented required methods
     pub required_methods: Vec<(TraitItemName, FunDeclId)>,

charon/src/ast/krate.rs

@@ -78,22 +78,29 @@ pub enum AnyTransItem<'ctx> {
 }
 
 /// The data of a translated crate.
-#[derive(Default)]
+#[derive(Default, Drive, DriveMut)]
 pub struct TranslatedCrate {
     /// The name of the crate.
     pub crate_name: String,
 
     /// File names to ids and vice-versa
+    #[drive(skip)]
     pub file_to_id: HashMap<FileName, FileId>,
+    #[drive(skip)]
     pub id_to_file: HashMap<FileId, FileName>,
+    #[drive(skip)]
     pub real_file_counter: Generator<LocalFileId>,
+    #[drive(skip)]
     pub virtual_file_counter: Generator<VirtualFileId>,
 
     /// All the ids, in the order in which we encountered them
+    #[drive(skip)]
     pub all_ids: LinkedHashSet<AnyTransId>,
     /// The map from rustc id to translated id.
+    #[drive(skip)]
     pub id_map: HashMap<DefId, AnyTransId>,
     /// The reverse map of ids.
+    #[drive(skip)]
     pub reverse_id_map: HashMap<AnyTransId, DefId>,
 
     /// The translated type definitions
@@ -109,6 +116,7 @@ pub struct TranslatedCrate {
     /// The translated trait declarations
     pub trait_impls: Vector<TraitImplId, TraitImpl>,
     /// The re-ordered groups of declarations, initialized as empty.
+    #[drive(skip)]
     pub ordered_decls: Option<DeclarationsGroups>,
 }
 
@@ -126,7 +134,6 @@ impl TranslatedCrate {
     pub fn all_items(&self) -> impl Iterator<Item = AnyTransItem<'_>> {
         self.all_items_with_ids().map(|(_, item)| item)
     }
-
     pub fn all_items_with_ids(&self) -> impl Iterator<Item = (AnyTransId, AnyTransItem<'_>)> {
         self.all_ids
             .iter()

charon/src/ast/types.rs

@@ -177,8 +177,8 @@ pub enum TraitRefKind {
     /// ```
     ParentClause(Box<TraitRefKind>, TraitDeclId, TraitClauseId),
 
-    /// A clause bound in a trait item (typically a trait clause in an
-    /// associated type).
+    /// A clause defined on an associated type. This variant is only used during translation; after
+    /// the `lift_associated_item_clauses` pass, clauses on items become `ParentClause`s.
     ///
     /// Remark: the [TraitDeclId] gives the trait declaration which is
     /// implemented by the trait implementation from which we take the item
@@ -202,8 +202,7 @@ pub enum TraitRefKind {
     ///                local clause 0 implements Foo
     /// }
     /// ```
-    ///
-    ///
+    #[charon::opaque]
     ItemClause(Box<TraitRefKind>, TraitDeclId, TraitItemName, TraitClauseId),
 
     /// Self, in case of trait declarations/implementations.

charon/src/ast/types_utils.rs

@@ -103,6 +103,7 @@ impl GenericArgs {
     }
 
     /// Check whether this matches the given `GenericParams`.
+    /// TODO: check more things, e.g. that the trait refs use the correct trait and generics.
     pub fn matches(&self, params: &GenericParams) -> bool {
         params.regions.len() == self.regions.len()
             && params.types.len() == self.types.len()

charon/src/bin/charon-driver/driver.rs

@@ -251,6 +251,7 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa
 
     // Run the micro-passes that clean up bodies.
     for pass in ULLBC_PASSES.iter() {
+        trace!("# Starting pass {}", pass.name());
         pass.transform_ctx(&mut ctx)
     }
 
@@ -269,6 +270,7 @@ pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> export::CrateDa
 
         // Run the micro-passes that clean up bodies.
         for pass in LLBC_PASSES.iter() {
+            trace!("# Starting pass {}", pass.name());
             pass.transform_ctx(&mut ctx)
         }
 

charon/src/bin/generate-ml/GAstOfJson.template.ml

@@ -261,6 +261,132 @@ let gglobal_decl_of_json (bodies : 'body gexpr_body option list)
         Ok global
     | _ -> Error "")
 
+(* Defined by hand because we discard the empty list of item clauses *)
+and trait_decl_of_json (id_to_file : id_to_file_map) (js : json) :
+    (trait_decl, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc
+        [
+          ("def_id", def_id);
+          ("item_meta", item_meta);
+          ("generics", generics);
+          ("parent_clauses", parent_clauses);
+          ("consts", consts);
+          ("types", types);
+          ("required_methods", required_methods);
+          ("provided_methods", provided_methods);
+        ] ->
+        let* def_id = trait_decl_id_of_json def_id in
+        let* item_meta = item_meta_of_json id_to_file item_meta in
+        let* generics = generic_params_of_json id_to_file generics in
+        let* parent_clauses =
+          vector_of_json trait_clause_id_of_json
+            (trait_clause_of_json id_to_file)
+            parent_clauses
+        in
+        let* consts =
+          list_of_json
+            (pair_of_json trait_item_name_of_json
+               (pair_of_json ty_of_json (option_of_json global_decl_id_of_json)))
+            consts
+        in
+        let* types =
+          list_of_json
+            (pair_of_json trait_item_name_of_json
+               (pair_of_json
+                  (vector_of_json trait_clause_id_of_json
+                     (trait_clause_of_json id_to_file))
+                  (option_of_json ty_of_json)))
+            types
+        in
+        let types = List.map (fun (name, (_, ty)) -> (name, ty)) types in
+        let* required_methods =
+          list_of_json
+            (pair_of_json trait_item_name_of_json fun_decl_id_of_json)
+            required_methods
+        in
+        let* provided_methods =
+          list_of_json
+            (pair_of_json trait_item_name_of_json
+               (option_of_json fun_decl_id_of_json))
+            provided_methods
+        in
+        Ok
+          {
+            def_id;
+            item_meta;
+            generics;
+            parent_clauses;
+            consts;
+            types;
+            required_methods;
+            provided_methods;
+          }
+    | _ -> Error "")
+
+(* Defined by hand because we discard the empty list of item clauses *)
+and trait_impl_of_json (id_to_file : id_to_file_map) (js : json) :
+    (trait_impl, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc
+        [
+          ("def_id", def_id);
+          ("item_meta", item_meta);
+          ("impl_trait", impl_trait);
+          ("generics", generics);
+          ("parent_trait_refs", parent_trait_refs);
+          ("consts", consts);
+          ("types", types);
+          ("required_methods", required_methods);
+          ("provided_methods", provided_methods);
+        ] ->
+        let* def_id = trait_impl_id_of_json def_id in
+        let* item_meta = item_meta_of_json id_to_file item_meta in
+        let* impl_trait = trait_decl_ref_of_json impl_trait in
+        let* generics = generic_params_of_json id_to_file generics in
+        let* parent_trait_refs =
+          vector_of_json trait_clause_id_of_json trait_ref_of_json
+            parent_trait_refs
+        in
+        let* consts =
+          list_of_json
+            (pair_of_json trait_item_name_of_json
+               (pair_of_json ty_of_json global_decl_id_of_json))
+            consts
+        in
+        let* types =
+          list_of_json
+            (pair_of_json trait_item_name_of_json
+               (pair_of_json (list_of_json trait_ref_of_json) ty_of_json))
+            types
+        in
+        let types = List.map (fun (name, (_, ty)) -> (name, ty)) types in
+        let* required_methods =
+          list_of_json
+            (pair_of_json trait_item_name_of_json fun_decl_id_of_json)
+            required_methods
+        in
+        let* provided_methods =
+          list_of_json
+            (pair_of_json trait_item_name_of_json fun_decl_id_of_json)
+            provided_methods
+        in
+        Ok
+          {
+            def_id;
+            item_meta;
+            impl_trait;
+            generics;
+            parent_trait_refs;
+            consts;
+            types;
+            required_methods;
+            provided_methods;
+          }
+    | _ -> Error "")
+
 (* __REPLACE5__ *)
 
 let type_declaration_group_of_json (js : json) :

charon/src/bin/generate-ml/main.rs

@@ -451,7 +451,7 @@ fn main() -> Result<()> {
             "GExprBody",
             "ItemKind",
         ],
-        &["TraitDecl", "TraitImpl", "GDeclarationGroup"],
+        &["GDeclarationGroup"],
     ];
     let template_path = dir.join("GAstOfJson.template.ml");
     let mut template = fs::read_to_string(&template_path)