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

charon_lib/ast/
types.rs
