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

Merge pull request #219 from HigherOrderCO/feature/sc-479/update-encodings-to-make-use-of-hvmc-n-ary

Browse Source 
[sc-479] Update encodings to make use of hvmc n-ary nodes. Add n-ary tups/dups
This commit is contained in:
Nicolas Abril 2024-03-04 15:15:10 +01:00 committed by GitHub
commit 319b2464ac
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
80 changed files with 675 additions and 708 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Cargo.toml
View File

@ -37,4 +37,4 @@ stdext = "0.3.1"
walkdir = "2.3.3"
[profile.test]
opt-level = 2
opt-level = 2

48
src/lib.rs
View File

@ -42,7 +42,7 @@ pub const CORE_BUILTINS: [&str; 3] = ["HVM.log", "HVM.black_box", "HVM.print"];
/// Creates a host with the hvm-core primitive definitions built-in.
/// This needs the book as an Arc because the closure that logs
/// data needs access to the book.
pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, compile_opts: CompileOpts) -> Arc<Mutex<Host>> {
pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, adt_encoding: AdtEncoding) -> Arc<Mutex<Host>> {
let host = Arc::new(Mutex::new(Host::default()));
host.lock().unwrap().insert_def(
"HVM.log",
@ -54,13 +54,8 @@ pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, compile_opts: CompileOp
let host = host.lock().unwrap();
let tree = host.readback_tree(&wire);
let net = hvmc::ast::Net { root: tree, redexes: vec![] };
let net = hvmc_to_net(&net);
let (mut term, mut readback_errors) = net_to_term(&net, &book, &labels, false);
let resugar_errs = term.resugar_adts(&book, compile_opts.adt_encoding);
term.resugar_builtins();
readback_errors.extend(resugar_errs);
println!("{}{}", display_readback_errors(&readback_errors), term);
let (term, errs) = readback_hvmc(&net, &book, &labels, false, adt_encoding);
println!("{}{}", display_readback_errors(&errs), term);
}
}))),
);
@ -74,13 +69,8 @@ pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, compile_opts: CompileOp
let host = host.lock().unwrap();
let tree = host.readback_tree(&wire);
let net = hvmc::ast::Net { root: tree, redexes: vec![] };
let net = hvmc_to_net(&net);
let (mut term, mut readback_errors) = net_to_term(&net, &book, &labels, false);
let resugar_errs = term.resugar_adts(&book, compile_opts.adt_encoding);
term.resugar_builtins();
readback_errors.extend(resugar_errs);
if let Term::Str { ref val } = term {
let (term, _errs) = readback_hvmc(&net, &book, &labels, false, adt_encoding);
if let Term::Str { val } = &term {
println!("{val}");
}
}
@ -208,18 +198,14 @@ pub fn run_book(
// Run
let debug_hook = run_opts.debug_hook(&book, &labels);
let host = create_host(book.clone(), labels.clone(), compile_opts);
let host = create_host(book.clone(), labels.clone(), compile_opts.adt_encoding);
host.lock().unwrap().insert_book(&core_book);
let (res_lnet, stats) = run_compiled(host, mem_size, run_opts, debug_hook, book.hvmc_entrypoint());
// Readback
let net = hvmc_to_net(&res_lnet);
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();
let (res_term, readback_errors) =
readback_hvmc(&res_lnet, &book, &labels, run_opts.linear, compile_opts.adt_encoding);
readback_errors.extend(resugar_errs);
let info = RunInfo { stats, readback_errors, net: res_lnet, book, labels };
Ok((res_term, info))
}
@ -317,6 +303,24 @@ pub fn run_compiled(
})
}
pub fn readback_hvmc(
net: &Net,
book: &Arc<Book>,
labels: &Arc<Labels>,
linear: bool,
adt_encoding: AdtEncoding,
) -> (Term, Vec<ReadbackError>) {
let net = hvmc_to_net(net);
let (mut term, mut readback_errors) = net_to_term(&net, book, labels, linear);
let resugar_errs = term.resugar_adts(book, adt_encoding);
term.resugar_builtins();
readback_errors.extend(resugar_errs);
(term, readback_errors)
}
#[derive(Clone, Copy, Debug, Default)]
pub struct RunOpts {
pub single_core: bool,

13
src/term/builtins.rs
View File

@ -40,13 +40,16 @@ impl Term {
}
Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.encode_builtins(),
Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. }
| Term::Dup { val: fst, nxt: snd, .. } => {
fst.encode_builtins();
snd.encode_builtins();
}
Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.encode_builtins();
}
}
Term::Mat { args, rules } => {
for arg in args {
arg.encode_builtins();
@ -81,15 +84,11 @@ impl Pattern {
match self {
Pattern::Lst(pats) => *self = Self::encode_list(std::mem::take(pats)),
Pattern::Str(str) => *self = Self::encode_str(str),
Pattern::Ctr(_, pats) => {
Pattern::Ctr(_, pats) | Pattern::Tup(pats) => {
for pat in pats {
pat.encode_builtins();
}
}
Pattern::Tup(fst, snd) => {
fst.encode_builtins();
snd.encode_builtins();
}
Pattern::Var(..) | Pattern::Num(..) => {}
}
}

10
src/term/check/ctrs_arities.rs
View File

@ -57,11 +57,7 @@ impl Pattern {
return Err(MatchErr::CtrArityMismatch(name.clone(), found, *expected));
}
}
Pattern::Tup(fst, snd) => {
to_check.push(fst);
to_check.push(snd);
}
Pattern::Lst(els) => {
Pattern::Lst(els) | Pattern::Tup(els) => {
for el in els {
to_check.push(el);
}
@ -94,15 +90,13 @@ impl Term {
nxt.check_ctrs_arities(arities)?;
}
Term::Lst { els } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.check_ctrs_arities(arities)?;
}
}
Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.check_ctrs_arities(arities)?;
snd.check_ctrs_arities(arities)?;

4
src/term/check/match_arity.rs
View File

@ -46,15 +46,13 @@ impl Term {
}
}
Term::Lst { els } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.check_match_arity()?;
}
}
Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. }
| Term::Let { val: fst, nxt: snd, .. } => {
fst.check_match_arity()?;

2
src/term/check/type_check.rs
View File

@ -32,7 +32,7 @@ fn unify(old: Type, new: Type) -> Result<Type, MatchErr> {
(Type::NumSucc(n), Type::Num) => Ok(Type::NumSucc(n)),
(Type::NumSucc(a), Type::NumSucc(b)) if a == b => Ok(Type::NumSucc(a)),
(Type::Tup, Type::Tup) => Ok(Type::Tup),
(Type::Tup(a), Type::Tup(b)) if a == b => Ok(Type::Tup(a)),
(old, new) => Err(MatchErr::TypeMismatch(new, old)),
}

14
src/term/check/unbound_pats.rs
View File

@ -53,11 +53,7 @@ impl Pattern {
}
check.extend(args.iter());
}
Pattern::Tup(fst, snd) => {
check.push(fst);
check.push(snd);
}
Pattern::Lst(args) => args.iter().for_each(|arg| check.push(arg)),
Pattern::Tup(args) | Pattern::Lst(args) => args.iter().for_each(|arg| check.push(arg)),
Pattern::Var(_) | Pattern::Num(_) | Pattern::Str(_) => {}
}
}
@ -85,16 +81,18 @@ impl Term {
rule.body.check_unbound_pats(is_ctr)?;
}
}
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.check_unbound_pats(is_ctr)?;
}
}
Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.check_unbound_pats(is_ctr)?;
snd.check_unbound_pats(is_ctr)?;
}
Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.check_unbound_pats(is_ctr)?,
Term::Lst { .. } => unreachable!(),
Term::Var { .. }
| Term::Lnk { .. }
| Term::Ref { .. }

38
src/term/check/unbound_vars.rs
View File

@ -95,7 +95,9 @@ pub fn check_uses<'a>(
}
}
Term::Chn { nam, bod, .. } => {
globals.entry(nam).or_default().0 += 1;
if let Some(nam) = nam {
globals.entry(nam).or_default().0 += 1;
}
check_uses(bod, scope, globals, errs);
}
Term::Lnk { nam } => {
@ -107,21 +109,27 @@ pub fn check_uses<'a>(
check_uses(nxt, scope, globals, errs);
pop_scope(nam.as_ref(), scope);
}
Term::Dup { fst, snd, val, nxt, .. }
| Term::Let { pat: Pattern::Tup(box Pattern::Var(fst), box Pattern::Var(snd)), val, nxt } => {
Term::Dup { bnd, val, nxt, .. } => {
check_uses(val, scope, globals, errs);
push_scope(fst.as_ref(), scope);
push_scope(snd.as_ref(), scope);
for bnd in bnd.iter() {
push_scope(bnd.as_ref(), scope);
}
check_uses(nxt, scope, globals, errs);
pop_scope(fst.as_ref(), scope);
pop_scope(snd.as_ref(), scope);
for bnd in bnd.iter() {
pop_scope(bnd.as_ref(), scope);
}
}
Term::Let { .. } => unreachable!(),
Term::App { fun, arg, .. } => {
check_uses(fun, scope, globals, errs);
check_uses(arg, scope, globals, errs);
Term::Let { pat, val, nxt } => {
check_uses(val, scope, globals, errs);
for bnd in pat.bind_or_eras() {
push_scope(bnd.as_ref(), scope);
}
check_uses(nxt, scope, globals, errs);
for bnd in pat.bind_or_eras() {
pop_scope(bnd.as_ref(), scope);
}
}
Term::Tup { fst, snd } | Term::Sup { fst, snd, .. } | Term::Opx { fst, snd, .. } => {
Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => {
check_uses(fst, scope, globals, errs);
check_uses(snd, scope, globals, errs);
}
@ -137,7 +145,11 @@ pub fn check_uses<'a>(
rule.pats.iter().flat_map(|p| p.binds()).rev().for_each(|nam| pop_scope(Some(nam), scope));
}
}
Term::Lst { .. } => unreachable!(),
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
check_uses(el, scope, globals, errs);
}
}
Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => (),
}
}

20
src/term/display.rs
View File

