Prepare charon for inner binding levels

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.57"
+let supported_charon_version = "0.1.58"

charon-ml/src/NameMatcher.ml

@@ -481,8 +481,8 @@ let rec match_name_with_generics (ctx : ctx) (c : match_config)
          - the impl is a trait impl
       *)
       match impl with
-      | ImplElemTy (_, ty) ->
-          match_expr_with_ty ctx c (mk_empty_maps ()) pty ty
+      | ImplElemTy bound_ty ->
+          match_expr_with_ty ctx c (mk_empty_maps ()) pty bound_ty.binder_value
           && g = TypesUtils.empty_generic_args
       | ImplElemTrait impl_id ->
           match_expr_with_trait_impl_id ctx c pty impl_id
@@ -496,8 +496,8 @@ let rec match_name_with_generics (ctx : ctx) (c : match_config)
          - the impl is a trait impl
       *)
       match impl with
-      | ImplElemTy (_, ty) ->
-          match_expr_with_ty ctx c (mk_empty_maps ()) pty ty
+      | ImplElemTy bound_ty ->
+          match_expr_with_ty ctx c (mk_empty_maps ()) pty bound_ty.binder_value
           && match_name_with_generics ctx c p n g
       | ImplElemTrait impl_id ->
           match_expr_with_trait_impl_id ctx c pty impl_id
@@ -935,7 +935,8 @@ and path_elem_with_generic_args_to_pattern (ctx : ctx) (c : to_pat_config)
 and impl_elem_to_pattern (ctx : ctx) (c : to_pat_config) (impl : T.impl_elem) :
     pattern_elem =
   match impl with
-  | ImplElemTy (generics, ty) -> PImpl (ty_to_pattern ctx c generics ty)
+  | ImplElemTy bound_ty ->
+      PImpl (ty_to_pattern ctx c bound_ty.binder_params bound_ty.binder_value)
   | ImplElemTrait impl_id ->
       let impl = T.TraitImplId.Map.find impl_id ctx.trait_impls in
       PImpl (trait_decl_ref_to_pattern ctx c impl.generics impl.impl_trait)

charon-ml/src/PrintTypes.ml

