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