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!($ident)
11        )
12    };
13}
14pub(crate) use unreachable_by_invariant;
15
16/// Placeholder trait for phases.
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
23mod explicit_monadic;
24mod reject_not_do_lean_dsl;
25
26pub use explicit_monadic::ExplicitMonadic;
27pub use reject_not_do_lean_dsl::RejectNotDoLeanDSL;
hax_rust_engine/phase.rs

hax_rust_engine/
phase.rs
