charon_lib/ast/
types.rs

1use crate::ids::Vector;
2use crate::{ast::*, common::hash_consing::HashConsed};
3use derive_generic_visitor::*;
4use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
5use serde::{Deserialize, Serialize};
6
7mod vars;
8pub use vars::*;
9
10#[derive(
11    Debug,
12    PartialEq,
13    Eq,
14    Copy,
15    Clone,
16    Hash,
17    PartialOrd,
18    Ord,
19    EnumIsA,
20    EnumAsGetters,
21    Serialize,
22    Deserialize,
23    Drive,
24    DriveMut,
25)]
26#[charon::variants_prefix("R")]
27pub enum Region {
28    /// Region variable. See `DeBruijnVar` for details.
29    Var(RegionDbVar),
30    /// Static region
31    Static,
32    /// Erased region
33    Erased,
34}
35
36/// Identifier of a trait instance.
37/// This is derived from the trait resolution.
38///
39/// Should be read as a path inside the trait clauses which apply to the current
40/// definition. Note that every path designated by `TraitInstanceId` refers
41/// to a *trait instance*, which is why the [`TraitRefKind::Clause`] variant may seem redundant
42/// with some of the other variants.
43#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
44#[charon::rename("TraitInstanceId")]
45pub enum TraitRefKind {
46    /// A specific top-level implementation item.
47    TraitImpl(TraitImplRef),
48
49    /// One of the local clauses.
50    ///
51    /// Example:
52    /// ```text
53    /// fn f<T>(...) where T : Foo
54    ///                    ^^^^^^^
55    ///                    Clause(0)
56    /// ```
57    Clause(ClauseDbVar),
58
59    /// A parent clause
60    ///
61    /// Remark: the [TraitDeclId] gives the trait declaration which is
62    /// implemented by the instance id from which we take the parent clause
63    /// (see example below). It is not necessary and included for convenience.
64    ///
65    /// Remark: Ideally we should store a full `TraitRef` instead, but hax does not give us enough
66    /// information to get the right generic args.
67    ///
68    /// Example:
69    /// ```text
70    /// trait Foo1 {}
71    /// trait Foo2 { fn f(); }
72    ///
73    /// trait Bar : Foo1 + Foo2 {}
74    ///             ^^^^   ^^^^
75    ///                    parent clause 1
76    ///     parent clause 0
77    ///
78    /// fn g<T : Bar>(x : T) {
79    ///   x.f()
80    ///   ^^^^^
81    ///   Parent(Clause(0), Bar, 1)::f(x)
82    ///                          ^
83    ///                          parent clause 1 of clause 0
84    ///                     ^^^
85    ///              clause 0 implements Bar
86    /// }
87    /// ```
88    ParentClause(Box<TraitRefKind>, TraitDeclId, TraitClauseId),
89
90    /// A clause defined on an associated type. This variant is only used during translation; after
91    /// the `lift_associated_item_clauses` pass, clauses on items become `ParentClause`s.
92    ///
93    /// Remark: the [TraitDeclId] gives the trait declaration which is
94    /// implemented by the trait implementation from which we take the item
95    /// (see below). It is not necessary and provided for convenience.
96    ///
97    /// Example:
98    /// ```text
99    /// trait Foo {
100    ///   type W: Bar0 + Bar1 // Bar1 contains a method bar1
101    ///                  ^^^^
102    ///               this is the clause 1 applying to W
103    /// }
104    ///
105    /// fn f<T : Foo>(x : T::W) {
106    ///   x.bar1();
107    ///   ^^^^^^^
108    ///   ItemClause(Clause(0), Foo, W, 1)
109    ///                              ^^^^
110    ///                              clause 1 from item W (from local clause 0)
111    ///                         ^^^
112    ///                local clause 0 implements Foo
113    /// }
114    /// ```
115    #[charon::opaque]
116    ItemClause(Box<TraitRefKind>, TraitDeclId, TraitItemName, TraitClauseId),
117
118    /// The implicit `Self: Trait` clause. Present inside trait declarations, including trait
119    /// method declarations. Not present in trait implementations as we can use `TraitImpl` intead.
120    #[charon::rename("Self")]
121    SelfId,
122
123    /// A trait implementation that is computed by the compiler, such as for built-in trait
124    /// `Sized`. This morally points to an invisible `impl` block; as such it contains
125    /// the information we may need from one.
126    BuiltinOrAuto {
127        trait_decl_ref: PolyTraitDeclRef,
128        /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration.
129        /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T:
130        /// FnOnce`.
131        parent_trait_refs: Vector<TraitClauseId, TraitRef>,
132        /// The values of the associated types for this trait.
133        types: Vec<(TraitItemName, Ty)>,
134    },
135
136    /// The automatically-generated implementation for `dyn Trait`.
137    Dyn(PolyTraitDeclRef),
138
139    /// For error reporting.
140    #[charon::rename("UnknownTrait")]
141    #[drive(skip)]
142    Unknown(String),
143}
144
145/// A reference to a trait
146#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
147pub struct TraitRef {
148    #[charon::rename("trait_id")]
149    pub kind: TraitRefKind,
150    /// Not necessary, but useful
151    pub trait_decl_ref: PolyTraitDeclRef,
152}
153
154/// A predicate of the form `Type: Trait<Args>`.
155///
156/// About the generics, if we write:
157/// ```text
158/// impl Foo<bool> for String { ... }
159/// ```
160///
161/// The substitution is: `[String, bool]`.
162#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
163pub struct TraitDeclRef {
164    pub id: TraitDeclId,
165    pub generics: BoxedArgs,
166}
167
168/// A quantified trait predicate, e.g. `for<'a> Type<'a>: Trait<'a, Args>`.
169pub type PolyTraitDeclRef = RegionBinder<TraitDeclRef>;
170
171/// A reference to a tait impl, using the provided arguments.
172#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
173pub struct TraitImplRef {
174    pub id: TraitImplId,
175    pub generics: BoxedArgs,
176}
177
178/// .0 outlives .1
179#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
180pub struct OutlivesPred<T, U>(pub T, pub U);
181
182pub type RegionOutlives = OutlivesPred<Region, Region>;
183pub type TypeOutlives = OutlivesPred<Ty, Region>;
184
185/// A constraint over a trait associated type.
186///
187/// Example:
188/// ```text
189/// T : Foo<S = String>
190///         ^^^^^^^^^^
191/// ```
192#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
193pub struct TraitTypeConstraint {
194    pub trait_ref: TraitRef,
195    pub type_name: TraitItemName,
196    pub ty: Ty,
197}
198
199/// A set of generic arguments.
200#[derive(Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)]
201pub struct GenericArgs {
202    pub regions: Vector<RegionId, Region>,
203    pub types: Vector<TypeVarId, Ty>,
204    pub const_generics: Vector<ConstGenericVarId, ConstGeneric>,
205    // TODO: rename to match [GenericParams]?
206    pub trait_refs: Vector<TraitClauseId, TraitRef>,
207}
208
209pub type BoxedArgs = Box<GenericArgs>;
210
211/// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash
212/// issues in the derived ocaml visitors.
213/// TODO: merge with `binder`
214#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
215pub struct RegionBinder<T> {
216    #[charon::rename("binder_regions")]
217    pub regions: Vector<RegionId, RegionVar>,
218    /// Named this way to highlight accesses to the inner value that might be handling parameters
219    /// incorrectly. Prefer using helper methods.
220    #[charon::rename("binder_value")]
221    pub skip_binder: T,
222}
223
224#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
225#[charon::variants_prefix("BK")]
226pub enum BinderKind {
227    /// The parameters of a trait method. Used in the `methods` lists in trait decls and trait
228    /// impls.
229    TraitMethod(TraitDeclId, TraitItemName),
230    /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods.
231    InherentImplBlock,
232    /// Some other use of a binder outside the main Charon ast.
233    Other,
234}
235
236/// A value of type `T` bound by generic parameters. Used in any context where we're adding generic
237/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for
238/// now), trait methods, GATs (TODO).
239#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
240pub struct Binder<T> {
241    #[charon::rename("binder_params")]
242    pub params: GenericParams,
243    /// Named this way to highlight accesses to the inner value that might be handling parameters
244    /// incorrectly. Prefer using helper methods.
245    #[charon::rename("binder_value")]
246    pub skip_binder: T,
247    /// The kind of binder this is.
248    #[charon::opaque]
249    #[drive(skip)]
250    pub kind: BinderKind,
251}
252
253/// Generic parameters for a declaration.
254/// We group the generics which come from the Rust compiler substitutions
255/// (the regions, types and const generics) as well as the trait clauses.
256/// The reason is that we consider that those are parameters that need to
257/// be filled. We group in a different place the predicates which are not
258/// trait clauses, because those enforce constraints but do not need to
259/// be filled with witnesses/instances.
260#[derive(Default, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
261pub struct GenericParams {
262    pub regions: Vector<RegionId, RegionVar>,
263    pub types: Vector<TypeVarId, TypeVar>,
264    pub const_generics: Vector<ConstGenericVarId, ConstGenericVar>,
265    // TODO: rename to match [GenericArgs]?
266    pub trait_clauses: Vector<TraitClauseId, TraitClause>,
267    /// The first region in the pair outlives the second region
268    pub regions_outlive: Vec<RegionBinder<RegionOutlives>>,
269    /// The type outlives the region
270    pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
271    /// Constraints over trait associated types
272    pub trait_type_constraints: Vector<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
273}
274
275/// A predicate of the form `exists<T> where T: Trait`.
276///
277/// TODO: store something useful here
278#[derive(Debug, Default, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
279pub struct ExistentialPredicate;
280
281/// Where a given predicate came from.
282#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
283pub enum PredicateOrigin {
284    // Note: we use this for globals too, but that's only available with an unstable feature.
285    // ```
286    // fn function<T: Clone>() {}
287    // fn function<T>() where T: Clone {}
288    // const NONE<T: Copy>: Option<T> = None;
289    // ```
290    WhereClauseOnFn,
291    // ```
292    // struct Struct<T: Clone> {}
293    // struct Struct<T> where T: Clone {}
294    // type TypeAlias<T: Clone> = ...;
295    // ```
296    WhereClauseOnType,
297    // Note: this is both trait impls and inherent impl blocks.
298    // ```
299    // impl<T: Clone> Type<T> {}
300    // impl<T> Type<T> where T: Clone {}
301    // impl<T> Trait for Type<T> where T: Clone {}
302    // ```
303    WhereClauseOnImpl,
304    // The special `Self: Trait` clause which is in scope inside the definition of `Foo` or an
305    // implementation of it.
306    // ```
307    // trait Trait {}
308    // ```
309    TraitSelf,
310    // Note: this also includes supertrait constraints.
311    // ```
312    // trait Trait<T: Clone> {}
313    // trait Trait<T> where T: Clone {}
314    // trait Trait: Clone {}
315    // ```
316    WhereClauseOnTrait,
317    // ```
318    // trait Trait {
319    //     type AssocType: Clone;
320    // }
321    // ```
322    TraitItem(TraitItemName),
323}
324
325// rustc counts bytes in layouts as u64
326type ByteCount = u64;
327
328/// Simplified layout of a single variant.
329///
330/// Maps fields to their offset within the layout.
331#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
332pub struct VariantLayout {
333    /// The offset of each field.
334    #[drive(skip)]
335    pub field_offsets: Vector<FieldId, ByteCount>,
336    /// Whether the variant is uninhabited, i.e. has any valid possible value.
337    /// Note that uninhabited types can have arbitrary layouts.
338    #[drive(skip)]
339    pub uninhabited: bool,
340    /// The memory representation of the discriminant corresponding to this
341    /// variant. It must be of the same type as the corresponding [`DiscriminantLayout::tag_ty`].
342    ///
343    /// If it's `None`, then this variant is either:
344    /// - the untagged variant (cf. [`TagEncoding::Niche::untagged_variant`]) of a niched enum;
345    /// - the single variant of a struct;
346    /// - uninhabited.
347    #[drive(skip)]
348    pub tag: Option<ScalarValue>,
349}
350
351/// Describes how we represent the active enum variant in memory.
352#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
353pub enum TagEncoding {
354    /// Represents the direct encoding of the discriminant as the tag via integer casts.
355    Direct,
356    /// Represents the encoding of the discriminant in the niche of variant `untagged_variant`.
357    Niche { untagged_variant: VariantId },
358}
359
360/// Layout of the discriminant.
361/// Describes the offset of the discriminant field as well as its encoding
362/// as `tag` in memory.
363#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
364pub struct DiscriminantLayout {
365    /// The offset of the discriminant in bytes.
366    pub offset: ByteCount,
367    /// The representation type of the discriminant.
368    pub tag_ty: IntegerTy,
369    /// How the tag is encoding in memory.
370    pub encoding: TagEncoding,
371    // FIXME: Should probably contain the valid range of the tag, too.
372}
373
374/// Simplified type layout information.
375///
376/// Does not include information about niches.
377/// If the type does not have a fully known layout (e.g. it is ?Sized)
378/// some of the layout parts are not available.
379#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
380pub struct Layout {
381    /// The size of the type in bytes.
382    #[drive(skip)]
383    pub size: Option<ByteCount>,
384    /// The alignment, in bytes.
385    #[drive(skip)]
386    pub align: Option<ByteCount>,
387    /// The discriminant's layout, if any. Only relevant for types with multiple variants.
388    ///
389    #[drive(skip)]
390    pub discriminant_layout: Option<DiscriminantLayout>,
391    /// Whether the type is uninhabited, i.e. has any valid value at all.
392    /// Note that uninhabited types can have arbitrary layouts: `(u32, !)` has space for the `u32`
393    /// and `enum E2 { A, B(!), C(i32, !) }` may have space for a discriminant.
394    #[drive(skip)]
395    pub uninhabited: bool,
396    /// Map from `VariantId` to the corresponding field layouts. Structs are modeled as having
397    /// exactly one variant, unions as having no variant.
398    pub variant_layouts: Vector<VariantId, VariantLayout>,
399}
400
401/// A placeholder for the vtable of a trait object.
402/// To be implemented in the future when `dyn Trait` is fully supported.
403#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
404pub struct VTable;
405
406/// The metadata stored in a pointer. That's the information stored in pointers alongside
407/// their address. It's empty for `Sized` types, and interesting for unsized
408/// aka dynamically-sized types.
409#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
410pub enum PtrMetadata {
411    /// Types that need no metadata, namely `T: Sized` types.
412    #[charon::rename("NoMetadata")]
413    None,
414    /// Metadata for `[T]`, `str`, and user-defined types
415    /// that directly or indirectly contain one of these two.
416    Length,
417    /// Metadata for `dyn Trait` and user-defined types
418    /// that directly or indirectly contain a `dyn Trait`.
419    VTable(VTable),
420}
421
422/// A type declaration.
423///
424/// Types can be opaque or transparent.
425///
426/// Transparent types are local types not marked as opaque.
427/// Opaque types are the others: local types marked as opaque, and non-local
428/// types (coming from external dependencies).
429///
430/// In case the type is transparent, the declaration also contains the
431/// type definition (see [TypeDeclKind]).
432///
433/// A type can only be an ADT (structure or enumeration), as type aliases are
434/// inlined in MIR.
435#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
436pub struct TypeDecl {
437    #[drive(skip)]
438    pub def_id: TypeDeclId,
439    /// Meta information associated with the item.
440    pub item_meta: ItemMeta,
441    pub generics: GenericParams,
442    /// The type kind: enum, struct, or opaque.
443    pub kind: TypeDeclKind,
444    /// The layout of the type. Information may be partial because of generics or dynamically-
445    /// sized types. If rustc cannot compute a layout, it is `None`.
446    pub layout: Option<Layout>,
447    /// The metadata associated with a pointer to the type.
448    /// This is `None` if we could not compute it because of generics.
449    /// The information is *accurate* if it is `Some`
450    ///     while if it is `None`, it may still be theoretically computable
451    ///     but due to some limitation to be fixed, we are unable to obtain the info.
452    /// See `translate_types::{impl ItemTransCtx}::translate_ptr_metadata` for more details.
453    pub ptr_metadata: Option<PtrMetadata>,
454}
455
456generate_index_type!(VariantId, "Variant");
457generate_index_type!(FieldId, "Field");
458
459#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)]
460pub enum TypeDeclKind {
461    Struct(Vector<FieldId, Field>),
462    Enum(Vector<VariantId, Variant>),
463    Union(Vector<FieldId, Field>),
464    /// An opaque type.
465    ///
466    /// Either a local type marked as opaque, or an external type.
467    Opaque,
468    /// An alias to another type. This only shows up in the top-level list of items, as rustc
469    /// inlines uses of type aliases everywhere else.
470    Alias(Ty),
471    /// Used if an error happened during the extraction, and we don't panic
472    /// on error.
473    #[charon::rename("TDeclError")]
474    #[drive(skip)]
475    Error(String),
476}
477
478#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
479pub struct Variant {
480    pub span: Span,
481    #[drive(skip)]
482    pub attr_info: AttrInfo,
483    #[charon::rename("variant_name")]
484    #[drive(skip)]
485    pub name: String,
486    pub fields: Vector<FieldId, Field>,
487    /// The discriminant value outputted by `std::mem::discriminant` for this variant. This is
488    /// different than the discriminant stored in memory (the one controlled by `repr`).
489    /// That one is described by [`DiscriminantLayout`] and [`TagEncoding`].
490    pub discriminant: ScalarValue,
491}
492
493#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
494pub struct Field {
495    pub span: Span,
496    #[drive(skip)]
497    pub attr_info: AttrInfo,
498    #[charon::rename("field_name")]
499    #[drive(skip)]
500    pub name: Option<String>,
501    #[charon::rename("field_ty")]
502    pub ty: Ty,
503}
504
505#[derive(
506    Debug,
507    PartialEq,
508    Eq,
509    Copy,
510    Clone,
511    EnumIsA,
512    VariantName,
513    Serialize,
514    Deserialize,
515    Drive,
516    DriveMut,
517    Hash,
518    Ord,
519    PartialOrd,
520)]
521#[charon::rename("IntegerType")]
522pub enum IntegerTy {
523    Isize,
524    I8,
525    I16,
526    I32,
527    I64,
528    I128,
529    Usize,
530    U8,
531    U16,
532    U32,
533    U64,
534    U128,
535}
536
537#[derive(
538    Debug,
539    PartialEq,
540    Eq,
541    Copy,
542    Clone,
543    EnumIsA,
544    VariantName,
545    Serialize,
546    Deserialize,
547    Drive,
548    DriveMut,
549    Hash,
550    Ord,
551    PartialOrd,
552)]
553#[charon::rename("FloatType")]
554pub enum FloatTy {
555    F16,
556    F32,
557    F64,
558    F128,
559}
560
561#[derive(
562    Debug,
563    PartialEq,
564    Eq,
565    Clone,
566    Copy,
567    Hash,
568    VariantName,
569    EnumIsA,
570    Serialize,
571    Deserialize,
572    Drive,
573    DriveMut,
574    Ord,
575    PartialOrd,
576)]
577#[charon::variants_prefix("R")]
578pub enum RefKind {
579    Mut,
580    Shared,
581}
582
583/// Type identifier.
584///
585/// Allows us to factorize the code for built-in types, adts and tuples
586#[derive(
587    Debug,
588    PartialEq,
589    Eq,
590    Clone,
591    Copy,
592    VariantName,
593    EnumAsGetters,
594    EnumIsA,
595    Serialize,
596    Deserialize,
597    Drive,
598    DriveMut,
599    Hash,
600    Ord,
601    PartialOrd,
602)]
603#[charon::variants_prefix("T")]
604pub enum TypeId {
605    /// A "regular" ADT type.
606    ///
607    /// Includes transparent ADTs and opaque ADTs (local ADTs marked as opaque,
608    /// and external ADTs).
609    #[charon::rename("TAdtId")]
610    Adt(TypeDeclId),
611    Tuple,
612    /// Built-in type. Either a primitive type like array or slice, or a
613    /// non-primitive type coming from a standard library
614    /// and that we handle like a primitive type. Types falling into this
615    /// category include: Box, Vec, Cell...
616    /// The Array and Slice types were initially modelled as primitive in
617    /// the [Ty] type. We decided to move them to built-in types as it allows
618    /// for more uniform treatment throughout the codebase.
619    #[charon::rename("TBuiltin")]
620    Builtin(BuiltinTy),
621}
622
623/// Reference to a type declaration or builtin type.
624#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
625pub struct TypeDeclRef {
626    pub id: TypeId,
627    pub generics: BoxedArgs,
628}
629
630/// Types of primitive values. Either an integer, bool, char
631#[derive(
632    Debug,
633    PartialEq,
634    Eq,
635    Clone,
636    Copy,
637    VariantName,
638    EnumIsA,
639    EnumAsGetters,
640    VariantIndexArity,
641    Serialize,
642    Deserialize,
643    Drive,
644    DriveMut,
645    Hash,
646    Ord,
647    PartialOrd,
648)]
649#[charon::rename("LiteralType")]
650#[charon::variants_prefix("T")]
651pub enum LiteralTy {
652    Integer(IntegerTy),
653    Float(FloatTy),
654    Bool,
655    Char,
656}
657
658/// Const Generic Values. Either a primitive value, or a variable corresponding to a primitve value
659#[derive(
660    Debug,
661    PartialEq,
662    Eq,
663    Clone,
664    VariantName,
665    EnumIsA,
666    EnumAsGetters,
667    VariantIndexArity,
668    Serialize,
669    Deserialize,
670    Drive,
671    DriveMut,
672    Hash,
673)]
674#[charon::variants_prefix("Cg")]
675pub enum ConstGeneric {
676    /// A global constant
677    Global(GlobalDeclId),
678    /// A const generic variable
679    Var(ConstGenericDbVar),
680    /// A concrete value
681    Value(Literal),
682}
683
684/// A type.
685///
686/// Warning: the `DriveMut` impls of `Ty` needs to clone and re-hash the modified type to maintain
687/// the hash-consing invariant. This is expensive, avoid visiting types mutably when not needed.
688#[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize)]
689pub struct Ty(HashConsed<TyKind>);
690
691impl Ty {
692    pub fn new(kind: TyKind) -> Self {
693        Ty(HashConsed::new(kind))
694    }
695
696    pub fn kind(&self) -> &TyKind {
697        self.0.inner()
698    }
699
700    pub fn with_kind_mut<R>(&mut self, f: impl FnOnce(&mut TyKind) -> R) -> R {
701        self.0.with_inner_mut(f)
702    }
703}
704
705impl<'s, V: Visit<'s, TyKind>> Drive<'s, V> for Ty {
706    fn drive_inner(&'s self, v: &mut V) -> std::ops::ControlFlow<V::Break> {
707        self.0.drive_inner(v)
708    }
709}
710/// This explores the type mutably by cloning and re-hashing afterwards.
711impl<'s, V> DriveMut<'s, V> for Ty
712where
713    for<'a> V: VisitMut<'a, TyKind>,
714{
715    fn drive_inner_mut(&'s mut self, v: &mut V) -> std::ops::ControlFlow<V::Break> {
716        self.0.drive_inner_mut(v)
717    }
718}
719
720#[derive(
721    Debug,
722    Clone,
723    PartialEq,
724    Eq,
725    Hash,
726    VariantName,
727    EnumIsA,
728    EnumAsGetters,
729    EnumToGetters,
730    VariantIndexArity,
731    Serialize,
732    Deserialize,
733    Drive,
734    DriveMut,
735)]
736#[charon::variants_prefix("T")]
737#[charon::rename("Ty")]
738pub enum TyKind {
739    /// An ADT.
740    /// Note that here ADTs are very general. They can be:
741    /// - user-defined ADTs
742    /// - tuples (including `unit`, which is a 0-tuple)
743    /// - built-in types (includes some primitive types, e.g., arrays or slices)
744    /// The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
745    /// The last list is used encode const generics, e.g., the size of an array
746    ///
747    /// Note: this is incorrectly named: this can refer to any valid `TypeDecl` including extern
748    /// types.
749    Adt(TypeDeclRef),
750    #[charon::rename("TVar")]
751    TypeVar(TypeDbVar),
752    Literal(LiteralTy),
753    /// The never type, for computations which don't return. It is sometimes
754    /// necessary for intermediate variables. For instance, if we do (coming
755    /// from the rust documentation):
756    /// ```text
757    /// let num: u32 = match get_a_number() {
758    ///     Some(num) => num,
759    ///     None => break,
760    /// };
761    /// ```
762    /// the second branch will have type `Never`. Also note that `Never`
763    /// can be coerced to any type.
764    ///
765    /// Note that we eliminate the variables which have this type in a micro-pass.
766    /// As statements don't have types, this type disappears eventually disappears
767    /// from the AST.
768    Never,
769    // We don't support floating point numbers on purpose (for now)
770    /// A borrow
771    Ref(Region, Ty, RefKind),
772    /// A raw pointer.
773    RawPtr(Ty, RefKind),
774    /// A trait associated type
775    ///
776    /// Ex.:
777    /// ```text
778    /// trait Foo {
779    ///   type Bar; // type associated to the trait Foo
780    /// }
781    /// ```
782    TraitType(TraitRef, TraitItemName),
783    /// `dyn Trait`
784    ///
785    /// This carries an existentially quantified list of predicates, e.g. `exists<T> where T:
786    /// Into<u64>`. The predicate must quantify over a single type and no any regions or constants.
787    ///
788    /// TODO: we don't translate this properly yet.
789    DynTrait(ExistentialPredicate),
790    /// Function pointer type. This is a literal pointer to a region of memory that
791    /// contains a callable function.
792    /// This is a function signature with limited generics: it only supports lifetime generics, not
793    /// other kinds of generics.
794    FnPtr(RegionBinder<(Vec<Ty>, Ty)>),
795    /// The unique type associated with each function item. Each function item is given
796    /// a unique generic type that takes as input the function's early-bound generics. This type
797    /// is not generally nameable in Rust; it's a ZST (there's a unique value), and a value of that type
798    /// can be cast to a function pointer or passed to functions that expect `FnOnce`/`FnMut`/`Fn` parameters.
799    /// There's a binder here because charon function items take both early and late-bound
800    /// lifetimes as arguments; given that the type here is polymorpohic in the late-bound
801    /// variables (those that could appear in a function pointer type like `for<'a> fn(&'a u32)`),
802    /// we need to bind them here.
803    FnDef(RegionBinder<FunDeclRef>),
804    /// A type that could not be computed or was incorrect.
805    #[drive(skip)]
806    Error(String),
807}
808
809/// Builtin types identifiers.
810///
811/// WARNING: for now, all the built-in types are covariant in the generic
812/// parameters (if there are). Adding types which don't satisfy this
813/// will require to update the code abstracting the signatures (to properly
814/// take into account the lifetime constraints).
815///
816/// TODO: update to not hardcode the types (except `Box` maybe) and be more
817/// modular.
818/// TODO: move to builtins.rs?
819#[derive(
820    Debug,
821    PartialEq,
822    Eq,
823    Clone,
824    Copy,
825    EnumIsA,
826    EnumAsGetters,
827    VariantName,
828    Serialize,
829    Deserialize,
830    Drive,
831    DriveMut,
832    Hash,
833    Ord,
834    PartialOrd,
835)]
836#[charon::variants_prefix("T")]
837pub enum BuiltinTy {
838    /// Boxes are de facto a primitive type.
839    Box,
840    /// Primitive type
841    Array,
842    /// Primitive type
843    Slice,
844    /// Primitive type
845    Str,
846}
847
848#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
849pub enum ClosureKind {
850    Fn,
851    FnMut,
852    FnOnce,
853}
854
855impl ClosureKind {
856    // pub fn trait_name(self) -> &'static str {}
857    pub fn method_name(self) -> &'static str {
858        match self {
859            ClosureKind::FnOnce => "call_once",
860            ClosureKind::FnMut => "call_mut",
861            ClosureKind::Fn => "call",
862        }
863    }
864}
865
866/// Additional information for closures.
867#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
868pub struct ClosureInfo {
869    pub kind: ClosureKind,
870    /// The signature of the function that this closure represents.
871    pub signature: RegionBinder<(Vec<Ty>, Ty)>,
872}
873
874/// A function signature.
875#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
876pub struct FunSig {
877    /// Is the function unsafe or not
878    #[drive(skip)]
879    pub is_unsafe: bool,
880    pub generics: GenericParams,
881    pub inputs: Vec<Ty>,
882    pub output: Ty,
883}