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, GenericArgs),
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: GenericArgs,
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: GenericArgs,
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
232/// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash
233/// issues in the derived ocaml visitors.
234/// TODO: merge with `binder`
235#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
236pub struct RegionBinder<T> {
237    #[charon::rename("binder_regions")]
238    pub regions: Vector<RegionId, RegionVar>,
239    /// Named this way to highlight accesses to the inner value that might be handling parameters
240    /// incorrectly. Prefer using helper methods.
241    #[charon::rename("binder_value")]
242    pub skip_binder: T,
243}
244
245#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
246#[charon::variants_prefix("BK")]
247pub enum BinderKind {
248    /// The parameters of a trait method. Used in the `methods` lists in trait decls and trait
249    /// impls.
250    TraitMethod(TraitDeclId, TraitItemName),
251    /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods.
252    InherentImplBlock,
253    /// Some other use of a binder outside the main Charon ast.
254    Other,
255}
256
257/// A value of type `T` bound by generic parameters. Used in any context where we're adding generic
258/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for
259/// now), trait methods, GATs (TODO).
260#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
261pub struct Binder<T> {
262    #[charon::rename("binder_params")]
263    pub params: GenericParams,
264    /// Named this way to highlight accesses to the inner value that might be handling parameters
265    /// incorrectly. Prefer using helper methods.
266    #[charon::rename("binder_value")]
267    pub skip_binder: T,
268    /// The kind of binder this is.
269    #[charon::opaque]
270    #[drive(skip)]
271    pub kind: BinderKind,
272}
273
274/// Generic parameters for a declaration.
275/// We group the generics which come from the Rust compiler substitutions
276/// (the regions, types and const generics) as well as the trait clauses.
277/// The reason is that we consider that those are parameters that need to
278/// be filled. We group in a different place the predicates which are not
279/// trait clauses, because those enforce constraints but do not need to
280/// be filled with witnesses/instances.
281#[derive(Default, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
282pub struct GenericParams {
283    pub regions: Vector<RegionId, RegionVar>,
284    pub types: Vector<TypeVarId, TypeVar>,
285    pub const_generics: Vector<ConstGenericVarId, ConstGenericVar>,
286    // TODO: rename to match [GenericArgs]?
287    pub trait_clauses: Vector<TraitClauseId, TraitClause>,
288    /// The first region in the pair outlives the second region
289    pub regions_outlive: Vec<RegionBinder<RegionOutlives>>,
290    /// The type outlives the region
291    pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
292    /// Constraints over trait associated types
293    pub trait_type_constraints: Vector<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
294}
295
296/// A predicate of the form `exists<T> where T: Trait`.
297///
298/// TODO: store something useful here
299#[derive(Debug, Default, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
300pub struct ExistentialPredicate;
301
302/// Where a given predicate came from.
303#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
304pub enum PredicateOrigin {
305    // Note: we use this for globals too, but that's only available with an unstable feature.
306    // ```
307    // fn function<T: Clone>() {}
308    // fn function<T>() where T: Clone {}
309    // const NONE<T: Copy>: Option<T> = None;
310    // ```
311    WhereClauseOnFn,
312    // ```
313    // struct Struct<T: Clone> {}
314    // struct Struct<T> where T: Clone {}
315    // type TypeAlias<T: Clone> = ...;
316    // ```
317    WhereClauseOnType,
318    // Note: this is both trait impls and inherent impl blocks.
319    // ```
320    // impl<T: Clone> Type<T> {}
321    // impl<T> Type<T> where T: Clone {}
322    // impl<T> Trait for Type<T> where T: Clone {}
323    // ```
324    WhereClauseOnImpl,
325    // The special `Self: Trait` clause which is in scope inside the definition of `Foo` or an
326    // implementation of it.
327    // ```
328    // trait Trait {}
329    // ```
330    TraitSelf,
331    // Note: this also includes supertrait constraints.
332    // ```
333    // trait Trait<T: Clone> {}
334    // trait Trait<T> where T: Clone {}
335    // trait Trait: Clone {}
336    // ```
337    WhereClauseOnTrait,
338    // ```
339    // trait Trait {
340    //     type AssocType: Clone;
341    // }
342    // ```
343    TraitItem(TraitItemName),
344}
345
346/// A type declaration.
347///
348/// Types can be opaque or transparent.
349///
350/// Transparent types are local types not marked as opaque.
351/// Opaque types are the others: local types marked as opaque, and non-local
352/// types (coming from external dependencies).
353///
354/// In case the type is transparent, the declaration also contains the
355/// type definition (see [TypeDeclKind]).
356///
357/// A type can only be an ADT (structure or enumeration), as type aliases are
358/// inlined in MIR.
359#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
360pub struct TypeDecl {
361    #[drive(skip)]
362    pub def_id: TypeDeclId,
363    /// Meta information associated with the item.
364    pub item_meta: ItemMeta,
365    pub generics: GenericParams,
366    /// The type kind: enum, struct, or opaque.
367    pub kind: TypeDeclKind,
368}
369
370generate_index_type!(VariantId, "Variant");
371generate_index_type!(FieldId, "Field");
372
373#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)]
374pub enum TypeDeclKind {
375    Struct(Vector<FieldId, Field>),
376    Enum(Vector<VariantId, Variant>),
377    Union(Vector<FieldId, Field>),
378    /// An opaque type.
379    ///
380    /// Either a local type marked as opaque, or an external type.
381    Opaque,
382    /// An alias to another type. This only shows up in the top-level list of items, as rustc
383    /// inlines uses of type aliases everywhere else.
384    Alias(Ty),
385    /// Used if an error happened during the extraction, and we don't panic
386    /// on error.
387    #[charon::rename("TDeclError")]
388    #[drive(skip)]
389    Error(String),
390}
391
392#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
393pub struct Variant {
394    pub span: Span,
395    #[drive(skip)]
396    pub attr_info: AttrInfo,
397    #[charon::rename("variant_name")]
398    #[drive(skip)]
399    pub name: String,
400    pub fields: Vector<FieldId, Field>,
401    /// The discriminant used at runtime. This is used in `remove_read_discriminant` to match up
402    /// `SwitchInt` targets with the corresponding `Variant`.
403    pub discriminant: ScalarValue,
404}
405
406#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
407pub struct Field {
408    pub span: Span,
409    #[drive(skip)]
410    pub attr_info: AttrInfo,
411    #[charon::rename("field_name")]
412    #[drive(skip)]
413    pub name: Option<String>,
414    #[charon::rename("field_ty")]
415    pub ty: Ty,
416}
417
418#[derive(
419    Debug,
420    PartialEq,
421    Eq,
422    Copy,
423    Clone,
424    EnumIsA,
425    VariantName,
426    Serialize,
427    Deserialize,
428    Drive,
429    DriveMut,
430    Hash,
431    Ord,
432    PartialOrd,
433)]
434#[charon::rename("IntegerType")]
435pub enum IntegerTy {
436    Isize,
437    I8,
438    I16,
439    I32,
440    I64,
441    I128,
442    Usize,
443    U8,
444    U16,
445    U32,
446    U64,
447    U128,
448}
449
450#[derive(
451    Debug,
452    PartialEq,
453    Eq,
454    Copy,
455    Clone,
456    EnumIsA,
457    VariantName,
458    Serialize,
459    Deserialize,
460    Drive,
461    DriveMut,
462    Hash,
463    Ord,
464    PartialOrd,
465)]
466#[charon::rename("FloatType")]
467pub enum FloatTy {
468    F16,
469    F32,
470    F64,
471    F128,
472}
473
474#[derive(
475    Debug,
476    PartialEq,
477    Eq,
478    Clone,
479    Copy,
480    Hash,
481    VariantName,
482    EnumIsA,
483    Serialize,
484    Deserialize,
485    Drive,
486    DriveMut,
487    Ord,
488    PartialOrd,
489)]
490#[charon::variants_prefix("R")]
491pub enum RefKind {
492    Mut,
493    Shared,
494}
495
496/// Type identifier.
497///
498/// Allows us to factorize the code for built-in types, adts and tuples
499#[derive(
500    Debug,
501    PartialEq,
502    Eq,
503    Clone,
504    Copy,
505    VariantName,
506    EnumAsGetters,
507    EnumIsA,
508    Serialize,
509    Deserialize,
510    Drive,
511    DriveMut,
512    Hash,
513    Ord,
514    PartialOrd,
515)]
516#[charon::variants_prefix("T")]
517pub enum TypeId {
518    /// A "regular" ADT type.
519    ///
520    /// Includes transparent ADTs and opaque ADTs (local ADTs marked as opaque,
521    /// and external ADTs).
522    #[charon::rename("TAdtId")]
523    Adt(TypeDeclId),
524    Tuple,
525    /// Built-in type. Either a primitive type like array or slice, or a
526    /// non-primitive type coming from a standard library
527    /// and that we handle like a primitive type. Types falling into this
528    /// category include: Box, Vec, Cell...
529    /// The Array and Slice types were initially modelled as primitive in
530    /// the [Ty] type. We decided to move them to built-in types as it allows
531    /// for more uniform treatment throughout the codebase.
532    #[charon::rename("TBuiltin")]
533    Builtin(BuiltinTy),
534}
535
536/// Types of primitive values. Either an integer, bool, char
537#[derive(
538    Debug,
539    PartialEq,
540    Eq,
541    Clone,
542    Copy,
543    VariantName,
544    EnumIsA,
545    EnumAsGetters,
546    VariantIndexArity,
547    Serialize,
548    Deserialize,
549    Drive,
550    DriveMut,
551    Hash,
552    Ord,
553    PartialOrd,
554)]
555#[charon::rename("LiteralType")]
556#[charon::variants_prefix("T")]
557pub enum LiteralTy {
558    Integer(IntegerTy),
559    Float(FloatTy),
560    Bool,
561    Char,
562}
563
564/// Const Generic Values. Either a primitive value, or a variable corresponding to a primitve value
565#[derive(
566    Debug,
567    PartialEq,
568    Eq,
569    Clone,
570    VariantName,
571    EnumIsA,
572    EnumAsGetters,
573    VariantIndexArity,
574    Serialize,
575    Deserialize,
576    Drive,
577    DriveMut,
578    Hash,
579)]
580#[charon::variants_prefix("Cg")]
581pub enum ConstGeneric {
582    /// A global constant
583    Global(GlobalDeclId),
584    /// A const generic variable
585    Var(ConstGenericDbVar),
586    /// A concrete value
587    Value(Literal),
588}
589
590/// A type.
591///
592/// Warning: the `DriveMut` impls of `Ty` needs to clone and re-hash the modified type to maintain
593/// the hash-consing invariant. This is expensive, avoid visiting types mutably when not needed.
594#[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize)]
595pub struct Ty(HashConsed<TyKind>);
596
597impl Ty {
598    pub fn new(kind: TyKind) -> Self {
599        Ty(HashConsed::new(kind))
600    }
601
602    pub fn kind(&self) -> &TyKind {
603        self.0.inner()
604    }
605
606    pub fn with_kind_mut<R>(&mut self, f: impl FnOnce(&mut TyKind) -> R) -> R {
607        self.0.with_inner_mut(f)
608    }
609}
610
611impl<'s, V: Visit<'s, TyKind>> Drive<'s, V> for Ty {
612    fn drive_inner(&'s self, v: &mut V) -> std::ops::ControlFlow<V::Break> {
613        self.0.drive_inner(v)
614    }
615}
616/// This explores the type mutably by cloning and re-hashing afterwards.
617impl<'s, V> DriveMut<'s, V> for Ty
618where
619    for<'a> V: VisitMut<'a, TyKind>,
620{
621    fn drive_inner_mut(&'s mut self, v: &mut V) -> std::ops::ControlFlow<V::Break> {
622        self.0.drive_inner_mut(v)
623    }
624}
625
626#[derive(
627    Debug,
628    Clone,
629    PartialEq,
630    Eq,
631    Hash,
632    VariantName,
633    EnumIsA,
634    EnumAsGetters,
635    EnumToGetters,
636    VariantIndexArity,
637    Serialize,
638    Deserialize,
639    Drive,
640    DriveMut,
641)]
642#[charon::variants_prefix("T")]
643#[charon::rename("Ty")]
644pub enum TyKind {
645    /// An ADT.
646    /// Note that here ADTs are very general. They can be:
647    /// - user-defined ADTs
648    /// - tuples (including `unit`, which is a 0-tuple)
649    /// - built-in types (includes some primitive types, e.g., arrays or slices)
650    /// The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
651    /// The last list is used encode const generics, e.g., the size of an array
652    ///
653    /// Note: this is incorrectly named: this can refer to any valid `TypeDecl` including extern
654    /// types.
655    Adt(TypeId, GenericArgs),
656    #[charon::rename("TVar")]
657    TypeVar(TypeDbVar),
658    Literal(LiteralTy),
659    /// The never type, for computations which don't return. It is sometimes
660    /// necessary for intermediate variables. For instance, if we do (coming
661    /// from the rust documentation):
662    /// ```text
663    /// let num: u32 = match get_a_number() {
664    ///     Some(num) => num,
665    ///     None => break,
666    /// };
667    /// ```
668    /// the second branch will have type `Never`. Also note that `Never`
669    /// can be coerced to any type.
670    ///
671    /// Note that we eliminate the variables which have this type in a micro-pass.
672    /// As statements don't have types, this type disappears eventually disappears
673    /// from the AST.
674    Never,
675    // We don't support floating point numbers on purpose (for now)
676    /// A borrow
677    Ref(Region, Ty, RefKind),
678    /// A raw pointer.
679    RawPtr(Ty, RefKind),
680    /// A trait associated type
681    ///
682    /// Ex.:
683    /// ```text
684    /// trait Foo {
685    ///   type Bar; // type associated to the trait Foo
686    /// }
687    /// ```
688    TraitType(TraitRef, TraitItemName),
689    /// `dyn Trait`
690    ///
691    /// This carries an existentially quantified list of predicates, e.g. `exists<T> where T:
692    /// Into<u64>`. The predicate must quantify over a single type and no any regions or constants.
693    ///
694    /// TODO: we don't translate this properly yet.
695    DynTrait(ExistentialPredicate),
696    /// Arrow type, used in particular for the local function pointers.
697    /// This is essentially a "constrained" function signature:
698    /// arrow types can only contain generic lifetime parameters
699    /// (no generic types), no predicates, etc.
700    Arrow(RegionBinder<(Vec<Ty>, Ty)>),
701    /// A type that could not be computed or was incorrect.
702    #[drive(skip)]
703    Error(String),
704}
705
706/// Builtin types identifiers.
707///
708/// WARNING: for now, all the built-in types are covariant in the generic
709/// parameters (if there are). Adding types which don't satisfy this
710/// will require to update the code abstracting the signatures (to properly
711/// take into account the lifetime constraints).
712///
713/// TODO: update to not hardcode the types (except `Box` maybe) and be more
714/// modular.
715/// TODO: move to builtins.rs?
716#[derive(
717    Debug,
718    PartialEq,
719    Eq,
720    Clone,
721    Copy,
722    EnumIsA,
723    EnumAsGetters,
724    VariantName,
725    Serialize,
726    Deserialize,
727    Drive,
728    DriveMut,
729    Hash,
730    Ord,
731    PartialOrd,
732)]
733#[charon::variants_prefix("T")]
734pub enum BuiltinTy {
735    /// Boxes are de facto a primitive type.
736    Box,
737    /// Primitive type
738    Array,
739    /// Primitive type
740    Slice,
741    /// Primitive type
742    Str,
743}
744
745#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
746pub enum ClosureKind {
747    Fn,
748    FnMut,
749    FnOnce,
750}
751
752/// Additional information for closures.
753/// We mostly use it in micro-passes like [crate::update_closure_signature].
754#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
755pub struct ClosureInfo {
756    pub kind: ClosureKind,
757    /// Contains the types of the fields in the closure state.
758    /// More precisely, for every place captured by the
759    /// closure, the state has one field (typically a ref).
760    ///
761    /// For instance, below the closure has a state with two fields of type `&u32`:
762    /// ```text
763    /// pub fn test_closure_capture(x: u32, y: u32) -> u32 {
764    ///   let f = &|z| x + y + z;
765    ///   (f)(0)
766    /// }
767    /// ```
768    pub state: Vector<TypeVarId, Ty>,
769}
770
771/// A function signature.
772#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
773pub struct FunSig {
774    /// Is the function unsafe or not
775    #[drive(skip)]
776    pub is_unsafe: bool,
777    /// `true` if the signature is for a closure.
778    ///
779    /// Importantly: if the signature is for a closure, then:
780    /// - the type and const generic params actually come from the parent function
781    ///   (the function in which the closure is defined)
782    /// - the region variables are local to the closure
783    #[drive(skip)]
784    pub is_closure: bool,
785    /// Additional information if this is the signature of a closure.
786    pub closure_info: Option<ClosureInfo>,
787    pub generics: GenericParams,
788    pub inputs: Vec<Ty>,
789    pub output: Ty,
790}