hax_rust_engine/phase/
legacy.rs

1//! This module exposes the legacy phases written in OCaml in the OCaml engine.
2
3use crate::{
4    ast::Item,
5    phase::{Phase, PhaseKind},
6};
7
8/// Group consecutive ocaml phases as one monolithic phase, so that we avoid extra roundtrips to the OCaml engine.
9pub fn group_consecutive_ocaml_phases(phases: Vec<PhaseKind>) -> Vec<Box<dyn Phase>> {
10    let mut output: Vec<Box<dyn Phase>> = vec![];
11    let mut ocaml_phases = vec![];
12    let mut phases = phases.into_iter();
13
14    struct LegacyOCamlPhases {
15        phases: Vec<LegacyOCamlPhase>,
16    }
17
18    impl Phase for LegacyOCamlPhases {
19        fn apply(&self, items: &mut Vec<Item>) {
20            apply_legacy_phases(&self.phases, items);
21        }
22    }
23
24    loop {
25        let phase = phases.next();
26        if let Some(PhaseKind::Legacy(ocaml_phase)) = phase {
27            ocaml_phases.push(ocaml_phase)
28        } else {
29            if !ocaml_phases.is_empty() {
30                output.push(Box::new(LegacyOCamlPhases {
31                    phases: std::mem::take(&mut ocaml_phases),
32                }));
33            }
34            if let Some(phase) = phase {
35                output.push(Box::new(phase));
36            } else {
37                break;
38            }
39        }
40    }
41
42    output
43}
44
45fn apply_legacy_phases(phases: &[LegacyOCamlPhase], items: &mut Vec<Item>) {
46    use crate::ocaml_engine::Response;
47    let query = crate::ocaml_engine::QueryKind::ApplyPhases {
48        input: std::mem::take(items),
49        phases: phases.iter().map(ToString::to_string).collect(),
50    };
51    let Some(Response::ApplyPhases { output }) = query.execute(None) else {
52        panic!()
53    };
54    *items = output;
55}
56
57macro_rules! make_ocaml_legacy_phase {
58    ($($name:ident),*) => {
59
60        pastey::paste!{
61            /// The list of exposed OCaml phases.
62            #[derive(Debug, Clone, Copy, serde::Serialize, serde::Deserialize)]
63            pub enum LegacyOCamlPhase {
64                $(
65                    #[doc = concat!("The phase ", stringify!($name), " from the OCaml engine.")]
66                    [< $name:camel >]
67                ),*
68            }
69
70
71            impl std::fmt::Display for LegacyOCamlPhase {
72                fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
73                    match self {
74                        $(Self::[< $name:camel >] => stringify!($name).fmt(f)),*
75                    }
76                }
77            }
78
79            impl Phase for LegacyOCamlPhase {
80                fn apply(&self, items: &mut Vec<Item>) {
81                    apply_legacy_phases(&[*self], items);
82                }
83            }
84        }
85    };
86}
87
88impl From<LegacyOCamlPhase> for PhaseKind {
89    fn from(legacy_phase: LegacyOCamlPhase) -> Self {
90        Self::Legacy(legacy_phase)
91    }
92}
93
94make_ocaml_legacy_phase!(
95    and_mut_defsite,
96    bundle_cycles,
97    cf_into_monads,
98    direct_and_mut,
99    drop_blocks,
100    drop_match_guards,
101    drop_references,
102    drop_return_break_continue,
103    drop_sized_trait,
104    explicit_conversions,
105    functionalize_loops,
106    hoist_disjunctive_patterns,
107    local_mutation,
108    newtype_as_refinement,
109    reconstruct_asserts,
110    reconstruct_for_index_loops,
111    reconstruct_for_loops,
112    reconstruct_question_marks,
113    reconstruct_while_loops,
114    reorder_fields,
115    rewrite_control_flow,
116    rewrite_local_self,
117    simplify_hoisting,
118    simplify_match_return,
119    simplify_question_marks,
120    sort_items,
121    specialize,
122    traits_specs,
123    transform_hax_lib_inline,
124    trivialize_assign_lhs,
125    reject_arbitrary_lhs,
126    reject_continue,
127    reject_question_mark,
128    reject_raw_or_mut_pointer,
129    reject_early_exit,
130    reject_as_pattern,
131    reject_dyn,
132    reject_trait_item_default,
133    reject_unsafe,
134    reject_impl_type_method,
135    hoist_side_effects
136);
hax_rust_engine/phase/legacy.rs

hax_rust_engine/phase/
legacy.rs
