Merge pull request #753 from hacspec/make-exporter-not-nightly

 exporter: make it need nightly only when feature `rustc` is on

.github/workflows/test.yml

@@ -30,6 +30,9 @@ jobs:
       - name: Test
         run: cargo test --workspace --exclude hax-engine-names-extract --verbose
 
+      - name: Test `hax-frontend-exporter` with feature `rustc` off
+        run: cargo check -p hax-frontend-exporter --no-default-features --verbose
+
   no-std-lib:
     runs-on: ubuntu-latest
     steps:

frontend/exporter/src/constant_utils.rs

@@ -278,20 +278,32 @@ mod rustc {
             // A [Scalar] might also be any zero-sized [Adt] or [Tuple] (i.e., unit)
             ty::Tuple(ty) if ty.is_empty() => ConstantExprKind::Tuple { fields: vec![] },
             // It seems we can have ADTs when there is only one variant, and this variant doesn't have any fields.
-            ty::Adt(def, _)
-                if let [variant_def] = &def.variants().raw
-                    && variant_def.fields.is_empty() =>
-            {
-                ConstantExprKind::Adt {
-                    info: get_variant_information(def, rustc_target::abi::FIRST_VARIANT, s),
-                    fields: vec![],
+            ty::Adt(def, _) => {
+                if let [variant_def] = &def.variants().raw {
+                    if variant_def.fields.is_empty() {
+                        ConstantExprKind::Adt {
+                            info: get_variant_information(def, rustc_target::abi::FIRST_VARIANT, s),
+                            fields: vec![],
+                        }
+                    } else {
+                        fatal!(
+                            s[span],
+                            "Unexpected type `ty` for scalar `scalar`. Case `ty::Adt(def, _)`: `variant_def.fields` was not empty";
+                            {ty, scalar, def, variant_def}
+                        )
+                    }
+                } else {
+                    fatal!(
+                        s[span],
+                        "Unexpected type `ty` for scalar `scalar`. Case `ty::Adt(def, _)`: `def.variants().raw` was supposed to contain exactly one variant.";
+                        {ty, scalar, def, &def.variants().raw}
+                    )
                 }
             }
             _ => fatal!(
                 s[span],
-                "Unexpected type {:#?} for scalar {:#?}",
-                ty,
-                scalar
+                "Unexpected type `ty` for scalar `scalar`";
+                {ty, scalar}
             ),
         };
         kind.decorate(ty.sinto(s), cspan)

frontend/exporter/src/lib.rs

@@ -1,12 +1,8 @@
-#![feature(concat_idents)]
-#![feature(trait_alias)]
-#![feature(type_changing_struct_update)]
-#![feature(macro_metavar_expr)]
-#![feature(if_let_guard)]
-#![feature(let_chains)]
-#![allow(incomplete_features)]
-#![feature(specialization)]
 #![allow(rustdoc::private_intra_doc_links)]
+#![cfg_attr(feature = "rustc", feature(type_changing_struct_update))]
+#![cfg_attr(feature = "rustc", feature(macro_metavar_expr))]
+#![cfg_attr(feature = "rustc", feature(concat_idents))]
+#![cfg_attr(feature = "rustc", feature(trait_alias))]
 #![cfg_attr(feature = "rustc", feature(rustc_private))]
 
 macro_rules! cfg_feature_rustc {

frontend/exporter/src/state.rs

@@ -235,9 +235,14 @@ pub fn with_owner_id<'tcx, THIR, MIR>(
 }
 
 pub trait BaseState<'tcx> = HasBase<'tcx> + Clone + IsState<'tcx>;
+
 /// State of anything below a `owner_id`
 pub trait UnderOwnerState<'tcx> = BaseState<'tcx> + HasOwnerId;
 
+/// While translating expressions, we expect to always have a THIR
+/// body and an `owner_id` in the state
+pub trait ExprState<'tcx> = UnderOwnerState<'tcx> + HasThir<'tcx>;
+
 impl ImplInfos {
     fn from<'tcx>(base: Base<'tcx>, did: rustc_hir::def_id::DefId) -> Self {
         let tcx = base.tcx;

frontend/exporter/src/types/copied.rs

@@ -1322,11 +1322,6 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Stmt> for rustc_middle::thir::StmtId {
     }
 }
 
-/// While translating expressions, we expect to always have a THIR
-/// body and an `owner_id` in the state
-#[cfg(feature = "rustc")]
-pub trait ExprState<'tcx> = UnderOwnerState<'tcx> + HasThir<'tcx>;
-
 #[cfg(feature = "rustc")]
 impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> for rustc_middle::thir::Expr<'tcx> {
     fn sinto(&self, s: &S) -> Expr {
@@ -1338,29 +1333,31 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> for rustc_middle::thir::Expr<'tcx>
             Some(contents) => contents,
             None => match kind {
                 // Introduce intermediate `Cast` from `T` to `U` when casting from a `#[repr(T)]` enum to `U`
-                rustc_middle::thir::ExprKind::Cast { source }
-                    if let rustc_middle::ty::TyKind::Adt(def, _) =
-                        s.thir().exprs[source].ty.kind() =>
-                {
-                    let tcx = s.base().tcx;
-                    let contents = kind.sinto(s);
-                    use crate::rustc_middle::ty::util::IntTypeExt;
-                    let repr_type = tcx
-                        .repr_options_of_def(def.did().expect_local())
-                        .discr_type()
-                        .to_ty(s.base().tcx);
-                    if repr_type == ty {
-                        contents
-                    } else {
-                        ExprKind::Cast {
-                            source: Decorated {
-                                ty: repr_type.sinto(s),
-                                span: span.sinto(s),
-                                contents: Box::new(contents),
-                                hir_id,
-                                attributes: vec![],
-                            },
+                rustc_middle::thir::ExprKind::Cast { source } => {
+                    if let rustc_middle::ty::TyKind::Adt(def, _) = s.thir().exprs[source].ty.kind()
+                    {
+                        let tcx = s.base().tcx;
+                        let contents = kind.sinto(s);
+                        use crate::rustc_middle::ty::util::IntTypeExt;
+                        let repr_type = tcx
+                            .repr_options_of_def(def.did().expect_local())
+                            .discr_type()
+                            .to_ty(s.base().tcx);
+                        if repr_type == ty {
+                            contents
+                        } else {
+                            ExprKind::Cast {
+                                source: Decorated {
+                                    ty: repr_type.sinto(s),
+                                    span: span.sinto(s),
+                                    contents: Box::new(contents),
+                                    hir_id,
+                                    attributes: vec![],
+                                },
+                            }
                         }
+                    } else {
+                        kind.sinto(s)
                     }
                 }
                 rustc_middle::thir::ExprKind::NonHirLiteral { lit, .. } => {