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

charon_lib/ast/
types.rs