@@ -281,10 +281,10 @@ and trait_instance_id_to_string (env : 'a fmt_env) (id : trait_instance_id) :
 
 and impl_elem_to_string (env : 'a fmt_env) (elem : impl_elem) : string =
   match elem with
-  | ImplElemTy (generics, ty) ->
+  | ImplElemTy bound_ty ->
       (* Locally replace the generics and the predicates *)
-      let env = fmt_env_update_generics_and_preds env generics in
-      ty_to_string env ty
+      let env = fmt_env_update_generics_and_preds env bound_ty.binder_params in
+      ty_to_string env bound_ty.binder_value
   | ImplElemTrait impl_id -> begin
       match TraitImplId.Map.find_opt impl_id env.trait_impls with
       | None -> trait_impl_id_to_string env impl_id

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -826,10 +826,9 @@ and impl_elem_of_json (ctx : of_json_ctx) (js : json) :
     (impl_elem, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("Ty", `List [ x_0; x_1 ]) ] ->
-        let* x_0 = generic_params_of_json ctx x_0 in
-        let* x_1 = ty_of_json ctx x_1 in
-        Ok (ImplElemTy (x_0, x_1))
+    | `Assoc [ ("Ty", ty) ] ->
+        let* ty = binder_of_json ty_of_json ctx ty in
+        Ok (ImplElemTy ty)
     | `Assoc [ ("Trait", trait) ] ->
         let* trait = trait_impl_id_of_json ctx trait in
         Ok (ImplElemTrait trait)
@@ -1087,6 +1086,21 @@ and region_binder_of_json :
         Ok ({ binder_regions; binder_value } : _ region_binder)
     | _ -> Error "")
 
+and binder_of_json :
+      'a0.
+      (of_json_ctx -> json -> ('a0, string) result) ->
+      of_json_ctx ->
+      json ->
+      ('a0 binder, string) result =
+ fun arg0_of_json ctx js ->
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("params", params); ("skip_binder", skip_binder) ] ->
+        let* binder_params = generic_params_of_json ctx params in
+        let* binder_value = arg0_of_json ctx skip_binder in
+        Ok ({ binder_params; binder_value } : _ binder)
+    | _ -> Error "")
+
 and generic_params_of_json (ctx : of_json_ctx) (js : json) :
     (generic_params, string) result =
   combine_error_msgs js __FUNCTION__

charon-ml/src/generated/Generated_Types.ml

@@ -328,7 +328,9 @@ type const_generic =
 (** Region variable. *)
 type region_var = (region_id, string option) indexed_var [@@deriving show, ord]
 
-(** A value of type `'a` bound by generic parameters. *)
+(** A value of type `'a` bound by region parameters. We can't use `binder`
+    below because this would require merging the two recursive def groups below
+    which causes name clash issues in the visitor derives. *)
 type 'a region_binder = { binder_regions : region_var list; binder_value : 'a }
 [@@deriving show, ord]
 
@@ -766,9 +768,7 @@ type path_elem =
       ```
     We distinguish the two.
  *)
-and impl_elem =
-  | ImplElemTy of generic_params * ty
-  | ImplElemTrait of trait_impl_id
+and impl_elem = ImplElemTy of ty binder | ImplElemTrait of trait_impl_id
 
 (** An item name/path
 
@@ -806,19 +806,57 @@ and impl_elem =
 
     Also note that the first path element in the name is always the crate name.
  *)
-and name = path_elem list [@@deriving show, ord]
+and name = path_elem list
+
+(** A value of type `T` bound by generic parameters. Used in any context where we're adding generic
+    parameters that aren't on the top-level item, e.g. `for<'a>` clauses, trait methods (TODO),
+    GATs (TODO).
+ *)
+and 'a0 binder = {
+  binder_params : generic_params;
+  binder_value : 'a0;
+      (** Named this way to highlight accesses to the inner value that might be handling parameters
+        incorrectly. Prefer using helper methods.
+     *)
+}
+[@@deriving show, ord]
+
+class ['self] iter_type_decl_base_base =
+  object (self : 'self)
+    inherit [_] iter_generic_params
+
+    method visit_binder : 'a. ('env -> 'a -> unit) -> 'env -> 'a binder -> unit
+        =
+      fun visit_binder_value env x ->
+        let { binder_params; binder_value } = x in
+        self#visit_generic_params env binder_params;
+        visit_binder_value env binder_value
+  end
+
+class virtual ['self] map_type_decl_base_base =
+  object (self : 'self)
+    inherit [_] map_generic_params
+
+    method visit_binder
+        : 'a. ('env -> 'a -> 'a) -> 'env -> 'a binder -> 'a binder =
+      fun visit_binder_value env x ->
+        let { binder_params; binder_value } = x in
+        let binder_params = self#visit_generic_params env binder_params in
+        let binder_value = visit_binder_value env binder_value in
+        { binder_params; binder_value }
+  end
 
 (* Ancestors for the type_decl visitors *)
 class ['self] iter_type_decl_base =
   object (self : 'self)
-    inherit [_] iter_generic_params
+    inherit [_] iter_type_decl_base_base
     method visit_attr_info : 'env -> attr_info -> unit = fun _ _ -> ()
     method visit_name : 'env -> name -> unit = fun _ _ -> ()
   end
 
 class ['self] map_type_decl_base =
   object (self : 'self)
-    inherit [_] map_generic_params
+    inherit [_] map_type_decl_base_base
     method visit_attr_info : 'env -> attr_info -> attr_info = fun _ x -> x
     method visit_name : 'env -> name -> name = fun _ x -> x
   end

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.57"
+version = "0.1.58"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"

charon/src/ast/mod.rs

@@ -27,4 +27,5 @@ pub use krate::*;
 pub use meta::*;
 pub use names::*;
 pub use types::*;
+pub use types_utils::TyVisitable;
 pub use values::*;

charon/src/ast/names.rs

@@ -29,10 +29,13 @@ pub enum PathElem {
 #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
 #[charon::variants_prefix("ImplElem")]
 pub enum ImplElem {
-    Ty(GenericParams, Ty),
+    Ty(BoundTy),
     Trait(TraitImplId),
 }
 
+/// Alias used for visitors.
+pub type BoundTy = Binder<Ty>;
+
 /// An item name/path
 ///
 /// A name really is a list of strings. However, we sometimes need to

charon/src/ast/types.rs

@@ -174,7 +174,7 @@ pub struct TraitImplRef {
 }
 
 /// .0 outlives .1
-#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
 pub struct OutlivesPred<T, U>(pub T, pub U);
 
 // The derive macro doesn't handle generics well.
@@ -205,7 +205,7 @@ pub type TypeOutlives = OutlivesPred<Ty, Region>;
 /// T : Foo<S = String>
 ///         ^^^^^^^^^^
 /// ```
-#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Drive, DriveMut)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub struct TraitTypeConstraint {
     pub trait_ref: TraitRef,
     pub type_name: TraitItemName,
@@ -221,9 +221,9 @@ pub struct GenericArgs {
     pub trait_refs: Vector<TraitClauseId, TraitRef>,
 }
 
-/// A value of type `T` bound by generic parameters. Used in any context where we're adding generic
-/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses, trait methods (TODO),
-/// GATs (TODO).
+/// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash
+/// issues in the derived ocaml visitors.
+/// TODO: merge with `binder`
 #[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash)]
 pub struct RegionBinder<T> {
     #[charon::rename("binder_regions")]
@@ -234,26 +234,44 @@ pub struct RegionBinder<T> {
     pub skip_binder: T,
 }
 
+// Renames useful for visitor derives
+pub type BoundTypeOutlives = RegionBinder<TypeOutlives>;
+pub type BoundRegionOutlives = RegionBinder<RegionOutlives>;
+pub type BoundTraitTypeConstraint = RegionBinder<TraitTypeConstraint>;
+
+/// A value of type `T` bound by generic parameters. Used in any context where we're adding generic
+/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses, trait methods (TODO),
+/// GATs (TODO).
+#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash)]
+pub struct Binder<T> {
+    #[charon::rename("binder_params")]
+    pub params: GenericParams,
+    /// Named this way to highlight accesses to the inner value that might be handling parameters
+    /// incorrectly. Prefer using helper methods.
+    #[charon::rename("binder_value")]
+    pub skip_binder: T,
+}
+
 /// Generic parameters for a declaration.
 /// We group the generics which come from the Rust compiler substitutions
 /// (the regions, types and const generics) as well as the trait clauses.
 /// The reason is that we consider that those are parameters that need to
 /// be filled. We group in a different place the predicates which are not
 /// trait clauses, because those enforce constraints but do not need to
 /// be filled with witnesses/instances.
-#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
+#[derive(Debug, Default, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub struct GenericParams {
     pub regions: Vector<RegionId, RegionVar>,
     pub types: Vector<TypeVarId, TypeVar>,
     pub const_generics: Vector<ConstGenericVarId, ConstGenericVar>,
     // TODO: rename to match [GenericArgs]?
     pub trait_clauses: Vector<TraitClauseId, TraitClause>,
     /// The first region in the pair outlives the second region
-    pub regions_outlive: Vec<RegionBinder<RegionOutlives>>,
+    pub regions_outlive: Vec<BoundRegionOutlives>,
     /// The type outlives the region
-    pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
+    pub types_outlive: Vec<BoundTypeOutlives>,
     /// Constraints over trait associated types
-    pub trait_type_constraints: Vec<RegionBinder<TraitTypeConstraint>>,
+    pub trait_type_constraints: Vec<BoundTraitTypeConstraint>,
 }
 
 /// A predicate of the form `exists<T> where T: Trait`.
@@ -263,7 +281,7 @@ pub struct GenericParams {
 pub struct ExistentialPredicate;
 
 /// Where a given predicate came from.
-#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub enum PredicateOrigin {
     // Note: we use this for globals too, but that's only available with an unstable feature.
     // ```
@@ -644,9 +662,11 @@ pub enum TyKind {
     /// This is essentially a "constrained" function signature:
     /// arrow types can only contain generic lifetime parameters
     /// (no generic types), no predicates, etc.
-    Arrow(RegionBinder<(Vec<Ty>, Ty)>),
+    Arrow(BoundArrowSig),
 }
 
+pub type BoundArrowSig = RegionBinder<(Vec<Ty>, Ty)>;
+
 /// Builtin types identifiers.
 ///
 /// WARNING: for now, all the built-in types are covariant in the generic