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    /// A recursive function definition. Detected by checking whether the function
33    /// body contains a reference to its own name.
34    RecursiveFn {
35        /// The identifier of the function.
36        name: GlobalId,
37        /// The generic arguments and constraints of the function.
38        generics: Generics,
39        /// The body of the function.
40        body: Expr,
41        /// The parameters of the function.
42        params: Vec<Param>,
43        /// The safety of the function.
44        safety: SafetyKind,
45    },
46}
47
48/// Resugared variants for expressions. This represent extra printing-only expressions, see [`super::ExprKind::Resugared`].
49#[derive_group_for_ast]
50// TODO: drop `clippy::large_enum_variant` when https://github.com/cryspen/hax/issues/1666 is addressed.
51#[allow(clippy::large_enum_variant)]
52pub enum ResugaredExprKind {
53    /// A tuple constructor.
54    ///
55    /// # Example:
56    /// `(a, b)`
57    Tuple(Vec<Expr>),
58    /// A let-binding of a "pure" (non-panicking) expression
59    ///
60    /// # Example:
61    /// `let x = 9; x + 0`
62    LetPure {
63        /// The left-hand side of the `let` expression. (`x` in the example)
64        lhs: Pat,
65        /// The right-hand side of the `let` expression. (`9` in the example)
66        rhs: Expr,
67        /// The body of the `let`. (`x + 0` in the example)
68        body: Expr,
69    },
70}
71
72/// Resugared variants for patterns. This represent extra printing-only patterns, see [`super::PatKind::Resugared`].
73#[derive_group_for_ast]
74pub enum ResugaredPatKind {
75    /// A record constructor pattern where wildcard fields are replaced by `..`.
76    ConstructWithEllipsis {
77        /// The identifier of the constructor we are matching.
78        constructor: GlobalId,
79        /// Is this a struct? (meaning, *not* a variant from an enum)
80        is_struct: bool,
81        /// Only the explicitly-bound (non-wildcard) fields.
82        fields: Vec<(GlobalId, Pat)>,
83    },
84}
85
86/// Resugared variants for types. This represent extra printing-only types, see [`super::TyKind::Resugared`].
87#[derive_group_for_ast]
88pub enum ResugaredTyKind {
89    /// A tuple tupe.
90    ///
91    /// # Example:
92    /// `(i32, bool)`
93    Tuple(Vec<Ty>),
94}
95
96/// Resugared variants for impl. items. This represent extra printing-only impl. items, see [`super::ImplItemKind::Resugared`].
97#[derive_group_for_ast]
98pub enum ResugaredImplItemKind {
99    /// An associated `const` impl item, for example `const NAME: T = body;`.
100    /// The type of the constant is `body.ty`.
101    Constant {
102        /// The body of the constant, for example `body`.
103        body: Expr,
104    },
105}
106
107/// Resugared variants for trait items. This represent extra printing-only trait items, see [`super::TraitItemKind::Resugared`].
108#[derive_group_for_ast]
109pub enum ResugaredTraitItemKind {}
110
111/// Marks a type as a resugar fragment of the AST.
112pub trait ResugaredFragment {
113    /// What fragment of the AST this resugar is extending?
114    type ParentFragment;
115}
116
117/// Convenience macro which implements [`ResugaredFragment`] on `$ty`, setting
118/// `$parent` as the `ParentFragment`, as well as `From<$ty>` for `$parent`, by
119/// wrapping the `$ty` in `$parent::Resugared(..)`.
120macro_rules! derive_from {
121    ($($ty:ty => $parent:ty),*) => {
122        $(impl ResugaredFragment for $ty {
123            type ParentFragment = $parent;
124        }
125        impl From<$ty> for <$ty as ResugaredFragment>::ParentFragment {
126            fn from(value: $ty) -> Self {
127                Self::Resugared(value)
128            }
129        })*
130    };
131}
132
133derive_from!(
134    ResugaredItemKind => ItemKind,
135    ResugaredExprKind => ExprKind,
136    ResugaredPatKind => PatKind,
137    ResugaredTyKind => TyKind,
138    ResugaredImplItemKind => ImplItemKind,
139    ResugaredTraitItemKind => TraitItemKind
140);
hax_rust_engine/ast/resugared.rs

hax_rust_engine/ast/
resugared.rs
