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(TraitImplRef),
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 pub id: TraitDeclId,
165 pub generics: BoxedArgs,
166}
167
168/// A quantified trait predicate, e.g. `for<'a> Type<'a>: Trait<'a, Args>`.
169pub type PolyTraitDeclRef = RegionBinder<TraitDeclRef>;
170
171/// A reference to a tait impl, using the provided arguments.
172#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
173pub struct TraitImplRef {
174 pub id: TraitImplId,
175 pub generics: BoxedArgs,
176}
177
178/// .0 outlives .1
179#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
180pub struct OutlivesPred<T, U>(pub T, pub U);
181
182pub type RegionOutlives = OutlivesPred<Region, Region>;
183pub type TypeOutlives = OutlivesPred<Ty, Region>;
184
185/// A constraint over a trait associated type.
186///
187/// Example:
188/// ```text
189/// T : Foo<S = String>
190/// ^^^^^^^^^^
191/// ```
192#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
193pub struct TraitTypeConstraint {
194 pub trait_ref: TraitRef,
195 pub type_name: TraitItemName,
196 pub ty: Ty,
197}
198
199/// A set of generic arguments.
200#[derive(Clone, Eq, PartialEq, Hash, Serialize, Deserialize, Drive, DriveMut)]
201pub struct GenericArgs {
202 pub regions: Vector<RegionId, Region>,
203 pub types: Vector<TypeVarId, Ty>,
204 pub const_generics: Vector<ConstGenericVarId, ConstGeneric>,
205 // TODO: rename to match [GenericParams]?
206 pub trait_refs: Vector<TraitClauseId, TraitRef>,
207}
208
209pub type BoxedArgs = Box<GenericArgs>;
210
211/// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash
212/// issues in the derived ocaml visitors.
213/// TODO: merge with `binder`
214#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
215pub struct RegionBinder<T> {
216 #[charon::rename("binder_regions")]
217 pub regions: Vector<RegionId, RegionVar>,
218 /// Named this way to highlight accesses to the inner value that might be handling parameters
219 /// incorrectly. Prefer using helper methods.
220 #[charon::rename("binder_value")]
221 pub skip_binder: T,
222}
223
224#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
225#[charon::variants_prefix("BK")]
226pub enum BinderKind {
227 /// The parameters of a trait method. Used in the `methods` lists in trait decls and trait
228 /// impls.
229 TraitMethod(TraitDeclId, TraitItemName),
230 /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods.
231 InherentImplBlock,
232 /// Some other use of a binder outside the main Charon ast.
233 Other,
234}
235
236/// A value of type `T` bound by generic parameters. Used in any context where we're adding generic
237/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for
238/// now), trait methods, GATs (TODO).
239#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
240pub struct Binder<T> {
241 #[charon::rename("binder_params")]
242 pub params: GenericParams,
243 /// Named this way to highlight accesses to the inner value that might be handling parameters
244 /// incorrectly. Prefer using helper methods.
245 #[charon::rename("binder_value")]
246 pub skip_binder: T,
247 /// The kind of binder this is.
248 #[charon::opaque]
249 #[drive(skip)]
250 pub kind: BinderKind,
251}
252
253/// Generic parameters for a declaration.
254/// We group the generics which come from the Rust compiler substitutions
255/// (the regions, types and const generics) as well as the trait clauses.
256/// The reason is that we consider that those are parameters that need to
257/// be filled. We group in a different place the predicates which are not
258/// trait clauses, because those enforce constraints but do not need to
259/// be filled with witnesses/instances.
260#[derive(Default, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
261pub struct GenericParams {
262 pub regions: Vector<RegionId, RegionVar>,
263 pub types: Vector<TypeVarId, TypeVar>,
264 pub const_generics: Vector<ConstGenericVarId, ConstGenericVar>,
265 // TODO: rename to match [GenericArgs]?
266 pub trait_clauses: Vector<TraitClauseId, TraitClause>,
267 /// The first region in the pair outlives the second region
268 pub regions_outlive: Vec<RegionBinder<RegionOutlives>>,
269 /// The type outlives the region
270 pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
271 /// Constraints over trait associated types
272 pub trait_type_constraints: Vector<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
273}
274
275/// A predicate of the form `exists<T> where T: Trait`.
276///
277/// TODO: store something useful here
278#[derive(Debug, Default, Clone, Hash, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
279pub struct ExistentialPredicate;
280
281/// Where a given predicate came from.
282#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
283pub enum PredicateOrigin {
284 // Note: we use this for globals too, but that's only available with an unstable feature.
285 // ```
286 // fn function<T: Clone>() {}
287 // fn function<T>() where T: Clone {}
288 // const NONE<T: Copy>: Option<T> = None;
289 // ```
290 WhereClauseOnFn,
291 // ```
292 // struct Struct<T: Clone> {}
293 // struct Struct<T> where T: Clone {}
294 // type TypeAlias<T: Clone> = ...;
295 // ```
296 WhereClauseOnType,
297 // Note: this is both trait impls and inherent impl blocks.
298 // ```
299 // impl<T: Clone> Type<T> {}
300 // impl<T> Type<T> where T: Clone {}
301 // impl<T> Trait for Type<T> where T: Clone {}
302 // ```
303 WhereClauseOnImpl,
304 // The special `Self: Trait` clause which is in scope inside the definition of `Foo` or an
305 // implementation of it.
306 // ```
307 // trait Trait {}
308 // ```
309 TraitSelf,
310 // Note: this also includes supertrait constraints.
311 // ```
312 // trait Trait<T: Clone> {}
313 // trait Trait<T> where T: Clone {}
314 // trait Trait: Clone {}
315 // ```
316 WhereClauseOnTrait,
317 // ```
318 // trait Trait {
319 // type AssocType: Clone;
320 // }
321 // ```
322 TraitItem(TraitItemName),
323}
324
325// rustc counts bytes in layouts as u64
326type ByteCount = u64;
327
328/// Simplified layout of a single variant.
329///
330/// Maps fields to their offset within the layout.
331#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
332pub struct VariantLayout {
333 /// The offset of each field.
334 #[drive(skip)]
335 pub field_offsets: Vector<FieldId, ByteCount>,
336 /// Whether the variant is uninhabited, i.e. has any valid possible value.
337 /// Note that uninhabited types can have arbitrary layouts.
338 #[drive(skip)]
339 pub uninhabited: bool,
340 /// The memory representation of the discriminant corresponding to this
341 /// variant. It must be of the same type as the corresponding [`DiscriminantLayout::tag_ty`].
342 ///
343 /// If it's `None`, then this variant is either:
344 /// - the untagged variant (cf. [`TagEncoding::Niche::untagged_variant`]) of a niched enum;
345 /// - the single variant of a struct;
346 /// - uninhabited.
347 #[drive(skip)]
348 pub tag: Option<ScalarValue>,
349}
350
351/// Describes how we represent the active enum variant in memory.
352#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
353pub enum TagEncoding {
354 /// Represents the direct encoding of the discriminant as the tag via integer casts.
355 Direct,
356 /// Represents the encoding of the discriminant in the niche of variant `untagged_variant`.
357 Niche { untagged_variant: VariantId },
358}
359
360/// Layout of the discriminant.
361/// Describes the offset of the discriminant field as well as its encoding
362/// as `tag` in memory.
363#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
364pub struct DiscriminantLayout {
365 /// The offset of the discriminant in bytes.
366 pub offset: ByteCount,
367 /// The representation type of the discriminant.
368 pub tag_ty: IntegerTy,
369 /// How the tag is encoding in memory.
370 pub encoding: TagEncoding,
371 // FIXME: Should probably contain the valid range of the tag, too.
372}
373
374/// Simplified type layout information.
375///
376/// Does not include information about niches.
377/// If the type does not have a fully known layout (e.g. it is ?Sized)
378/// some of the layout parts are not available.
379#[derive(Debug, Default, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
380pub struct Layout {
381 /// The size of the type in bytes.
382 #[drive(skip)]
383 pub size: Option<ByteCount>,
384 /// The alignment, in bytes.
385 #[drive(skip)]
386 pub align: Option<ByteCount>,
387 /// The discriminant's layout, if any. Only relevant for types with multiple variants.
388 ///
389 #[drive(skip)]
390 pub discriminant_layout: Option<DiscriminantLayout>,
391 /// Whether the type is uninhabited, i.e. has any valid value at all.
392 /// Note that uninhabited types can have arbitrary layouts: `(u32, !)` has space for the `u32`
393 /// and `enum E2 { A, B(!), C(i32, !) }` may have space for a discriminant.
394 #[drive(skip)]
395 pub uninhabited: bool,
396 /// Map from `VariantId` to the corresponding field layouts. Structs are modeled as having
397 /// exactly one variant, unions as having no variant.
398 pub variant_layouts: Vector<VariantId, VariantLayout>,
399}
400
401/// A placeholder for the vtable of a trait object.
402/// To be implemented in the future when `dyn Trait` is fully supported.
403#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
404pub struct VTable;
405
406/// The metadata stored in a pointer. That's the information stored in pointers alongside
407/// their address. It's empty for `Sized` types, and interesting for unsized
408/// aka dynamically-sized types.
409#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
410pub enum PtrMetadata {
411 /// Types that need no metadata, namely `T: Sized` types.
412 #[charon::rename("NoMetadata")]
413 None,
414 /// Metadata for `[T]`, `str`, and user-defined types
415 /// that directly or indirectly contain one of these two.
416 Length,
417 /// Metadata for `dyn Trait` and user-defined types
418 /// that directly or indirectly contain a `dyn Trait`.
419 VTable(VTable),
420}
421
422/// A type declaration.
423///
424/// Types can be opaque or transparent.
425///
426/// Transparent types are local types not marked as opaque.
427/// Opaque types are the others: local types marked as opaque, and non-local
428/// types (coming from external dependencies).
429///
430/// In case the type is transparent, the declaration also contains the
431/// type definition (see [TypeDeclKind]).
432///
433/// A type can only be an ADT (structure or enumeration), as type aliases are
434/// inlined in MIR.
435#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
436pub struct TypeDecl {
437 #[drive(skip)]
438 pub def_id: TypeDeclId,
439 /// Meta information associated with the item.
440 pub item_meta: ItemMeta,
441 pub generics: GenericParams,
442 /// The type kind: enum, struct, or opaque.
443 pub kind: TypeDeclKind,
444 /// The layout of the type. Information may be partial because of generics or dynamically-
445 /// sized types. If rustc cannot compute a layout, it is `None`.
446 pub layout: Option<Layout>,
447 /// The metadata associated with a pointer to the type.
448 /// This is `None` if we could not compute it because of generics.
449 /// The information is *accurate* if it is `Some`
450 /// while if it is `None`, it may still be theoretically computable
451 /// but due to some limitation to be fixed, we are unable to obtain the info.
452 /// See `translate_types::{impl ItemTransCtx}::translate_ptr_metadata` for more details.
453 pub ptr_metadata: Option<PtrMetadata>,
454}
455
456generate_index_type!(VariantId, "Variant");
457generate_index_type!(FieldId, "Field");
458
459#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)]
460pub enum TypeDeclKind {
461 Struct(Vector<FieldId, Field>),
462 Enum(Vector<VariantId, Variant>),
463 Union(Vector<FieldId, Field>),
464 /// An opaque type.
465 ///
466 /// Either a local type marked as opaque, or an external type.
467 Opaque,
468 /// An alias to another type. This only shows up in the top-level list of items, as rustc
469 /// inlines uses of type aliases everywhere else.
470 Alias(Ty),
471 /// Used if an error happened during the extraction, and we don't panic
472 /// on error.
473 #[charon::rename("TDeclError")]
474 #[drive(skip)]
475 Error(String),
476}
477
478#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
479pub struct Variant {
480 pub span: Span,
481 #[drive(skip)]
482 pub attr_info: AttrInfo,
483 #[charon::rename("variant_name")]
484 #[drive(skip)]
485 pub name: String,
486 pub fields: Vector<FieldId, Field>,
487 /// The discriminant value outputted by `std::mem::discriminant` for this variant. This is
488 /// different than the discriminant stored in memory (the one controlled by `repr`).
489 /// That one is described by [`DiscriminantLayout`] and [`TagEncoding`].
490 pub discriminant: ScalarValue,
491}
492
493#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
494pub struct Field {
495 pub span: Span,
496 #[drive(skip)]
497 pub attr_info: AttrInfo,
498 #[charon::rename("field_name")]
499 #[drive(skip)]
500 pub name: Option<String>,
501 #[charon::rename("field_ty")]
502 pub ty: Ty,
503}
504
505#[derive(
506 Debug,
507 PartialEq,
508 Eq,
509 Copy,
510 Clone,
511 EnumIsA,
512 VariantName,
513 Serialize,
514 Deserialize,
515 Drive,
516 DriveMut,
517 Hash,
518 Ord,
519 PartialOrd,
520)]
521#[charon::rename("IntegerType")]
522pub enum IntegerTy {
523 Isize,
524 I8,
525 I16,
526 I32,
527 I64,
528 I128,
529 Usize,
530 U8,
531 U16,
532 U32,
533 U64,
534 U128,
535}
536
537#[derive(
538 Debug,
539 PartialEq,
540 Eq,
541 Copy,
542 Clone,
543 EnumIsA,
544 VariantName,
545 Serialize,
546 Deserialize,
547 Drive,
548 DriveMut,
549 Hash,
550 Ord,
551 PartialOrd,
552)]
553#[charon::rename("FloatType")]
554pub enum FloatTy {
555 F16,
556 F32,
557 F64,
558 F128,
559}
560
561#[derive(
562 Debug,
563 PartialEq,
564 Eq,
565 Clone,
566 Copy,
567 Hash,
568 VariantName,
569 EnumIsA,
570 Serialize,
571 Deserialize,
572 Drive,
573 DriveMut,
574 Ord,
575 PartialOrd,
576)]
577#[charon::variants_prefix("R")]
578pub enum RefKind {
579 Mut,
580 Shared,
581}
582
583/// Type identifier.
584///
585/// Allows us to factorize the code for built-in types, adts and tuples
586#[derive(
587 Debug,
588 PartialEq,
589 Eq,
590 Clone,
591 Copy,
592 VariantName,
593 EnumAsGetters,
594 EnumIsA,
595 Serialize,
596 Deserialize,
597 Drive,
598 DriveMut,
599 Hash,
600 Ord,
601 PartialOrd,
602)]
603#[charon::variants_prefix("T")]
604pub enum TypeId {
605 /// A "regular" ADT type.
606 ///
607 /// Includes transparent ADTs and opaque ADTs (local ADTs marked as opaque,
608 /// and external ADTs).
609 #[charon::rename("TAdtId")]
610 Adt(TypeDeclId),
611 Tuple,
612 /// Built-in type. Either a primitive type like array or slice, or a
613 /// non-primitive type coming from a standard library
614 /// and that we handle like a primitive type. Types falling into this
615 /// category include: Box, Vec, Cell...
616 /// The Array and Slice types were initially modelled as primitive in
617 /// the [Ty] type. We decided to move them to built-in types as it allows
618 /// for more uniform treatment throughout the codebase.
619 #[charon::rename("TBuiltin")]
620 Builtin(BuiltinTy),
621}
622
623/// Reference to a type declaration or builtin type.
624#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
625pub struct TypeDeclRef {
626 pub id: TypeId,
627 pub generics: BoxedArgs,
628}
629
630/// Types of primitive values. Either an integer, bool, char
631#[derive(
632 Debug,
633 PartialEq,
634 Eq,
635 Clone,
636 Copy,
637 VariantName,
638 EnumIsA,
639 EnumAsGetters,
640 VariantIndexArity,
641 Serialize,
642 Deserialize,
643 Drive,
644 DriveMut,
645 Hash,
646 Ord,
647 PartialOrd,
648)]
649#[charon::rename("LiteralType")]
650#[charon::variants_prefix("T")]
651pub enum LiteralTy {
652 Integer(IntegerTy),
653 Float(FloatTy),
654 Bool,
655 Char,
656}
657
658/// Const Generic Values. Either a primitive value, or a variable corresponding to a primitve value
659#[derive(
660 Debug,
661 PartialEq,
662 Eq,
663 Clone,
664 VariantName,
665 EnumIsA,
666 EnumAsGetters,
667 VariantIndexArity,
668 Serialize,
669 Deserialize,
670 Drive,
671 DriveMut,
672 Hash,
673)]
674#[charon::variants_prefix("Cg")]
675pub enum ConstGeneric {
676 /// A global constant
677 Global(GlobalDeclId),
678 /// A const generic variable
679 Var(ConstGenericDbVar),
680 /// A concrete value
681 Value(Literal),
682}
683
684/// A type.
685///
686/// Warning: the `DriveMut` impls of `Ty` needs to clone and re-hash the modified type to maintain
687/// the hash-consing invariant. This is expensive, avoid visiting types mutably when not needed.
688#[derive(Debug, Clone, Hash, PartialEq, Eq, Serialize, Deserialize)]
689pub struct Ty(HashConsed<TyKind>);
690
691impl Ty {
692 pub fn new(kind: TyKind) -> Self {
693 Ty(HashConsed::new(kind))
694 }
695
696 pub fn kind(&self) -> &TyKind {
697 self.0.inner()
698 }
699
700 pub fn with_kind_mut<R>(&mut self, f: impl FnOnce(&mut TyKind) -> R) -> R {
701 self.0.with_inner_mut(f)
702 }
703}
704
705impl<'s, V: Visit<'s, TyKind>> Drive<'s, V> for Ty {
706 fn drive_inner(&'s self, v: &mut V) -> std::ops::ControlFlow<V::Break> {
707 self.0.drive_inner(v)
708 }
709}
710/// This explores the type mutably by cloning and re-hashing afterwards.
711impl<'s, V> DriveMut<'s, V> for Ty
712where
713 for<'a> V: VisitMut<'a, TyKind>,
714{
715 fn drive_inner_mut(&'s mut self, v: &mut V) -> std::ops::ControlFlow<V::Break> {
716 self.0.drive_inner_mut(v)
717 }
718}
719
720#[derive(
721 Debug,
722 Clone,
723 PartialEq,
724 Eq,
725 Hash,
726 VariantName,
727 EnumIsA,
728 EnumAsGetters,
729 EnumToGetters,
730 VariantIndexArity,
731 Serialize,
732 Deserialize,
733 Drive,
734 DriveMut,
735)]
736#[charon::variants_prefix("T")]
737#[charon::rename("Ty")]
738pub enum TyKind {
739 /// An ADT.
740 /// Note that here ADTs are very general. They can be:
741 /// - user-defined ADTs
742 /// - tuples (including `unit`, which is a 0-tuple)
743 /// - built-in types (includes some primitive types, e.g., arrays or slices)
744 /// The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
745 /// The last list is used encode const generics, e.g., the size of an array
746 ///
747 /// Note: this is incorrectly named: this can refer to any valid `TypeDecl` including extern
748 /// types.
749 Adt(TypeDeclRef),
750 #[charon::rename("TVar")]
751 TypeVar(TypeDbVar),
752 Literal(LiteralTy),
753 /// The never type, for computations which don't return. It is sometimes
754 /// necessary for intermediate variables. For instance, if we do (coming
755 /// from the rust documentation):
756 /// ```text
757 /// let num: u32 = match get_a_number() {
758 /// Some(num) => num,
759 /// None => break,
760 /// };
761 /// ```
762 /// the second branch will have type `Never`. Also note that `Never`
763 /// can be coerced to any type.
764 ///
765 /// Note that we eliminate the variables which have this type in a micro-pass.
766 /// As statements don't have types, this type disappears eventually disappears
767 /// from the AST.
768 Never,
769 // We don't support floating point numbers on purpose (for now)
770 /// A borrow
771 Ref(Region, Ty, RefKind),
772 /// A raw pointer.
773 RawPtr(Ty, RefKind),
774 /// A trait associated type
775 ///
776 /// Ex.:
777 /// ```text
778 /// trait Foo {
779 /// type Bar; // type associated to the trait Foo
780 /// }
781 /// ```
782 TraitType(TraitRef, TraitItemName),
783 /// `dyn Trait`
784 ///
785 /// This carries an existentially quantified list of predicates, e.g. `exists<T> where T:
786 /// Into<u64>`. The predicate must quantify over a single type and no any regions or constants.
787 ///
788 /// TODO: we don't translate this properly yet.
789 DynTrait(ExistentialPredicate),
790 /// Function pointer type. This is a literal pointer to a region of memory that
791 /// contains a callable function.
792 /// This is a function signature with limited generics: it only supports lifetime generics, not
793 /// other kinds of generics.
794 FnPtr(RegionBinder<(Vec<Ty>, Ty)>),
795 /// The unique type associated with each function item. Each function item is given
796 /// a unique generic type that takes as input the function's early-bound generics. This type
797 /// is not generally nameable in Rust; it's a ZST (there's a unique value), and a value of that type
798 /// can be cast to a function pointer or passed to functions that expect `FnOnce`/`FnMut`/`Fn` parameters.
799 /// There's a binder here because charon function items take both early and late-bound
800 /// lifetimes as arguments; given that the type here is polymorpohic in the late-bound
801 /// variables (those that could appear in a function pointer type like `for<'a> fn(&'a u32)`),
802 /// we need to bind them here.
803 FnDef(RegionBinder<FunDeclRef>),
804 /// A type that could not be computed or was incorrect.
805 #[drive(skip)]
806 Error(String),
807}
808
809/// Builtin types identifiers.
810///
811/// WARNING: for now, all the built-in types are covariant in the generic
812/// parameters (if there are). Adding types which don't satisfy this
813/// will require to update the code abstracting the signatures (to properly
814/// take into account the lifetime constraints).
815///
816/// TODO: update to not hardcode the types (except `Box` maybe) and be more
817/// modular.
818/// TODO: move to builtins.rs?
819#[derive(
820 Debug,
821 PartialEq,
822 Eq,
823 Clone,
824 Copy,
825 EnumIsA,
826 EnumAsGetters,
827 VariantName,
828 Serialize,
829 Deserialize,
830 Drive,
831 DriveMut,
832 Hash,
833 Ord,
834 PartialOrd,
835)]
836#[charon::variants_prefix("T")]
837pub enum BuiltinTy {
838 /// Boxes are de facto a primitive type.
839 Box,
840 /// Primitive type
841 Array,
842 /// Primitive type
843 Slice,
844 /// Primitive type
845 Str,
846}
847
848#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
849pub enum ClosureKind {
850 Fn,
851 FnMut,
852 FnOnce,
853}
854
855impl ClosureKind {
856 // pub fn trait_name(self) -> &'static str {}
857 pub fn method_name(self) -> &'static str {
858 match self {
859 ClosureKind::FnOnce => "call_once",
860 ClosureKind::FnMut => "call_mut",
861 ClosureKind::Fn => "call",
862 }
863 }
864}
865
866/// Additional information for closures.
867#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
868pub struct ClosureInfo {
869 pub kind: ClosureKind,
870 /// The signature of the function that this closure represents.
871 pub signature: RegionBinder<(Vec<Ty>, Ty)>,
872}
873
874/// A function signature.
875#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
876pub struct FunSig {
877 /// Is the function unsafe or not
878 #[drive(skip)]
879 pub is_unsafe: bool,
880 pub generics: GenericParams,
881 pub inputs: Vec<Ty>,
882 pub output: Ty,
883}