hax_rust_engine/ast/
resugared.rs

1//! This module defines *resugared fragments* for the Hax Rust engine's AST.
2//!
3//! A resugared fragment is an additional AST node used solely for pretty-printing purposes.
4//! These nodes carry no semantic meaning in hax core logic but enable more accurate
5//! or backend-specific surface syntax reconstruction.
6//!
7//! For example, the engine represents the `unit` type as a zero-sized tuple `()`,
8//! mirroring Rust's internal representation. However, this may not suit all backends:
9//! in F*, `unit` is explicitly written as `unit`, not `()`.
10//!
11//! To accommodate such differences, we introduce resugared fragments (e.g. `UnitType`) that
12//! allow the printer to emit the expected syntax while maintaining the same internal semantics.
13
14use hax_rust_engine_macros::*;
15
16use super::*;
17
18/// Resugared variants for items. This represent extra printing-only items, see [`super::ItemKind::Resugared`].
19#[derive_group_for_ast]
20pub enum ResugaredItemKind {
21    /// A `const` item, for example `const NAME: T = body;`.
22    /// The type of the constant is `body.ty`.
23    Constant {
24        /// The identifier of the constant, for example `krate::module::NAME`.
25        name: GlobalId,
26        /// The body of the constant, for example `body`.
27        body: Expr,
28        /// The generic arguments and constraints of the constant.
29        /// Note: constant supporting generics is a nightly feature (generic_const_items).
30        generics: Generics,
31    },
32}
33
34/// Resugared variants for expressions. This represent extra printing-only expressions, see [`super::ExprKind::Resugared`].
35#[derive_group_for_ast]
36// TODO: drop `clippy::large_enum_variant` when https://github.com/cryspen/hax/issues/1666 is addressed.
37#[allow(clippy::large_enum_variant)]
38pub enum ResugaredExprKind {
39    /// Binary operations (identified by resugaring) of the form `f(e1, e2)`
40    BinOp {
41        /// The identifier of the operation (`f`)
42        op: GlobalId,
43        /// The left-hand side of the operation (`e1`)
44        lhs: Expr,
45        /// The right-hand side of the operation (`e2`)
46        rhs: Expr,
47        /// The generic arguments applied to the function.
48        generic_args: Vec<GenericValue>,
49        /// If the function requires generic bounds to be called, `bounds_impls`
50        /// is a vector of impl. expressions for those bounds.
51        bounds_impls: Vec<ImplExpr>,
52        /// If we apply an associated function, contains the impl. expr used.
53        trait_: Option<(ImplExpr, Vec<GenericValue>)>,
54    },
55    /// A tuple constructor.
56    ///
57    /// # Example:
58    /// `(a, b)`
59    Tuple(Vec<Expr>),
60}
61
62/// Resugared variants for patterns. This represent extra printing-only patterns, see [`super::PatKind::Resugared`].
63#[derive_group_for_ast]
64pub enum ResugaredPatKind {}
65
66/// Resugared variants for types. This represent extra printing-only types, see [`super::TyKind::Resugared`].
67#[derive_group_for_ast]
68pub enum ResugaredTyKind {
69    /// A tuple tupe.
70    ///
71    /// # Example:
72    /// `(i32, bool)`
73    Tuple(Vec<Ty>),
74}
75
76/// Resugared variants for impl. items. This represent extra printing-only impl. items, see [`super::ImplItemKind::Resugared`].
77#[derive_group_for_ast]
78pub enum ResugaredImplItemKind {}
79
80/// Resugared variants for trait items. This represent extra printing-only trait items, see [`super::TraitItemKind::Resugared`].
81#[derive_group_for_ast]
82pub enum ResugaredTraitItemKind {}
83
84/// Marks a type as a resugar fragment of the AST.
85pub trait ResugaredFragment {
86    /// What fragment of the AST this resugar is extending?
87    type ParentFragment;
88}
89
90/// Convenience macro which implements [`ResugaredFragment`] on `$ty`, setting
91/// `$parent` as the `ParentFragment`, as well as `From<$ty>` for `$parent`, by
92/// wrapping the `$ty` in `$parent::Resugared(..)`.
93macro_rules! derive_from {
94    ($($ty:ty => $parent:ty),*) => {
95        $(impl ResugaredFragment for $ty {
96            type ParentFragment = $parent;
97        }
98        impl From<$ty> for <$ty as ResugaredFragment>::ParentFragment {
99            fn from(value: $ty) -> Self {
100                Self::Resugared(value)
101            }
102        })*
103    };
104}
105
106derive_from!(
107    ResugaredItemKind => ItemKind,
108    ResugaredExprKind => ExprKind,
109    ResugaredPatKind => PatKind,
110    ResugaredTyKind => TyKind,
111    ResugaredImplItemKind => ImplItemKind,
112    ResugaredTraitItemKind => TraitItemKind
113);
hax_rust_engine/ast/resugared.rs

hax_rust_engine/ast/
resugared.rs
