Remove Hidden

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,42 +366,28 @@ 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),
 }
 
 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"),
         }
     }
 
     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);
     }

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"),
         }
     }

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"),

creusot/src/util.rs

@@ -195,7 +195,10 @@ pub(crate) fn get_builtin(tcx: TyCtxt, def_id: DefId) -> Option<Symbol> {
 }
 
 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 {