Skip to content

Commit b0d5fa0

Browse files
NadrierilNadrieril
committed
Improve diff precision with a generic tree differ
1 parent 340bf25 commit b0d5fa0

File tree

6 files changed

+422
-126
lines changed

6 files changed

+422
-126
lines changed

‎Cargo.lock

+31-1
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎Cargo.toml

+1
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ nom-supreme = "0.8.0"
2222
serde_json = "1.0.125"
2323
serde = { version = "1.0.208", features = ["derive"] }
2424
serde_yaml = "0.9.34"
25+
strip-ansi-escapes = "0.2.0"
2526
wasm-bindgen = "0.2"
2627
wasm-rs-dbg = "0.1.2"
2728
web-sys = { version = "0.3.70", features = ["console"] }

‎src/analyses/compute_rules.rs

+40-55
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@ use bincode::{Decode, Encode};
22
use serde::{Deserialize, Serialize};
33
use std::cmp::max;
44
use std::collections::HashSet;
5-
use std::fmt::Write;
65

76
use itertools::{EitherOrBoth, Itertools};
87

@@ -315,17 +314,23 @@ enum RenderablePredicate<'a> {
315314
}
316315

317316
impl RenderablePredicate<'_> {
318-
fn display(&self, style: PredicateStyle) -> String {
317+
fn display_to_tree<'d>(&self, a: &'d Arenas<'d>, style: PredicateStyle) -> DisplayTree<'d> {
319318
match self {
320-
RenderablePredicate::Pred(p) => p.display(style),
321-
RenderablePredicate::ExprNotRef(e) => format!("{e} is not a reference"),
322-
RenderablePredicate::TyNotRef(ty) => format!("{ty} is not a reference"),
319+
RenderablePredicate::Pred(p) => p.display_to_tree(a, style),
320+
RenderablePredicate::ExprNotRef(e) => e
321+
.to_string()
322+
.to_display_tree(a)
323+
.then(a, " is not a reference"),
324+
RenderablePredicate::TyNotRef(ty) => ty
325+
.to_string()
326+
.to_display_tree(a)
327+
.then(a, " is not a reference"),
323328
RenderablePredicate::Mutability(e, mtbl) => {
324329
let mtbl = match mtbl {
325330
Mutability::Shared => "read-only",
326331
Mutability::Mutable => "mutable",
327332
};
328-
format!("{e} {mtbl}")
333+
e.to_string().to_display_tree(a).sep_then(a, " ", mtbl)
329334
}
330335
}
331336
}
@@ -448,67 +453,47 @@ impl<'a> TypingRule<'a> {
448453

449454
impl<'a> RenderableTypingRule<'a> {
450455
pub fn display(&self, style: PredicateStyle) -> String {
451-
Self::assemble_pieces(self.display_piecewise(style))
452-
}
453-
454-
pub fn assemble_pieces(
455-
[preconditions_str, bar, name, postconditions_str]: [String; 4],
456-
) -> String {
457-
let mut out = String::new();
458-
let _ = write!(&mut out, "{preconditions_str}\n");
459-
let _ = write!(&mut out, "{bar} \"{name}\"\n");
460-
let _ = write!(&mut out, "{postconditions_str}");
461-
out
456+
let a = &Arenas::default();
457+
self.display_to_tree(a, style).to_string()
462458
}
463459

464-
pub fn display_piecewise(&self, style: PredicateStyle) -> [String; 4] {
465-
let postconditions_str = self
466-
.postconditions
467-
.iter()
468-
.map(|x| x.display(style))
469-
.join(", ");
470-
let preconditions_str = self
471-
.preconditions
472-
.iter()
473-
.map(|x| x.display(style))
474-
.join(", ");
475-
476-
let display_len = if cfg!(target_arch = "wasm32") {
477-
// Compute string length skipping html tags.
478-
|s: &str| {
479-
let mut in_tag = false;
480-
s.chars()
481-
.filter(|&c| {
482-
if c == '<' {
483-
in_tag = true;
484-
false
485-
} else if c == '>' {
486-
in_tag = false;
487-
false
488-
} else {
489-
!in_tag
490-
}
491-
})
492-
.count()
493-
}
494-
} else {
495-
// Compute string length skipping ansi escape codes.
496-
ansi_width::ansi_width
497-
};
498-
460+
pub fn display_to_tree<'d>(&self, a: &'d Arenas<'d>, style: PredicateStyle) -> DisplayTree<'d> {
461+
let preconditions = DisplayTree::sep_by(
462+
a,
463+
", ",
464+
self.preconditions
465+
.iter()
466+
.map(|x| x.display_to_tree(a, style)),
467+
);
468+
let postconditions = DisplayTree::sep_by(
469+
a,
470+
", ",
471+
self.postconditions
472+
.iter()
473+
.map(|x| x.display_to_tree(a, style)),
474+
);
499475
let len = max(
500-
display_len(&preconditions_str),
501-
display_len(&postconditions_str),
476+
preconditions.len_ignoring_markup(),
477+
postconditions.len_ignoring_markup(),
502478
);
503479
let bar = "-".repeat(len);
504480
let name = self.name.display(self.options);
505-
[preconditions_str, bar, name, postconditions_str]
481+
DisplayTree::sep_by(
482+
a,
483+
"\n",
484+
[
485+
preconditions,
486+
DisplayTree::sep2_by(a, bar, " ", format!("\"{name}\"")).ignore_for_diff(),
487+
postconditions,
488+
],
489+
)
506490
}
507491
}
508492

509493
#[test]
510494
/// Compute the rulesets for each known bundle.
511495
fn bundle_rules() -> anyhow::Result<()> {
496+
use std::fmt::Write;
512497
colored::control::set_override(false);
513498

514499
#[derive(Serialize)]

‎src/ast/printer.rs

+59-31
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,9 @@ use std::fmt::{Debug, Display, Write};
33

44
use crate::*;
55

6+
pub mod display_tree;
7+
pub use display_tree::*;
8+
69
pub trait Style {
710
fn green(&self) -> String;
811
fn red(&self) -> String;
@@ -101,17 +104,42 @@ impl BindingMode {
101104
}
102105
}
103106

107+
impl<'d> ToDisplayTree<'d> for Type<'_> {
108+
fn to_display_tree(&self, a: &'d Arenas<'d>) -> DisplayTree<'d> {
109+
match self {
110+
Self::Tuple(tys) => DisplayTree::sep_by(a, ", ", tys.iter())
111+
.surrounded(a, "[", "]")
112+
.tag("ty_list"),
113+
Self::Ref(mutable, ty) => format!("&{mutable}")
114+
.to_display_tree(a)
115+
.then(a, ty)
116+
.tag("ty_ref"),
117+
Self::OtherNonRef(name) | Self::AbstractNonRef(name) | Self::Abstract(name) => {
118+
name.to_display_tree(a)
119+
}
120+
}
121+
}
122+
}
123+
104124
impl<'a> TypingPredicate<'a> {
105125
/// Display as `let ...`.
106126
pub fn display_as_let(&self) -> String {
107127
format!("let {}: {} = {}", self.pat, self.expr.ty, self.expr)
108128
}
109129

110130
pub fn display(&self, style: PredicateStyle) -> String {
131+
let a = &Arenas::default();
132+
self.display_to_tree(a, style).to_string()
133+
}
134+
135+
pub fn display_to_tree<'d>(&self, a: &'d Arenas<'d>, style: PredicateStyle) -> DisplayTree<'d> {
111136
match style {
112-
PredicateStyle::Expression => {
113-
format!("{} @ {}: {}", self.pat, self.expr, self.expr.ty)
114-
}
137+
PredicateStyle::Expression => self
138+
.pat
139+
.to_string()
140+
.to_display_tree(a)
141+
.sep_then(a, " @ ", self.expr.to_string())
142+
.sep_then(a, ": ", self.expr.ty),
115143
PredicateStyle::Sequent {
116144
ty: toi,
117145
show_reference_state,
@@ -148,45 +176,50 @@ impl<'a> TypingPredicate<'a> {
148176
};
149177
pre_turnstile.push(scrut_access.to_string());
150178
}
179+
let pre_turnstile = DisplayTree::sep_by(a, ", ", pre_turnstile);
151180

152181
// Type to display.
153182
let ty = match toi {
154183
TypeOfInterest::UserVisible => {
155-
let mut ty = self.expr.ty.to_string();
184+
let ty = self.expr.ty;
156185
if show_reference_state
157186
&& let Some(BindingMode::ByRef(_)) = self.expr.binding_mode().ok()
187+
&& let Type::Ref(mtbl, sub_ty) = ty
158188
{
159-
if let Some(rest) = ty.strip_prefix("&mut") {
160-
ty = format!("{}{rest}", "&mut".inherited_ref());
161-
} else if let Some(rest) = ty.strip_prefix("&") {
162-
ty = format!("{}{rest}", "&".inherited_ref());
163-
}
189+
// Highlight the inherited reference.
190+
format!("&{mtbl}")
191+
.inherited_ref()
192+
.to_display_tree(a)
193+
.then(a, sub_ty)
194+
.tag("ty_ref")
195+
} else {
196+
ty.to_display_tree(a)
164197
}
165-
ty
166198
}
167199
TypeOfInterest::InMemory => match self.expr.binding_mode().ok() {
168-
Some(BindingMode::ByMove) => self.expr.ty.to_string(),
169-
Some(BindingMode::ByRef(_)) => {
170-
self.expr.reset_binding_mode().unwrap().ty.to_string()
171-
}
200+
Some(BindingMode::ByMove) => self.expr.ty.to_display_tree(a),
201+
Some(BindingMode::ByRef(_)) => self
202+
.expr
203+
.reset_binding_mode()
204+
.unwrap()
205+
.ty
206+
.to_display_tree(a),
172207
None => match self.expr.ty {
173208
Type::Ref(_, inner_ty) => {
174-
format!("{} or {}", self.expr.ty, inner_ty)
209+
format!("{} or {}", self.expr.ty, inner_ty).to_display_tree(a)
175210
}
176-
Type::Abstract(_) => self.expr.ty.to_string(),
211+
Type::Abstract(_) => self.expr.ty.to_display_tree(a),
177212
_ => unreachable!(),
178213
},
179214
},
180215
};
216+
let post_turnstile = self
217+
.pat
218+
.to_string()
219+
.to_display_tree(a)
220+
.sep_then(a, ": ", ty);
181221

182-
let turnstile = if pre_turnstile.is_empty() {
183-
""
184-
} else {
185-
" ⊢ "
186-
};
187-
let pre_turnstile = pre_turnstile.join(", ");
188-
let pat = self.pat;
189-
format!("{pre_turnstile}{turnstile}{pat}: {ty}")
222+
pre_turnstile.sep_then(a, " ⊢ ", post_turnstile)
190223
}
191224
}
192225
}
@@ -268,13 +301,8 @@ impl Display for Pattern<'_> {
268301

269302
impl Display for Type<'_> {
270303
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
271-
match self {
272-
Self::Tuple(tys) => write!(f, "[{}]", tys.iter().format(", ")),
273-
Self::Ref(mutable, ty) => write!(f, "&{mutable}{ty}"),
274-
Self::OtherNonRef(name) | Self::AbstractNonRef(name) | Self::Abstract(name) => {
275-
write!(f, "{name}")
276-
}
277-
}
304+
let a = &Arenas::default();
305+
write!(f, "{}", self.to_display_tree(a))
278306
}
279307
}
280308

0 commit comments

Comments
 (0)