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}