Improve the check_generics pass

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.60"
+let supported_charon_version = "0.1.61"

charon-ml/src/generated/Generated_GAst.ml

@@ -113,14 +113,6 @@ and call = { func : fn_operand; args : operand list; dest : place }
  *)
 and assertion = { cond : operand; expected : bool }
 
-(** The id of a translated item. *)
-and any_decl_id =
-  | IdType of type_decl_id
-  | IdFun of fun_decl_id
-  | IdGlobal of global_decl_id
-  | IdTraitDecl of trait_decl_id
-  | IdTraitImpl of trait_impl_id
-
 and closure_kind = Fn | FnMut | FnOnce
 
 (** Additional information for closures.

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1057,6 +1057,20 @@ and trait_type_constraint_of_json (ctx : of_json_ctx) (js : json) :
         Ok ({ trait_ref; type_name; ty } : trait_type_constraint)
     | _ -> Error "")
 
+and generics_source_of_json (ctx : of_json_ctx) (js : json) :
+    (generics_source, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("Item", item) ] ->
+        let* item = any_decl_id_of_json ctx item in
+        Ok (Item item)
+    | `Assoc [ ("Method", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = trait_decl_id_of_json ctx x_0 in
+        let* x_1 = trait_item_name_of_json ctx x_1 in
+        Ok (Method (x_0, x_1))
+    | `String "Builtin" -> Ok Builtin
+    | _ -> Error "")
+
 and generic_args_of_json (ctx : of_json_ctx) (js : json) :
     (generic_args, string) result =
   combine_error_msgs js __FUNCTION__
@@ -1067,6 +1081,7 @@ and generic_args_of_json (ctx : of_json_ctx) (js : json) :
           ("types", types);
           ("const_generics", const_generics);
           ("trait_refs", trait_refs);
+          ("target", _);
         ] ->
         let* regions =
           vector_of_json region_id_of_json region_of_json ctx regions

charon-ml/src/generated/Generated_Types.ml

