hax-rust-engine 0.3.6

The engine of the hax toolchain.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

//! A phase rewrites the AST.

use crate::ast::Item;

// Special kind of unreachability that should be prevented by a phase
macro_rules! unreachable_by_invariant {
    ($phase:ident) => {
        unreachable!(
            "The phase {} should make this unreachable",
            stringify!($ident)
        )
    };
}
pub(crate) use unreachable_by_invariant;

/// Placeholder trait for phases.
pub trait Phase {
    /// Apply the phase on items.
    /// A phase may transform an item into zero, one or more items.
    fn apply(&self, items: &mut Vec<Item>);
}

mod explicit_monadic;
mod reject_not_do_lean_dsl;

pub use explicit_monadic::ExplicitMonadic;
pub use reject_not_do_lean_dsl::RejectNotDoLeanDSL;