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
22/// Resugared variants for expressions. This represent extra printing-only expressions, see [`super::ExprKind::Resugared`].
23#[derive_group_for_ast]
24pub enum ResugaredExprKind {
25    /// Binary operations (identified by resugaring) of the form `f(e1, e2)`
26    BinOp {
27        /// The identifier of the operation (`f`)
28        op: GlobalId,
29        /// The left-hand side of the operation (`e1`)
30        lhs: Expr,
31        /// The right-hand side of the operation (`e2`)
32        rhs: Expr,
33        /// The generic arguments applied to the function.
34        generic_args: Vec<GenericValue>,
35        /// If the function requires generic bounds to be called, `bounds_impls`
36        /// is a vector of impl. expressions for those bounds.
37        bounds_impls: Vec<ImplExpr>,
38        /// If we apply an associated function, contains the impl. expr used.
39        trait_: Option<(ImplExpr, Vec<GenericValue>)>,
40    },
41}
42
43/// Resugared variants for patterns. This represent extra printing-only patterns, see [`super::PatKind::Resugared`].
44#[derive_group_for_ast]
45pub enum ResugaredPatKind {}
46
47/// Resugared variants for types. This represent extra printing-only types, see [`super::TyKind::Resugared`].
48#[derive_group_for_ast]
49pub enum ResugaredTyKind {}
50
51/// Resugared variants for impl. items. This represent extra printing-only impl. items, see [`super::ImplItemKind::Resugared`].
52#[derive_group_for_ast]
53pub enum ResugaredImplItemKind {}
54
55/// Resugared variants for trait items. This represent extra printing-only trait items, see [`super::TraitItemKind::Resugared`].
56#[derive_group_for_ast]
57pub enum ResugaredTraitItemKind {}
58
59/// Marks a type as a resugar fragment of the AST.
60pub trait ResugaredFragment {
61    /// What fragment of the AST this resugar is extending?
62    type ParentFragment;
63}
64
65/// Convenience macro which implements [`ResugaredFragment`] on `$ty`, setting
66/// `$parent` as the `ParentFragment`, as well as `From<$ty>` for `$parent`, by
67/// wrapping the `$ty` in `$parent::Resugared(..)`.
68macro_rules! derive_from {
69    ($($ty:ty => $parent:ty),*) => {
70        $(impl ResugaredFragment for $ty {
71            type ParentFragment = $parent;
72        }
73        impl From<$ty> for <$ty as ResugaredFragment>::ParentFragment {
74            fn from(value: $ty) -> Self {
75                Self::Resugared(value)
76            }
77        })*
78    };
79}
80
81derive_from!(
82    ResugaredItemKind => ItemKind,
83    ResugaredExprKind => ExprKind,
84    ResugaredPatKind => PatKind,
85    ResugaredTyKind => TyKind,
86    ResugaredImplItemKind => ImplItemKind,
87    ResugaredTraitItemKind => TraitItemKind
88);
hax_rust_engine/ast/resugared.rs

hax_rust_engine/ast/
resugared.rs
