Update PathElem::Impl to store a type

charon/src/assumed.rs

@@ -144,7 +144,7 @@ pub fn get_fun_id_from_name(name: &FunName) -> Option<ullbc_ast::AssumedFunId> {
 /// For instance, many types like box or vec are parameterized (in MIR) by an allocator
 /// (`std::alloc::Allocator`): we ignore it.
 pub fn type_to_used_params(name: &TypeName) -> Option<Vec<bool>> {
-    trace!("{}", name);
+    trace!("{:?}", name);
     match get_type_id_from_name(name) {
         Option::None => Option::None,
         Option::Some(id) => {
@@ -174,7 +174,7 @@ pub struct FunInfo {
 
 /// See the comments for [type_to_used_params]
 pub fn function_to_info(name: &FunName) -> Option<FunInfo> {
-    trace!("{}", name);
+    trace!("{:?}", name);
     match get_fun_id_from_name_full(name) {
         Option::None => Option::None,
         Option::Some(id) => {

charon/src/expressions.rs

@@ -67,9 +67,6 @@ pub enum ProjectionElem {
 pub enum FieldProjKind {
     #[serde(rename = "ProjAdt")]
     Adt(TypeDeclId::Id, Option<VariantId::Id>),
-    /// The option type is assumed (it comes from the standard library)
-    #[serde(rename = "ProjOption")]
-    Option(VariantId::Id),
     /// If we project from a tuple, the projection kind gives the arity of the
     #[serde(rename = "ProjTuple")]
     Tuple(usize),

charon/src/expressions_utils.rs

@@ -126,9 +126,6 @@ impl Place {
                     FieldProjKind::Tuple(_) => {
                         out = format!("({out}).{field_id}");
                     }
-                    FieldProjKind::Option(_) => {
-                        out = format!("({out}).{field_id}");
-                    }
                 },
                 ProjectionElem::Index(i, _) => out = format!("({out})[{}]", ctx.format_object(*i)),
             }

charon/src/gast_utils.rs

@@ -99,7 +99,7 @@ impl TraitDecl {
     where
         C: TypeFormatter,
     {
-        let name = self.name.to_string();
+        let name = self.name.fmt_with_ctx(ctx);
         let (generics, trait_clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx);
         let clauses = fmt_where_clauses_with_ctx(ctx, "", &None, trait_clauses, &self.preds);
 
@@ -172,7 +172,7 @@ impl TraitImpl {
     where
         C: TypeFormatter,
     {
-        let name = self.name.to_string();
+        let name = self.name.fmt_with_ctx(ctx);
         let (generics, trait_clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx);
         let clauses = fmt_where_clauses_with_ctx(ctx, "", &None, trait_clauses, &self.preds);
 
@@ -328,7 +328,7 @@ impl<T> GFunDecl<T> {
         };
 
         // Function name
-        let name = self.name.to_string();
+        let name = self.name.fmt_with_ctx(ctx);
 
         // Generic parameters
         let (params, trait_clauses) = self.signature.generics.fmt_with_ctx_with_trait_clauses(ctx);
@@ -397,7 +397,7 @@ impl<T> GGlobalDecl<T> {
         C: GGlobalDeclFormatter<'a, T>,
     {
         // Decl name
-        let name = self.name.to_string();
+        let name = self.name.fmt_with_ctx(ctx);
 
         // Case disjunction on the presence of a body (transparent/opaque definition)
         match &self.body {

charon/src/index_to_function_calls.rs

@@ -294,7 +294,8 @@ fn transform_st(locals: &mut VarId::Vector<Var>, s: &mut Statement) -> Option<Ve
 pub fn transform(ctx: &TransCtx, funs: &mut FunDecls, globals: &mut GlobalDecls) {
     for (name, b) in iter_function_bodies(funs).chain(iter_global_bodies(globals)) {
         trace!(
-            "# About to transform array/slice index operations to function calls: {name}:\n{}",
+            "# About to transform array/slice index operations to function calls: {}:\n{}",
+            name.fmt_with_ctx(ctx),
             ctx.format_object(&*b)
         );
         let body = &mut b.body;
@@ -303,7 +304,8 @@ pub fn transform(ctx: &TransCtx, funs: &mut FunDecls, globals: &mut GlobalDecls)
         let mut tr = |s: &mut Statement| transform_st(locals, s);
         body.transform(&mut tr);
         trace!(
-            "# After transforming array/slice index operations to function calls: {name}:\n{}",
+            "# After transforming array/slice index operations to function calls: {}:\n{}",
+            name.fmt_with_ctx(ctx),
             ctx.format_object(&*b)
         );
     }

charon/src/insert_assign_return_unit.rs

@@ -34,7 +34,8 @@ fn transform_st(st: &mut Statement) -> Option<Vec<Statement>> {
 fn transform_body(ctx: &TransCtx, name: &Name, body: &mut Option<ExprBody>) {
     if let Some(b) = body.as_mut() {
         trace!(
-            "About to insert assign and return unit in decl: {name}:\n{}",
+            "About to insert assign and return unit in decl: {}:\n{}",
+            name.fmt_with_ctx(ctx),
             ctx.format_object(&*b)
         );
         b.body.transform(&mut transform_st);

charon/src/llbc_ast_utils.rs

@@ -5,15 +5,12 @@ use std::ops::DerefMut;
 
 use crate::common::*;
 use crate::expressions::{MutExprVisitor, Operand, Place, Rvalue};
-use crate::formatter::Formatter;
 use crate::gast_utils::{ExprFormatter, GFunDeclFormatter, GGlobalDeclFormatter};
-use crate::llbc_ast::{
-    Assert, FunDecl, FunDecls, GlobalDecl, GlobalDecls, RawStatement, Statement, Switch,
-};
+use crate::llbc_ast::{Assert, FunDecl, GlobalDecl, RawStatement, Statement, Switch};
 use crate::meta;
 use crate::meta::Meta;
 use crate::types::*;
-use crate::ullbc_ast::{fmt_call, FunDeclId, GlobalDeclId};
+pub use crate::ullbc_ast::fmt_call;
 use crate::values::*;
 use macros::make_generic_in_borrows;
 use serde::ser::SerializeTupleVariant;
@@ -296,18 +293,6 @@ impl Statement {
     }
 }
 
-impl Formatter<FunDeclId::Id> for FunDecls {
-    fn format_object(&self, id: FunDeclId::Id) -> String {
-        self.get(id).unwrap().name.to_string()
-    }
-}
-
-impl Formatter<GlobalDeclId::Id> for GlobalDecls {
-    fn format_object(&self, id: GlobalDeclId::Id) -> String {
-        self.get(id).unwrap().name.to_string()
-    }
-}
-
 impl FunDecl {
     pub fn fmt_with_ctx<'a, C>(&'a self, ctx: &C) -> String
     where

charon/src/names.rs

@@ -2,6 +2,7 @@
 #![allow(dead_code)]
 
 pub use crate::names_utils::*;
+use crate::types::*;
 use macros::generate_index_type;
 use macros::{EnumAsGetters, EnumIsA};
 use serde::Serialize;
@@ -11,8 +12,16 @@ generate_index_type!(Disambiguator);
 /// See the comments for [Name]
 #[derive(Debug, Clone, PartialEq, Eq, Serialize, EnumIsA, EnumAsGetters)]
 pub enum PathElem {
-    Ident(String),
-    Disambiguator(Disambiguator::Id),
+    Ident(String, Disambiguator::Id),
+    Impl(ImplElem),
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
+pub struct ImplElem {
+    pub generics: GenericParams,
+    pub preds: Predicates,
+    pub ty: Ty,
+    pub disambiguator: Disambiguator::Id,
 }
 
 /// An item name/path