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 [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 traits
124    /// `Sized` or `FnMut`. 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/// A type declaration.
349///
350/// Types can be opaque or transparent.
351///
352/// Transparent types are local types not marked as opaque.
353/// Opaque types are the others: local types marked as opaque, and non-local
354/// types (coming from external dependencies).
355///
356/// In case the type is transparent, the declaration also contains the
357/// type definition (see [TypeDeclKind]).
358///
359/// A type can only be an ADT (structure or enumeration), as type aliases are
360/// inlined in MIR.
361#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
362pub struct TypeDecl {
363    #[drive(skip)]
364    pub def_id: TypeDeclId,
365    /// Meta information associated with the item.
366    pub item_meta: ItemMeta,
367    pub generics: GenericParams,
368    /// The type kind: enum, struct, or opaque.
369    pub kind: TypeDeclKind,
370}
371
372generate_index_type!(VariantId, "Variant");
373generate_index_type!(FieldId, "Field");
374
375#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)]
376pub enum TypeDeclKind {
377    Struct(Vector<FieldId, Field>),
378    Enum(Vector<VariantId, Variant>),
379    Union(Vector<FieldId, Field>),
380    /// An opaque type.
381    ///
382    /// Either a local type marked as opaque, or an external type.
383    Opaque,
384    /// An alias to another type. This only shows up in the top-level list of items, as rustc
385    /// inlines uses of type aliases everywhere else.
386    Alias(Ty),
387    /// Used if an error happened during the extraction, and we don't panic
388    /// on error.
389    #[charon::rename("TDeclError")]
390    #[drive(skip)]
391    Error(String),
392}
393
394#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
395pub struct Variant {
396    pub span: Span,
397    #[drive(skip)]
398    pub attr_info: AttrInfo,
399    #[charon::rename("variant_name")]
400    #[drive(skip)]
401    pub name: String,
402    pub fields: Vector<FieldId, Field>,
403    /// The discriminant value outputted by `std::mem::discriminant` for this variant. This is
404    /// different than the discriminant stored in memory (the one controlled by `repr`).
405    pub discriminant: ScalarValue,
406}
407
408#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
409pub struct Field {
410    pub span: Span,
411    #[drive(skip)]
412    pub attr_info: AttrInfo,
413    #[charon::rename("field_name")]
414    #[drive(skip)]
415    pub name: Option<String>,
416    #[charon::rename("field_ty")]
417    pub ty: Ty,
418}
419
420#[derive(
421    Debug,
422    PartialEq,
423    Eq,
424    Copy,
425    Clone,
426    EnumIsA,
427    VariantName,
428    Serialize,
429    Deserialize,
430    Drive,
431    DriveMut,
432    Hash,
433    Ord,
434    PartialOrd,
435)]
436#[charon::rename("IntegerType")]
437pub enum IntegerTy {
438    Isize,
439    I8,
440    I16,
441    I32,
442    I64,
443    I128,
444    Usize,
445    U8,
446    U16,
447    U32,
448    U64,
449    U128,
450}
451
452#[derive(
453    Debug,
454    PartialEq,
455    Eq,
456    Copy,
457    Clone,
458    EnumIsA,
459    VariantName,
460    Serialize,
461    Deserialize,
462    Drive,
463    DriveMut,
464    Hash,
465    Ord,
466    PartialOrd,
467)]
468#[charon::rename("FloatType")]
469pub enum FloatTy {
470    F16,
471    F32,
472    F64,
473    F128,
474}
475
476#[derive(
477    Debug,
478    PartialEq,
479    Eq,
480    Clone,
481    Copy,
482    Hash,
483    VariantName,
484    EnumIsA,
485    Serialize,
486    Deserialize,
487    Drive,
488    DriveMut,
489    Ord,
490    PartialOrd,
491)]
492#[charon::variants_prefix("R")]
493pub enum RefKind {
494    Mut,
495    Shared,
496}
497
498/// Type identifier.
499///
500/// Allows us to factorize the code for built-in types, adts and tuples
501#[derive(
502    Debug,
503    PartialEq,
504    Eq,
505    Clone,
506    Copy,
507    VariantName,
508    EnumAsGetters,
509    EnumIsA,
510    Serialize,
511    Deserialize,
512    Drive,
513    DriveMut,
514    Hash,
515    Ord,
516    PartialOrd,
517)]
518#[charon::variants_prefix("T")]
519pub enum TypeId {
520    /// A "regular" ADT type.
521    ///
522    /// Includes transparent ADTs and opaque ADTs (local ADTs marked as opaque,
523    /// and external ADTs).
524    #[charon::rename("TAdtId")]
525    Adt(TypeDeclId),
526    Tuple,
527    /// Built-in type. Either a primitive type like array or slice, or a
528    /// non-primitive type coming from a standard library
529    /// and that we handle like a primitive type. Types falling into this
530    /// category include: Box, Vec, Cell...
531    /// The Array and Slice types were initially modelled as primitive in
532    /// the [Ty] type. We decided to move them to built-in types as it allows
533    /// for more uniform treatment throughout the codebase.
534    #[charon::rename("TBuiltin")]
535    Builtin(BuiltinTy),
536}
537
538/// Types of primitive values. Either an integer, bool, char
539#[derive(
540    Debug,
541    PartialEq,
542    Eq,
543    Clone,
544    Copy,
545    VariantName,
546    EnumIsA,
547    EnumAsGetters,
548    VariantIndexArity,
549    Serialize,
550    Deserialize,
551    Drive,
552    DriveMut,
553    Hash,
554    Ord,
555    PartialOrd,
556)]
557#[charon::rename("LiteralType")]
558#[charon::variants_prefix("T")]
559pub enum LiteralTy {
560    Integer(IntegerTy),
561    Float(FloatTy),
562    Bool,
563    Char,
564}
565
566/// Const Generic Values. Either a primitive value, or a variable corresponding to a primitve value
567#[derive(
568    Debug,
569    PartialEq,
570    Eq,
571    Clone,
572    VariantName,
573    EnumIsA,
574    EnumAsGetters,
575    VariantIndexArity,
576    Serialize,
577    Deserialize,
578    Drive,
579    DriveMut,
580    Hash,
581)]
582#[charon::variants_prefix("Cg")]
583pub enum ConstGeneric {
584    /// A global constant
585    Global(GlobalDeclId),
586    /// A const generic variable
587    Var(ConstGenericDbVar),
588    /// A concrete value
589    Value(Literal),
590}
591
592/// A type.
593///
594/// Warning: the `DriveMut` impls of `Ty` needs to clone and re-hash the modified type to maintain
595/// the hash-consing invariant. This is expensive, avoid visiting types mutably when not needed.
596#[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize)]
597pub struct Ty(HashConsed<TyKind>);
598
599impl Ty {
600    pub fn new(kind: TyKind) -> Self {
601        Ty(HashConsed::new(kind))
602    }
603
604    pub fn kind(&self) -> &TyKind {
605        self.0.inner()
606    }
607
608    pub fn with_kind_mut<R>(&mut self, f: impl FnOnce(&mut TyKind) -> R) -> R {
609        self.0.with_inner_mut(f)
610    }
611}
612
613impl<'s, V: Visit<'s, TyKind>> Drive<'s, V> for Ty {
614    fn drive_inner(&'s self, v: &mut V) -> std::ops::ControlFlow<V::Break> {
615        self.0.drive_inner(v)
616    }
617}
618/// This explores the type mutably by cloning and re-hashing afterwards.
619impl<'s, V> DriveMut<'s, V> for Ty
620where
621    for<'a> V: VisitMut<'a, TyKind>,
622{
623    fn drive_inner_mut(&'s mut self, v: &mut V) -> std::ops::ControlFlow<V::Break> {
624        self.0.drive_inner_mut(v)
625    }
626}
627
628#[derive(
629    Debug,
630    Clone,
631    PartialEq,
632    Eq,
633    Hash,
634    VariantName,
635    EnumIsA,
636    EnumAsGetters,
637    EnumToGetters,
638    VariantIndexArity,
639    Serialize,
640    Deserialize,
641    Drive,
642    DriveMut,
643)]
644#[charon::variants_prefix("T")]
645#[charon::rename("Ty")]
646pub enum TyKind {
647    /// An ADT.
648    /// Note that here ADTs are very general. They can be:
649    /// - user-defined ADTs
650    /// - tuples (including `unit`, which is a 0-tuple)
651    /// - built-in types (includes some primitive types, e.g., arrays or slices)
652    /// The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
653    /// The last list is used encode const generics, e.g., the size of an array
654    ///
655    /// Note: this is incorrectly named: this can refer to any valid `TypeDecl` including extern
656    /// types.
657    Adt(TypeId, GenericArgs),
658    /// A closure type, which is essentially a struct with builtin impls. Currently we don't
659    /// translate the struct itself, only the function item that contains the closure's code.
660    Closure {
661        /// The FunDecl item containing the code of the closure. That function takes the closure
662        /// state as its first argument.
663        fun_id: FunDeclId,
664        /// Generics that apply to the parent of this closure.
665        /// Warning: hax may not handle nexted closure correctly yet.
666        parent_args: BoxedArgs,
667        /// The types of the variables captured by this closure.
668        upvar_tys: Vec<Ty>,
669        /// The signature of the function that this closure represents.
670        signature: RegionBinder<(Vec<Ty>, Ty)>,
671    },
672    #[charon::rename("TVar")]
673    TypeVar(TypeDbVar),
674    Literal(LiteralTy),
675    /// The never type, for computations which don't return. It is sometimes
676    /// necessary for intermediate variables. For instance, if we do (coming
677    /// from the rust documentation):
678    /// ```text
679    /// let num: u32 = match get_a_number() {
680    ///     Some(num) => num,
681    ///     None => break,
682    /// };
683    /// ```
684    /// the second branch will have type `Never`. Also note that `Never`
685    /// can be coerced to any type.
686    ///
687    /// Note that we eliminate the variables which have this type in a micro-pass.
688    /// As statements don't have types, this type disappears eventually disappears
689    /// from the AST.
690    Never,
691    // We don't support floating point numbers on purpose (for now)
692    /// A borrow
693    Ref(Region, Ty, RefKind),
694    /// A raw pointer.
695    RawPtr(Ty, RefKind),
696    /// A trait associated type
697    ///
698    /// Ex.:
699    /// ```text
700    /// trait Foo {
701    ///   type Bar; // type associated to the trait Foo
702    /// }
703    /// ```
704    TraitType(TraitRef, TraitItemName),
705    /// `dyn Trait`
706    ///
707    /// This carries an existentially quantified list of predicates, e.g. `exists<T> where T:
708    /// Into<u64>`. The predicate must quantify over a single type and no any regions or constants.
709    ///
710    /// TODO: we don't translate this properly yet.
711    DynTrait(ExistentialPredicate),
712    /// Arrow type, used for function pointers and reused for the unique type associated with each
713    /// function item.
714    /// This is a function signature with limited generics: it only supports lifetime generics, not
715    /// other kinds of
716    /// generics.
717    Arrow(RegionBinder<(Vec<Ty>, Ty)>),
718    /// A type that could not be computed or was incorrect.
719    #[drive(skip)]
720    Error(String),
721}
722
723/// Builtin types identifiers.
724///
725/// WARNING: for now, all the built-in types are covariant in the generic
726/// parameters (if there are). Adding types which don't satisfy this
727/// will require to update the code abstracting the signatures (to properly
728/// take into account the lifetime constraints).
729///
730/// TODO: update to not hardcode the types (except `Box` maybe) and be more
731/// modular.
732/// TODO: move to builtins.rs?
733#[derive(
734    Debug,
735    PartialEq,
736    Eq,
737    Clone,
738    Copy,
739    EnumIsA,
740    EnumAsGetters,
741    VariantName,
742    Serialize,
743    Deserialize,
744    Drive,
745    DriveMut,
746    Hash,
747    Ord,
748    PartialOrd,
749)]
750#[charon::variants_prefix("T")]
751pub enum BuiltinTy {
752    /// Boxes are de facto a primitive type.
753    Box,
754    /// Primitive type
755    Array,
756    /// Primitive type
757    Slice,
758    /// Primitive type
759    Str,
760}
761
762#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
763pub enum ClosureKind {
764    Fn,
765    FnMut,
766    FnOnce,
767}
768
769/// Additional information for closures.
770/// We mostly use it in micro-passes like [crate::update_closure_signature].
771#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
772pub struct ClosureInfo {
773    pub kind: ClosureKind,
774    /// Contains the types of the fields in the closure state.
775    /// More precisely, for every place captured by the
776    /// closure, the state has one field (typically a ref).
777    ///
778    /// For instance, below the closure has a state with two fields of type `&u32`:
779    /// ```text
780    /// pub fn test_closure_capture(x: u32, y: u32) -> u32 {
781    ///   let f = &|z| x + y + z;
782    ///   (f)(0)
783    /// }
784    /// ```
785    pub state: Vector<TypeVarId, Ty>,
786}
787
788/// A function signature.
789#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
790pub struct FunSig {
791    /// Is the function unsafe or not
792    #[drive(skip)]
793    pub is_unsafe: bool,
794    /// `true` if the signature is for a closure.
795    ///
796    /// Importantly: if the signature is for a closure, then:
797    /// - the type and const generic params actually come from the parent function
798    ///   (the function in which the closure is defined)
799    /// - the region variables are local to the closure
800    #[drive(skip)]
801    pub is_closure: bool,
802    /// Additional information if this is the signature of a closure.
803    pub closure_info: Option<ClosureInfo>,
804    pub generics: GenericParams,
805    pub inputs: Vec<Ty>,
806    pub output: Ty,
807}