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}