Skip to content

Commit

Permalink
Merge pull request #414 from Nadrieril/printing
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril authored Oct 8, 2024
2 parents 45f5a34 + 02e747a commit 07e94eb
Show file tree
Hide file tree
Showing 47 changed files with 1,693 additions and 1,696 deletions.
32 changes: 11 additions & 21 deletions charon/src/pretty/fmt_with_ctx.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,7 +206,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for FnOperand {

impl<C: AstFormatter> FmtWithCtx<C> for FnPtr {
fn fmt_with_ctx(&self, ctx: &C) -> String {
let generics = self.generics.fmt_with_ctx_split_trait_refs(ctx);
let generics = self.generics.fmt_with_ctx(ctx);
let f = match &self.func {
FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id)) => {
format!("{}", ctx.format_object(*def_id),)
Expand Down Expand Up @@ -280,12 +280,13 @@ impl GenericArgs {
where
C: AstFormatter,
{
assert!(self.trait_refs.is_empty());
let mut params = Vec::new();
let GenericArgs {
regions,
types,
const_generics,
trait_refs,
trait_refs: _,
} = self;
for x in regions {
params.push(x.fmt_with_ctx(ctx));
Expand All @@ -296,9 +297,6 @@ impl GenericArgs {
for x in const_generics {
params.push(x.fmt_with_ctx(ctx));
}
for x in trait_refs {
params.push(x.fmt_with_ctx(ctx))
}
params.join(", ")
}

Expand Down Expand Up @@ -343,11 +341,7 @@ impl GenericArgs {

impl<C: AstFormatter> FmtWithCtx<C> for GenericArgs {
fn fmt_with_ctx(&self, ctx: &C) -> String {
if self.is_empty() {
"".to_string()
} else {
format!("<{}>", self.fmt_with_ctx_no_brackets(ctx),)
}
self.fmt_with_ctx_split_trait_refs(ctx)
}
}

Expand Down Expand Up @@ -671,7 +665,7 @@ where
impl<C: AstFormatter> FmtWithCtx<C> for GlobalDeclRef {
fn fmt_with_ctx(&self, ctx: &C) -> String {
let global_id = ctx.format_object(self.id);
let generics = self.generics.fmt_with_ctx_split_trait_refs(ctx);
let generics = self.generics.fmt_with_ctx(ctx);
format!("{global_id}{generics}")
}
}
Expand Down Expand Up @@ -974,7 +968,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for Rvalue {
format!(
"{{{}{}}} {{{}}}",
ctx.format_object(*fn_id),
generics.fmt_with_ctx_split_trait_refs(ctx),
generics.fmt_with_ctx(ctx),
ops_s.join(", ")
)
}
Expand Down Expand Up @@ -1212,8 +1206,8 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitDecl {
.iter()
.map(|c| {
format!(
"{TAB_INCR}parent_clause_{} : {}\n",
c.clause_id.to_string(),
"{TAB_INCR}parent_clause{} : {}\n",
c.clause_id,
c.fmt_with_ctx(ctx)
)
})
Expand Down Expand Up @@ -1259,7 +1253,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitDecl {
impl<C: AstFormatter> FmtWithCtx<C> for TraitDeclRef {
fn fmt_with_ctx(&self, ctx: &C) -> String {
let trait_id = ctx.format_object(self.trait_id);
let generics = self.generics.fmt_with_ctx_split_trait_refs(ctx);
let generics = self.generics.fmt_with_ctx(ctx);
format!("{trait_id}{generics}")
}
}
Expand Down Expand Up @@ -1332,11 +1326,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitRefKind {
TraitRefKind::SelfId => "Self".to_string(),
TraitRefKind::ParentClause(id, _decl_id, clause_id) => {
let id = id.fmt_with_ctx(ctx);
// Using on purpose [to_pretty_string] instead of [format_object]:
// the clause is local to the associated type, so it should not
// be referenced in the current context.
let clause = clause_id.to_pretty_string();
format!("(parents({id})::[{clause}])")
format!("{id}::parent_clause{clause_id}")
}
TraitRefKind::ItemClause(id, _decl_id, type_name, clause_id) => {
let id = id.fmt_with_ctx(ctx);
Expand All @@ -1348,7 +1338,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitRefKind {
}
TraitRefKind::TraitImpl(id, args) => {
let impl_ = ctx.format_object(*id);
let args = args.fmt_with_ctx_split_trait_refs(ctx);
let args = args.fmt_with_ctx(ctx);
format!("{impl_}{args}")
}
TraitRefKind::Clause(id) => ctx.format_object(*id),
Expand Down
8 changes: 4 additions & 4 deletions charon/tests/cargo/dependencies.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@ trait core::marker::Tuple<Self>

trait core::ops::function::FnOnce<Self, Args>
{
parent_clause_0 : [@TraitClause0]: core::marker::Sized<Args>
parent_clause_1 : [@TraitClause1]: core::marker::Tuple<Args>
parent_clause_2 : [@TraitClause2]: core::marker::Sized<Self::Output>
parent_clause0 : [@TraitClause0]: core::marker::Sized<Args>
parent_clause1 : [@TraitClause1]: core::marker::Tuple<Args>
parent_clause2 : [@TraitClause2]: core::marker::Sized<Self::Output>
type Output
fn call_once : core::ops::function::FnOnce::call_once
}
Expand Down Expand Up @@ -95,7 +95,7 @@ fn test_cargo_dependencies::main()
let @18: &'_ (u32); // anonymous local
let @19: &'_ (u32); // anonymous local
let @20: &'_ (u32); // anonymous local
let @21: core::option::Option<core::fmt::Arguments<'_>, core::marker::Sized<core::fmt::Arguments<'_>>>; // anonymous local
let @21: core::option::Option<core::fmt::Arguments<'_>>[core::marker::Sized<core::fmt::Arguments<'_>>]; // anonymous local
let @22: (); // anonymous local
let @23: (); // anonymous local

Expand Down
10 changes: 5 additions & 5 deletions charon/tests/cargo/toml.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,13 @@ enum core::option::Option<T>
| Some(T)


fn core::option::{core::option::Option<T, @TraitClause0>}::is_some<'_0, T>(@1: &'_0 (core::option::Option<T, @TraitClause0>)) -> bool
fn core::option::{core::option::Option<T>[@TraitClause0]}::is_some<'_0, T>(@1: &'_0 (core::option::Option<T>[@TraitClause0])) -> bool
where
// Inherited clauses:
[@TraitClause0]: core::marker::Sized<T>,
{
let @0: bool; // return
let self@1: &'_ (core::option::Option<T, @TraitClause0>); // arg #1
let self@1: &'_ (core::option::Option<T>[@TraitClause0]); // arg #1

match *(self@1) {
1 => {
Expand All @@ -33,13 +33,13 @@ fn test_cargo_toml::main()
{
let @0: (); // return
let @1: bool; // anonymous local
let @2: &'_ (core::option::Option<bool, core::marker::Sized<bool>>); // anonymous local
let @3: core::option::Option<bool, core::marker::Sized<bool>>; // anonymous local
let @2: &'_ (core::option::Option<bool>[core::marker::Sized<bool>]); // anonymous local
let @3: core::option::Option<bool>[core::marker::Sized<bool>]; // anonymous local
let @4: (); // anonymous local

@3 := core::option::Option::Some { 0: const (false) }
@2 := &@3
@1 := core::option::{core::option::Option<T, @TraitClause0>}::is_some<bool>[core::marker::Sized<bool>](move (@2))
@1 := core::option::{core::option::Option<T>[@TraitClause0]}::is_some<bool>[core::marker::Sized<bool>](move (@2))
drop @2
@fake_read(@1)
drop @3
Expand Down
Loading

0 comments on commit 07e94eb

Please sign in to comment.