hax_types/
engine_api.rs

1use crate::cli_options::*;
2use crate::prelude::*;
3
4type ThirBody = hax_frontend_exporter::ThirBody;
5
6#[derive_group(Serializers)]
7#[derive(JsonSchema, Debug, Clone)]
8pub struct EngineOptions {
9    pub hax_version: String,
10    pub backend: BackendOptions<()>,
11    pub input: Vec<hax_frontend_exporter::Item<ThirBody>>,
12    pub impl_infos: Vec<(
13        hax_frontend_exporter::DefId,
14        hax_frontend_exporter::ImplInfos,
15    )>,
16}
17
18#[derive_group(Serializers)]
19#[allow(non_snake_case)]
20#[derive(JsonSchema, Debug, Clone)]
21pub struct SourceMap {
22    pub mappings: String,
23    pub sourceRoot: String,
24    pub sources: Vec<String>,
25    pub sourcesContent: Vec<Option<String>>,
26    pub names: Vec<String>,
27    pub version: u8,
28    pub file: String,
29}
30
31impl SourceMap {
32    pub fn inline_sources_content(&mut self) {
33        self.sourcesContent = vec![];
34        for source in &self.sources {
35            let path = if self.sourceRoot.is_empty() {
36                source.clone()
37            } else {
38                format!("{}/{}", &self.sourceRoot, source)
39            };
40            let contents = Some(std::fs::read_to_string(path).unwrap());
41            self.sourcesContent.push(contents);
42        }
43    }
44}
45
46#[derive_group(Serializers)]
47#[derive(JsonSchema, Debug, Clone)]
48pub struct File {
49    pub path: String,
50    pub contents: String,
51    pub sourcemap: Option<SourceMap>,
52}
53
54#[derive_group(Serializers)]
55#[derive(JsonSchema, Debug, Clone)]
56pub struct Output {
57    pub diagnostics: Vec<crate::diagnostics::Diagnostics>,
58    pub files: Vec<File>,
59    pub debug_json: Option<String>,
60}
61
62#[derive_group(Serializers)]
63#[derive(JsonSchema, Debug, Clone)]
64pub struct ProfilingData {
65    /// What context are we profiling?
66    pub context: String,
67    /// How long this took?
68    pub time_ns: u64,
69    /// How much memory this took? This is using OCaml's
70    /// `Gc.minor_words`, and is probably not very precise.
71    pub memory: u64,
72    /// How many things were processed? (often, this is the number of
73    /// items a phase processes)
74    pub quantity: u32,
75    /// Did the action errored? This is important since a failed
76    /// action might have exited very early, making the numbers
77    /// unusable.
78    pub errored: bool,
79}
80
81pub mod protocol {
82    use super::*;
83
84    #[derive_group(Serializers)]
85    #[derive(JsonSchema, Debug, Clone)]
86    pub enum FromEngine {
87        Diagnostic(crate::diagnostics::Diagnostics),
88        File(File),
89        PrettyPrintDiagnostic(crate::diagnostics::Diagnostics),
90        PrettyPrintRust(String),
91        DebugString(String),
92        ProfilingData(ProfilingData),
93        /// Declares a list of items that will be processed by the engine
94        ItemProcessed(Vec<hax_frontend_exporter::DefId>),
95        Exit,
96        Ping,
97    }
98    #[derive_group(Serializers)]
99    #[derive(JsonSchema, Debug, Clone)]
100    pub enum ToEngine {
101        PrettyPrintedDiagnostic(String),
102        PrettyPrintedRust(Result<String, String>),
103        Pong,
104    }
105
106    impl FromEngine {
107        pub fn requires_response(&self) -> bool {
108            matches!(
109                self,
110                Self::PrettyPrintRust { .. }
111                    | Self::Ping { .. }
112                    | Self::PrettyPrintDiagnostic { .. }
113            )
114        }
115    }
116}
117
118// This is located here for dependency reason, but this is not related
119// to the engine (yet?).
120#[derive_group(Serializers)]
121#[derive(JsonSchema, Debug, Clone)]
122pub struct WithDefIds<Body: hax_frontend_exporter::IsBody> {
123    pub def_ids: Vec<hax_frontend_exporter::DefId>,
124    pub impl_infos: Vec<(
125        hax_frontend_exporter::DefId,
126        hax_frontend_exporter::ImplInfos,
127    )>,
128    pub items: Vec<hax_frontend_exporter::Item<Body>>,
129    pub comments: Vec<(hax_frontend_exporter::Span, String)>,
130}
hax_types/engine_api.rs

hax_types/
engine_api.rs
