From 85c75f38abadf75d11ee1688e8c50363fe7cc49b Mon Sep 17 00:00:00 2001 From: imaqtkatt Date: Fri, 23 Feb 2024 11:55:23 -0300 Subject: [PATCH 01/10] WIP dont linearize used once variables in match arm --- src/term/transform/detach_supercombinators.rs | 3 +- src/term/transform/linearize_matches.rs | 33 +++++++++++++++---- 2 files changed, 28 insertions(+), 8 deletions(-) diff --git a/src/term/transform/detach_supercombinators.rs b/src/term/transform/detach_supercombinators.rs index 7427a30a3..499e9a37e 100644 --- a/src/term/transform/detach_supercombinators.rs +++ b/src/term/transform/detach_supercombinators.rs @@ -253,8 +253,9 @@ impl Term { }; // It is expected that match arms were already linearized + println!("{:?}", term_info.needed_names); + // FIXME debug_assert!(term_info.has_no_free_vars()); - detach = detach & arm_detach; } diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs index 031954dd2..e1cd1ac39 100644 --- a/src/term/transform/linearize_matches.rs +++ b/src/term/transform/linearize_matches.rs @@ -5,7 +5,7 @@ use crate::{ }; use indexmap::IndexSet; use itertools::Itertools; -use std::collections::BTreeSet; +use std::collections::{BTreeMap, BTreeSet}; impl Ctx<'_> { /// Linearizes the variables between match cases, transforming them into combinators when possible. @@ -78,12 +78,31 @@ pub fn linearize_match_free_vars(match_term: &mut Term) -> &mut Term { let Term::Mat { args: _, rules } = match_term else { unreachable!() }; // Collect the vars. // We need consistent iteration order. - let free_vars: BTreeSet = rules - .iter() - .flat_map(|r| { - r.body.free_vars().into_keys().filter(|k| !r.pats.iter().flat_map(|p| p.binds()).contains(k)) - }) - .collect(); + + let mut acc: BTreeMap = BTreeMap::new(); + rules.iter().for_each(|r| { + let fvs = r.body.free_vars().into_iter(); + for (k, v) in fvs { + if !r.pats.iter().flat_map(|p| p.binds()).contains(&k) { + match acc.entry(k) { + std::collections::btree_map::Entry::Occupied(mut o) => *o.get_mut() += v, + std::collections::btree_map::Entry::Vacant(vc) => { + vc.insert(v); + } + }; + } + } + }); + let free_vars: BTreeSet = acc.into_iter().filter(|(_, v)| *v >= 2).map(|(k, _)| k).collect(); + + // panic!("{acc:?}"); + + // let free_vars: BTreeSet = rules + // .iter() + // .flat_map(|r| { + // r.body.free_vars().into_keys().filter(|k| !r.pats.iter().flat_map(|p| p.binds()).contains(k)) + // }) + // .collect(); // Add lambdas to the arms for rule in rules { From 19181598da3915c2b59d75ec1e643bb3282a5126 Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Fri, 23 Feb 2024 16:13:41 -0300 Subject: [PATCH 02/10] Make supercombinators work with non-linear match arms --- src/term/transform/detach_supercombinators.rs | 74 ++++++++++++++----- ...ompile_file_o_all__adt_option_and.hvm.snap | 5 +- ...all__match_dup_and_reconstruction.hvm.snap | 3 +- ..._file_o_all__num_pattern_with_var.hvm.snap | 5 +- ...e_o_all__scrutinee_reconstruction.hvm.snap | 5 +- ...encode_pattern_match__adt_tup_era.hvm.snap | 6 +- .../encode_pattern_match__def_tups.hvm.snap | 6 +- ...de_pattern_match__flatten_era_pat.hvm.snap | 14 ++-- .../encode_pattern_match__match_bind.hvm.snap | 6 +- ...ode_pattern_match__nested_let_tup.hvm.snap | 6 +- .../encode_pattern_match__ntup_sum.hvm.snap | 6 +- .../run_file__adt_option_and.hvm.snap | 2 +- .../run_lazy__adt_option_and.hvm.snap | 2 +- ...mplify_matches__double_unwrap_box.hvm.snap | 2 +- .../simplify_matches__nested.hvm.snap | 2 +- ...plify_matches__redundant_with_era.hvm.snap | 2 +- 16 files changed, 82 insertions(+), 64 deletions(-) diff --git a/src/term/transform/detach_supercombinators.rs b/src/term/transform/detach_supercombinators.rs index 499e9a37e..db9c8943f 100644 --- a/src/term/transform/detach_supercombinators.rs +++ b/src/term/transform/detach_supercombinators.rs @@ -1,6 +1,6 @@ -use crate::term::{Book, Definition, Name, Pattern, Rule, Term}; +use crate::term::{Book, Definition, MatchNum, Name, Pattern, Rule, Term}; use std::{ - collections::{BTreeMap, HashSet}, + collections::{BTreeMap, BTreeSet}, ops::BitAnd, }; @@ -34,13 +34,13 @@ struct TermInfo<'d> { counter: u32, def_name: Name, builtin: bool, - needed_names: HashSet, + needed_names: BTreeSet, 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: HashSet::new(), combinators } + Self { counter: 0, def_name, builtin, needed_names: BTreeSet::new(), combinators } } fn request_name(&mut self, name: &Name) { self.needed_names.insert(name.clone()); @@ -56,11 +56,11 @@ impl<'d> TermInfo<'d> { self.needed_names.is_empty() } - fn replace_scope(&mut self, new_scope: HashSet) -> HashSet { + fn replace_scope(&mut self, new_scope: BTreeSet) -> BTreeSet { std::mem::replace(&mut self.needed_names, new_scope) } - fn merge_scope(&mut self, target: HashSet) { + fn merge_scope(&mut self, target: BTreeSet) { self.needed_names.extend(target); } @@ -82,7 +82,7 @@ enum Detach { /// Can be detached freely Combinator, /// Can not be detached - Unscoped { lams: HashSet, vars: HashSet }, + Unscoped { lams: BTreeSet, vars: BTreeSet }, /// Should be detached to make the program not hang Recursive, } @@ -117,8 +117,8 @@ impl BitAnd for Detach { lams.extend(rhs_lams); vars.extend(rhs_vars); - let res_lams: HashSet<_> = lams.difference(&vars).cloned().collect(); - let res_vars: HashSet<_> = vars.difference(&lams).cloned().collect(); + 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 @@ -141,7 +141,7 @@ impl BitAnd for Detach { impl Term { pub fn detach_combinators(&mut self, def_name: &Name, builtin: bool, combinators: &mut Combinators) { fn go_lam(term: &mut Term, depth: usize, term_info: &mut TermInfo) -> Detach { - let parent_scope = term_info.replace_scope(HashSet::new()); + let parent_scope = term_info.replace_scope(BTreeSet::new()); let (nam, bod, unscoped): (Option<&Name>, &mut Term, bool) = match term { Term::Lam { nam, bod, .. } => (nam.as_ref(), bod, false), @@ -174,10 +174,10 @@ impl Term { Term::Chn { .. } => go_lam(term, depth, term_info), Term::App { fun, arg, .. } => { - let parent_scope = term_info.replace_scope(HashSet::new()); + let parent_scope = term_info.replace_scope(BTreeSet::new()); let fun_detach = go(fun, depth + 1, term_info); - let fun_scope = term_info.replace_scope(HashSet::new()); + let fun_scope = term_info.replace_scope(BTreeSet::new()); let arg_detach = go(arg, depth + 1, term_info); let arg_scope = term_info.replace_scope(parent_scope); @@ -239,9 +239,9 @@ impl Term { for arg in args { detach = detach & go(arg, depth + 1, term_info); } - let parent_scope = term_info.replace_scope(HashSet::new()); + let parent_scope = term_info.replace_scope(BTreeSet::new()); - for rule in rules { + for rule in rules.iter_mut() { for pat in &rule.pats { debug_assert!(pat.is_detached_num_match()); } @@ -253,13 +253,51 @@ impl Term { }; // It is expected that match arms were already linearized - println!("{:?}", term_info.needed_names); - // FIXME - debug_assert!(term_info.has_no_free_vars()); detach = detach & arm_detach; } - term_info.replace_scope(parent_scope); + // This happens when a var is used in only one arm so it is not linearized + if !term_info.has_no_free_vars() { + for rule in rules { + let (arm_body, already_extracted) = match rule.pats[0] { + Pattern::Num(MatchNum::Zero) => (&mut rule.body, false), + _ => match &mut rule.body { + Term::Lam { bod, .. } => (bod.as_mut(), false), + Term::Ref { nam } => { + let extracted = term_info.combinators.get_mut(nam).unwrap(); + let Term::Lam { ref mut bod, .. } = &mut extracted.rules[0].body else { unreachable!() }; + (bod.as_mut(), true) + } + _ => unreachable!(), + }, + }; + + let term = std::mem::take(arm_body); + + let body_vars = term.free_vars(); + + let term = term_info.needed_names.iter().rev().fold(term, |acc, arg| { + if body_vars.contains_key(arg) { + Term::named_lam(arg.clone(), acc) + } else { + Term::lam(None, acc) + } + }); + + *arm_body = term; + if !already_extracted { + term_info.detach_term(&mut rule.body); + } + } + + let mat = std::mem::take(term); + *term = term_info + .needed_names + .iter() + .fold(mat, |acc, arg| Term::app(acc, Term::Var { nam: arg.clone() })); + } + + term_info.merge_scope(parent_scope); detach } Term::Sup { fst, snd, .. } | Term::Tup { fst, snd } | Term::Opx { fst, snd, .. } => { diff --git a/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap b/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap index 28d3ce80f..75b33bfa5 100644 --- a/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap +++ b/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap @@ -3,10 +3,7 @@ source: tests/golden_tests.rs 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$S3_$_Option.and$S1 = (* @None) +@Option.and = ({2 {4 a b} {2 @None c}} ({2 {4 d {2 {4 [a d] e} {2 * e}}} {2 @None b}} c)) @Some = (a {2 {4 a b} {2 * b}}) @main = a & @Option.and ~ (b (c a)) diff --git a/tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap b/tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap index 4e9e419e4..bc13a83c9 100644 --- a/tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap +++ b/tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap @@ -3,8 +3,7 @@ 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}) -@Got = ({3 {2 @Got$S0 (a b)} a} b) -@Got$S0 = {4 a (b [b a])} +@Got = ({3 {2 {4 a [b a]} c} b} c) @main = a & @Got ~ (b a) & @Boxed ~ (#10 b) diff --git a/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap b/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap index 370013f57..b221cbd77 100644 --- a/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap +++ b/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap @@ -2,9 +2,8 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm --- -@Foo = ({2 (* #0) {2 @Foo$S3 a}} a) -@Foo$S2 = (a (* a)) -@Foo$S3 = (?<((* #0) @Foo$S2) (* a)> a) +@Foo = ({2 (* #0) {2 @Foo$S1 a}} a) +@Foo$S1 = (?<(#0 (a a)) b> b) @main = a & @Foo ~ (@true (#3 a)) @true = {2 * {2 a a}} diff --git a/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap b/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap index 5b22067ad..1b796d8e5 100644 --- a/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap +++ b/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap @@ -3,10 +3,7 @@ source: tests/golden_tests.rs 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$S2 = (* (a a)) +@Option.or = ({3 {2 {4 * a} {2 b c}} a} (b c)) @Some = (a {2 {4 a b} {2 * b}}) @main = a & @Option.or ~ (b (@None a)) diff --git a/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap b/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap index 721f284cf..7dba7642f 100644 --- a/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap +++ b/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap @@ -3,17 +3,15 @@ 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.Pair.a λb #Tuple.Pair.b λ* #Tuple (b #Tuple.Pair.a λd #Tuple.Pair.b λ* d)) (Main) = (Foo (Pair 1 5)) (Pair) = λa λb #Tuple λc #Tuple.Pair.b (#Tuple.Pair.a (c a) b) Scott: -(Foo) = λa (a λb λc (b λd λ* λ* d c)) +(Foo) = λa (a λb λ* (b λd λ* d)) (Main) = (Foo (Pair 1 5)) (Pair) = λa λb λc (c a b) - - diff --git a/tests/snapshots/encode_pattern_match__def_tups.hvm.snap b/tests/snapshots/encode_pattern_match__def_tups.hvm.snap index 71378a77f..c9f5fdb05 100644 --- a/tests/snapshots/encode_pattern_match__def_tups.hvm.snap +++ b/tests/snapshots/encode_pattern_match__def_tups.hvm.snap @@ -3,13 +3,11 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/def_tups.hvm --- TaggedScott: -(go) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, h) = e; λi λj (let (k, l) = h; λm λn λo (+ (+ (+ (+ l k) o) n) m) i j g) f d) b) +(go) = λa let (b, c) = a; let (d, e) = c; let (f, g) = e; let (h, i) = g; (+ (+ (+ (+ i h) f) d) b) (main) = (go (1, (2, (3, (4, 5))))) Scott: -(go) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, h) = e; λi λj (let (k, l) = h; λm λn λo (+ (+ (+ (+ l k) o) n) m) i j g) f d) b) +(go) = λa let (b, c) = a; let (d, e) = c; let (f, g) = e; let (h, i) = g; (+ (+ (+ (+ i h) f) d) b) (main) = (go (1, (2, (3, (4, 5))))) - - diff --git a/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap b/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap index 4cb8d3345..5a962b6d0 100644 --- a/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap +++ b/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap @@ -3,21 +3,19 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm --- TaggedScott: -(Fn1) = λa λb (let (c, d) = a; λe (let (f, *) = d; λ* λ* f c e) b) +(Fn1) = λa λ* let (*, d) = a; let (e, *) = d; e -(Fn2) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, *) = e; λ* λ* g f d) b) +(Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f -(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; +: λi λ* λ* i } d e) b) +(Fn3) = λa λb let (c, d) = a; (match c { 0: λ* λ* 0; +: λh λ* λ* h } d b) (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0) Scott: -(Fn1) = λa λb (let (c, d) = a; λe (let (f, *) = d; λ* λ* f c e) b) +(Fn1) = λa λ* let (*, d) = a; let (e, *) = d; e -(Fn2) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, *) = e; λ* λ* g f d) b) +(Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f -(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; +: λi λ* λ* i } d e) b) +(Fn3) = λa λb let (c, d) = a; (match c { 0: λ* λ* 0; +: λh λ* λ* h } d b) (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0) - - diff --git a/tests/snapshots/encode_pattern_match__match_bind.hvm.snap b/tests/snapshots/encode_pattern_match__match_bind.hvm.snap index 172e70721..57b840eb6 100644 --- a/tests/snapshots/encode_pattern_match__match_bind.hvm.snap +++ b/tests/snapshots/encode_pattern_match__match_bind.hvm.snap @@ -3,13 +3,11 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/match_bind.hvm --- TaggedScott: -(cheese) = let {a a_2} = (+ 2 3); (match a { 0: λ* 653323; +: λd λe (+ e d) } a_2) +(cheese) = let {a a_2} = (+ 2 3); match a { 0: 653323; +: λc (+ a_2 c) } (main) = cheese Scott: -(cheese) = let {a a_2} = (+ 2 3); (match a { 0: λ* 653323; +: λd λe (+ e d) } a_2) +(cheese) = let {a a_2} = (+ 2 3); match a { 0: 653323; +: λc (+ a_2 c) } (main) = cheese - - diff --git a/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap b/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap index 872145b78..04e6a0ef9 100644 --- a/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap +++ b/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap @@ -3,9 +3,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/nested_let_tup.hvm --- TaggedScott: -(main) = let (k, l) = let (b, c) = (10, ((1, ((2, 3), 4)), 3)); (let (d, *) = c; λ* d b); (let (m, *) = l; λ* let (s, *) = m; s k) +(main) = let (*, k) = let (*, c) = (10, ((1, ((2, 3), 4)), 3)); let (d, *) = c; d; let (l, *) = k; let (q, *) = l; q Scott: -(main) = let (k, l) = let (b, c) = (10, ((1, ((2, 3), 4)), 3)); (let (d, *) = c; λ* d b); (let (m, *) = l; λ* let (s, *) = m; s k) - - +(main) = let (*, k) = let (*, c) = (10, ((1, ((2, 3), 4)), 3)); let (d, *) = c; d; let (l, *) = k; let (q, *) = l; q diff --git a/tests/snapshots/encode_pattern_match__ntup_sum.hvm.snap b/tests/snapshots/encode_pattern_match__ntup_sum.hvm.snap index cdb517685..43d6bcd2e 100644 --- a/tests/snapshots/encode_pattern_match__ntup_sum.hvm.snap +++ b/tests/snapshots/encode_pattern_match__ntup_sum.hvm.snap @@ -3,13 +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) = a; let (d, e) = b; let (f, g) = c; let (h, i) = g; (+ d (+ e (+ f (+ h i)))) (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) = a; let (d, e) = b; let (f, g) = c; let (h, i) = g; (+ d (+ e (+ f (+ h i)))) (main) = (ntupSum ((1, 3), (3, (2, 1)))) - - diff --git a/tests/snapshots/run_file__adt_option_and.hvm.snap b/tests/snapshots/run_file__adt_option_and.hvm.snap index 87118776f..493ce8486 100644 --- a/tests/snapshots/run_file__adt_option_and.hvm.snap +++ b/tests/snapshots/run_file__adt_option_and.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/adt_option_and.hvm --- -λa match a { (Some b): λc (match c { (Some d): λe (Some (e, d)); (None): λ* None } b); (None): λ* None } +λa λb match a { (Some c): match b { (Some d): (Some (c, d)); (None): None }; (None): None } diff --git a/tests/snapshots/run_lazy__adt_option_and.hvm.snap b/tests/snapshots/run_lazy__adt_option_and.hvm.snap index fafab6193..e86516c81 100644 --- a/tests/snapshots/run_lazy__adt_option_and.hvm.snap +++ b/tests/snapshots/run_lazy__adt_option_and.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_lazy/adt_option_and.hvm --- -λa match a { (Some b): λc (match c { (Some d): λe (Some (e, d)); (None): λ* None } b); (None): λ* None } +λa λb match a { (Some c): match b { (Some d): (Some (c, d)); (None): None }; (None): None } diff --git a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap index 4257a7684..e7efc5c7d 100644 --- a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap +++ b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap @@ -2,7 +2,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/double_unwrap_box.hvm --- -(DoubleUnbox) = λa λb (match a { (Box c): λd (match c { (Box e): λ* e } d) } b) +(DoubleUnbox) = λa λ* match a { (Box c): match c { (Box d): d } } (Main) = (DoubleUnbox (Box (Box 0)) 5) diff --git a/tests/snapshots/simplify_matches__nested.hvm.snap b/tests/snapshots/simplify_matches__nested.hvm.snap index d1b900557..009bfb848 100644 --- a/tests/snapshots/simplify_matches__nested.hvm.snap +++ b/tests/snapshots/simplify_matches__nested.hvm.snap @@ -2,7 +2,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/nested.hvm --- -(Rule) = λa match a { (CtrA b c): (match c { (CtrB1 d): λe (e d); (CtrB2 h i): λj (match h { (CtrC): λk λl (k l) } j i) } b); (CtrB p): p } +(Rule) = λa match a { (CtrA b c): (match c { (CtrB1 d): λe (e d); (CtrB2 h i): λj match h { (CtrC): (j i) } } b); (CtrB n): n } (CtrC) = #Baz λa a diff --git a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap index a0f05ce94..8946642cd 100644 --- a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap +++ b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap @@ -2,6 +2,6 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/redundant_with_era.hvm --- -(Fn2) = λa λb (match a { 0: λc (match c { (e, f): λg (match f { (*, i): λ* λ* i } g e) } *); +m: λn (match n { (o, p): λq (match p { (*, s): λ* λ* s } q o) } m) } b) +(Fn2) = λa λb (match a { 0: λc match c { (*, f): match f { (*, h): h } }; +*: λk match k { (*, m): match m { (*, o): o } } } b) (main) = * From e903af152f48616e1f7ba5fc16bff86a2ae12058 Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Mon, 26 Feb 2024 13:42:29 -0300 Subject: [PATCH 03/10] Refactor lift_combinaotors to work with linearize_matches change --- docs/compiler-options.md | 4 +- src/lib.rs | 43 ++- src/main.rs | 38 +- src/term/transform/detach_supercombinators.rs | 325 ----------------- src/term/transform/lift_combinators.rs | 338 ++++++++++++++++++ src/term/transform/linearize_matches.rs | 31 +- src/term/transform/mod.rs | 2 +- tests/golden_tests.rs | 4 +- 8 files changed, 409 insertions(+), 376 deletions(-) delete mode 100644 src/term/transform/detach_supercombinators.rs create mode 100644 src/term/transform/lift_combinators.rs diff --git a/docs/compiler-options.md b/docs/compiler-options.md index 4faa016d7..d637f4a7e 100644 --- a/docs/compiler-options.md +++ b/docs/compiler-options.md @@ -8,7 +8,7 @@ | `-Oref-to-ref` `-Ono-ref-to-ref` | Disabled | [ref-to-ref](#ref-to-ref) | | `-Oprune` `-Ono-prune` | Disabled | [definition-pruning](#definition-pruning) | | `-Opre-reduce` `-Ono-pre-reduce` | Disabled | [pre-reduce](#pre-reduce) | -| `-Osupercombinators` `-Ono-supercombinators` | Enabled | [supercombinators](#supercombinators) | +| `-Olift_combinators` `-Ono-lift_combinators` | Enabled | [lift-combinators](#lift-combinators) | | `-Osimplify-main` `-Ono-simplify-main` | Disabled | [simplify-main](#simplify-main) | | `-Omerge` `-Ono-merge` | Disabled | [definition-merging](#definition-merging) | | `-Oinline` `-Ono-inline` | Disabled | [inline](#inline) | @@ -134,7 +134,7 @@ main = (bar) @main = @bar ``` -## Supercombinators +## Lift-Combinators Extracts closed terms to new definitions. See [lazy definitions](lazy-definitions#automatic-optimization). Since HVM-Core is an eager runtime, this pass is enabled by default to prevent infinite expansions. diff --git a/src/lib.rs b/src/lib.rs index cb03fa796..d127a645b 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -134,12 +134,16 @@ pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result, ctx.book.desugar_implicit_match_binds(); ctx.check_ctrs_arities()?; - // Must be between [`Book::desugar_implicit_match_binds`] and [`Ctx::linearize_simple_matches`] + // Must be between [`Book::desugar_implicit_match_binds`] and [`Ctx::linearize_matches`] ctx.check_unbound_vars()?; ctx.book.convert_match_def_to_term(); ctx.simplify_matches()?; - ctx.linearize_simple_matches()?; + + if !matches!(opts.linearize_matches, OptLevel::Disabled) { + ctx.linearize_matches()?; + } + ctx.book.encode_simple_matches(opts.adt_encoding); // sanity check @@ -155,8 +159,8 @@ pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result, if opts.eta { ctx.book.eta_reduction(); } - if opts.supercombinators { - ctx.book.detach_supercombinators(); + if opts.lift_combinators { + ctx.book.lift_combinators(matches!(opts.linearize_matches, OptLevel::Extra)); } if opts.ref_to_ref { ctx.simplify_ref_to_ref()?; @@ -331,6 +335,14 @@ impl RunOpts { } } +#[derive(Clone, Copy, Debug, Default)] +pub enum OptLevel { + #[default] + Disabled, + Enabled, + Extra, +} + #[derive(Clone, Copy, Debug, Default)] pub struct CompileOpts { /// Selects the encoding for the ADT syntax. @@ -348,8 +360,11 @@ pub struct CompileOpts { /// Enables [hvmc_net::pre_reduce]. pub pre_reduce: bool, - /// Enables [term::transform::detach_supercombinators]. - pub supercombinators: bool, + /// Enables [term::transform::linearize_matches]. + pub linearize_matches: OptLevel, + + /// Enables [term::transform::lift_combinators]. + pub lift_combinators: bool, /// Enables [term::transform::simplify_main_ref]. pub simplify_main: bool, @@ -369,11 +384,12 @@ impl CompileOpts { ref_to_ref: true, prune: true, pre_reduce: true, - supercombinators: true, + lift_combinators: true, simplify_main: true, merge: true, inline: true, adt_encoding: Default::default(), + linearize_matches: OptLevel::Extra, } } @@ -387,23 +403,26 @@ impl CompileOpts { Self { adt_encoding: self.adt_encoding, ..Self::default() } } - /// All optimizations disabled, except detach supercombinators. + /// All optimizations disabled, except lift_combinators and linearize_matches pub fn light() -> Self { - Self { supercombinators: true, ..Self::default() } + Self { lift_combinators: true, linearize_matches: OptLevel::Extra, ..Self::default() } } // Disable optimizations that don't work or are unnecessary on lazy mode pub fn lazy_mode(&mut self) { - self.supercombinators = false; + self.lift_combinators = false; + if let OptLevel::Extra = self.linearize_matches { + self.linearize_matches = OptLevel::Enabled; + } self.pre_reduce = false; } } impl CompileOpts { pub fn check(&self, lazy_mode: bool) { - if !self.supercombinators && !lazy_mode { + if !self.lift_combinators && !lazy_mode { println!( - "Warning: Running in strict mode without enabling the supercombinators pass can lead to some functions expanding infinitely." + "Warning: Running in strict mode without enabling the lift_combinators pass can lead to some functions expanding infinitely." ); } } diff --git a/src/main.rs b/src/main.rs index 58a59b670..a08d3158b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -4,7 +4,7 @@ use hvml::{ diagnostics::Info, load_file_to_book, run_book, term::{display::display_readback_errors, AdtEncoding, Book, Name}, - CompileOpts, RunInfo, RunOpts, WarnState, WarningOpts, + CompileOpts, OptLevel, RunInfo, RunOpts, WarnState, WarningOpts, }; use std::{ path::{Path, PathBuf}, @@ -38,7 +38,7 @@ enum Mode { value_delimiter = ' ', action = clap::ArgAction::Append, long_help = r#"Enables or disables the given optimizations - supercombinators is enabled by default."#, + lift_combinators is enabled by default on strict mode."#, )] comp_opts: Vec, @@ -82,7 +82,7 @@ enum Mode { value_delimiter = ' ', action = clap::ArgAction::Append, long_help = r#"Enables or disables the given optimizations - supercombinators is enabled by default."#, + lift_combinators is enabled by default on strict mode."#, )] comp_opts: Vec, @@ -91,12 +91,15 @@ enum Mode { }, /// Runs the lambda-term level desugaring passes. Desugar { + #[arg(short = 'L', help = "Lazy mode")] + lazy_mode: bool, + #[arg( short = 'O', value_delimiter = ' ', action = clap::ArgAction::Append, long_help = r#"Enables or disables the given optimizations - supercombinators is enabled by default."#, + lift_combinators is enabled by default on strict mode."#, )] comp_opts: Vec, @@ -185,15 +188,18 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Info> { let mut opts = OptArgs::opts_from_cli(&comp_opts); if lazy_mode { - opts.lazy_mode() + opts.lazy_mode(); } let mut book = load_book(&path)?; let compiled = compile_book(&mut book, opts)?; println!("{}", compiled.display_with_warns(warning_opts)?); } - Mode::Desugar { path, comp_opts } => { - let opts = OptArgs::opts_from_cli(&comp_opts); + Mode::Desugar { path, comp_opts, lazy_mode } => { + let mut opts = OptArgs::opts_from_cli(&comp_opts); + if lazy_mode { + opts.lazy_mode(); + } let mut book = load_book(&path)?; // TODO: Shouldn't the desugar have `warn_opts` too? maybe WarningOpts::allow_all() by default let _warns = desugar_book(&mut book, opts)?; @@ -221,7 +227,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Info> { if lazy_mode { single_core = true; - opts.lazy_mode() + opts.lazy_mode(); } let book = load_book(&path)?; @@ -288,8 +294,11 @@ pub enum OptArgs { NoRefToRef, PreReduce, NoPreReduce, - Supercombinators, - NoSupercombinators, + LinearizeMatches, + LinearizeMatchesExtra, + NoLinearizeMatches, + LiftCombinators, + NoLiftCombinators, SimplifyMain, NoSimplifyMain, Merge, @@ -316,16 +325,21 @@ impl OptArgs { NoRefToRef => opts.ref_to_ref = false, PreReduce => opts.pre_reduce = true, NoPreReduce => opts.pre_reduce = false, - Supercombinators => opts.supercombinators = true, - NoSupercombinators => opts.supercombinators = false, + LiftCombinators => opts.lift_combinators = true, + NoLiftCombinators => opts.lift_combinators = false, SimplifyMain => opts.simplify_main = true, NoSimplifyMain => opts.simplify_main = false, Merge => opts.merge = true, NoMerge => opts.merge = false, Inline => opts.inline = true, NoInline => opts.inline = false, + AdtScott => opts.adt_encoding = AdtEncoding::Scott, AdtTaggedScott => opts.adt_encoding = AdtEncoding::TaggedScott, + + LinearizeMatches => opts.linearize_matches = OptLevel::Enabled, + LinearizeMatchesExtra => opts.linearize_matches = OptLevel::Extra, + NoLinearizeMatches => opts.linearize_matches = OptLevel::Disabled, } } opts diff --git a/src/term/transform/detach_supercombinators.rs b/src/term/transform/detach_supercombinators.rs deleted file mode 100644 index db9c8943f..000000000 --- a/src/term/transform/detach_supercombinators.rs +++ /dev/null @@ -1,325 +0,0 @@ -use crate::term::{Book, Definition, MatchNum, Name, Pattern, Rule, Term}; -use std::{ - collections::{BTreeMap, BTreeSet}, - ops::BitAnd, -}; - -/// Replaces closed Terms (i.e. without free variables) with a Ref to the extracted term -/// Precondition: Vars must have been sanitized -impl Book { - pub fn detach_supercombinators(&mut self) { - let mut combinators = Combinators::new(); - - for (def_name, def) in self.defs.iter_mut() { - if self.entrypoint.as_ref().is_some_and(|m| m == def_name) { - continue; - } - - let builtin = def.builtin; - let rule = def.rule_mut(); - rule.body.detach_combinators(def_name, builtin, &mut combinators); - } - - // 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); - } -} - -type Combinators = BTreeMap; - -#[derive(Debug)] -struct TermInfo<'d> { - // Number of times a Term has been detached from the current Term - counter: u32, - def_name: Name, - builtin: bool, - needed_names: BTreeSet, - 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) -> BTreeSet { - std::mem::replace(&mut self.needed_names, new_scope) - } - - fn merge_scope(&mut self, target: BTreeSet) { - self.needed_names.extend(target); - } - - fn detach_term(&mut self, term: &mut Term) { - let comb_name = Name::new(format!("{}$S{}", 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)] -enum Detach { - /// Can be detached freely - Combinator, - /// Can not be detached - Unscoped { lams: BTreeSet, vars: BTreeSet }, - /// Should be detached to make the program not hang - Recursive, -} - -impl Detach { - fn can_detach(&self) -> bool { - !matches!(self, Detach::Unscoped { .. }) - } - - fn unscoped_lam(nam: Name) -> Self { - Detach::Unscoped { lams: [nam].into(), vars: Default::default() } - } - - fn unscoped_var(nam: Name) -> Self { - Detach::Unscoped { lams: Default::default(), vars: [nam].into() } - } -} - -impl BitAnd for Detach { - type Output = Detach; - - fn bitand(self, rhs: Self) -> Self::Output { - match (self, rhs) { - (Detach::Combinator, Detach::Combinator) => Detach::Combinator, - - (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 { - Detach::Unscoped { lams: res_lams, vars: res_vars } - } - } - - (Detach::Combinator, Detach::Recursive) => Detach::Recursive, - (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? - (unscoped @ Detach::Unscoped { .. }, Detach::Recursive) => unscoped, - (Detach::Recursive, unscoped @ Detach::Unscoped { .. }) => unscoped, - } - } -} - -impl Term { - pub fn detach_combinators(&mut self, def_name: &Name, builtin: bool, combinators: &mut Combinators) { - fn go_lam(term: &mut Term, depth: usize, term_info: &mut TermInfo) -> Detach { - let parent_scope = term_info.replace_scope(BTreeSet::new()); - - let (nam, bod, unscoped): (Option<&Name>, &mut Term, bool) = match term { - Term::Lam { nam, bod, .. } => (nam.as_ref(), bod, false), - Term::Chn { nam, bod, .. } => (Some(nam), bod, true), - _ => unreachable!(), - }; - - let mut detach = go(bod, depth + 1, term_info); - - if unscoped { - detach = detach & Detach::unscoped_lam(nam.cloned().unwrap()); - } - - if !unscoped { - term_info.provide(nam); - } - - if detach.can_detach() && !term.is_id() && depth != 0 && term_info.has_no_free_vars() { - term_info.detach_term(term); - } - - term_info.merge_scope(parent_scope); - - detach - } - - fn go(term: &mut Term, depth: usize, term_info: &mut TermInfo) -> Detach { - match term { - Term::Lam { .. } => go_lam(term, depth, term_info), - Term::Chn { .. } => go_lam(term, depth, term_info), - - Term::App { fun, arg, .. } => { - let parent_scope = term_info.replace_scope(BTreeSet::new()); - - let fun_detach = go(fun, depth + 1, term_info); - let fun_scope = term_info.replace_scope(BTreeSet::new()); - - let arg_detach = go(arg, 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(term); - 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 - } - - Term::Var { nam } => { - term_info.request_name(nam); - Detach::Combinator - } - - Term::Lnk { nam } => Detach::unscoped_var(nam.clone()), - - Term::Let { pat: Pattern::Var(nam), val, nxt } => { - let val_detach = go(val, depth + 1, term_info); - let nxt_detach = go(nxt, depth + 1, term_info); - term_info.provide(nam.as_ref()); - - val_detach & nxt_detach - } - Term::Dup { fst, snd, val, nxt, .. } - | Term::Let { pat: Pattern::Tup(box Pattern::Var(fst), box Pattern::Var(snd)), val, nxt } => { - let val_detach = go(val, depth + 1, term_info); - let nxt_detach = go(nxt, depth + 1, term_info); - - term_info.provide(fst.as_ref()); - term_info.provide(snd.as_ref()); - - val_detach & nxt_detach - } - Term::Mat { args, rules } => { - let mut detach = Detach::Combinator; - for arg in args { - detach = detach & go(arg, 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_detached_num_match()); - } - - let arm_detach = match go(&mut rule.body, depth + 1, term_info) { - // If the recursive ref reached here, it is not in a active position - Detach::Recursive => Detach::Combinator, - detach => detach, - }; - - // It is expected that match arms were already linearized - detach = detach & arm_detach; - } - - // This happens when a var is used in only one arm so it is not linearized - if !term_info.has_no_free_vars() { - for rule in rules { - let (arm_body, already_extracted) = match rule.pats[0] { - Pattern::Num(MatchNum::Zero) => (&mut rule.body, false), - _ => match &mut rule.body { - Term::Lam { bod, .. } => (bod.as_mut(), false), - Term::Ref { nam } => { - let extracted = term_info.combinators.get_mut(nam).unwrap(); - let Term::Lam { ref mut bod, .. } = &mut extracted.rules[0].body else { unreachable!() }; - (bod.as_mut(), true) - } - _ => unreachable!(), - }, - }; - - let term = std::mem::take(arm_body); - - let body_vars = term.free_vars(); - - let term = term_info.needed_names.iter().rev().fold(term, |acc, arg| { - if body_vars.contains_key(arg) { - Term::named_lam(arg.clone(), acc) - } else { - Term::lam(None, acc) - } - }); - - *arm_body = term; - if !already_extracted { - term_info.detach_term(&mut rule.body); - } - } - - let mat = std::mem::take(term); - *term = term_info - .needed_names - .iter() - .fold(mat, |acc, arg| Term::app(acc, Term::Var { nam: arg.clone() })); - } - - term_info.merge_scope(parent_scope); - detach - } - Term::Sup { fst, snd, .. } | Term::Tup { fst, snd } | Term::Opx { fst, snd, .. } => { - let fst_is_super = go(fst, depth + 1, term_info); - let snd_is_super = go(snd, depth + 1, term_info); - - fst_is_super & snd_is_super - } - Term::Ref { nam: def_name } if def_name == &term_info.def_name => Detach::Recursive, - Term::Let { .. } | Term::Lst { .. } => unreachable!(), - Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => Detach::Combinator, - } - } - - go(self, 0, &mut TermInfo::new(def_name.clone(), builtin, combinators)); - } - - // 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 { - Term::Lam { nam: Some(lam_nam), bod: box Term::Var { nam: var_nam }, .. } => lam_nam == var_nam, - _ => false, - } - } -} diff --git a/src/term/transform/lift_combinators.rs b/src/term/transform/lift_combinators.rs new file mode 100644 index 000000000..07afa9f62 --- /dev/null +++ b/src/term/transform/lift_combinators.rs @@ -0,0 +1,338 @@ +use crate::term::{Book, Definition, MatchNum, Name, Pattern, Rule, Term}; +use std::{ + collections::{BTreeMap, BTreeSet}, + ops::BitAnd, +}; + +/// Replaces closed Terms (i.e. without free variables) with a Ref to the extracted term +/// Precondition: Vars must have been sanitized +impl Book { + pub fn lift_combinators(&mut self, lift_matches: bool) { + let mut combinators = Combinators::new(); + + for (def_name, def) in self.defs.iter_mut() { + if self.entrypoint.as_ref().is_some_and(|m| m == def_name) { + continue; + } + + let builtin = def.builtin; + let rule = def.rule_mut(); + rule.body.lift_combinators(def_name, lift_matches, builtin, &mut combinators); + } + + // 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); + } +} + +type Combinators = BTreeMap; + +#[derive(Debug)] +struct TermInfo<'d> { + // Number of times a Term has been detached from the current Term + counter: u32, + def_name: Name, + lift_matches: bool, + builtin: bool, + needed_names: BTreeSet, + combinators: &'d mut Combinators, +} + +impl<'d> TermInfo<'d> { + fn new(def_name: Name, lift_matches: bool, builtin: bool, combinators: &'d mut Combinators) -> Self { + Self { counter: 0, def_name, lift_matches, 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) -> BTreeSet { + std::mem::replace(&mut self.needed_names, new_scope) + } + + fn merge_scope(&mut self, target: BTreeSet) { + self.needed_names.extend(target); + } + + fn detach_term(&mut self, term: &mut Term) { + let comb_name = Name::new(format!("{}$S{}", 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)] +enum Detach { + /// Can be detached freely + Combinator, + /// Can not be detached + Unscoped { lams: BTreeSet, vars: BTreeSet }, + /// Should be detached to make the program not hang + Recursive, +} + +impl Detach { + fn can_detach(&self) -> bool { + !matches!(self, Detach::Unscoped { .. }) + } + + fn unscoped_lam(nam: Name) -> Self { + Detach::Unscoped { lams: [nam].into(), vars: Default::default() } + } + + fn unscoped_var(nam: Name) -> Self { + Detach::Unscoped { lams: Default::default(), vars: [nam].into() } + } +} + +impl BitAnd for Detach { + type Output = Detach; + + fn bitand(self, rhs: Self) -> Self::Output { + match (self, rhs) { + (Detach::Combinator, Detach::Combinator) => Detach::Combinator, + + (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 { + Detach::Unscoped { lams: res_lams, vars: res_vars } + } + } + + (Detach::Combinator, Detach::Recursive) => Detach::Recursive, + (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? + (unscoped @ Detach::Unscoped { .. }, Detach::Recursive) => unscoped, + (Detach::Recursive, unscoped @ Detach::Unscoped { .. }) => unscoped, + } + } +} + +impl Term { + pub fn lift_combinators( + &mut self, + def_name: &Name, + lift_matches: bool, + builtin: bool, + combinators: &mut Combinators, + ) { + self.go_lift(0, &mut TermInfo::new(def_name.clone(), lift_matches, builtin, combinators)); + } + + fn go_lift(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach { + match self { + Term::Lam { .. } | Term::Chn { .. } if self.is_id() => Detach::Combinator, + + Term::Lam { .. } => self.lift_lam(depth, term_info), + Term::Chn { .. } => self.lift_lam(depth, term_info), + Term::App { .. } => self.lift_app(depth, term_info), + Term::Mat { .. } => self.lift_mat(depth, term_info), + + Term::Var { nam } => { + term_info.request_name(nam); + Detach::Combinator + } + + Term::Lnk { nam } => Detach::unscoped_var(nam.clone()), + + Term::Let { pat, val, nxt } => { + let val_detach = val.go_lift(depth + 1, term_info); + let nxt_detach = nxt.go_lift(depth + 1, term_info); + + for nam in pat.bind_or_eras() { + term_info.provide(nam.as_ref()); + } + + val_detach & nxt_detach + } + + Term::Dup { fst, snd, val, nxt, .. } => { + let val_detach = val.go_lift(depth + 1, term_info); + let nxt_detach = nxt.go_lift(depth + 1, term_info); + + term_info.provide(fst.as_ref()); + term_info.provide(snd.as_ref()); + + val_detach & nxt_detach + } + + Term::Sup { fst, snd, .. } | Term::Tup { fst, snd } | Term::Opx { fst, snd, .. } => { + let fst_is_super = fst.go_lift(depth + 1, term_info); + let snd_is_super = snd.go_lift(depth + 1, term_info); + + fst_is_super & snd_is_super + } + + 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, + } + } + + fn lift_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), + _ => unreachable!(), + }; + + let parent_scope = term_info.replace_scope(BTreeSet::new()); + + let mut detach = bod.go_lift(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 lift_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_lift(depth + 1, term_info); + let fun_scope = term_info.replace_scope(BTreeSet::new()); + + let arg_detach = arg.go_lift(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 lift_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_lift(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_detached_num_match()); + } + + let arm_detach = match rule.body.go_lift(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; + } + + // This happens when a var is used in only one arm so it is not linearized + if term_info.lift_matches && !term_info.has_no_free_vars() { + for rule in rules { + let (arm_body, already_extracted) = match rule.pats[0] { + Pattern::Num(MatchNum::Zero) => (&mut rule.body, false), + _ => match &mut rule.body { + Term::Lam { bod, .. } => (bod.as_mut(), false), + Term::Ref { nam } => { + let extracted = term_info.combinators.get_mut(nam).unwrap(); + let Term::Lam { ref mut bod, .. } = &mut extracted.rules[0].body else { unreachable!() }; + (bod.as_mut(), true) + } + _ => unreachable!(), + }, + }; + + let term = std::mem::take(arm_body); + + let body_vars = term.free_vars(); + + let term = term_info.needed_names.iter().rev().fold(term, |acc, arg| { + if body_vars.contains_key(arg) { Term::named_lam(arg.clone(), acc) } else { Term::lam(None, acc) } + }); + + *arm_body = term; + if !already_extracted { + term_info.detach_term(&mut rule.body); + } + } + + let mat = std::mem::take(self); + *self = + term_info.needed_names.iter().fold(mat, |acc, arg| Term::app(acc, Term::Var { nam: arg.clone() })); + } + + 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 { + Term::Lam { nam: Some(lam_nam), bod: box Term::Var { nam: var_nam }, .. } => lam_nam == var_nam, + _ => false, + } + } +} diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs index e1cd1ac39..29956ba6f 100644 --- a/src/term/transform/linearize_matches.rs +++ b/src/term/transform/linearize_matches.rs @@ -9,12 +9,12 @@ use std::collections::{BTreeMap, BTreeSet}; impl Ctx<'_> { /// Linearizes the variables between match cases, transforming them into combinators when possible. - pub fn linearize_simple_matches(&mut self) -> Result<(), Info> { + pub fn linearize_matches(&mut self) -> Result<(), Info> { self.info.start_pass(); for (def_name, def) in self.book.defs.iter_mut() { for rule in def.rules.iter_mut() { - let res = rule.body.linearize_simple_matches(&self.book.ctrs); + let res = rule.body.linearize_matches(&self.book.ctrs); self.info.take_err(res, Some(def_name)); } } @@ -24,11 +24,11 @@ impl Ctx<'_> { } impl Term { - fn linearize_simple_matches(&mut self, ctrs: &Constructors) -> Result<(), MatchErr> { + fn linearize_matches(&mut self, ctrs: &Constructors) -> Result<(), MatchErr> { match self { Term::Mat { args: _, rules } => { for rule in rules.iter_mut() { - rule.body.linearize_simple_matches(ctrs).unwrap(); + rule.body.linearize_matches(ctrs).unwrap(); } let matched_type = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs)?; match matched_type { @@ -40,7 +40,7 @@ impl Term { } Term::Lam { bod, .. } | Term::Chn { bod, .. } => { - bod.linearize_simple_matches(ctrs)?; + bod.linearize_matches(ctrs)?; } Term::Let { pat: Pattern::Var(..), val: fst, nxt: snd } @@ -49,8 +49,8 @@ impl Term { | Term::Sup { fst, snd, .. } | Term::Opx { fst, snd, .. } | Term::App { fun: fst, arg: snd, .. } => { - fst.linearize_simple_matches(ctrs)?; - snd.linearize_simple_matches(ctrs)?; + fst.linearize_matches(ctrs)?; + snd.linearize_matches(ctrs)?; } Term::Lst { .. } => unreachable!(), @@ -84,26 +84,13 @@ pub fn linearize_match_free_vars(match_term: &mut Term) -> &mut Term { let fvs = r.body.free_vars().into_iter(); for (k, v) in fvs { if !r.pats.iter().flat_map(|p| p.binds()).contains(&k) { - match acc.entry(k) { - std::collections::btree_map::Entry::Occupied(mut o) => *o.get_mut() += v, - std::collections::btree_map::Entry::Vacant(vc) => { - vc.insert(v); - } - }; + // Counts the number of arms that the var is used + *acc.entry(k).or_insert(0) += u64::min(v, 1); } } }); let free_vars: BTreeSet = acc.into_iter().filter(|(_, v)| *v >= 2).map(|(k, _)| k).collect(); - // panic!("{acc:?}"); - - // let free_vars: BTreeSet = rules - // .iter() - // .flat_map(|r| { - // r.body.free_vars().into_keys().filter(|k| !r.pats.iter().flat_map(|p| p.binds()).contains(k)) - // }) - // .collect(); - // Add lambdas to the arms for rule in rules { let old_body = std::mem::take(&mut rule.body); diff --git a/src/term/transform/mod.rs b/src/term/transform/mod.rs index d087a0d6a..b7895ebee 100644 --- a/src/term/transform/mod.rs +++ b/src/term/transform/mod.rs @@ -2,11 +2,11 @@ pub mod definition_merge; pub mod definition_pruning; pub mod desugar_implicit_match_binds; pub mod desugar_let_destructors; -pub mod detach_supercombinators; pub mod encode_adts; pub mod encode_pattern_matching; pub mod eta_reduction; pub mod inline; +pub mod lift_combinators; pub mod linearize_matches; pub mod linearize_vars; pub mod match_defs_to_term; diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs index 63a6b3368..443765b42 100644 --- a/tests/golden_tests.rs +++ b/tests/golden_tests.rs @@ -201,7 +201,7 @@ fn simplify_matches() { ctx.check_ctrs_arities()?; ctx.check_unbound_vars()?; ctx.simplify_matches()?; - ctx.linearize_simple_matches()?; + ctx.linearize_matches()?; ctx.check_unbound_vars()?; ctx.book.make_var_names_unique(); ctx.book.linearize_vars(); @@ -239,7 +239,7 @@ fn encode_pattern_match() { ctx.check_ctrs_arities()?; ctx.check_unbound_vars()?; ctx.simplify_matches()?; - ctx.linearize_simple_matches()?; + ctx.linearize_matches()?; ctx.book.encode_simple_matches(adt_encoding); ctx.check_unbound_vars()?; ctx.book.make_var_names_unique(); From 65fd779598552d0feceaefff3b9158bf6850afe8 Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Mon, 26 Feb 2024 15:43:04 -0300 Subject: [PATCH 04/10] Revert linearize_extra to an `linearize_matches` argument --- aaaa.hvm | 6 ++ src/lib.rs | 18 ++++-- src/term/transform/lift_combinators.rs | 57 +++---------------- src/term/transform/linearize_matches.rs | 50 +++++++++------- tests/golden_tests.rs | 4 +- ...ompile_file_o_all__adt_option_and.hvm.snap | 5 +- ...all__match_dup_and_reconstruction.hvm.snap | 3 +- ..._file_o_all__num_pattern_with_var.hvm.snap | 5 +- ...e_o_all__scrutinee_reconstruction.hvm.snap | 5 +- ...encode_pattern_match__adt_tup_era.hvm.snap | 4 +- .../encode_pattern_match__def_tups.hvm.snap | 4 +- ...de_pattern_match__flatten_era_pat.hvm.snap | 12 ++-- .../encode_pattern_match__match_bind.hvm.snap | 4 +- ...ode_pattern_match__nested_let_tup.hvm.snap | 4 +- .../encode_pattern_match__ntup_sum.hvm.snap | 4 +- .../run_file__adt_option_and.hvm.snap | 2 +- tests/snapshots/run_file__print.hvm.snap | 5 ++ ...mplify_matches__double_unwrap_box.hvm.snap | 2 +- .../simplify_matches__nested.hvm.snap | 2 +- ...plify_matches__redundant_with_era.hvm.snap | 2 +- 20 files changed, 96 insertions(+), 102 deletions(-) create mode 100644 aaaa.hvm create mode 100644 tests/snapshots/run_file__print.hvm.snap diff --git a/aaaa.hvm b/aaaa.hvm new file mode 100644 index 000000000..9ae1746c0 --- /dev/null +++ b/aaaa.hvm @@ -0,0 +1,6 @@ +Map f xs = match xs { + List.nil: List.nil + (List.cons x xs): (List.cons (f x) (Map f xs)) +} + +main = (Map @a a [1 2 3]) \ No newline at end of file diff --git a/src/lib.rs b/src/lib.rs index d127a645b..91068d967 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -83,7 +83,7 @@ pub fn create_host(book: Arc, labels: Arc, compile_opts: CompileOp match term { Term::Str { val } => { println!("{}", val); - }, + } _ => (), } } @@ -140,8 +140,8 @@ pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result, ctx.book.convert_match_def_to_term(); ctx.simplify_matches()?; - if !matches!(opts.linearize_matches, OptLevel::Disabled) { - ctx.linearize_matches()?; + if opts.linearize_matches.enabled() { + ctx.linearize_matches(opts.linearize_matches.is_extra())?; } ctx.book.encode_simple_matches(opts.adt_encoding); @@ -160,7 +160,7 @@ pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result, ctx.book.eta_reduction(); } if opts.lift_combinators { - ctx.book.lift_combinators(matches!(opts.linearize_matches, OptLevel::Extra)); + ctx.book.lift_combinators(); } if opts.ref_to_ref { ctx.simplify_ref_to_ref()?; @@ -343,6 +343,16 @@ pub enum OptLevel { Extra, } +impl OptLevel { + pub fn enabled(&self) -> bool { + !matches!(self, OptLevel::Disabled) + } + + pub fn is_extra(&self) -> bool { + matches!(self, OptLevel::Extra) + } +} + #[derive(Clone, Copy, Debug, Default)] pub struct CompileOpts { /// Selects the encoding for the ADT syntax. diff --git a/src/term/transform/lift_combinators.rs b/src/term/transform/lift_combinators.rs index 07afa9f62..a27b10da1 100644 --- a/src/term/transform/lift_combinators.rs +++ b/src/term/transform/lift_combinators.rs @@ -1,4 +1,4 @@ -use crate::term::{Book, Definition, MatchNum, Name, Pattern, Rule, Term}; +use crate::term::{Book, Definition, Name, Rule, Term}; use std::{ collections::{BTreeMap, BTreeSet}, ops::BitAnd, @@ -7,7 +7,7 @@ use std::{ /// Replaces closed Terms (i.e. without free variables) with a Ref to the extracted term /// Precondition: Vars must have been sanitized impl Book { - pub fn lift_combinators(&mut self, lift_matches: bool) { + pub fn lift_combinators(&mut self) { let mut combinators = Combinators::new(); for (def_name, def) in self.defs.iter_mut() { @@ -17,7 +17,7 @@ impl Book { let builtin = def.builtin; let rule = def.rule_mut(); - rule.body.lift_combinators(def_name, lift_matches, builtin, &mut combinators); + rule.body.lift_combinators(def_name, builtin, &mut combinators); } // Definitions are not inserted to the book as they are defined to appease the borrow checker. @@ -33,15 +33,15 @@ struct TermInfo<'d> { // Number of times a Term has been detached from the current Term counter: u32, def_name: Name, - lift_matches: bool, + builtin: bool, needed_names: BTreeSet, combinators: &'d mut Combinators, } impl<'d> TermInfo<'d> { - fn new(def_name: Name, lift_matches: bool, builtin: bool, combinators: &'d mut Combinators) -> Self { - Self { counter: 0, def_name, lift_matches, builtin, needed_names: BTreeSet::new(), combinators } + 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()); @@ -140,14 +140,8 @@ impl BitAnd for Detach { } impl Term { - pub fn lift_combinators( - &mut self, - def_name: &Name, - lift_matches: bool, - builtin: bool, - combinators: &mut Combinators, - ) { - self.go_lift(0, &mut TermInfo::new(def_name.clone(), lift_matches, builtin, combinators)); + pub fn lift_combinators(&mut self, def_name: &Name, builtin: bool, combinators: &mut Combinators) { + self.go_lift(0, &mut TermInfo::new(def_name.clone(), builtin, combinators)); } fn go_lift(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach { @@ -289,41 +283,6 @@ impl Term { detach = detach & arm_detach; } - // This happens when a var is used in only one arm so it is not linearized - if term_info.lift_matches && !term_info.has_no_free_vars() { - for rule in rules { - let (arm_body, already_extracted) = match rule.pats[0] { - Pattern::Num(MatchNum::Zero) => (&mut rule.body, false), - _ => match &mut rule.body { - Term::Lam { bod, .. } => (bod.as_mut(), false), - Term::Ref { nam } => { - let extracted = term_info.combinators.get_mut(nam).unwrap(); - let Term::Lam { ref mut bod, .. } = &mut extracted.rules[0].body else { unreachable!() }; - (bod.as_mut(), true) - } - _ => unreachable!(), - }, - }; - - let term = std::mem::take(arm_body); - - let body_vars = term.free_vars(); - - let term = term_info.needed_names.iter().rev().fold(term, |acc, arg| { - if body_vars.contains_key(arg) { Term::named_lam(arg.clone(), acc) } else { Term::lam(None, acc) } - }); - - *arm_body = term; - if !already_extracted { - term_info.detach_term(&mut rule.body); - } - } - - let mat = std::mem::take(self); - *self = - term_info.needed_names.iter().fold(mat, |acc, arg| Term::app(acc, Term::Var { nam: arg.clone() })); - } - term_info.merge_scope(parent_scope); detach } diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs index 29956ba6f..460583ad2 100644 --- a/src/term/transform/linearize_matches.rs +++ b/src/term/transform/linearize_matches.rs @@ -9,12 +9,12 @@ use std::collections::{BTreeMap, BTreeSet}; impl Ctx<'_> { /// Linearizes the variables between match cases, transforming them into combinators when possible. - pub fn linearize_matches(&mut self) -> Result<(), Info> { + pub fn linearize_matches(&mut self, linearize_extra: bool) -> Result<(), Info> { self.info.start_pass(); for (def_name, def) in self.book.defs.iter_mut() { for rule in def.rules.iter_mut() { - let res = rule.body.linearize_matches(&self.book.ctrs); + let res = rule.body.linearize_matches(&self.book.ctrs, linearize_extra); self.info.take_err(res, Some(def_name)); } } @@ -24,23 +24,23 @@ impl Ctx<'_> { } impl Term { - fn linearize_matches(&mut self, ctrs: &Constructors) -> Result<(), MatchErr> { + fn linearize_matches(&mut self, ctrs: &Constructors, linearize_extra: bool) -> Result<(), MatchErr> { match self { Term::Mat { args: _, rules } => { for rule in rules.iter_mut() { - rule.body.linearize_matches(ctrs).unwrap(); + rule.body.linearize_matches(ctrs, linearize_extra).unwrap(); } let matched_type = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs)?; match matched_type { - Type::Num | Type::Tup | Type::Any => _ = linearize_match_free_vars(self), + Type::Num | Type::Tup | Type::Any => _ = linearize_match_free_vars(self, linearize_extra), Type::Adt(_) => { - linearize_match_free_vars(self); + linearize_match_free_vars(self, linearize_extra); } } } Term::Lam { bod, .. } | Term::Chn { bod, .. } => { - bod.linearize_matches(ctrs)?; + bod.linearize_matches(ctrs, linearize_extra)?; } Term::Let { pat: Pattern::Var(..), val: fst, nxt: snd } @@ -49,8 +49,8 @@ impl Term { | Term::Sup { fst, snd, .. } | Term::Opx { fst, snd, .. } | Term::App { fun: fst, arg: snd, .. } => { - fst.linearize_matches(ctrs)?; - snd.linearize_matches(ctrs)?; + fst.linearize_matches(ctrs, linearize_extra)?; + snd.linearize_matches(ctrs, linearize_extra)?; } Term::Lst { .. } => unreachable!(), @@ -74,22 +74,28 @@ impl Term { /// Converts free vars inside the match arms into lambdas with applications to give them the external value. /// Makes the rules extractable and linear (no need for dups when variable used in both rules) -pub fn linearize_match_free_vars(match_term: &mut Term) -> &mut Term { +pub fn linearize_match_free_vars(match_term: &mut Term, linearize_extra: bool) -> &mut Term { let Term::Mat { args: _, rules } = match_term else { unreachable!() }; - // Collect the vars. - // We need consistent iteration order. - let mut acc: BTreeMap = BTreeMap::new(); - rules.iter().for_each(|r| { - let fvs = r.body.free_vars().into_iter(); - for (k, v) in fvs { - if !r.pats.iter().flat_map(|p| p.binds()).contains(&k) { - // Counts the number of arms that the var is used - *acc.entry(k).or_insert(0) += u64::min(v, 1); - } - } + let free = rules.iter().flat_map(|rule| { + rule.body.free_vars().into_iter().filter(|(name, _)| !rule.pats.iter().any(|p| p.binds().contains(name))) }); - let free_vars: BTreeSet = acc.into_iter().filter(|(_, v)| *v >= 2).map(|(k, _)| k).collect(); + + // Collect the vars. + // We need consistent iteration order. + let free_vars: BTreeSet = if linearize_extra { + free.map(|(name, _)| name).collect() + } else { + free + .fold(BTreeMap::new(), |mut acc, (name, count)| { + *acc.entry(name).or_insert(0) += count.min(1); + acc + }) + .into_iter() + .filter(|(_, count)| *count >= 2) + .map(|(name, _)| name) + .collect() + }; // Add lambdas to the arms for rule in rules { diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs index 443765b42..75485016b 100644 --- a/tests/golden_tests.rs +++ b/tests/golden_tests.rs @@ -201,7 +201,7 @@ fn simplify_matches() { ctx.check_ctrs_arities()?; ctx.check_unbound_vars()?; ctx.simplify_matches()?; - ctx.linearize_matches()?; + ctx.linearize_matches(true)?; ctx.check_unbound_vars()?; ctx.book.make_var_names_unique(); ctx.book.linearize_vars(); @@ -239,7 +239,7 @@ fn encode_pattern_match() { ctx.check_ctrs_arities()?; ctx.check_unbound_vars()?; ctx.simplify_matches()?; - ctx.linearize_matches()?; + ctx.linearize_matches(true)?; ctx.book.encode_simple_matches(adt_encoding); ctx.check_unbound_vars()?; ctx.book.make_var_names_unique(); diff --git a/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap b/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap index 75b33bfa5..28d3ce80f 100644 --- a/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap +++ b/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap @@ -3,7 +3,10 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/compile_file_o_all/adt_option_and.hvm --- @None = {2 * {2 a a}} -@Option.and = ({2 {4 a b} {2 @None c}} ({2 {4 d {2 {4 [a d] e} {2 * e}}} {2 @None b}} c)) +@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$S3_$_Option.and$S1 = (* @None) @Some = (a {2 {4 a b} {2 * b}}) @main = a & @Option.and ~ (b (c a)) diff --git a/tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap b/tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap index bc13a83c9..4e9e419e4 100644 --- a/tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap +++ b/tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap @@ -3,7 +3,8 @@ 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}) -@Got = ({3 {2 {4 a [b a]} c} b} c) +@Got = ({3 {2 @Got$S0 (a b)} a} b) +@Got$S0 = {4 a (b [b a])} @main = a & @Got ~ (b a) & @Boxed ~ (#10 b) diff --git a/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap b/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap index b221cbd77..370013f57 100644 --- a/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap +++ b/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap @@ -2,8 +2,9 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm --- -@Foo = ({2 (* #0) {2 @Foo$S1 a}} a) -@Foo$S1 = (?<(#0 (a a)) b> b) +@Foo = ({2 (* #0) {2 @Foo$S3 a}} a) +@Foo$S2 = (a (* a)) +@Foo$S3 = (?<((* #0) @Foo$S2) (* a)> a) @main = a & @Foo ~ (@true (#3 a)) @true = {2 * {2 a a}} diff --git a/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap b/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap index 1b796d8e5..5b22067ad 100644 --- a/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap +++ b/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap @@ -3,7 +3,10 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/compile_file_o_all/scrutinee_reconstruction.hvm --- @None = {2 * {2 a a}} -@Option.or = ({3 {2 {4 * a} {2 b c}} a} (b c)) +@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$S2 = (* (a a)) @Some = (a {2 {4 a b} {2 * b}}) @main = a & @Option.or ~ (b (@None a)) diff --git a/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap b/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap index 7dba7642f..9e2d9a0e9 100644 --- a/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap +++ b/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap @@ -3,14 +3,14 @@ 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 λ* #Tuple (b #Tuple.Pair.a λd #Tuple.Pair.b λ* d)) +(Foo) = λa #Tuple (a #Tuple.Pair.a λb #Tuple.Pair.b λc (#Tuple (b #Tuple.Pair.a λd #Tuple.Pair.b λ* λ* d) c)) (Main) = (Foo (Pair 1 5)) (Pair) = λa λb #Tuple λc #Tuple.Pair.b (#Tuple.Pair.a (c a) b) Scott: -(Foo) = λa (a λb λ* (b λd λ* d)) +(Foo) = λa (a λb λc (b λd λ* λ* d c)) (Main) = (Foo (Pair 1 5)) diff --git a/tests/snapshots/encode_pattern_match__def_tups.hvm.snap b/tests/snapshots/encode_pattern_match__def_tups.hvm.snap index c9f5fdb05..3bee95847 100644 --- a/tests/snapshots/encode_pattern_match__def_tups.hvm.snap +++ b/tests/snapshots/encode_pattern_match__def_tups.hvm.snap @@ -3,11 +3,11 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/def_tups.hvm --- TaggedScott: -(go) = λa let (b, c) = a; let (d, e) = c; let (f, g) = e; let (h, i) = g; (+ (+ (+ (+ i h) f) d) b) +(go) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, h) = e; λi λj (let (k, l) = h; λm λn λo (+ (+ (+ (+ l k) o) n) m) i j g) f d) b) (main) = (go (1, (2, (3, (4, 5))))) Scott: -(go) = λa let (b, c) = a; let (d, e) = c; let (f, g) = e; let (h, i) = g; (+ (+ (+ (+ i h) f) d) b) +(go) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, h) = e; λi λj (let (k, l) = h; λm λn λo (+ (+ (+ (+ l k) o) n) m) i j g) f d) b) (main) = (go (1, (2, (3, (4, 5))))) diff --git a/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap b/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap index 5a962b6d0..db2ad4fa2 100644 --- a/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap +++ b/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap @@ -3,19 +3,19 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm --- TaggedScott: -(Fn1) = λa λ* let (*, d) = a; let (e, *) = d; e +(Fn1) = λa λb (let (c, d) = a; λe (let (f, *) = d; λ* λ* f c e) b) -(Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f +(Fn2) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, *) = e; λ* λ* g f d) b) -(Fn3) = λa λb let (c, d) = a; (match c { 0: λ* λ* 0; +: λh λ* λ* h } d b) +(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; +: λi λ* λ* i } d e) b) (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0) Scott: -(Fn1) = λa λ* let (*, d) = a; let (e, *) = d; e +(Fn1) = λa λb (let (c, d) = a; λe (let (f, *) = d; λ* λ* f c e) b) -(Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f +(Fn2) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, *) = e; λ* λ* g f d) b) -(Fn3) = λa λb let (c, d) = a; (match c { 0: λ* λ* 0; +: λh λ* λ* h } d b) +(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; +: λi λ* λ* i } d e) b) (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0) diff --git a/tests/snapshots/encode_pattern_match__match_bind.hvm.snap b/tests/snapshots/encode_pattern_match__match_bind.hvm.snap index 57b840eb6..f1b9170b8 100644 --- a/tests/snapshots/encode_pattern_match__match_bind.hvm.snap +++ b/tests/snapshots/encode_pattern_match__match_bind.hvm.snap @@ -3,11 +3,11 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/match_bind.hvm --- TaggedScott: -(cheese) = let {a a_2} = (+ 2 3); match a { 0: 653323; +: λc (+ a_2 c) } +(cheese) = let {a a_2} = (+ 2 3); (match a { 0: λ* 653323; +: λd λe (+ e d) } a_2) (main) = cheese Scott: -(cheese) = let {a a_2} = (+ 2 3); match a { 0: 653323; +: λc (+ a_2 c) } +(cheese) = let {a a_2} = (+ 2 3); (match a { 0: λ* 653323; +: λd λe (+ e d) } a_2) (main) = cheese diff --git a/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap b/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap index 04e6a0ef9..ce13f20ac 100644 --- a/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap +++ b/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap @@ -3,7 +3,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/nested_let_tup.hvm --- TaggedScott: -(main) = let (*, k) = let (*, c) = (10, ((1, ((2, 3), 4)), 3)); let (d, *) = c; d; let (l, *) = k; let (q, *) = l; q +(main) = let (k, l) = let (b, c) = (10, ((1, ((2, 3), 4)), 3)); (let (d, *) = c; λ* d b); (let (m, *) = l; λ* let (s, *) = m; s k) Scott: -(main) = let (*, k) = let (*, c) = (10, ((1, ((2, 3), 4)), 3)); let (d, *) = c; d; let (l, *) = k; let (q, *) = l; q +(main) = let (k, l) = let (b, c) = (10, ((1, ((2, 3), 4)), 3)); (let (d, *) = c; λ* d b); (let (m, *) = l; λ* let (s, *) = m; s k) diff --git a/tests/snapshots/encode_pattern_match__ntup_sum.hvm.snap b/tests/snapshots/encode_pattern_match__ntup_sum.hvm.snap index 43d6bcd2e..657be29a2 100644 --- a/tests/snapshots/encode_pattern_match__ntup_sum.hvm.snap +++ b/tests/snapshots/encode_pattern_match__ntup_sum.hvm.snap @@ -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; let (f, g) = c; let (h, i) = g; (+ d (+ e (+ f (+ h i)))) +(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) (main) = (ntupSum ((1, 3), (3, (2, 1)))) Scott: -(ntupSum) = λa let (b, c) = a; let (d, e) = b; let (f, g) = c; let (h, i) = g; (+ d (+ e (+ f (+ h i)))) +(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) (main) = (ntupSum ((1, 3), (3, (2, 1)))) diff --git a/tests/snapshots/run_file__adt_option_and.hvm.snap b/tests/snapshots/run_file__adt_option_and.hvm.snap index 493ce8486..87118776f 100644 --- a/tests/snapshots/run_file__adt_option_and.hvm.snap +++ b/tests/snapshots/run_file__adt_option_and.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/adt_option_and.hvm --- -λa λb match a { (Some c): match b { (Some d): (Some (c, d)); (None): None }; (None): None } +λa match a { (Some b): λc (match c { (Some d): λe (Some (e, d)); (None): λ* None } b); (None): λ* None } diff --git a/tests/snapshots/run_file__print.hvm.snap b/tests/snapshots/run_file__print.hvm.snap new file mode 100644 index 000000000..4cdae60ab --- /dev/null +++ b/tests/snapshots/run_file__print.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/run_file/print.hvm +--- +"goodbye world" diff --git a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap index e7efc5c7d..4257a7684 100644 --- a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap +++ b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap @@ -2,7 +2,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/double_unwrap_box.hvm --- -(DoubleUnbox) = λa λ* match a { (Box c): match c { (Box d): d } } +(DoubleUnbox) = λa λb (match a { (Box c): λd (match c { (Box e): λ* e } d) } b) (Main) = (DoubleUnbox (Box (Box 0)) 5) diff --git a/tests/snapshots/simplify_matches__nested.hvm.snap b/tests/snapshots/simplify_matches__nested.hvm.snap index 009bfb848..d1b900557 100644 --- a/tests/snapshots/simplify_matches__nested.hvm.snap +++ b/tests/snapshots/simplify_matches__nested.hvm.snap @@ -2,7 +2,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/nested.hvm --- -(Rule) = λa match a { (CtrA b c): (match c { (CtrB1 d): λe (e d); (CtrB2 h i): λj match h { (CtrC): (j i) } } b); (CtrB n): n } +(Rule) = λa match a { (CtrA b c): (match c { (CtrB1 d): λe (e d); (CtrB2 h i): λj (match h { (CtrC): λk λl (k l) } j i) } b); (CtrB p): p } (CtrC) = #Baz λa a diff --git a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap index 8946642cd..a0f05ce94 100644 --- a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap +++ b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap @@ -2,6 +2,6 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/redundant_with_era.hvm --- -(Fn2) = λa λb (match a { 0: λc match c { (*, f): match f { (*, h): h } }; +*: λk match k { (*, m): match m { (*, o): o } } } b) +(Fn2) = λa λb (match a { 0: λc (match c { (e, f): λg (match f { (*, i): λ* λ* i } g e) } *); +m: λn (match n { (o, p): λq (match p { (*, s): λ* λ* s } q o) } m) } b) (main) = * From 6ad080b5eb6d7095bbb9ac307ed8e2790de3db2d Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Mon, 26 Feb 2024 16:20:41 -0300 Subject: [PATCH 05/10] Remove unused test file --- aaaa.hvm | 6 ------ 1 file changed, 6 deletions(-) delete mode 100644 aaaa.hvm diff --git a/aaaa.hvm b/aaaa.hvm deleted file mode 100644 index 9ae1746c0..000000000 --- a/aaaa.hvm +++ /dev/null @@ -1,6 +0,0 @@ -Map f xs = match xs { - List.nil: List.nil - (List.cons x xs): (List.cons (f x) (Map f xs)) -} - -main = (Map @a a [1 2 3]) \ No newline at end of file From 3c4f0dbcf12820a01cd38b41f1801ad29309e5ce Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Mon, 26 Feb 2024 16:25:58 -0300 Subject: [PATCH 06/10] Fix `lazy_mode` flag check --- src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib.rs b/src/lib.rs index 91068d967..2cba01f66 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -421,7 +421,7 @@ impl CompileOpts { // Disable optimizations that don't work or are unnecessary on lazy mode pub fn lazy_mode(&mut self) { self.lift_combinators = false; - if let OptLevel::Extra = self.linearize_matches { + if self.linearize_matches.is_extra() { self.linearize_matches = OptLevel::Enabled; } self.pre_reduce = false; From ed190fa60c7caca47f6d250a26737224d3833125 Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Tue, 27 Feb 2024 09:30:11 -0300 Subject: [PATCH 07/10] Rename passes to be more descriptive --- docs/compiler-options.md | 4 +- docs/lazy-definitions.md | 2 +- src/lib.rs | 20 +++--- src/main.rs | 14 ++--- ...ft_combinators.rs => float_combinators.rs} | 46 +++++++------- src/term/transform/linearize_matches.rs | 62 +++++-------------- src/term/transform/mod.rs | 2 +- 7 files changed, 60 insertions(+), 90 deletions(-) rename src/term/transform/{lift_combinators.rs => float_combinators.rs} (84%) diff --git a/docs/compiler-options.md b/docs/compiler-options.md index d637f4a7e..889577a51 100644 --- a/docs/compiler-options.md +++ b/docs/compiler-options.md @@ -8,7 +8,7 @@ | `-Oref-to-ref` `-Ono-ref-to-ref` | Disabled | [ref-to-ref](#ref-to-ref) | | `-Oprune` `-Ono-prune` | Disabled | [definition-pruning](#definition-pruning) | | `-Opre-reduce` `-Ono-pre-reduce` | Disabled | [pre-reduce](#pre-reduce) | -| `-Olift_combinators` `-Ono-lift_combinators` | Enabled | [lift-combinators](#lift-combinators) | +| `-Ofloat_combinators` `-Ono-float_combinators` | Enabled | [float-combinators](#float-combinators) | | `-Osimplify-main` `-Ono-simplify-main` | Disabled | [simplify-main](#simplify-main) | | `-Omerge` `-Ono-merge` | Disabled | [definition-merging](#definition-merging) | | `-Oinline` `-Ono-inline` | Disabled | [inline](#inline) | @@ -134,7 +134,7 @@ main = (bar) @main = @bar ``` -## Lift-Combinators +## float-combinators Extracts closed terms to new definitions. See [lazy definitions](lazy-definitions#automatic-optimization). Since HVM-Core is an eager runtime, this pass is enabled by default to prevent infinite expansions. diff --git a/docs/lazy-definitions.md b/docs/lazy-definitions.md index 9c7da9535..31967521a 100644 --- a/docs/lazy-definitions.md +++ b/docs/lazy-definitions.md @@ -49,4 +49,4 @@ The lambda terms without free variables are extracted to new definitions. ToMachine0 = λp (+ 1 (ToMachine p)) ToMachine = λn (n ToMachine0 0) ``` -Definitions are lazy in the runtime. Lifting lambda terms to new definitions will prevent infinite expansion. +Definitions are lazy in the runtime. Floating lambda terms into new definitions will prevent infinite expansion. diff --git a/src/lib.rs b/src/lib.rs index 2cba01f66..968dd4375 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -159,8 +159,8 @@ pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result, if opts.eta { ctx.book.eta_reduction(); } - if opts.lift_combinators { - ctx.book.lift_combinators(); + if opts.float_combinators { + ctx.book.float_combinators(); } if opts.ref_to_ref { ctx.simplify_ref_to_ref()?; @@ -373,8 +373,8 @@ pub struct CompileOpts { /// Enables [term::transform::linearize_matches]. pub linearize_matches: OptLevel, - /// Enables [term::transform::lift_combinators]. - pub lift_combinators: bool, + /// Enables [term::transform::float_combinators]. + pub float_combinators: bool, /// Enables [term::transform::simplify_main_ref]. pub simplify_main: bool, @@ -394,7 +394,7 @@ impl CompileOpts { ref_to_ref: true, prune: true, pre_reduce: true, - lift_combinators: true, + float_combinators: true, simplify_main: true, merge: true, inline: true, @@ -413,14 +413,14 @@ impl CompileOpts { Self { adt_encoding: self.adt_encoding, ..Self::default() } } - /// All optimizations disabled, except lift_combinators and linearize_matches + /// All optimizations disabled, except float_combinators and linearize_matches pub fn light() -> Self { - Self { lift_combinators: true, linearize_matches: OptLevel::Extra, ..Self::default() } + Self { float_combinators: true, linearize_matches: OptLevel::Extra, ..Self::default() } } // Disable optimizations that don't work or are unnecessary on lazy mode pub fn lazy_mode(&mut self) { - self.lift_combinators = false; + self.float_combinators = false; if self.linearize_matches.is_extra() { self.linearize_matches = OptLevel::Enabled; } @@ -430,9 +430,9 @@ impl CompileOpts { impl CompileOpts { pub fn check(&self, lazy_mode: bool) { - if !self.lift_combinators && !lazy_mode { + if !self.float_combinators && !lazy_mode { println!( - "Warning: Running in strict mode without enabling the lift_combinators pass can lead to some functions expanding infinitely." + "Warning: Running in strict mode without enabling the float_combinators pass can lead to some functions expanding infinitely." ); } } diff --git a/src/main.rs b/src/main.rs index a08d3158b..6afe45f8e 100644 --- a/src/main.rs +++ b/src/main.rs @@ -38,7 +38,7 @@ enum Mode { value_delimiter = ' ', action = clap::ArgAction::Append, long_help = r#"Enables or disables the given optimizations - lift_combinators is enabled by default on strict mode."#, + float_combinators is enabled by default on strict mode."#, )] comp_opts: Vec, @@ -82,7 +82,7 @@ enum Mode { value_delimiter = ' ', action = clap::ArgAction::Append, long_help = r#"Enables or disables the given optimizations - lift_combinators is enabled by default on strict mode."#, + float_combinators is enabled by default on strict mode."#, )] comp_opts: Vec, @@ -99,7 +99,7 @@ enum Mode { value_delimiter = ' ', action = clap::ArgAction::Append, long_help = r#"Enables or disables the given optimizations - lift_combinators is enabled by default on strict mode."#, + float_combinators is enabled by default on strict mode."#, )] comp_opts: Vec, @@ -297,8 +297,8 @@ pub enum OptArgs { LinearizeMatches, LinearizeMatchesExtra, NoLinearizeMatches, - LiftCombinators, - NoLiftCombinators, + FloatCombinators, + NoFloatCombinators, SimplifyMain, NoSimplifyMain, Merge, @@ -325,8 +325,8 @@ impl OptArgs { NoRefToRef => opts.ref_to_ref = false, PreReduce => opts.pre_reduce = true, NoPreReduce => opts.pre_reduce = false, - LiftCombinators => opts.lift_combinators = true, - NoLiftCombinators => opts.lift_combinators = false, + FloatCombinators => opts.float_combinators = true, + NoFloatCombinators => opts.float_combinators = false, SimplifyMain => opts.simplify_main = true, NoSimplifyMain => opts.simplify_main = false, Merge => opts.merge = true, diff --git a/src/term/transform/lift_combinators.rs b/src/term/transform/float_combinators.rs similarity index 84% rename from src/term/transform/lift_combinators.rs rename to src/term/transform/float_combinators.rs index a27b10da1..8bcac0718 100644 --- a/src/term/transform/lift_combinators.rs +++ b/src/term/transform/float_combinators.rs @@ -7,7 +7,7 @@ use std::{ /// Replaces closed Terms (i.e. without free variables) with a Ref to the extracted term /// Precondition: Vars must have been sanitized impl Book { - pub fn lift_combinators(&mut self) { + pub fn float_combinators(&mut self) { let mut combinators = Combinators::new(); for (def_name, def) in self.defs.iter_mut() { @@ -17,7 +17,7 @@ impl Book { let builtin = def.builtin; let rule = def.rule_mut(); - rule.body.lift_combinators(def_name, builtin, &mut combinators); + rule.body.float_combinators(def_name, builtin, &mut combinators); } // Definitions are not inserted to the book as they are defined to appease the borrow checker. @@ -140,18 +140,18 @@ impl BitAnd for Detach { } impl Term { - pub fn lift_combinators(&mut self, def_name: &Name, builtin: bool, combinators: &mut Combinators) { - self.go_lift(0, &mut TermInfo::new(def_name.clone(), builtin, combinators)); + pub fn float_combinators(&mut self, def_name: &Name, builtin: bool, combinators: &mut Combinators) { + self.go_float(0, &mut TermInfo::new(def_name.clone(), builtin, combinators)); } - fn go_lift(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach { + fn go_float(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach { match self { Term::Lam { .. } | Term::Chn { .. } if self.is_id() => Detach::Combinator, - Term::Lam { .. } => self.lift_lam(depth, term_info), - Term::Chn { .. } => self.lift_lam(depth, term_info), - Term::App { .. } => self.lift_app(depth, term_info), - Term::Mat { .. } => self.lift_mat(depth, term_info), + 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); @@ -161,8 +161,8 @@ impl Term { Term::Lnk { nam } => Detach::unscoped_var(nam.clone()), Term::Let { pat, val, nxt } => { - let val_detach = val.go_lift(depth + 1, term_info); - let nxt_detach = nxt.go_lift(depth + 1, term_info); + let val_detach = val.go_float(depth + 1, term_info); + let nxt_detach = nxt.go_float(depth + 1, term_info); for nam in pat.bind_or_eras() { term_info.provide(nam.as_ref()); @@ -172,8 +172,8 @@ impl Term { } Term::Dup { fst, snd, val, nxt, .. } => { - let val_detach = val.go_lift(depth + 1, term_info); - let nxt_detach = nxt.go_lift(depth + 1, term_info); + 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()); @@ -182,8 +182,8 @@ impl Term { } Term::Sup { fst, snd, .. } | Term::Tup { fst, snd } | Term::Opx { fst, snd, .. } => { - let fst_is_super = fst.go_lift(depth + 1, term_info); - let snd_is_super = snd.go_lift(depth + 1, term_info); + let fst_is_super = fst.go_float(depth + 1, term_info); + let snd_is_super = snd.go_float(depth + 1, term_info); fst_is_super & snd_is_super } @@ -195,7 +195,7 @@ impl Term { } } - fn lift_lam(&mut self, depth: usize, term_info: &mut TermInfo) -> 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, .. } => (Some(nam), bod, true), @@ -204,7 +204,7 @@ impl Term { let parent_scope = term_info.replace_scope(BTreeSet::new()); - let mut detach = bod.go_lift(depth + 1, term_info); + let mut detach = bod.go_float(depth + 1, term_info); if unscoped { detach = detach & Detach::unscoped_lam(nam.cloned().unwrap()); @@ -221,15 +221,15 @@ impl Term { detach } - fn lift_app(&mut self, depth: usize, term_info: &mut TermInfo) -> 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_lift(depth + 1, term_info); + let fun_detach = fun.go_float(depth + 1, term_info); let fun_scope = term_info.replace_scope(BTreeSet::new()); - let arg_detach = arg.go_lift(depth + 1, term_info); + let arg_detach = arg.go_float(depth + 1, term_info); let arg_scope = term_info.replace_scope(parent_scope); let detach = match fun_detach { @@ -260,12 +260,12 @@ impl Term { detach } - fn lift_mat(&mut self, depth: usize, term_info: &mut TermInfo) -> 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_lift(depth + 1, term_info); + detach = detach & arg.go_float(depth + 1, term_info); } let parent_scope = term_info.replace_scope(BTreeSet::new()); @@ -274,7 +274,7 @@ impl Term { debug_assert!(pat.is_detached_num_match()); } - let arm_detach = match rule.body.go_lift(depth + 1, term_info) { + 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, diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs index 460583ad2..dce2dddcc 100644 --- a/src/term/transform/linearize_matches.rs +++ b/src/term/transform/linearize_matches.rs @@ -3,18 +3,17 @@ use crate::{ diagnostics::Info, term::{check::type_check::infer_type, Constructors, Ctx, Name, Pattern, Term, Type}, }; -use indexmap::IndexSet; use itertools::Itertools; use std::collections::{BTreeMap, BTreeSet}; impl Ctx<'_> { /// Linearizes the variables between match cases, transforming them into combinators when possible. - pub fn linearize_matches(&mut self, linearize_extra: bool) -> Result<(), Info> { + pub fn linearize_matches(&mut self, lift_all_vars: bool) -> Result<(), Info> { self.info.start_pass(); for (def_name, def) in self.book.defs.iter_mut() { for rule in def.rules.iter_mut() { - let res = rule.body.linearize_matches(&self.book.ctrs, linearize_extra); + let res = rule.body.linearize_matches(&self.book.ctrs, lift_all_vars); self.info.take_err(res, Some(def_name)); } } @@ -24,23 +23,23 @@ impl Ctx<'_> { } impl Term { - fn linearize_matches(&mut self, ctrs: &Constructors, linearize_extra: bool) -> Result<(), MatchErr> { + fn linearize_matches(&mut self, ctrs: &Constructors, lift_all_vars: bool) -> Result<(), MatchErr> { match self { Term::Mat { args: _, rules } => { for rule in rules.iter_mut() { - rule.body.linearize_matches(ctrs, linearize_extra).unwrap(); + rule.body.linearize_matches(ctrs, lift_all_vars).unwrap(); } let matched_type = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs)?; match matched_type { - Type::Num | Type::Tup | Type::Any => _ = linearize_match_free_vars(self, linearize_extra), + Type::Num | Type::Tup | Type::Any => _ = lift_match_vars(self, lift_all_vars), Type::Adt(_) => { - linearize_match_free_vars(self, linearize_extra); + lift_match_vars(self, lift_all_vars); } } } Term::Lam { bod, .. } | Term::Chn { bod, .. } => { - bod.linearize_matches(ctrs, linearize_extra)?; + bod.linearize_matches(ctrs, lift_all_vars)?; } Term::Let { pat: Pattern::Var(..), val: fst, nxt: snd } @@ -49,8 +48,8 @@ impl Term { | Term::Sup { fst, snd, .. } | Term::Opx { fst, snd, .. } | Term::App { fun: fst, arg: snd, .. } => { - fst.linearize_matches(ctrs, linearize_extra)?; - snd.linearize_matches(ctrs, linearize_extra)?; + fst.linearize_matches(ctrs, lift_all_vars)?; + snd.linearize_matches(ctrs, lift_all_vars)?; } Term::Lst { .. } => unreachable!(), @@ -74,7 +73,12 @@ impl Term { /// Converts free vars inside the match arms into lambdas with applications to give them the external value. /// Makes the rules extractable and linear (no need for dups when variable used in both rules) -pub fn linearize_match_free_vars(match_term: &mut Term, linearize_extra: bool) -> &mut Term { +/// +/// If `lift_all_vars`, acts on all variables found in the arms, +/// Otherwise, only lift vars that are used on more than one arm. +/// +/// Obs: This does not interact unscoped variables +pub fn lift_match_vars(match_term: &mut Term, lift_all_vars: bool) -> &mut Term { let Term::Mat { args: _, rules } = match_term else { unreachable!() }; let free = rules.iter().flat_map(|rule| { @@ -83,7 +87,7 @@ pub fn linearize_match_free_vars(match_term: &mut Term, linearize_extra: bool) - // Collect the vars. // We need consistent iteration order. - let free_vars: BTreeSet = if linearize_extra { + let free_vars: BTreeSet = if lift_all_vars { free.map(|(name, _)| name).collect() } else { free @@ -110,40 +114,6 @@ pub fn linearize_match_free_vars(match_term: &mut Term, linearize_extra: bool) - get_match_reference(match_term) } -pub fn linearize_match_unscoped_vars(match_term: &mut Term) -> Result<&mut Term, MatchErr> { - let Term::Mat { args: _, rules } = match_term else { unreachable!() }; - // Collect the vars - let mut free_vars = IndexSet::new(); - for rule in rules.iter_mut() { - let (decls, uses) = rule.body.unscoped_vars(); - // Not allowed to declare unscoped var and not use it since we need to extract the match arm. - if let Some(var) = decls.difference(&uses).next() { - return Err(MatchErr::Linearize(Name::new(format!("λ${var}")))); - } - // Change unscoped var to normal scoped var if it references something outside this match arm. - let arm_free_vars = uses.difference(&decls); - for var in arm_free_vars.clone() { - rule.body.subst_unscoped(var, &Term::Var { nam: Name::new(format!("%match%unscoped%{var}")) }); - } - free_vars.extend(arm_free_vars.cloned()); - } - - // Add lambdas to the arms - for rule in rules { - let old_body = std::mem::take(&mut rule.body); - rule.body = free_vars - .iter() - .rev() - .fold(old_body, |body, var| Term::named_lam(Name::new(format!("%match%unscoped%{var}")), body)); - } - - // Add apps to the match - let old_match = std::mem::take(match_term); - *match_term = free_vars.into_iter().fold(old_match, |acc, nam| Term::call(acc, [Term::Lnk { nam }])); - - Ok(get_match_reference(match_term)) -} - /// Get a reference to the match again /// It returns a reference and not an owned value because we want /// to keep the new surrounding Apps but still modify the match further. diff --git a/src/term/transform/mod.rs b/src/term/transform/mod.rs index b7895ebee..5a8693c66 100644 --- a/src/term/transform/mod.rs +++ b/src/term/transform/mod.rs @@ -5,8 +5,8 @@ pub mod desugar_let_destructors; pub mod encode_adts; pub mod encode_pattern_matching; pub mod eta_reduction; +pub mod float_combinators; pub mod inline; -pub mod lift_combinators; pub mod linearize_matches; pub mod linearize_vars; pub mod match_defs_to_term; From 5548cff89b626f15fc7e9c6d31da1cb3d01ddee2 Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Tue, 27 Feb 2024 10:00:02 -0300 Subject: [PATCH 08/10] Rename pass, add flag docs --- docs/compiler-options.md | 24 ++++++++++++++++++++++++ src/lib.rs | 17 ++++++++++++----- src/term/transform/linearize_matches.rs | 14 +++++++------- tests/golden_tests.rs | 4 ++-- 4 files changed, 45 insertions(+), 14 deletions(-) diff --git a/docs/compiler-options.md b/docs/compiler-options.md index 889577a51..bc3e940a2 100644 --- a/docs/compiler-options.md +++ b/docs/compiler-options.md @@ -8,6 +8,7 @@ | `-Oref-to-ref` `-Ono-ref-to-ref` | Disabled | [ref-to-ref](#ref-to-ref) | | `-Oprune` `-Ono-prune` | Disabled | [definition-pruning](#definition-pruning) | | `-Opre-reduce` `-Ono-pre-reduce` | Disabled | [pre-reduce](#pre-reduce) | +| `-Olinearize-matches` `-Olinearize-matches-extra` `-Ono-linearize-matches` | Extra | [linearize-matches](#linearize-matches) | | `-Ofloat_combinators` `-Ono-float_combinators` | Enabled | [float-combinators](#float-combinators) | | `-Osimplify-main` `-Ono-simplify-main` | Disabled | [simplify-main](#simplify-main) | | `-Omerge` `-Ono-merge` | Disabled | [definition-merging](#definition-merging) | @@ -134,6 +135,29 @@ main = (bar) @main = @bar ``` +## linearize-matches + +Linearizes the variables between match cases, transforming them into combinators when possible. +When `linearize-matches` linearizes only vars that are used in more than one arm. + +Example: +```rs +λa λb match a { 0: b; +: b } + +// Is tranformed to +λa λb (match a { 0: λc c; +: λd d } b) +``` + +When `linearize-matches-extra`, linearizes all vars used in the arms. + +example: +```rs +λa λb λc match a { 0: b; +: c } + +// Is tranformed to +λa λb λc (match a { 0: λd λ* d; +: λ* λe e } b c) +``` + ## float-combinators Extracts closed terms to new definitions. See [lazy definitions](lazy-definitions#automatic-optimization). diff --git a/src/lib.rs b/src/lib.rs index 968dd4375..ad8811f60 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -141,7 +141,7 @@ pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result, ctx.simplify_matches()?; if opts.linearize_matches.enabled() { - ctx.linearize_matches(opts.linearize_matches.is_extra())?; + ctx.linearize_simple_matches(opts.linearize_matches.is_extra())?; } ctx.book.encode_simple_matches(opts.adt_encoding); @@ -430,10 +430,17 @@ impl CompileOpts { impl CompileOpts { pub fn check(&self, lazy_mode: bool) { - if !self.float_combinators && !lazy_mode { - println!( - "Warning: Running in strict mode without enabling the float_combinators pass can lead to some functions expanding infinitely." - ); + if !lazy_mode { + if !self.float_combinators { + println!( + "Warning: Running in strict mode without enabling the float_combinators pass can lead to some functions expanding infinitely." + ); + } + if !self.linearize_matches.enabled() { + println!( + "Warning: Running in strict mode without enabling the linearize_matches pass can lead to some functions expanding infinitely." + ); + } } } } diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs index dce2dddcc..0c606c334 100644 --- a/src/term/transform/linearize_matches.rs +++ b/src/term/transform/linearize_matches.rs @@ -8,12 +8,12 @@ use std::collections::{BTreeMap, BTreeSet}; impl Ctx<'_> { /// Linearizes the variables between match cases, transforming them into combinators when possible. - pub fn linearize_matches(&mut self, lift_all_vars: bool) -> Result<(), Info> { + pub fn linearize_simple_matches(&mut self, lift_all_vars: bool) -> Result<(), Info> { self.info.start_pass(); for (def_name, def) in self.book.defs.iter_mut() { for rule in def.rules.iter_mut() { - let res = rule.body.linearize_matches(&self.book.ctrs, lift_all_vars); + let res = rule.body.linearize_simple_matches(&self.book.ctrs, lift_all_vars); self.info.take_err(res, Some(def_name)); } } @@ -23,11 +23,11 @@ impl Ctx<'_> { } impl Term { - fn linearize_matches(&mut self, ctrs: &Constructors, lift_all_vars: bool) -> Result<(), MatchErr> { + fn linearize_simple_matches(&mut self, ctrs: &Constructors, lift_all_vars: bool) -> Result<(), MatchErr> { match self { Term::Mat { args: _, rules } => { for rule in rules.iter_mut() { - rule.body.linearize_matches(ctrs, lift_all_vars).unwrap(); + rule.body.linearize_simple_matches(ctrs, lift_all_vars).unwrap(); } let matched_type = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs)?; match matched_type { @@ -39,7 +39,7 @@ impl Term { } Term::Lam { bod, .. } | Term::Chn { bod, .. } => { - bod.linearize_matches(ctrs, lift_all_vars)?; + bod.linearize_simple_matches(ctrs, lift_all_vars)?; } Term::Let { pat: Pattern::Var(..), val: fst, nxt: snd } @@ -48,8 +48,8 @@ impl Term { | Term::Sup { fst, snd, .. } | Term::Opx { fst, snd, .. } | Term::App { fun: fst, arg: snd, .. } => { - fst.linearize_matches(ctrs, lift_all_vars)?; - snd.linearize_matches(ctrs, lift_all_vars)?; + fst.linearize_simple_matches(ctrs, lift_all_vars)?; + snd.linearize_simple_matches(ctrs, lift_all_vars)?; } Term::Lst { .. } => unreachable!(), diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs index 75485016b..6b6b28beb 100644 --- a/tests/golden_tests.rs +++ b/tests/golden_tests.rs @@ -201,7 +201,7 @@ fn simplify_matches() { ctx.check_ctrs_arities()?; ctx.check_unbound_vars()?; ctx.simplify_matches()?; - ctx.linearize_matches(true)?; + ctx.linearize_simple_matches(true)?; ctx.check_unbound_vars()?; ctx.book.make_var_names_unique(); ctx.book.linearize_vars(); @@ -239,7 +239,7 @@ fn encode_pattern_match() { ctx.check_ctrs_arities()?; ctx.check_unbound_vars()?; ctx.simplify_matches()?; - ctx.linearize_matches(true)?; + ctx.linearize_simple_matches(true)?; ctx.book.encode_simple_matches(adt_encoding); ctx.check_unbound_vars()?; ctx.book.make_var_names_unique(); From d80639dcc9b6e9f7d85d807da822c1612165fba0 Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Tue, 27 Feb 2024 11:47:07 -0300 Subject: [PATCH 09/10] Small doc fix --- docs/compiler-options.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/compiler-options.md b/docs/compiler-options.md index bc3e940a2..62b79ecab 100644 --- a/docs/compiler-options.md +++ b/docs/compiler-options.md @@ -138,7 +138,7 @@ main = (bar) ## linearize-matches Linearizes the variables between match cases, transforming them into combinators when possible. -When `linearize-matches` linearizes only vars that are used in more than one arm. +When the `linearize-matches` option is used, linearizes only vars that are used in more than one arm. Example: ```rs @@ -148,7 +148,7 @@ Example: λa λb (match a { 0: λc c; +: λd d } b) ``` -When `linearize-matches-extra`, linearizes all vars used in the arms. +When the `linearize-matches-extra` option is used, linearizes all vars used in the arms. example: ```rs From d992c276702a147939adac7049c7e099dc8d6ba6 Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Tue, 27 Feb 2024 14:05:53 -0300 Subject: [PATCH 10/10] Fix doc tipos --- docs/compiler-options.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/compiler-options.md b/docs/compiler-options.md index 62b79ecab..7ae6f75f7 100644 --- a/docs/compiler-options.md +++ b/docs/compiler-options.md @@ -144,7 +144,7 @@ Example: ```rs λa λb match a { 0: b; +: b } -// Is tranformed to +// Is transformed to λa λb (match a { 0: λc c; +: λd d } b) ``` @@ -154,7 +154,7 @@ example: ```rs λa λb λc match a { 0: b; +: c } -// Is tranformed to +// Is transformed to λa λb λc (match a { 0: λd λ* d; +: λ* λe e } b c) ```