From c46c2d3444132b86bbbea4e04756101c784d9dbd Mon Sep 17 00:00:00 2001 From: Xavier Denis Date: Mon, 8 Apr 2024 14:07:45 +0200 Subject: [PATCH] Remove Hidden --- creusot/src/backend/clone_map.rs | 30 +++++---------------- creusot/src/backend/clone_map/elaborator.rs | 22 +++++++-------- creusot/src/backend/dependency.rs | 4 ++- creusot/src/util.rs | 5 +++- 4 files changed, 23 insertions(+), 38 deletions(-) diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs index 7b9eacceef..2e33d6c357 100644 --- a/creusot/src/backend/clone_map.rs +++ b/creusot/src/backend/clone_map.rs @@ -138,10 +138,9 @@ impl<'tcx> Namer<'tcx> for Dependencies<'tcx> { node = DepNode::Type(Ty::new_closure(self.tcx, def_id, subst)); } - let name = item_name(self.tcx, def_id, Namespace::TypeNS); match self.tcx.def_kind(def_id) { DefKind::AssocTy => self.insert(node).qname(), - _ => self.insert(node).qname() , + _ => self.insert(node).qname(), } } @@ -194,10 +193,7 @@ impl<'tcx> Namer<'tcx> for Dependencies<'tcx> { let clone = self.insert(node); match util::item_type(tcx, def_id) { ItemType::Closure => clone.qname(), - ItemType::Type => { - let ident = node.base_ident(tcx); - clone.qname_ident(util::ident_of(ident)) - } + ItemType::Type => clone.qname(), _ => panic!("accessor: invalid item kind"), } } @@ -370,9 +366,9 @@ impl<'tcx> DepGraph<'tcx> { // TODO: Get rid of the enum #[derive(Clone, Copy, Debug, PartialEq, Eq, TyEncodable, TyDecodable, Hash)] enum Kind { + /// This symbol is locally defined Named(Symbol), - // Unclear why we need to keep `Hidden` around - Hidden(Symbol), + /// This symbol must be acompanied by a `Use` statement in Why3 Used(Symbol, Symbol), } @@ -380,7 +376,6 @@ impl Kind { fn ident(&self) -> Ident { match self { Kind::Named(nm) => nm.as_str().into(), - Kind::Hidden(nm) => nm.as_str().into(), Kind::Used(_, _) => panic!("cannot get ident of used module"), } } @@ -388,24 +383,11 @@ impl Kind { fn qname(&self) -> QName { match self { Kind::Named(nm) => nm.as_str().into(), - Kind::Hidden(nm) => nm.as_str().into(), Kind::Used(modl, id) => { QName { module: vec![modl.as_str().into()], name: id.as_str().into() } } } } - - // TODO: Get rid - fn qname_ident(&self, method: Ident) -> QName { - let module = match &self { - Kind::Named(name) => vec![name.to_string().into()], - Kind::Hidden(_) => Vec::new(), - Kind::Used(modl, _) => { - return QName { module: vec![modl.to_string().into()], name: method } - } - }; - QName { module, name: method } - } } #[derive(Clone, Copy, Debug, PartialEq, Eq, TyEncodable, TyDecodable)] @@ -469,7 +451,7 @@ impl<'tcx> Dependencies<'tcx> { for i in self_ids { let node = DepNode::from_trans_id(tcx, i); - deps.names.names.insert(node, Kind::Hidden(node.base_ident(tcx))); + deps.names.names.insert(node, Kind::Named(node.base_ident(tcx))); deps.levels.insert(node, CloneLevel::Body); deps.hidden.insert(node); } @@ -480,7 +462,7 @@ impl<'tcx> Dependencies<'tcx> { // Hack: for closure ty decls pub(crate) fn insert_hidden_type(&mut self, ty: Ty<'tcx>) { let node = DepNode::Type(ty); - self.names.names.insert(node, Kind::Hidden(node.base_ident(self.tcx))); + self.names.names.insert(node, Kind::Named(node.base_ident(self.tcx))); self.levels.insert(node, CloneLevel::Body); self.hidden.insert(node); } diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs index ad21f8caf2..dad48886ad 100644 --- a/creusot/src/backend/clone_map/elaborator.rs +++ b/creusot/src/backend/clone_map/elaborator.rs @@ -8,7 +8,8 @@ use rustc_span::Symbol; use rustc_target::abi::FieldIdx; use why3::{ - declaration::{Axiom, Decl, LetDecl, LetKind, Signature, Use, ValDecl}, Ident, QName + declaration::{Axiom, Decl, LetDecl, LetKind, Signature, Use, ValDecl}, + Ident, QName, }; use crate::{ @@ -94,11 +95,12 @@ impl<'tcx> SymbolElaborator<'tcx> { } else { let name = names.ty(def_id, subst); let name = name.module_qname(); - let mod_name : Ident = if util::item_type(ctx.tcx, def_id) == ItemType::Closure { - format!("{}_Type", module_name(ctx.tcx, def_id)).into() - } else { - module_name(ctx.tcx, def_id).to_string().into() - }; + let mod_name: Ident = + if util::item_type(ctx.tcx, def_id) == ItemType::Closure { + format!("{}_Type", module_name(ctx.tcx, def_id)).into() + } else { + module_name(ctx.tcx, def_id).to_string().into() + }; Use { name: mod_name.into(), as_: Some(name), export: false } } }); @@ -295,10 +297,9 @@ impl<'tcx> Namer<'tcx> for SymNamer<'tcx> { node = DepNode::Type(Ty::new_closure(self.tcx, def_id, subst)); } - let name = item_name(self.tcx, def_id, Namespace::TypeNS); match self.tcx.def_kind(def_id) { DefKind::AssocTy => self.get(node).ident().into(), - _ => self.insert(node).qname() , + _ => self.insert(node).qname(), } } @@ -351,10 +352,7 @@ impl<'tcx> Namer<'tcx> for SymNamer<'tcx> { let clone = self.get(node); match util::item_type(tcx, def_id) { ItemType::Closure => clone.ident().into(), - ItemType::Type => { - let ident = node.base_ident(tcx); - clone.qname_ident(util::ident_of(ident)) - } + ItemType::Type => clone.qname(), _ => panic!("accessor: invalid item kind"), } } diff --git a/creusot/src/backend/dependency.rs b/creusot/src/backend/dependency.rs index e4a9f01a21..f3295055e6 100644 --- a/creusot/src/backend/dependency.rs +++ b/creusot/src/backend/dependency.rs @@ -173,7 +173,9 @@ impl<'tcx> Dependency<'tcx> { match self { Dependency::Type(ty) => { let nm = match ty.kind() { - TyKind::Adt(def, _) => Symbol::intern(&format!("t_{}", tcx.item_name(def.did()))), + TyKind::Adt(def, _) => { + Symbol::intern(&format!("t_{}", tcx.item_name(def.did()))) + } TyKind::Alias(_, aty) => tcx.item_name(aty.def_id), TyKind::Closure(def_id, _) => util::ident_path(tcx, *def_id), _ => Symbol::intern("debug_ty_name"), diff --git a/creusot/src/util.rs b/creusot/src/util.rs index 01883743af..bf636ef816 100644 --- a/creusot/src/util.rs +++ b/creusot/src/util.rs @@ -195,7 +195,10 @@ pub(crate) fn get_builtin(tcx: TyCtxt, def_id: DefId) -> Option { } pub(crate) fn item_qname(ctx: &TranslationCtx, def_id: DefId, ns: Namespace) -> QName { - QName { module: vec![module_name(ctx.tcx, def_id).to_string().into()], name: item_name(ctx.tcx, def_id, ns) } + QName { + module: vec![module_name(ctx.tcx, def_id).to_string().into()], + name: item_name(ctx.tcx, def_id, ns), + } } pub(crate) fn item_name(tcx: TyCtxt, def_id: DefId, ns: Namespace) -> Ident {