charon_lib/ast/
types.rs

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

charon_lib/ast/
types.rs
