hax_rust_engine/
phase.rs

1//! A phase rewrites the AST.
2
3use crate::ast::Item;
4
5// Special kind of unreachability that should be prevented by a phase
6macro_rules! unreachable_by_invariant {
7    ($phase:ident) => {
8        unreachable!(
9            "The phase {} should make this unreachable",
10            stringify!($phase)
11        )
12    };
13}
14pub(crate) use unreachable_by_invariant;
15
16/// A Rust phase that operates on the AST.
17pub trait Phase {
18    /// Apply the phase on items.
19    /// A phase may transform an item into zero, one or more items.
20    fn apply(&self, items: &mut Vec<Item>);
21}
22
23pub mod legacy;
24
25mod explicit_monadic;
26mod filter_unprintable_items;
27mod reject_not_do_lean_dsl;
28
29macro_rules! declare_phase_kind {
30    {$($name:ident = $phase:expr),*$(,)?} => {
31        /// Enumeration of the available phases.
32        #[derive(Clone, Debug, Copy, serde::Serialize, serde::Deserialize)]
33        pub enum PhaseKind {
34            $(
35                #[doc = concat!("The phase [`", stringify!($phase), "].")]
36                $name,
37            )*
38            /// A legacy (OCaml) phase.
39            Legacy(crate::phase::legacy::LegacyOCamlPhase),
40        }
41
42        impl crate::phase::Phase for PhaseKind {
43            fn apply(&self, items: &mut Vec<Item>) {
44                match *self {
45                    $(Self::$name => $phase.apply(items),)*
46                    Self::Legacy(phase) => phase.apply(items),
47                }
48            }
49        }
50    };
51}
52
53declare_phase_kind! {
54    ExplicitMonadic = explicit_monadic::ExplicitMonadic,
55    RejectNotDoLeanDSL = reject_not_do_lean_dsl::RejectNotDoLeanDSL,
56    FilterUnprintableItems = filter_unprintable_items::FilterUnprintableItems,
57}
hax_rust_engine/phase.rs

hax_rust_engine/
phase.rs