@ -47,7 +47,7 @@ impl fmt::Display for Term {
}
Term::Var { nam } => write!(f, "{nam}"),
Term::Chn { tag, nam, bod } => {
write!(f, "{}λ${} {}", tag.display_padded(), nam, bod)
write!(f, "{}λ${} {}", tag.display_padded(), var_as_str(nam), bod)
}
Term::Lnk { nam } => write!(f, "${nam}"),
Term::Let { pat, val, nxt } => {
@ -68,11 +68,11 @@ impl fmt::Display for Term {
),
)
}
Term::Dup { tag, fst, snd, val, nxt } => {
write!(f, "let {}{{{} {}}} = {}; {}", tag, var_as_str(fst), var_as_str(snd), val, nxt)
Term::Dup { tag, bnd, val, nxt } => {
write!(f, "let {}{{{}}} = {}; {}", tag, DisplayJoin(|| bnd.iter().map(var_as_str), " "), val, nxt)
}
Term::Sup { tag, fst, snd } => {
write!(f, "{}{{{} {}}}", tag, fst, snd)
Term::Sup { tag, els } => {
write!(f, "{}{{{}}}", tag, DisplayJoin(|| els, " "))
}
Term::Era => write!(f, "*"),
Term::Num { val } => write!(f, "{val}"),
@ -80,10 +80,8 @@ impl fmt::Display for Term {
Term::Opx { op, fst, snd } => {
write!(f, "({} {} {})", op, fst, snd)
}
Term::Tup { fst, snd } => write!(f, "({}, {})", fst, snd),
Term::Lst { els } => {
write!(f, "[{}]", DisplayJoin(|| els.iter(), ", "),)
}
Term::Tup { els } => write!(f, "({})", DisplayJoin(|| els.iter(), ", "),),
Term::Lst { els } => write!(f, "[{}]", DisplayJoin(|| els.iter(), ", "),),
Term::Err => write!(f, "<Invalid>"),
}
}
@ -109,7 +107,7 @@ impl fmt::Display for Pattern {
write!(f, "({}{})", nam, DisplayJoin(|| pats.iter().map(|p| display!(" {p}")), ""))
}
Pattern::Num(num) => write!(f, "{num}"),
Pattern::Tup(fst, snd) => write!(f, "({}, {})", fst, snd,),
Pattern::Tup(pats) => write!(f, "({})", DisplayJoin(|| pats, ", ")),
Pattern::Lst(pats) => write!(f, "[{}]", DisplayJoin(|| pats, ", ")),
Pattern::Str(str) => write!(f, "\"{str}\""),
}
@ -184,7 +182,7 @@ impl fmt::Display for Type {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Type::Any => write!(f, "any"),
Type::Tup => write!(f, "tup"),
Type::Tup(n) => write!(f, "tup{n}"),
Type::Num => write!(f, "num"),
Type::NumSucc(n) => write!(f, "{n}+"),
Type::Adt(nam) => write!(f, "{nam}"),

261
src/term/mod.rs
View File

@ -80,7 +80,7 @@ pub enum Term {
/// Like a scopeless lambda, where the variable can occur outside the body
Chn {
tag: Tag,
nam: Name,
nam: Option<Name>,
bod: Box<Term>,
},
/// The use of a Channel variable.
@ -98,20 +98,17 @@ pub enum Term {
arg: Box<Term>,
},
Tup {
fst: Box<Term>,
snd: Box<Term>,
els: Vec<Term>,
},
Dup {
tag: Tag,
fst: Option<Name>,
snd: Option<Name>,
bnd: Vec<Option<Name>>,
val: Box<Term>,
nxt: Box<Term>,
},
Sup {
tag: Tag,
fst: Box<Term>,
snd: Box<Term>,
els: Vec<Term>,
},
Num {
val: u64,
@ -140,87 +137,12 @@ pub enum Term {
Err,
}
impl Clone for Term {
fn clone(&self) -> Self {
stacker::maybe_grow(1024 * 32, 1024 * 1024, move || match self {
Self::Lam { tag, nam, bod } => Self::Lam { tag: tag.clone(), nam: nam.clone(), bod: bod.clone() },
Self::Var { nam } => Self::Var { nam: nam.clone() },
Self::Chn { tag, nam, bod } => Self::Chn { tag: tag.clone(), nam: nam.clone(), bod: bod.clone() },
Self::Lnk { nam } => Self::Lnk { nam: nam.clone() },
Self::Let { pat, val, nxt } => Self::Let { pat: pat.clone(), val: val.clone(), nxt: nxt.clone() },
Self::App { tag, fun, arg } => Self::App { tag: tag.clone(), fun: fun.clone(), arg: arg.clone() },
Self::Tup { fst, snd } => Self::Tup { fst: fst.clone(), snd: snd.clone() },
Self::Dup { tag, fst, snd, val, nxt } => {
Self::Dup { tag: tag.clone(), fst: fst.clone(), snd: snd.clone(), val: val.clone(), nxt: nxt.clone() }
}
Self::Sup { tag, fst, snd } => Self::Sup { tag: tag.clone(), fst: fst.clone(), snd: snd.clone() },
Self::Num { val } => Self::Num { val: *val },
Self::Str { val } => Self::Str { val: val.clone() },
Self::Lst { els } => Self::Lst { els: els.clone() },
Self::Opx { op, fst, snd } => Self::Opx { op: *op, fst: fst.clone(), snd: snd.clone() },
Self::Mat { args, rules } => Self::Mat { args: args.clone(), rules: rules.clone() },
Self::Ref { nam } => Self::Ref { nam: nam.clone() },
Self::Era => Self::Era,
Self::Err => Self::Err,
})
}
}
impl Drop for Term {
fn drop(&mut self) {
if matches!(self, Term::Era | Term::Err) {
return;
}
let mut stack = vec![];
self.take_children(&mut stack);
while let Some(mut term) = stack.pop() {
term.take_children(&mut stack)
}
}
}
impl Term {
fn take_children(&mut self, stack: &mut Vec<Term>) {
match self {
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
stack.push(std::mem::take(bod.as_mut()));
}
Term::Let { val: fst, nxt: snd, .. }
| Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
stack.push(std::mem::take(fst.as_mut()));
stack.push(std::mem::take(snd.as_mut()));
}
Term::Mat { args, rules } => {
for arg in std::mem::take(args).into_iter() {
stack.push(arg);
}
for Rule { body, .. } in std::mem::take(rules).into_iter() {
stack.push(body);
}
}
Term::Lst { els } => {
for el in std::mem::take(els).into_iter() {
stack.push(el);
}
}
_ => {}
}
}
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum Pattern {
Var(Option<Name>),
Ctr(Name, Vec<Pattern>),
Num(NumCtr),
Tup(Box<Pattern>, Box<Pattern>),
Tup(Vec<Pattern>),
Lst(Vec<Pattern>),
Str(GlobalString),
}
@ -266,7 +188,7 @@ pub enum Type {
/// Variables/wildcards.
Any,
/// A native tuple.
Tup,
Tup(usize),
/// A sequence of arbitrary numbers ending in a variable.
Num,
/// A strictly incrementing sequence of numbers starting from 0, ending in a + ctr.
@ -299,6 +221,18 @@ impl PartialEq<str> for Name {
}
}
impl PartialEq<Option<Name>> for Name {
fn eq(&self, other: &Option<Name>) -> bool {
if let Some(other) = other.as_ref() { self == other } else { false }
}
}
impl PartialEq<Name> for Option<Name> {
fn eq(&self, other: &Name) -> bool {
other.eq(self)
}
}
pub fn num_to_name(mut num: u64) -> String {
let mut name = String::new();
loop {
@ -316,9 +250,78 @@ impl Tag {
pub fn adt_name(name: &Name) -> Self {
Self::Named(name.clone())
}
}
pub fn adt_field(adt: &Name, ctr: &Name, field: &Name) -> Self {
Self::Named(Name::new(format!("{adt}.{ctr}.{field}")))
impl Clone for Term {
fn clone(&self) -> Self {
stacker::maybe_grow(1024 * 32, 1024 * 1024, move || match self {
Self::Lam { tag, nam, bod } => Self::Lam { tag: tag.clone(), nam: nam.clone(), bod: bod.clone() },
Self::Var { nam } => Self::Var { nam: nam.clone() },
Self::Chn { tag, nam, bod } => Self::Chn { tag: tag.clone(), nam: nam.clone(), bod: bod.clone() },
Self::Lnk { nam } => Self::Lnk { nam: nam.clone() },
Self::Let { pat, val, nxt } => Self::Let { pat: pat.clone(), val: val.clone(), nxt: nxt.clone() },
Self::App { tag, fun, arg } => Self::App { tag: tag.clone(), fun: fun.clone(), arg: arg.clone() },
Self::Tup { els } => Self::Tup { els: els.clone() },
Self::Dup { tag, bnd, val, nxt } => {
Self::Dup { tag: tag.clone(), bnd: bnd.clone(), val: val.clone(), nxt: nxt.clone() }
}
Self::Sup { tag, els } => Self::Sup { tag: tag.clone(), els: els.clone() },
Self::Num { val } => Self::Num { val: *val },
Self::Str { val } => Self::Str { val: val.clone() },
Self::Lst { els } => Self::Lst { els: els.clone() },
Self::Opx { op, fst, snd } => Self::Opx { op: *op, fst: fst.clone(), snd: snd.clone() },
Self::Mat { args, rules } => Self::Mat { args: args.clone(), rules: rules.clone() },
Self::Ref { nam } => Self::Ref { nam: nam.clone() },
Self::Era => Self::Era,
Self::Err => Self::Err,
})
}
}
impl Drop for Term {
fn drop(&mut self) {
impl Term {
fn take_children(&mut self, stack: &mut Vec<Term>) {
match self {
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
stack.push(std::mem::take(bod.as_mut()));
}
Term::Let { val: fst, nxt: snd, .. }
| Term::App { fun: fst, arg: snd, .. }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Opx { fst, snd, .. } => {
stack.push(std::mem::take(fst.as_mut()));
stack.push(std::mem::take(snd.as_mut()));
}
Term::Mat { args, rules } => {
for arg in std::mem::take(args).into_iter() {
stack.push(arg);
}
for Rule { body, .. } in std::mem::take(rules).into_iter() {
stack.push(body);
}
}
Term::Lst { els } | Term::Tup { els } | Term::Sup { els, .. } => {
for el in std::mem::take(els).into_iter() {
stack.push(el);
}
}
_ => {}
}
}
}
if matches!(self, Term::Era | Term::Err) {
return;
}
let mut stack = vec![];
self.take_children(&mut stack);
while let Some(mut term) = stack.pop() {
term.take_children(&mut stack)
}
}
}
@ -416,9 +419,9 @@ impl Term {
nxt.subst(from, to);
}
}
Term::Dup { tag: _, fst, snd, val, nxt } => {
Term::Dup { tag: _, bnd, val, nxt } => {
val.subst(from, to);
if fst.as_ref().map_or(true, |fst| fst != from) && snd.as_ref().map_or(true, |snd| snd != from) {
if bnd.iter().all(|var| var != from) {
nxt.subst(from, to);
}
}
@ -432,11 +435,10 @@ impl Term {
}
}
}
Term::Lst { els } => els.iter_mut().for_each(|el| el.subst(from, to)),
Term::App { fun: fst, arg: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Tup { fst, snd }
| Term::Opx { fst, snd, .. } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
els.iter_mut().for_each(|el| el.subst(from, to))
}
Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => {
fst.subst(from, to);
snd.subst(from, to);
}
@ -454,13 +456,13 @@ impl Term {
args.iter_mut().for_each(|arg| arg.subst_unscoped(from, to));
rules.iter_mut().for_each(|rule| rule.body.subst_unscoped(from, to));
}
Term::Lst { els } => els.iter_mut().for_each(|el| el.subst_unscoped(from, to)),
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
els.iter_mut().for_each(|el| el.subst_unscoped(from, to))
}
Term::Chn { bod, .. } | Term::Lam { bod, .. } => bod.subst_unscoped(from, to),
Term::App { fun: fst, arg: snd, .. }
| Term::Let { val: fst, nxt: snd, .. }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Tup { fst, snd }
| Term::Opx { fst, snd, .. } => {
fst.subst(from, to);
snd.subst(from, to);
@ -503,21 +505,19 @@ impl Term {
free_vars.extend(new_scope);
}
Term::Dup { fst, snd, val, nxt, .. } => {
Term::Dup { bnd, val, nxt, .. } => {
go(val, free_vars);
let mut new_scope = Default::default();
go(nxt, &mut new_scope);
fst.as_ref().map(|fst| new_scope.remove(fst));
snd.as_ref().map(|snd| new_scope.remove(snd));
for bnd in bnd.iter().flatten() {
new_scope.remove(bnd);
}
free_vars.extend(new_scope);
}
Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Sup { fst, snd, .. }
| Term::Opx { op: _, fst, snd } => {
Term::App { fun: fst, arg: snd, .. } | Term::Opx { op: _, fst, snd } => {
go(fst, free_vars);
go(snd, free_vars);
}
@ -536,11 +536,9 @@ impl Term {
free_vars.extend(new_scope);
}
}
Term::Lst { els } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
let mut fvs = Default::default();
go(el, &mut fvs);
free_vars.extend(fvs);
go(el, free_vars);
}
}
Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {}
@ -557,7 +555,9 @@ impl Term {
fn go(term: &Term, decls: &mut IndexSet<Name>, uses: &mut IndexSet<Name>) {
match term {
Term::Chn { tag: _, nam, bod } => {
decls.insert(nam.clone());
if let Some(nam) = nam {
decls.insert(nam.clone());
}
go(bod, decls, uses);
}
Term::Lnk { nam } => {
@ -571,16 +571,14 @@ impl Term {
go(&rule.body, decls, uses);
}
}
Term::Lst { els } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
go(el, decls, uses);
}
}
Term::Let { val: fst, nxt: snd, .. }
| Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
go(fst, decls, uses);
go(snd, decls, uses);
@ -629,11 +627,12 @@ impl Term {
return false;
}
}
Type::Tup => {
Type::Tup(_) => {
if rules.len() != 1 {
return false;
}
if !matches!(rules[0].pats.as_slice(), [Pattern::Tup(box Pattern::Var(_), box Pattern::Var(_))]) {
let Pattern::Tup(args) = &rules[0].pats[0] else { return false };
if args.iter().any(|p| !matches!(p, Pattern::Var(_))) {
return false;
}
}
@ -707,10 +706,8 @@ impl Pattern {
fn go<'a>(pat: &'a mut Pattern, set: &mut Vec<&'a mut Option<Name>>) {
match pat {
Pattern::Var(nam) => set.push(nam),
Pattern::Ctr(_, pats) | Pattern::Lst(pats) => pats.iter_mut().for_each(|pat| go(pat, set)),
Pattern::Tup(fst, snd) => {
go(fst, set);
go(snd, set);
Pattern::Ctr(_, pats) | Pattern::Lst(pats) | Pattern::Tup(pats) => {
pats.iter_mut().for_each(|pat| go(pat, set))
}
Pattern::Num(NumCtr::Succ(_, Some(nam))) => {
set.push(nam);
@ -736,12 +733,8 @@ impl Pattern {
/// Considers Lists as its own pattern and not a sequence of Cons.
pub fn children<'a>(&'a self) -> Box<dyn DoubleEndedIterator<Item = &'a Pattern> + 'a> {
match self {
Pattern::Ctr(_, children) => Box::new(children.iter()),
Pattern::Var(_) => Box::new([].iter()),
Pattern::Num(_) => Box::new([].iter()),
Pattern::Tup(fst, snd) => Box::new([fst.as_ref(), snd.as_ref()].into_iter()),
Pattern::Lst(els) => Box::new(els.iter()),
Pattern::Str(_) => Box::new([].iter()),
Pattern::Ctr(_, pats) | Pattern::Tup(pats) | Pattern::Lst(pats) => Box::new(pats.iter()),
Pattern::Var(_) | Pattern::Num(_) | Pattern::Str(_) => Box::new([].iter()),
}
}
@ -763,7 +756,7 @@ impl Pattern {
Pattern::Ctr(nam, _) => Some(nam.clone()),
Pattern::Num(NumCtr::Num(num)) => Some(Name::new(format!("{num}"))),
Pattern::Num(NumCtr::Succ(num, _)) => Some(Name::new(format!("{num}+"))),
Pattern::Tup(_, _) => Some(Name::new("(,)")),
Pattern::Tup(pats) => Some(Name::new(format!("({})", ",".repeat(pats.len())))),
Pattern::Lst(_) => todo!(),
Pattern::Str(_) => todo!(),
}
@ -781,11 +774,8 @@ impl Pattern {
pub fn is_simple(&self) -> bool {
match self {
Pattern::Var(_) => true,
Pattern::Ctr(_, args) => args.iter().all(|arg| matches!(arg, Pattern::Var(_))),
Pattern::Ctr(_, args) | Pattern::Tup(args) => args.iter().all(|arg| matches!(arg, Pattern::Var(_))),
Pattern::Num(_) => true,
Pattern::Tup(fst, snd) => {
matches!(fst.as_ref(), Pattern::Var(_)) && matches!(snd.as_ref(), Pattern::Var(_))
}
Pattern::Lst(_) | Pattern::Str(_) => todo!(),
}
}
@ -797,7 +787,7 @@ impl Pattern {
let adt_nam = ctrs.get(ctr_nam).expect("Unknown constructor '{ctr_nam}'");
Type::Adt(adt_nam.clone())
}
Pattern::Tup(..) => Type::Tup,
Pattern::Tup(args) => Type::Tup(args.len()),
Pattern::Num(NumCtr::Num(_)) => Type::Num,
Pattern::Num(NumCtr::Succ(n, _)) => Type::NumSucc(*n),
Pattern::Lst(..) => Type::Adt(builtins::LIST.into()),
@ -816,7 +806,7 @@ impl Pattern {
Pattern::Num(NumCtr::Succ(_, None)) => unreachable!(),
Pattern::Num(NumCtr::Succ(val, Some(Some(nam)))) => Term::add_num(Term::Var { nam: nam.clone() }, *val),
Pattern::Num(NumCtr::Succ(_, Some(None))) => Term::Era,
Pattern::Tup(fst, snd) => Term::Tup { fst: Box::new(fst.to_term()), snd: Box::new(snd.to_term()) },
Pattern::Tup(args) => Term::Tup { els: args.iter().map(|p| p.to_term()).collect() },
Pattern::Lst(_) | Pattern::Str(_) => todo!(),
}
}
@ -827,7 +817,7 @@ impl Pattern {
(Pattern::Ctr(a, _), Pattern::Ctr(b, _)) if a == b => true,
(Pattern::Num(NumCtr::Num(a)), Pattern::Num(NumCtr::Num(b))) if a == b => true,
(Pattern::Num(NumCtr::Succ(a, _)), Pattern::Num(NumCtr::Succ(b, _))) if a == b => true,
(Pattern::Tup(_, _), Pattern::Tup(_, _)) => true,
(Pattern::Tup(a), Pattern::Tup(b)) if a.len() == b.len() => true,
(Pattern::Lst(_), Pattern::Lst(_)) => true,
(Pattern::Var(_), Pattern::Var(_)) => true,
_ => false,
@ -881,10 +871,9 @@ impl Type {
pub fn ctrs(&self, adts: &Adts) -> Vec<Pattern> {
match self {
Type::Any => vec![Pattern::Var(None)],
Type::Tup => vec![Pattern::Tup(
Box::new(Pattern::Var(Some("%fst".into()))),
Box::new(Pattern::Var(Some("%snd".into()))),
)],
Type::Tup(len) => {
vec![Pattern::Tup((0 .. *len).map(|i| Pattern::Var(Some(Name::new(format!("%x{i}"))))).collect())]
}
Type::NumSucc(n) => {
let mut ctrs = (0 .. *n).map(|n| Pattern::Num(NumCtr::Num(n))).collect::<Vec<_>>();
ctrs.push(Pattern::Num(NumCtr::Succ(*n, Some(Some("%pred".into())))));
@ -906,7 +895,7 @@ impl Type {
/// True if the type is an ADT or a builtin equivalent of an ADT (like tups and numbers)
pub fn is_ctr_type(&self) -> bool {
matches!(self, Type::Adt(_) | Type::Num | Type::Tup)
matches!(self, Type::Adt(_) | Type::Num | Type::Tup(_))
}
pub fn is_var_type(&self) -> bool {

49
src/term/net_to_term.rs
View File

@ -110,7 +110,9 @@ impl<'a> Reader<'a> {
match &mut succ_term {
Term::Lam { nam, bod, .. } => {
Term::native_num_match(scrutinee, zero_term, std::mem::take(bod), Some(nam.take()))
let nam = std::mem::take(nam);
let bod = std::mem::take(bod);
Term::native_num_match(scrutinee, zero_term, *bod, Some(nam))
}
_ => {
self.error(ReadbackError::InvalidNumericMatch);
@ -157,11 +159,7 @@ impl<'a> Reader<'a> {
.unwrap_or_else(|| {
// If no Dup with same label in the path, we can't resolve the Sup, so keep it as a term.
self.decay_or_get_ports(node).map_or_else(
|(fst, snd)| Term::Sup {
tag: self.labels.dup.to_tag(Some(*lab)),
fst: Box::new(fst),
snd: Box::new(snd),
},
|(fst, snd)| Term::Sup { tag: self.labels.dup.to_tag(Some(*lab)), els: vec![fst, snd] },
|term| term,
)
})
@ -204,7 +202,7 @@ impl<'a> Reader<'a> {
// If we're visiting a port 0, then it is a Tup.
0 => self
.decay_or_get_ports(node)
.map_or_else(|(fst, snd)| Term::Tup { fst: Box::new(fst), snd: Box::new(snd) }, |term| term),
.map_or_else(|(fst, snd)| Term::Tup { els: vec![fst, snd] }, |term| term),
// If we're visiting a port 1 or 2, then it is a variable.
1 | 2 => {
if self.seen_fans.insert(node) {
@ -307,12 +305,17 @@ impl Term {
Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.insert_split(split, threshold)?,
Term::Let { val: fst, nxt: snd, .. }
| Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.insert_split(split, threshold)? + snd.insert_split(split, threshold)?
}
Term::Sup { els, .. } | Term::Tup { els } => {
let mut n = 0;
for el in els {
n += el.insert_split(split, threshold)?;
}
n
}
Term::Mat { args, rules } => {
debug_assert_eq!(args.len(), 1);
let mut n = args[0].insert_split(split, threshold)?;
@ -324,16 +327,15 @@ impl Term {
Term::Lst { .. } => unreachable!(),
Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Ref { .. } | Term::Era | Term::Err => 0,
};
if n >= threshold {
let Split { tag, fst, snd, val } = std::mem::take(split);
let nxt = Box::new(std::mem::take(self));
*self = match tag {
None => Term::Let {
pat: Pattern::Tup(Box::new(Pattern::Var(fst)), Box::new(Pattern::Var(snd))),
val: Box::new(val),
nxt,
},
Some(tag) => Term::Dup { tag, fst, snd, val: Box::new(val), nxt },
None => {
Term::Let { pat: Pattern::Tup(vec![Pattern::Var(fst), Pattern::Var(snd)]), val: Box::new(val), nxt }
}
Some(tag) => Term::Dup { tag, bnd: vec![fst, snd], val: Box::new(val), nxt },
};
None
} else {
@ -364,20 +366,23 @@ impl Term {
*self = term;
}
}
Term::Dup { fst, snd, val, nxt, .. } => {
Term::Dup { bnd, val, nxt, .. } => {
val.fix_names(id_counter, book);
fix_name(fst, id_counter, nxt);
fix_name(snd, id_counter, nxt);
for bnd in bnd {
fix_name(bnd, id_counter, nxt);
}
nxt.fix_names(id_counter, book);
}
Term::Chn { bod, .. } => bod.fix_names(id_counter, book),
Term::App { fun: fst, arg: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Tup { fst, snd }
| Term::Opx { op: _, fst, snd } => {
Term::App { fun: fst, arg: snd, .. } | Term::Opx { op: _, fst, snd } => {
fst.fix_names(id_counter, book);
snd.fix_names(id_counter, book);
}
Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.fix_names(id_counter, book);
}
}
Term::Mat { args, rules } => {
for arg in args {
arg.fix_names(id_counter, book);

38
src/term/parser/parser.rs
View File

@ -220,44 +220,36 @@ where
.then_ignore(just(Token::Lambda))
.then(name_or_era())
.then(term.clone())
.map(|((tag, name), body)| Term::Lam { tag, nam: name, bod: Box::new(body) })
.map(|((tag, nam), bod)| Term::Lam { tag, nam, bod: Box::new(bod) })
.boxed();
// #tag? λ$x body
let global_lam = tag(Tag::Static)
.then_ignore(just(Token::Lambda))
.then(just(Token::Dollar).ignore_then(name()))
.then(just(Token::Dollar).ignore_then(name_or_era()))
.then(term.clone())
.map(|((tag, name), body)| Term::Chn { tag, nam: name, bod: Box::new(body) })
.map(|((tag, nam), bod)| Term::Chn { tag, nam, bod: Box::new(bod) })
.boxed();
// #tag {fst snd}
let sup = tag(Tag::Auto)
.then_ignore(just(Token::LBracket))
.then(term.clone())
.then(term.clone())
.then(term.clone().separated_by(list_sep.clone()).at_least(2).collect())
.then_ignore(just(Token::RBracket))
.map(|((tag, fst), snd)| Term::Sup { tag, fst: Box::new(fst), snd: Box::new(snd) })
.map(|(tag, els)| Term::Sup { tag, els })
.boxed();
// let #tag? {x1 x2} = body; next
let dup = just(Token::Let)
.ignore_then(tag(Tag::Auto))
.then_ignore(just(Token::LBracket))
.then(name_or_era())
.then(name_or_era())
.then(name_or_era().separated_by(list_sep.clone()).at_least(2).collect())
.then_ignore(just(Token::RBracket))
.then_ignore(just(Token::Equals))
.then(term.clone())
.then_ignore(term_sep.clone())
.then(term.clone())
.map(|((((tag, fst), snd), val), next)| Term::Dup {
tag,
fst,
snd,
val: Box::new(val),
nxt: Box::new(next),
})
.map(|(((tag, bnd), val), next)| Term::Dup { tag, bnd, val: Box::new(val), nxt: Box::new(next) })
.boxed();
// let a = ...
@ -339,8 +331,8 @@ where
.separated_by(just(Token::Comma))
.at_least(2)
.collect::<Vec<Term>>()
.map(|xs| make_tup_tree(&xs, |a, b| Term::Tup { fst: Box::new(a), snd: Box::new(b) }))
.delimited_by(just(Token::LParen), just(Token::RParen))
.map(|els| Term::Tup { els })
.boxed();
let str = select!(Token::Str(s) => Term::Str { val: s }).boxed();
@ -363,18 +355,6 @@ where
})
}
fn make_tup_tree<A: Clone>(xs: &[A], make: fn(A, A) -> A) -> A {
match xs {
[] => unreachable!(),
[x] => x.clone(),
xs => {
let half = xs.len() / 2;
let (x, y) = xs.split_at(half);
make(make_tup_tree(x, make), make_tup_tree(y, make))
}
}
}
fn pattern<'a, I>() -> impl Parser<'a, I, Pattern, extra::Err<Rich<'a, Token>>>
where
I: ValueInput<'a, Token = Token, Span = SimpleSpan>,
@ -394,7 +374,7 @@ where
.at_least(2)
.collect::<Vec<Pattern>>()
.delimited_by(just(Token::LParen), just(Token::RParen))
.map(|xs| make_tup_tree(&xs, |a, b| Pattern::Tup(Box::new(a), Box::new(b))))
.map(Pattern::Tup)
.boxed();
let list = pattern

105
src/term/term_to_net.rs
View File

@ -1,5 +1,9 @@
use crate::{
net::{INet, NodeKind::*, Port, ROOT},
net::{
INet,
NodeKind::{self, *},
Port, ROOT,
},
term::{Book, Name, NumCtr, Op, Pattern, Tag, Term},
};
use std::collections::{hash_map::Entry, HashMap};
@ -84,7 +88,9 @@ impl<'a> EncodeTermState<'a> {
// core: (var_use bod)
Term::Chn { tag, nam, bod } => {
let fun = self.inet.new_node(Con { lab: self.labels.con.generate(tag) });
self.global_vars.entry(nam.clone()).or_default().0 = Port(fun, 1);
if let Some(nam) = nam {
self.global_vars.entry(nam.clone()).or_default().0 = Port(fun, 1);
}
let bod = self.encode_term(bod, Port(fun, 2));
self.link_local(Port(fun, 2), bod);
Some(Port(fun, 0))
@ -130,22 +136,30 @@ impl<'a> EncodeTermState<'a> {
Some(Port(if_, 2))
}
// A dup becomes a dup node too. Ports:
// A dup becomes a dup node too. Ports for dups of size 2:
// - 0: points to the value projected.
// - 1: points to the occurrence of the first variable.
// - 2: points to the occurrence of the second variable.
// core: & val ~ {lab fst snd} (val not necessarily main port)
Term::Dup { fst, snd, val, nxt, tag } => {
let dup = self.inet.new_node(Dup { lab: self.labels.dup.generate(tag).unwrap() });
// Dups with more than 2 variables become a list-like node tree of n-1 nodes.
// All the nodes of a dup tree have the same label.
// `@x dup #i {x0 x1 x2 x3}; A` => `({i x0 {i x1 {i x2 x3}}} A)`
Term::Dup { tag, bnd, val, nxt } => {
let lab = self.labels.dup.generate(tag).unwrap();
let (main, aux) = self.make_node_list(Dup { lab }, bnd.len());
let val = self.encode_term(val, Port(dup, 0));
self.link_local(Port(dup, 0), val);
let val = self.encode_term(val, main);
self.link_local(main, val);
for (bnd, aux) in bnd.iter().zip(aux.iter()) {
self.push_scope(bnd, *aux);
}
self.push_scope(fst, Port(dup, 1));
self.push_scope(snd, Port(dup, 2));
let nxt = self.encode_term(nxt, up);
self.pop_scope(snd, Port(dup, 2));
self.pop_scope(fst, Port(dup, 1));
for (bnd, aux) in bnd.iter().rev().zip(aux.iter().rev()) {
self.pop_scope(bnd, *aux);
}
nxt
}
@ -175,17 +189,20 @@ impl<'a> EncodeTermState<'a> {
self.inet.link(up, Port(node, 0));
Some(Port(node, 0))
}
Term::Let { pat: Pattern::Tup(box Pattern::Var(l_nam), box Pattern::Var(r_nam)), val, nxt } => {
let dup = self.inet.new_node(Tup);
Term::Let { pat: Pattern::Tup(args), val, nxt } => {
let nams = args.iter().map(|arg| if let Pattern::Var(nam) = arg { nam } else { unreachable!() });
let (main, aux) = self.make_node_list(Tup, args.len());
let val = self.encode_term(val, Port(dup, 0));
self.link_local(Port(dup, 0), val);
let val = self.encode_term(val, main);
self.link_local(main, val);
self.push_scope(l_nam, Port(dup, 1));
self.push_scope(r_nam, Port(dup, 2));
for (nam, aux) in nams.clone().zip(aux.iter()) {
self.push_scope(nam, *aux);
}
let nxt = self.encode_term(nxt, up);
self.pop_scope(r_nam, Port(dup, 2));
self.pop_scope(l_nam, Port(dup, 1));
for (nam, aux) in nams.rev().zip(aux.iter().rev()) {
self.pop_scope(nam, *aux);
}
nxt
}
@ -198,16 +215,16 @@ impl<'a> EncodeTermState<'a> {
self.encode_term(nxt, up)
}
Term::Let { .. } => unreachable!(), // Removed in earlier pass
Term::Sup { tag, fst, snd } => {
let sup = self.inet.new_node(Dup { lab: self.labels.dup.generate(tag).unwrap() });
Term::Sup { tag, els } => {
let lab = self.labels.dup.generate(tag).unwrap();
let (main, aux) = self.make_node_list(Dup { lab }, els.len());
let fst = self.encode_term(fst, Port(sup, 1));
self.link_local(Port(sup, 1), fst);
for (el, aux) in els.iter().zip(aux) {
let el = self.encode_term(el, aux);
self.link_local(aux, el);
}
let snd = self.encode_term(snd, Port(sup, 2));
self.link_local(Port(sup, 2), snd);
Some(Port(sup, 0))
Some(main)
}
Term::Era => {
let era = self.inet.new_node(Era);
@ -235,16 +252,14 @@ impl<'a> EncodeTermState<'a> {
Some(Port(opx, 2))
}
Term::Tup { fst, snd } => {
let tup = self.inet.new_node(Tup);
Term::Tup { els } => {
let (main, aux) = self.make_node_list(Tup, els.len());
for (el, aux) in els.iter().zip(aux.iter()) {
let el = self.encode_term(el, *aux);
self.link_local(*aux, el);
}
let fst = self.encode_term(fst, Port(tup, 1));
self.link_local(Port(tup, 1), fst);
let snd = self.encode_term(snd, Port(tup, 2));
self.link_local(Port(tup, 2), snd);
Some(Port(tup, 0))
Some(main)
}
Term::Err => unreachable!(),
}
@ -273,6 +288,24 @@ impl<'a> EncodeTermState<'a> {
self.inet.link(ptr_a, ptr_b);
}
}
/// Adds a list-like tree of nodes of the same kind to the inet.
/// Doesn't attach this tree to anything
fn make_node_list(&mut self, kind: NodeKind, num_ports: usize) -> (Port, Vec<Port>) {
debug_assert!(num_ports >= 2);
let nodes: Vec<_> = (0 .. num_ports - 1).map(|_| self.inet.new_node(kind.clone())).collect();
let mut up = Some(Port(nodes[0], 2));
for &node in nodes.iter().skip(1) {
self.link_local(Port(node, 0), up);
up = Some(Port(node, 2));
}
let main_port = Port(nodes[0], 0);
let mut aux_ports = nodes.iter().map(|n| Port(*n, 1)).collect::<Vec<_>>();
aux_ports.push(Port(*nodes.last().unwrap(), 2));
(main_port, aux_ports)
}
}
impl Op {

7
src/term/transform/definition_pruning.rs
View File

@ -102,8 +102,6 @@ impl Book {
Term::Let { val: fst, nxt: snd, .. }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::App { fun: fst, arg: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Tup { fst, snd }
| Term::Opx { fst, snd, .. } => {
to_find.push(fst);
to_find.push(snd);
@ -116,6 +114,11 @@ impl Book {
to_find.push(&rule.body);
}
}
Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
to_find.push(el);
}
}
Term::Lst { els } => {
self.insert_ctrs_used(&Name::from(LIST), uses, adt_encoding);
for term in els {

10
src/term/transform/desugar_implicit_match_binds.rs
View File

@ -51,7 +51,7 @@ impl Term {
// Implicit num arg
*p = Some(Some(Name::new(format!("{nam}-{n}"))));
}
Pattern::Tup(_, _) => (),
Pattern::Tup(..) => (),
Pattern::Lst(..) => (),
Pattern::Str(..) => (),
}
@ -76,11 +76,14 @@ impl Term {
let Term::Mat { args: _, rules } = term else { unreachable!() };
to_desugar.extend(rules.iter_mut().map(|r| &mut r.body));
}
Term::Sup { els, .. } | Term::Lst { els } | Term::Tup { els } => {
for el in els {
to_desugar.push(el);
}
}
Term::Let { pat: Pattern::Var(_), val: fst, nxt: snd }
| Term::App { fun: fst, arg: snd, .. }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Tup { fst, snd }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
to_desugar.push(fst);
to_desugar.push(snd);
@ -96,7 +99,6 @@ impl Term {
Term::Let { pat: _, .. } => {
unreachable!("Expected destructor let expressions to have been desugared already")
}
Term::Lst { .. } => unreachable!("Should have been desugared already"),
}
}
}

8
src/term/transform/desugar_let_destructors.rs
View File

@ -16,9 +16,7 @@ impl Term {
match self {
Term::Let { pat: Pattern::Var(_), val: fst, nxt: snd }
| Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.desugar_let_destructors();
snd.desugar_let_destructors();
@ -31,6 +29,11 @@ impl Term {
rule.body.desugar_let_destructors();
}
}
Term::Sup { els, .. } | Term::Lst { els } | Term::Tup { els } => {
for el in els {
el.desugar_let_destructors();
}
}
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
bod.desugar_let_destructors();
}
@ -62,7 +65,6 @@ impl Term {
Term::Let { pat, val, nxt: Box::new(Term::Mat { args, rules }) }
};
}
Term::Lst { .. } => unreachable!("Should have been desugared already"),
}
}
}

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

@ -37,7 +37,7 @@ fn encode_ctr(
AdtEncoding::TaggedScott => {
let ctr = Term::Var { nam: ctr_name.clone() };
let app = ctr_args.iter().cloned().fold(ctr, |acc, nam| {
let tag = Tag::adt_field(adt_name, ctr_name, &nam);
let tag = Tag::adt_name(adt_name);
Term::tagged_app(tag, acc, Term::Var { nam })
});
let lam = ctrs

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

@ -32,14 +32,14 @@ impl Term {
}
let arg = std::mem::take(&mut args[0]);
let rules = std::mem::take(rules);
*self = encode_match(arg, rules, ctrs, adts, adt_encoding);
*self = encode_match(arg, rules, ctrs, adt_encoding);
}
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
els.iter_mut().for_each(|e| e.encode_simple_matches(ctrs, adts, adt_encoding))
}
Term::Lst { els } => els.iter_mut().for_each(|e| e.encode_simple_matches(ctrs, adts, adt_encoding)),
Term::Let { val: fst, nxt: snd, .. }
| Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.encode_simple_matches(ctrs, adts, adt_encoding);
snd.encode_simple_matches(ctrs, adts, adt_encoding);
@ -56,23 +56,17 @@ impl Term {
}
}
fn encode_match(
arg: Term,
rules: Vec<Rule>,
ctrs: &Constructors,
adts: &Adts,
adt_encoding: AdtEncoding,
) -> Term {
fn encode_match(arg: Term, rules: Vec<Rule>, ctrs: &Constructors, adt_encoding: AdtEncoding) -> Term {
let typ = infer_match_arg_type(&rules, 0, ctrs).unwrap();
match typ {
Type::Any | Type::Tup => {
Type::Any | Type::Tup(_) => {
let fst_rule = rules.into_iter().next().unwrap();
encode_var(arg, fst_rule)
}
Type::NumSucc(_) => encode_num_succ(arg, rules),
Type::Num => encode_num(arg, rules),
// ADT Encoding depends on compiler option
Type::Adt(adt) => encode_adt(arg, rules, adt, adt_encoding, adts),
Type::Adt(adt) => encode_adt(arg, rules, adt, adt_encoding),
}
}
@ -169,7 +163,7 @@ fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
go(rules.into_iter(), last_rule, None, Some(arg))
}
fn encode_adt(arg: Term, rules: Vec<Rule>, adt: Name, adt_encoding: AdtEncoding, adts: &Adts) -> Term {
fn encode_adt(arg: Term, rules: Vec<Rule>, adt: Name, adt_encoding: AdtEncoding) -> Term {
match adt_encoding {
// (x @field1 @field2 ... body1 @field1 body2 ...)
AdtEncoding::Scott => {
@ -184,11 +178,11 @@ fn encode_adt(arg: Term, rules: Vec<Rule>, adt: Name, adt_encoding: AdtEncoding,
// #adt_name(x arm[0] arm[1] ...)
AdtEncoding::TaggedScott => {
let mut arms = vec![];
for (rule, (ctr, fields)) in rules.into_iter().zip(&adts[&adt].ctrs) {
let body =
rule.pats[0].binds().rev().zip(fields.iter().rev()).fold(rule.body, |bod, (var, field)| {
Term::tagged_lam(Tag::adt_field(&adt, ctr, field), var.clone(), bod)
});
for rule in rules.into_iter() {
let body = rule.pats[0]
.binds()
.rev()
.fold(rule.body, |bod, var| Term::tagged_lam(Tag::adt_name(&adt), var.clone(), bod));
arms.push(body);
}
Term::tagged_call(Tag::adt_name(&adt), arg, arms)

4
src/term/transform/eta_reduction.rs
View File

@ -47,7 +47,7 @@ impl Term {
rule.body.eta_reduction();
}
}
Term::Lst { els } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.eta_reduction();
}
@ -55,8 +55,6 @@ impl Term {
Term::Let { val: fst, nxt: snd, .. }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.eta_reduction();
snd.eta_reduction();

15
src/term/transform/float_combinators.rs
View File

@ -171,17 +171,21 @@ impl Term {
val_detach & nxt_detach
}
Term::Dup { fst, snd, val, nxt, .. } => {
Term::Dup { bnd, val, nxt, .. } => {
let val_detach = val.go_float(depth + 1, term_info);
let nxt_detach = nxt.go_float(depth + 1, term_info);
term_info.provide(fst.as_ref());
term_info.provide(snd.as_ref());
for bnd in bnd {
term_info.provide(bnd.as_ref());
}
val_detach & nxt_detach
}
Term::Sup { fst, snd, .. } | Term::Tup { fst, snd } | Term::Opx { fst, snd, .. } => {
Term::Sup { els, .. } | Term::Lst { els } | Term::Tup { els } => {
els.iter_mut().map(|el| el.go_float(depth + 1, term_info)).fold(Detach::Combinator, |a, b| a & b)
}
Term::Opx { fst, snd, .. } => {
let fst_is_super = fst.go_float(depth + 1, term_info);
let snd_is_super = snd.go_float(depth + 1, term_info);
@ -190,7 +194,6 @@ impl Term {
Term::Ref { nam: def_name } if def_name == &term_info.def_name => Detach::Recursive,
Term::Lst { .. } => unreachable!(),
Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => Detach::Combinator,
}
}
@ -198,7 +201,7 @@ impl Term {
fn float_lam(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach {
let (nam, bod, unscoped): (Option<&Name>, &mut Term, bool) = match self {
Term::Lam { nam, bod, .. } => (nam.as_ref(), bod, false),
Term::Chn { nam, bod, .. } => (Some(nam), bod, true),
Term::Chn { nam, bod, .. } => (nam.as_ref(), bod, true),
_ => unreachable!(),
};

27
src/term/transform/inline.rs
View File

@ -32,32 +32,32 @@ impl Term {
}
}
Term::Lam { bod, .. } => to_inline.push(bod),
Term::Lam { bod, .. } | Term::Chn { bod, .. } => to_inline.push(bod),
Term::Sup { els, .. } | Term::Lst { els } | Term::Tup { els } => {
for el in els {
to_inline.push(el);
}
}
Term::App { fun: fst, arg: snd, .. }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Opx { fst, snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Tup { fst, snd } => {
| Term::Opx { fst, snd, .. } => {
to_inline.push(fst);
to_inline.push(snd);
}
Term::Mat { rules, .. } => {
Term::Mat { args, rules } => {
for arg in args {
to_inline.push(arg);
}
for rule in rules {
to_inline.push(&mut rule.body);
}
}
Term::Var { .. }
| Term::Chn { .. }
| Term::Lnk { .. }
| Term::Let { .. }
| Term::Num { .. }
| Term::Str { .. }
| Term::Lst { .. }
| Term::Era => {}
Term::Err => unreachable!(),
}
}
@ -71,7 +71,10 @@ impl Term {
match term {
Term::Era | Term::Var { .. } | Term::Num { .. } => scope.saturating_sub(1) == 0,
Term::Lam { bod, .. } => go(bod, scope + 1),
Term::Tup { fst, snd } | Term::Sup { fst, snd, .. } => go(fst, scope + 1) && go(snd, scope + 1),
Term::Sup { els, .. } | Term::Tup { els } => match els.as_slice() {
[fst, snd] => go(fst, scope + 1) && go(snd, scope + 1),
_ => false,
},
Term::Chn { .. } | Term::Lnk { .. } => false,
Term::Str { .. } | Term::Lst { .. } => false,

15
src/term/transform/linearize_matches.rs
View File

@ -36,22 +36,21 @@ impl Term {
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
bod.linearize_simple_matches(lift_all_vars)?;
}
Term::Let { pat: Pattern::Var(..), val: fst, nxt: snd }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. }
| Term::App { fun: fst, arg: snd, .. } => {
fst.linearize_simple_matches(lift_all_vars)?;
snd.linearize_simple_matches(lift_all_vars)?;
}
Term::Lst { .. } => unreachable!(),
Term::Let { pat, .. } => {
unreachable!("Destructor let expression should have been desugared already. {pat}")
}
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.linearize_simple_matches(lift_all_vars)?;
}
}
Term::Str { .. }
| Term::Lnk { .. }
| Term::Var { .. }
@ -59,8 +58,8 @@ impl Term {
| Term::Ref { .. }
| Term::Era => {}
Term::Err => todo!(),
};
Term::Err => unreachable!(),
}
Ok(())
})

153
src/term/transform/linearize_vars.rs
View File

@ -26,7 +26,7 @@ impl Term {
term_to_affine(self, &mut HashMap::new());
}
/// Returns false wether the term has no unscoped terms,
/// Returns false whether the term has no unscoped terms,
/// or all its unscoped binds and usage pairs are within the term.
fn has_unscoped(&self) -> bool {
let (decl, uses) = self.unscoped_vars();
@ -34,60 +34,43 @@ impl Term {
}
}
/// Var-declaring terms
fn term_with_binds_to_affine<'a>(
term: &mut Term,
nams: impl IntoIterator<Item = &'a mut Option<Name>>,
inst_count: &mut HashMap<Name, u64>,
) {
term_to_affine(term, inst_count);
for nam in nams {
if nam.is_some() {
let instantiated_count = get_var_uses(nam.as_ref(), inst_count);
duplicate_lam(nam, term, instantiated_count);
}
}
}
fn term_to_affine(term: &mut Term, inst_count: &mut HashMap<Name, u64>) {
fn term_to_affine(term: &mut Term, var_uses: &mut HashMap<Name, u64>) {
match term {
Term::Lam { nam, bod, .. } => term_with_binds_to_affine(bod, [nam], inst_count),
Term::Let { pat: Pattern::Var(Some(nam)), val, nxt } => {
term_to_affine(nxt, inst_count);
term_to_affine(nxt, var_uses);
match get_var_uses(Some(nam), inst_count) {
match get_var_uses(Some(nam), var_uses) {
0 => {
if val.has_unscoped() {
term_to_affine(val, inst_count);
term_to_affine(val, var_uses);
let Term::Let { val, nxt, .. } = term else { unreachable!() };
let val = std::mem::take(val);
let nxt = std::mem::take(nxt);
*term = Term::Let { pat: Pattern::Var(None), val, nxt };
return;
} else {
*term = std::mem::take(nxt.as_mut());
}
}
1 => {
term_to_affine(val, inst_count);
nxt.subst(&dup_name(nam, 1), val.as_ref());
term_to_affine(val, var_uses);
nxt.subst(nam, val.as_ref());
*term = std::mem::take(nxt.as_mut());
}
instantiated_count => {
term_to_affine(val, inst_count);
duplicate_let(nam, nxt, instantiated_count, val);
term_to_affine(val, var_uses);
duplicate_term(nam, nxt, instantiated_count, Some(val));
*term = std::mem::take(nxt.as_mut());
}
}
*term = std::mem::take(nxt.as_mut());
}
Term::Let { pat: Pattern::Var(None), val, nxt } => {
term_to_affine(nxt, inst_count);
term_to_affine(nxt, var_uses);
if val.has_unscoped() {
term_to_affine(val, inst_count);
term_to_affine(val, var_uses);
} else {
let Term::Let { nxt, .. } = term else { unreachable!() };
let nxt = std::mem::take(nxt.as_mut());
@ -95,97 +78,95 @@ fn term_to_affine(term: &mut Term, inst_count: &mut HashMap<Name, u64>) {
}
}
Term::Dup { fst, snd, val, nxt, .. }
| Term::Let { pat: Pattern::Tup(box Pattern::Var(fst), box Pattern::Var(snd)), val, nxt } => {
term_to_affine(val, inst_count);
term_to_affine(nxt, inst_count);
let uses_fst = get_var_uses(fst.as_ref(), inst_count);
let uses_snd = get_var_uses(snd.as_ref(), inst_count);
duplicate_lam(fst, nxt, uses_fst);
duplicate_lam(snd, nxt, uses_snd);
Term::Lam { nam, bod, .. } => term_with_binds_to_affine(bod, [nam], var_uses),
Term::Dup { bnd, val, nxt, .. } => {
term_to_affine(val, var_uses);
term_with_binds_to_affine(nxt, bnd, var_uses);
}
Term::Let { pat, val, nxt } => {
term_to_affine(val, var_uses);
term_with_binds_to_affine(nxt, pat.bind_or_eras_mut(), var_uses);
}
Term::Let { .. } => unreachable!(),
// Var-using terms
Term::Var { nam } => {
let instantiated_count = inst_count.entry(nam.clone()).or_default();
let instantiated_count = var_uses.entry(nam.clone()).or_default();
*instantiated_count += 1;
*nam = dup_name(nam, *instantiated_count);
}
// Others
Term::Chn { bod, .. } => term_to_affine(bod, inst_count),
Term::App { fun: fst, arg: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Tup { fst, snd }
| Term::Opx { fst, snd, .. } => {
term_to_affine(fst, inst_count);
term_to_affine(snd, inst_count);
Term::Chn { bod, .. } => term_to_affine(bod, var_uses),
Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => {
term_to_affine(fst, var_uses);
term_to_affine(snd, var_uses);
}
Term::Mat { args, rules } => {
for arg in args {
term_to_affine(arg, inst_count);
term_to_affine(arg, var_uses);
}
for rule in rules {
let nams = rule.pats.iter_mut().flat_map(|p| p.bind_or_eras_mut());
term_with_binds_to_affine(&mut rule.body, nams, inst_count)
term_with_binds_to_affine(&mut rule.body, nams, var_uses)
}
}
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
term_to_affine(el, var_uses);
}
}
Term::Lst { .. } => unreachable!("Should have been desugared already"),
Term::Era | Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Err => {}
};
}
/// Var-declaring terms
fn term_with_binds_to_affine<'a>(
term: &mut Term,
nams: impl IntoIterator<Item = &'a mut Option<Name>>,
var_uses: &mut HashMap<Name, u64>,
) {
term_to_affine(term, var_uses);
for nam in nams {
if nam.is_some() {
let instantiated_count = get_var_uses(nam.as_ref(), var_uses);
duplicate_bind(nam, term, instantiated_count);
}
}
}
fn get_var_uses(nam: Option<&Name>, var_uses: &HashMap<Name, u64>) -> u64 {
nam.and_then(|nam| var_uses.get(nam).copied()).unwrap_or_default()
}
// TODO: Is there a difference between a list of dups and a complete binary tree of dups?
//
/// # Example
/// Creates the duplication bindings for variables used multiple times.
///
/// ```txt
/// let {x1 x1_dup} = body;
/// let {x2 x2_dup} = x1_dup;
/// let {x3 x4} = x2_dup;
/// nxt
/// ```
fn make_dup_tree(nam: &Name, nxt: &mut Term, uses: u64, mut dup_body: Option<&mut Term>) {
for i in (1 .. uses).rev() {
*nxt = Term::Dup {
tag: Tag::Auto,
fst: Some(dup_name(nam, i)),
snd: if i == uses - 1 { Some(dup_name(nam, uses)) } else { Some(internal_dup_name(nam, i)) },
val: if i == 1 {
Box::new(dup_body.as_mut().map_or_else(|| Term::Var { nam: nam.clone() }, |x| std::mem::take(x)))
} else {
Box::new(Term::Var { nam: internal_dup_name(nam, i - 1) })
},
nxt: Box::new(std::mem::take(nxt)),
};
/// Example:
///
/// `@x (x x x x)` becomes `@x let {x0 x1 x2 x3} = x; (x0 x1 x2 x3)`.
///
/// `let x = @y y; (x x x)` becomes `let {x0 x1 x2} = @y y; (x0 x1 x2)`.
fn duplicate_term(nam: &Name, nxt: &mut Term, uses: u64, dup_body: Option<&mut Term>) {
debug_assert!(uses > 1);
*nxt = Term::Dup {
tag: Tag::Auto,
bnd: (1 .. uses + 1).map(|i| Some(dup_name(nam, i))).collect(),
val: Box::new(dup_body.map_or_else(|| Term::Var { nam: nam.clone() }, std::mem::take)),
nxt: Box::new(std::mem::take(nxt)),
}
}
fn duplicate_lam(nam: &mut Option<Name>, nxt: &mut Term, uses: u64) {
fn duplicate_bind(nam: &mut Option<Name>, nxt: &mut Term, uses: u64) {
match uses {
0 => *nam = None,
1 => *nam = Some(dup_name(nam.as_ref().unwrap(), 1)),
uses => make_dup_tree(nam.as_ref().unwrap(), nxt, uses, None),
uses => duplicate_term(nam.as_ref().unwrap(), nxt, uses, None),
}
}
fn duplicate_let(nam: &Name, nxt: &mut Term, uses: u64, let_body: &mut Term) {
make_dup_tree(nam, nxt, uses, Some(let_body));
}
fn dup_name(nam: &Name, uses: u64) -> Name {
if uses == 1 { nam.clone() } else { Name::new(format!("{nam}_{uses}")) }
}
fn internal_dup_name(nam: &Name, uses: u64) -> Name {
Name::new(format!("{}_dup", dup_name(nam, uses)))
}

14
src/term/transform/resolve_ctrs_in_pats.rs
View File

@ -29,7 +29,7 @@ impl Pattern {
*pat = Pattern::Ctr(nam.clone(), vec![]);
}
}
Pattern::Ctr(_, args) | Pattern::Lst(args) => {
Pattern::Ctr(_, args) | Pattern::Lst(args) | Pattern::Tup(args) => {
for arg in args {
to_resolve.push(arg);
}
@ -37,10 +37,6 @@ impl Pattern {
Pattern::Var(None) => (),
Pattern::Num(_) => (),
Pattern::Str(_) => (),
Pattern::Tup(fst, snd) => {
to_resolve.push(fst);
to_resolve.push(snd);
}
}
}
}
@ -68,10 +64,13 @@ impl Term {
to_resolve.push(&mut rule.body);
}
}
Term::Sup { els, .. } | Term::Lst { els } | Term::Tup { els } => {
for el in els {
to_resolve.push(el);
}
}
Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
to_resolve.push(fst);
to_resolve.push(snd);
@ -82,7 +81,6 @@ impl Term {
| Term::Ref { .. }
| Term::Num { .. }
| Term::Str { .. }
| Term::Lst { .. }
| Term::Era
| Term::Err => (),
}

35
src/term/transform/resolve_refs.rs
View File

@ -64,24 +64,23 @@ impl Term {
}
Term::Let { pat, val, nxt } => {
val.resolve_refs(def_names, main, scope)?;
for nam in pat.binds() {
push_scope(Some(nam), scope);
for nam in pat.bind_or_eras() {
push_scope(nam.as_ref(), scope);
}
nxt.resolve_refs(def_names, main, scope)?;
for nam in pat.binds() {
pop_scope(Some(nam), scope);
for nam in pat.bind_or_eras() {
pop_scope(nam.as_ref(), scope);
}
}
Term::Dup { tag: _, fst, snd, val, nxt } => {
Term::Dup { tag: _, bnd, val, nxt } => {
val.resolve_refs(def_names, main, scope)?;
push_scope(fst.as_ref(), scope);
push_scope(snd.as_ref(), scope);
for bnd in bnd.iter() {
push_scope(bnd.as_ref(), scope);
}
nxt.resolve_refs(def_names, main, scope)?;
pop_scope(fst.as_ref(), scope);
pop_scope(snd.as_ref(), scope);
for bnd in bnd.iter() {
pop_scope(bnd.as_ref(), scope);
}
}
// If variable not defined, we check if it's a ref and swap if it is.
@ -99,13 +98,15 @@ impl Term {
}
}
Term::Chn { bod, .. } => bod.resolve_refs(def_names, main, scope)?,
Term::App { fun: fst, arg: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Tup { fst, snd }
| Term::Opx { fst, snd, .. } => {
Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => {
fst.resolve_refs(def_names, main, scope)?;
snd.resolve_refs(def_names, main, scope)?;
}
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.resolve_refs(def_names, main, scope)?;
}
}
Term::Mat { args, rules } => {
for arg in args {
arg.resolve_refs(def_names, main, scope)?;
@ -122,7 +123,7 @@ impl Term {
}
}
}
Term::Lst { .. } => unreachable!("Should have been desugared already"),
Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {
}
}

18
src/term/transform/resugar_adts.rs
View File

@ -32,11 +32,14 @@ impl Term {
}
}
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.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);
@ -49,7 +52,6 @@ impl Term {
rule.body.resugar_tagged_scott(book, errs);
}
}
Term::Lst { .. } => unreachable!(),
Term::Lnk { .. }
| Term::Num { .. }
| Term::Var { .. }
@ -71,7 +73,7 @@ impl Term {
/// (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))
/// #Option λa #Option λ* #Option (a #Option λb #Option λ* #Option (b #Option λ* #Option λc c))
///
/// // Which gets resugared as:
/// (Some (Some None))
@ -112,8 +114,8 @@ impl Term {
let mut cur = &mut *app;
for field in ctr_args.iter().rev() {
let expected_tag = Tag::adt_field(adt_name, ctr, field);
for _ in ctr_args.iter().rev() {
let expected_tag = Tag::adt_name(adt_name);
match cur {
Term::App { tag, .. } if tag == &expected_tag => {
@ -163,7 +165,7 @@ impl Term {
/// }
///
/// // Gives the following readback:
/// λa λb (#Option (a #Option.Some.val λ* λc #Option (c #Option.Some.val λ* 1 2) λ* 3) b)
/// λa λb (#Option (a #Option λ* λc #Option (c #Option λ* 1 2) λ* 3) b)
///
/// // Which gets resugared as:
/// λa λb (match a {
@ -191,7 +193,7 @@ impl Term {
let mut arm = arg.as_mut();
for field in ctr_args {
let expected_tag = Tag::adt_field(adt_name, ctr, field);
let expected_tag = Tag::adt_name(adt_name);
match arm {
Term::Lam { tag, .. } if tag == &expected_tag => {

8
src/term/transform/resugar_builtins.rs
View File

@ -51,16 +51,14 @@ impl Term {
rule.body.resugar_strings();
}
}
Term::Lst { els } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { 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();
@ -114,16 +112,14 @@ impl Term {
rule.body.resugar_lists();
}
}
Term::Lst { els } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { 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();

36
src/term/transform/simplify_matches.rs
View File

@ -42,22 +42,21 @@ impl Term {
stacker::maybe_grow(1024 * 32, 1024 * 1024, move || {
match self {
Term::Mat { args, rules } => {
let (new_args, extracted) = extract_args(args);
let term = simplify_match_expression(new_args, std::mem::take(rules), ctrs, adts)?;
let extracted = extract_args(args);
let args = std::mem::take(args);
let rules = std::mem::take(rules);
let term = simplify_match_expression(args, rules, ctrs, adts)?;
*self = bind_extracted_args(extracted, term);
}
Term::Lst { els } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
el.simplify_matches(ctrs, adts)?;
}
}
Term::Let { val: fst, nxt: snd, .. }
| Term::App { fun: fst, arg: snd, .. }
| Term::Tup { fst, snd }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Opx { fst, snd, .. } => {
fst.simplify_matches(ctrs, adts)?;
snd.simplify_matches(ctrs, adts)?;
@ -372,26 +371,27 @@ fn switch_rule_submatch_arm(rule: &Rule, ctr: &Pattern, nested_fields: &[Option<
}
}
fn extract_args(args: &mut [Term]) -> (Vec<Term>, Vec<(Name, Term)>) {
let mut new_args = vec![];
/// Swaps non-Var arguments in a match by vars with generated names,
/// returning a vec with the extracted args and what they were replaced by.
///
/// `match Term {...}` => `match %match_arg0 {...}` + `vec![(%match_arg0, Term)])`
fn extract_args(args: &mut [Term]) -> Vec<(Name, Term)> {
let mut extracted = vec![];
for (i, arg) in args.iter_mut().enumerate() {
if matches!(arg, Term::Var { .. }) {
new_args.push(std::mem::take(arg));
} else {
if !matches!(arg, Term::Var { .. }) {
let nam = Name::new(format!("%match_arg{i}"));
let old_arg = std::mem::take(arg);
extracted.push((nam.clone(), old_arg));
let new_arg = Term::Var { nam };
new_args.push(new_arg);
let new_arg = Term::Var { nam: nam.clone() };
let old_arg = std::mem::replace(arg, new_arg);
extracted.push((nam, old_arg));
}
}
(new_args, extracted)
extracted
}
/// Binds the arguments that were extracted from a match with [`extract_args`];
///
/// `vec![(%match_arg0, arg)]` + `term` => `let %match_arg0 = arg; term`
fn bind_extracted_args(extracted: Vec<(Name, Term)>, term: Term) -> Term {
extracted.into_iter().rev().fold(term, |term, (nam, val)| Term::Let {
pat: Pattern::Var(Some(nam)),

4
src/term/transform/simplify_ref_to_ref.rs
View File

@ -64,8 +64,6 @@ pub fn subst_ref_to_ref(term: &mut Term, ref_map: &BTreeMap<Name, Name>) -> bool
Term::App { fun: fst, arg: snd, .. }
| Term::Let { val: fst, nxt: snd, .. }
| Term::Dup { val: fst, nxt: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Tup { fst, snd }
| Term::Opx { fst, snd, .. } => {
let fst_subst = subst_ref_to_ref(fst, ref_map);
let snd_subst = subst_ref_to_ref(snd, ref_map);
@ -81,7 +79,7 @@ pub fn subst_ref_to_ref(term: &mut Term, ref_map: &BTreeMap<Name, Name>) -> bool
}
subst
}
Term::Lst { els } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
let mut subst = false;
for e in els {
subst |= subst_ref_to_ref(e, ref_map);

43
src/term/transform/unique_names.rs
View File

@ -50,27 +50,39 @@ impl UniqueNameGenerator {
self.unique_names_in_term(nxt);
*nam = self.pop(nam.as_ref());
}
Term::Dup { tag: _, fst, snd, val, nxt }
| Term::Let { pat: Pattern::Tup(box Pattern::Var(fst), box Pattern::Var(snd)), val, nxt } => {
Term::Dup { tag: _, bnd, val, nxt } => {
self.unique_names_in_term(val);
self.push(fst.as_ref());
self.push(snd.as_ref());
for bnd in bnd.iter() {
self.push(bnd.as_ref());
}
self.unique_names_in_term(nxt);
*snd = self.pop(snd.as_ref());
*fst = self.pop(fst.as_ref());
for bnd in bnd.iter_mut().rev() {
*bnd = self.pop(bnd.as_ref());
}
}
Term::Let { pat, val, nxt } => {
self.unique_names_in_term(val);
for bnd in pat.bind_or_eras() {
self.push(bnd.as_ref());
}
self.unique_names_in_term(nxt);
for bnd in pat.bind_or_eras_mut().rev() {
*bnd = self.pop(bnd.as_ref());
}
}
Term::Mat { args, rules } => {
for arg in args {
self.unique_names_in_term(arg);
}
for rule in rules {
rule.pats.iter().flat_map(|p| p.binds()).for_each(|nam| self.push(Some(nam)));
rule.pats.iter().flat_map(|p| p.bind_or_eras().flatten()).for_each(|nam| self.push(Some(nam)));
self.unique_names_in_term(&mut rule.body);
rule
.pats
.iter_mut()
.flat_map(|p| p.binds_mut())
.flat_map(|p| p.bind_or_eras_mut().flatten())
.rev()
.for_each(|nam| *nam = self.pop(Some(nam)).unwrap());
}
@ -80,21 +92,18 @@ impl UniqueNameGenerator {
Term::Var { nam } => *nam = self.use_var(nam),
// Others
Term::App { fun: fst, arg: snd, .. }
| Term::Sup { fst, snd, .. }
| Term::Tup { fst, snd }
| Term::Opx { fst, snd, .. } => {
Term::Lst { els } | Term::Sup { els, .. } | Term::Tup { els } => {
for el in els {
self.unique_names_in_term(el);
}
}
Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => {
self.unique_names_in_term(fst);
self.unique_names_in_term(snd);
}
// Global lam names are already unique, so no need to do anything
Term::Chn { bod, .. } => self.unique_names_in_term(bod),
Term::Lnk { .. } | Term::Ref { .. } | Term::Era | Term::Num { .. } | Term::Str { .. } | Term::Err => (),
Term::Let { .. } => {
unreachable!("Let terms other than tuple destruction should have been desugared already.")
}
Term::Lst { .. } => unreachable!("Should have been desugared already."),
}
}

8
tests/golden_tests/run_lazy/def_tups.hvm
View File

@ -1,3 +1,9 @@
go (a, (b, (c, (d, e)))) = (+ (+ (+ (+ e d) c) b) a)
main = (go (1, (2, (3, (4, 5)))))
go2 (a, b, c, d, e) = (+ (+ (+ (+ e d) c) b) a)
main = (
(go (1, (2, (3, (4, 5))))),
(go2 (1, 2, 3, 4, 5))
)

7
tests/snapshots/compile_file__huge_tree.hvm.snap
View File

@ -1,9 +1,9 @@
---
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file/huge_matrix.hvm
input_file: tests/golden_tests/compile_file/huge_tree.hvm
---
@Leaf = (a {2 * {2 {4 a b} b}})
@Node = (a (b (c (d {2 {12 a {10 b {8 c {6 d e}}}} {2 * e}}))))
@Leaf = (a {2 * {2 {2 a b} b}})
@Node = (a (b (c (d {2 {2 a {2 b {2 c {2 d e}}}} {2 * e}}))))
@main = a
& @Node ~ (b (c (d (e a))))
& @Leaf ~ (#0 e)
@ -68578,4 +68578,3 @@ input_file: tests/golden_tests/compile_file/huge_matrix.hvm
& @Leaf ~ (#0 jlxd)
& @Leaf ~ (#1 ilxd)
& @Leaf ~ (#1 hlxd)

6
tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap
View File

@ -4,10 +4,10 @@ input_file: tests/golden_tests/compile_file_o_all/adt_option_and.hvm
---
@None = {2 * {2 a a}}
@Option.and = ({2 @Option.and$S2 {2 @Option.and$S3_$_Option.and$S1 a}} a)
@Option.and$S0 = {4 a (b {2 {4 [b a] c} {2 * c}})}
@Option.and$S2 = {4 a ({2 @Option.and$S0 {2 @Option.and$S3_$_Option.and$S1 (a b)}} b)}
@Option.and$S0 = {2 a (b {2 {2 [b a] c} {2 * c}})}
@Option.and$S2 = {2 a ({2 @Option.and$S0 {2 @Option.and$S3_$_Option.and$S1 (a b)}} b)}
@Option.and$S3_$_Option.and$S1 = (* @None)
@Some = (a {2 {4 a b} {2 * b}})
@Some = (a {2 {2 a b} {2 * b}})
@main = a
& @Option.and ~ (b (c a))
& @Some ~ (#3 c)

13
tests/snapshots/compile_file_o_all__expr.hvm.snap
View File

@ -2,17 +2,17 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/expr.hvm
---
@App = (a (b {4 * {4 * {4 {12 a {10 b c}} {4 * {4 * {4 * {4 * {4 * {4 * c}}}}}}}}}))
@Dup = (a (b (c (d {4 * {4 * {4 * {4 * {4 * {4 * {4 {36 a {34 b {32 c {30 d e}}}} {4 * {4 * e}}}}}}}}}))))
@Let = (a (b (c {4 * {4 * {4 * {4 * {4 * {4 {28 a {26 b {24 c d}}} {4 * {4 * {4 * d}}}}}}}}})))
@App = (a (b {4 * {4 * {4 {4 a {4 b c}} {4 * {4 * {4 * {4 * {4 * {4 * c}}}}}}}}}))
@Dup = (a (b (c (d {4 * {4 * {4 * {4 * {4 * {4 * {4 {4 a {4 b {4 c {4 d e}}}} {4 * {4 * e}}}}}}}}}))))
@Let = (a (b (c {4 * {4 * {4 * {4 * {4 * {4 {4 a {4 b {4 c d}}} {4 * {4 * {4 * d}}}}}}}}})))
@Mul = {2 * @Mul$S1}
@Mul$S0 = {2 a {2 * a}}
@Mul$S1 = {2 * @Mul$S0}
@Num = (a {4 * {4 {8 a b} {4 * {4 * {4 * {4 * {4 * {4 * {4 * b}}}}}}}}})
@Op2 = (a (b (c {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 {46 a {44 b {42 c d}}} d}}}}}}}}})))
@Num = (a {4 * {4 {4 a b} {4 * {4 * {4 * {4 * {4 * {4 * {4 * b}}}}}}}}})
@Op2 = (a (b (c {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 {4 a {4 b {4 c d}}} d}}}}}}}}})))
@Sub = {2 * @Sub$S0}
@Sub$S0 = {2 a {2 * {2 * a}}}
@Var = (a {4 {6 a b} {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 * b}}}}}}}}})
@Var = (a {4 {4 a b} {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 * b}}}}}}}}})
@main = a
& @Let ~ (b (c (d a)))
& @Dup ~ (e (f (g (h d))))
@ -28,4 +28,3 @@ input_file: tests/golden_tests/compile_file_o_all/expr.hvm
& @Num ~ (#1 m)
& @Num ~ (#2 l)
& @Var ~ (#0 b)

4
tests/snapshots/compile_file_o_all__let_adt_destructuring.hvm.snap
View File

@ -2,8 +2,8 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/let_adt_destructuring.hvm
---
@Box = (a {2 {4 a b} b})
@Unbox = ({2 {4 a a} b} b)
@Box = (a {2 {2 a b} b})
@Unbox = ({2 {2 a a} b} b)
@main = a
& @Unbox ~ (b a)
& @Box ~ (#1 b)

20
tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap
View File

@ -2,25 +2,25 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
---
@Cons = (a (b {4 {6 a {8 b c}} {4 * c}}))
@Cons = (a (b {4 {4 a {4 b c}} {4 * c}}))
@If$S0 = (a (* a))
@If$S1 = (* (a a))
@Map = ({4 @Map$S0 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 a}} a)
@Map$S0 = {6 a {8 {4 @Map$S0 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (b c)}} ({5 (a d) b} {4 {6 d {8 c e}} {4 * e}})}}
@Merge$S0 = {6 {9 a {11 b c}} {8 {7 d {4 @Merge$S0 {4 @Merge$S1 (e (f (g h)))}}} ({19 (i (a {2 @If$S0 {2 @If$S1 ({4 {6 j {8 k l}} {4 * l}} ({4 {6 c {8 h m}} {4 * m}} n))}})) {21 o e}} ({15 i {17 j f}} ({13 {4 @Merge$S2 {4 @Merge$S3 (o ({4 {6 b {8 d p}} {4 * p}} k))}} g} n)))}}
@Map$S0 = {4 a {4 {4 @Map$S0 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (b c)}} ({5 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
@Merge$S0 = {4 {9 a {9 b c}} {4 {7 d {4 @Merge$S0 {4 @Merge$S1 (e (f (g h)))}}} ({15 (i (a {2 @If$S0 {2 @If$S1 ({4 {4 j {4 k l}} {4 * l}} ({4 {4 c {4 h m}} {4 * m}} n))}})) {15 o e}} ({13 i {13 j f}} ({11 {4 @Merge$S2 {4 @Merge$S3 (o ({4 {4 b {4 d p}} {4 * p}} k))}} g} n)))}}
@Merge$S1 = (* @Cons)
@Merge$S2 = {6 a {8 b (c ({4 @Merge$S0 {4 @Merge$S1 (c (a (b d)))}} d))}}
@Merge$S2 = {4 a {4 b (c ({4 @Merge$S0 {4 @Merge$S1 (c (a (b d)))}} d))}}
@Merge$S3 = (* (a a))
@MergePair$S0 = {6 a {8 {4 @MergePair$S3 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (b c)}} ({23 d b} ({4 @Merge$S2 {4 @Merge$S3 (d (a e))}} {4 {6 e {8 c f}} {4 * f}}))}}
@MergePair$S1 = (a {4 {6 a {8 @Nil b}} {4 * b}})
@MergePair$S0 = {4 a {4 {4 @MergePair$S3 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (b c)}} ({17 d b} ({4 @Merge$S2 {4 @Merge$S3 (d (a e))}} {4 {4 e {4 c f}} {4 * f}}))}}
@MergePair$S1 = (a {4 {4 a {4 @Nil b}} {4 * b}})
@MergePair$S2 = (* @MergePair$S1)
@MergePair$S3 = {6 a {8 {4 @MergePair$S0 {4 @MergePair$S2 (b (a c))}} (b c)}}
@MergePair$S3 = {4 a {4 {4 @MergePair$S0 {4 @MergePair$S2 (b (a c))}} (b c)}}
@Nil = {4 * {4 a a}}
@Pure = (a {4 {6 a {8 @Nil b}} {4 * b}})
@Pure = (a {4 {4 a {4 @Nil b}} {4 * b}})
@Unpack = (a ({4 @Unpack$S2 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (a b)}} b))
@Unpack$S0 = {6 a {8 {4 @MergePair$S3 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (b {4 @Unpack$S0 {4 @Unpack$S1 (c (d e))}})}} ({3 c {23 f b}} ({4 @Merge$S2 {4 @Merge$S3 (f (a d))}} e))}}
@Unpack$S0 = {4 a {4 {4 @MergePair$S3 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (b {4 @Unpack$S0 {4 @Unpack$S1 (c (d e))}})}} ({3 c {17 f b}} ({4 @Merge$S2 {4 @Merge$S3 (f (a d))}} e))}}
@Unpack$S1 = (* (a a))
@Unpack$S2 = {6 a {8 {4 @Unpack$S0 {4 @Unpack$S1 (b (a c))}} (b c)}}
@Unpack$S2 = {4 a {4 {4 @Unpack$S0 {4 @Unpack$S1 (b (a c))}} (b c)}}
@Unpack$S3_$_MergePair$S4_$_Map$S1 = (* @Nil)
@main = (a (b c))
& @Unpack ~ (a (d c))

7
tests/snapshots/compile_file_o_all__list_reverse.hvm.snap
View File

@ -2,8 +2,8 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/list_reverse.hvm
---
@concat$S0 = {4 a {6 {2 @concat$S0 {2 (b b) (c d)}} (c {2 {4 a {6 d e}} {2 * e}})}}
@cons = (a (b {2 {4 a {6 b c}} {2 * c}}))
@concat$S0 = {2 a {2 {2 @concat$S0 {2 (b b) (c d)}} (c {2 {2 a {2 d e}} {2 * e}})}}
@cons = (a (b {2 {2 a {2 b c}} {2 * c}}))
@main = a
& @reverse ~ (b a)
& @cons ~ (#3 (c b))
@ -11,5 +11,4 @@ input_file: tests/golden_tests/compile_file_o_all/list_reverse.hvm
& @cons ~ (#1 (@nil d))
@nil = {2 * {2 a a}}
@reverse = ({2 @reverse$S0 {2 @nil a}} a)
@reverse$S0 = {4 a {6 {2 @reverse$S0 {2 @nil {2 @concat$S0 {2 (b b) ({2 {4 a {6 @nil c}} {2 * c}} d)}}}} d}}
@reverse$S0 = {2 a {2 {2 @reverse$S0 {2 @nil {2 @concat$S0 {2 (b b) ({2 {2 a {2 @nil c}} {2 * c}} d)}}}} d}}

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

@ -2,7 +2,7 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/long_str_file.hvm
---
@String.cons = (a (b {2 {6 a {4 b c}} {2 * c}}))
@String.cons = (a (b {2 {2 a {2 b c}} {2 * c}}))
@String.nil = {2 * {2 a a}}
@main = a
& @String.cons ~ (#40 (b a))

4
tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap
View File

@ -2,9 +2,9 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/match_dup_and_reconstruction.hvm
---
@Boxed = (a {2 {4 a b} b})
@Boxed = (a {2 {2 a b} b})
@Got = ({3 {2 @Got$S0 (a b)} a} b)
@Got$S0 = {4 a (b [b a])}
@Got$S0 = {2 a (b [b a])}
@main = a
& @Got ~ (b a)
& @Boxed ~ (#10 b)

4
tests/snapshots/compile_file_o_all__nested_adt_match.hvm.snap
View File

@ -2,7 +2,7 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/nested_adt_match.hvm
---
@Some = (a {2 {4 a b} {2 * b}})
@Some = (a {2 {2 a b} {2 * b}})
@main = a
& @Some ~ (b {2 {4 {2 {4 c c} {2 #0 d}} d} {2 #0 a}})
& @Some ~ (b {2 {2 {2 {2 c c} {2 #0 d}} d} {2 #0 a}})
& @Some ~ (#1 b)

4
tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap
View File

@ -5,9 +5,9 @@ input_file: tests/golden_tests/compile_file_o_all/scrutinee_reconstruction.hvm
@None = {2 * {2 a a}}
@Option.or = ({3 {2 @Option.or$S1 {2 @Option.or$S2 (a b)}} a} b)
@Option.or$S0 = (a (* a))
@Option.or$S1 = {4 * @Option.or$S0}
@Option.or$S1 = {2 * @Option.or$S0}
@Option.or$S2 = (* (a a))
@Some = (a {2 {4 a b} {2 * b}})
@Some = (a {2 {2 a b} {2 * b}})
@main = a
& @Option.or ~ (b (@None a))
& @Some ~ (#5 b)

3
tests/snapshots/compile_file_o_all__str.hvm.snap
View File

@ -2,7 +2,7 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/str.hvm
---
@String.cons = (a (b {2 {6 a {4 b c}} {2 * c}}))
@String.cons = (a (b {2 {2 a {2 b c}} {2 * c}}))
@String.nil = {2 * {2 a a}}
@main = a
& @String.cons ~ (#109 (b a))
@ -11,4 +11,3 @@ input_file: tests/golden_tests/compile_file_o_all/str.hvm
& @String.cons ~ (#110 (e d))
& @String.cons ~ (#32 (f e))
& @String.cons ~ (#61 (@String.nil f))

4
tests/snapshots/compile_term__lets.hvm.snap
View File

@ -4,6 +4,6 @@ input_file: tests/golden_tests/compile_term/lets.hvm
---
a
& (b b) ~ (c (d (e a)))
& (f f) ~ {9 (g (h (i e))) {11 g {13 h i}}}
& (j j) ~ {5 (k (l d)) {7 k l}}
& (f f) ~ {7 (g (h (i e))) {7 g {7 h i}}}
& (j j) ~ {5 (k (l d)) {5 k l}}
& (m m) ~ {3 (n c) n}

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

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/desugar_file/dup_linearization.hvm
---
(main) = let {a a_dup} = *; let {a_2 a_2_dup} = a_dup; let {a_3 a_3_dup} = a_2_dup; let {a_4 a_5} = a_3_dup; ((a, a_5), (a_4, (a_3, a_2)))
(main) = let {a a_2 a_3 a_4 a_5} = *; (a, a_5, a_4, a_3, a_2)

4
tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap
View File

@ -3,11 +3,11 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/adt_tup_era.hvm
---
TaggedScott:
(Foo) = λa #Tuple (a #Tuple.Pair.a λb #Tuple.Pair.b λc (#Tuple (b #Tuple.Pair.a λd #Tuple.Pair.b λ* λ* d) c))
(Foo) = λa #Tuple (a #Tuple λb #Tuple λc (#Tuple (b #Tuple λd #Tuple λ* λ* d) c))
(Main) = (Foo (Pair 1 5))
(Pair) = λa λb #Tuple λc #Tuple.Pair.b (#Tuple.Pair.a (c a) b)
(Pair) = λa λb #Tuple λc #Tuple (c a b)
Scott:
(Foo) = λa (a λb λc (b λd λ* λ* d c))

10
tests/snapshots/encode_pattern_match__and3.hvm.snap
View File

@ -3,21 +3,19 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/and3.hvm
---
TaggedScott:
(And) = λa let (b, c) = a; (#Bool (b λd let (f, g) = d; (#Bool (f λh #Bool (h T F) λ* F) g) λ* F) c)
(And) = λa let (b, c, d) = a; (#Bool (b λe λf (#Bool (e λh #Bool (h T F) λ* F) f) λ* λ* F) c d)
(main) = (And (F, (T, F)))
(main) = (And (F, T, F))
(F) = #Bool λ* #Bool λb b
(T) = #Bool λa #Bool λ* a
Scott:
(And) = λa let (b, c) = a; (b λd let (f, g) = d; (f λh (h T F) λ* F g) λ* F c)
(And) = λa let (b, c, d) = a; (b λe λf (e λh (h T F) λ* F f) λ* λ* F c d)
(main) = (And (F, (T, F)))
(main) = (And (F, T, F))
(F) = λ* λb b
(T) = λa λ* a

6
tests/snapshots/encode_pattern_match__box.hvm.snap
View File

@ -3,13 +3,11 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/box.hvm
---
TaggedScott:
(unbox) = λa #box (a #box.new.val λb b)
(unbox) = λa #box (a #box λb b)
(new) = λa #box λb #box.new.val (b a)
(new) = λa #box λb #box (b a)
Scott:
(unbox) = λa (a λb b)
(new) = λa λb (b a)

12
tests/snapshots/encode_pattern_match__common.hvm.snap
View File

@ -11,19 +11,19 @@ TaggedScott:
(North) = #Direction λa #Direction λ* #Direction λ* #Direction λ* a
(Filled) = λa #Box λb #Box λ* #Box.Filled.value (b a)
(Filled) = λa #Box λb #Box λ* #Box (b a)
(Empty) = #Box λ* #Box λb b
(Some) = λa #Option λb #Option λ* #Option.Some.x (b a)
(Some) = λa #Option λb #Option λ* #Option (b a)
(None) = #Option λ* #Option λb b
(Ok) = λa #Result λb #Result λ* #Result.Ok.a (b a)
(Ok) = λa #Result λb #Result λ* #Result (b a)
(Err) = λa #Result λ* #Result λc #Result.Err.b (c a)
(Err) = λa #Result λ* #Result λc #Result (c a)
(Cons) = λa λb #List_ λc #List_ λ* #List_.Cons.xs (#List_.Cons.x (c a) b)
(Cons) = λa λb #List_ λc #List_ λ* #List_ (c a b)
(Nil) = #List_ λ* #List_ λb b
@ -71,5 +71,3 @@ Scott:
(Yellow) = λ* λb λ* b
(Green) = λ* λ* λc c

6
tests/snapshots/encode_pattern_match__concat.hvm.snap
View File

@ -3,11 +3,11 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/concat.hvm
---
TaggedScott:
(String.concat) = λa λb (#String (a #String.String.cons.head λc #String.String.cons.tail λd λe (String.cons c (String.concat d e)) λh h) b)
(String.concat) = λa λb (#String (a #String λc #String λd λe (String.cons c (String.concat d e)) λh h) b)
(main) = (String.concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b)
(String.cons) = λa λb #String λc #String λ* #String (c a b)
(String.nil) = #String λ* #String λb b
@ -19,5 +19,3 @@ Scott:
(String.cons) = λa λb λc λ* (c a b)
(String.nil) = λ* λb b

6
tests/snapshots/encode_pattern_match__concat_def.hvm.snap
View File

@ -3,11 +3,11 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/concat_def.hvm
---
TaggedScott:
(concat) = λa λb (#String (a #String.String.cons.head λc #String.String.cons.tail λd λe (String.cons c (concat d e)) λi i) b)
(concat) = λa λb (#String (a #String λc #String λd λe (String.cons c (concat d e)) λi i) b)
(main) = (concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b)
(String.cons) = λa λb #String λc #String λ* #String (c a b)
(String.nil) = #String λ* #String λb b
@ -19,5 +19,3 @@ Scott:
(String.cons) = λa λb λc λ* (c a b)
(String.nil) = λ* λb b

8
tests/snapshots/encode_pattern_match__definition_merge.hvm.snap
View File

@ -3,15 +3,15 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/definition_merge.hvm
---
TaggedScott:
(Foo) = λa λb (#Either (a #Either.Left.value λc λd (#Bool (c λe #Either (e #Either.Left.value λg #Bool (g 1 1) #Either.Right.value λj #Bool (j 2 2)) λm #Either (m #Either.Left.value λo #Bool (o 1 1) #Either.Right.value λr #Bool (r 2 2))) d) #Either.Right.value λu λv (#Bool (u λw #Either (w #Either.Left.value λy #Bool (y 3 3) #Either.Right.value λbb #Bool (bb 3 3)) λeb #Either (eb #Either.Left.value λgb #Bool (gb 3 3) #Either.Right.value λjb #Bool (jb 3 3))) v)) b)
(Foo) = λa λb (#Either (a #Either λc λd (#Bool (c λe #Either (e #Either λg #Bool (g 1 1) #Either λj #Bool (j 2 2)) λm #Either (m #Either λo #Bool (o 1 1) #Either λr #Bool (r 2 2))) d) #Either λu λv (#Bool (u λw #Either (w #Either λy #Bool (y 3 3) #Either λbb #Bool (bb 3 3)) λeb #Either (eb #Either λgb #Bool (gb 3 3) #Either λjb #Bool (jb 3 3))) v)) b)
(False) = #Bool λ* #Bool λb b
(True) = #Bool λa #Bool λ* a
(Right) = λa #Either λ* #Either λc #Either.Right.value (c a)
(Right) = λa #Either λ* #Either λc #Either (c a)
(Left) = λa #Either λb #Either λ* #Either.Left.value (b a)
(Left) = λa #Either λb #Either λ* #Either (b a)
Scott:
(Foo) = λa λb (a λc λd (c λe (e λg (g 1 1) λj (j 2 2)) λm (m λo (o 1 1) λr (r 2 2)) d) λu λv (u λw (w λy (y 3 3) λbb (bb 3 3)) λeb (eb λgb (gb 3 3) λjb (jb 3 3)) v) b)
@ -23,5 +23,3 @@ Scott:
(Right) = λa λ* λc (c a)
(Left) = λa λb λ* (b a)

20
tests/snapshots/encode_pattern_match__expr.hvm.snap
View File

@ -11,23 +11,23 @@ TaggedScott:
(Add) = #Op λa #Op λ* #Op λ* #Op λ* a
(Var) = λa #Expr λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.Var.name (b a)
(Var) = λa #Expr λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (b a)
(Num) = λa #Expr λ* #Expr λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.Num.val (c a)
(Num) = λa #Expr λ* #Expr λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (c a)
(App) = λa λb #Expr λ* #Expr λ* #Expr λe #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.App.arg (#Expr.App.fun (e a) b)
(App) = λa λb #Expr λ* #Expr λ* #Expr λe #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (e a b)
(Fun) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λf #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.Fun.body (#Expr.Fun.name (f a) b)
(Fun) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λf #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (f a b)
(If) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λh #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.If.else (#Expr.If.then (#Expr.If.cond (h a) b) c)
(If) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λh #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (h a b c)
(Let) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λi #Expr λ* #Expr λ* #Expr λ* #Expr.Let.next (#Expr.Let.val (#Expr.Let.bind (i a) b) c)
(Let) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λi #Expr λ* #Expr λ* #Expr λ* #Expr (i a b c)
(Dup) = λa λb λc λd #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λk #Expr λ* #Expr λ* #Expr.Dup.next (#Expr.Dup.val (#Expr.Dup.snd (#Expr.Dup.fst (k a) b) c) d)
(Dup) = λa λb λc λd #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λk #Expr λ* #Expr λ* #Expr (k a b c d)
(Tup) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λj #Expr λ* #Expr.Tup.snd (#Expr.Tup.fst (j a) b)
(Tup) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λj #Expr λ* #Expr (j a b)
(Op2) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λl #Expr.Op2.snd (#Expr.Op2.fst (#Expr.Op2.op (l a) b) c)
(Op2) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λl #Expr (l a b c)
Scott:
(Div) = λ* λ* λ* λd d
@ -55,5 +55,3 @@ Scott:
(Tup) = λa λb λ* λ* λ* λ* λ* λ* λ* λj λ* (j a b)
(Op2) = λa λb λc λ* λ* λ* λ* λ* λ* λ* λ* λl (l a b c)

6
tests/snapshots/encode_pattern_match__is_some_some.hvm.snap
View File

@ -3,13 +3,13 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/is_some_some.hvm
---
TaggedScott:
(some_some) = λa #Option (a #Option.Some.x λb #Option (b #Option.Some.x λ* 1 0) 0)
(some_some) = λa #Option (a #Option λb #Option (b #Option λ* 1 0) 0)
(main) = (some_some (Some 1))
(None) = #Option λ* #Option λb b
(Some) = λa #Option λb #Option λ* #Option.Some.x (b a)
(Some) = λa #Option λb #Option λ* #Option (b a)
Scott:
(some_some) = λa (a λb (b λ* 1 0) 0)
@ -19,5 +19,3 @@ Scott:
(None) = λ* λb b
(Some) = λa λb λ* (b a)

14
tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap
View File

@ -7,19 +7,19 @@ TaggedScott:
(Pure) = λa (Cons a Nil)
(Map) = λa λb (#List_ (a #List_.Cons.head λc #List_.Cons.tail λd λe let {f f_2} = e; (Cons (f c) (Map d f_2)) λ* Nil) b)
(Map) = λa λb (#List_ (a #List_ λc #List_ λd λe let {f f_2} = e; (Cons (f c) (Map d f_2)) λ* Nil) b)
(MergeSort) = λa λb (Unpack a (Map b Pure))
(Unpack) = λa λb (#List_ (b #List_.Cons.head λc #List_.Cons.tail λd λe (#List_ (d #List_.Cons.head λf #List_.Cons.tail λg λh λi let {o o_2} = h; (Unpack o (MergePair o_2 (Cons i (Cons f g)))) λ* λq q) e c) λ* Nil) a)
(Unpack) = λa λb (#List_ (b #List_ λc #List_ λd λe (#List_ (d #List_ λf #List_ λg λh λi let {o o_2} = h; (Unpack o (MergePair o_2 (Cons i (Cons f g)))) λ* λq q) e c) λ* Nil) a)
(MergePair) = λa λb (#List_ (b #List_.Cons.head λc #List_.Cons.tail λd λe (#List_ (d #List_.Cons.head λf #List_.Cons.tail λg λh λi let {m m_2} = h; (Cons (Merge m i f) (MergePair m_2 g)) λ* λo (Cons o Nil)) e c) λ* Nil) a)
(MergePair) = λa λb (#List_ (b #List_ λc #List_ λd λe (#List_ (d #List_ λf #List_ λg λh λi let {m m_2} = h; (Cons (Merge m i f) (MergePair m_2 g)) λ* λo (Cons o Nil)) e c) λ* Nil) a)
(Merge) = λa λb λc (#List_ (b #List_.Cons.head λd #List_.Cons.tail λe λf λg (#List_ (g #List_.Cons.head λh #List_.Cons.tail λi λj λk λl let {m m_2} = i; let {n n_dup} = h; let {n_2 n_3} = n_dup; let {o o_2} = l; let {p p_dup} = k; let {p_2 p_3} = p_dup; let {q q_dup} = j; let {q_2 q_3} = q_dup; (If (q p n) (Cons p_2 (Merge q_2 o (Cons n_2 m))) (Cons n_3 (Merge q_3 (Cons p_3 o_2) m_2))) λ* λu λv (Cons u v)) f d e) λ* λcb cb) a c)
(Merge) = λa λb λc (#List_ (b #List_ λd #List_ λe λf λg (#List_ (g #List_ λh #List_ λi λj λk λl let {m m_2} = i; let {n n_2 n_3} = h; let {o o_2} = l; let {p p_2 p_3} = k; let {q q_2 q_3} = j; (If (q p n) (Cons p_2 (Merge q_2 o (Cons n_2 m))) (Cons n_3 (Merge q_3 (Cons p_3 o_2) m_2))) λ* λu λv (Cons u v)) f d e) λ* λcb cb) a c)
(Nil) = #List_ λ* #List_ λb b
(Cons) = λa λb #List_ λc #List_ λ* #List_.Cons.tail (#List_.Cons.head (c a) b)
(Cons) = λa λb #List_ λc #List_ λ* #List_ (c a b)
(False) = #Bool λ* #Bool λb b
@ -38,7 +38,7 @@ Scott:
(MergePair) = λa λb (b λc λd λe (d λf λg λh λi let {m m_2} = h; (Cons (Merge m i f) (MergePair m_2 g)) λ* λo (Cons o Nil) e c) λ* Nil a)
(Merge) = λa λb λc (b λd λe λf λg (g λh λi λj λk λl let {m m_2} = i; let {n n_dup} = h; let {n_2 n_3} = n_dup; let {o o_2} = l; let {p p_dup} = k; let {p_2 p_3} = p_dup; let {q q_dup} = j; let {q_2 q_3} = q_dup; (If (q p n) (Cons p_2 (Merge q_2 o (Cons n_2 m))) (Cons n_3 (Merge q_3 (Cons p_3 o_2) m_2))) λ* λu λv (Cons u v) f d e) λ* λcb cb a c)
(Merge) = λa λb λc (b λd λe λf λg (g λh λi λj λk λl let {m m_2} = i; let {n n_2 n_3} = h; let {o o_2} = l; let {p p_2 p_3} = k; let {q q_2 q_3} = j; (If (q p n) (Cons p_2 (Merge q_2 o (Cons n_2 m))) (Cons n_3 (Merge q_3 (Cons p_3 o_2) m_2))) λ* λu λv (Cons u v) f d e) λ* λcb cb a c)
(Nil) = λ* λb b
@ -47,5 +47,3 @@ Scott:
(False) = λ* λb b
(True) = λa λ* a

10
tests/snapshots/encode_pattern_match__list_str_encoding_undeclared_fn.hvm.snap
View File

@ -5,15 +5,15 @@ input_file: tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared
TaggedScott:
(main) = *
(Foo) = λa #String (a #String.String.cons.head λ* #String.String.cons.tail λ* 1 0)
(Foo) = λa #String (a #String λ* #String λ* 1 0)
(Bar) = λa #List (a #List.List.cons.head λ* #List.List.cons.tail λ* 0 1)
(Bar) = λa #List (a #List λ* #List λ* 0 1)
(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b)
(String.cons) = λa λb #String λc #String λ* #String (c a b)
(String.nil) = #String λ* #String λb b
(List.cons) = λa λb #List λc #List λ* #List.List.cons.tail (#List.List.cons.head (c a) b)
(List.cons) = λa λb #List λc #List λ* #List (c a b)
(List.nil) = #List λ* #List λb b
@ -23,5 +23,3 @@ Scott:
(Foo) = λa (a λ* λ* 1 0)
(Bar) = λa (a λ* λ* 0 1)

8
tests/snapshots/encode_pattern_match__list_str_encoding_undeclared_map.hvm.snap
View File

@ -3,17 +3,15 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared_map.hvm
---
TaggedScott:
(main) = λa λb (#String (a #String.String.cons.head λ* #String.String.cons.tail λ* 1 2), #List (b #List.List.cons.head λ* #List.List.cons.tail λ* 1 2))
(main) = λa λb (#String (a #String λ* #String λ* 1 2), #List (b #List λ* #List λ* 1 2))
(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b)
(String.cons) = λa λb #String λc #String λ* #String (c a b)
(String.nil) = #String λ* #String λb b
(List.cons) = λa λb #List λc #List λ* #List.List.cons.tail (#List.List.cons.head (c a) b)
(List.cons) = λa λb #List λc #List λ* #List (c a b)
(List.nil) = #List λ* #List λb b
Scott:
(main) = λa λb ((a λ* λ* 1 2), (b λ* λ* 1 2))

6
tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap
View File

@ -3,9 +3,9 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hvm
---
TaggedScott:
(main) = (#Maybe ((Some 1) λ$x * #Maybe.Some.val λc c) $x)
(main) = (#Maybe ((Some 1) λ$x * #Maybe λc c) $x)
(Some) = λa #Maybe λ* #Maybe λc #Maybe.Some.val (c a)
(Some) = λa #Maybe λ* #Maybe λc #Maybe (c a)
(None) = #Maybe λa #Maybe λ* a
@ -15,5 +15,3 @@ Scott:
(Some) = λa λ* λc (c a)
(None) = λa λ* a

8
tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap
View File

@ -3,13 +3,13 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm
---
TaggedScott:
(Foo) = λ$x #Maybe ((Some 1) $x #Maybe.Some.val λc c)
(Foo) = λ$x #Maybe ((Some 1) $x #Maybe λc c)
(Bar) = (#Maybe ((Some 1) $x #Maybe.Some.val λc c) λ$x *)
(Bar) = (#Maybe ((Some 1) $x #Maybe λc c) λ$x *)
(main) = *
(Some) = λa #Maybe λ* #Maybe λc #Maybe.Some.val (c a)
(Some) = λa #Maybe λ* #Maybe λc #Maybe (c a)
(None) = #Maybe λa #Maybe λ* a
@ -23,5 +23,3 @@ Scott:
(Some) = λa λ* λc (c a)
(None) = λa λ* a

6
tests/snapshots/encode_pattern_match__match_list_sugar.hvm.snap
View File

@ -3,11 +3,11 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/match_list_sugar.hvm
---
TaggedScott:
(main) = #List (List.nil #List.List.cons.head λ* #List.List.cons.tail λ* 1 0)
(main) = #List (List.nil #List λ* #List λ* 1 0)
(List.nil) = #List λ* #List λb b
(List.cons) = λa λb #List λc #List λ* #List.List.cons.tail (#List.List.cons.head (c a) b)
(List.cons) = λa λb #List λc #List λ* #List (c a b)
Scott:
(main) = (List.nil λ* λ* 1 0)
@ -15,5 +15,3 @@ Scott:
(List.nil) = λ* λb b
(List.cons) = λa λb λc λ* (c a b)

20
tests/snapshots/encode_pattern_match__match_many_args.hvm.snap
View File

@ -3,29 +3,29 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/match_many_args.hvm
---
TaggedScott:
(tail_tail) = λa #L (a #L.C.h λb #L.C.t λc (#L (c #L.C.h λ* #L.C.t λe λ* e λ* N) b) N)
(tail_tail) = λa #L (a #L λb #L λc (#L (c #L λ* #L λe λ* e λ* N) b) N)
(or) = λa λb (#Option (b #Option.Some.val λc λ* c λf f) a)
(or) = λa λb (#Option (b #Option λc λ* c λf f) a)
(or2) = λa λb (#Option (a #Option.Some.val λc λ* c λf f) b)
(or2) = λa λb (#Option (a #Option λc λ* c λf f) b)
(map) = λa λb (#Option (b #Option.Some.val λc λd (d c) λ* None) a)
(map) = λa λb (#Option (b #Option λc λd (d c) λ* None) a)
(map2) = λa λb (#Option (b #Option.Some.val λc λd (d c) λ* None) a)
(map2) = λa λb (#Option (b #Option λc λd (d c) λ* None) a)
(flatten) = λa #Option (a #Option.Some.val λb #Option (b #Option.Some.val λc (Some c) None) None)
(flatten) = λa #Option (a #Option λb #Option (b #Option λc (Some c) None) None)
(map_pair) = λa λb λc (#L (b #L.C.h λd #L.C.t λe λf λg (#L (g #L.C.h λh #L.C.t λi λj λk λl (C (j k h) (map_pair l i)) λ* λ* λ* N) f d e) λ* λ* N) a c)
(map_pair) = λa λb λc (#L (b #L λd #L λe λf λg (#L (g #L λh #L λi λj λk λl (C (j k h) (map_pair l i)) λ* λ* λ* N) f d e) λ* λ* N) a c)
(main) = *
(None) = #Option λ* #Option λb b
(Some) = λa #Option λb #Option λ* #Option.Some.val (b a)
(Some) = λa #Option λb #Option λ* #Option (b a)
(N) = #L λ* #L λb b
(C) = λa λb #L λc #L λ* #L.C.t (#L.C.h (c a) b)
(C) = λa λb #L λc #L λ* #L (c a b)
Scott:
(tail_tail) = λa (a λb λc (c λ* λe λ* e λ* N b) N)
@ -51,5 +51,3 @@ Scott:
(N) = λ* λb b
(C) = λa λb λc λ* (c a b)

14
tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
View File

@ -3,22 +3,22 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm
---
TaggedScott:
(Parse) = λa λb (#String (b #String.String.cons.head λc #String.String.cons.tail λd λe (match (- c 40) { 0: λf λg (Ok (40, (g, f))); 1+: λk match k { 0: λl λm (Ok (41, (m, l))); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, (s, r))); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb))) a)
(Parse) = λa λb (#String (b #String λc #String λd λe (match (- c 40) { 0: λf λg (Ok (40, g, f)); 1+: λk match k { 0: λl λm (Ok (41, m, l)); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, s, r)); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb))) a)
(main) = #Result ((Parse * (String.cons 40 (String.cons 43 String.nil))) #Result.Ok.val λd let (e, f) = d; (let (g, h) = f; λi (i, (Parse h g)) e) #Result.Err.err λm (Err m))
(main) = #Result ((Parse * (String.cons 40 (String.cons 43 String.nil))) #Result λd let (e, f, g) = d; (e, (Parse g f)) #Result λk (Err k))
(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b)
(String.cons) = λa λb #String λc #String λ* #String (c a b)
(String.nil) = #String λ* #String λb b
(Err) = λa #Result λ* #Result λc #Result.Err.err (c a)
(Err) = λa #Result λ* #Result λc #Result (c a)
(Ok) = λa #Result λb #Result λ* #Result.Ok.val (b a)
(Ok) = λa #Result λb #Result λ* #Result (b a)
Scott:
(Parse) = λa λb (b λc λd λe (match (- c 40) { 0: λf λg (Ok (40, (g, f))); 1+: λk match k { 0: λl λm (Ok (41, (m, l))); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, (s, r))); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb)) a)
(Parse) = λa λb (b λc λd λe (match (- c 40) { 0: λf λg (Ok (40, g, f)); 1+: λk match k { 0: λl λm (Ok (41, m, l)); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, s, r)); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb)) a)
(main) = (Parse * (String.cons 40 (String.cons 43 String.nil)) λd let (e, f) = d; (let (g, h) = f; λi (i, (Parse h g)) e) λm (Err m))
(main) = (Parse * (String.cons 40 (String.cons 43 String.nil)) λd let (e, f, g) = d; (e, (Parse g f)) λk (Err k))
(String.cons) = λa λb λc λ* (c a b)

6
tests/snapshots/encode_pattern_match__match_syntax.hvm.snap
View File

@ -3,11 +3,11 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/match_syntax.hvm
---
TaggedScott:
(head) = λa #List_ (a #List_.Cons.x λc #List_.Cons.xs λ* c Nil)
(head) = λa #List_ (a #List_ λc #List_ λ* c Nil)
(Nil) = #List_ λ* #List_ λb b
(Cons) = λa λb #List_ λc #List_ λ* #List_.Cons.xs (#List_.Cons.x (c a) b)
(Cons) = λa λb #List_ λc #List_ λ* #List_ (c a b)
Scott:
(head) = λa (a λc λ* c Nil)
@ -15,5 +15,3 @@ Scott:
(Nil) = λ* λb b
(Cons) = λa λb λc λ* (c a b)

8
tests/snapshots/encode_pattern_match__ntup_sum.hvm.snap
View File

@ -3,11 +3,11 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/ntup_sum.hvm
---
TaggedScott:
(ntupSum) = λa let (b, c) = a; (let (d, e) = b; λf (let (g, h) = f; λi λj (let (k, l) = h; λm λn λo (+ m (+ n (+ o (+ k l)))) i j g) d e) c)
(ntupSum) = λa let (b, c, d, e, f) = a; (+ b (+ c (+ d (+ e f))))
(main) = (ntupSum ((1, 3), (3, (2, 1))))
(main) = (ntupSum (1, 3, 3, 2, 1))
Scott:
(ntupSum) = λa let (b, c) = a; (let (d, e) = b; λf (let (g, h) = f; λi λj (let (k, l) = h; λm λn λo (+ m (+ n (+ o (+ k l)))) i j g) d e) c)
(ntupSum) = λa let (b, c, d, e, f) = a; (+ b (+ c (+ d (+ e f))))
(main) = (ntupSum ((1, 3), (3, (2, 1))))
(main) = (ntupSum (1, 3, 3, 2, 1))

14
tests/snapshots/encode_pattern_match__pattern_match_encoding.hvm.snap
View File

@ -3,19 +3,19 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/encode_pattern_match/pattern_match_encoding.hvm
---
TaggedScott:
(Foo) = λa #MyType (a #MyType.A.a λ* 100 #MyType.B.b λ* 200 #MyType.C.c λ* 200 #MyType.D.d1 λ* #MyType.D.d2 λ* 200 #MyType.E.e1 λ* #MyType.E.e2 λ* 200)
(Foo) = λa #MyType (a #MyType λ* 100 #MyType λ* 200 #MyType λ* 200 #MyType λ* #MyType λ* 200 #MyType λ* #MyType λ* 200)
(main) = (Foo A 2)
(E) = λa λb #MyType λ* #MyType λ* #MyType λ* #MyType λ* #MyType λg #MyType.E.e2 (#MyType.E.e1 (g a) b)
(E) = λa λb #MyType λ* #MyType λ* #MyType λ* #MyType λ* #MyType λg #MyType (g a b)
(D) = λa λb #MyType λ* #MyType λ* #MyType λ* #MyType λf #MyType λ* #MyType.D.d2 (#MyType.D.d1 (f a) b)
(D) = λa λb #MyType λ* #MyType λ* #MyType λ* #MyType λf #MyType λ* #MyType (f a b)
(C) = λa #MyType λ* #MyType λ* #MyType λd #MyType λ* #MyType λ* #MyType.C.c (d a)
(C) = λa #MyType λ* #MyType λ* #MyType λd #MyType λ* #MyType λ* #MyType (d a)
(B) = λa #MyType λ* #MyType λc #MyType λ* #MyType λ* #MyType λ* #MyType.B.b (c a)
(B) = λa #MyType λ* #MyType λc #MyType λ* #MyType λ* #MyType λ* #MyType (c a)
(A) = λa #MyType λb #MyType λ* #MyType λ* #MyType λ* #MyType λ* #MyType.A.a (b a)
(A) = λa #MyType λb #MyType λ* #MyType λ* #MyType λ* #MyType λ* #MyType (b a)
Scott:
(Foo) = λa (a λ* 100 λ* 200 λ* 200 λ* λ* 200 λ* λ* 200)
@ -31,5 +31,3 @@ Scott:
(B) = λa λ* λc λ* λ* λ* (c a)
(A) = λa λb λ* λ* λ* λ* (b a)

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

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/linear_readback/church_mul.hvm
---
λa λb let #0{c g} = (let #1{d h} = a; d let #2{e f} = h; (e (f #0{g b}))); c
λa λb let #0{c g} = (let #1{d h} = a; d let #1{e f} = h; (e (f #0{g b}))); c

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

@ -3,6 +3,6 @@ source: tests/golden_tests.rs
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 Some.val): #Option.Some.val (#wrong_tag λb b Some.val); (None): * }
Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'
Invalid Adt Match
λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * }

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

@ -3,6 +3,6 @@ source: tests/golden_tests.rs
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 Some.val): #Option.Some.val (#wrong_tag λb b Some.val); (None): * }
Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'
Invalid Adt Match
λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * }

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

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/nested_str.hvm
---
(((String.cons "a" String.nil), (String.cons 97 (String.cons "bc" String.nil))), ((String.cons "ab" "c"), (String.cons "ab" (String.cons "cd" String.nil))))
((String.cons "a" String.nil), ((String.cons 97 (String.cons "bc" String.nil)), ((String.cons "ab" "c"), (String.cons "ab" (String.cons "cd" String.nil)))))

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

@ -3,6 +3,6 @@ source: tests/golden_tests.rs
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 Some.val): #Option.Some.val (#wrong_tag λb b Some.val); (None): * }
Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'
Invalid Adt Match
λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * }

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

@ -3,6 +3,6 @@ source: tests/golden_tests.rs
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 Some.val): #Option.Some.val (#wrong_tag λb b Some.val); (None): * }
Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'
Invalid Adt Match
λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * }

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

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_lazy/def_tups.hvm
---
15
(15, 15)

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

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_lazy/nested_str.hvm
---
(((String.cons "a" String.nil), (String.cons 97 (String.cons "bc" String.nil))), ((String.cons "ab" "c"), (String.cons "ab" (String.cons "cd" String.nil))))
((String.cons "a" String.nil), ((String.cons 97 (String.cons "bc" String.nil)), ((String.cons "ab" "c"), (String.cons "ab" (String.cons "cd" String.nil)))))

14
tests/snapshots/simplify_matches__already_flat.hvm.snap
View File

@ -14,20 +14,20 @@ input_file: tests/golden_tests/simplify_matches/already_flat.hvm
(Rule6) = λa a
(CtrB3) = λa #Baz λ* #Baz λ* #Baz λ* #Baz λe #Baz.CtrB3.b (e a)
(CtrB3) = λa #Baz λ* #Baz λ* #Baz λ* #Baz λe #Baz (e a)
(CtrB2) = λa #Baz λ* #Baz λ* #Baz λd #Baz λ* #Baz.CtrB2.b (d a)
(CtrB2) = λa #Baz λ* #Baz λ* #Baz λd #Baz λ* #Baz (d a)
(CtrB1) = λa #Baz λ* #Baz λc #Baz λ* #Baz λ* #Baz.CtrB1.b (c a)
(CtrB1) = λa #Baz λ* #Baz λc #Baz λ* #Baz λ* #Baz (c a)
(CtrB0) = #Baz λa #Baz λ* #Baz λ* #Baz λ* a
(CtrA) = #Foo λa #Foo λ* a
(CtrB) = λa #Foo λ* #Foo λc #Foo.CtrB.x (c a)
(CtrB) = λa #Foo λ* #Foo λc #Foo (c a)
(CtrA1) = λa #Bar λb #Bar λ* #Bar λ* #Bar.CtrA1.a (b a)
(CtrA1) = λa #Bar λb #Bar λ* #Bar λ* #Bar (b a)
(CtrA2) = λa λb #Bar λ* #Bar λd #Bar λ* #Bar.CtrA2.a2 (#Bar.CtrA2.a1 (d a) b)
(CtrA2) = λa λb #Bar λ* #Bar λd #Bar λ* #Bar (d a b)
(CtrA3) = λa #Bar λ* #Bar λ* #Bar λd #Bar.CtrA3.a (d a)
(CtrA3) = λa #Bar λ* #Bar λ* #Bar λd #Bar (d a)

4
tests/snapshots/simplify_matches__bits_dec.hvm.snap
View File

@ -4,8 +4,8 @@ input_file: tests/golden_tests/simplify_matches/bits_dec.hvm
---
(Data.Bits.dec) = λa match a { (Data.Bits.e): Data.Bits.e; (Data.Bits.o c): match c { (Data.Bits.e): Data.Bits.e; (Data.Bits.o e): (Data.Bits.i (Data.Bits.dec e)); (Data.Bits.i g): (Data.Bits.i (Data.Bits.dec g)) }; (Data.Bits.i i): match i { (Data.Bits.e): (Data.Bits.o Data.Bits.e); (Data.Bits.o k): (Data.Bits.o k); (Data.Bits.i m): (Data.Bits.o m) } }
(Data.Bits.i) = λa #Data.Bits λ* #Data.Bits λ* #Data.Bits λd #Data.Bits.Data.Bits.i.t (d a)
(Data.Bits.i) = λa #Data.Bits λ* #Data.Bits λ* #Data.Bits λd #Data.Bits (d a)
(Data.Bits.o) = λa #Data.Bits λ* #Data.Bits λc #Data.Bits λ* #Data.Bits.Data.Bits.o.t (c a)
(Data.Bits.o) = λa #Data.Bits λ* #Data.Bits λc #Data.Bits λ* #Data.Bits (c a)
(Data.Bits.e) = #Data.Bits λa #Data.Bits λ* #Data.Bits λ* a

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

@ -6,4 +6,4 @@ input_file: tests/golden_tests/simplify_matches/double_unwrap_box.hvm
(Main) = (DoubleUnbox (Box (Box 0)) 5)
(Box) = λa #Boxed λb #Boxed.Box.x (b a)
(Box) = λa #Boxed λb #Boxed (b a)

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

@ -8,4 +8,4 @@ input_file: tests/golden_tests/simplify_matches/double_unwrap_maybe.hvm
(None) = #Maybe λ* #Maybe λb b
(Some) = λa #Maybe λb #Maybe λ* #Maybe.Some.x (b a)
(Some) = λa #Maybe λb #Maybe λ* #Maybe (b a)

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

@ -8,4 +8,4 @@ input_file: tests/golden_tests/simplify_matches/flatten_with_terminal.hvm
(B) = #B_t λa a
(A) = λa #A_t λb #A_t.A.b (b a)
(A) = λa #A_t λb #A_t (b a)

8
tests/snapshots/simplify_matches__nested.hvm.snap
View File

@ -6,10 +6,10 @@ input_file: tests/golden_tests/simplify_matches/nested.hvm
(CtrC) = #Baz λa a
(CtrB2) = λa λb #Bar λ* #Bar λd #Bar.CtrB2.b (#Bar.CtrB2.a (d a) b)
(CtrB2) = λa λb #Bar λ* #Bar λd #Bar (d a b)
(CtrB1) = λa #Bar λb #Bar λ* #Bar.CtrB1.b (b a)
(CtrB1) = λa #Bar λb #Bar λ* #Bar (b a)
(CtrB) = λa #Foo λ* #Foo λc #Foo.CtrB.a (c a)
(CtrB) = λa #Foo λ* #Foo λc #Foo (c a)
(CtrA) = λa λb #Foo λc #Foo λ* #Foo.CtrA.b (#Foo.CtrA.a (c a) b)
(CtrA) = λa λb #Foo λc #Foo λ* #Foo (c a b)

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

@ -6,4 +6,4 @@ input_file: tests/golden_tests/simplify_matches/nested2.hvm
(List.nil) = #List λ* #List λb b
(List.cons) = λa λb #List λc #List λ* #List.List.cons.tail (#List.List.cons.head (c a) b)
(List.cons) = λa λb #List λc #List λ* #List (c a b)

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

@ -6,4 +6,4 @@ input_file: tests/golden_tests/simplify_matches/nested_0ary.hvm
(Nil) = #list λ* #list λb b
(Cons) = λa λb #list λc #list λ* #list.Cons.tail (#list.Cons.head (c a) b)
(Cons) = λa λb #list λc #list λ* #list (c a b)