@@ -298,8 +298,16 @@ class virtual ['self] mapreduce_const_generic_base =
       fun _ x -> (x, self#zero)
   end
 
+(** The id of a translated item. *)
+type any_decl_id =
+  | IdType of type_decl_id
+  | IdFun of fun_decl_id
+  | IdGlobal of global_decl_id
+  | IdTraitDecl of trait_decl_id
+  | IdTraitImpl of trait_impl_id
+
 (** Const Generic Values. Either a primitive value, or a variable corresponding to a primitve value *)
-type const_generic =
+and const_generic =
   | CgGlobal of global_decl_id  (** A global constant *)
   | CgVar of const_generic_var_id de_bruijn_var  (** A const generic variable *)
   | CgValue of literal  (** A concrete value *)
@@ -549,6 +557,13 @@ and trait_impl_ref = {
   impl_generics : generic_args;
 }
 
+(** Each `GenericArgs` is meant for a corresponding `GenericParams`; this describes which one. *)
+and generics_source =
+  | Item of any_decl_id  (** A top-level item. *)
+  | Method of trait_decl_id * trait_item_name  (** A trait method. *)
+  | Builtin  (** A builtin item like `Box`. *)
+
+(** A set of generic arguments. *)
 and generic_args = {
   regions : region list;
   types : ty list;

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.60"
+version = "0.1.61"
 authors = ["Son Ho <[email protected]>"]
 edition = "2021"
 license = "Apache-2.0"

charon/src/ast/krate.rs

@@ -218,15 +218,21 @@ impl<'ctx> AnyTransItem<'ctx> {
         }
     }
 
+    /// See [`GenericParams::identity_args`].
+    pub fn identity_args(&self) -> GenericArgs {
+        self.generic_params()
+            .identity_args(GenericsSource::Item(self.id()))
+    }
+
     /// We can't implement `AstVisitable` because of the `'static` constraint, but it's ok because
     /// `AnyTransItem` isn't contained in any of our types.
     pub fn drive<V: VisitAst>(&self, visitor: &mut V) -> ControlFlow<V::Break> {
-        match self {
-            AnyTransItem::Type(d) => d.drive(visitor),
-            AnyTransItem::Fun(d) => d.drive(visitor),
-            AnyTransItem::Global(d) => d.drive(visitor),
-            AnyTransItem::TraitDecl(d) => d.drive(visitor),
-            AnyTransItem::TraitImpl(d) => d.drive(visitor),
+        match *self {
+            AnyTransItem::Type(d) => visitor.visit(d),
+            AnyTransItem::Fun(d) => visitor.visit(d),
+            AnyTransItem::Global(d) => visitor.visit(d),
+            AnyTransItem::TraitDecl(d) => visitor.visit(d),
+            AnyTransItem::TraitImpl(d) => visitor.visit(d),
         }
     }
 }
@@ -257,11 +263,11 @@ impl<'ctx> AnyTransItemMut<'ctx> {
     /// `AnyTransItemMut` isn't contained in any of our types.
     pub fn drive_mut<V: VisitAstMut>(&mut self, visitor: &mut V) -> ControlFlow<V::Break> {
         match self {
-            AnyTransItemMut::Type(d) => d.drive_mut(visitor),
-            AnyTransItemMut::Fun(d) => d.drive_mut(visitor),
-            AnyTransItemMut::Global(d) => d.drive_mut(visitor),
-            AnyTransItemMut::TraitDecl(d) => d.drive_mut(visitor),
-            AnyTransItemMut::TraitImpl(d) => d.drive_mut(visitor),
+            AnyTransItemMut::Type(d) => visitor.visit(*d),
+            AnyTransItemMut::Fun(d) => visitor.visit(*d),
+            AnyTransItemMut::Global(d) => visitor.visit(*d),
+            AnyTransItemMut::TraitDecl(d) => visitor.visit(*d),
+            AnyTransItemMut::TraitImpl(d) => visitor.visit(*d),
         }
     }
 }

charon/src/ast/types.rs

@@ -195,13 +195,29 @@ pub struct TraitTypeConstraint {
     pub ty: Ty,
 }
 
-#[derive(Default, Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)]
+/// Each `GenericArgs` is meant for a corresponding `GenericParams`; this describes which one.
+#[derive(Debug, Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)]
+pub enum GenericsSource {
+    /// A top-level item.
+    Item(AnyTransId),
+    /// A trait method.
+    Method(TraitDeclId, TraitItemName),
+    /// A builtin item like `Box`.
+    Builtin,
+}
+
+/// A set of generic arguments.
+#[derive(Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub struct GenericArgs {
     pub regions: Vector<RegionId, Region>,
     pub types: Vector<TypeVarId, Ty>,
     pub const_generics: Vector<ConstGenericVarId, ConstGeneric>,
     // TODO: rename to match [GenericParams]?
     pub trait_refs: Vector<TraitClauseId, TraitRef>,
+    #[charon::opaque]
+    #[drive(skip)]
+    /// Each `GenericArgs` is meant for a corresponding `GenericParams`; this records which one.
+    pub target: GenericsSource,
 }
 
 /// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash

charon/src/ast/types_utils.rs

@@ -5,6 +5,7 @@ use derive_generic_visitor::*;
 use std::collections::HashSet;
 use std::convert::Infallible;
 use std::iter::Iterator;
+use std::mem;
 use std::ops::Index;
 
 impl GenericParams {
@@ -71,12 +72,12 @@ impl GenericParams {
     /// Construct a set of generic arguments in the scope of `self` that matches `self` and feeds
     /// each required parameter with itself. E.g. given parameters for `<T, U> where U:
     /// PartialEq<T>`, the arguments would be `<T, U>[@TraitClause0]`.
-    pub fn identity_args(&self) -> GenericArgs {
-        self.identity_args_at_depth(DeBruijnId::zero())
+    pub fn identity_args(&self, target: GenericsSource) -> GenericArgs {
+        self.identity_args_at_depth(target, DeBruijnId::zero())
     }
 
     /// Like `identity_args` but uses variables bound at the given depth.
-    pub fn identity_args_at_depth(&self, depth: DeBruijnId) -> GenericArgs {
+    pub fn identity_args_at_depth(&self, target: GenericsSource, depth: DeBruijnId) -> GenericArgs {
         GenericArgs {
             regions: self
                 .regions
@@ -91,25 +92,7 @@ impl GenericParams {
                 kind: TraitRefKind::Clause(DeBruijnVar::bound(depth, id)),
                 trait_decl_ref: clause.trait_.clone(),
             }),
-        }
-    }
-
-    /// Like `identity_args`, but uses free variables instead of bound ones.
-    pub fn free_identity_args(&self) -> GenericArgs {
-        GenericArgs {
-            regions: self
-                .regions
-                .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::free(id))),
-            types: self
-                .types
-                .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::free(id)).into_ty()),
-            const_generics: self
-                .const_generics
-                .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::free(id))),
-            trait_refs: self.trait_clauses.map_ref_indexed(|id, clause| TraitRef {
-                kind: TraitRefKind::Clause(DeBruijnVar::free(id)),
-                trait_decl_ref: clause.trait_.clone(),
-            }),
+            target,
         }
     }
 }
@@ -142,6 +125,7 @@ impl GenericArgs {
             types,
             const_generics,
             trait_refs,
+            target: _,
         } = self;
         regions.len() + types.len() + const_generics.len() + trait_refs.len()
     }
@@ -150,14 +134,20 @@ impl GenericArgs {
         self.len() == 0
     }
 
