hax_rust_engine/backends/
fstar.rs

1//! The F* backend. The F* printer is still implemented in Ocaml but the phase driver uses this infrastructure
2
3/// The F* backend
4pub struct FStarBackend;
5
6impl super::Backend for FStarBackend {
7    // TODO Replace by an empty printer
8    // This is a dummy value. The fstar backend's printer is implemented in OCaml
9    type Printer = super::lean::LeanPrinter;
10
11    fn module_path(&self, _module: &super::Module) -> camino::Utf8PathBuf {
12        todo!("The fstar backend's printer is implemented in OCaml")
13    }
14
15    fn phases(&self) -> Vec<crate::phase::PhaseKind> {
16        use crate::phase::legacy::LegacyOCamlPhase::*;
17        vec![
18            RejectRawOrMutPointer.into(),
19            RewriteLocalSelf.into(),
20            TransformHaxLibInline.into(),
21            Specialize.into(),
22            DropSizedTrait.into(),
23            SimplifyQuestionMarks.into(),
24            AndMutDefsite.into(),
25            ReconstructAsserts.into(),
26            ReconstructForLoops.into(),
27            ReconstructWhileLoops.into(),
28            DirectAndMut.into(),
29            RejectArbitraryLhs.into(),
30            DropBlocks.into(),
31            DropMatchGuards.into(),
32            DropReferences.into(),
33            ExplicitConversions.into(),
34            TrivializeAssignLhs.into(),
35            HoistSideEffects.into(),
36            HoistDisjunctivePatterns.into(),
37            SimplifyMatchReturn.into(),
38            LocalMutation.into(),
39            RewriteControlFlow.into(),
40            DropReturnBreakContinue.into(),
41            FunctionalizeLoops.into(),
42            RejectQuestionMark.into(),
43            RejectAsPattern.into(),
44            TraitsSpecs.into(),
45            SimplifyHoisting.into(),
46            NewtypeAsRefinement.into(),
47            RejectTraitItemDefault.into(),
48            BundleCycles.into(),
49            ReorderFields.into(),
50            SortItems.into(),
51        ]
52    }
53}
hax_rust_engine/backends/fstar.rs

hax_rust_engine/backends/
fstar.rs
