Merge pull request #743 from hacspec/frontend-haxmeta

Refactor of the frontend

Cargo.toml

@@ -2,10 +2,6 @@
 members = [
      "frontend/exporter",
      "frontend/exporter/options",
-     "frontend/diagnostics",
-     "frontend/lint",
-     "cli/options",
-     "cli/options/engine",
      "cli/subcommands",
      "cli/driver",
      "test-harness",
@@ -18,15 +14,12 @@ members = [
      "hax-bounded-integers",
      "engine/names",
      "engine/names/extract",
+     "hax-types",
 ]
 exclude = ["tests"]
 default-members = [
      "frontend/exporter",
      "frontend/exporter/options",
-     "frontend/diagnostics",
-     "frontend/lint",
-     "cli/options",
-     "cli/options/engine",
      "cli/subcommands",
      "cli/driver",
      "test-harness",
@@ -77,17 +70,16 @@ quote = "1.0.32"
 proc-macro2 = "1.0.66"
 cargo_metadata = "0.15"
 colored = "2"
+bincode = "2.0.0-rc.3"
+annotate-snippets = "0.11"
 
 # Crates in this repository
-hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-pre.1" }
+hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-pre.1", default-features = false }
 hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-pre.1" }
-hax-cli-options = { path = "cli/options", version = "=0.1.0-pre.1" }
-hax-cli-options-engine = { path = "cli/options/engine", version = "=0.1.0-pre.1" }
 hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-pre.1" }
-hax-diagnostics = { path = "frontend/diagnostics", version = "=0.1.0-pre.1" }
-hax-lint = { path = "frontend/lint", version = "=0.1.0-pre.1" }
 hax-phase-debug-webapp = { path = "engine/utils/phase-debug-webapp", version = "=0.1.0-pre.1" }
 hax-lib-macros-types = { path = "hax-lib-macros/types", version = "=0.1.0-pre.1" }
 hax-lib-macros = { path = "hax-lib-macros", version = "=0.1.0-pre.1" }
 hax-lib = { path = "hax-lib", version = "=0.1.0-pre.1" }
 hax-engine-names = { path = "engine/names", version = "=0.1.0-pre.1" }
+hax-types = { path = "hax-types", version = "=0.1.0-pre.1" }

PUBLISHING.md

@@ -14,10 +14,8 @@ and `examples`):
 1. `hax-frontend-exporter-options` (`frontend/exporter/options `)
 2. `hax-adt-into` (`frontend/exporter/adt-into`)
 3. `hax-frontend-exporter` (`frontend/exporter`)
-4. `hax-cli-options` (`cli/options`)
-5. `hax-diagnostics` (`frontend/diagnostics`)
-6. `hax-cli-options-engine` (`cli/options/engine`)
-7. `hax-subcommands` (binaries) (`cli/subcommands`)
+4. `hax-types` (`hax-types`)
+5. `hax-subcommands` (binaries) (`cli/subcommands`)
    - `cargo-hax`
    - `hax-export-json-schemas`
    - `hax-pretty-print-diagnostics`

cli/driver/Cargo.toml

@@ -21,18 +21,11 @@ serde.workspace = true
 serde_json.workspace = true
 clap.workspace = true
 colored.workspace = true
-hax-frontend-exporter.workspace = true
-hax-cli-options.workspace = true
-hax-cli-options-engine.workspace = true
+hax-frontend-exporter = {workspace = true, features = ["rustc"]}
+hax-types = {workspace = true, features = ["rustc"]}
 hax-frontend-exporter-options.workspace = true
-hax-lint.workspace = true
-hax-diagnostics.workspace = true
 hax-lib-macros-types.workspace = true
 itertools.workspace = true
-which.workspace = true
-inquire = "0.6"
-const_format = "0.2"
 tracing.workspace = true
 tracing-subscriber.workspace = true
 tracing-tree.workspace = true
-hax-phase-debug-webapp.workspace = true

cli/driver/src/callbacks_wrapper.rs

@@ -1,5 +1,4 @@
-use const_format::formatcp;
-use hax_cli_options::{Command, ENV_VAR_OPTIONS_FRONTEND};
+use hax_types::cli_options::{Command, Options, ENV_VAR_OPTIONS_FRONTEND};
 
 use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::{interface, Queries};
@@ -9,14 +8,14 @@ use rustc_span::symbol::Symbol;
 /// configuration in the `config` phase of rustc
 pub struct CallbacksWrapper<'a> {
     pub sub: &'a mut (dyn Callbacks + Send + 'a),
