Skip to content

Commit

Permalink
Improve diff precision with a generic tree differ
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril committed Jan 1, 2025
1 parent 340bf25 commit b0d5fa0
Show file tree
Hide file tree
Showing 6 changed files with 422 additions and 126 deletions.
32 changes: 31 additions & 1 deletion Cargo.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ nom-supreme = "0.8.0"
serde_json = "1.0.125"
serde = { version = "1.0.208", features = ["derive"] }
serde_yaml = "0.9.34"
strip-ansi-escapes = "0.2.0"
wasm-bindgen = "0.2"
wasm-rs-dbg = "0.1.2"
web-sys = { version = "0.3.70", features = ["console"] }
Expand Down
95 changes: 40 additions & 55 deletions src/analyses/compute_rules.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@ use bincode::{Decode, Encode};
use serde::{Deserialize, Serialize};
use std::cmp::max;
use std::collections::HashSet;
use std::fmt::Write;

use itertools::{EitherOrBoth, Itertools};

Expand Down Expand Up @@ -315,17 +314,23 @@ enum RenderablePredicate<'a> {
}

impl RenderablePredicate<'_> {
fn display(&self, style: PredicateStyle) -> String {
fn display_to_tree<'d>(&self, a: &'d Arenas<'d>, style: PredicateStyle) -> DisplayTree<'d> {
match self {
RenderablePredicate::Pred(p) => p.display(style),
RenderablePredicate::ExprNotRef(e) => format!("{e} is not a reference"),
RenderablePredicate::TyNotRef(ty) => format!("{ty} is not a reference"),
RenderablePredicate::Pred(p) => p.display_to_tree(a, style),
RenderablePredicate::ExprNotRef(e) => e
.to_string()
.to_display_tree(a)
.then(a, " is not a reference"),
RenderablePredicate::TyNotRef(ty) => ty
.to_string()
.to_display_tree(a)
.then(a, " is not a reference"),
RenderablePredicate::Mutability(e, mtbl) => {
let mtbl = match mtbl {
Mutability::Shared => "read-only",
Mutability::Mutable => "mutable",
};
format!("{e} {mtbl}")
e.to_string().to_display_tree(a).sep_then(a, " ", mtbl)
}
}
}
Expand Down Expand Up @@ -448,67 +453,47 @@ impl<'a> TypingRule<'a> {

impl<'a> RenderableTypingRule<'a> {
pub fn display(&self, style: PredicateStyle) -> String {
Self::assemble_pieces(self.display_piecewise(style))
}

pub fn assemble_pieces(
[preconditions_str, bar, name, postconditions_str]: [String; 4],
) -> String {
let mut out = String::new();
let _ = write!(&mut out, "{preconditions_str}\n");
let _ = write!(&mut out, "{bar} \"{name}\"\n");
let _ = write!(&mut out, "{postconditions_str}");
out
let a = &Arenas::default();
self.display_to_tree(a, style).to_string()
}

pub fn display_piecewise(&self, style: PredicateStyle) -> [String; 4] {
let postconditions_str = self
.postconditions
.iter()
.map(|x| x.display(style))
.join(", ");
let preconditions_str = self
.preconditions
.iter()
.map(|x| x.display(style))
.join(", ");

let display_len = if cfg!(target_arch = "wasm32") {
// Compute string length skipping html tags.
|s: &str| {
let mut in_tag = false;
s.chars()
.filter(|&c| {
if c == '<' {
in_tag = true;
false
} else if c == '>' {
in_tag = false;
false
} else {
!in_tag
}
})
.count()
}
} else {
// Compute string length skipping ansi escape codes.
ansi_width::ansi_width
};

pub fn display_to_tree<'d>(&self, a: &'d Arenas<'d>, style: PredicateStyle) -> DisplayTree<'d> {
let preconditions = DisplayTree::sep_by(
a,
", ",
self.preconditions
.iter()
.map(|x| x.display_to_tree(a, style)),
);
let postconditions = DisplayTree::sep_by(
a,
", ",
self.postconditions
.iter()
.map(|x| x.display_to_tree(a, style)),
);
let len = max(
display_len(&preconditions_str),
display_len(&postconditions_str),
preconditions.len_ignoring_markup(),
postconditions.len_ignoring_markup(),
);
let bar = "-".repeat(len);
let name = self.name.display(self.options);
[preconditions_str, bar, name, postconditions_str]
DisplayTree::sep_by(
a,
"\n",
[
preconditions,
DisplayTree::sep2_by(a, bar, " ", format!("\"{name}\"")).ignore_for_diff(),
postconditions,
],
)
}
}

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

#[derive(Serialize)]
Expand Down
90 changes: 59 additions & 31 deletions src/ast/printer.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,9 @@ use std::fmt::{Debug, Display, Write};

use crate::*;

pub mod display_tree;
pub use display_tree::*;

pub trait Style {
fn green(&self) -> String;
fn red(&self) -> String;
Expand Down Expand Up @@ -101,17 +104,42 @@ impl BindingMode {
}
}

impl<'d> ToDisplayTree<'d> for Type<'_> {
fn to_display_tree(&self, a: &'d Arenas<'d>) -> DisplayTree<'d> {
match self {
Self::Tuple(tys) => DisplayTree::sep_by(a, ", ", tys.iter())
.surrounded(a, "[", "]")
.tag("ty_list"),
Self::Ref(mutable, ty) => format!("&{mutable}")
.to_display_tree(a)
.then(a, ty)
.tag("ty_ref"),
Self::OtherNonRef(name) | Self::AbstractNonRef(name) | Self::Abstract(name) => {
name.to_display_tree(a)
}
}
}
}

impl<'a> TypingPredicate<'a> {
/// Display as `let ...`.
pub fn display_as_let(&self) -> String {
format!("let {}: {} = {}", self.pat, self.expr.ty, self.expr)
}

pub fn display(&self, style: PredicateStyle) -> String {
let a = &Arenas::default();
self.display_to_tree(a, style).to_string()
}

pub fn display_to_tree<'d>(&self, a: &'d Arenas<'d>, style: PredicateStyle) -> DisplayTree<'d> {
match style {
PredicateStyle::Expression => {
format!("{} @ {}: {}", self.pat, self.expr, self.expr.ty)
}
PredicateStyle::Expression => self
.pat
.to_string()
.to_display_tree(a)
.sep_then(a, " @ ", self.expr.to_string())
.sep_then(a, ": ", self.expr.ty),
PredicateStyle::Sequent {
ty: toi,
show_reference_state,
Expand Down Expand Up @@ -148,45 +176,50 @@ impl<'a> TypingPredicate<'a> {
};
pre_turnstile.push(scrut_access.to_string());
}
let pre_turnstile = DisplayTree::sep_by(a, ", ", pre_turnstile);

// Type to display.
let ty = match toi {
TypeOfInterest::UserVisible => {
let mut ty = self.expr.ty.to_string();
let ty = self.expr.ty;
if show_reference_state
&& let Some(BindingMode::ByRef(_)) = self.expr.binding_mode().ok()
&& let Type::Ref(mtbl, sub_ty) = ty
{
if let Some(rest) = ty.strip_prefix("&mut") {
ty = format!("{}{rest}", "&mut".inherited_ref());
} else if let Some(rest) = ty.strip_prefix("&") {
ty = format!("{}{rest}", "&".inherited_ref());
}
// Highlight the inherited reference.
format!("&{mtbl}")
.inherited_ref()
.to_display_tree(a)
.then(a, sub_ty)
.tag("ty_ref")
} else {
ty.to_display_tree(a)
}
ty
}
TypeOfInterest::InMemory => match self.expr.binding_mode().ok() {
Some(BindingMode::ByMove) => self.expr.ty.to_string(),
Some(BindingMode::ByRef(_)) => {
self.expr.reset_binding_mode().unwrap().ty.to_string()
}
Some(BindingMode::ByMove) => self.expr.ty.to_display_tree(a),
Some(BindingMode::ByRef(_)) => self
.expr
.reset_binding_mode()
.unwrap()
.ty
.to_display_tree(a),
None => match self.expr.ty {
Type::Ref(_, inner_ty) => {
format!("{} or {}", self.expr.ty, inner_ty)
format!("{} or {}", self.expr.ty, inner_ty).to_display_tree(a)
}
Type::Abstract(_) => self.expr.ty.to_string(),
Type::Abstract(_) => self.expr.ty.to_display_tree(a),
_ => unreachable!(),
},
},
};
let post_turnstile = self
.pat
.to_string()
.to_display_tree(a)
.sep_then(a, ": ", ty);

let turnstile = if pre_turnstile.is_empty() {
""
} else {
" ⊢ "
};
let pre_turnstile = pre_turnstile.join(", ");
let pat = self.pat;
format!("{pre_turnstile}{turnstile}{pat}: {ty}")
pre_turnstile.sep_then(a, " ⊢ ", post_turnstile)
}
}
}
Expand Down Expand Up @@ -268,13 +301,8 @@ impl Display for Pattern<'_> {

impl Display for Type<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
Self::Tuple(tys) => write!(f, "[{}]", tys.iter().format(", ")),
Self::Ref(mutable, ty) => write!(f, "&{mutable}{ty}"),
Self::OtherNonRef(name) | Self::AbstractNonRef(name) | Self::Abstract(name) => {
write!(f, "{name}")
}
}
let a = &Arenas::default();
write!(f, "{}", self.to_display_tree(a))
}
}

Expand Down
Loading

0 comments on commit b0d5fa0

Please sign in to comment.