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

charon_lib/ast/
types.rs
