mirror of
https://github.com/HigherOrderCO/Bend.git
synced 2024-09-17 14:47:21 +03:00
Update float combinators doc and combinators test
This commit is contained in:
parent
bcbcdc5442
commit
ec24ae2a80
@ -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",
|
||||||
|
@ -10,15 +10,13 @@ impl Book {
|
|||||||
///
|
///
|
||||||
/// Precondition: Variables must have been sanitized.
|
/// Precondition: Variables must have been sanitized.
|
||||||
///
|
///
|
||||||
/// The term is floated if it:
|
/// The floating algorithm follows these rules:
|
||||||
/// - Is an Application without free variables.
|
/// - Don't extract safe terms or terms that contains unscoped variables.
|
||||||
/// - Is a Superposition.
|
/// - Extract if it is a closed Application
|
||||||
/// - Is a combinator.
|
/// - Extract if it is a combinator
|
||||||
/// The term is not floated if it:
|
/// - Float every element of a Superposition
|
||||||
/// - Is safe or has unscoped variables.
|
|
||||||
pub fn float_combinators(&mut self) {
|
pub fn float_combinators(&mut self) {
|
||||||
let mut combinators = Combinators::new();
|
let mut combinators = Combinators::new();
|
||||||
let mut safe_defs = IndexSet::new();
|
|
||||||
|
|
||||||
let slf = self.clone();
|
let slf = self.clone();
|
||||||
for (def_name, def) in self.defs.iter_mut() {
|
for (def_name, def) in self.defs.iter_mut() {
|
||||||
@ -30,7 +28,8 @@ impl Book {
|
|||||||
|
|
||||||
let builtin = def.builtin;
|
let builtin = def.builtin;
|
||||||
let rule = def.rule_mut();
|
let rule = def.rule_mut();
|
||||||
rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name, builtin, &mut safe_defs);
|
let mut seen = IndexSet::new();
|
||||||
|
rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name, builtin, &mut seen);
|
||||||
}
|
}
|
||||||
|
|
||||||
self.defs.extend(combinators);
|
self.defs.extend(combinators);
|
||||||
@ -45,17 +44,17 @@ impl Term {
|
|||||||
book: &Book,
|
book: &Book,
|
||||||
def_name: &Name,
|
def_name: &Name,
|
||||||
builtin: bool,
|
builtin: bool,
|
||||||
safe_defs: &mut IndexSet<Name>,
|
seen: &mut IndexSet<Name>,
|
||||||
) {
|
) {
|
||||||
Term::recursive_call(move || {
|
Term::recursive_call(move || {
|
||||||
for term in self.children_mut() {
|
for term in self.children_mut() {
|
||||||
// Don't float if it's safe or has unscoped variables.
|
// Don't float if it's safe or has unscoped variables.
|
||||||
if term.is_safe(book, safe_defs) || term.has_unscoped_diff() {
|
if term.is_safe(book, seen) || term.has_unscoped_diff() {
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Recusively float the children terms.
|
// Recusively float the children terms.
|
||||||
term.float_combinators(combinators, name_gen, book, def_name, builtin, safe_defs);
|
term.float_combinators(combinators, name_gen, book, def_name, builtin, seen);
|
||||||
|
|
||||||
match term {
|
match term {
|
||||||
// If it is an Application without free variables like '(bar 0)', float into a new definition.
|
// If it is an Application without free variables like '(bar 0)', float into a new definition.
|
||||||
@ -68,7 +67,7 @@ impl Term {
|
|||||||
// If it is a Superposition, float every child element.
|
// If it is a Superposition, float every child element.
|
||||||
Term::Sup { els, .. } => els
|
Term::Sup { els, .. } => els
|
||||||
.iter_mut()
|
.iter_mut()
|
||||||
.for_each(|e| e.float_combinators(combinators, name_gen, book, def_name, builtin, safe_defs)),
|
.for_each(|e| e.float_combinators(combinators, name_gen, book, def_name, builtin, seen)),
|
||||||
|
|
||||||
// If it is a combinator, float into a new definition.
|
// If it is a combinator, float into a new definition.
|
||||||
term if term.is_combinator() => float_combinator(def_name, name_gen, term, builtin, combinators),
|
term if term.is_combinator() => float_combinator(def_name, name_gen, term, builtin, combinators),
|
||||||
@ -102,34 +101,36 @@ fn float_combinator(
|
|||||||
impl Term {
|
impl Term {
|
||||||
/// A term can be considered safe if it is:
|
/// A term can be considered safe if it is:
|
||||||
/// - A Number or an Eraser.
|
/// - A Number or an Eraser.
|
||||||
/// - A Tuple or Superposition where all elements are constants.
|
/// - A Tuple or Superposition where all elements are safe.
|
||||||
/// - A constant Lambda, e.g a nullary constructor.
|
/// - A constant Lambda, e.g. a nullary constructor.
|
||||||
/// - A Reference with safe body.
|
/// - A Reference with safe body.
|
||||||
pub fn is_safe(&self, book: &Book, safe_defs: &mut IndexSet<Name>) -> bool {
|
pub fn is_safe(&self, book: &Book, seen: &mut IndexSet<Name>) -> bool {
|
||||||
Term::recursive_call(move || match self {
|
Term::recursive_call(move || match self {
|
||||||
Term::Num { .. } | Term::Era => true,
|
Term::Num { .. } | Term::Era => true,
|
||||||
|
|
||||||
Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(|e| Term::is_safe(e, book, safe_defs)),
|
Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(|e| Term::is_safe(e, book, seen)),
|
||||||
|
|
||||||
Term::Lam { .. } => self.is_constant_lambda(book, safe_defs),
|
Term::Lam { .. } => self.is_constant_lambda(book, seen),
|
||||||
|
|
||||||
Term::Ref { nam } => {
|
Term::Ref { nam } => {
|
||||||
!safe_defs.insert(nam.clone())
|
if seen.contains(nam) {
|
||||||
|| if let Some(definition) = book.defs.get(nam) {
|
return false;
|
||||||
definition.rule().body.is_safe(book, safe_defs)
|
}
|
||||||
|
|
||||||
|
seen.insert(nam.clone());
|
||||||
|
if let Some(definition) = book.defs.get(nam) {
|
||||||
|
definition.rule().body.is_safe(book, seen)
|
||||||
} else {
|
} else {
|
||||||
false
|
false
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// TODO?: Any term that, when fully expanded, becomes a supercombinator is safe.
|
|
||||||
// _ => self.is_supercombinator(),
|
|
||||||
_ => false,
|
_ => false,
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Checks if the term is a lambda sequence with the body being a variable in the scope or a reference.
|
/// Checks if the term is a lambda sequence with the body being a variable in the scope or a reference.
|
||||||
fn is_constant_lambda(&self, book: &Book, safe_defs: &mut IndexSet<Name>) -> bool {
|
fn is_constant_lambda(&self, book: &Book, seen: &mut IndexSet<Name>) -> bool {
|
||||||
let mut current = self;
|
let mut current = self;
|
||||||
let mut scope = Vec::new();
|
let mut scope = Vec::new();
|
||||||
|
|
||||||
@ -143,7 +144,7 @@ impl Term {
|
|||||||
match current {
|
match current {
|
||||||
Term::Var { nam } if scope.contains(&nam) => true,
|
Term::Var { nam } if scope.contains(&nam) => true,
|
||||||
Term::Ref { .. } => true,
|
Term::Ref { .. } => true,
|
||||||
term => term.is_safe(book, safe_defs),
|
term => term.is_safe(book, seen),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -12,6 +12,10 @@
|
|||||||
|
|
||||||
(qux) = {0 qux}
|
(qux) = {0 qux}
|
||||||
|
|
||||||
|
(tup) = (tup, 1, 0)
|
||||||
|
|
||||||
(list) = [0 list]
|
(list) = [0 list]
|
||||||
|
|
||||||
|
(A x) = let {a b} = A; (a b x)
|
||||||
|
|
||||||
(Main) = list
|
(Main) = list
|
||||||
|
35
tests/snapshots/desugar_file__combinators.hvm.snap
Normal file
35
tests/snapshots/desugar_file__combinators.hvm.snap
Normal file
@ -0,0 +1,35 @@
|
|||||||
|
---
|
||||||
|
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$C1 0)
|
||||||
|
|
||||||
|
(baz) = {0 1 2 3 λa a foo}
|
||||||
|
|
||||||
|
(qux) = {0 qux}
|
||||||
|
|
||||||
|
(tup) = (tup, 1, 0)
|
||||||
|
|
||||||
|
(list) = (list$C0 list$C2)
|
||||||
|
|
||||||
|
(A) = λa let {b c} = A; (b c a)
|
||||||
|
|
||||||
|
(Main) = list
|
||||||
|
|
||||||
|
(List.cons) = λa λb #List λc #List λ* #List (c a b)
|
||||||
|
|
||||||
|
(List.nil) = #List λ* #List λb b
|
||||||
|
|
||||||
|
(List.ignore$C0) = #List λd (List.ignore d List.ignore)
|
||||||
|
|
||||||
|
(List.ignore$C1) = #List λ* List.ignore$C0
|
||||||
|
|
||||||
|
(list$C0) = (List.cons 0)
|
||||||
|
|
||||||
|
(list$C1) = (List.cons list)
|
||||||
|
|
||||||
|
(list$C2) = (list$C1 List.nil)
|
Loading…
Reference in New Issue
Block a user