Skip to content

Commit

Permalink
Merge pull request #268 from HigherOrderCO/feature/sc-608/binding-on-…
Browse files Browse the repository at this point in the history 
…match-arguments-should-not-generate

[sc-608] Refactor pattern matching terms, improve match linearization
  • Loading branch information
@developedby
developedby authored Apr 15, 2024
2 parents 7d5065e + f1270da commit 352d318
Show file tree
Hide file tree
Showing 69 changed files with 806 additions and 699 deletions.
2 changes: 1 addition & 1 deletion src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ pub fn desugar_book(
// Auto match linearization
match opts.linearize_matches {
OptLevel::Disabled => (),
OptLevel::Enabled => ctx.book.linearize_match_lambdas(),
OptLevel::Enabled => ctx.book.linearize_match_binds(),
OptLevel::Extra => ctx.book.linearize_matches(),
}
// Manual match linearization
Expand Down
11 changes: 9 additions & 2 deletions src/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,6 +116,9 @@ enum Mode {
#[command(flatten)]
transform_opts: TransformOpts,

#[arg(short = 'p', help = "Debug and normalization pretty printing")]
pretty: bool,

#[arg(short = 'L', help = "Lazy mode")]
lazy_mode: bool,

Expand Down Expand Up @@ -328,7 +331,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
println!("{}", compile_res.core_book);
}

Mode::Desugar { path, comp_opts, warn_opts, lazy_mode, transform_opts } => {
Mode::Desugar { path, comp_opts, warn_opts, pretty, lazy_mode, transform_opts } => {
let diagnostics_cfg = set_warning_cfg_from_cli(
if lazy_mode { DiagnosticsConfig::default_lazy() } else { DiagnosticsConfig::default_strict() },
lazy_mode,
Expand All @@ -341,7 +344,11 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
let diagnostics = desugar_book(&mut book, opts, diagnostics_cfg, None)?;

eprint!("{diagnostics}");
println!("{book}");
if pretty {
println!("{}", book.display_pretty())
} else {
println!("{book}");
}
}

Mode::Run { lazy_mode, run_opts, pretty, comp_opts, transform_opts, warn_opts, arguments, path } => {
Expand Down
145 changes: 102 additions & 43 deletions src/term/display.rs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use super::{Book, Definition, Name, NumCtr, Pattern, Rule, Tag, Term};
use super::{Book, Definition, Name, Pattern, Rule, Tag, Term};
use crate::maybe_grow;
use std::{fmt, ops::Deref};

Expand Down Expand Up @@ -62,33 +62,36 @@ impl fmt::Display for Term {
Term::App { tag, fun, arg } => {
write!(f, "{}({} {})", tag.display_padded(), fun.display_app(tag), arg)
}
Term::Mat { arg, with, rules } => {
Term::Mat { arg, bnd, with, arms: rules } => {
let with: Box<dyn std::fmt::Display> = if with.is_empty() {
Box::new(display!(""))
} else {
Box::new(display!(" with {}", DisplayJoin(|| with, ", ")))
};
write!(
f,
"match {}{} {{ {} }}",
"match {} = {}{} {{ {} }}",
bnd.as_ref().unwrap(),
arg,
with,
DisplayJoin(|| rules.iter().map(|rule| display!("{}: {}", var_as_str(&rule.0), rule.2)), "; "),
)
}
Term::Swt { arg, with, rules } => {
Term::Swt { arg, bnd, with, pred: _, arms } => {
let with: Box<dyn std::fmt::Display> = if with.is_empty() {
Box::new(display!(""))
} else {
Box::new(display!(" with {}", DisplayJoin(|| with, ", ")))
};
write!(
f,
"switch {}{} {{ {} }}",
arg,
with,
DisplayJoin(|| rules.iter().map(|rule| display!("{}: {}", rule.0, rule.1)), "; "),
)
let arms = DisplayJoin(
|| {
arms.iter().enumerate().map(|(i, rule)| {
display!("{}: {}", if i == arms.len() - 1 { "_".to_string() } else { i.to_string() }, rule)
})
},
"; ",
);
write!(f, "switch {} = {}{} {{ {} }}", bnd.as_ref().unwrap(), arg, with, arms)
}
Term::Ltp { bnd, val, nxt } => {
write!(f, "let ({}) = {}; {}", DisplayJoin(|| bnd.iter().map(var_as_str), ", "), val, nxt)
Expand Down Expand Up @@ -163,15 +166,6 @@ impl fmt::Display for Book {
}
}

impl fmt::Display for NumCtr {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
NumCtr::Num(n) => write!(f, "{n}"),
NumCtr::Succ(_) => write!(f, "_"),
}
}
}

impl fmt::Display for Name {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
self.0.fmt(f)
Expand All @@ -180,11 +174,13 @@ impl fmt::Display for Name {

impl Term {
fn display_app<'a>(&'a self, tag: &'a Tag) -> impl fmt::Display + 'a {
DisplayFn(move |f| match self {
Term::App { tag: tag2, fun, arg } if tag2 == tag => {
write!(f, "{} {}", fun.display_app(tag), arg)
}
_ => write!(f, "{}", self),
maybe_grow(|| {
DisplayFn(move |f| match self {
Term::App { tag: tag2, fun, arg } if tag2 == tag => {
write!(f, "{} {}", fun.display_app(tag), arg)
}
_ => write!(f, "{}", self),
})
})
}
}
Expand All @@ -204,6 +200,31 @@ fn var_as_str(nam: &Option<Name>) -> &str {
nam.as_ref().map_or("*", Name::deref)
}

/* Pretty printing */

impl Book {
pub fn display_pretty(&self) -> impl fmt::Display + '_ {
display!("{}", DisplayJoin(|| self.defs.values().map(|def| def.display_pretty()), "\n\n"))
}
}

impl Definition {
pub fn display_pretty(&self) -> impl fmt::Display + '_ {
display!("{}", DisplayJoin(|| self.rules.iter().map(|x| x.display_pretty(&self.name)), "\n"))
}
}

impl Rule {
pub fn display_pretty<'a>(&'a self, def_name: &'a Name) -> impl fmt::Display + 'a {
display!(
"({}{}) =\n {}",
def_name,
DisplayJoin(|| self.pats.iter().map(|x| display!(" {x}")), ""),
self.body.display_pretty(2)
)
}
}

impl Term {
pub fn display_pretty(&self, tab: usize) -> impl fmt::Display + '_ {
maybe_grow(|| {
Expand All @@ -221,23 +242,44 @@ impl Term {
Term::Lnk { nam } => write!(f, "${nam}"),

Term::Let { nam, val, nxt } => {
write!(f, "let {} = {};\n{}", var_as_str(nam), val.display_pretty(tab), nxt.display_pretty(tab))
write!(
f,
"let {} = {};\n{:tab$}{}",
var_as_str(nam),
val.display_pretty(tab),
"",
nxt.display_pretty(tab)
)
}

Term::Use { nam, val, nxt } => {
write!(f, "use {} = {};\n{}", var_as_str(nam), val.display_pretty(tab), nxt.display_pretty(tab))
write!(
f,
"use {} = {};\n{:tab$}{}",
var_as_str(nam),
val.display_pretty(tab),
"",
nxt.display_pretty(tab)
)
}

Term::App { tag, fun, arg } => {
write!(f, "{}({} {})", tag.display_padded(), fun.display_pretty(tab), arg.display_pretty(tab))
write!(
f,
"{}({} {})",
tag.display_padded(),
fun.display_app_pretty(tag, tab),
arg.display_pretty(tab)
)
}

Term::Ltp { bnd, val, nxt } => {
write!(
f,
"let ({}) = {};\n{}",
"let ({}) = {};\n{:tab$}{}",
DisplayJoin(|| bnd.iter().map(var_as_str), ", "),
val.display_pretty(tab),
"",
nxt.display_pretty(tab),
)
}
Expand All @@ -249,10 +291,11 @@ impl Term {
Term::Dup { tag, bnd, val, nxt } => {
write!(
f,
"let {}{{{}}} = {};\n{}",
"let {}{{{}}} = {};\n{:tab$}{}",
tag.display_padded(),
DisplayJoin(|| bnd.iter().map(var_as_str), " "),
val.display_pretty(tab),
"",
nxt.display_pretty(tab),
)
}
Expand All @@ -274,40 +317,45 @@ impl Term {
write!(f, "({} {} {})", opr, fst.display_pretty(tab), snd.display_pretty(tab))
}

Term::Mat { arg, with, rules } => {
Term::Mat { bnd, arg, with, arms } => {
let with: Box<dyn std::fmt::Display> = if with.is_empty() {
Box::new(DisplayFn(|f| write!(f, "")))
} else {
Box::new(DisplayFn(|f| {
write!(f, "with {}", DisplayJoin(|| with.iter().map(|e| e.to_string()), ", "))
}))
};
writeln!(f, "match {} {}{{", arg.display_pretty(tab), with)?;
for rule in rules {
writeln!(f, "match {} = {} {}{{", var_as_str(bnd), arg.display_pretty(tab), with)?;
for rule in arms {
writeln!(
f,
"{:tab$}{}: {}",
"{:tab$}{}: {};",
"",
var_as_str(&rule.0),
rule.2.display_pretty(tab + 2),
rule.2.display_pretty(tab + 4),
tab = tab + 2
)?;
}
write!(f, "{:tab$}}}", "")?;
Ok(())
}

Term::Swt { arg, with, rules } => {
Term::Swt { bnd, arg, with, pred: _, arms } => {
let with: Box<dyn std::fmt::Display> = if with.is_empty() {
Box::new(DisplayFn(|f| write!(f, "")))
Box::new(display!(""))
} else {
Box::new(DisplayFn(|f| {
write!(f, "with {}", DisplayJoin(|| with.iter().map(|e| e.to_string()), ", "))
}))
Box::new(display!(" with {}", DisplayJoin(|| with, ", ")))
};
writeln!(f, "switch {} {}{{", arg.display_pretty(tab), with)?;
for rule in rules {
writeln!(f, "{:tab$}{}: {}", "", rule.0, rule.1.display_pretty(tab + 2), tab = tab + 2)?;
writeln!(f, "switch {} = {} {}{{", var_as_str(bnd), arg.display_pretty(tab), with)?;
for (i, rule) in arms.iter().enumerate() {
writeln!(
f,
"{:tab$}{}: {};",
"",
if i == arms.len() - 1 { "_".to_string() } else { i.to_string() },
rule.display_pretty(tab + 4),
tab = tab + 2
)?;
}
write!(f, "{:tab$}}}", "")?;
Ok(())
Expand All @@ -322,4 +370,15 @@ impl Term {
})
})
}

fn display_app_pretty<'a>(&'a self, tag: &'a Tag, tab: usize) -> impl fmt::Display + 'a {
maybe_grow(|| {
DisplayFn(move |f| match self {
Term::App { tag: tag2, fun, arg } if tag2 == tag => {
write!(f, "{} {}", fun.display_app_pretty(tag, tab), arg.display_pretty(tab))
}
_ => write!(f, "{}", self.display_pretty(tab)),
})
})
}
}
Loading

0 comments on commit 352d318

Please sign in to comment.