mirror of
https://github.com/HigherOrderCO/Bend.git
synced 2024-09-17 14:47:21 +03:00
Merge pull request #245 from HigherOrderCO/bug/sc-525/float-combinators-not-extracting-some-terms
[sc-525] Float combinators not extracting some terms
This commit is contained in:
commit
817aec9d4a
@ -45,6 +45,7 @@
|
|||||||
"namegen",
|
"namegen",
|
||||||
"nams",
|
"nams",
|
||||||
"nats",
|
"nats",
|
||||||
|
"nullary",
|
||||||
"numop",
|
"numop",
|
||||||
"nums",
|
"nums",
|
||||||
"oper",
|
"oper",
|
||||||
@ -54,6 +55,7 @@
|
|||||||
"peekable",
|
"peekable",
|
||||||
"postcondition",
|
"postcondition",
|
||||||
"readback",
|
"readback",
|
||||||
|
"recursively",
|
||||||
"redex",
|
"redex",
|
||||||
"redexes",
|
"redexes",
|
||||||
"resugar",
|
"resugar",
|
||||||
|
@ -231,6 +231,7 @@ pub struct Name(GlobalString);
|
|||||||
/// A macro for creating iterators that can have statically known
|
/// A macro for creating iterators that can have statically known
|
||||||
/// different types. Useful for iterating over tree children, where
|
/// different types. Useful for iterating over tree children, where
|
||||||
/// each tree node variant yields a different iterator type.
|
/// each tree node variant yields a different iterator type.
|
||||||
|
#[macro_export]
|
||||||
macro_rules! multi_iterator {
|
macro_rules! multi_iterator {
|
||||||
($Iter:ident { $($Variant:ident),* $(,)? }) => {
|
($Iter:ident { $($Variant:ident),* $(,)? }) => {
|
||||||
#[derive(Debug, Clone)]
|
#[derive(Debug, Clone)]
|
||||||
|
@ -1,277 +1,175 @@
|
|||||||
use crate::term::{Book, Definition, Name, Rule, Term};
|
use indexmap::IndexSet;
|
||||||
use std::{
|
|
||||||
collections::{BTreeMap, BTreeSet},
|
use crate::{
|
||||||
ops::BitAnd,
|
multi_iterator,
|
||||||
};
|
term::{Book, Definition, Name, Rule, Term},
|
||||||
|
};
|
||||||
|
use std::collections::BTreeMap;
|
||||||
|
|
||||||
|
type Combinators = BTreeMap<Name, Definition>;
|
||||||
|
|
||||||
/// Replaces closed Terms (i.e. without free variables) with a Ref to the extracted term
|
|
||||||
/// Precondition: Vars must have been sanitized
|
|
||||||
impl Book {
|
impl Book {
|
||||||
|
/// Extracts unsafe terms into new definitions.
|
||||||
|
///
|
||||||
|
/// Precondition: Variables must have been sanitized.
|
||||||
|
///
|
||||||
|
/// The floating algorithm follows these rules:
|
||||||
|
/// - Recursively float every child term.
|
||||||
|
/// - Extract if it is a combinator and is not a safe term.
|
||||||
|
/// See [`Term::is_safe`] for what is considered safe here.
|
||||||
pub fn float_combinators(&mut self) {
|
pub fn float_combinators(&mut self) {
|
||||||
let mut combinators = Combinators::new();
|
let mut combinators = Combinators::new();
|
||||||
|
|
||||||
|
let slf = self.clone();
|
||||||
for (def_name, def) in self.defs.iter_mut() {
|
for (def_name, def) in self.defs.iter_mut() {
|
||||||
|
let mut name_gen = 0;
|
||||||
|
|
||||||
if self.entrypoint.as_ref().is_some_and(|m| m == def_name) {
|
if self.entrypoint.as_ref().is_some_and(|m| m == def_name) {
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
let builtin = def.builtin;
|
let builtin = def.builtin;
|
||||||
let rule = def.rule_mut();
|
let rule = def.rule_mut();
|
||||||
rule.body.float_combinators(def_name, builtin, &mut combinators);
|
let mut seen = IndexSet::new();
|
||||||
|
rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name, builtin, &mut seen);
|
||||||
}
|
}
|
||||||
|
|
||||||
// Definitions are not inserted to the book as they are defined to appease the borrow checker.
|
|
||||||
// Since we are mut borrowing the rules we can't borrow the book to insert at the same time.
|
|
||||||
self.defs.extend(combinators);
|
self.defs.extend(combinators);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
type Combinators = BTreeMap<Name, Definition>;
|
impl Term {
|
||||||
|
fn float_combinators(
|
||||||
|
&mut self,
|
||||||
|
combinators: &mut Combinators,
|
||||||
|
name_gen: &mut usize,
|
||||||
|
book: &Book,
|
||||||
|
def_name: &Name,
|
||||||
|
builtin: bool,
|
||||||
|
seen: &mut IndexSet<Name>,
|
||||||
|
) {
|
||||||
|
for term in self.float_children_mut() {
|
||||||
|
// Recursively float the children terms.
|
||||||
|
term.float_combinators(combinators, name_gen, book, def_name, builtin, seen);
|
||||||
|
|
||||||
#[derive(Debug)]
|
if term.is_combinator() && !term.is_safe(book, seen) {
|
||||||
struct TermInfo<'d> {
|
float_combinator(def_name, name_gen, term, builtin, combinators);
|
||||||
// Number of times a Term has been detached from the current Term
|
}
|
||||||
counter: u32,
|
|
||||||
def_name: Name,
|
|
||||||
|
|
||||||
builtin: bool,
|
|
||||||
needed_names: BTreeSet<Name>,
|
|
||||||
combinators: &'d mut Combinators,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'d> TermInfo<'d> {
|
|
||||||
fn new(def_name: Name, builtin: bool, combinators: &'d mut Combinators) -> Self {
|
|
||||||
Self { counter: 0, def_name, builtin, needed_names: BTreeSet::new(), combinators }
|
|
||||||
}
|
|
||||||
fn request_name(&mut self, name: &Name) {
|
|
||||||
self.needed_names.insert(name.clone());
|
|
||||||
}
|
|
||||||
|
|
||||||
fn provide(&mut self, name: Option<&Name>) {
|
|
||||||
if let Some(name) = name {
|
|
||||||
self.needed_names.remove(name);
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn has_no_free_vars(&self) -> bool {
|
|
||||||
self.needed_names.is_empty()
|
|
||||||
}
|
|
||||||
|
|
||||||
fn replace_scope(&mut self, new_scope: BTreeSet<Name>) -> BTreeSet<Name> {
|
|
||||||
std::mem::replace(&mut self.needed_names, new_scope)
|
|
||||||
}
|
|
||||||
|
|
||||||
fn merge_scope(&mut self, target: BTreeSet<Name>) {
|
|
||||||
self.needed_names.extend(target);
|
|
||||||
}
|
|
||||||
|
|
||||||
fn detach_term(&mut self, term: &mut Term) {
|
|
||||||
let comb_name = Name::new(format!("{}$C{}", self.def_name, self.counter));
|
|
||||||
self.counter += 1;
|
|
||||||
|
|
||||||
let comb_var = Term::Ref { nam: comb_name.clone() };
|
|
||||||
let extracted_term = std::mem::replace(term, comb_var);
|
|
||||||
|
|
||||||
let rules = vec![Rule { body: extracted_term, pats: Vec::new() }];
|
|
||||||
let rule = Definition { name: comb_name.clone(), rules, builtin: self.builtin };
|
|
||||||
self.combinators.insert(comb_name, rule);
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Debug)]
|
/// Inserts a new definition for the given term in the combinators map.
|
||||||
enum Detach {
|
fn float_combinator(
|
||||||
/// Can be detached freely
|
def_name: &Name,
|
||||||
Combinator,
|
name_gen: &mut usize,
|
||||||
/// Can not be detached
|
term: &mut Term,
|
||||||
Unscoped { lams: BTreeSet<Name>, vars: BTreeSet<Name> },
|
builtin: bool,
|
||||||
/// Should be detached to make the program not hang
|
combinators: &mut BTreeMap<Name, Definition>,
|
||||||
Recursive,
|
) {
|
||||||
|
let comb_name = Name::new(format!("{}$C{}", def_name, *name_gen));
|
||||||
|
*name_gen += 1;
|
||||||
|
|
||||||
|
let comb_ref = Term::Ref { nam: comb_name.clone() };
|
||||||
|
let extracted_term = std::mem::replace(term, comb_ref);
|
||||||
|
|
||||||
|
let rules = vec![Rule { body: extracted_term, pats: Vec::new() }];
|
||||||
|
let rule = Definition { name: comb_name.clone(), rules, builtin };
|
||||||
|
combinators.insert(comb_name, rule);
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Detach {
|
impl Term {
|
||||||
fn can_detach(&self) -> bool {
|
/// A term can be considered safe if it is:
|
||||||
!matches!(self, Detach::Unscoped { .. })
|
/// - A Number or an Eraser.
|
||||||
}
|
/// - A Tuple or Superposition where all elements are safe.
|
||||||
|
/// - A safe Lambda, e.g. a nullary constructor or a lambda with safe body.
|
||||||
|
/// - A Reference with safe body.
|
||||||
|
pub fn is_safe(&self, book: &Book, seen: &mut IndexSet<Name>) -> bool {
|
||||||
|
Term::recursive_call(move || match self {
|
||||||
|
Term::Num { .. } | Term::Era => true,
|
||||||
|
|
||||||
fn unscoped_lam(nam: Name) -> Self {
|
Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(|e| Term::is_safe(e, book, seen)),
|
||||||
Detach::Unscoped { lams: [nam].into(), vars: Default::default() }
|
|
||||||
}
|
|
||||||
|
|
||||||
fn unscoped_var(nam: Name) -> Self {
|
Term::Lam { .. } => self.is_safe_lambda(book, seen),
|
||||||
Detach::Unscoped { lams: Default::default(), vars: [nam].into() }
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl BitAnd for Detach {
|
Term::Ref { nam } => {
|
||||||
type Output = Detach;
|
if seen.contains(nam) {
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
fn bitand(self, rhs: Self) -> Self::Output {
|
seen.insert(nam.clone());
|
||||||
match (self, rhs) {
|
if let Some(definition) = book.defs.get(nam) {
|
||||||
(Detach::Combinator, Detach::Combinator) => Detach::Combinator,
|
definition.rule().body.is_safe(book, seen)
|
||||||
|
|
||||||
(Detach::Combinator, unscoped @ Detach::Unscoped { .. }) => unscoped,
|
|
||||||
(unscoped @ Detach::Unscoped { .. }, Detach::Combinator) => unscoped,
|
|
||||||
|
|
||||||
// Merge two unscoped terms into one, removing entries of each matching `Lam` and `Var`.
|
|
||||||
// If all unscoped pairs are found and removed this way, the term can be treated as a Combinator.
|
|
||||||
(Detach::Unscoped { mut lams, mut vars }, Detach::Unscoped { lams: rhs_lams, vars: rhs_vars }) => {
|
|
||||||
lams.extend(rhs_lams);
|
|
||||||
vars.extend(rhs_vars);
|
|
||||||
|
|
||||||
let res_lams: BTreeSet<_> = lams.difference(&vars).cloned().collect();
|
|
||||||
let res_vars: BTreeSet<_> = vars.difference(&lams).cloned().collect();
|
|
||||||
|
|
||||||
if res_lams.is_empty() && res_vars.is_empty() {
|
|
||||||
Detach::Combinator
|
|
||||||
} else {
|
} else {
|
||||||
Detach::Unscoped { lams: res_lams, vars: res_vars }
|
false
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
(Detach::Combinator, Detach::Recursive) => Detach::Recursive,
|
_ => false,
|
||||||
(Detach::Recursive, Detach::Combinator) => Detach::Recursive,
|
})
|
||||||
(Detach::Recursive, Detach::Recursive) => Detach::Recursive,
|
}
|
||||||
|
|
||||||
// TODO: Is this the best way to best deal with a term that is both unscoped and recursive?
|
/// Checks if the term is a lambda sequence with the body being a variable in the scope or a reference.
|
||||||
(unscoped @ Detach::Unscoped { .. }, Detach::Recursive) => unscoped,
|
fn is_safe_lambda(&self, book: &Book, seen: &mut IndexSet<Name>) -> bool {
|
||||||
(Detach::Recursive, unscoped @ Detach::Unscoped { .. }) => unscoped,
|
let mut current = self;
|
||||||
|
let mut scope = Vec::new();
|
||||||
|
|
||||||
|
while let Term::Lam { nam, bod, .. } = current {
|
||||||
|
if let Some(nam) = nam {
|
||||||
|
scope.push(nam);
|
||||||
|
}
|
||||||
|
current = bod;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
match current {
|
||||||
|
Term::Var { nam } if scope.contains(&nam) => true,
|
||||||
|
Term::Ref { .. } => true,
|
||||||
|
term => term.is_safe(book, seen),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn has_unscoped_diff(&self) -> bool {
|
||||||
|
let (declared, used) = self.unscoped_vars();
|
||||||
|
|
||||||
|
declared.difference(&used).count() != 0 || used.difference(&declared).count() != 0
|
||||||
|
}
|
||||||
|
|
||||||
|
fn is_combinator(&self) -> bool {
|
||||||
|
self.free_vars().is_empty() && !self.has_unscoped_diff() && !matches!(self, Term::Ref { .. })
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Term {
|
impl Term {
|
||||||
pub fn float_combinators(&mut self, def_name: &Name, builtin: bool, combinators: &mut Combinators) {
|
pub fn float_children_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Term> {
|
||||||
self.go_float(0, &mut TermInfo::new(def_name.clone(), builtin, combinators));
|
multi_iterator!(FloatIter { Zero, Two, Vec, Mat, App });
|
||||||
}
|
|
||||||
|
|
||||||
fn go_float(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach {
|
|
||||||
Term::recursive_call(move || match self {
|
|
||||||
Term::Lam { .. } | Term::Chn { .. } if self.is_id() => Detach::Combinator,
|
|
||||||
|
|
||||||
Term::Lam { .. } => self.float_lam(depth, term_info),
|
|
||||||
Term::Chn { .. } => self.float_lam(depth, term_info),
|
|
||||||
Term::App { .. } => self.float_app(depth, term_info),
|
|
||||||
Term::Mat { .. } => self.float_mat(depth, term_info),
|
|
||||||
|
|
||||||
Term::Var { nam } => {
|
|
||||||
term_info.request_name(nam);
|
|
||||||
Detach::Combinator
|
|
||||||
}
|
|
||||||
|
|
||||||
Term::Lnk { nam } => Detach::unscoped_var(nam.clone()),
|
|
||||||
|
|
||||||
Term::Ref { nam: def_name } if def_name == &term_info.def_name => Detach::Recursive,
|
|
||||||
|
|
||||||
_ => {
|
|
||||||
let mut detach = Detach::Combinator;
|
|
||||||
for (child, binds) in self.children_mut_with_binds() {
|
|
||||||
detach = detach & child.go_float(depth + 1, term_info);
|
|
||||||
for bind in binds {
|
|
||||||
term_info.provide(bind.as_ref());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
detach
|
|
||||||
}
|
|
||||||
})
|
|
||||||
}
|
|
||||||
|
|
||||||
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, .. } => (nam.as_ref(), bod, true),
|
|
||||||
_ => unreachable!(),
|
|
||||||
};
|
|
||||||
|
|
||||||
let parent_scope = term_info.replace_scope(BTreeSet::new());
|
|
||||||
|
|
||||||
let mut detach = bod.go_float(depth + 1, term_info);
|
|
||||||
|
|
||||||
if unscoped {
|
|
||||||
detach = detach & Detach::unscoped_lam(nam.cloned().unwrap());
|
|
||||||
} else {
|
|
||||||
term_info.provide(nam);
|
|
||||||
}
|
|
||||||
|
|
||||||
if depth != 0 && detach.can_detach() && term_info.has_no_free_vars() {
|
|
||||||
term_info.detach_term(self);
|
|
||||||
}
|
|
||||||
|
|
||||||
term_info.merge_scope(parent_scope);
|
|
||||||
|
|
||||||
detach
|
|
||||||
}
|
|
||||||
|
|
||||||
fn float_app(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach {
|
|
||||||
let Term::App { fun, arg, .. } = self else { unreachable!() };
|
|
||||||
|
|
||||||
let parent_scope = term_info.replace_scope(BTreeSet::new());
|
|
||||||
|
|
||||||
let fun_detach = fun.go_float(depth + 1, term_info);
|
|
||||||
let fun_scope = term_info.replace_scope(BTreeSet::new());
|
|
||||||
|
|
||||||
let arg_detach = arg.go_float(depth + 1, term_info);
|
|
||||||
let arg_scope = term_info.replace_scope(parent_scope);
|
|
||||||
|
|
||||||
let detach = match fun_detach {
|
|
||||||
// If the fun scope is not empty, we know the recursive ref is not in a active position,
|
|
||||||
// Because if it was an application, it would be already extracted
|
|
||||||
//
|
|
||||||
// e.g.: {recursive_ref some_var}
|
|
||||||
Detach::Recursive if !fun_scope.is_empty() => arg_detach,
|
|
||||||
|
|
||||||
Detach::Recursive if arg_scope.is_empty() && arg_detach.can_detach() => {
|
|
||||||
term_info.detach_term(self);
|
|
||||||
Detach::Combinator
|
|
||||||
}
|
|
||||||
|
|
||||||
// If the only term that is possible to detach is just a Term::Ref,
|
|
||||||
// there is no benefit to it, so that case is skipped
|
|
||||||
Detach::Recursive if !matches!(fun, box Term::Ref { .. }) => {
|
|
||||||
term_info.detach_term(fun);
|
|
||||||
arg_detach
|
|
||||||
}
|
|
||||||
|
|
||||||
_ => fun_detach & arg_detach,
|
|
||||||
};
|
|
||||||
|
|
||||||
term_info.merge_scope(fun_scope);
|
|
||||||
term_info.merge_scope(arg_scope);
|
|
||||||
|
|
||||||
detach
|
|
||||||
}
|
|
||||||
|
|
||||||
fn float_mat(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach {
|
|
||||||
let Term::Mat { args, rules } = self else { unreachable!() };
|
|
||||||
|
|
||||||
let mut detach = Detach::Combinator;
|
|
||||||
for arg in args {
|
|
||||||
detach = detach & arg.go_float(depth + 1, term_info);
|
|
||||||
}
|
|
||||||
let parent_scope = term_info.replace_scope(BTreeSet::new());
|
|
||||||
|
|
||||||
for rule in rules.iter_mut() {
|
|
||||||
for pat in &rule.pats {
|
|
||||||
debug_assert!(pat.is_native_num_match());
|
|
||||||
}
|
|
||||||
|
|
||||||
let arm_detach = match rule.body.go_float(depth + 1, term_info) {
|
|
||||||
// If the recursive ref reached here, it is not in a active position
|
|
||||||
Detach::Recursive => Detach::Combinator,
|
|
||||||
detach => detach,
|
|
||||||
};
|
|
||||||
|
|
||||||
detach = detach & arm_detach;
|
|
||||||
}
|
|
||||||
|
|
||||||
term_info.merge_scope(parent_scope);
|
|
||||||
detach
|
|
||||||
}
|
|
||||||
|
|
||||||
// We don't want to detach id function, since that's not a net gain in performance or space
|
|
||||||
fn is_id(&self) -> bool {
|
|
||||||
match self {
|
match self {
|
||||||
Term::Lam { nam: Some(lam_nam), bod: box Term::Var { nam: var_nam }, .. } => lam_nam == var_nam,
|
Term::App { fun, arg, .. } => {
|
||||||
_ => false,
|
let mut args = vec![arg.as_mut()];
|
||||||
|
let mut app = fun.as_mut();
|
||||||
|
while let Term::App { fun, arg, .. } = app {
|
||||||
|
args.push(arg);
|
||||||
|
app = fun;
|
||||||
|
}
|
||||||
|
args.push(app);
|
||||||
|
FloatIter::App(args)
|
||||||
|
}
|
||||||
|
Term::Mat { args, rules } => {
|
||||||
|
FloatIter::Mat(args.iter_mut().chain(rules.iter_mut().map(|r| &mut r.body)))
|
||||||
|
}
|
||||||
|
Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => FloatIter::Vec(els),
|
||||||
|
Term::Let { val: fst, nxt: snd, .. }
|
||||||
|
| Term::Use { val: fst, nxt: snd, .. }
|
||||||
|
| Term::Dup { val: fst, nxt: snd, .. }
|
||||||
|
| Term::Opx { fst, snd, .. } => FloatIter::Two([fst.as_mut(), snd.as_mut()]),
|
||||||
|
Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.float_children_mut(),
|
||||||
|
Term::Var { .. }
|
||||||
|
| Term::Lnk { .. }
|
||||||
|
| Term::Num { .. }
|
||||||
|
| Term::Nat { .. }
|
||||||
|
| Term::Str { .. }
|
||||||
|
| Term::Ref { .. }
|
||||||
|
| Term::Era
|
||||||
|
| Term::Err => FloatIter::Zero([]),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -276,7 +276,8 @@ fn encode_pattern_match() {
|
|||||||
#[test]
|
#[test]
|
||||||
fn desugar_file() {
|
fn desugar_file() {
|
||||||
run_golden_test_dir(function_name!(), &|code, path| {
|
run_golden_test_dir(function_name!(), &|code, path| {
|
||||||
let diagnostics_cfg = DiagnosticsConfig::new(Severity::Error, true);
|
let mut diagnostics_cfg = DiagnosticsConfig::new(Severity::Error, true);
|
||||||
|
diagnostics_cfg.unused_definition = Severity::Allow;
|
||||||
let mut book = do_parse_book(code, path)?;
|
let mut book = do_parse_book(code, path)?;
|
||||||
desugar_book(&mut book, CompileOpts::light(), diagnostics_cfg, None)?;
|
desugar_book(&mut book, CompileOpts::light(), diagnostics_cfg, None)?;
|
||||||
Ok(book.to_string())
|
Ok(book.to_string())
|
||||||
|
25
tests/golden_tests/desugar_file/combinators.hvm
Normal file
25
tests/golden_tests/desugar_file/combinators.hvm
Normal file
@ -0,0 +1,25 @@
|
|||||||
|
(foo) = λa λb λc (foo a)
|
||||||
|
|
||||||
|
(bar) = λa λb (a bar b)
|
||||||
|
|
||||||
|
(List.ignore list ignore) =
|
||||||
|
match list {
|
||||||
|
(List.cons): (List.ignore list.tail (List.ignore))
|
||||||
|
(List.nil): 0
|
||||||
|
}
|
||||||
|
|
||||||
|
(baz) = {0 1 2 3 λa a foo}
|
||||||
|
|
||||||
|
(qux) = {0 qux}
|
||||||
|
|
||||||
|
(clax) = (λx x λa λb λc λd (clax d))
|
||||||
|
|
||||||
|
(tup) = (tup, 1, 0)
|
||||||
|
|
||||||
|
(list) = [0 list]
|
||||||
|
|
||||||
|
(A x) = (let {a b} = A; λc (a b c) x)
|
||||||
|
|
||||||
|
(B x) = (let (a, b) = B; λc (a b c) x)
|
||||||
|
|
||||||
|
(Main) = list
|
10
tests/golden_tests/desugar_file/deref_loop.hvm
Normal file
10
tests/golden_tests/desugar_file/deref_loop.hvm
Normal file
@ -0,0 +1,10 @@
|
|||||||
|
data nat = (succ pred) | zero
|
||||||
|
|
||||||
|
foo = @x match x {
|
||||||
|
succ: x.pred
|
||||||
|
zero: (bar 0)
|
||||||
|
}
|
||||||
|
|
||||||
|
bar = (foo 1)
|
||||||
|
|
||||||
|
main = (foo 0)
|
@ -30,10 +30,12 @@ In definition 'zero_var_succ':
|
|||||||
|
|
||||||
@succ_var = (?<#0 (a a) b> b)
|
@succ_var = (?<#0 (a a) b> b)
|
||||||
|
|
||||||
@succ_var_zero = (?<a @succ_var_zero$C0 b> b)
|
@succ_var_zero = (?<@succ_var_zero$C0 @succ_var_zero$C1 a> a)
|
||||||
|
|
||||||
|
@succ_var_zero$C0 = a
|
||||||
& #0 ~ <+ #1 a>
|
& #0 ~ <+ #1 a>
|
||||||
|
|
||||||
@succ_var_zero$C0 = (<+ #2 a> a)
|
@succ_var_zero$C1 = (<+ #2 a> a)
|
||||||
|
|
||||||
@succ_zero = (?<#0 (a a) b> b)
|
@succ_zero = (?<#0 (a a) b> b)
|
||||||
|
|
||||||
|
@ -14,9 +14,13 @@ input_file: tests/golden_tests/compile_file/redex_order.hvm
|
|||||||
& @c ~ (a d)
|
& @c ~ (a d)
|
||||||
|
|
||||||
@foo2 = a
|
@foo2 = a
|
||||||
& @a ~ (b a)
|
& @a ~ (@foo2$C1 a)
|
||||||
& @b ~ (c b)
|
|
||||||
& @c ~ (#0 c)
|
@foo2$C0 = a
|
||||||
|
& @c ~ (#0 a)
|
||||||
|
|
||||||
|
@foo2$C1 = a
|
||||||
|
& @b ~ (@foo2$C0 a)
|
||||||
|
|
||||||
@main = a
|
@main = a
|
||||||
& @foo ~ (@foo2 a)
|
& @foo ~ (@foo2 a)
|
||||||
|
@ -2,7 +2,7 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/compile_file/unscoped_supercombinator.hvm
|
input_file: tests/golden_tests/compile_file/unscoped_supercombinator.hvm
|
||||||
---
|
---
|
||||||
@Foo = ((@Foo$C0 (@Foo$C1 a)) a)
|
@Foo = ((@Foo$C1 (@Foo$C0 a)) a)
|
||||||
|
|
||||||
@Foo$C0 = (a ((a b) b))
|
@Foo$C0 = (a ((a b) b))
|
||||||
|
|
||||||
|
@ -4,13 +4,11 @@ input_file: tests/golden_tests/compile_file_o_all/adt_option_and.hvm
|
|||||||
---
|
---
|
||||||
@None = {2 * {2 a a}}
|
@None = {2 * {2 a a}}
|
||||||
|
|
||||||
@Option.and = ({2 @Option.and$C2 {2 @Option.and$C1_$_Option.and$C3 a}} a)
|
@Option.and = ({2 @Option.and$C1 {2 (* @None) a}} a)
|
||||||
|
|
||||||
@Option.and$C0 = {2 a (b {2 {2 [b a] c} {2 * c}})}
|
@Option.and$C0 = {2 a (b {2 {2 [b a] c} {2 * c}})}
|
||||||
|
|
||||||
@Option.and$C1_$_Option.and$C3 = (* @None)
|
@Option.and$C1 = {2 a ({2 @Option.and$C0 {2 (* @None) (a b)}} b)}
|
||||||
|
|
||||||
@Option.and$C2 = {2 a ({2 @Option.and$C0 {2 @Option.and$C1_$_Option.and$C3 (a b)}} b)}
|
|
||||||
|
|
||||||
@Some = (a {2 {2 a b} {2 * b}})
|
@Some = (a {2 {2 a b} {2 * b}})
|
||||||
|
|
||||||
|
@ -2,9 +2,7 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/compile_file_o_all/and.hvm
|
input_file: tests/golden_tests/compile_file_o_all/and.hvm
|
||||||
---
|
---
|
||||||
@and = (a ({2 (b b) {2 @and$C0 (a c)}} c))
|
@and = (a ({2 (b b) {2 (* @false) (a c)}} c))
|
||||||
|
|
||||||
@and$C0 = (* @false)
|
|
||||||
|
|
||||||
@false = {2 * {2 a a}}
|
@false = {2 * {2 a a}}
|
||||||
|
|
||||||
|
@ -2,5 +2,8 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/compile_file_o_all/black_box_ref.hvm
|
input_file: tests/golden_tests/compile_file_o_all/black_box_ref.hvm
|
||||||
---
|
---
|
||||||
|
@def_that_uses_black_box$C0 = a
|
||||||
|
& @HVM.black_box ~ (#6 a)
|
||||||
|
|
||||||
@main = a
|
@main = a
|
||||||
& @HVM.black_box ~ (#6 <* #7 a>)
|
& @def_that_uses_black_box$C0 ~ <* #7 a>
|
||||||
|
@ -2,9 +2,7 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/compile_file_o_all/ex2.hvm
|
input_file: tests/golden_tests/compile_file_o_all/ex2.hvm
|
||||||
---
|
---
|
||||||
@E = (* @E$C0)
|
@E = (* (* (a a)))
|
||||||
|
|
||||||
@E$C0 = (* (a a))
|
|
||||||
|
|
||||||
@I = (a (* ((a b) (* b))))
|
@I = (a (* ((a b) (* b))))
|
||||||
|
|
||||||
|
@ -8,19 +8,13 @@ input_file: tests/golden_tests/compile_file_o_all/expr.hvm
|
|||||||
|
|
||||||
@Let = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} {2 * {2 * {2 * d}}}}}}}}})))
|
@Let = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} {2 * {2 * {2 * d}}}}}}}}})))
|
||||||
|
|
||||||
@Mul = {4 * @Mul$C1}
|
@Mul = {4 * {4 * {4 a {4 * a}}}}
|
||||||
|
|
||||||
@Mul$C0 = {4 a {4 * a}}
|
|
||||||
|
|
||||||
@Mul$C1 = {4 * @Mul$C0}
|
|
||||||
|
|
||||||
@Num = (a {2 * {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
|
@Num = (a {2 * {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
|
||||||
|
|
||||||
@Op2 = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} d}}}}}}}}})))
|
@Op2 = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} d}}}}}}}}})))
|
||||||
|
|
||||||
@Sub = {4 * @Sub$C0}
|
@Sub = {4 * {4 a {4 * {4 * a}}}}
|
||||||
|
|
||||||
@Sub$C0 = {4 a {4 * {4 * a}}}
|
|
||||||
|
|
||||||
@Var = (a {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
|
@Var = (a {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
|
||||||
|
|
||||||
|
@ -4,43 +4,29 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
|
|||||||
---
|
---
|
||||||
@Cons = (a (b {4 {4 a {4 b c}} {4 * c}}))
|
@Cons = (a (b {4 {4 a {4 b c}} {4 * c}}))
|
||||||
|
|
||||||
@If$C0 = (a (* a))
|
@Map = ({4 @Map$C0 {4 (* @Nil) a}} a)
|
||||||
|
|
||||||
@If$C1 = (* (a a))
|
@Map$C0 = {4 a {4 {4 @Map$C0 {4 (* @Nil) (b c)}} ({3 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
|
||||||
|
|
||||||
@Map = ({4 @Map$C0 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 a}} a)
|
@Merge$C0 = {4 {5 a {5 b c}} {4 {7 d {4 @Merge$C0 {4 (* @Cons) (e (f (g h)))}}} ({9 (i (a {2 (j (* j)) {2 (* (k k)) ({4 {4 l {4 m n}} {4 * n}} ({4 {4 c {4 h o}} {4 * o}} p))}})) {9 q e}} ({11 i {11 l f}} ({13 {4 @Merge$C1 {4 (* (r r)) (q ({4 {4 b {4 d s}} {4 * s}} m))}} g} p)))}}
|
||||||
|
|
||||||
@Map$C0 = {4 a {4 {4 @Map$C0 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (b c)}} ({3 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
|
@Merge$C1 = {4 a {4 b (c ({4 @Merge$C0 {4 (* @Cons) (c (a (b d)))}} d))}}
|
||||||
|
|
||||||
@Map$C1_$_MergePair$C4_$_Unpack$C3 = (* @Nil)
|
@MergePair$C0 = (* (a {4 {4 a {4 @Nil b}} {4 * b}}))
|
||||||
|
|
||||||
@Merge$C0 = {4 {5 a {5 b c}} {4 {7 d {4 @Merge$C0 {4 @Merge$C1 (e (f (g h)))}}} ({9 (i (a {2 @If$C0 {2 @If$C1 ({4 {4 j {4 k l}} {4 * l}} ({4 {4 c {4 h m}} {4 * m}} n))}})) {9 o e}} ({11 i {11 j f}} ({13 {4 @Merge$C2 {4 @Merge$C3 (o ({4 {4 b {4 d p}} {4 * p}} k))}} g} n)))}}
|
@MergePair$C1 = {4 a {4 {4 @MergePair$C2 {4 (* @Nil) (b c)}} ({15 d b} ({4 @Merge$C1 {4 (* (e e)) (d (a f))}} {4 {4 f {4 c g}} {4 * g}}))}}
|
||||||
|
|
||||||
@Merge$C1 = (* @Cons)
|
@MergePair$C2 = {4 a {4 {4 @MergePair$C1 {4 @MergePair$C0 (b (a c))}} (b c)}}
|
||||||
|
|
||||||
@Merge$C2 = {4 a {4 b (c ({4 @Merge$C0 {4 @Merge$C1 (c (a (b d)))}} d))}}
|
|
||||||
|
|
||||||
@Merge$C3 = (* (a a))
|
|
||||||
|
|
||||||
@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (b c)}} ({15 d b} ({4 @Merge$C2 {4 @Merge$C3 (d (a e))}} {4 {4 e {4 c f}} {4 * f}}))}}
|
|
||||||
|
|
||||||
@MergePair$C1 = (a {4 {4 a {4 @Nil b}} {4 * b}})
|
|
||||||
|
|
||||||
@MergePair$C2 = (* @MergePair$C1)
|
|
||||||
|
|
||||||
@MergePair$C3 = {4 a {4 {4 @MergePair$C0 {4 @MergePair$C2 (b (a c))}} (b c)}}
|
|
||||||
|
|
||||||
@Nil = {4 * {4 a a}}
|
@Nil = {4 * {4 a a}}
|
||||||
|
|
||||||
@Pure = (a {4 {4 a {4 @Nil b}} {4 * b}})
|
@Pure = (a {4 {4 a {4 @Nil b}} {4 * b}})
|
||||||
|
|
||||||
@Unpack = (a ({4 @Unpack$C2 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (a b)}} b))
|
@Unpack = (a ({4 @Unpack$C1 {4 (* @Nil) (a b)}} b))
|
||||||
|
|
||||||
@Unpack$C0 = {4 a {4 {4 @MergePair$C3 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (b {4 @Unpack$C0 {4 @Unpack$C1 (c (d e))}})}} ({17 c {15 f b}} ({4 @Merge$C2 {4 @Merge$C3 (f (a d))}} e))}}
|
@Unpack$C0 = {4 a {4 {4 @MergePair$C2 {4 (* @Nil) (b {4 @Unpack$C0 {4 (* (c c)) (d (e f))}})}} ({17 d {15 g b}} ({4 @Merge$C1 {4 (* (h h)) (g (a e))}} f))}}
|
||||||
|
|
||||||
@Unpack$C1 = (* (a a))
|
@Unpack$C1 = {4 a {4 {4 @Unpack$C0 {4 (* (b b)) (c (a d))}} (c d)}}
|
||||||
|
|
||||||
@Unpack$C2 = {4 a {4 {4 @Unpack$C0 {4 @Unpack$C1 (b (a c))}} (b c)}}
|
|
||||||
|
|
||||||
@main = (a (b c))
|
@main = (a (b c))
|
||||||
& @Unpack ~ (a (d c))
|
& @Unpack ~ (a (d c))
|
||||||
|
@ -2,9 +2,9 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm
|
input_file: tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm
|
||||||
---
|
---
|
||||||
@Foo = ({2 (* #0) {2 @Foo$C1 a}} a)
|
@Foo = ({2 (* #0) {2 @Foo$C0 a}} a)
|
||||||
|
|
||||||
@Foo$C1 = (?<#0 (a a) b> b)
|
@Foo$C0 = (?<#0 (a a) b> b)
|
||||||
|
|
||||||
@main = a
|
@main = a
|
||||||
& @Foo ~ (@true (#3 a))
|
& @Foo ~ (@true (#3 a))
|
||||||
|
@ -2,9 +2,9 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm
|
input_file: tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm
|
||||||
---
|
---
|
||||||
@Foo = (?<{3 @Foo @Foo} @Foo$C0 a> a)
|
@Foo = (?<@Foo$C0 (a (* a)) b> b)
|
||||||
|
|
||||||
@Foo$C0 = (a (* a))
|
@Foo$C0 = {3 @Foo @Foo}
|
||||||
|
|
||||||
@main = a
|
@main = a
|
||||||
& @Foo ~ (#0 a)
|
& @Foo ~ (#0 a)
|
||||||
|
@ -28,9 +28,7 @@ For let expressions where the variable is non-linear (used more than once), you
|
|||||||
See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
|
See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
|
||||||
|
|
||||||
|
|
||||||
@long_name_that_truncates = (* @long_name_that_truncates$C0)
|
@long_name_that_truncates = (* (* @long_name_that_truncates))
|
||||||
|
|
||||||
@long_name_that_truncates$C0 = (* @long_name_that_truncates)
|
|
||||||
|
|
||||||
@main = a
|
@main = a
|
||||||
& @long_name_that_truncates ~ ((b b) a)
|
& @long_name_that_truncates ~ ((b b) a)
|
||||||
|
@ -4,13 +4,7 @@ input_file: tests/golden_tests/compile_file_o_all/scrutinee_reconstruction.hvm
|
|||||||
---
|
---
|
||||||
@None = {2 * {2 a a}}
|
@None = {2 * {2 a a}}
|
||||||
|
|
||||||
@Option.or = ({3 {2 @Option.or$C1 {2 @Option.or$C2 (a b)}} a} b)
|
@Option.or = ({3 {2 {2 * (a (* a))} {2 (* (b b)) (c d)}} c} d)
|
||||||
|
|
||||||
@Option.or$C0 = (a (* a))
|
|
||||||
|
|
||||||
@Option.or$C1 = {2 * @Option.or$C0}
|
|
||||||
|
|
||||||
@Option.or$C2 = (* (a a))
|
|
||||||
|
|
||||||
@Some = (a {2 {2 a b} {2 * b}})
|
@Some = (a {2 {2 a b} {2 * b}})
|
||||||
|
|
||||||
|
@ -2,17 +2,7 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/compile_file_o_all/weekday.hvm
|
input_file: tests/golden_tests/compile_file_o_all/weekday.hvm
|
||||||
---
|
---
|
||||||
@Saturday = {2 * @Saturday$C4}
|
@Saturday = {2 * {2 * {2 * {2 * {2 * {2 a {2 * a}}}}}}}
|
||||||
|
|
||||||
@Saturday$C0 = {2 a {2 * a}}
|
|
||||||
|
|
||||||
@Saturday$C1 = {2 * @Saturday$C0}
|
|
||||||
|
|
||||||
@Saturday$C2 = {2 * @Saturday$C1}
|
|
||||||
|
|
||||||
@Saturday$C3 = {2 * @Saturday$C2}
|
|
||||||
|
|
||||||
@Saturday$C4 = {2 * @Saturday$C3}
|
|
||||||
|
|
||||||
@main = a
|
@main = a
|
||||||
& (b b) ~ (@Saturday a)
|
& (b b) ~ (@Saturday a)
|
||||||
|
39
tests/snapshots/desugar_file__combinators.hvm.snap
Normal file
39
tests/snapshots/desugar_file__combinators.hvm.snap
Normal file
@ -0,0 +1,39 @@
|
|||||||
|
---
|
||||||
|
source: tests/golden_tests.rs
|
||||||
|
input_file: tests/golden_tests/desugar_file/combinators.hvm
|
||||||
|
---
|
||||||
|
(foo) = λa λ* λ* (foo a)
|
||||||
|
|
||||||
|
(bar) = λa λb (a bar b)
|
||||||
|
|
||||||
|
(List.ignore) = λa λ* #List (a List.ignore$C0 0)
|
||||||
|
|
||||||
|
(baz) = {0 1 2 3 λa a foo}
|
||||||
|
|
||||||
|
(qux) = {0 qux}
|
||||||
|
|
||||||
|
(clax) = (λa a clax$C0)
|
||||||
|
|
||||||
|
(tup) = (tup, 1, 0)
|
||||||
|
|
||||||
|
(list) = (List.cons 0 list$C0)
|
||||||
|
|
||||||
|
(A) = λa (A$C0 a)
|
||||||
|
|
||||||
|
(B) = λa (B$C0 a)
|
||||||
|
|
||||||
|
(Main) = list
|
||||||
|
|
||||||
|
(List.cons) = λa λb #List λc #List λ* #List (c a b)
|
||||||
|
|
||||||
|
(List.nil) = #List λ* #List λb b
|
||||||
|
|
||||||
|
(A$C0) = let {b c} = A; λd (b c d)
|
||||||
|
|
||||||
|
(B$C0) = let (c, d) = B; λe (c d e)
|
||||||
|
|
||||||
|
(List.ignore$C0) = #List λ* #List λd (List.ignore d List.ignore)
|
||||||
|
|
||||||
|
(clax$C0) = λ* λ* λ* λe (clax e)
|
||||||
|
|
||||||
|
(list$C0) = (List.cons list List.nil)
|
15
tests/snapshots/desugar_file__deref_loop.hvm.snap
Normal file
15
tests/snapshots/desugar_file__deref_loop.hvm.snap
Normal file
@ -0,0 +1,15 @@
|
|||||||
|
---
|
||||||
|
source: tests/golden_tests.rs
|
||||||
|
input_file: tests/golden_tests/desugar_file/deref_loop.hvm
|
||||||
|
---
|
||||||
|
(foo) = λa #nat (a #nat λb b foo$C0)
|
||||||
|
|
||||||
|
(bar) = (foo 1)
|
||||||
|
|
||||||
|
(main) = (foo 0)
|
||||||
|
|
||||||
|
(succ) = λa #nat λb #nat λ* #nat (b a)
|
||||||
|
|
||||||
|
(zero) = #nat λ* #nat λb b
|
||||||
|
|
||||||
|
(foo$C0) = (bar 0)
|
@ -2,14 +2,12 @@
|
|||||||
source: tests/golden_tests.rs
|
source: tests/golden_tests.rs
|
||||||
input_file: tests/golden_tests/mutual_recursion/len.hvm
|
input_file: tests/golden_tests/mutual_recursion/len.hvm
|
||||||
---
|
---
|
||||||
@Len = ({2 @Len$C1 {2 #0 a}} a)
|
@Len = ({2 @Len$C0 {2 #0 a}} a)
|
||||||
|
|
||||||
@Len$C0 = {2 a b}
|
@Len$C0 = {2 * {2 a b}}
|
||||||
& #1 ~ <+ c b>
|
& #1 ~ <+ c b>
|
||||||
& @Len ~ (a c)
|
& @Len ~ (a c)
|
||||||
|
|
||||||
@Len$C1 = {2 * @Len$C0}
|
|
||||||
|
|
||||||
@List.cons = (a (b {2 {2 a {2 b c}} {2 * c}}))
|
@List.cons = (a (b {2 {2 a {2 b c}} {2 * c}}))
|
||||||
|
|
||||||
@List.nil = {2 * {2 a a}}
|
@List.nil = {2 * {2 a a}}
|
||||||
|
Loading…
Reference in New Issue
Block a user