HigherOrderCO/Bend
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Bend.git synced 2024-11-05 04:51:40 +03:00
Code Issues Packages Projects Releases Wiki Activity

[sc-436] Separate adt and builtin resugaring into separate passes

Browse Source
This commit is contained in:
Nicolas Abril 2024-02-08 21:24:09 +01:00
parent dc930c0075
commit 25a6926ab1
18 changed files with 459 additions and 371 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
src/lib.rs
View File

@ -11,9 +11,10 @@ use net::{hvmc_to_net::hvmc_to_net, net_to_hvmc::nets_to_hvmc};
use std::time::Instant;
use term::{
book_to_nets,
net_to_term::{net_to_term, ReadbackErrors},
display::display_readback_errors,
net_to_term::net_to_term,
term_to_net::{HvmcNames, Labels},
AdtEncoding, Book, DefName, Name, Term,
AdtEncoding, Book, DefName, Name, ReadbackError, Term,
};
pub mod hvmc_net;
@ -123,11 +124,17 @@ pub fn run_book(
display_warnings(warning_opts, &warnings)?;
let debug_hook = run_opts.debug_hook(&book, &hvmc_names, &labels, &compile_opts.adt_encoding);
// Run
let debug_hook = run_opts.debug_hook(&book, &hvmc_names, &labels);
let (res_lnet, stats) = run_compiled(&core_book, mem_size, run_opts, debug_hook, &book.hvmc_entrypoint());
// Readback
let net = hvmc_to_net(&res_lnet, &hvmc_names.hvmc_to_hvml);
let (res_term, readback_errors) =
net_to_term(&net, &book, &labels, run_opts.linear, compile_opts.adt_encoding);
let (mut res_term, mut readback_errors) = net_to_term(&net, &book, &labels, run_opts.linear);
let resugar_errs = res_term.resugar_adts(&book, compile_opts.adt_encoding);
res_term.resugar_builtins();
readback_errors.extend(resugar_errs);
let info = RunInfo { stats, readback_errors, net: res_lnet };
Ok((res_term, info))
}
@ -204,13 +211,16 @@ impl RunOpts {
book: &'a Book,
hvmc_names: &'a HvmcNames,
labels: &'a Labels,
adt_encoding: &'a AdtEncoding,
) -> Option<impl FnMut(&Net) + 'a> {
self.debug.then_some({
|net: &_| {
let net = hvmc_to_net(net, &hvmc_names.hvmc_to_hvml);
let (res_term, errors) = net_to_term(&net, book, labels, self.linear, *adt_encoding);
println!("{}{}\n---------------------------------------", errors.display(), res_term.display())
let (res_term, errors) = net_to_term(&net, book, labels, self.linear);
println!(
"{}{}\n---------------------------------------",
display_readback_errors(&errors),
res_term.display()
)
}
})
}
@ -316,8 +326,8 @@ impl WarningOpts {
}
/// Filters warnings based on the enabled flags.
pub fn filter<'a>(&'a self, wrns: &'a [Warning], ws: WarnState) -> Vec<&Warning> {
wrns
pub fn filter<'a>(&'a self, warns: &'a [Warning], ws: WarnState) -> Vec<&Warning> {
warns
.iter()
.filter(|w| {
(match w {
@ -378,7 +388,7 @@ impl std::fmt::Display for Warning {
pub struct RunInfo {
pub stats: RunStats,
pub readback_errors: ReadbackErrors,
pub readback_errors: Vec<ReadbackError>,
pub net: Net,
}

4
src/main.rs
View File

@ -2,7 +2,7 @@ use clap::{Args, CommandFactory, Parser, Subcommand};
use hvmc::ast::{show_book, show_net};
use hvml::{
check_book, compile_book, desugar_book, load_file_to_book, run_book,
term::{AdtEncoding, Name},
term::{display::display_readback_errors, AdtEncoding, Name},
CompileOpts, RunInfo, RunOpts, WarnState, WarningOpts,
};
use std::{path::PathBuf, vec::IntoIter};
@ -211,7 +211,7 @@ fn execute_cli_mode(cli: Cli, verbose: &dyn Fn(&hvml::term::Book)) -> Result<(),
println!("\n{}", show_net(&net));
}
println!("{}{}", readback_errors.display(), res_term.display());
println!("{}{}", display_readback_errors(&readback_errors), res_term.display());
if arg_stats {
println!("\nRWTS : {}", total_rewrites);

16
src/net/hvmc_to_net.rs
View File

@ -8,27 +8,27 @@ use hvmc::{
run::Val,
};
pub fn hvmc_to_net(net: &Net, hvmc_to_hvml_name: &HashMap<Val, DefName>) -> INet {
let inodes = hvmc_to_inodes(net, hvmc_to_hvml_name);
pub fn hvmc_to_net(net: &Net, hvmc_to_hvml: &HashMap<Val, DefName>) -> INet {
let inodes = hvmc_to_inodes(net, hvmc_to_hvml);
inodes_to_inet(&inodes)
}
fn hvmc_to_inodes(net: &Net, hvmc_to_hvml_name: &HashMap<Val, DefName>) -> INodes {
fn hvmc_to_inodes(net: &Net, hvmc_to_hvml: &HashMap<Val, DefName>) -> INodes {
let mut inodes = vec![];
let mut n_vars = 0;
let net_root = if let Tree::Var { nam } = &net.root { nam } else { "" };
// If we have a tree attached to the net root, convert that first
if !matches!(&net.root, Tree::Var { .. }) {
let mut root = tree_to_inodes(&net.root, "_".to_string(), net_root, &mut n_vars, hvmc_to_hvml_name);
let mut root = tree_to_inodes(&net.root, "_".to_string(), net_root, &mut n_vars, hvmc_to_hvml);
inodes.append(&mut root);
}
// Convert all the trees forming active pairs.
for (i, (tree1, tree2)) in net.rdex.iter().enumerate() {
let tree_root = format!("a{i}");
let mut tree1 = tree_to_inodes(tree1, tree_root.clone(), net_root, &mut n_vars, hvmc_to_hvml_name);
let mut tree1 = tree_to_inodes(tree1, tree_root.clone(), net_root, &mut n_vars, hvmc_to_hvml);
inodes.append(&mut tree1);
let mut tree2 = tree_to_inodes(tree2, tree_root, net_root, &mut n_vars, hvmc_to_hvml_name);
let mut tree2 = tree_to_inodes(tree2, tree_root, net_root, &mut n_vars, hvmc_to_hvml);
inodes.append(&mut tree2);
}
inodes
@ -39,7 +39,7 @@ fn tree_to_inodes(
tree_root: String,
net_root: &str,
n_vars: &mut NodeId,
hvmc_to_hvml_name: &HashMap<Val, DefName>,
hvmc_to_hvml: &HashMap<Val, DefName>,
) -> INodes {
fn new_var(n_vars: &mut NodeId) -> String {
let new_var = format!("x{n_vars}");
@ -90,7 +90,7 @@ fn tree_to_inodes(
}
Tree::Var { .. } => unreachable!(),
Tree::Ref { nam } => {
let kind = Ref { def_name: hvmc_to_hvml_name[nam].clone() };
let kind = Ref { def_name: hvmc_to_hvml[nam].clone() };
let var = new_var(n_vars);
inodes.push(INode { kind, ports: [subtree_root, var.clone(), var] });
}

45
src/term/display.rs
View File

@ -1,8 +1,7 @@
use std::fmt::{self, Display};
use super::{
net_to_term::{ReadbackError, ReadbackErrors},
Book, DefName, Definition, MatchNum, Name, Op, Pattern, Rule, Tag, Term, Type,
net_to_term::ReadbackError, Book, DefName, Definition, MatchNum, Name, Op, Pattern, Rule, Tag, Term, Type,
};
macro_rules! display {
@ -209,33 +208,31 @@ where
}
}
impl ReadbackErrors {
pub fn display(&self) -> impl fmt::Display + '_ {
DisplayFn(move |f| {
if self.0.is_empty() {
return Ok(());
}
pub fn display_readback_errors(errs: &[ReadbackError]) -> impl fmt::Display + '_ {
DisplayFn(move |f| {
if errs.is_empty() {
return Ok(());
}
writeln!(f, "Readback Warning:")?;
let mut err_counts = std::collections::HashMap::new();
for err in &self.0 {
if err.can_count() {
*err_counts.entry(err).or_insert(0) += 1;
} else {
writeln!(f, "{}", err.display())?;
}
writeln!(f, "Readback Warning:")?;
let mut err_counts = std::collections::HashMap::new();
for err in errs {
if err.can_count() {
*err_counts.entry(err).or_insert(0) += 1;
} else {
writeln!(f, "{}", err.display())?;
}
}
for (err, count) in err_counts {
write!(f, "{}", err.display())?;
if count > 1 {
writeln!(f, " with {} occurrences", count)?;
}
for (err, count) in err_counts {
write!(f, "{}", err.display())?;
if count > 1 {
writeln!(f, " with {} occurrences", count)?;
}
}
writeln!(f)
})
}
writeln!(f)
})
}
impl ReadbackError {

1
src/term/mod.rs
View File

@ -9,7 +9,6 @@ pub mod display;
pub mod load_book;
pub mod net_to_term;
pub mod parser;
pub mod resugar;
pub mod term_to_net;
pub mod transform;

23
src/term/net_to_term.rs
View File

@ -1,8 +1,6 @@
use crate::{
net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT},
term::{
num_to_name, term_to_net::Labels, AdtEncoding, Book, MatchNum, Op, Pattern, Tag, Term, Val, VarName,
},
term::{num_to_name, term_to_net::Labels, Book, MatchNum, Op, Pattern, Tag, Term, Val, VarName},
};
use hvmc::run::Loc;
use indexmap::IndexSet;
@ -10,13 +8,7 @@ use std::collections::{HashMap, HashSet};
// TODO: Display scopeless lambdas as such
/// Converts an Interaction-INet to a Lambda Calculus term
pub fn net_to_term(
net: &INet,
book: &Book,
labels: &Labels,
linear: bool,
adt_encoding: AdtEncoding,
) -> (Term, ReadbackErrors) {
pub fn net_to_term(net: &INet, book: &Book, labels: &Labels, linear: bool) -> (Term, Vec<ReadbackError>) {
let mut reader = Reader {
net,
labels,
@ -47,9 +39,6 @@ pub fn net_to_term(
let result = term.insert_split(split, uses);
debug_assert_eq!(result, None);
}
reader.resugar_adts(&mut term, adt_encoding);
(term, reader.errors)
}
@ -61,7 +50,7 @@ pub struct Reader<'a> {
dup_paths: Option<HashMap<u32, Vec<SlotId>>>,
scope: Scope,
seen: HashSet<Port>,
errors: ReadbackErrors,
errors: Vec<ReadbackError>,
}
impl<'a> Reader<'a> {
@ -276,7 +265,7 @@ impl<'a> Reader<'a> {
}
pub fn error(&mut self, error: ReadbackError) {
self.errors.0.push(error);
self.errors.push(error);
}
}
@ -461,10 +450,6 @@ impl Op {
}
}
#[derive(Default)]
/// A structure that implements display logic for Readback Errors.
pub struct ReadbackErrors(pub Vec<ReadbackError>);
#[derive(Debug)]
pub enum ReadbackError {
InvalidNumericMatch,

275
src/term/resugar.rs
View File

@ -1,275 +0,0 @@
use super::{
net_to_term::{ReadbackError, Reader},
Adt, AdtEncoding, DefName, Pattern, Tag, Term, LCONS, LIST, LNIL, SNIL, STRING,
};
use std::borrow::BorrowMut;
impl<'a> Reader<'a> {
pub fn resugar_adts(&mut self, term: &mut Term, adt_encoding: AdtEncoding) {
match adt_encoding {
// No way of resugaring simple scott encoded terms.
AdtEncoding::Scott => (),
AdtEncoding::TaggedScott => self.resugar_tagged_scott(term),
}
}
pub fn resugar_tagged_scott(&mut self, term: &mut Term) {
match term {
Term::Lam { tag: Tag::Named(adt_name), bod, .. } | Term::Chn { tag: Tag::Named(adt_name), bod, .. } => {
let Some((adt_name, adt)) = self.book.adts.get_key_value(adt_name) else {
return self.resugar_tagged_scott(bod);
};
self.resugar_ctr_tagged_scott(term, adt, adt_name);
match adt_name.0.as_str() {
STRING => {
*term = Self::resugar_string(term);
}
LIST => {
*term = Self::resugar_list(term);
}
_ => {}
}
}
Term::Lam { bod, .. } | Term::Chn { bod, .. } => self.resugar_tagged_scott(bod),
Term::App { tag: Tag::Named(adt_name), fun, arg } => {
let Some((adt_name, adt)) = self.book.adts.get_key_value(adt_name) else {
self.resugar_tagged_scott(fun);
self.resugar_tagged_scott(arg);
return;
};
self.resugar_match_tagged_scott(term, adt_name, adt);
}
Term::App { fun: fst, arg: snd, .. }
| Term::Let { val: fst, nxt: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
self.resugar_tagged_scott(fst);
self.resugar_tagged_scott(snd);
}
Term::Match { scrutinee, arms } => {
self.resugar_tagged_scott(scrutinee);
for (_, arm) in arms {
self.resugar_tagged_scott(arm);
}
}
Term::List { .. } => unreachable!(),
Term::Lnk { .. }
| Term::Num { .. }
| Term::Var { .. }
| Term::Str { .. }
| Term::Ref { .. }
| Term::Era
| Term::Invalid => {}
}
}
/// Reconstructs adt-tagged lambdas as their constructors
///
/// # Example
///
/// ```hvm
/// data Option = (Some val) | None
///
/// // This value:
/// (Some (Some None))
///
/// // Gives the following readback:
/// #Option λa #Option λ* #Option.Some.val (a #Option λb #Option λ* #Option.Some.val (b #Option λ* #Option λc c))
///
/// // Which gets resugared as:
/// (Some (Some None))
/// ```
fn resugar_ctr_tagged_scott(&mut self, term: &mut Term, adt: &Adt, adt_name: &DefName) {
let mut app = &mut *term;
let mut current_arm = None;
for ctr in &adt.ctrs {
self.deref(app);
match app {
Term::Lam { tag: Tag::Named(tag), nam, bod } if tag == adt_name => {
if let Some(nam) = nam {
if current_arm.is_some() {
return self.error(ReadbackError::InvalidAdt);
}
current_arm = Some((nam.clone(), ctr));
}
app = &mut *bod;
}
_ => return self.error(ReadbackError::InvalidAdt),
}
}
let Some((arm_name, (ctr, ctr_args))) = current_arm else {
return self.error(ReadbackError::InvalidAdt);
};
let mut cur = &mut *app;
for field in ctr_args.iter().rev() {
self.deref(cur);
let expected_tag = Tag::adt_field(adt_name, ctr, field);
match cur {
Term::App { tag, .. } if tag == &expected_tag => {
let Term::App { tag, fun, .. } = cur.borrow_mut() else { unreachable!() };
*tag = Tag::Static;
cur = fun;
}
Term::App { tag, .. } => return self.error(ReadbackError::UnexpectedTag(expected_tag, tag.clone())),
_ => return self.error(ReadbackError::InvalidAdt),
}
}
match cur {
Term::Var { nam } if nam == &arm_name => {}
_ => return self.error(ReadbackError::InvalidAdt),
}
*cur = Term::r#ref(ctr);
*term = std::mem::take(app);
self.resugar_tagged_scott(term);
}
/// Reconstructs adt-tagged applications as a match term
///
/// # Example
///
/// ```hvm
/// data Option = (Some val) | None
///
/// // This match expression:
/// Option.and = @a @b match a {
/// Some: match b {
/// Some: 1
/// None: 2
/// }
/// None: 3
/// }
///
/// // Gives the following readback:
/// λa λb (#Option (a #Option.Some.val λ* λc #Option (c #Option.Some.val λ* 1 2) λ* 3) b)
///
/// // Which gets resugared as:
/// λa λb (match a {
/// (Some *): λc match c {
/// (Some *): 1;
/// (None) : 2
/// };
/// (None): λ* 3
/// } b)
/// ```
fn resugar_match_tagged_scott(&mut self, term: &mut Term, adt_name: &DefName, adt: &Adt) {
let mut cur = &mut *term;
let mut arms = Vec::new();
for (ctr, ctr_args) in adt.ctrs.iter().rev() {
self.deref(cur);
match cur {
Term::App { tag: Tag::Named(tag), fun, arg } if tag == adt_name => {
let mut args = Vec::new();
let mut arm = arg.as_mut();
for field in ctr_args {
self.deref(arm);
let expected_tag = Tag::adt_field(adt_name, ctr, field);
match arm {
Term::Lam { tag, .. } if tag == &expected_tag => {
let Term::Lam { nam, bod, .. } = arm.borrow_mut() else { unreachable!() };
args.push(nam.clone().map_or(Pattern::Var(None), |x| Pattern::Var(Some(x))));
arm = bod.as_mut();
}
_ => {
if let Term::Lam { tag, .. } = arm {
self.error(ReadbackError::UnexpectedTag(expected_tag.clone(), tag.clone()));
}
let nam = self.namegen.unique();
args.push(Pattern::Var(Some(nam.clone())));
*arm = Term::tagged_app(expected_tag, std::mem::take(arm), Term::Var { nam });
}
}
}
arms.push((Pattern::Ctr(ctr.clone(), args), arm));
cur = &mut *fun;
}
_ => return self.error(ReadbackError::InvalidAdtMatch),
}
}
let scrutinee = Box::new(std::mem::take(cur));
let arms = arms.into_iter().rev().map(|(pat, term)| (pat, std::mem::take(term))).collect();
*term = Term::Match { scrutinee, arms };
self.resugar_tagged_scott(term);
}
fn resugar_string(term: &mut Term) -> Term {
match term {
// (SCons Num tail)
Term::App { fun: box Term::App { fun: ctr, arg: box Term::Num { val }, .. }, arg: tail, .. } => {
let tail = Self::resugar_string(tail);
let char: String = unsafe { char::from_u32_unchecked(*val as u32) }.into();
match tail {
Term::Str { val: tail } => Term::Str { val: char + &tail },
// (SNil)
Term::Ref { def_name } if def_name.as_str() == SNIL => Term::Str { val: char },
_ => {
// FIXME: warnings are not good with this resugar
// Just make the constructor again
let fun =
Term::App { tag: Tag::Static, fun: ctr.clone(), arg: Box::new(Term::Num { val: *val }) };
Term::App { tag: Tag::Static, fun: Box::new(fun), arg: Box::new(tail) }
}
}
}
other => std::mem::take(other),
}
}
fn resugar_list(term: &mut Term) -> Term {
match term {
// (LCons el tail)
Term::App {
fun: box Term::App { fun: box Term::Ref { def_name: ctr }, arg: el, .. },
arg: tail,
..
} => {
let tail = Self::resugar_list(tail);
if ctr.as_str() == LCONS && let Term::List { els: tail } = tail {
let mut els = vec![*el.clone()];
els.extend(tail);
Term::List { els }
} else {
// Make the constructor again
Term::call(Term::Ref { def_name: ctr.clone() }, [*el.clone(), tail])
}
}
// (LNil)
Term::Ref { def_name } if def_name.as_str() == LNIL => Term::List { els: vec![] },
other => std::mem::take(other),
}
}
fn deref(&mut self, term: &mut Term) {
while let Term::Ref { def_name } = term {
let def = self.book.defs.get(def_name).unwrap();
*term = def.rule().body.clone();
term.fix_names(&mut self.namegen.id_counter, self.book);
}
}
}

39
src/term/transform/encode_pattern_matching.rs
View File

@ -95,24 +95,11 @@ fn make_pattern_matching_case(
let only_var_left = fst_rule.pats[crnt_arg_idx ..].iter().all(|p| matches!(p, Pattern::Var(_)));
let is_fst_rule_irrefutable = all_args_done || only_var_left;
let (new_match, old_matches) = match_path.split_last().unzip();
let old_args: Vec<VarName> = old_matches
.unwrap_or_default()
.iter()
.flat_map(|pat| pat.vars())
.enumerate()
.map(|(i, _)| format!("%x{i}").into())
.collect();
let new_args: Vec<VarName> = new_match
.map(|pat| pat.vars().enumerate().map(|(i, _)| format!("%y{i}").into()).collect())
.unwrap_or(vec![]);
if is_fst_rule_irrefutable {
// First rule will always be selected, generate leaf case.
make_leaf_case(book, fst_rule, fst_rule_idx, match_path, old_args, new_args, adt_encoding)
make_leaf_case(book, fst_rule, fst_rule_idx, match_path, adt_encoding)
} else {
make_match_case(book, def, def_type, crnt_rules, match_path, old_args, new_args, adt_encoding)
make_match_case(book, def, def_type, crnt_rules, match_path, adt_encoding)
}
}
@ -124,8 +111,6 @@ fn make_match_case(
def_type: &[Type],
crnt_rules: Vec<usize>,
match_path: Vec<Pattern>,
old_args: Vec<VarName>,
new_args: Vec<VarName>,
adt_encoding: AdtEncoding,
) -> Term {
let next_arg_idx = match_path.len();
@ -150,6 +135,8 @@ fn make_match_case(
next_cases.push(next_case);
}
let (old_args, new_args) = args_from_match_path(&match_path);
// Encode the current pattern matching, calling the subfunctions
let match_var = VarName::new("x");
// The match term itself
@ -209,10 +196,9 @@ fn make_leaf_case(
rule: &Rule,
rule_idx: usize,
match_path: Vec<Pattern>,
old_args: Vec<VarName>,
new_args: Vec<VarName>,
adt_encoding: AdtEncoding,
) -> Term {
let (old_args, new_args) = args_from_match_path(&match_path);
let args = &mut old_args.iter().chain(new_args.iter()).cloned();
// The term we're building
@ -281,6 +267,21 @@ fn add_arg_lams(
}
}
fn args_from_match_path(match_path: &[Pattern]) -> (Vec<VarName>, Vec<VarName>) {
let (new_match, old_matches) = match_path.split_last().unzip();
let old_args: Vec<VarName> = old_matches
.unwrap_or_default()
.iter()
.flat_map(|pat| pat.vars())
.enumerate()
.map(|(i, _)| format!("%x{i}").into())
.collect();
let new_args: Vec<VarName> = new_match
.map(|pat| pat.vars().enumerate().map(|(i, _)| format!("%y{i}").into()).collect())
.unwrap_or(vec![]);
(old_args, new_args)
}
/* Functions used to normalize generated part of the def */
/// Name for a variable to be substituted with the rule body.

2
src/term/transform/mod.rs
View File

@ -12,6 +12,8 @@ pub mod inline;
pub mod linearize;
pub mod resolve_ctrs_in_pats;
pub mod resolve_refs;
pub mod resugar_adts;
pub mod resugar_builtins;
pub mod simplify_main_ref;
pub mod simplify_ref_to_ref;
pub mod unique_names;

229
src/term/transform/resugar_adts.rs Normal file
View File

@ -0,0 +1,229 @@
use crate::term::{net_to_term::ReadbackError, Adt, AdtEncoding, Book, DefName, Pattern, Tag, Term, VarName};
impl Term {
pub fn resugar_adts(&mut self, book: &Book, adt_encoding: AdtEncoding) -> Vec<ReadbackError> {
let mut errs = Default::default();
match adt_encoding {
// No way of resugaring simple scott encoded terms.
AdtEncoding::Scott => (),
AdtEncoding::TaggedScott => self.resugar_tagged_scott(book, &mut errs),
};
errs
}
fn resugar_tagged_scott(&mut self, book: &Book, errs: &mut Vec<ReadbackError>) {
match self {
Term::Lam { tag: Tag::Named(adt_name), bod, .. } | Term::Chn { tag: Tag::Named(adt_name), bod, .. } => {
if let Some((adt_name, adt)) = book.adts.get_key_value(adt_name) {
self.resugar_ctr_tagged_scott(book, adt, adt_name, errs);
} else {
bod.resugar_tagged_scott(book, errs);
}
}
Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.resugar_tagged_scott(book, errs),
Term::App { tag: Tag::Named(adt_name), fun, arg } => {
if let Some((adt_name, adt)) = book.adts.get_key_value(adt_name) {
self.resugar_match_tagged_scott(book, adt_name, adt, errs);
} else {
fun.resugar_tagged_scott(book, errs);
arg.resugar_tagged_scott(book, errs);
}
}
Term::App { fun: fst, arg: snd, .. }
| Term::Let { val: fst, nxt: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.resugar_tagged_scott(book, errs);
snd.resugar_tagged_scott(book, errs);
}
Term::Match { scrutinee, arms } => {
scrutinee.resugar_tagged_scott(book, errs);
for (_, arm) in arms {
arm.resugar_tagged_scott(book, errs);
}
}
Term::List { .. } => unreachable!(),
Term::Lnk { .. }
| Term::Num { .. }
| Term::Var { .. }
| Term::Str { .. }
| Term::Ref { .. }
| Term::Era
| Term::Invalid => {}
}
}
/// Reconstructs adt-tagged lambdas as their constructors
///
/// # Example
///
/// ```hvm
/// data Option = (Some val) | None
///
/// // This value:
/// (Some (Some None))
///
/// // Gives the following readback:
/// #Option λa #Option λ* #Option.Some.val (a #Option λb #Option λ* #Option.Some.val (b #Option λ* #Option λc c))
///
/// // Which gets resugared as:
/// (Some (Some None))
/// ```
fn resugar_ctr_tagged_scott(
&mut self,
book: &Book,
adt: &Adt,
adt_name: &DefName,
errs: &mut Vec<ReadbackError>,
) {
let mut app = &mut *self;
let mut current_arm = None;
for ctr in &adt.ctrs {
match app {
Term::Lam { tag: Tag::Named(tag), nam, bod } if tag == adt_name => {
if let Some(nam) = nam {
if current_arm.is_some() {
errs.push(ReadbackError::InvalidAdt);
return;
}
current_arm = Some((nam.clone(), ctr));
}
app = bod;
}
_ => {
errs.push(ReadbackError::InvalidAdt);
return;
}
}
}
let Some((arm_name, (ctr, ctr_args))) = current_arm else {
errs.push(ReadbackError::InvalidAdt);
return;
};
let mut cur = &mut *app;
for field in ctr_args.iter().rev() {
let expected_tag = Tag::adt_field(adt_name, ctr, field);
match cur {
Term::App { tag, .. } if tag == &expected_tag => {
let Term::App { tag, fun, .. } = cur else { unreachable!() };
*tag = Tag::Static;
cur = fun.as_mut();
}
Term::App { tag, .. } => {
errs.push(ReadbackError::UnexpectedTag(expected_tag, tag.clone()));
return;
}
_ => {
errs.push(ReadbackError::InvalidAdt);
return;
}
}
}
match cur {
Term::Var { nam } if nam == &arm_name => {}
_ => {
errs.push(ReadbackError::InvalidAdt);
return;
}
}
*cur = Term::r#ref(ctr);
*self = std::mem::take(app);
self.resugar_tagged_scott(book, errs);
}
/// Reconstructs adt-tagged applications as a match term
///
/// # Example
///
/// ```hvm
/// data Option = (Some val) | None
///
/// // This match expression:
/// Option.and = @a @b match a {
/// Some: match b {
/// Some: 1
/// None: 2
/// }
/// None: 3
/// }
///
/// // Gives the following readback:
/// λa λb (#Option (a #Option.Some.val λ* λc #Option (c #Option.Some.val λ* 1 2) λ* 3) b)
///
/// // Which gets resugared as:
/// λa λb (match a {
/// (Some *): λc match c {
/// (Some *): 1;
/// (None) : 2
/// };
/// (None): λ* 3
/// } b)
/// ```
fn resugar_match_tagged_scott(
&mut self,
book: &Book,
adt_name: &DefName,
adt: &Adt,
errs: &mut Vec<ReadbackError>,
) {
let mut cur = &mut *self;
let mut arms = Vec::new();
for (ctr, ctr_args) in adt.ctrs.iter().rev() {
match cur {
Term::App { tag: Tag::Named(tag), fun, arg } if tag == adt_name => {
let mut args = Vec::new();
let mut arm = arg.as_mut();
for field in ctr_args {
let expected_tag = Tag::adt_field(adt_name, ctr, field);
match arm {
Term::Lam { tag, .. } if tag == &expected_tag => {
let Term::Lam { nam, bod, .. } = arm else { unreachable!() };
args.push(nam.clone().map_or(Pattern::Var(None), |x| Pattern::Var(Some(x))));
arm = bod.as_mut();
}
_ => {
if let Term::Lam { tag, .. } = arm {
errs.push(ReadbackError::UnexpectedTag(expected_tag.clone(), tag.clone()));
}
let arg = VarName::from(format!("{ctr}.{field}"));
args.push(Pattern::Var(Some(arg.clone())));
*arm = Term::tagged_app(expected_tag, std::mem::take(arm), Term::Var { nam: arg });
}
}
}
arms.push((Pattern::Ctr(ctr.clone(), args), arm));
cur = &mut *fun;
}
_ => {
errs.push(ReadbackError::InvalidAdtMatch);
return;
}
}
}
let scrutinee = Box::new(std::mem::take(cur));
let arms = arms.into_iter().rev().map(|(pat, term)| (pat, std::mem::take(term))).collect();
*self = Term::Match { scrutinee, arms };
self.resugar_tagged_scott(book, errs);
}
}

132
src/term/transform/resugar_builtins.rs Normal file
View File

@ -0,0 +1,132 @@
use crate::term::{Term, LCONS, LNIL, SCONS, SNIL};
impl Term {
pub fn resugar_builtins(&mut self) {
self.resugar_strings();
self.resugar_lists();
}
/// Rebuilds the String syntax sugar, converting `(SCons 97 SNil)` into `"a"`.
pub fn resugar_strings(&mut self) {
match self {
// (SCons Num tail)
Term::App {
fun: box Term::App { fun: box Term::Ref { def_name: ctr }, arg: box head, .. },
arg: box tail,
..
} => {
head.resugar_strings();
tail.resugar_strings();
let head = std::mem::take(head);
let mut tail = std::mem::take(tail);
if ctr.as_str() == SCONS && let Term::Num{ val } = head && let Term::Str { val: tail } = tail {
// If well formed string, add the next character to the string we're building
let head = unsafe { char::from_u32_unchecked(val as u32) }.to_string();
let str = head + &tail;
*self = Term::Str { val: str }
} else {
// Otherwise rebuild the constructor with the new tail
// Create `(SCons head SNil)` instead of `(SCons head "")`
if tail == (Term::Str { val: String::new() }) {
tail = Term::r#ref(SNIL);
}
*self = Term::call(Term::Ref { def_name: ctr.clone() }, [head, tail]);
}
}
// (SNil)
Term::Ref { def_name } if def_name.as_str() == SNIL => *self = Term::Str { val: String::new() },
Term::Match { scrutinee, arms } => {
scrutinee.resugar_strings();
for (_, arm) in arms {
arm.resugar_strings();
}
}
Term::List { els } => {
for el in els {
el.resugar_strings();
}
}
Term::App { fun: fst, arg: snd, .. }
| Term::Let { val: fst, nxt: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.resugar_strings();
snd.resugar_strings();
}
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
bod.resugar_strings();
}
Term::Lnk { .. }
| Term::Num { .. }
| Term::Var { .. }
| Term::Str { .. }
| Term::Ref { .. }
| Term::Era
| Term::Invalid => {}
}
}
/// Rebuilds the List syntax sugar, converting `(LCons head LNil)` into `[head]`.
pub fn resugar_lists(&mut self) {
match self {
// (LCons el tail)
Term::App {
fun: box Term::App { fun: box Term::Ref { def_name: ctr }, arg: box head, .. },
arg: box tail,
..
} => {
head.resugar_lists();
tail.resugar_lists();
let head = std::mem::take(head);
let tail = std::mem::take(tail);
if ctr.as_str() == LCONS && let Term::List { els: tail } = tail {
// If well formed list, cons the next element to the list being formed
let mut els = vec![head];
els.extend(tail);
*self = Term::List { els };
} else {
*self = Term::call(Term::Ref { def_name: ctr.clone() }, [head, tail]);
}
}
// (LNil)
Term::Ref { def_name } if def_name.as_str() == LNIL => *self = Term::List { els: vec![] },
Term::Match { scrutinee, arms } => {
scrutinee.resugar_lists();
for (_, arm) in arms {
arm.resugar_lists();
}
}
Term::List { els } => {
for el in els {
el.resugar_lists();
}
}
Term::App { fun: fst, arg: snd, .. }
| Term::Let { val: fst, nxt: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.resugar_lists();
snd.resugar_lists();
}
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
bod.resugar_lists();
}
Term::Lnk { .. }
| Term::Num { .. }
| Term::Var { .. }
| Term::Str { .. }
| Term::Ref { .. }
| Term::Era
| Term::Invalid => {}
}
}
}

15
tests/golden_tests.rs
View File

@ -4,8 +4,8 @@ use hvml::{
net::{hvmc_to_net::hvmc_to_net, net_to_hvmc::net_to_hvmc},
run_book,
term::{
load_book::do_parse_book, net_to_term::net_to_term, parser::parse_term, term_to_compat_net,
term_to_net::Labels, AdtEncoding, Book, Name, Term,
display::display_readback_errors, load_book::do_parse_book, net_to_term::net_to_term, parser::parse_term,
term_to_compat_net, term_to_net::Labels, AdtEncoding, Book, Name, Term,
},
CompileOpts, RunOpts, WarningOpts,
};
@ -117,7 +117,7 @@ fn run_file() {
// 1 million nodes for the test runtime. Smaller doesn't seem to make it any faster
let (res, info) =
run_book(book, 1 << 20, RunOpts::default(), WarningOpts::deny_all(), CompileOpts::heavy(), None)?;
Ok(format!("{}{}", info.readback_errors.display(), res.display()))
Ok(format!("{}{}", display_readback_errors(&info.readback_errors), res.display()))
})
}
@ -132,7 +132,7 @@ fn run_lazy() {
// 1 million nodes for the test runtime. Smaller doesn't seem to make it any faster
let (res, info) = run_book(book, 1 << 20, run_opts, WarningOpts::deny_all(), desugar_opts, None)?;
Ok(format!("{}{}", info.readback_errors.display(), res.display()))
Ok(format!("{}{}", display_readback_errors(&info.readback_errors), res.display()))
})
}
@ -142,9 +142,8 @@ fn readback_lnet() {
let net = do_parse_net(code)?;
let book = Book::default();
let compat_net = hvmc_to_net(&net, &Default::default());
let (term, errors) =
net_to_term(&compat_net, &book, &Labels::default(), false, hvml::term::AdtEncoding::TaggedScott);
Ok(format!("{}{}", errors.display(), term.display()))
let (term, errors) = net_to_term(&compat_net, &book, &Labels::default(), false);
Ok(format!("{}{}", display_readback_errors(&errors), term.display()))
})
}
@ -248,6 +247,6 @@ fn run_entrypoint() {
CompileOpts::heavy(),
Some(Name::new("foo")),
)?;
Ok(format!("{}{}", info.readback_errors.display(), res.display()))
Ok(format!("{}{}", display_readback_errors(&info.readback_errors), res.display()))
})
}

4
tests/golden_tests/run_file/readback_list_other_ctr.hvm Normal file
View File

@ -0,0 +1,4 @@
// Check that the ctr in the middle are interpreted correctly
data tup = (pair a b)
main = (LCons (SCons 'a' (pair 'b' (SCons 'c' SNil))) (LCons 1 (pair 2 (LCons 3 (LCons 4 LNil)))))

2
tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap
View File

@ -5,4 +5,4 @@ input_file: tests/golden_tests/run_file/adt_match_wrong_tag.hvm
Readback Warning:
Unexpected tag found during Adt readback, expected '#Option.Some.val', but found '#wrong_tag'
λa match a { (Some c): #Option.Some.val (#wrong_tag λb b c); (None): * }
λa match a { (Some Some.val): #Option.Some.val (#wrong_tag λb b Some.val); (None): * }

2
tests/snapshots/run_file__adt_wrong_tag.hvm.snap
View File

@ -5,4 +5,4 @@ input_file: tests/golden_tests/run_file/adt_wrong_tag.hvm
Readback Warning:
Unexpected tag found during Adt readback, expected '#Option.Some.val', but found '#wrong_tag'
λa match a { (Some c): #Option.Some.val (#wrong_tag λb b c); (None): * }
λa match a { (Some Some.val): #Option.Some.val (#wrong_tag λb b Some.val); (None): * }

5
tests/snapshots/run_file__readback_list_other_ctr.hvm.snap Normal file
View File

@ -0,0 +1,5 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/readback_list_other_ctr.hvm
---
(LCons (SCons 97 (pair 98 "c")) (LCons 1 (pair 2 [3, 4])))

2
tests/snapshots/run_lazy__adt_match_wrong_tag.hvm.snap
View File

@ -5,4 +5,4 @@ input_file: tests/golden_tests/run_lazy/adt_match_wrong_tag.hvm
Readback Warning:
Unexpected tag found during Adt readback, expected '#Option.Some.val', but found '#wrong_tag'
λa match a { (Some c): #Option.Some.val (#wrong_tag λb b c); (None): * }
λa match a { (Some Some.val): #Option.Some.val (#wrong_tag λb b Some.val); (None): * }

2
tests/snapshots/run_lazy__adt_wrong_tag.hvm.snap
View File

@ -5,4 +5,4 @@ input_file: tests/golden_tests/run_lazy/adt_wrong_tag.hvm
Readback Warning:
Unexpected tag found during Adt readback, expected '#Option.Some.val', but found '#wrong_tag'
λa match a { (Some c): #Option.Some.val (#wrong_tag λb b c); (None): * }
λa match a { (Some Some.val): #Option.Some.val (#wrong_tag λb b Some.val); (None): * }