-    pub options: hax_cli_options::Options,
+    pub options: Options,
 }
 impl<'a> Callbacks for CallbacksWrapper<'a> {
     fn config(&mut self, config: &mut interface::Config) {
         let options = self.options.clone();
         config.psess_created = Some(Box::new(move |parse_sess| {
             parse_sess.env_depinfo.get_mut().insert((
-                Symbol::intern(hax_cli_options::ENV_VAR_OPTIONS_FRONTEND),
+                Symbol::intern(ENV_VAR_OPTIONS_FRONTEND),
                 Some(Symbol::intern(&serde_json::to_string(&options).unwrap())),
             ));
         }));

cli/driver/src/driver.rs

@@ -30,18 +30,13 @@ mod exporter;
 use std::collections::HashSet;
 
 use exporter::ExtractionCallbacks;
-use hax_lint::Type;
-
-mod linter;
-use linter::LinterCallbacks;
 
 mod callbacks_wrapper;
 mod features;
 use callbacks_wrapper::*;
 use features::*;
 
-use const_format::formatcp;
-use hax_cli_options::{BackendOptions, Command, ExporterCommand, ENV_VAR_OPTIONS_FRONTEND};
+use hax_types::cli_options::{BackendOptions, Command, ENV_VAR_OPTIONS_FRONTEND};
 
 use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::{interface, Queries};
@@ -83,12 +78,12 @@ const HAX_VANILLA_RUSTC: &str = "HAX_VANILLA_RUSTC";
 fn main() {
     setup_logging();
 
-    let options: hax_cli_options::Options =
-        serde_json::from_str(&std::env::var(ENV_VAR_OPTIONS_FRONTEND).expect(&formatcp!(
+    let options: hax_types::cli_options::Options =
+        serde_json::from_str(&std::env::var(ENV_VAR_OPTIONS_FRONTEND).expect(&format!(
             "Cannot find environnement variable {}",
             ENV_VAR_OPTIONS_FRONTEND
         )))
-        .expect(&formatcp!(
+        .expect(&format!(
             "Invalid value for the environnement variable {}",
             ENV_VAR_OPTIONS_FRONTEND
         ));
@@ -127,24 +122,11 @@ fn main() {
     let translate_package =
         !vanilla_rustc && !is_build_script && (options.deps || is_primary_package);
     let mut callbacks: Box<dyn Callbacks + Send> = if translate_package {
-        match &options.command {
-            Some(Command::ExporterCommand(command)) => Box::new(exporter::ExtractionCallbacks {
-                inline_macro_calls: options.inline_macro_calls.clone(),
-                command: command.clone(),
-                macro_calls: std::collections::HashMap::new(),
-            }),
-            Some(Command::LintCommand(command)) => {
-                let ltype = match command {
-                    hax_cli_options::LinterCommand::Hacspec => Type::Hacspec,
-                    hax_cli_options::LinterCommand::Rust => Type::Rust,
-                };
-                Box::new(LinterCallbacks::new(ltype))
-            }
-            None => {
-                // hacspec lint
-                Box::new(LinterCallbacks::new(Type::Rust))
-            }
-        }
+        Box::new(exporter::ExtractionCallbacks {
+            inline_macro_calls: options.inline_macro_calls.clone(),
+            body_types: options.command.body_kinds(),
+            macro_calls: std::collections::HashMap::new(),
+        })
     } else {
         struct CallbacksNoop;
         impl Callbacks for CallbacksNoop {}
@@ -171,10 +153,9 @@ fn main() {
                 hax_lib_macros_types::HAX_CFG_OPTION_NAME.into(),
             ])
             .chain(match &options.command {
-                Some(Command::ExporterCommand(ExporterCommand::Backend(BackendOptions {
-                    backend,
-                    ..
-                }))) => vec!["--cfg".into(), format!("hax_backend_{backend}")],
+                Command::Backend(BackendOptions { backend, .. }) => {
+                    vec!["--cfg".into(), format!("hax_backend_{backend}")]
+                }
                 _ => vec![],
             })
             .chain(features.into_iter().map(|s| format!("-Zcrate-attr={}", s)))
@@ -184,13 +165,14 @@ fn main() {
 
     let mut callbacks = CallbacksWrapper {
         sub: &mut *callbacks,
-        options: hax_cli_options::Options {
-            force_cargo_build: if translate_package {
+        options: {
+            let mut options = options.clone();
+            options.force_cargo_build = if translate_package {
                 options.force_cargo_build
             } else {
-                hax_cli_options::ForceCargoBuild::default()
-            },
-            ..options
+                hax_types::cli_options::ForceCargoBuild::default()
+            };
+            options
         },
     };