refactor: get rid of crate hax-frontend-exporter-options

Cargo.toml

@@ -1,7 +1,6 @@
 [workspace]
 members = [
      "frontend/exporter",
-     "frontend/exporter/options",
      "frontend/diagnostics",
      "frontend/lint",
      "cli/options",
@@ -22,7 +21,6 @@ members = [
 exclude = ["tests"]
 default-members = [
      "frontend/exporter",
-     "frontend/exporter/options",
      "frontend/diagnostics",
      "frontend/lint",
      "cli/options",
@@ -83,7 +81,6 @@ hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-pre.1" }
 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" }

cli/driver/Cargo.toml

@@ -24,7 +24,6 @@ colored.workspace = true
 hax-frontend-exporter.workspace = true
 hax-cli-options.workspace = true
 hax-cli-options-engine.workspace = true
-hax-frontend-exporter-options.workspace = true
 hax-lint.workspace = true
 hax-diagnostics.workspace = true
 hax-lib-macros-types.workspace = true

cli/driver/src/exporter.rs

@@ -157,7 +157,7 @@ fn precompute_local_thir_bodies<'tcx>(
 /// (I call "THIR'" the AST described in this crate)
 #[tracing::instrument(skip_all)]
 fn convert_thir<'tcx, Body: hax_frontend_exporter::IsBody>(
-    options: &hax_frontend_exporter_options::Options,
+    options: &hax_frontend_exporter::options::Options,
     macro_calls: HashMap<hax_frontend_exporter::Span, hax_frontend_exporter::Span>,
     tcx: TyCtxt<'tcx>,
 ) -> (
@@ -278,9 +278,9 @@ pub(crate) struct ExtractionCallbacks {
     pub macro_calls: HashMap<hax_frontend_exporter::Span, hax_frontend_exporter::Span>,
 }
 
-impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
-    fn from(opts: ExtractionCallbacks) -> hax_frontend_exporter_options::Options {
-        hax_frontend_exporter_options::Options {
+impl From<ExtractionCallbacks> for hax_frontend_exporter::options::Options {
+    fn from(opts: ExtractionCallbacks) -> hax_frontend_exporter::options::Options {
+        hax_frontend_exporter::options::Options {
             inline_macro_calls: opts.inline_macro_calls,
         }
     }
@@ -323,7 +323,7 @@ impl Callbacks for ExtractionCallbacks {
                     include_extra,
                 } => {
                     struct Driver<'tcx> {
-                        options: hax_frontend_exporter_options::Options,
+                        options: hax_frontend_exporter::options::Options,
                         macro_calls:
                             HashMap<hax_frontend_exporter::Span, hax_frontend_exporter::Span>,
                         tcx: TyCtxt<'tcx>,
@@ -452,7 +452,7 @@ impl Callbacks for ExtractionCallbacks {
                             )
                         });
                     let options_frontend =
-                        hax_frontend_exporter_options::Options::from(self.clone());
+                        hax_frontend_exporter::options::Options::from(self.clone());
                     let state =
                         hax_frontend_exporter::state::State::new(tcx, options_frontend.clone());
                     report_diagnostics(

cli/options/Cargo.toml

@@ -15,5 +15,5 @@ serde.workspace = true
 serde_json.workspace = true
 schemars.workspace = true
 clap.workspace = true
-hax-frontend-exporter-options.workspace = true
+hax-frontend-exporter = { workspace = true, features = [] }
 path-clean = "1.0.1"

cli/options/engine/Cargo.toml

@@ -17,7 +17,6 @@ itertools.workspace = true
 clap.workspace = true
 hax-diagnostics.workspace = true
 hax-cli-options.workspace = true
-hax-frontend-exporter.workspace = true
-hax-frontend-exporter-options.workspace = true
+hax-frontend-exporter = { workspace = true, features = [] }
 path-clean = "1.0.1"
 

cli/options/src/lib.rs

@@ -4,7 +4,7 @@ use serde::{Deserialize, Serialize};
 use std::fmt;
 use std::path::{Path, PathBuf};
 
-pub use hax_frontend_exporter_options::*;
+pub use hax_frontend_exporter::options::{self, Namespace};
 
 #[derive(JsonSchema, Debug, Clone, Serialize, Deserialize)]
 pub enum DebugEngineMode {
@@ -449,9 +449,9 @@ impl NormalizePaths for Options {
     }
 }
 
-impl From<Options> for hax_frontend_exporter_options::Options {
-    fn from(opts: Options) -> hax_frontend_exporter_options::Options {
-        hax_frontend_exporter_options::Options {
+impl From<Options> for options::Options {
+    fn from(opts: Options) -> options::Options {
+        options::Options {
             inline_macro_calls: opts.inline_macro_calls,
         }
     }

cli/subcommands/Cargo.toml

@@ -30,7 +30,7 @@ itertools.workspace = true
 clap.workspace = true
 paste = "1.0.11"
 hax-cli-options.workspace = true
-hax-frontend-exporter-options.workspace = true
+hax-frontend-exporter = { workspace = true, features = [] }
 hax-diagnostics.workspace = true
 path-clean = "1.0.1"
 tempfile = "3.8"

frontend/exporter/Cargo.toml

@@ -16,7 +16,6 @@ rustc_private=true
 serde.workspace = true
 serde_json.workspace = true
 schemars.workspace = true
-hax-frontend-exporter-options.workspace = true
 hax-adt-into.workspace = true
 paste = "1.0.11"
 

frontend/exporter/src/lib.rs

@@ -48,11 +48,11 @@ cfg_if::cfg_if! {
 mod body;
 mod constant_utils;
 mod index_vec;
+pub mod options;
 mod prelude;
 mod sinto;
 mod traits;
 mod types;
 
 pub use hax_adt_into::AdtInto;
-pub use hax_frontend_exporter_options as options;
 pub use prelude::*;

frontend/exporter/options/src/lib.rs → frontend/exporter/src/options.rs

@@ -24,13 +24,29 @@ impl std::convert::From<&str> for NamespaceChunk {
 }
 
 #[derive(Debug, Clone, Serialize, Deserialize, JsonSchema)]
-pub struct Namespace {
-    pub chunks: Vec<NamespaceChunk>,
+pub struct NamespacePattern {
+    chunks: Vec<NamespaceChunk>,
+}
+#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema)]
+pub enum Namespace {
+    /// A pattern that matches `DefId`s
+    Pattern(NamespacePattern),
+    /// An exact `DefId`
+    Exact(crate::DefId),
 }
 
 impl std::convert::From<String> for Namespace {
     fn from(s: String) -> Self {
-        Namespace {
+        if let Some(def_id) = crate::DefId::deserialize_compact(&s) {
+            Self::Exact(def_id)
+        } else {
+            Self::Pattern(s.into())
+        }
+    }
+}
+impl std::convert::From<String> for NamespacePattern {
+    fn from(s: String) -> Self {
+        Self {
             chunks: s
                 .split("::")
                 .into_iter()
@@ -41,7 +57,7 @@ impl std::convert::From<String> for Namespace {
     }
 }
 
-impl Namespace {
+impl NamespacePattern {
     pub fn matches(&self, path: &Vec<String>) -> bool {
         fn aux(pattern: &[NamespaceChunk], path: &[String]) -> bool {
             match (pattern, path) {

frontend/exporter/src/rustc_utils.rs

@@ -231,7 +231,7 @@ pub(crate) fn raw_macro_invocation_of_span<'t, S: BaseState<'t>>(
     span: rustc_span::Span,
     state: &S,
 ) -> Option<(DefId, rustc_span::hygiene::ExpnData)> {
-    let opts: Rc<hax_frontend_exporter_options::Options> = state.base().options;
+    let opts: Rc<crate::options::Options> = state.base().options;
     let macro_calls: crate::state::MacroCalls = state.base().macro_infos;
 
     let sess = state.base().tcx.sess;

frontend/exporter/src/state.rs

@@ -115,7 +115,7 @@ mod types {
 
     #[derive(Clone)]
     pub struct Base<'tcx> {
-        pub options: Rc<hax_frontend_exporter_options::Options>,
+        pub options: Rc<crate::options::Options>,
         pub macro_infos: MacroCalls,
         pub local_ctx: Rc<RefCell<LocalContextS>>,
         pub opt_def_id: Option<rustc_hir::def_id::DefId>,
@@ -134,10 +134,7 @@ mod types {
     }
 
     impl<'tcx> Base<'tcx> {
-        pub fn new(
-            tcx: rustc_middle::ty::TyCtxt<'tcx>,
-            options: hax_frontend_exporter_options::Options,
-        ) -> Self {
+        pub fn new(tcx: rustc_middle::ty::TyCtxt<'tcx>, options: crate::options::Options) -> Self {
             Self {
                 tcx,
                 macro_infos: Rc::new(HashMap::new()),
@@ -172,10 +169,7 @@ mk!(
 pub use self::types::*;
 
 impl<'tcx> State<Base<'tcx>, (), (), ()> {
-    pub fn new(
-        tcx: rustc_middle::ty::TyCtxt<'tcx>,
-        options: hax_frontend_exporter_options::Options,
-    ) -> Self {
+    pub fn new(tcx: rustc_middle::ty::TyCtxt<'tcx>, options: crate::options::Options) -> Self {
         Self {
             thir: (),
             mir: (),
@@ -198,7 +192,7 @@ impl<'tcx> State<Base<'tcx>, (), (), rustc_hir::def_id::DefId> {
 impl<'tcx> State<Base<'tcx>, (), Rc<rustc_middle::mir::Body<'tcx>>, rustc_hir::def_id::DefId> {
     pub fn new_from_mir(
         tcx: rustc_middle::ty::TyCtxt<'tcx>,
-        options: hax_frontend_exporter_options::Options,
+        options: crate::options::Options,
         mir: rustc_middle::mir::Body<'tcx>,
         owner_id: rustc_hir::def_id::DefId,
     ) -> Self {