From 2493d278fa186d6afdc87d7fe1a1885e828c1070 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas.franceschino@inria.fr>
Date: Wed, 12 Jun 2024 14:19:58 +0200
Subject: [PATCH] refactor: get rid of crate hax-frontend-exporter-options

---
 Cargo.lock                                       | 15 +--------------
 Cargo.toml                                       |  3 ---
 cli/driver/Cargo.toml                            |  1 -
 cli/driver/src/exporter.rs                       | 12 ++++++------
 cli/options/Cargo.toml                           |  2 +-
 cli/options/engine/Cargo.toml                    |  3 +--
 cli/options/src/lib.rs                           |  8 ++++----
 cli/subcommands/Cargo.toml                       |  2 +-
 frontend/exporter/Cargo.toml                     |  1 -
 frontend/exporter/options/Cargo.toml             | 16 ----------------
 frontend/exporter/src/lib.rs                     |  2 +-
 .../{options/src/lib.rs => src/options.rs}       |  2 +-
 frontend/exporter/src/rustc_utils.rs             |  2 +-
 frontend/exporter/src/state.rs                   | 14 ++++----------
 frontend/exporter/src/traits.rs                  |  2 +-
 15 files changed, 22 insertions(+), 63 deletions(-)
 delete mode 100644 frontend/exporter/options/Cargo.toml
 rename frontend/exporter/{options/src/lib.rs => src/options.rs} (99%)

diff --git a/Cargo.lock b/Cargo.lock
index 7c619ec4b..b8ad5f28e 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -134,7 +134,6 @@ dependencies = [
  "hax-cli-options-engine",
  "hax-diagnostics",
  "hax-frontend-exporter",
- "hax-frontend-exporter-options",
  "hax-lib-macros-types",
  "is-terminal",
  "itertools",
@@ -452,7 +451,7 @@ name = "hax-cli-options"
 version = "0.1.0-pre.1"
 dependencies = [
  "clap",
- "hax-frontend-exporter-options",
+ "hax-frontend-exporter",
  "path-clean",
  "schemars",
  "serde",
@@ -467,7 +466,6 @@ dependencies = [
  "hax-cli-options",
  "hax-diagnostics",
  "hax-frontend-exporter",
- "hax-frontend-exporter-options",
  "itertools",
  "path-clean",
  "schemars",
@@ -495,7 +493,6 @@ dependencies = [
  "hax-cli-options-engine",
  "hax-diagnostics",
  "hax-frontend-exporter",
- "hax-frontend-exporter-options",
  "hax-lib-macros-types",
  "hax-lint",
  "hax-phase-debug-webapp",
@@ -538,7 +535,6 @@ dependencies = [
  "cfg-if",
  "extension-traits",
  "hax-adt-into",
- "hax-frontend-exporter-options",
  "itertools",
  "lazy_static",
  "paste",
@@ -548,15 +544,6 @@ dependencies = [
  "tracing",
 ]
 
-[[package]]
-name = "hax-frontend-exporter-options"
-version = "0.1.0-pre.1"
-dependencies = [
- "schemars",
- "serde",
- "serde_json",
-]
-
 [[package]]
 name = "hax-lib"
 version = "0.1.0-pre.1"
diff --git a/Cargo.toml b/Cargo.toml
index 6ed486c11..335a13c54 100644
--- a/Cargo.toml
+++ b/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" }
diff --git a/cli/driver/Cargo.toml b/cli/driver/Cargo.toml
index 0f33501ff..7afd1da74 100644
--- a/cli/driver/Cargo.toml
+++ b/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
diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs
index 948fbf5b5..c7b5aee1a 100644
--- a/cli/driver/src/exporter.rs
+++ b/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(
diff --git a/cli/options/Cargo.toml b/cli/options/Cargo.toml
index f302e3f18..d92b5aaa8 100644
--- a/cli/options/Cargo.toml
+++ b/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"
diff --git a/cli/options/engine/Cargo.toml b/cli/options/engine/Cargo.toml
index 2a649bb7b..59c9ed9f8 100644
--- a/cli/options/engine/Cargo.toml
+++ b/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"
 
diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs
index c50fdc8c8..a71c6045e 100644
--- a/cli/options/src/lib.rs
+++ b/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,
         }
     }
diff --git a/cli/subcommands/Cargo.toml b/cli/subcommands/Cargo.toml
index 0f8e453f3..f3f3221be 100644
--- a/cli/subcommands/Cargo.toml
+++ b/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"
diff --git a/frontend/exporter/Cargo.toml b/frontend/exporter/Cargo.toml
index b8a350aa7..3df222e85 100644
--- a/frontend/exporter/Cargo.toml
+++ b/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"
 
diff --git a/frontend/exporter/options/Cargo.toml b/frontend/exporter/options/Cargo.toml
deleted file mode 100644
index fadcbc905..000000000
--- a/frontend/exporter/options/Cargo.toml
+++ /dev/null
@@ -1,16 +0,0 @@
-[package]
-name = "hax-frontend-exporter-options"
-version.workspace = true
-authors.workspace = true
-license.workspace = true
-homepage.workspace = true
-edition.workspace = true
-repository.workspace = true
-readme.workspace = true
-description = "The options the `hax-frontend-exporter` crate is sensible to."
-
-[dependencies]
-serde.workspace = true
-serde_json.workspace = true
-schemars.workspace = true
-
diff --git a/frontend/exporter/src/lib.rs b/frontend/exporter/src/lib.rs
index 610f818e8..e04e88ac9 100644
--- a/frontend/exporter/src/lib.rs
+++ b/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::*;
diff --git a/frontend/exporter/options/src/lib.rs b/frontend/exporter/src/options.rs
similarity index 99%
rename from frontend/exporter/options/src/lib.rs
rename to frontend/exporter/src/options.rs
index a19c79f70..786496f26 100644
--- a/frontend/exporter/options/src/lib.rs
+++ b/frontend/exporter/src/options.rs
@@ -30,7 +30,7 @@ pub struct Namespace {
 
 impl std::convert::From<String> for Namespace {
     fn from(s: String) -> Self {
-        Namespace {
+        Self {
             chunks: s
                 .split("::")
                 .into_iter()
diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs
index f83248752..c9621a65c 100644
--- a/frontend/exporter/src/rustc_utils.rs
+++ b/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;
diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs
index b805e00c5..c59d07082 100644
--- a/frontend/exporter/src/state.rs
+++ b/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 {
diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
index 106b79078..4ade138b0 100644
--- a/frontend/exporter/src/traits.rs
+++ b/frontend/exporter/src/traits.rs
@@ -322,8 +322,8 @@ mod full {
         }
     }
 
-    #[tracing::instrument(level = "trace", skip(s))]
     impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
+        #[tracing::instrument(level = "trace", skip(s))]
         fn impl_expr<S: UnderOwnerState<'tcx>>(
             &self,
             s: &S,