-    pub fn empty() -> Self {
-        GenericArgs::default()
+    pub fn empty(target: GenericsSource) -> Self {
+        GenericArgs {
+            regions: Default::default(),
+            types: Default::default(),
+            const_generics: Default::default(),
+            trait_refs: Default::default(),
+            target,
+        }
     }
 
-    pub fn new_from_types(types: Vector<TypeVarId, Ty>) -> Self {
+    pub fn new_for_builtin(types: Vector<TypeVarId, Ty>) -> Self {
         GenericArgs {
             types,
-            ..Self::default()
+            ..Self::empty(GenericsSource::Builtin)
         }
     }
 
@@ -166,15 +156,23 @@ impl GenericArgs {
         types: Vector<TypeVarId, Ty>,
         const_generics: Vector<ConstGenericVarId, ConstGeneric>,
         trait_refs: Vector<TraitClauseId, TraitRef>,
+        target: GenericsSource,
     ) -> Self {
         Self {
             regions,
             types,
             const_generics,
             trait_refs,
+            target,
         }
     }
 
+    /// Changes the target.
+    pub fn with_target(mut self, target: GenericsSource) -> Self {
+        self.target = target;
+        self
+    }
+
     /// 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 {
@@ -189,43 +187,38 @@ impl GenericArgs {
     /// because the first type argument is the type for which the trait is
     /// implemented.
     pub fn pop_first_type_arg(&self) -> (Ty, Self) {
-        let GenericArgs {
-            regions,
-            types,
-            const_generics,
-            trait_refs,
-        } = self;
-        let mut it = types.iter();
-        let ty = it.next().unwrap().clone();
-        let types = it.cloned().collect();
-        (
-            ty,
-            GenericArgs {
-                regions: regions.clone(),
-                types,
-                const_generics: const_generics.clone(),
-                trait_refs: trait_refs.clone(),
-            },
-        )
+        let mut generics = self.clone();
+        let mut it = mem::take(&mut generics.types).into_iter();
+        let ty = it.next().unwrap();
+        generics.types = it.collect();
+        (ty, generics)
     }
 
     /// Concatenate this set of arguments with another one. Use with care, you must manage the
     /// order of arguments correctly.
-    pub fn concat(mut self, other: &Self) -> Self {
+    pub fn concat(mut self, target: GenericsSource, other: &Self) -> Self {
         let Self {
             regions,
             types,
             const_generics,
             trait_refs,
+            target: _,
         } = other;
         self.regions.extend_from_slice(regions);
         self.types.extend_from_slice(types);
         self.const_generics.extend_from_slice(const_generics);
         self.trait_refs.extend_from_slice(trait_refs);
+        self.target = target;
         self
     }
 }
 
+impl GenericsSource {
+    pub fn item<I: Into<AnyTransId>>(id: I) -> Self {
+        Self::Item(id.into())
+    }
+}
+
 impl IntegerTy {
     pub fn is_signed(&self) -> bool {
         matches!(
@@ -278,7 +271,7 @@ impl Ty {
 
     /// Return the unit type
     pub fn mk_unit() -> Ty {
-        TyKind::Adt(TypeId::Tuple, GenericArgs::empty()).into_ty()
+        TyKind::Adt(TypeId::Tuple, GenericArgs::empty(GenericsSource::Builtin)).into_ty()
     }
 
     /// Return true if this is a scalar type
@@ -381,6 +374,35 @@ impl std::ops::Deref for Ty {
 /// For deref patterns.
 unsafe impl std::ops::DerefPure for Ty {}
 
+impl TypeId {
+    pub fn generics_target(&self) -> GenericsSource {
+        match *self {
+            TypeId::Adt(decl_id) => GenericsSource::item(decl_id),
+            TypeId::Tuple | TypeId::Builtin(..) => GenericsSource::Builtin,
+        }
+    }
+}
+
+impl FunId {
+    pub fn generics_target(&self) -> GenericsSource {
+        match *self {
+            FunId::Regular(fun_id) => GenericsSource::item(fun_id),
+            FunId::Builtin(..) => GenericsSource::Builtin,
+        }
+    }
+}
+
+impl FunIdOrTraitMethodRef {
+    pub fn generics_target(&self) -> GenericsSource {
+        match self {
+            FunIdOrTraitMethodRef::Fun(fun_id) => fun_id.generics_target(),
+            FunIdOrTraitMethodRef::Trait(trait_ref, name, _) => {
+                GenericsSource::Method(trait_ref.trait_decl_ref.skip_binder.trait_id, name.clone())
+            }
+        }
+    }
+}
+
 impl Field {
     /// The new name for this field, as suggested by the `#[charon::rename]` attribute.
     pub fn renamed_name(&self) -> Option<&str> {

charon/src/ast/visitor.rs

@@ -75,6 +75,10 @@ use index_vec::Idx;
     )
 )]
 pub trait AstVisitable: Any {
+    /// The name of the type, used for debug logging.
+    fn name(&self) -> &'static str {
+        std::any::type_name::<Self>()
+    }
     /// Visit all occurrences of that type inside `self`, in pre-order traversal.
     fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T)) {
         self.drive(&mut DynVisitor::new_shared::<T>(f));