Merge pull request #532 from Nadrieril/associated-types

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.63"
+let supported_charon_version = "0.1.64"

charon-ml/src/generated/Generated_GAst.ml

@@ -417,6 +417,8 @@ and cli_options = {
       (** Blacklist of items to keep opaque. These use the name-matcher syntax. *)
   exclude : string list;
       (** Blacklist of items to not translate at all. These use the name-matcher syntax. *)
+  remove_associated_types : string list;
+      (** List of traits for which we transform associated types to type parameters. *)
   hide_marker_traits : bool;
       (** Whether to hide the `Sized`, `Sync`, `Send` and `Unpin` marker traits anywhere they show
         up.

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -907,6 +907,13 @@ and trait_clause_id_of_json (ctx : of_json_ctx) (js : json) :
     | x -> TraitClauseId.id_of_json ctx x
     | _ -> Error "")
 
+and trait_type_constraint_id_of_json (ctx : of_json_ctx) (js : json) :
+    (trait_type_constraint_id, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | x -> TraitTypeConstraintId.id_of_json ctx x
+    | _ -> Error "")
+
 and type_var_of_json (ctx : of_json_ctx) (js : json) : (type_var, string) result
     =
   combine_error_msgs js __FUNCTION__
@@ -1202,7 +1209,7 @@ and generic_params_of_json (ctx : of_json_ctx) (js : json) :
             ctx types_outlive
         in
         let* trait_type_constraints =
-          list_of_json
+          vector_of_json trait_type_constraint_id_of_json
             (region_binder_of_json trait_type_constraint_of_json)
             ctx trait_type_constraints
         in
@@ -1619,6 +1626,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
           ("include", include_);
           ("opaque", opaque);
           ("exclude", exclude);
+          ("remove_associated_types", remove_associated_types);
           ("hide_marker_traits", hide_marker_traits);
           ("no_cargo", no_cargo);
           ("rustc_args", rustc_args);
@@ -1647,6 +1655,9 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
         let* included = list_of_json string_of_json ctx include_ in
         let* opaque = list_of_json string_of_json ctx opaque in
         let* exclude = list_of_json string_of_json ctx exclude in
+        let* remove_associated_types =
+          list_of_json string_of_json ctx remove_associated_types
+        in
         let* hide_marker_traits = bool_of_json ctx hide_marker_traits in
         let* no_cargo = bool_of_json ctx no_cargo in
         let* rustc_args = list_of_json string_of_json ctx rustc_args in
@@ -1676,6 +1687,7 @@ and cli_options_of_json (ctx : of_json_ctx) (js : json) :
              included;
              opaque;
              exclude;
+             remove_associated_types;
              hide_marker_traits;
              no_cargo;
              rustc_args;

charon-ml/src/generated/Generated_Types.ml

@@ -20,6 +20,7 @@ module ConstGenericVarId = IdGen ()
 module TraitDeclId = IdGen ()
 module TraitImplId = IdGen ()
 module TraitClauseId = IdGen ()
+module TraitTypeConstraintId = IdGen ()
 module UnsolvedTraitId = IdGen ()
 module RegionId = IdGen ()
 module Disambiguator = IdGen ()
@@ -31,6 +32,11 @@ type integer_type = Values.integer_type [@@deriving show, ord]
 type float_type = Values.float_type [@@deriving show, ord]
 type literal_type = Values.literal_type [@@deriving show, ord]
 
+(* Manually implemented because no type uses it (we use plain lists instead of
+   vectors in generic_params), which causes visitor inference problems if we
+   declare it within a visitor group. *)
+type trait_type_constraint_id = TraitTypeConstraintId.id [@@deriving show, ord]
+
 (** We define these types to control the name of the visitor functions *)
 type ('id, 'name) indexed_var = {
   index : 'id;  (** Unique index identifying the variable *)
@@ -256,12 +262,8 @@ and trait_instance_id =
           ```
        *)
   | Self
-      (** Self, in case of trait declarations/implementations.
-
-          Putting [Self] at the end on purpose, so that when ordering the clauses
-          we start with the other clauses (in particular, the local clauses). It
-          is useful to give priority to the local clauses when solving the trait
-          obligations which are fullfilled by the trait parameters.
+      (** The implicit `Self: Trait` clause. Present inside trait declarations, including trait
+          method declarations. Not present in trait implementations as we can use `TraitImpl` intead.
        *)
   | BuiltinOrAuto of
       trait_decl_ref region_binder

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.63"
+version = "0.1.64"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"
@@ -51,7 +51,7 @@ crates_io_api = { version = "0.11.0", optional = true }
 derive_generic_visitor = "0.1.0"
 env_logger = { version = "0.11", features = ["color"] }
 flate2 = { version = "1.0.34", optional = true }
-hashlink = { version = "0.9", features = ["serde_impl"] }
+indexmap = { version = "2.7.1", features = ["serde"] }
 index_vec = { version = "0.1.3", features = ["serde"] }
 indoc = "2"
 itertools = "0.13"

charon/src/ast/expressions_utils.rs

@@ -100,16 +100,23 @@ impl ProjectionElem {
                                 if variant_id.is_some() {
                                     return Err(());
                                 };
-                                let mut ty = fields.get(*field_id).ok_or(())?.ty.clone();
-                                ty.substitute(generics);
-                                ty
+                                fields
+                                    .get(*field_id)
+                                    .ok_or(())?
+                                    .ty
+                                    .clone()
+                                    .substitute(generics)
                             }
                             Enum(variants) => {
                                 let variant_id = variant_id.ok_or(())?;
                                 let variant = variants.get(variant_id).ok_or(())?;
-                                let mut ty = variant.fields.get(*field_id).ok_or(())?.ty.clone();
-                                ty.substitute(generics);
-                                ty
+                                variant
+                                    .fields
+                                    .get(*field_id)
+                                    .ok_or(())?
+                                    .ty
+                                    .clone()
+                                    .substitute(generics)
                             }
                             Opaque | Alias(_) | Error(_) => return Err(()),
                         }

charon/src/ast/krate.rs

@@ -3,7 +3,7 @@ use crate::formatter::{FmtCtx, Formatter, IntoFormatter};
 use crate::ids::Vector;
 use crate::reorder_decls::DeclarationsGroups;
 use derive_generic_visitor::{ControlFlow, Drive, DriveMut};
-use hashlink::LinkedHashSet;
+use indexmap::IndexSet;
 use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
 use serde::{Deserialize, Serialize};
 use serde_map_to_array::HashMapToArray;
@@ -114,7 +114,7 @@ pub struct TranslatedCrate {
 
     /// All the item ids, in the order in which we encountered them
     #[drive(skip)]
-    pub all_ids: LinkedHashSet<AnyTransId>,
+    pub all_ids: IndexSet<AnyTransId>,
     /// The names of all registered items. Available so we can know the names even of items that
     /// failed to translate.
     #[serde(with = "HashMapToArray::<AnyTransId, Name>")]

charon/src/ast/mod.rs

@@ -28,6 +28,6 @@ pub use krate::*;
 pub use meta::*;
 pub use names::*;
 pub use types::*;
-pub use types_utils::TyVisitable;
+pub use types_utils::*;
 pub use values::*;
 pub use visitor::*;

charon/src/ast/types.rs

@@ -115,12 +115,8 @@ pub enum TraitRefKind {
     #[charon::opaque]
     ItemClause(Box<TraitRefKind>, TraitDeclId, TraitItemName, TraitClauseId),
 
-    /// Self, in case of trait declarations/implementations.
-    ///
-    /// Putting [Self] at the end on purpose, so that when ordering the clauses
-    /// we start with the other clauses (in particular, the local clauses). It
-    /// is useful to give priority to the local clauses when solving the trait
-    /// obligations which are fullfilled by the trait parameters.
+    /// The implicit `Self: Trait` clause. Present inside trait declarations, including trait
+    /// method declarations. Not present in trait implementations as we can use `TraitImpl` intead.
     #[charon::rename("Self")]
     SelfId,
 
@@ -291,7 +287,7 @@ pub struct GenericParams {
     /// The type outlives the region
     pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
     /// Constraints over trait associated types
-    pub trait_type_constraints: Vec<RegionBinder<TraitTypeConstraint>>,
+    pub trait_type_constraints: Vector<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
 }
 
 /// A predicate of the form `exists<T> where T: Trait`.
@@ -329,7 +325,7 @@ pub enum PredicateOrigin {
     // trait Trait {}
     // ```
     TraitSelf,
-    // Note: this also includes supertrait constraings.
+    // Note: this also includes supertrait constraints.
     // ```
     // trait Trait<T: Clone> {}
     // trait Trait<T> where T: Clone {}