diff --git a/engine/lib/concrete_ident/concrete_ident_view.ml b/engine/lib/concrete_ident/concrete_ident_view.ml index 83b0f7960..d3b0d5a4d 100644 --- a/engine/lib/concrete_ident/concrete_ident_view.ml +++ b/engine/lib/concrete_ident/concrete_ident_view.ml @@ -128,12 +128,12 @@ let rec poly : (match List.last_exn (Explicit_def_id.to_def_id did).path with | { data = GlobalAsm; disambiguator } -> into_d did disambiguator | _ -> broken_invariant "last path chunk to be GlobalAsm" did) - | TyParam | ConstParam | InlineConst | LifetimeParam | Closure - | SyntheticCoroutineBody -> + | TyParam | ConstParam | InlineConst | PromotedConst | LifetimeParam + | Closure | SyntheticCoroutineBody -> (* It should be impossible for such items to ever be referenced by anyting in hax. *) broken_invariant - "non (TyParam | ConstParam | InlineConst | LifetimeParam | Closure | \ - SyntheticCoroutineBody) identifier" + "non (TyParam | ConstParam | InlineConst | PromotedConst | \ + LifetimeParam | Closure | SyntheticCoroutineBody) identifier" did in result diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs index 44d18d8a1..4026bf4e9 100644 --- a/engine/names/extract/build.rs +++ b/engine/names/extract/build.rs @@ -67,6 +67,7 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String { DefPathItem::Closure => "Closure".into(), DefPathItem::Ctor => "Ctor".into(), DefPathItem::AnonConst => "AnonConst".into(), + DefPathItem::PromotedConst => "PromotedConst".into(), DefPathItem::TypeNs(None) | DefPathItem::OpaqueTy => "OpaqueTy".into(), } } diff --git a/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js b/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js index 6decb4220..1a42a1c4d 100644 --- a/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js +++ b/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js @@ -364,7 +364,7 @@ let export_record = (fields, path, name) => { let record_expression = fields.map(([field, type, _doc], i) => { if (field == 'index' && name == 'def_id_contents') { // This is a hack to always parse Rust DefId indexes to `(0, 0)` - return 'index = Base.Int64.(zero, zero)'; + return 'index = Base.Int64.(zero, zero, None)'; } let p = [...path, 'field_' + field]; let sub = mk_match('x', ocaml_arms_of_type_expr(type, p), p); diff --git a/frontend/exporter/src/body.rs b/frontend/exporter/src/body.rs index 654093ea9..83e6eac91 100644 --- a/frontend/exporter/src/body.rs +++ b/frontend/exporter/src/body.rs @@ -30,6 +30,14 @@ mod module { pub trait IsBody: Sized + Clone + 'static { fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self; + + /// Reuse a MIR body we already got. Panic if that's impossible. + fn from_mir<'tcx, S: UnderOwnerState<'tcx>>( + _s: &S, + _body: rustc_middle::mir::Body<'tcx>, + ) -> Self { + panic!("Can't convert MIR to the requested body type") + } } pub fn make_fn_def<'tcx, Body: IsBody, S: UnderOwnerState<'tcx>>( @@ -67,6 +75,12 @@ mod module { use super::*; impl IsBody for () { fn body<'tcx, S: UnderOwnerState<'tcx>>(_did: RLocalDefId, _s: &S) -> Self {} + fn from_mir<'tcx, S: UnderOwnerState<'tcx>>( + _s: &S, + _body: rustc_middle::mir::Body<'tcx>, + ) -> Self { + () + } } impl IsBody for ThirBody { fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self { @@ -106,6 +120,20 @@ mod module { }); mir.s_unwrap(s) } + fn from_mir<'tcx, S: UnderOwnerState<'tcx>>( + s: &S, + body: rustc_middle::mir::Body<'tcx>, + ) -> Self { + let body = Rc::new(body.clone()); + let s = &State { + base: s.base(), + owner_id: s.owner_id(), + mir: body.clone(), + binder: (), + thir: (), + }; + body.sinto(s) + } } } diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs index 6f8e48d16..4bcc40d27 100644 --- a/frontend/exporter/src/state.rs +++ b/frontend/exporter/src/state.rs @@ -136,13 +136,21 @@ mod types { type Value = Arc>; } + /// Defines a mapping from types to types, for use with `TypeMap`. + pub struct PromotedFullDefsMapper {} + impl TypeMapper for PromotedFullDefsMapper { + type Value = HashMap>>; + } + /// Per-item cache #[derive(Default)] pub struct ItemCache<'tcx> { /// The translated `DefId`. pub def_id: Option, - /// The translated definitions, generic in the body. + /// The translated definitions, generic in the Body kind. pub full_def: TypeMap, + /// The Promoted constants of this body, if any. + pub promoteds: TypeMap, /// Cache the `Ty` translations. pub tys: HashMap, Ty>, /// Cache the trait resolution engine for each item. diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs index fac5dddb0..56ffc855d 100644 --- a/frontend/exporter/src/types/def_id.rs +++ b/frontend/exporter/src/types/def_id.rs @@ -18,7 +18,7 @@ use crate::prelude::*; use crate::{AdtInto, JsonSchema}; #[cfg(feature = "rustc")] -use {rustc_hir as hir, rustc_span::def_id::DefId as RDefId}; +use {rustc_hir as hir, rustc_hir::def_id::DefId as RDefId, rustc_middle::ty}; pub type Symbol = String; @@ -72,10 +72,29 @@ pub enum MacroKind { Derive, } +/// The id of a promoted MIR constant. +/// +/// Reflects [`rustc_middle::mir::Promoted`]. +#[derive_group(Serializers)] +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)] +#[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema, AdtInto))] +#[cfg_attr(not(feature = "extract_names_mode"), args(, from: rustc_middle::mir::Promoted, state: S as _s))] +pub struct PromotedId { + #[cfg_attr(not(feature = "extract_names_mode"), value(self.as_u32()))] + pub id: u32, +} + +#[cfg(feature = "rustc")] +impl PromotedId { + pub fn as_rust_promoted_id(&self) -> rustc_middle::mir::Promoted { + rustc_middle::mir::Promoted::from_u32(self.id) + } +} + /// Reflects [`rustc_hir::def::DefKind`] #[derive_group(Serializers)] #[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema, AdtInto))] -#[cfg_attr(not(feature = "extract_names_mode"),args(, from: rustc_hir::def::DefKind, state: S as tcx))] +#[cfg_attr(not(feature = "extract_names_mode"), args(, from: rustc_hir::def::DefKind, state: S as tcx))] #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)] pub enum DefKind { Mod, @@ -106,6 +125,9 @@ pub enum DefKind { ForeignMod, AnonConst, InlineConst, + #[cfg_attr(not(feature = "extract_names_mode"), disable_mapping)] + /// Added by hax: promoted constants don't have def_ids in rustc but they do in hax. + PromotedConst, OpaqueTy, Field, LifetimeParam, @@ -117,7 +139,8 @@ pub enum DefKind { SyntheticCoroutineBody, } -/// Reflects [`rustc_hir::def_id::DefId`] +/// Reflects [`rustc_hir::def_id::DefId`], augmented to also give ids to promoted constants (which +/// have their own ad-hoc numbering scheme in rustc for now). #[derive_group(Serializers)] #[derive(Clone, PartialEq, Eq, PartialOrd, Ord)] #[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema))] @@ -132,30 +155,52 @@ pub struct DefIdContents { pub krate: String, pub path: Vec, pub parent: Option, - /// Rustc's `CrateNum` and `DefIndex` raw indexes. This can be - /// useful if one needs to convert a [`DefId`] into a - /// [`rustc_hir::def_id::DefId`]; there is a `From` instance for - /// that purpose. + /// Stores rustc's `CrateNum`, `DefIndex` and `Promoted` raw indices. This can be useful if one + /// needs to convert a [`DefId`] into a [`rustc_hir::def_id::DefId`]. If the promoted id is + /// `Some`, then this `DefId` indicates the nth promoted constant associated with the item, + /// which doesn't have a real `rustc::DefId`. /// - /// **Warning: this `index` field might not be safe to use**. They are - /// valid only for one Rustc sesssion. Please do not rely on those - /// indexes unless you cannot do otherwise. - pub index: (u32, u32), + /// **Warning: this `index` field might not be safe to use**. They are valid only for one Rustc + /// sesssion. Please do not rely on those indices unless you cannot do otherwise. + pub index: (u32, u32, Option), pub is_local: bool, /// The kind of definition this `DefId` points to. pub kind: crate::DefKind, } +#[cfg(feature = "rustc")] +impl DefIdContents { + pub fn make_def_id<'tcx, S: BaseState<'tcx>>(self, s: &S) -> DefId { + let contents = + s.with_global_cache(|cache| id_table::Node::new(self, &mut cache.id_table_session)); + DefId { contents } + } +} + #[cfg(feature = "rustc")] impl DefId { - pub fn to_rust_def_id(&self) -> RDefId { - let (krate, index) = self.index; + /// The rustc def_id corresponding to this item, if there is one. Promoted constants don't have + /// a rustc def_id. + pub fn as_rust_def_id(&self) -> Option { + let (_, _, promoted) = self.index; + match promoted { + None => Some(self.underlying_rust_def_id()), + Some(_) => None, + } + } + /// The def_id of this item or its parent if this is a promoted constant. + pub fn underlying_rust_def_id(&self) -> RDefId { + let (krate, index, _) = self.index; RDefId { krate: rustc_hir::def_id::CrateNum::from_u32(krate), index: rustc_hir::def_id::DefIndex::from_u32(index), } } + pub fn promoted_id(&self) -> Option { + let (_, _, promoted) = self.index; + promoted + } /// Iterate over this element and its parents. pub fn ancestry(&self) -> impl Iterator { @@ -174,6 +219,31 @@ impl DefId { }, }) } + + /// Construct a hax `DefId` for the nth promoted constant of the current item. That `DefId` has + /// no corresponding rustc `DefId`. + pub fn make_promoted_child<'tcx, S: BaseState<'tcx>>( + &self, + s: &S, + promoted_id: PromotedId, + ) -> Self { + let mut path = self.path.clone(); + path.push(DisambiguatedDefPathItem { + data: DefPathItem::PromotedConst, + // Reuse the promoted id as disambiguator, like for inline consts. + disambiguator: promoted_id.id, + }); + let (krate, index, _) = self.index; + let contents = DefIdContents { + krate: self.krate.clone(), + path, + parent: Some(self.clone()), + is_local: self.is_local, + index: (krate, index, Some(promoted_id)), + kind: DefKind::PromotedConst, + }; + contents.make_def_id(s) + } } impl std::ops::Deref for DefId { @@ -197,7 +267,11 @@ impl std::fmt::Debug for DefId { impl std::fmt::Debug for DefId { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { // Use the more legible rustc debug implementation. - write!(f, "{:?}", rustc_span::def_id::DefId::from(self)) + write!(f, "{:?}", self.underlying_rust_def_id())?; + if let Some(promoted) = self.promoted_id() { + write!(f, "::promoted#{}", promoted.id)?; + } + Ok(()) } } @@ -210,6 +284,18 @@ impl std::hash::Hash for DefId { } } +/// Gets the kind of the definition. Can't use `def_kind` directly because this crashes on the +/// crate root. +#[cfg(feature = "rustc")] +pub(crate) fn get_def_kind<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> hir::def::DefKind { + if def_id == rustc_span::def_id::CRATE_DEF_ID.to_def_id() { + // Horrible hack: without this, `def_kind` crashes on the crate root. Presumably some table + // isn't properly initialized otherwise. + let _ = tcx.def_span(def_id); + }; + tcx.def_kind(def_id) +} + #[cfg(feature = "rustc")] pub(crate) fn translate_def_id<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) -> DefId { let tcx = s.base().tcx; @@ -229,13 +315,12 @@ pub(crate) fn translate_def_id<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) index: ( rustc_hir::def_id::CrateNum::as_u32(def_id.krate), rustc_hir::def_id::DefIndex::as_u32(def_id.index), + None, ), is_local: def_id.is_local(), - kind: tcx.def_kind(def_id).sinto(s), + kind: get_def_kind(tcx, def_id).sinto(s), }; - let contents = - s.with_global_cache(|cache| id_table::Node::new(contents, &mut cache.id_table_session)); - DefId { contents } + contents.make_def_id(s) } #[cfg(all(not(feature = "extract_names_mode"), feature = "rustc"))] @@ -250,21 +335,6 @@ impl<'s, S: BaseState<'s>> SInto for RDefId { } } -#[cfg(feature = "rustc")] -impl From<&DefId> for RDefId { - fn from<'tcx>(def_id: &DefId) -> Self { - def_id.to_rust_def_id() - } -} - -// Impl to be able to use hax's `DefId` for many rustc queries. -#[cfg(feature = "rustc")] -impl rustc_middle::query::IntoQueryParam for &DefId { - fn into_query_param(self) -> RDefId { - self.into() - } -} - #[cfg(not(feature = "extract_names_mode"))] pub type Path = Vec; @@ -315,6 +385,8 @@ pub enum DefPathItem { Closure, Ctor, AnonConst, + #[cfg_attr(not(feature = "extract_names_mode"), disable_mapping)] + PromotedConst, OpaqueTy, } diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 2e3fb45ce..6af99486e 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -159,28 +159,6 @@ pub mod mir_kinds { #[cfg(feature = "rustc")] pub use mir_kinds::IsMirKind; -#[derive_group(Serializers)] -#[derive(AdtInto, Clone, Debug, JsonSchema)] -#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_middle::mir::Promoted, state: S as _s)] -pub struct PromotedId { - #[value(self.as_u32())] - pub id: u32, -} - -/// Part of a MIR body that was promoted to be a constant. -#[derive_group(Serializers)] -#[derive(Clone, Debug, JsonSchema)] -pub struct PromotedConstant { - /// The `def_id` of the body this was extracted from. - pub def_id: DefId, - /// The identifier for this sub-body. This is the contents of a `mir::Promoted` identifier. - pub promoted_id: PromotedId, - /// The generics applied to the definition corresponding to `def_id`. - pub args: Vec, - /// The MIR for this sub-body. - pub mir: MirBody<()>, -} - /// The contents of `Operand::Const`. #[derive_group(Serializers)] #[derive(Clone, Debug, JsonSchema)] @@ -195,14 +173,20 @@ pub struct ConstOperand { pub enum ConstOperandKind { /// An evaluated constant represented as an expression. Value(ConstantExpr), - /// A promoted constant, that may not be evaluatable because of generics. - Promoted(PromotedConstant, Option), + /// Part of a MIR body that was promoted to be a constant. May not be evaluatable because of + /// generics. + Promoted { + /// The `def_id` of the constant. Note that rustc does not give a DefId to promoted constants, + /// but we do in hax. + def_id: DefId, + /// The generics applied to the definition corresponding to `def_id`. + args: Vec, + impl_exprs: Vec, + }, } #[cfg(feature = "rustc")] -impl<'tcx, S: UnderOwnerState<'tcx>> SInto - for rustc_middle::mir::ConstOperand<'tcx> -{ +impl<'tcx, S: UnderOwnerState<'tcx>> SInto for mir::ConstOperand<'tcx> { fn sinto(&self, s: &S) -> ConstOperand { let kind = translate_mir_const(s, self.span, self.const_); ConstOperand { @@ -215,14 +199,12 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto /// Retrieve the MIR for a promoted body. #[cfg(feature = "rustc")] -fn get_promoted_mir<'tcx, S: UnderOwnerState<'tcx>>( - s: &S, - uneval: mir::UnevaluatedConst<'tcx>, -) -> PromotedConstant { - let tcx = s.base().tcx; - let promoted_id = uneval.promoted.unwrap(); - let def_id = uneval.def; - let body = if let Some(local_def_id) = def_id.as_local() { +pub fn get_promoted_mir<'tcx>( + tcx: ty::TyCtxt<'tcx>, + def_id: RDefId, + promoted_id: mir::Promoted, +) -> mir::Body<'tcx> { + if let Some(local_def_id) = def_id.as_local() { let (_, promoteds) = tcx.mir_promoted(local_def_id); if !promoteds.is_stolen() { promoteds.borrow()[promoted_id].clone() @@ -231,20 +213,6 @@ fn get_promoted_mir<'tcx, S: UnderOwnerState<'tcx>>( } } else { tcx.promoted_mir(def_id)[promoted_id].clone() - }; - let body = Rc::new(body); - let s = &State { - base: s.base(), - owner_id: s.owner_id(), - mir: body.clone(), - binder: (), - thir: (), - }; - PromotedConstant { - def_id: def_id.sinto(s), - promoted_id: promoted_id.sinto(s), - args: uneval.args.sinto(s), - mir: body.sinto(s), } } @@ -277,10 +245,15 @@ fn translate_mir_const<'tcx, S: UnderOwnerState<'tcx>>( .unwrap_or_else(|| ucv.def.default_span(tcx)), ); match ucv.promoted { - Some(_) => { - let promoted = get_promoted_mir(s, ucv); - let evaluated = eval_mir_constant(s, konst).sinto(s); - Promoted(promoted, evaluated) + Some(promoted) => { + // Construct a def_id for the promoted constant. + let def_id = ucv.def.sinto(s).make_promoted_child(s, promoted.sinto(s)); + let impl_exprs = solve_item_required_traits(s, ucv.def, ucv.args); + Promoted { + def_id, + args: ucv.args.sinto(s), + impl_exprs, + } } None => Value(match translate_constant_reference(s, span, ucv.shrink()) { Some(val) => val, @@ -302,10 +275,10 @@ fn translate_mir_const<'tcx, S: UnderOwnerState<'tcx>>( impl<'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_middle::mir::Const<'tcx> { fn sinto(&self, s: &S) -> ConstantExpr { match translate_mir_const(s, rustc_span::DUMMY_SP, *self) { - ConstOperandKind::Value(val) | ConstOperandKind::Promoted(_, Some(val)) => val, - ConstOperandKind::Promoted(body, None) => fatal!( + ConstOperandKind::Value(val) => val, + ConstOperandKind::Promoted { .. } => fatal!( s, "Cannot convert constant back to an expression"; - {body} + {self} ), } } diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index 8a1825c5a..7c627814e 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -33,54 +33,127 @@ pub struct FullDef { } #[cfg(feature = "rustc")] -fn translate_full_def<'tcx, S, Body>(s: &S, def_id: RDefId) -> FullDef +fn translate_full_def<'tcx, S, Body>(s: &S, def_id: &DefId) -> FullDef where S: BaseState<'tcx>, Body: IsBody + TypeMappable, { let tcx = s.base().tcx; - let def_kind = get_def_kind(tcx, def_id); - let kind = { - let state_with_id = with_owner_id(s.base(), (), (), def_id); - def_kind.sinto(&state_with_id) - }; + let rust_def_id = def_id.underlying_rust_def_id(); + let state_with_id = with_owner_id(s.base(), (), (), rust_def_id); + let source_span; + let attributes; + let visibility; + let lang_item; + let diagnostic_item; + let kind; + match def_id.promoted_id() { + None => { + let def_kind = get_def_kind(tcx, rust_def_id); + kind = def_kind.sinto(&state_with_id); + + source_span = rust_def_id.as_local().map(|ldid| tcx.source_span(ldid)); + attributes = get_def_attrs(tcx, rust_def_id, def_kind).sinto(s); + visibility = get_def_visibility(tcx, rust_def_id, def_kind); + lang_item = s + .base() + .tcx + .as_lang_item(rust_def_id) + .map(|litem| litem.name()) + .sinto(s); + diagnostic_item = tcx.get_diagnostic_name(rust_def_id).sinto(s); + } + + Some(promoted_id) => { + let parent_def = def_id.parent.as_ref().unwrap().full_def::<_, Body>(s); + let parent_param_env = parent_def.param_env().unwrap(); + let param_env = ParamEnv { + generics: TyGenerics { + parent: def_id.parent.clone(), + parent_count: parent_param_env.generics.count_total_params(), + params: vec![], + has_self: false, + has_late_bound_regions: None, + }, + predicates: GenericPredicates { predicates: vec![] }, + }; + let body = get_promoted_mir(tcx, rust_def_id, promoted_id.as_rust_promoted_id()); + source_span = Some(body.span); + + let ty: Ty = body.local_decls[rustc_middle::mir::Local::ZERO] + .ty + .sinto(&state_with_id); + let body = Body::from_mir(&state_with_id, body); + kind = FullDefKind::PromotedConst { + param_env, + ty, + body, + }; + + // None of these make sense for a promoted constant. + attributes = Default::default(); + visibility = Default::default(); + lang_item = Default::default(); + diagnostic_item = Default::default(); + } + } - let source_span = def_id.as_local().map(|ldid| tcx.source_span(ldid)); let source_text = source_span .filter(|source_span| source_span.ctxt().is_root()) .and_then(|source_span| tcx.sess.source_map().span_to_snippet(source_span).ok()); - FullDef { - def_id: def_id.sinto(s), - parent: tcx.opt_parent(def_id).sinto(s), - span: get_def_span(tcx, def_id, def_kind).sinto(s), + def_id: def_id.clone(), + parent: def_id.parent.clone(), + span: def_id.def_span(s), source_span: source_span.sinto(s), source_text, - attributes: get_def_attrs(tcx, def_id, def_kind).sinto(s), - visibility: get_def_visibility(tcx, def_id, def_kind), - lang_item: s - .base() - .tcx - .as_lang_item(def_id) - .map(|litem| litem.name()) - .sinto(s), - diagnostic_item: tcx.get_diagnostic_name(def_id).sinto(s), + attributes, + visibility, + lang_item, + diagnostic_item, kind, } } #[cfg(feature = "rustc")] -impl<'tcx, S, Body> SInto>> for RDefId -where - Body: IsBody + TypeMappable, - S: BaseState<'tcx>, -{ - fn sinto(&self, s: &S) -> Arc> { - if let Some(def) = s.with_item_cache(*self, |cache| cache.full_def.get().cloned()) { +impl DefId { + /// Get the span of the definition of this item. This is the span used in diagnostics when + /// referring to the item. + pub fn def_span<'tcx>(&self, s: &impl BaseState<'tcx>) -> Span { + use DefKind::*; + match &self.kind { + // These kinds cause `def_span` to panic. + ForeignMod => rustc_span::DUMMY_SP, + _ => s.base().tcx.def_span(self.underlying_rust_def_id()), + } + .sinto(s) + } + + /// Get the full definition of this item. + pub fn full_def<'tcx, S, Body>(&self, s: &S) -> Arc> + where + Body: IsBody + TypeMappable, + S: BaseState<'tcx>, + { + let rust_def_id = self.underlying_rust_def_id(); + if let Some(def) = s.with_item_cache(rust_def_id, |cache| match self.promoted_id() { + None => cache.full_def.get().cloned(), + Some(promoted_id) => cache.promoteds.or_default().get(&promoted_id).cloned(), + }) { return def; } - let def = Arc::new(translate_full_def(s, *self)); - s.with_item_cache(*self, |cache| cache.full_def.insert(def.clone())); + let def = Arc::new(translate_full_def(s, self)); + s.with_item_cache(rust_def_id, |cache| match self.promoted_id() { + None => { + cache.full_def.insert(def.clone()); + } + Some(promoted_id) => { + cache + .promoteds + .or_default() + .insert(promoted_id, def.clone()); + } + }); def } } @@ -186,9 +259,11 @@ pub enum FullDefKind { .tcx .associated_items(s.owner_id()) .in_definition_order() - .map(|assoc| (assoc, assoc.def_id)) + .map(|assoc| { + let def_id = assoc.def_id.sinto(s); + (assoc.sinto(s), def_id.full_def(s)) + }) .collect::>() - .sinto(s) )] items: Vec<(AssocItem, Arc>)>, }, @@ -311,6 +386,13 @@ pub enum FullDefKind { #[value(s.owner_id().as_local().map(|ldid| Body::body(ldid, s)))] body: Option, }, + /// A promoted constant, e.g. `&(1 + 2)` + #[disable_mapping] + PromotedConst { + param_env: ParamEnv, + ty: Ty, + body: Body, + }, Static { #[value(get_param_env(s, s.owner_id()))] param_env: ParamEnv, @@ -424,9 +506,8 @@ pub enum ImplAssocItemValue { } impl FullDef { - #[cfg(feature = "rustc")] - pub fn rust_def_id(&self) -> RDefId { - (&self.def_id).into() + pub fn def_id(&self) -> &DefId { + &self.def_id } pub fn kind(&self) -> &FullDefKind { @@ -484,13 +565,15 @@ impl FullDef { _ => vec![], }; // Add inherent impl items if any. - let tcx = s.base().tcx; - for impl_def_id in tcx.inherent_impls(self.rust_def_id()) { - children.extend( - tcx.associated_items(impl_def_id) - .in_definition_order() - .map(|assoc| (assoc.name, assoc.def_id).sinto(s)), - ); + if let Some(rust_def_id) = self.def_id.as_rust_def_id() { + let tcx = s.base().tcx; + for impl_def_id in tcx.inherent_impls(rust_def_id) { + children.extend( + tcx.associated_items(impl_def_id) + .in_definition_order() + .map(|assoc| (assoc.name, assoc.def_id).sinto(s)), + ); + } } children } @@ -517,32 +600,6 @@ impl ImplAssocItem { } } -/// Gets the kind of the definition. -#[cfg(feature = "rustc")] -pub fn get_def_kind<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> RDefKind { - if def_id == rustc_span::def_id::CRATE_DEF_ID.to_def_id() { - // Horrible hack: without this, `def_kind` crashes on the crate root. Presumably some table - // isn't properly initialized otherwise. - let _ = tcx.def_span(def_id); - }; - tcx.def_kind(def_id) -} - -/// Gets the attributes of the definition. -#[cfg(feature = "rustc")] -pub fn get_def_span<'tcx>( - tcx: ty::TyCtxt<'tcx>, - def_id: RDefId, - def_kind: RDefKind, -) -> rustc_span::Span { - use RDefKind::*; - match def_kind { - // These kinds cause `def_span` to panic. - ForeignMod => rustc_span::DUMMY_SP, - _ => tcx.def_span(def_id), - } -} - /// Gets the visibility (`pub` or not) of the definition. Returns `None` for defs that don't have a /// meaningful visibility. #[cfg(feature = "rustc")] @@ -665,9 +722,11 @@ where let items = tcx .associated_items(impl_def_id) .in_definition_order() - .map(|assoc| (assoc, assoc.def_id)) - .collect::>() - .sinto(s); + .map(|assoc| { + let def_id = assoc.def_id.sinto(s); + (assoc.sinto(s), def_id.full_def(s)) + }) + .collect::>(); FullDefKind::InherentImpl { param_env, ty: ty.sinto(s), @@ -695,7 +754,7 @@ where .in_definition_order() .map(|decl_assoc| { let decl_def_id = decl_assoc.def_id; - let decl_def = decl_def_id.sinto(s); + let decl_def = decl_def_id.sinto(s).full_def(s); // Impl exprs required by the item. let required_impl_exprs; let value = match item_map.remove(&decl_def_id) { @@ -711,7 +770,7 @@ where }; ImplAssocItemValue::Provided { - def: impl_assoc.def_id.sinto(s), + def: impl_assoc.def_id.sinto(s).full_def(s), is_override: decl_assoc.defaultness(tcx).has_value(), } } diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index b144f1b42..117bc73ba 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -647,6 +647,13 @@ pub struct TyGenerics { pub has_late_bound_regions: Option, } +#[cfg(feature = "rustc")] +impl TyGenerics { + pub(crate) fn count_total_params(&self) -> usize { + self.parent_count + self.params.len() + } +} + /// This type merges the information from /// `rustc_type_ir::AliasKind` and `ty::AliasTy` #[derive_group(Serializers)] diff --git a/frontend/exporter/src/utils/type_map.rs b/frontend/exporter/src/utils/type_map.rs index f7a3bc3a5..c7e1e0907 100644 --- a/frontend/exporter/src/utils/type_map.rs +++ b/frontend/exporter/src/utils/type_map.rs @@ -34,6 +34,15 @@ impl TypeMap { .map(|val: &mut Box| &mut **val) .and_then(|val: &mut dyn TypeMappable| (val as &mut dyn Any).downcast_mut()) } + pub fn or_default(&mut self) -> &mut M::Value + where + M::Value: Default, + { + if self.get::().is_none() { + self.insert::(Default::default()); + } + self.get_mut().unwrap() + } pub fn insert(&mut self, val: M::Value) -> Option>> { self.data diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap index b46940c46..de45cbda5 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap @@ -58,7 +58,7 @@ Class t_Trait `{v_Self : Type} : Type := Arguments t_Trait:clear implicits. Arguments t_Trait (_). -Instance t_Trait_373159623 : t_Trait ((t_Foo)) := +Instance t_Trait_257736684 : t_Trait ((t_Foo)) := { }.