Merge pull request #518 from Nadrieril/tweaks

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.61"
+let supported_charon_version = "0.1.62"

charon-ml/src/Substitute.ml

@@ -158,29 +158,27 @@ let st_substitute_visitor =
       (* Note that we don't visit the bound variables. *)
       let { binder_params; binder_value } = x in
       (* Crucial: we shift the substitution to be valid under this binder. *)
-      let binder_value = visit_value (shift_subst subst) binder_value in
+      let subst = shift_subst subst in
+      let binder_params = self#visit_generic_params subst binder_params in
+      let binder_value = visit_value subst binder_value in
       { binder_params; binder_value }
 
     method! visit_region_binder visit_value (subst : subst) x =
       (* Note that we don't visit the bound variables. *)
       let { binder_regions; binder_value } = x in
       (* Crucial: we shift the substitution to be valid under this binder. *)
-      let binder_value = visit_value (shift_subst subst) binder_value in
+      let subst = shift_subst subst in
+      let binder_regions =
+        self#visit_list self#visit_region_var subst binder_regions
+      in
+      let binder_value = visit_value subst binder_value in
       { binder_regions; binder_value }
 
     method! visit_RVar (subst : subst) var = subst.r_subst var
     method! visit_TVar (subst : subst) var = subst.ty_subst var
     method! visit_CgVar (subst : subst) var = subst.cg_subst var
     method! visit_Clause (subst : subst) var = subst.tr_subst var
     method! visit_Self (subst : subst) = subst.tr_self
-
-    method! visit_type_var_id _ _ =
-      (* We should never get here because we reimplemented [visit_TypeVar] *)
-      raise (Failure "Unexpected")
-
-    method! visit_const_generic_var_id _ _ =
-      (* We should never get here because we reimplemented [visit_Var] *)
-      raise (Failure "Unexpected")
   end
 
 (** Substitute types variables and regions in a type.

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -1063,12 +1063,12 @@ and generics_source_of_json (ctx : of_json_ctx) (js : json) :
     (match js with
     | `Assoc [ ("Item", item) ] ->
         let* item = any_decl_id_of_json ctx item in
-        Ok (Item item)
+        Ok (GSItem 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
+        Ok (GSMethod (x_0, x_1))
+    | `String "Builtin" -> Ok GSBuiltin
     | _ -> Error "")
 
 and generic_args_of_json (ctx : of_json_ctx) (js : json) :
@@ -1115,6 +1115,18 @@ and region_binder_of_json :
         Ok ({ binder_regions; binder_value } : _ region_binder)
     | _ -> Error "")
 
+and binder_kind_of_json (ctx : of_json_ctx) (js : json) :
+    (binder_kind, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("TraitMethod", `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 (BKTraitMethod (x_0, x_1))
+    | `String "InherentImplBlock" -> Ok BKInherentImplBlock
+    | `String "Other" -> Ok BKOther
+    | _ -> Error "")
+
 and binder_of_json :
       'a0.
       (of_json_ctx -> json -> ('a0, string) result) ->
@@ -1124,7 +1136,8 @@ and binder_of_json :
  fun arg0_of_json ctx js ->
   combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("params", params); ("skip_binder", skip_binder) ] ->
+    | `Assoc [ ("params", params); ("skip_binder", skip_binder); ("kind", _) ]
+      ->
         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)

charon-ml/src/generated/Generated_Types.ml

@@ -300,9 +300,9 @@ and trait_impl_ref = {
 
 (** 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`. *)
+  | GSItem of any_decl_id  (** A top-level item. *)
+  | GSMethod of trait_decl_id * trait_item_name  (** A trait method. *)
+  | GSBuiltin  (** A builtin item like `Box`. *)
 
 (** A set of generic arguments. *)
 and generic_args = {
@@ -578,9 +578,18 @@ and trait_type_constraint = {
   ty : ty;
 }
 
+and binder_kind =
+  | BKTraitMethod of trait_decl_id * trait_item_name
+      (** The parameters of a trait method. Used in the `methods` lists in trait decls and trait
+          impls.
+       *)
+  | BKInherentImplBlock
+      (** The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods. *)
+  | BKOther  (** Some other use of a binder outside the main Charon ast. *)
+
 (** 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).
+    parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for
+    now), trait methods, GATs (TODO).
  *)
 and 'a0 binder = {
   binder_params : generic_params;

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.61"
+version = "0.1.62"
 authors = ["Son Ho <[email protected]>"]
 edition = "2021"
 license = "Apache-2.0"
@@ -76,8 +76,7 @@ tracing = { version = "0.1", features = [ "max_level_trace" ] }
 wait-timeout = { version = "0.2.0", optional = true }
 which = "7.0"
 
-# hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
-hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "fix-call-generics", optional = true }
+hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 

charon/src/ast/names.rs

@@ -29,13 +29,10 @@ pub enum PathElem {
 #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
 #[charon::variants_prefix("ImplElem")]
 pub enum ImplElem {
-    Ty(BoundTy),
+    Ty(Binder<Ty>),
     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

@@ -197,6 +197,7 @@ pub struct TraitTypeConstraint {
 
 /// Each `GenericArgs` is meant for a corresponding `GenericParams`; this describes which one.
 #[derive(Debug, Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)]
+#[charon::variants_prefix("GS")]
 pub enum GenericsSource {
     /// A top-level item.
     Item(AnyTransId),
@@ -233,14 +234,21 @@ 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>;
+#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
+#[charon::variants_prefix("BK")]
+pub enum BinderKind {
+    /// The parameters of a trait method. Used in the `methods` lists in trait decls and trait
+    /// impls.
+    TraitMethod(TraitDeclId, TraitItemName),
+    /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods.
+    InherentImplBlock,
+    /// Some other use of a binder outside the main Charon ast.
+    Other,
+}
 
 /// 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).
+/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for
+/// now), trait methods, GATs (TODO).
 #[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
 pub struct Binder<T> {
     #[charon::rename("binder_params")]
@@ -249,6 +257,10 @@ pub struct Binder<T> {
     /// incorrectly. Prefer using helper methods.
     #[charon::rename("binder_value")]
     pub skip_binder: T,
+    /// The kind of binder this is.
+    #[charon::opaque]
+    #[drive(skip)]
+    pub kind: BinderKind,
 }
 
 /// Generic parameters for a declaration.
@@ -266,11 +278,11 @@ pub struct GenericParams {
     // 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<BoundRegionOutlives>,
+    pub regions_outlive: Vec<RegionBinder<RegionOutlives>>,
     /// The type outlives the region
-    pub types_outlive: Vec<BoundTypeOutlives>,
+    pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
     /// Constraints over trait associated types
-    pub trait_type_constraints: Vec<BoundTraitTypeConstraint>,
+    pub trait_type_constraints: Vec<RegionBinder<TraitTypeConstraint>>,
 }
 
 /// A predicate of the form `exists<T> where T: Trait`.
@@ -677,11 +689,9 @@ 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(BoundArrowSig),
+    Arrow(RegionBinder<(Vec<Ty>, Ty)>),
 }
 
-pub type BoundArrowSig = RegionBinder<(Vec<Ty>, Ty)>;
-
 /// Builtin types identifiers.
 ///
 /// WARNING: for now, all the built-in types are covariant in the generic

charon/src/ast/types_utils.rs

@@ -98,10 +98,11 @@ impl GenericParams {
 }
 
 impl<T> Binder<T> {
-    pub fn new(params: GenericParams, skip_binder: T) -> Self {
+    pub fn new(kind: BinderKind, params: GenericParams, skip_binder: T) -> Self {
         Self {
             params,
             skip_binder,
+            kind,
         }
     }
 
@@ -118,6 +119,19 @@ impl<T> Binder<T> {
     }
 }
 
+impl<T> RegionBinder<T> {
+    /// Wrap the value in an empty region binder, shifting variables appropriately.
+    pub fn empty(x: T) -> Self
+    where
+        T: TyVisitable,
+    {
+        RegionBinder {
+            regions: Default::default(),
+            skip_binder: x.move_under_binder(),
+        }
+    }
+}
+
 impl GenericArgs {
     pub fn len(&self) -> usize {
         let GenericArgs {
@@ -557,6 +571,11 @@ pub trait TyVisitable: Sized + AstVisitable {
         self.drive_mut(&mut SubstVisitor::new(generics));
     }
 
+    /// Move under one binder.
+    fn move_under_binder(self) -> Self {
+        self.move_under_binders(DeBruijnId::one())
+    }
+
     /// Move under `depth` binders.
     fn move_under_binders(mut self, depth: DeBruijnId) -> Self {
         let Continue(()) = self.visit_db_id::<Infallible>(|id| {