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}