Skip to content

Commit

Permalink
refactor: get rid of crate hax-frontend-exporter-options
Browse files Browse the repository at this point in the history
  • Loading branch information
W95Psp committed Jun 13, 2024
1 parent 521371c commit 2493d27
Show file tree
Hide file tree
Showing 15 changed files with 22 additions and 63 deletions.
15 changes: 1 addition & 14 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 0 additions & 3 deletions Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
[workspace]
members = [
"frontend/exporter",
"frontend/exporter/options",
"frontend/diagnostics",
"frontend/lint",
"cli/options",
Expand All @@ -22,7 +21,6 @@ members = [
exclude = ["tests"]
default-members = [
"frontend/exporter",
"frontend/exporter/options",
"frontend/diagnostics",
"frontend/lint",
"cli/options",
Expand Down Expand Up @@ -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" }
Expand Down
1 change: 0 additions & 1 deletion cli/driver/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
12 changes: 6 additions & 6 deletions cli/driver/src/exporter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
) -> (
Expand Down Expand Up @@ -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,
}
}
Expand Down Expand Up @@ -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>,
Expand Down Expand Up @@ -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(
Expand Down
2 changes: 1 addition & 1 deletion cli/options/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
3 changes: 1 addition & 2 deletions cli/options/engine/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"

8 changes: 4 additions & 4 deletions cli/options/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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,
}
}
Expand Down
2 changes: 1 addition & 1 deletion cli/subcommands/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
1 change: 0 additions & 1 deletion frontend/exporter/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand Down
16 changes: 0 additions & 16 deletions frontend/exporter/options/Cargo.toml

This file was deleted.

2 changes: 1 addition & 1 deletion frontend/exporter/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::*;
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
2 changes: 1 addition & 1 deletion frontend/exporter/src/rustc_utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
14 changes: 4 additions & 10 deletions frontend/exporter/src/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
Expand All @@ -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()),
Expand Down Expand Up @@ -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: (),
Expand All @@ -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 {
Expand Down
2 changes: 1 addition & 1 deletion frontend/exporter/src/traits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down

0 comments on commit 2493d27

Please sign in to comment.