From ec24ae2a80ffe1bdfeb516898d2482e5d6594df8 Mon Sep 17 00:00:00 2001 From: imaqtkatt Date: Wed, 27 Mar 2024 16:41:30 -0300 Subject: [PATCH] Update float combinators doc and combinators test --- cspell.json | 2 + src/term/transform/float_combinators.rs | 55 ++++++++++--------- .../golden_tests/desugar_file/combinators.hvm | 4 ++ .../desugar_file__combinators.hvm.snap | 35 ++++++++++++ 4 files changed, 69 insertions(+), 27 deletions(-) create mode 100644 tests/snapshots/desugar_file__combinators.hvm.snap diff --git a/cspell.json b/cspell.json index 3ee82f47..42bdc6ae 100644 --- a/cspell.json +++ b/cspell.json @@ -45,6 +45,7 @@ "namegen", "nams", "nats", + "nullary", "numop", "nums", "oper", @@ -54,6 +55,7 @@ "peekable", "postcondition", "readback", + "recursively", "redex", "redexes", "resugar", diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs index bcd8f82c..33f17900 100644 --- a/src/term/transform/float_combinators.rs +++ b/src/term/transform/float_combinators.rs @@ -10,15 +10,13 @@ impl Book { /// /// Precondition: Variables must have been sanitized. /// - /// The term is floated if it: - /// - Is an Application without free variables. - /// - Is a Superposition. - /// - Is a combinator. - /// The term is not floated if it: - /// - Is safe or has unscoped variables. + /// The floating algorithm follows these rules: + /// - Don't extract safe terms or terms that contains unscoped variables. + /// - Extract if it is a closed Application + /// - Extract if it is a combinator + /// - Float every element of a Superposition pub fn float_combinators(&mut self) { let mut combinators = Combinators::new(); - let mut safe_defs = IndexSet::new(); let slf = self.clone(); for (def_name, def) in self.defs.iter_mut() { @@ -30,7 +28,8 @@ impl Book { let builtin = def.builtin; 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); @@ -45,17 +44,17 @@ impl Term { book: &Book, def_name: &Name, builtin: bool, - safe_defs: &mut IndexSet, + seen: &mut IndexSet, ) { Term::recursive_call(move || { for term in self.children_mut() { // 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; } // 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 { // 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. Term::Sup { els, .. } => els .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. term if term.is_combinator() => float_combinator(def_name, name_gen, term, builtin, combinators), @@ -102,34 +101,36 @@ fn float_combinator( impl Term { /// A term can be considered safe if it is: /// - A Number or an Eraser. - /// - A Tuple or Superposition where all elements are constants. - /// - A constant Lambda, e.g a nullary constructor. + /// - A Tuple or Superposition where all elements are safe. + /// - A constant Lambda, e.g. a nullary constructor. /// - A Reference with safe body. - pub fn is_safe(&self, book: &Book, safe_defs: &mut IndexSet) -> bool { + pub fn is_safe(&self, book: &Book, seen: &mut IndexSet) -> bool { Term::recursive_call(move || match self { 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 } => { - !safe_defs.insert(nam.clone()) - || if let Some(definition) = book.defs.get(nam) { - definition.rule().body.is_safe(book, safe_defs) - } else { - false - } + if seen.contains(nam) { + return false; + } + + seen.insert(nam.clone()); + if let Some(definition) = book.defs.get(nam) { + definition.rule().body.is_safe(book, seen) + } else { + false + } } - // TODO?: Any term that, when fully expanded, becomes a supercombinator is safe. - // _ => self.is_supercombinator(), _ => false, }) } /// 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) -> bool { + fn is_constant_lambda(&self, book: &Book, seen: &mut IndexSet) -> bool { let mut current = self; let mut scope = Vec::new(); @@ -143,7 +144,7 @@ impl Term { match current { Term::Var { nam } if scope.contains(&nam) => true, Term::Ref { .. } => true, - term => term.is_safe(book, safe_defs), + term => term.is_safe(book, seen), } } diff --git a/tests/golden_tests/desugar_file/combinators.hvm b/tests/golden_tests/desugar_file/combinators.hvm index 50f80b58..cf4e398a 100644 --- a/tests/golden_tests/desugar_file/combinators.hvm +++ b/tests/golden_tests/desugar_file/combinators.hvm @@ -12,6 +12,10 @@ (qux) = {0 qux} +(tup) = (tup, 1, 0) + (list) = [0 list] +(A x) = let {a b} = A; (a b x) + (Main) = list diff --git a/tests/snapshots/desugar_file__combinators.hvm.snap b/tests/snapshots/desugar_file__combinators.hvm.snap new file mode 100644 index 00000000..7a075339 --- /dev/null +++ b/tests/snapshots/desugar_file__combinators.hvm.snap @@ -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)