From 39ffe05d721cf7f408d2d63879832a13b3c85321 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Fri, 23 Feb 2024 16:25:56 +0100 Subject: [PATCH 1/4] [sc-301] Add pattern matching on non-zero numbers --- src/lib.rs | 7 +- src/term/builtins.rs | 1 - src/term/check/ctrs_arities.rs | 1 - src/term/check/type_check.rs | 14 +- src/term/check/unbound_pats.rs | 1 - src/term/display.rs | 16 +- src/term/mod.rs | 136 +++++++++----- src/term/net_to_term.rs | 10 +- src/term/parser/parser.rs | 23 ++- src/term/term_to_net.rs | 6 +- .../transform/desugar_implicit_match_binds.rs | 11 +- src/term/transform/encode_pattern_matching.rs | 169 +++++++++++++----- src/term/transform/eta_reduction.rs | 2 +- src/term/transform/linearize_matches.rs | 3 +- src/term/transform/resolve_ctrs_in_pats.rs | 1 - src/term/transform/simplify_matches.rs | 68 +++++-- .../compile_file/match_num_all_patterns.hvm | 20 +-- .../match_num_unscoped_lambda.hvm | 4 +- .../extracted_match_pred.hvm | 2 +- .../compile_file_o_all/linearize_match.hvm | 2 +- .../match_mult_linearization.hvm | 2 +- .../match_num_explicit_bind.hvm | 2 +- .../num_pattern_with_var.hvm | 2 +- .../recursive_combinator_inactive.hvm | 2 +- .../compile_file_o_all/sum_predicates.hvm | 6 +- tests/golden_tests/compile_term/match.hvm | 2 +- .../encode_pattern_match/flatten_era_pat.hvm | 2 +- .../encode_pattern_match/match_bind.hvm | 2 +- .../match_num_adt_tup_parser.hvm | 15 ++ .../encode_pattern_match/match_num_pred.hvm | 18 ++ tests/golden_tests/run_file/bitonic_sort.hvm | 4 +- .../run_file/bitonic_sort_lam.hvm | 4 +- tests/golden_tests/run_file/box.hvm | 2 +- tests/golden_tests/run_file/box2.hvm | 2 +- tests/golden_tests/run_file/def_bool_num.hvm | 2 +- tests/golden_tests/run_file/example.hvm | 2 +- .../run_file/extracted_match_pred.hvm | 2 +- .../golden_tests/run_file/linearize_match.hvm | 2 +- tests/golden_tests/run_file/list_take.hvm | 2 +- tests/golden_tests/run_file/list_to_tree.hvm | 4 +- tests/golden_tests/run_file/match.hvm | 2 +- .../run_file/match_mult_linearization.hvm | 2 +- .../run_file/match_num_adt_tup_parser.hvm | 15 ++ .../run_file/match_num_explicit_bind.hvm | 2 +- .../run_file/match_num_num_to_char.hvm | 36 ++++ .../run_file/match_num_succ_complex.hvm | 16 ++ tests/golden_tests/run_file/match_sup.hvm | 2 +- tests/golden_tests/run_file/merge_sort.hvm | 4 +- tests/golden_tests/run_file/names_hyphen.hvm | 2 +- .../run_file/num_match_missing_var.hvm | 22 +++ tests/golden_tests/run_file/num_pred.hvm | 2 +- tests/golden_tests/run_file/pred.hvm | 2 +- .../golden_tests/run_file/radix_sort_ctr.hvm | 4 +- .../run_file/recursive_combinator_nested.hvm | 2 +- .../run_file/recursive_match_native.hvm | 2 +- tests/golden_tests/run_file/str_inc.hvm | 2 +- tests/golden_tests/run_file/str_inc_eta.hvm | 2 +- tests/golden_tests/run_file/sum_tree.hvm | 2 +- tests/golden_tests/run_file/tuple_rots.hvm | 2 +- tests/golden_tests/run_lazy/bitonic_sort.hvm | 4 +- .../run_lazy/bitonic_sort_lam.hvm | 4 +- tests/golden_tests/run_lazy/box.hvm | 2 +- tests/golden_tests/run_lazy/box2.hvm | 2 +- tests/golden_tests/run_lazy/example.hvm | 2 +- .../run_lazy/extracted_match_pred.hvm | 2 +- .../golden_tests/run_lazy/linearize_match.hvm | 2 +- tests/golden_tests/run_lazy/list_take.hvm | 2 +- tests/golden_tests/run_lazy/list_to_tree.hvm | 4 +- tests/golden_tests/run_lazy/match.hvm | 2 +- .../run_lazy/match_mult_linearization.hvm | 2 +- .../run_lazy/match_num_explicit_bind.hvm | 2 +- tests/golden_tests/run_lazy/merge_sort.hvm | 4 +- tests/golden_tests/run_lazy/num_pred.hvm | 2 +- .../golden_tests/run_lazy/radix_sort_ctr.hvm | 4 +- .../run_lazy/recursive_match_native.hvm | 2 +- tests/golden_tests/run_lazy/str_inc.hvm | 2 +- tests/golden_tests/run_lazy/str_inc_eta.hvm | 2 +- tests/golden_tests/run_lazy/sum_tree.hvm | 2 +- tests/golden_tests/run_lazy/tuple_rots.hvm | 2 +- .../simplify_matches/redundant_with_era.hvm | 2 +- ...pile_file__match_num_all_patterns.hvm.snap | 1 - .../compile_file__missing_pat.hvm.snap | 2 +- ...de_pattern_match__flatten_era_pat.hvm.snap | 4 +- .../encode_pattern_match__match_bind.hvm.snap | 4 +- ...n_match__match_num_adt_tup_parser.hvm.snap | 29 +++ ...ode_pattern_match__match_num_pred.hvm.snap | 25 +++ .../readback_lnet__invalid_mat_mat.hvm.snap | 2 +- tests/snapshots/readback_lnet__match.hvm.snap | 2 +- .../run_file__linearize_match.hvm.snap | 2 +- ...un_file__match_mult_linearization.hvm.snap | 2 +- ...un_file__match_num_adt_tup_parser.hvm.snap | 5 + .../run_file__match_num_num_to_char.hvm.snap | 5 + .../run_file__match_num_succ_complex.hvm.snap | 5 + .../run_file__multi_num_match.hvm.snap | 5 + .../run_file__num_match_missing_var.hvm.snap | 9 + .../run_lazy__linearize_match.hvm.snap | 2 +- ...un_lazy__match_mult_linearization.hvm.snap | 2 +- ...fy_matches__flatten_with_terminal.hvm.snap | 2 +- ...plify_matches__redundant_with_era.hvm.snap | 2 +- 99 files changed, 627 insertions(+), 234 deletions(-) create mode 100644 tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm create mode 100644 tests/golden_tests/encode_pattern_match/match_num_pred.hvm create mode 100644 tests/golden_tests/run_file/match_num_adt_tup_parser.hvm create mode 100644 tests/golden_tests/run_file/match_num_num_to_char.hvm create mode 100644 tests/golden_tests/run_file/match_num_succ_complex.hvm create mode 100644 tests/golden_tests/run_file/num_match_missing_var.hvm create mode 100644 tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap create mode 100644 tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap create mode 100644 tests/snapshots/run_file__match_num_adt_tup_parser.hvm.snap create mode 100644 tests/snapshots/run_file__match_num_num_to_char.hvm.snap create mode 100644 tests/snapshots/run_file__match_num_succ_complex.hvm.snap create mode 100644 tests/snapshots/run_file__multi_num_match.hvm.snap create mode 100644 tests/snapshots/run_file__num_match_missing_var.hvm.snap diff --git a/src/lib.rs b/src/lib.rs index ad8811f60..fff01d99f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -80,11 +80,8 @@ pub fn create_host(book: Arc, labels: Arc, compile_opts: CompileOp term.resugar_builtins(); readback_errors.extend(resugar_errs); - match term { - Term::Str { val } => { - println!("{}", val); - } - _ => (), + if let Term::Str { val } = term { + println!("{val}"); } } }))), diff --git a/src/term/builtins.rs b/src/term/builtins.rs index 1e073d9da..751aaaed0 100644 --- a/src/term/builtins.rs +++ b/src/term/builtins.rs @@ -90,7 +90,6 @@ impl Pattern { snd.encode_builtins(); } Pattern::Var(..) | Pattern::Num(..) => {} - Pattern::Err => unreachable!(), } } diff --git a/src/term/check/ctrs_arities.rs b/src/term/check/ctrs_arities.rs index 8b0e312cd..ecbd327f4 100644 --- a/src/term/check/ctrs_arities.rs +++ b/src/term/check/ctrs_arities.rs @@ -67,7 +67,6 @@ impl Pattern { } } Pattern::Var(..) | Pattern::Num(..) => {} - Pattern::Err => unreachable!(), } } Ok(()) diff --git a/src/term/check/type_check.rs b/src/term/check/type_check.rs index d18ee3e25..945750401 100644 --- a/src/term/check/type_check.rs +++ b/src/term/check/type_check.rs @@ -1,8 +1,12 @@ -use crate::term::{transform::encode_pattern_matching::MatchErr, Constructors, Name, Pattern, Type}; +use crate::term::{transform::encode_pattern_matching::MatchErr, Constructors, Name, Pattern, Rule, Type}; use indexmap::IndexMap; pub type DefinitionTypes = IndexMap>; +pub fn infer_match_arg_type(rules: &[Rule], arg_idx: usize, ctrs: &Constructors) -> Result { + infer_type(rules.iter().map(|r| &r.pats[arg_idx]), ctrs) +} + /// Infers the type of a sequence of arguments pub fn infer_type<'a>( pats: impl IntoIterator, @@ -19,9 +23,17 @@ fn unify(old: Type, new: Type) -> Result { match (old, new) { (Type::Any, new) => Ok(new), (old, Type::Any) => Ok(old), + (Type::Adt(old), Type::Adt(new)) if new == old => Ok(Type::Adt(old)), + (Type::Num, Type::Num) => Ok(Type::Num), + (Type::Num, Type::NumSucc(n)) => Ok(Type::NumSucc(n)), + + (Type::NumSucc(n), Type::Num) => Ok(Type::NumSucc(n)), + (Type::NumSucc(a), Type::NumSucc(b)) if a == b => Ok(Type::NumSucc(a)), + (Type::Tup, Type::Tup) => Ok(Type::Tup), + (old, new) => Err(MatchErr::TypeMismatch(new, old)), } } diff --git a/src/term/check/unbound_pats.rs b/src/term/check/unbound_pats.rs index 8ea279eb9..53e599fc7 100644 --- a/src/term/check/unbound_pats.rs +++ b/src/term/check/unbound_pats.rs @@ -59,7 +59,6 @@ impl Pattern { } Pattern::Lst(args) => args.iter().for_each(|arg| check.push(arg)), Pattern::Var(_) | Pattern::Num(_) => {} - Pattern::Err => unreachable!(), } } unbounds diff --git a/src/term/display.rs b/src/term/display.rs index 2156c5682..8071542ef 100644 --- a/src/term/display.rs +++ b/src/term/display.rs @@ -1,6 +1,4 @@ -use super::{ - net_to_term::ReadbackError, Book, Definition, MatchNum, Name, Op, Pattern, Rule, Tag, Term, Type, -}; +use super::{net_to_term::ReadbackError, Book, Definition, Name, NumCtr, Op, Pattern, Rule, Tag, Term, Type}; use std::{fmt, ops::Deref}; /* Some aux structures for things that are not so simple to display */ @@ -113,7 +111,6 @@ impl fmt::Display for Pattern { Pattern::Num(num) => write!(f, "{num}"), Pattern::Tup(fst, snd) => write!(f, "({}, {})", fst, snd,), Pattern::Lst(pats) => write!(f, "[{}]", DisplayJoin(|| pats, ", ")), - Pattern::Err => write!(f, ""), } } } @@ -141,13 +138,13 @@ impl fmt::Display for Book { } } -impl fmt::Display for MatchNum { +impl fmt::Display for NumCtr { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - MatchNum::Zero => write!(f, "0"), - MatchNum::Succ(None) => write!(f, "+"), - MatchNum::Succ(Some(None)) => write!(f, "+*"), - MatchNum::Succ(Some(Some(nam))) => write!(f, "+{nam}"), + NumCtr::Num(n) => write!(f, "{n}"), + NumCtr::Succ(n, None) => write!(f, "{n}+"), + NumCtr::Succ(n, Some(None)) => write!(f, "{n}+*"), + NumCtr::Succ(n, Some(Some(nam))) => write!(f, "{n}+{nam}"), } } } @@ -188,6 +185,7 @@ impl fmt::Display for Type { Type::Any => write!(f, "any"), Type::Tup => write!(f, "tup"), Type::Num => write!(f, "num"), + Type::NumSucc(n) => write!(f, "{n}+"), Type::Adt(nam) => write!(f, "{nam}"), } } diff --git a/src/term/mod.rs b/src/term/mod.rs index 1d76cba23..9dc6dd9d7 100644 --- a/src/term/mod.rs +++ b/src/term/mod.rs @@ -1,9 +1,13 @@ -use self::{check::type_check::infer_type, parser::lexer::STRINGS}; +use self::{check::type_check::infer_match_arg_type, parser::lexer::STRINGS}; use crate::{diagnostics::Info, term::builtins::*, ENTRY_POINT}; use indexmap::{IndexMap, IndexSet}; use interner::global::GlobalString; use itertools::Itertools; -use std::{borrow::Cow, collections::HashMap, ops::Deref}; +use std::{ + borrow::Cow, + collections::{HashMap, HashSet}, + ops::Deref, +}; pub mod builtins; pub mod check; @@ -136,21 +140,19 @@ pub enum Term { Err, } -#[derive(Debug, Clone, PartialEq, Eq, Hash, Default)] +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Pattern { Var(Option), Ctr(Name, Vec), - Num(MatchNum), + Num(NumCtr), Tup(Box, Box), Lst(Vec), - #[default] - Err, } #[derive(Debug, Clone, PartialEq, Eq, Hash)] -pub enum MatchNum { - Zero, - Succ(Option>), +pub enum NumCtr { + Num(u64), + Succ(u64, Option>), } #[derive(Debug, Clone, PartialEq, Eq, Hash)] @@ -185,9 +187,15 @@ pub enum Op { /// Pattern types. #[derive(Debug, Clone, PartialEq, Eq)] pub enum Type { + /// Variables/wildcards. Any, + /// A native tuple. Tup, + /// A sequence of arbitrary numbers ending in a variable. Num, + /// A strictly incrementing sequence of numbers starting from 0, ending in a + ctr. + NumSucc(u64), + /// Adt constructors declared with the `data` syntax. Adt(Name), } @@ -239,6 +247,7 @@ impl Tag { } impl Term { + /* Common construction patterns */ pub fn lam(nam: Option, bod: Term) -> Self { Term::Lam { tag: Tag::Static, nam, bod: Box::new(bod) } } @@ -289,6 +298,30 @@ impl Term { Term::Str { val: STRINGS.get(str) } } + pub fn native_num_match(arg: Term, zero: Term, succ: Term) -> Term { + let zero = Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: zero }; + let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, None))], body: succ }; + Term::Mat { args: vec![arg], rules: vec![zero, succ] } + } + + pub fn sub_num(arg: Term, val: u64) -> Term { + if val == 0 { + arg + } else { + Term::Opx { op: Op::SUB, fst: Box::new(arg), snd: Box::new(Term::Num { val }) } + } + } + + pub fn add_num(arg: Term, val: u64) -> Term { + if val == 0 { + arg + } else { + Term::Opx { op: Op::ADD, fst: Box::new(arg), snd: Box::new(Term::Num { val }) } + } + } + + /* Common checks and transformations */ + /// Substitute the occurrences of a variable in a term with the given term. /// Caution: can cause invalid shadowing of variables if used incorrectly. /// Ex: Using subst to beta-reduce (@a @b a b) converting it into (@b b). @@ -507,7 +540,7 @@ impl Term { return false; } // The match is over a valid type - let Ok(typ) = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs) else { + let Ok(typ) = infer_match_arg_type(rules, 0, ctrs) else { return false; }; // The match has one arm for each constructor, matching the constructors in adt declaration order @@ -529,14 +562,32 @@ impl Term { } } Type::Num => { - if rules.len() != 2 { - return false; + let mut nums = HashSet::new(); + for rule in rules { + if let Pattern::Num(NumCtr::Num(n)) = &rule.pats[0] { + if nums.contains(n) { + return false; + } + nums.insert(*n); + } } - if !matches!(rules[0].pats[0], Pattern::Num(MatchNum::Zero)) { + } + Type::NumSucc(n) => { + if rules.len() as u64 != n + 1 { return false; } - if !matches!(rules[1].pats[0], Pattern::Num(MatchNum::Succ(Some(_)))) { - return false; + for (i, _) in rules.iter().enumerate() { + if i as u64 == n { + let Pattern::Num(NumCtr::Succ(n_pat, Some(_))) = &rules[i].pats[0] else { return false }; + if n != *n_pat { + return false; + } + } else { + let Pattern::Num(NumCtr::Num(i_pat)) = &rules[i].pats[0] else { return false }; + if i as u64 != *i_pat { + return false; + } + } } } Type::Adt(adt) => { @@ -570,7 +621,7 @@ impl Pattern { pub fn bind_or_eras(&self) -> impl DoubleEndedIterator> { self.iter().filter_map(|pat| match pat { Pattern::Var(nam) => Some(nam), - Pattern::Num(MatchNum::Succ(nam)) => nam.as_ref(), + Pattern::Num(NumCtr::Succ(_, nam)) => nam.as_ref(), _ => None, }) } @@ -585,11 +636,10 @@ impl Pattern { go(fst, set); go(snd, set); } - Pattern::Num(MatchNum::Succ(Some(nam))) => { + Pattern::Num(NumCtr::Succ(_, Some(nam))) => { set.push(nam); } Pattern::Num(_) => {} - Pattern::Err => unreachable!(), } } let mut set = Vec::new(); @@ -614,7 +664,6 @@ impl Pattern { Pattern::Num(_) => Box::new([].iter()), Pattern::Tup(fst, snd) => Box::new([fst.as_ref(), snd.as_ref()].into_iter()), Pattern::Lst(els) => Box::new(els.iter()), - Pattern::Err => unreachable!(), } } @@ -634,11 +683,10 @@ impl Pattern { match self { Pattern::Var(_) => None, Pattern::Ctr(nam, _) => Some(nam.clone()), - Pattern::Num(MatchNum::Zero) => Some(Name::new("0")), - Pattern::Num(MatchNum::Succ(_)) => Some(Name::new("+")), + Pattern::Num(NumCtr::Num(num)) => Some(Name::new(format!("{num}"))), + Pattern::Num(NumCtr::Succ(num, _)) => Some(Name::new(format!("{num}+"))), Pattern::Tup(_, _) => Some(Name::new("(,)")), Pattern::Lst(_) => todo!(), - Pattern::Err => unreachable!(), } } @@ -646,12 +694,13 @@ impl Pattern { matches!(self, Pattern::Var(_)) } - pub fn is_detached_num_match(&self) -> bool { - if let Pattern::Num(num) = self { - match num { - MatchNum::Zero => true, - MatchNum::Succ(None) => true, - MatchNum::Succ(Some(_)) => false, + pub fn is_native_num_match(&self) -> bool { + if let Pattern::Num(ctr) = self { + match ctr { + NumCtr::Num(0) => true, + NumCtr::Num(_) => false, + NumCtr::Succ(1, None) => true, + NumCtr::Succ(_, _) => false, } } else { false @@ -667,7 +716,6 @@ impl Pattern { Pattern::Tup(fst, snd) => { matches!(fst.as_ref(), Pattern::Var(_)) && matches!(snd.as_ref(), Pattern::Var(_)) } - Pattern::Err => unreachable!(), } } @@ -679,9 +727,9 @@ impl Pattern { Type::Adt(adt_nam.clone()) } Pattern::Tup(..) => Type::Tup, - Pattern::Num(..) => Type::Num, + Pattern::Num(NumCtr::Num(_)) => Type::Num, + Pattern::Num(NumCtr::Succ(n, _)) => Type::NumSucc(*n), Pattern::Lst(..) => Type::Adt(builtins::LIST.into()), - Pattern::Err => unreachable!(), } } @@ -691,22 +739,17 @@ impl Pattern { Pattern::Ctr(ctr, args) => { Term::call(Term::Ref { nam: ctr.clone() }, args.iter().map(|arg| arg.to_term())) } - Pattern::Num(MatchNum::Zero) => Term::Num { val: 0 }, + Pattern::Num(NumCtr::Num(val)) => Term::Num { val: *val }, // Succ constructor with no variable is not a valid term, only a compiler intermediate for a MAT inet node. - Pattern::Num(MatchNum::Succ(None)) => unreachable!(), - Pattern::Num(MatchNum::Succ(Some(Some(nam)))) => Term::Opx { - op: Op::ADD, - fst: Box::new(Term::Var { nam: nam.clone() }), - snd: Box::new(Term::Num { val: 1 }), - }, - Pattern::Num(MatchNum::Succ(Some(None))) => Term::Era, + Pattern::Num(NumCtr::Succ(_, None)) => unreachable!(), + Pattern::Num(NumCtr::Succ(val, Some(Some(nam)))) => Term::add_num(Term::Var { nam: nam.clone() }, *val), + Pattern::Num(NumCtr::Succ(_, Some(None))) => Term::Era, Pattern::Tup(fst, snd) => Term::Tup { fst: Box::new(fst.to_term()), snd: Box::new(snd.to_term()) }, Pattern::Lst(_) => { let mut p = self.clone(); p.encode_builtins(); p.to_term() } - Pattern::Err => unreachable!(), } } @@ -714,8 +757,10 @@ impl Pattern { pub fn simple_equals(&self, other: &Pattern) -> bool { match (self, other) { (Pattern::Ctr(a, _), Pattern::Ctr(b, _)) if a == b => true, - (Pattern::Num(MatchNum::Zero), Pattern::Num(MatchNum::Zero)) => true, - (Pattern::Num(MatchNum::Succ(_)), Pattern::Num(MatchNum::Succ(_))) => true, + (Pattern::Num(NumCtr::Num(a)), Pattern::Num(NumCtr::Num(b))) if a == b => true, + (Pattern::Num(NumCtr::Num(_)), Pattern::Num(NumCtr::Num(_))) => false, + (Pattern::Num(NumCtr::Succ(a, _)), Pattern::Num(NumCtr::Succ(b, _))) if a == b => true, + (Pattern::Num(NumCtr::Succ(_, _)), Pattern::Num(NumCtr::Succ(_, _))) => false, (Pattern::Tup(_, _), Pattern::Tup(_, _)) => true, (Pattern::Lst(_), Pattern::Lst(_)) => true, (Pattern::Var(_), Pattern::Var(_)) => true, @@ -774,9 +819,12 @@ impl Type { Box::new(Pattern::Var(Some("%fst".into()))), Box::new(Pattern::Var(Some("%snd".into()))), )], - Type::Num => { - vec![Pattern::Num(MatchNum::Zero), Pattern::Num(MatchNum::Succ(Some(Some("%pred".into()))))] + Type::NumSucc(n) => { + let mut ctrs = (0 .. *n).map(|n| Pattern::Num(NumCtr::Num(n))).collect::>(); + ctrs.push(Pattern::Num(NumCtr::Succ(*n, Some(Some("%pred".into()))))); + ctrs } + Type::Num => unreachable!(), Type::Adt(adt) => { // TODO: Should return just a ref to ctrs and not clone. adts[adt] diff --git a/src/term/net_to_term.rs b/src/term/net_to_term.rs index f8abfd8fc..3fbab7780 100644 --- a/src/term/net_to_term.rs +++ b/src/term/net_to_term.rs @@ -1,7 +1,7 @@ use super::Rule; use crate::{ net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT}, - term::{num_to_name, term_to_net::Labels, Book, MatchNum, Name, Op, Pattern, Tag, Term}, + term::{num_to_name, term_to_net::Labels, Book, Name, NumCtr, Op, Pattern, Tag, Term}, }; use std::collections::{BTreeSet, HashMap, HashSet}; @@ -396,7 +396,7 @@ impl Term { /// Creates a new [`Term::Match`] from the given terms. /// If `scrutinee` is not a `Term::Var`, creates a let binding containing the match in its body fn new_native_match(arg: Self, zero_term: Self, mut succ_label: Option, mut succ_term: Self) -> Self { - let zero = Rule { pats: vec![Pattern::Num(MatchNum::Zero)], body: zero_term }; + let zero = Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: zero_term }; if let Term::Var { nam } = &arg { if let Some(label) = &succ_label { @@ -405,7 +405,7 @@ impl Term { succ_label = Some(new_label); } - let succ = Rule { pats: vec![Pattern::Num(MatchNum::Succ(Some(succ_label)))], body: succ_term }; + let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, Some(succ_label)))], body: succ_term }; Term::Mat { args: vec![arg], rules: vec![zero, succ] } } else { match succ_label { @@ -416,7 +416,7 @@ impl Term { succ_term.subst(&succ, &Term::Var { nam: new_label.clone() }); succ_label = Some(new_label); - let succ = Rule { pats: vec![Pattern::Num(MatchNum::Succ(Some(succ_label)))], body: succ_term }; + let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, Some(succ_label)))], body: succ_term }; Term::Let { pat: Pattern::Var(Some(match_bind.clone())), @@ -425,7 +425,7 @@ impl Term { } } None => { - let succ = Rule { pats: vec![Pattern::Num(MatchNum::Succ(None))], body: succ_term }; + let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, None))], body: succ_term }; Term::Mat { args: vec![arg], rules: vec![zero, succ] } } diff --git a/src/term/parser/parser.rs b/src/term/parser/parser.rs index 77e3a5600..31fba38cc 100644 --- a/src/term/parser/parser.rs +++ b/src/term/parser/parser.rs @@ -1,6 +1,6 @@ use crate::term::{ parser::lexer::{LexingError, Token}, - Adt, Book, Definition, MatchNum, Name, Op, Pattern, Rule, Tag, Term, + Adt, Book, Definition, Name, NumCtr, Op, Pattern, Rule, Tag, Term, }; use chumsky::{ error::{Error, RichReason}, @@ -405,15 +405,24 @@ where .map(Pattern::Lst) .boxed(); - let zero = any().filter(|t| matches!(t, Token::Num(0))).to(Pattern::Num(MatchNum::Zero)).labelled("0"); + let num = any() + .filter(|t| matches!(t, Token::Num(_))) + .map(|t| { + let Token::Num(n) = t else { unreachable!() }; + n + }) + .labelled(""); + + let num_ctr = num.map(|n| Pattern::Num(NumCtr::Num(n))); - let succ = just(Token::Add) - .ignore_then(name_or_era().or_not()) - .map(|nam| Pattern::Num(MatchNum::Succ(nam))) - .labelled("+") + let succ_ctr = num + .then_ignore(just(Token::Add)) + .then(name_or_era().or_not()) + .map(|(num, nam)| Pattern::Num(NumCtr::Succ(num, nam))) + .labelled("+") .boxed(); - choice((zero, succ, var, ctr, list, tup)) + choice((succ_ctr, num_ctr, var, ctr, list, tup)) }) } diff --git a/src/term/term_to_net.rs b/src/term/term_to_net.rs index 826058af8..cac2bf3ae 100644 --- a/src/term/term_to_net.rs +++ b/src/term/term_to_net.rs @@ -1,6 +1,6 @@ use crate::{ net::{INet, NodeKind::*, Port, ROOT}, - term::{Book, MatchNum, Name, Op, Pattern, Tag, Term}, + term::{Book, Name, NumCtr, Op, Pattern, Tag, Term}, }; use std::collections::{hash_map::Entry, HashMap}; @@ -108,8 +108,8 @@ impl<'a> EncodeTermState<'a> { Term::Mat { args, rules } => { // At this point should be only simple num matches. let arg = args.iter().next().unwrap(); - debug_assert!(matches!(rules[0].pats[..], [Pattern::Num(MatchNum::Zero)])); - debug_assert!(matches!(rules[1].pats[..], [Pattern::Num(MatchNum::Succ(None))])); + debug_assert!(matches!(rules[0].pats[..], [Pattern::Num(NumCtr::Num(0))])); + debug_assert!(matches!(rules[1].pats[..], [Pattern::Num(NumCtr::Succ(1, None))])); let if_ = self.inet.new_node(Mat); diff --git a/src/term/transform/desugar_implicit_match_binds.rs b/src/term/transform/desugar_implicit_match_binds.rs index 8d28945a4..9d6d929be 100644 --- a/src/term/transform/desugar_implicit_match_binds.rs +++ b/src/term/transform/desugar_implicit_match_binds.rs @@ -1,4 +1,4 @@ -use crate::term::{Adts, Book, Constructors, MatchNum, Name, Pattern, Term}; +use crate::term::{Adts, Book, Constructors, Name, NumCtr, Pattern, Term}; impl Book { pub fn desugar_implicit_match_binds(&mut self) { @@ -45,15 +45,14 @@ impl Term { .collect(); } } - Pattern::Num(MatchNum::Zero) => (), - Pattern::Num(MatchNum::Succ(Some(_))) => (), - Pattern::Num(MatchNum::Succ(p @ None)) => { + Pattern::Num(NumCtr::Num(_)) => (), + Pattern::Num(NumCtr::Succ(_, Some(_))) => (), + Pattern::Num(NumCtr::Succ(n, p @ None)) => { // Implicit num arg - *p = Some(Some(Name::new(format!("{nam}-1")))); + *p = Some(Some(Name::new(format!("{nam}-{n}")))); } Pattern::Tup(_, _) => (), Pattern::Lst(..) => unreachable!(), - Pattern::Err => unreachable!(), } } } diff --git a/src/term/transform/encode_pattern_matching.rs b/src/term/transform/encode_pattern_matching.rs index 4288082ca..bd386dd00 100644 --- a/src/term/transform/encode_pattern_matching.rs +++ b/src/term/transform/encode_pattern_matching.rs @@ -5,8 +5,8 @@ use itertools::Itertools; use crate::{ diagnostics::ERR_INDENT_SIZE, term::{ - check::type_check::infer_type, display::DisplayFn, AdtEncoding, Adts, Book, Constructors, MatchNum, Name, - Pattern, Rule, Tag, Term, Type, + check::type_check::infer_match_arg_type, display::DisplayFn, AdtEncoding, Adts, Book, Constructors, Name, + NumCtr, Pattern, Rule, Tag, Term, Type, }, }; @@ -63,52 +63,135 @@ fn encode_match( adts: &Adts, adt_encoding: AdtEncoding, ) -> Term { - let typ = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs).unwrap(); + let typ = infer_match_arg_type(&rules, 0, ctrs).unwrap(); match typ { - // Just move the match into a let term Type::Any | Type::Tup => { - let rule = rules.into_iter().next().unwrap(); - Term::Let { pat: rule.pats.into_iter().next().unwrap(), val: Box::new(arg), nxt: Box::new(rule.body) } - } - // Detach the variable from the match, converting into a native num match - Type::Num => { - let mut rules = rules; - let Pattern::Num(MatchNum::Succ(Some(var))) = - std::mem::replace(&mut rules[1].pats[0], Pattern::Num(MatchNum::Succ(None))) - else { - unreachable!() - }; - rules[1].body = Term::lam(var, std::mem::take(&mut rules[1].body)); - Term::Mat { args: vec![arg], rules } + let fst_rule = rules.into_iter().next().unwrap(); + encode_var(arg, fst_rule) } + Type::NumSucc(_) => encode_num_succ(arg, rules), + Type::Num => encode_num(arg, rules), // ADT Encoding depends on compiler option - Type::Adt(adt) => { - match adt_encoding { - // (x @field1 @field2 ... body1 @field1 body2 ...) - AdtEncoding::Scott => { - let mut arms = vec![]; - for rule in rules { - let body = rule.body; - let body = rule.pats[0].binds().rev().fold(body, |bod, nam| Term::named_lam(nam.clone(), bod)); - arms.push(body); - } - Term::call(arg, arms) - } - // #adt_name(x arm[0] arm[1] ...) - AdtEncoding::TaggedScott => { - let mut arms = vec![]; - for (rule, (ctr, fields)) in rules.into_iter().zip(&adts[&adt].ctrs) { - let body = - rule.pats[0].binds().rev().zip(fields.iter().rev()).fold(rule.body, |bod, (var, field)| { - Term::tagged_lam(Tag::adt_field(&adt, ctr, field), var.clone(), bod) - }); - arms.push(body); - } - Term::tagged_call(Tag::adt_name(&adt), arg, arms) - } + Type::Adt(adt) => encode_adt(arg, rules, adt, adt_encoding, adts), + } +} + +/// Just move the match into a let term +fn encode_var(arg: Term, rule: Rule) -> Term { + Term::Let { pat: rule.pats.into_iter().next().unwrap(), val: Box::new(arg), nxt: Box::new(rule.body) } +} + +/// Convert into a sequence of native matches, decrementing by 1 each match. +/// match n {0: A; 1: B; 2+: (C n-2)} converted to +/// match n {0: A; 1+: @%x match %x {0: B; 1+: @n-2 (C n-2)}} +fn encode_num_succ(arg: Term, mut rules: Vec) -> Term { + let last_rule = rules.pop().unwrap(); + + let match_var = Name::from("%x"); + + // @n-2 (C n-2) + let Pattern::Num(NumCtr::Succ(_, Some(last_var))) = last_rule.pats.into_iter().next().unwrap() else { + unreachable!() + }; + let last_arm = Term::lam(last_var, last_rule.body); + + rules.into_iter().rev().fold(last_arm, |term, rule| { + let rules = vec![Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: rule.body }, Rule { + pats: vec![Pattern::Num(NumCtr::Succ(1, None))], + body: term, + }]; + + let Pattern::Num(NumCtr::Num(num)) = rule.pats.into_iter().next().unwrap() else { unreachable!() }; + if num == 0 { + Term::Mat { args: vec![arg.clone()], rules } + } else { + let mat = Term::Mat { args: vec![Term::Var { nam: match_var.clone() }], rules }; + Term::named_lam(match_var.clone(), mat) + } + }) +} + +/// Convert into a sequence of native matches on (- n num_case) +/// match n {a: A; b: B; n: (C n)} converted to +/// match (- n a) {0: A; 1+: @%p match (- %p b-a-1) { 0: B; 1+: @%p let n = (+ %p b+1); (C n)}} +fn encode_num(arg: Term, mut rules: Vec) -> Term { + fn go( + mut rules: impl Iterator, + last_rule: Rule, + prev_num: Option, + arg: Option, + ) -> Term { + let rule = rules.next(); + match (prev_num, rule) { + // Num matches must have at least 2 rules (1 num and 1 var). + // The first rule can't also be the last. + (None, None) => unreachable!(), + // First match + // match (- n a) {0: A; 1+: ...} + (None, Some(rule)) => { + let Pattern::Num(NumCtr::Num(val)) = &rule.pats[0] else { unreachable!() }; + Term::native_num_match( + Term::sub_num(arg.unwrap(), *val), + rule.body, + go(rules, last_rule, Some(*val), None), + ) + } + // Middle match + // @%p match (- %p b-a-1) { 0: B; 1+: ... } + (Some(prev_num), Some(rule)) => { + let Pattern::Num(NumCtr::Num(val)) = &rule.pats[0] else { unreachable!() }; + let pred_nam = Name::from("%p"); + Term::named_lam( + pred_nam.clone(), + Term::native_num_match( + Term::sub_num(Term::Var { nam: pred_nam }, val.wrapping_sub(prev_num).wrapping_sub(1)), + rule.body, + go(rules, last_rule, Some(*val), None), + ), + ) + } + // Last match + // @%p let n = (+ %p b+1); (C n) + (Some(prev_num), None) => { + let pred_nam = Name::from("%p"); + Term::named_lam(pred_nam.clone(), Term::Let { + pat: last_rule.pats.into_iter().next().unwrap(), + val: Box::new(Term::add_num(Term::Var { nam: pred_nam }, prev_num.wrapping_add(1))), + nxt: Box::new(last_rule.body), + }) } } } + + let last_rule = rules.pop().unwrap(); + go(rules.into_iter(), last_rule, None, Some(arg)) +} + +fn encode_adt(arg: Term, rules: Vec, adt: Name, adt_encoding: AdtEncoding, adts: &Adts) -> Term { + match adt_encoding { + // (x @field1 @field2 ... body1 @field1 body2 ...) + AdtEncoding::Scott => { + let mut arms = vec![]; + for rule in rules { + let body = rule.body; + let body = rule.pats[0].binds().rev().fold(body, |bod, nam| Term::named_lam(nam.clone(), bod)); + arms.push(body); + } + Term::call(arg, arms) + } + // #adt_name(x arm[0] arm[1] ...) + AdtEncoding::TaggedScott => { + let mut arms = vec![]; + for (rule, (ctr, fields)) in rules.into_iter().zip(&adts[&adt].ctrs) { + let body = + rule.pats[0].binds().rev().zip(fields.iter().rev()).fold(rule.body, |bod, (var, field)| { + Term::tagged_lam(Tag::adt_field(&adt, ctr, field), var.clone(), bod) + }); + arms.push(body); + } + Term::tagged_call(Tag::adt_name(&adt), arg, arms) + } + } } #[derive(Debug, Clone)] @@ -120,6 +203,7 @@ pub enum MatchErr { TypeMismatch(Type, Type), ArityMismatch(usize, usize), CtrArityMismatch(Name, usize, usize), + MalformedNumSucc(Pattern, Pattern), } #[derive(Debug, Clone)] @@ -155,6 +239,9 @@ impl MatchErr { f, "Constructor arity mismatch in pattern matching. Constructor '{ctr}' expects {exp} fields, found {got}." ), + MatchErr::MalformedNumSucc(got, exp) => { + write!(f, "Expected a sequence of incrementing numbers ending with '{exp}', found '{got}'.") + } }) } } diff --git a/src/term/transform/eta_reduction.rs b/src/term/transform/eta_reduction.rs index ec10d9577..aa0b9e11b 100644 --- a/src/term/transform/eta_reduction.rs +++ b/src/term/transform/eta_reduction.rs @@ -55,7 +55,7 @@ impl Term { } for rule in rules { for pat in &rule.pats { - debug_assert!(pat.is_detached_num_match()); + debug_assert!(pat.is_native_num_match()); } rule.body.eta_reduction(); } diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs index 0c606c334..70c3e988a 100644 --- a/src/term/transform/linearize_matches.rs +++ b/src/term/transform/linearize_matches.rs @@ -1,7 +1,7 @@ use super::encode_pattern_matching::MatchErr; use crate::{ diagnostics::Info, - term::{check::type_check::infer_type, Constructors, Ctx, Name, Pattern, Term, Type}, + term::{Ctx, Name, Pattern, Term}, }; use itertools::Itertools; use std::collections::{BTreeMap, BTreeSet}; @@ -36,6 +36,7 @@ impl Term { lift_match_vars(self, lift_all_vars); } } + linearize_match_free_vars(self); } Term::Lam { bod, .. } | Term::Chn { bod, .. } => { diff --git a/src/term/transform/resolve_ctrs_in_pats.rs b/src/term/transform/resolve_ctrs_in_pats.rs index 09e101a9f..7ba73650f 100644 --- a/src/term/transform/resolve_ctrs_in_pats.rs +++ b/src/term/transform/resolve_ctrs_in_pats.rs @@ -40,7 +40,6 @@ impl Pattern { to_resolve.push(fst); to_resolve.push(snd); } - Pattern::Err => unreachable!(), } } } diff --git a/src/term/transform/simplify_matches.rs b/src/term/transform/simplify_matches.rs index 86d5829fd..d8b53451c 100644 --- a/src/term/transform/simplify_matches.rs +++ b/src/term/transform/simplify_matches.rs @@ -1,11 +1,12 @@ +use indexmap::IndexSet; use itertools::Itertools; use crate::{ diagnostics::Info, term::{ - check::type_check::infer_type, + check::type_check::infer_match_arg_type, transform::encode_pattern_matching::{ExhaustivenessErr, MatchErr}, - Adts, Constructors, Ctx, Definition, MatchNum, Name, Pattern, Rule, Term, Type, + Adts, Constructors, Ctx, Definition, Name, NumCtr, Pattern, Rule, Term, Type, }, }; @@ -101,16 +102,15 @@ fn simplify_match_expression( ctrs: &Constructors, adts: &Adts, ) -> Result { - let fst_row_irrefutable = matches!(infer_type(&rules[0].pats, ctrs), Ok(Type::Any)); - let fst_col_type = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs)?; + let fst_row_irrefutable = rules[0].pats.iter().all(|p| p.is_wildcard()); + let fst_col_type = infer_match_arg_type(rules, 0, ctrs)?; if fst_row_irrefutable { irrefutable_fst_row_rule(args, rules, ctrs, adts) } else if fst_col_type == Type::Any { var_rule(args, rules, ctrs, adts) } else { - let adt_ctrs = fst_col_type.ctrs(adts); - switch_rule(args, rules, adt_ctrs, ctrs, adts) + switch_rule(args, rules, fst_col_type, ctrs, adts) } } @@ -202,22 +202,63 @@ fn var_rule(args: &[Term], rules: &[Rule], ctrs: &Constructors, adts: &Adts) -> fn switch_rule( args: &[Term], rules: &[Rule], - adt_ctrs: Vec, + typ: Type, ctrs: &Constructors, adts: &Adts, ) -> Result { let mut new_rules = vec![]; + + let adt_ctrs = match typ { + Type::Num => { + // Since numbers have infinite (2^60) constructors, they require special treatment. + let mut ctrs = IndexSet::new(); + for rule in rules { + ctrs.insert(rule.pats[0].clone()); + if rule.pats[0].is_wildcard() { + break; + } + } + + Vec::from_iter(ctrs) + } + _ => typ.ctrs(adts), + }; + + // Check valid number match + match typ { + Type::Num => { + // Number match without + must have a default case + if !rules.iter().any(|r| r.pats[0].is_wildcard()) { + return Err(MatchErr::NotExhaustive(ExhaustivenessErr(vec![Name::from("+")]))); + } + } + Type::NumSucc(exp) => { + // Number match with + can't have number larger than that in the + + // TODO: could be just a warning. + for rule in rules { + if let Pattern::Num(NumCtr::Num(got)) = rule.pats[0] + && got >= exp + { + return Err(MatchErr::MalformedNumSucc( + rule.pats[0].clone(), + Pattern::Num(NumCtr::Succ(exp, None)), + )); + } + } + } + _ => (), + } + for ctr in adt_ctrs { // Create the matched constructor and the name of the bound variables. let Term::Var { nam: arg_nam } = &args[0] else { unreachable!() }; let nested_fields = switch_rule_nested_fields(arg_nam, &ctr); - let matched_ctr = switch_rule_matched_ctr(ctr, &nested_fields); + let matched_ctr = switch_rule_matched_ctr(ctr.clone(), &nested_fields); let mut body = switch_rule_submatch(args, rules, &matched_ctr, &nested_fields)?; body.simplify_matches(ctrs, adts)?; let pats = vec![matched_ctr]; new_rules.push(Rule { pats, body }); } - let term = Term::Mat { args: vec![args[0].clone()], rules: new_rules }; Ok(term) } @@ -281,11 +322,12 @@ fn switch_rule_submatch_arm(rule: &Rule, ctr: &Pattern, nested_fields: &[Option< // match x ... {(Ctr p0_0...) ...: Body; ...} // becomes // match x {(Ctr x%field0 ...): match x1 ... {p0_0 ...: Body; ...}; ...} - let mut pats = if let Pattern::Num(MatchNum::Succ(Some(var))) = &rule.pats[0] { + let mut pats = match &rule.pats[0] { // Since the variable in the succ ctr is not a nested pattern, we need this special case. - vec![Pattern::Var(var.clone())] - } else { - rule.pats[0].children().cloned().collect::>() + Pattern::Num(NumCtr::Succ(_, Some(var))) => vec![Pattern::Var(var.clone())], + // Similarly for the default case in a num match + Pattern::Var(var) => vec![Pattern::Var(var.clone())], + _ => rule.pats[0].children().cloned().collect::>() }; if pats.is_empty() { // We say that a unit variant always has an unused wildcard nested diff --git a/tests/golden_tests/compile_file/match_num_all_patterns.hvm b/tests/golden_tests/compile_file/match_num_all_patterns.hvm index 6118c0690..ad033339b 100644 --- a/tests/golden_tests/compile_file/match_num_all_patterns.hvm +++ b/tests/golden_tests/compile_file/match_num_all_patterns.hvm @@ -1,9 +1,9 @@ zero_succ = @x match x { 0: 0 - +: x-1 + 1+: x-1 } succ_zero = @x match x { - +: x-1 + 1+: x-1 0: 0 } @@ -14,7 +14,7 @@ var_zero = @x match x { var_succ = @x match x { var: var - +: x-1 + 1+: x-1 } zero_var = @x match x { @@ -23,38 +23,38 @@ zero_var = @x match x { } succ_var = @x match x { - +: x-1 + 1+: x-1 var: 0 } zero_var_succ = @x match x { 0: 0 var: (- var 1) - +: x-1 + 1+: x-1 } succ_var_zero = @x match x { - +: (+ x-1 2) + 1+: (+ x-1 2) var: (+ var 1) 0: 1 } zero_succ_var = @x match x { 0: 0 - +: x-1 + 1+: x-1 var: (- var 1) } succ_zero_var = @x match x { - +: x-1 + 1+: x-1 0: 0 var: (- var 1) } succ_zero_succ = @x match x { - +: x-1 + 1+: x-1 0: 0 - +a: (+ a 1) + 1+a: (+ a 1) } main = 0 \ No newline at end of file diff --git a/tests/golden_tests/compile_file/match_num_unscoped_lambda.hvm b/tests/golden_tests/compile_file/match_num_unscoped_lambda.hvm index e3f141db8..fe3be08e7 100644 --- a/tests/golden_tests/compile_file/match_num_unscoped_lambda.hvm +++ b/tests/golden_tests/compile_file/match_num_unscoped_lambda.hvm @@ -1,11 +1,11 @@ lambda_out = @x @$y match x { 0: $y - +: x-1 + 1+: x-1 } lambda_in = @x (match x { 0: @x x - +: @$y x-1 + 1+: @$y x-1 } $y) main = * \ No newline at end of file diff --git a/tests/golden_tests/compile_file_o_all/extracted_match_pred.hvm b/tests/golden_tests/compile_file_o_all/extracted_match_pred.hvm index 41dea841d..7f368aa99 100644 --- a/tests/golden_tests/compile_file_o_all/extracted_match_pred.hvm +++ b/tests/golden_tests/compile_file_o_all/extracted_match_pred.hvm @@ -1,5 +1,5 @@ // We expect the inferred 'λn-1' from the match to be extracted which allows this recursive func -val = λn (match n { 0: valZ; +: (valS n-1) }) +val = λn (match n { 0: valZ; 1+: (valS n-1) }) valZ = 0 valS = λp (val p) main = (val 1) \ No newline at end of file diff --git a/tests/golden_tests/compile_file_o_all/linearize_match.hvm b/tests/golden_tests/compile_file_o_all/linearize_match.hvm index f09ccda76..e950ba582 100644 --- a/tests/golden_tests/compile_file_o_all/linearize_match.hvm +++ b/tests/golden_tests/compile_file_o_all/linearize_match.hvm @@ -1,4 +1,4 @@ main = @a @b let c = (+ a a); match a { 0: b; - +: (+ a-1 b); + 1+: (+ a-1 b); } diff --git a/tests/golden_tests/compile_file_o_all/match_mult_linearization.hvm b/tests/golden_tests/compile_file_o_all/match_mult_linearization.hvm index 8aef2ad49..f2d8723f8 100644 --- a/tests/golden_tests/compile_file_o_all/match_mult_linearization.hvm +++ b/tests/golden_tests/compile_file_o_all/match_mult_linearization.hvm @@ -1,4 +1,4 @@ main = @a @b @c @d match a { 0: (+ (+ b c) d); - +: (+ (+ (+ a-1 b) c) d); + 1+: (+ (+ (+ a-1 b) c) d); } \ No newline at end of file diff --git a/tests/golden_tests/compile_file_o_all/match_num_explicit_bind.hvm b/tests/golden_tests/compile_file_o_all/match_num_explicit_bind.hvm index a5c8d4a42..4b167c1bc 100644 --- a/tests/golden_tests/compile_file_o_all/match_num_explicit_bind.hvm +++ b/tests/golden_tests/compile_file_o_all/match_num_explicit_bind.hvm @@ -1,6 +1,6 @@ pred = @n match n { 0: 0 - +: n-1 + 1+: n-1 } main = (pred 4) \ No newline at end of file diff --git a/tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm b/tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm index 603805343..e01d13e80 100644 --- a/tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm +++ b/tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm @@ -3,6 +3,6 @@ data bool = false | true (Foo false a) = 0 (Foo true 0) = 0 -(Foo true +n) = n +(Foo true 1+n) = n Main = (Foo true 3) \ No newline at end of file diff --git a/tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm b/tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm index c5ea8fc46..f4adf83dc 100644 --- a/tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm +++ b/tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm @@ -1,4 +1,4 @@ // `Foo` inside the term `{Foo Foo}` is not in a active position, tests that it is not unnecessarily extracted -Foo = @a match a { 0: {Foo Foo}; +p: @* p } +Foo = @a match a { 0: {Foo Foo}; 1+p: @* p } main = (Foo 0) diff --git a/tests/golden_tests/compile_file_o_all/sum_predicates.hvm b/tests/golden_tests/compile_file_o_all/sum_predicates.hvm index 93b35ea97..30b30164e 100644 --- a/tests/golden_tests/compile_file_o_all/sum_predicates.hvm +++ b/tests/golden_tests/compile_file_o_all/sum_predicates.hvm @@ -1,11 +1,11 @@ sum_pred = @a @b match a { 0: match b { 0: 0 - +: b-1 + 1+: b-1 }; - +: match b { + 1+: match b { 0: a-1 - +: (+ a-1 b-1) + 1+: (+ a-1 b-1) } } diff --git a/tests/golden_tests/compile_term/match.hvm b/tests/golden_tests/compile_term/match.hvm index fe3c636e1..653405565 100644 --- a/tests/golden_tests/compile_term/match.hvm +++ b/tests/golden_tests/compile_term/match.hvm @@ -1,4 +1,4 @@ match (+ 0 1) { 0: λt λf t - +: λ* λt λf f // The term to hvmc function assumes the pred variable is already detached from the match + 1+: λ* λt λf f // The term to hvmc function assumes the pred variable is already detached from the match } \ No newline at end of file diff --git a/tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm b/tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm index 91358506e..c87283a54 100644 --- a/tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm +++ b/tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm @@ -4,6 +4,6 @@ (Fn2 (*,(*,(a,*)))) = a (Fn3 (0,*) *) = 0 -(Fn3 (+a,*) *) = a +(Fn3 (1+a,*) *) = a main = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0) \ No newline at end of file diff --git a/tests/golden_tests/encode_pattern_match/match_bind.hvm b/tests/golden_tests/encode_pattern_match/match_bind.hvm index f437366cb..15e0621a4 100644 --- a/tests/golden_tests/encode_pattern_match/match_bind.hvm +++ b/tests/golden_tests/encode_pattern_match/match_bind.hvm @@ -1,7 +1,7 @@ cheese = match num = (+ 2 3) { | 0: 653323 - | +: (+ num num-1) + | 1+: (+ num num-1) } main = cheese \ No newline at end of file diff --git a/tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm b/tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm new file mode 100644 index 000000000..7348be00b --- /dev/null +++ b/tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm @@ -0,0 +1,15 @@ +// Testing various forms of pattern matching +data Result = (Ok val) | (Err err) + +Parse state (String.cons 40 xs) = (Ok (40, xs, state)) +Parse state (String.cons 41 xs) = (Ok (41, xs, state)) +Parse state (String.cons 10 xs) = (Ok (0, xs, state)) +Parse state xs = (Err (xs, state)) + +main = + let str = (String.cons 40 (String.cons 50 String.nil)); + let state = *; + match (Parse state str) { + (Ok (val, xs, state)): (val, (Parse state xs)) + err: err + } \ No newline at end of file diff --git a/tests/golden_tests/encode_pattern_match/match_num_pred.hvm b/tests/golden_tests/encode_pattern_match/match_num_pred.hvm new file mode 100644 index 000000000..008014b72 --- /dev/null +++ b/tests/golden_tests/encode_pattern_match/match_num_pred.hvm @@ -0,0 +1,18 @@ +pred 0 = 0 +pred 1+x = x + +pred2 2+x = x +pred2 * = 0 + +pred3 0 = 0 +pred3 1 = 0 +pred3 2 = 0 +pred3 3+x-3 = x-3 + +pred4 0 = 0 +pred4 1 = 0 +pred4 2 = 0 +pred4 3 = 0 +pred4 n = (- n 4) + +main = * \ No newline at end of file diff --git a/tests/golden_tests/run_file/bitonic_sort.hvm b/tests/golden_tests/run_file/bitonic_sort.hvm index e97cc6100..c128f4595 100644 --- a/tests/golden_tests/run_file/bitonic_sort.hvm +++ b/tests/golden_tests/run_file/bitonic_sort.hvm @@ -4,7 +4,7 @@ data Error = Err // Atomic Swapper (Swap n a b) = match n { 0: (Both a b) - +: (Both b a) + 1+: (Both b a) } // Swaps distant values in parallel; corresponds to a Red Box @@ -31,7 +31,7 @@ data Error = Err // Generates a tree of depth `n` (Gen n x) = match n { 0: (Leaf x) - +: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1))) + 1+: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1))) } // Reverses a tree diff --git a/tests/golden_tests/run_file/bitonic_sort_lam.hvm b/tests/golden_tests/run_file/bitonic_sort_lam.hvm index 0389d6517..8cf316065 100644 --- a/tests/golden_tests/run_file/bitonic_sort_lam.hvm +++ b/tests/golden_tests/run_file/bitonic_sort_lam.hvm @@ -4,7 +4,7 @@ Node = λx0 λx1 #Tree λl #Tree λn (n x0 x1) swap = λn match n { 0: λx0 λx1 (Node x0 x1) - +: λx0 λx1 (Node x1 x0) + 1+: λx0 λx1 (Node x1 x0) } warp = λa @@ -43,7 +43,7 @@ sort = λa gen = λn match n { 0: λx (Leaf x) - +: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 1))) + 1+: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 1))) } rev = λa diff --git a/tests/golden_tests/run_file/box.hvm b/tests/golden_tests/run_file/box.hvm index 8af146a81..e7740bff2 100644 --- a/tests/golden_tests/run_file/box.hvm +++ b/tests/golden_tests/run_file/box.hvm @@ -2,6 +2,6 @@ data _Box = (Box val) Box.subst (Box n) from to = (Box.subst.go n (== from n) to) Box.subst.go a 0 to = (Box a) -Box.subst.go a +* to = to +Box.subst.go a 1+* to = to Main = (Box.subst (Box 4) 4 (Box 10)) \ No newline at end of file diff --git a/tests/golden_tests/run_file/box2.hvm b/tests/golden_tests/run_file/box2.hvm index 8f66fa234..bbfa4138a 100644 --- a/tests/golden_tests/run_file/box2.hvm +++ b/tests/golden_tests/run_file/box2.hvm @@ -2,6 +2,6 @@ data _Box = (Box val) Box.subst (Box n) from to = (Box.subst.go n (== from n) to) Box.subst.go a 0 to = (Box a) -Box.subst.go a +* to = to +Box.subst.go a 1+* to = to Main = (Box.subst (Box 4) 8000 (Box 10)) \ No newline at end of file diff --git a/tests/golden_tests/run_file/def_bool_num.hvm b/tests/golden_tests/run_file/def_bool_num.hvm index 1a97e33c4..3573534a9 100644 --- a/tests/golden_tests/run_file/def_bool_num.hvm +++ b/tests/golden_tests/run_file/def_bool_num.hvm @@ -1,6 +1,6 @@ data bool = true | false go true 0 = 1 -go false +* = 0 +go false 1+* = 0 main = (go true 1) \ No newline at end of file diff --git a/tests/golden_tests/run_file/example.hvm b/tests/golden_tests/run_file/example.hvm index 5170f5a92..ca7fe5a40 100644 --- a/tests/golden_tests/run_file/example.hvm +++ b/tests/golden_tests/run_file/example.hvm @@ -22,7 +22,7 @@ (Num.pred) = λn match n { 0: 0 - +: n-1 + 1+: n-1 } // Write new data types like this diff --git a/tests/golden_tests/run_file/extracted_match_pred.hvm b/tests/golden_tests/run_file/extracted_match_pred.hvm index 2aff08ce0..7de905385 100644 --- a/tests/golden_tests/run_file/extracted_match_pred.hvm +++ b/tests/golden_tests/run_file/extracted_match_pred.hvm @@ -1,5 +1,5 @@ // We expect the lambda 'p' from the match to be extracted which allows this recursive func -val = λn (match n { 0: valZ; +: (valS n-1) }) +val = λn (match n { 0: valZ; 1+: (valS n-1) }) valZ = 0 valS = λp (val p) main = (val 1) \ No newline at end of file diff --git a/tests/golden_tests/run_file/linearize_match.hvm b/tests/golden_tests/run_file/linearize_match.hvm index f09ccda76..e950ba582 100644 --- a/tests/golden_tests/run_file/linearize_match.hvm +++ b/tests/golden_tests/run_file/linearize_match.hvm @@ -1,4 +1,4 @@ main = @a @b let c = (+ a a); match a { 0: b; - +: (+ a-1 b); + 1+: (+ a-1 b); } diff --git a/tests/golden_tests/run_file/list_take.hvm b/tests/golden_tests/run_file/list_take.hvm index 6ac2c8940..68a1c8b43 100644 --- a/tests/golden_tests/run_file/list_take.hvm +++ b/tests/golden_tests/run_file/list_take.hvm @@ -1,7 +1,7 @@ Take_ n list = match (== n 0) { | 0: (Take n list) - | +: [] + | 1+: [] } Take n (List.nil) = [] Take n (List.cons x xs) = (List.cons x (Take_ (- n 1) xs)) diff --git a/tests/golden_tests/run_file/list_to_tree.hvm b/tests/golden_tests/run_file/list_to_tree.hvm index 8cf8160c0..7a3e7e4b8 100644 --- a/tests/golden_tests/run_file/list_to_tree.hvm +++ b/tests/golden_tests/run_file/list_to_tree.hvm @@ -5,7 +5,7 @@ List.len.go (List.cons x xs) count = (List.len.go xs (+ count 1)) Take.go n list = match (== n 0) { | 0: (Take n list) - | +: [] + | 1+: [] } Take n [] = [] Take n (List.cons x xs) = (List.cons x (Take.go (- n 1) xs)) @@ -13,7 +13,7 @@ Take n (List.cons x xs) = (List.cons x (Take.go (- n 1) xs)) Drop.go n list = match (== n 0) { | 0: (Drop n list) - | +: list + | 1+: list } Drop n [] = [] Drop n (List.cons x xs) = (Drop.go (- n 1) xs) diff --git a/tests/golden_tests/run_file/match.hvm b/tests/golden_tests/run_file/match.hvm index af74400aa..a0e972644 100644 --- a/tests/golden_tests/run_file/match.hvm +++ b/tests/golden_tests/run_file/match.hvm @@ -1,5 +1,5 @@ main = match (+ 0 1) { 0: λt λf t - +: λt λf f + 1+: λt λf f } \ No newline at end of file diff --git a/tests/golden_tests/run_file/match_mult_linearization.hvm b/tests/golden_tests/run_file/match_mult_linearization.hvm index 8aef2ad49..f2d8723f8 100644 --- a/tests/golden_tests/run_file/match_mult_linearization.hvm +++ b/tests/golden_tests/run_file/match_mult_linearization.hvm @@ -1,4 +1,4 @@ main = @a @b @c @d match a { 0: (+ (+ b c) d); - +: (+ (+ (+ a-1 b) c) d); + 1+: (+ (+ (+ a-1 b) c) d); } \ No newline at end of file diff --git a/tests/golden_tests/run_file/match_num_adt_tup_parser.hvm b/tests/golden_tests/run_file/match_num_adt_tup_parser.hvm new file mode 100644 index 000000000..7348be00b --- /dev/null +++ b/tests/golden_tests/run_file/match_num_adt_tup_parser.hvm @@ -0,0 +1,15 @@ +// Testing various forms of pattern matching +data Result = (Ok val) | (Err err) + +Parse state (String.cons 40 xs) = (Ok (40, xs, state)) +Parse state (String.cons 41 xs) = (Ok (41, xs, state)) +Parse state (String.cons 10 xs) = (Ok (0, xs, state)) +Parse state xs = (Err (xs, state)) + +main = + let str = (String.cons 40 (String.cons 50 String.nil)); + let state = *; + match (Parse state str) { + (Ok (val, xs, state)): (val, (Parse state xs)) + err: err + } \ No newline at end of file diff --git a/tests/golden_tests/run_file/match_num_explicit_bind.hvm b/tests/golden_tests/run_file/match_num_explicit_bind.hvm index a5c8d4a42..4b167c1bc 100644 --- a/tests/golden_tests/run_file/match_num_explicit_bind.hvm +++ b/tests/golden_tests/run_file/match_num_explicit_bind.hvm @@ -1,6 +1,6 @@ pred = @n match n { 0: 0 - +: n-1 + 1+: n-1 } main = (pred 4) \ No newline at end of file diff --git a/tests/golden_tests/run_file/match_num_num_to_char.hvm b/tests/golden_tests/run_file/match_num_num_to_char.hvm new file mode 100644 index 000000000..acbeef564 --- /dev/null +++ b/tests/golden_tests/run_file/match_num_num_to_char.hvm @@ -0,0 +1,36 @@ +num_to_char n = match n { + 0: '0' + 1: '1' + 2: '2' + 3: '3' + 4: '4' + 5: '5' + 6: '6' + 7: '7' + 8: '8' + 9: '9' + 10+: '\0' +} + +char_to_num c = match c { + 57: 9 + 56: 8 + 55: 7 + 54: 6 + 53: 5 + 52: 4 + 51: 3 + 50: 2 + 49: 1 + 48: 0 + c : (- 0 1) +} + +map f List.nil = List.nil +map f (List.cons x xs) = (List.cons (f x) (map f xs)) + +main = + let nums = [0 1 2 3 4 5 6 7 8 9 10]; + let chars = (map num_to_char nums); + let nums2 = (map char_to_num chars); + ((nums, nums2), chars) diff --git a/tests/golden_tests/run_file/match_num_succ_complex.hvm b/tests/golden_tests/run_file/match_num_succ_complex.hvm new file mode 100644 index 000000000..9fd730972 --- /dev/null +++ b/tests/golden_tests/run_file/match_num_succ_complex.hvm @@ -0,0 +1,16 @@ +min1 * 0 = 0 +min1 0 * = 0 +min1 1+a 1+b = (+ 1 (min1 a b)) + +min2 0 * = 0 +min2 * 0 = 0 +min2 1+a 1+b = (+ (min2 a b) 1) + +min3 1+a 1+b = (+ (min3 a b) 1) +min3 * * = 0 + +main = [ + [(min1 5 10) (min1 10 5) (min1 0 12) (min1 12 0) (min1 0 0) (min1 6 6)] + [(min2 5 10) (min2 10 5) (min2 0 12) (min2 12 0) (min2 0 0) (min2 6 6)] + [(min3 5 10) (min3 10 5) (min3 0 12) (min3 12 0) (min3 0 0) (min3 6 6)] +] \ No newline at end of file diff --git a/tests/golden_tests/run_file/match_sup.hvm b/tests/golden_tests/run_file/match_sup.hvm index 19836b20d..000d28567 100644 --- a/tests/golden_tests/run_file/match_sup.hvm +++ b/tests/golden_tests/run_file/match_sup.hvm @@ -1,4 +1,4 @@ main = let k = #a{0 1}; match k { 0: 1 - +p: (+ p 2) + 1+p: (+ p 2) } \ No newline at end of file diff --git a/tests/golden_tests/run_file/merge_sort.hvm b/tests/golden_tests/run_file/merge_sort.hvm index 061d82873..cf62c944c 100644 --- a/tests/golden_tests/run_file/merge_sort.hvm +++ b/tests/golden_tests/run_file/merge_sort.hvm @@ -9,7 +9,7 @@ merge (Cons x xs) (Nil) = (Cons x xs) merge (Cons x xs) (Cons y ys) = let t = match (< x y) { 0: λaλbλcλt(t c a b) - +: λaλbλcλt(t a b c) + 1+: λaλbλcλt(t a b c) } let t = (t (Cons x) λx(x) (Cons y)) @@ -21,7 +21,7 @@ sum (Cons h t) = (+ h (sum t)) range n = match n { 0: λx (Leaf x) - +: λx (Node (range n-1 (+ (* x 2) 1)) (range n-1 (* x 2))) + 1+: λx (Node (range n-1 (+ (* x 2) 1)) (range n-1 (* x 2))) } main = (sum (sort (range 4 0))) diff --git a/tests/golden_tests/run_file/names_hyphen.hvm b/tests/golden_tests/run_file/names_hyphen.hvm index 68bbb3dd0..16e20f19b 100644 --- a/tests/golden_tests/run_file/names_hyphen.hvm +++ b/tests/golden_tests/run_file/names_hyphen.hvm @@ -5,7 +5,7 @@ data Done_ = (Done done-var) toZero n = match n { 0: (Done 1) - +: (toZero n-1) + 1+: (toZero n-1) } main = diff --git a/tests/golden_tests/run_file/num_match_missing_var.hvm b/tests/golden_tests/run_file/num_match_missing_var.hvm new file mode 100644 index 000000000..078474859 --- /dev/null +++ b/tests/golden_tests/run_file/num_match_missing_var.hvm @@ -0,0 +1,22 @@ +if 0 t f = f +if 1 t f = t + +if2 n t f = match n { + 0: f + 1+: t + n: f +} + +if3 n t f = match n { + 0: f + *: t + 1+: t +} + +if4 n t f = match n { + 0: f + 1+: t + 1: t +} + +main = (if2 1 2 3) \ No newline at end of file diff --git a/tests/golden_tests/run_file/num_pred.hvm b/tests/golden_tests/run_file/num_pred.hvm index 5424af8a1..bea29e05d 100644 --- a/tests/golden_tests/run_file/num_pred.hvm +++ b/tests/golden_tests/run_file/num_pred.hvm @@ -1,4 +1,4 @@ Pred 0 = 0 -Pred +pred = pred +Pred 1+pred = pred Main = (Pred 43) \ No newline at end of file diff --git a/tests/golden_tests/run_file/pred.hvm b/tests/golden_tests/run_file/pred.hvm index e5fc185c6..809517b7b 100644 --- a/tests/golden_tests/run_file/pred.hvm +++ b/tests/golden_tests/run_file/pred.hvm @@ -1,6 +1,6 @@ Pred = λt match t { 0: 0 - +: t-1 + 1+: t-1 } main = (Pred 3) \ No newline at end of file diff --git a/tests/golden_tests/run_file/radix_sort_ctr.hvm b/tests/golden_tests/run_file/radix_sort_ctr.hvm index 13488bed2..acd51decd 100644 --- a/tests/golden_tests/run_file/radix_sort_ctr.hvm +++ b/tests/golden_tests/run_file/radix_sort_ctr.hvm @@ -3,7 +3,7 @@ data Arr = Null | (Leaf x) | (Node a b) (Swap s a b) = match s { 0: (Both a b) - +: (Both b a) + 1+: (Both b a) } // Sort : Arr -> Arr @@ -76,7 +76,7 @@ data Arr = Null | (Leaf x) | (Node a b) (Gen n) = (Gen.go n 0) (Gen.go n x) = match n { 0: (Leaf x) - +: + 1+: let x = (<< x 1) let y = (| x 1) (Node (Gen.go n-1 x) (Gen.go n-1 y)) diff --git a/tests/golden_tests/run_file/recursive_combinator_nested.hvm b/tests/golden_tests/run_file/recursive_combinator_nested.hvm index e67d2ae7d..131cca0a7 100644 --- a/tests/golden_tests/run_file/recursive_combinator_nested.hvm +++ b/tests/golden_tests/run_file/recursive_combinator_nested.hvm @@ -1,4 +1,4 @@ // Tests that `({Foo @* a} 9)` is correctly extracted as a combinator, otherwise the file would hang when running -Foo = @a match a { 0: (#a {Foo @* a} 9); +p: p } +Foo = @a match a { 0: (#a {Foo @* a} 9); 1+p: p } main = (Foo 0) diff --git a/tests/golden_tests/run_file/recursive_match_native.hvm b/tests/golden_tests/run_file/recursive_match_native.hvm index 7e0ba7798..a3223cb69 100644 --- a/tests/golden_tests/run_file/recursive_match_native.hvm +++ b/tests/golden_tests/run_file/recursive_match_native.hvm @@ -2,7 +2,7 @@ add = λa λb (+ a b) sum = λn match n { 0: 1 - +: (add (sum n-1) (sum n-1)) + 1+: (add (sum n-1) (sum n-1)) } main = (sum 9) \ No newline at end of file diff --git a/tests/golden_tests/run_file/str_inc.hvm b/tests/golden_tests/run_file/str_inc.hvm index 8e025012f..268a479dc 100644 --- a/tests/golden_tests/run_file/str_inc.hvm +++ b/tests/golden_tests/run_file/str_inc.hvm @@ -1,7 +1,7 @@ (StrInc (len, buf)) = (len, #str λx (StrGo len #str (buf x))) (StrGo 0 str) = str -(StrGo +x (head, tail)) = ((+ 1 head), (StrGo x tail)) +(StrGo 1+x (head, tail)) = ((+ 1 head), (StrGo x tail)) // Old str encoding Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x)))))))))))) diff --git a/tests/golden_tests/run_file/str_inc_eta.hvm b/tests/golden_tests/run_file/str_inc_eta.hvm index b000efcb9..22279b4d4 100644 --- a/tests/golden_tests/run_file/str_inc_eta.hvm +++ b/tests/golden_tests/run_file/str_inc_eta.hvm @@ -1,7 +1,7 @@ (StrInc (len, buf)) = (len, #str λx (StrGo len #str (buf x))) (StrGo 0 (head, tail)) = (head, tail) -(StrGo +x (head, tail)) = ((+ 1 head), (StrGo x tail)) +(StrGo 1+x (head, tail)) = ((+ 1 head), (StrGo x tail)) // Old str encoding Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x)))))))))))) diff --git a/tests/golden_tests/run_file/sum_tree.hvm b/tests/golden_tests/run_file/sum_tree.hvm index fc8429838..5feee56e2 100644 --- a/tests/golden_tests/run_file/sum_tree.hvm +++ b/tests/golden_tests/run_file/sum_tree.hvm @@ -4,7 +4,7 @@ add = λa λb (+ a b) gen = λn match n { 0: (Leaf 1) - +: (Node (gen n-1) (gen n-1)) + 1+: (Node (gen n-1) (gen n-1)) } sum = λt diff --git a/tests/golden_tests/run_file/tuple_rots.hvm b/tests/golden_tests/run_file/tuple_rots.hvm index 0aae52927..c8d83c622 100644 --- a/tests/golden_tests/run_file/tuple_rots.hvm +++ b/tests/golden_tests/run_file/tuple_rots.hvm @@ -4,7 +4,7 @@ rot = λx (x λa λb λc λd λe λf λg λh (MkTup8 b c d e f g h a)) app = λn match n { 0: λf λx x - +: λf λx (app n-1 f (f x)) + 1+: λf λx (app n-1 f (f x)) } main = (app 100 rot (MkTup8 1 2 3 4 5 6 7 8)) \ No newline at end of file diff --git a/tests/golden_tests/run_lazy/bitonic_sort.hvm b/tests/golden_tests/run_lazy/bitonic_sort.hvm index e97cc6100..c128f4595 100644 --- a/tests/golden_tests/run_lazy/bitonic_sort.hvm +++ b/tests/golden_tests/run_lazy/bitonic_sort.hvm @@ -4,7 +4,7 @@ data Error = Err // Atomic Swapper (Swap n a b) = match n { 0: (Both a b) - +: (Both b a) + 1+: (Both b a) } // Swaps distant values in parallel; corresponds to a Red Box @@ -31,7 +31,7 @@ data Error = Err // Generates a tree of depth `n` (Gen n x) = match n { 0: (Leaf x) - +: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1))) + 1+: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1))) } // Reverses a tree diff --git a/tests/golden_tests/run_lazy/bitonic_sort_lam.hvm b/tests/golden_tests/run_lazy/bitonic_sort_lam.hvm index 0389d6517..8cf316065 100644 --- a/tests/golden_tests/run_lazy/bitonic_sort_lam.hvm +++ b/tests/golden_tests/run_lazy/bitonic_sort_lam.hvm @@ -4,7 +4,7 @@ Node = λx0 λx1 #Tree λl #Tree λn (n x0 x1) swap = λn match n { 0: λx0 λx1 (Node x0 x1) - +: λx0 λx1 (Node x1 x0) + 1+: λx0 λx1 (Node x1 x0) } warp = λa @@ -43,7 +43,7 @@ sort = λa gen = λn match n { 0: λx (Leaf x) - +: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 1))) + 1+: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 1))) } rev = λa diff --git a/tests/golden_tests/run_lazy/box.hvm b/tests/golden_tests/run_lazy/box.hvm index 8af146a81..e7740bff2 100644 --- a/tests/golden_tests/run_lazy/box.hvm +++ b/tests/golden_tests/run_lazy/box.hvm @@ -2,6 +2,6 @@ data _Box = (Box val) Box.subst (Box n) from to = (Box.subst.go n (== from n) to) Box.subst.go a 0 to = (Box a) -Box.subst.go a +* to = to +Box.subst.go a 1+* to = to Main = (Box.subst (Box 4) 4 (Box 10)) \ No newline at end of file diff --git a/tests/golden_tests/run_lazy/box2.hvm b/tests/golden_tests/run_lazy/box2.hvm index 8f66fa234..bbfa4138a 100644 --- a/tests/golden_tests/run_lazy/box2.hvm +++ b/tests/golden_tests/run_lazy/box2.hvm @@ -2,6 +2,6 @@ data _Box = (Box val) Box.subst (Box n) from to = (Box.subst.go n (== from n) to) Box.subst.go a 0 to = (Box a) -Box.subst.go a +* to = to +Box.subst.go a 1+* to = to Main = (Box.subst (Box 4) 8000 (Box 10)) \ No newline at end of file diff --git a/tests/golden_tests/run_lazy/example.hvm b/tests/golden_tests/run_lazy/example.hvm index 5170f5a92..ca7fe5a40 100644 --- a/tests/golden_tests/run_lazy/example.hvm +++ b/tests/golden_tests/run_lazy/example.hvm @@ -22,7 +22,7 @@ (Num.pred) = λn match n { 0: 0 - +: n-1 + 1+: n-1 } // Write new data types like this diff --git a/tests/golden_tests/run_lazy/extracted_match_pred.hvm b/tests/golden_tests/run_lazy/extracted_match_pred.hvm index 2aff08ce0..7de905385 100644 --- a/tests/golden_tests/run_lazy/extracted_match_pred.hvm +++ b/tests/golden_tests/run_lazy/extracted_match_pred.hvm @@ -1,5 +1,5 @@ // We expect the lambda 'p' from the match to be extracted which allows this recursive func -val = λn (match n { 0: valZ; +: (valS n-1) }) +val = λn (match n { 0: valZ; 1+: (valS n-1) }) valZ = 0 valS = λp (val p) main = (val 1) \ No newline at end of file diff --git a/tests/golden_tests/run_lazy/linearize_match.hvm b/tests/golden_tests/run_lazy/linearize_match.hvm index f09ccda76..e950ba582 100644 --- a/tests/golden_tests/run_lazy/linearize_match.hvm +++ b/tests/golden_tests/run_lazy/linearize_match.hvm @@ -1,4 +1,4 @@ main = @a @b let c = (+ a a); match a { 0: b; - +: (+ a-1 b); + 1+: (+ a-1 b); } diff --git a/tests/golden_tests/run_lazy/list_take.hvm b/tests/golden_tests/run_lazy/list_take.hvm index 6ac2c8940..68a1c8b43 100644 --- a/tests/golden_tests/run_lazy/list_take.hvm +++ b/tests/golden_tests/run_lazy/list_take.hvm @@ -1,7 +1,7 @@ Take_ n list = match (== n 0) { | 0: (Take n list) - | +: [] + | 1+: [] } Take n (List.nil) = [] Take n (List.cons x xs) = (List.cons x (Take_ (- n 1) xs)) diff --git a/tests/golden_tests/run_lazy/list_to_tree.hvm b/tests/golden_tests/run_lazy/list_to_tree.hvm index 8cf8160c0..7a3e7e4b8 100644 --- a/tests/golden_tests/run_lazy/list_to_tree.hvm +++ b/tests/golden_tests/run_lazy/list_to_tree.hvm @@ -5,7 +5,7 @@ List.len.go (List.cons x xs) count = (List.len.go xs (+ count 1)) Take.go n list = match (== n 0) { | 0: (Take n list) - | +: [] + | 1+: [] } Take n [] = [] Take n (List.cons x xs) = (List.cons x (Take.go (- n 1) xs)) @@ -13,7 +13,7 @@ Take n (List.cons x xs) = (List.cons x (Take.go (- n 1) xs)) Drop.go n list = match (== n 0) { | 0: (Drop n list) - | +: list + | 1+: list } Drop n [] = [] Drop n (List.cons x xs) = (Drop.go (- n 1) xs) diff --git a/tests/golden_tests/run_lazy/match.hvm b/tests/golden_tests/run_lazy/match.hvm index af74400aa..a0e972644 100644 --- a/tests/golden_tests/run_lazy/match.hvm +++ b/tests/golden_tests/run_lazy/match.hvm @@ -1,5 +1,5 @@ main = match (+ 0 1) { 0: λt λf t - +: λt λf f + 1+: λt λf f } \ No newline at end of file diff --git a/tests/golden_tests/run_lazy/match_mult_linearization.hvm b/tests/golden_tests/run_lazy/match_mult_linearization.hvm index 8aef2ad49..f2d8723f8 100644 --- a/tests/golden_tests/run_lazy/match_mult_linearization.hvm +++ b/tests/golden_tests/run_lazy/match_mult_linearization.hvm @@ -1,4 +1,4 @@ main = @a @b @c @d match a { 0: (+ (+ b c) d); - +: (+ (+ (+ a-1 b) c) d); + 1+: (+ (+ (+ a-1 b) c) d); } \ No newline at end of file diff --git a/tests/golden_tests/run_lazy/match_num_explicit_bind.hvm b/tests/golden_tests/run_lazy/match_num_explicit_bind.hvm index a5c8d4a42..4b167c1bc 100644 --- a/tests/golden_tests/run_lazy/match_num_explicit_bind.hvm +++ b/tests/golden_tests/run_lazy/match_num_explicit_bind.hvm @@ -1,6 +1,6 @@ pred = @n match n { 0: 0 - +: n-1 + 1+: n-1 } main = (pred 4) \ No newline at end of file diff --git a/tests/golden_tests/run_lazy/merge_sort.hvm b/tests/golden_tests/run_lazy/merge_sort.hvm index 061d82873..cf62c944c 100644 --- a/tests/golden_tests/run_lazy/merge_sort.hvm +++ b/tests/golden_tests/run_lazy/merge_sort.hvm @@ -9,7 +9,7 @@ merge (Cons x xs) (Nil) = (Cons x xs) merge (Cons x xs) (Cons y ys) = let t = match (< x y) { 0: λaλbλcλt(t c a b) - +: λaλbλcλt(t a b c) + 1+: λaλbλcλt(t a b c) } let t = (t (Cons x) λx(x) (Cons y)) @@ -21,7 +21,7 @@ sum (Cons h t) = (+ h (sum t)) range n = match n { 0: λx (Leaf x) - +: λx (Node (range n-1 (+ (* x 2) 1)) (range n-1 (* x 2))) + 1+: λx (Node (range n-1 (+ (* x 2) 1)) (range n-1 (* x 2))) } main = (sum (sort (range 4 0))) diff --git a/tests/golden_tests/run_lazy/num_pred.hvm b/tests/golden_tests/run_lazy/num_pred.hvm index 5424af8a1..bea29e05d 100644 --- a/tests/golden_tests/run_lazy/num_pred.hvm +++ b/tests/golden_tests/run_lazy/num_pred.hvm @@ -1,4 +1,4 @@ Pred 0 = 0 -Pred +pred = pred +Pred 1+pred = pred Main = (Pred 43) \ No newline at end of file diff --git a/tests/golden_tests/run_lazy/radix_sort_ctr.hvm b/tests/golden_tests/run_lazy/radix_sort_ctr.hvm index 13488bed2..acd51decd 100644 --- a/tests/golden_tests/run_lazy/radix_sort_ctr.hvm +++ b/tests/golden_tests/run_lazy/radix_sort_ctr.hvm @@ -3,7 +3,7 @@ data Arr = Null | (Leaf x) | (Node a b) (Swap s a b) = match s { 0: (Both a b) - +: (Both b a) + 1+: (Both b a) } // Sort : Arr -> Arr @@ -76,7 +76,7 @@ data Arr = Null | (Leaf x) | (Node a b) (Gen n) = (Gen.go n 0) (Gen.go n x) = match n { 0: (Leaf x) - +: + 1+: let x = (<< x 1) let y = (| x 1) (Node (Gen.go n-1 x) (Gen.go n-1 y)) diff --git a/tests/golden_tests/run_lazy/recursive_match_native.hvm b/tests/golden_tests/run_lazy/recursive_match_native.hvm index 7e0ba7798..a3223cb69 100644 --- a/tests/golden_tests/run_lazy/recursive_match_native.hvm +++ b/tests/golden_tests/run_lazy/recursive_match_native.hvm @@ -2,7 +2,7 @@ add = λa λb (+ a b) sum = λn match n { 0: 1 - +: (add (sum n-1) (sum n-1)) + 1+: (add (sum n-1) (sum n-1)) } main = (sum 9) \ No newline at end of file diff --git a/tests/golden_tests/run_lazy/str_inc.hvm b/tests/golden_tests/run_lazy/str_inc.hvm index 8e025012f..268a479dc 100644 --- a/tests/golden_tests/run_lazy/str_inc.hvm +++ b/tests/golden_tests/run_lazy/str_inc.hvm @@ -1,7 +1,7 @@ (StrInc (len, buf)) = (len, #str λx (StrGo len #str (buf x))) (StrGo 0 str) = str -(StrGo +x (head, tail)) = ((+ 1 head), (StrGo x tail)) +(StrGo 1+x (head, tail)) = ((+ 1 head), (StrGo x tail)) // Old str encoding Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x)))))))))))) diff --git a/tests/golden_tests/run_lazy/str_inc_eta.hvm b/tests/golden_tests/run_lazy/str_inc_eta.hvm index b000efcb9..22279b4d4 100644 --- a/tests/golden_tests/run_lazy/str_inc_eta.hvm +++ b/tests/golden_tests/run_lazy/str_inc_eta.hvm @@ -1,7 +1,7 @@ (StrInc (len, buf)) = (len, #str λx (StrGo len #str (buf x))) (StrGo 0 (head, tail)) = (head, tail) -(StrGo +x (head, tail)) = ((+ 1 head), (StrGo x tail)) +(StrGo 1+x (head, tail)) = ((+ 1 head), (StrGo x tail)) // Old str encoding Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x)))))))))))) diff --git a/tests/golden_tests/run_lazy/sum_tree.hvm b/tests/golden_tests/run_lazy/sum_tree.hvm index fc8429838..5feee56e2 100644 --- a/tests/golden_tests/run_lazy/sum_tree.hvm +++ b/tests/golden_tests/run_lazy/sum_tree.hvm @@ -4,7 +4,7 @@ add = λa λb (+ a b) gen = λn match n { 0: (Leaf 1) - +: (Node (gen n-1) (gen n-1)) + 1+: (Node (gen n-1) (gen n-1)) } sum = λt diff --git a/tests/golden_tests/run_lazy/tuple_rots.hvm b/tests/golden_tests/run_lazy/tuple_rots.hvm index 0aae52927..c8d83c622 100644 --- a/tests/golden_tests/run_lazy/tuple_rots.hvm +++ b/tests/golden_tests/run_lazy/tuple_rots.hvm @@ -4,7 +4,7 @@ rot = λx (x λa λb λc λd λe λf λg λh (MkTup8 b c d e f g h a)) app = λn match n { 0: λf λx x - +: λf λx (app n-1 f (f x)) + 1+: λf λx (app n-1 f (f x)) } main = (app 100 rot (MkTup8 1 2 3 4 5 6 7 8)) \ No newline at end of file diff --git a/tests/golden_tests/simplify_matches/redundant_with_era.hvm b/tests/golden_tests/simplify_matches/redundant_with_era.hvm index d27646d8d..427b8d99c 100644 --- a/tests/golden_tests/simplify_matches/redundant_with_era.hvm +++ b/tests/golden_tests/simplify_matches/redundant_with_era.hvm @@ -1,6 +1,6 @@ // Should not create flattened rules for the 2 bottom rules and should properly erase the first arg. (Fn2 * (*, (*, a))) = a (Fn2 0 *) = 0 -(Fn2 +a *) = a +(Fn2 1+a *) = a main = * diff --git a/tests/snapshots/compile_file__match_num_all_patterns.hvm.snap b/tests/snapshots/compile_file__match_num_all_patterns.hvm.snap index 0641700ee..9dbbbf592 100644 --- a/tests/snapshots/compile_file__match_num_all_patterns.hvm.snap +++ b/tests/snapshots/compile_file__match_num_all_patterns.hvm.snap @@ -29,4 +29,3 @@ input_file: tests/golden_tests/compile_file/match_num_all_patterns.hvm @zero_var$S0 = (<+ #1 <- #1 a>> a) @zero_var_succ = (?<(#0 @zero_var_succ$S0) a> a) @zero_var_succ$S0 = (<+ #1 <- #1 a>> a) - diff --git a/tests/snapshots/compile_file__missing_pat.hvm.snap b/tests/snapshots/compile_file__missing_pat.hvm.snap index fe1283bb4..856adeea6 100644 --- a/tests/snapshots/compile_file__missing_pat.hvm.snap +++ b/tests/snapshots/compile_file__missing_pat.hvm.snap @@ -2,5 +2,5 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/compile_file/missing_pat.hvm --- -At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected '(', '#', '$', , '[', '{', 'λ', 'let', 'match', '*', '|', 0, or + +At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected '(', '#', '$', , '[', '{', 'λ', 'let', 'match', '*', '|', +, or  2 | : * 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 db2ad4fa2..992385330 100644 --- a/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap +++ b/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap @@ -7,7 +7,7 @@ TaggedScott: (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; λe (match c { 0: λ* λ* 0; +: λi λ* λ* i } d e) b) +(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; 1+: λi λ* λ* i } d e) b) (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0) @@ -16,6 +16,6 @@ Scott: (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; λe (match c { 0: λ* λ* 0; +: λi λ* λ* i } d e) b) +(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; 1+: λ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 f1b9170b8..448104966 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; +: λd λe (+ e d) } a_2) +(cheese) = let {a a_2} = (+ 2 3); (match a { 0: λ* 653323; 1+: λd λe (+ e d) } a_2) (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; 1+: λd λe (+ e d) } a_2) (main) = cheese diff --git a/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap new file mode 100644 index 000000000..95d979f91 --- /dev/null +++ b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap @@ -0,0 +1,29 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm +--- +TaggedScott: +(Parse) = λa λb (#String (b #String.String.cons.head λc #String.String.cons.tail λd λe (match (- c 40) { 0: λf λg (Ok (40, (g, f))); 1+: λk match k { 0: λl λm (Ok (41, (m, l))); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, (s, r))); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb))) a) + +(main) = #Result ((Parse * (String.cons 40 (String.cons 50 String.nil))) #Result.Ok.val λd let (e, f) = d; (let (g, h) = f; λi (i, (Parse h g)) e) #Result.Err.err λm (Err m)) + +(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b) + +(String.nil) = #String λ* #String λb b + +(Err) = λa #Result λ* #Result λc #Result.Err.err (c a) + +(Ok) = λa #Result λb #Result λ* #Result.Ok.val (b a) + +Scott: +(Parse) = λa λb (b λc λd λe (match (- c 40) { 0: λf λg (Ok (40, (g, f))); 1+: λk match k { 0: λl λm (Ok (41, (m, l))); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, (s, r))); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb)) a) + +(main) = (Parse * (String.cons 40 (String.cons 50 String.nil)) λd let (e, f) = d; (let (g, h) = f; λi (i, (Parse h g)) e) λm (Err m)) + +(String.cons) = λa λb λc λ* (c a b) + +(String.nil) = λ* λb b + +(Err) = λa λ* λc (c a) + +(Ok) = λa λb λ* (b a) diff --git a/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap b/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap new file mode 100644 index 000000000..56425e05e --- /dev/null +++ b/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap @@ -0,0 +1,25 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/encode_pattern_match/match_num_pred.hvm +--- +TaggedScott: +(pred) = λa match a { 0: 0; 1+: λc c } + +(pred2) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe e } } + +(pred3) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe match e { 0: 0; 1+: λg g } } } + +(pred4) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe match e { 0: 0; 1+: λg match g { 0: 0; 1+: λi (- (+ i 4) 4) } } } } + +(main) = * + +Scott: +(pred) = λa match a { 0: 0; 1+: λc c } + +(pred2) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe e } } + +(pred3) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe match e { 0: 0; 1+: λg g } } } + +(pred4) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe match e { 0: 0; 1+: λg match g { 0: 0; 1+: λi (- (+ i 4) 4) } } } } + +(main) = * diff --git a/tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap b/tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap index d453315c9..8e712c1f4 100644 --- a/tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap +++ b/tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap @@ -5,4 +5,4 @@ input_file: tests/golden_tests/readback_lnet/invalid_mat_mat.hvm Readback Warning: Invalid Numeric Match (4 occurrences) -λa match match { 0: 3; +: 4 } { 0: ; +: } +λa match match { 0: 3; 1+: 4 } { 0: ; 1+: } diff --git a/tests/snapshots/readback_lnet__match.hvm.snap b/tests/snapshots/readback_lnet__match.hvm.snap index 63b19f77f..4ffacc30f 100644 --- a/tests/snapshots/readback_lnet__match.hvm.snap +++ b/tests/snapshots/readback_lnet__match.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/readback_lnet/match.hvm --- -let b = 1; match b { 0: λa a; +b-1: b-1 } +let b = 1; match b { 0: λa a; 1+b-1: b-1 } diff --git a/tests/snapshots/run_file__linearize_match.hvm.snap b/tests/snapshots/run_file__linearize_match.hvm.snap index 8d30a906f..dd151e88e 100644 --- a/tests/snapshots/run_file__linearize_match.hvm.snap +++ b/tests/snapshots/run_file__linearize_match.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/linearize_match.hvm --- -λa match a { 0: λb b; +a-1: λd (+ a-1 d) } +λa match a { 0: λb b; 1+a-1: λd (+ a-1 d) } diff --git a/tests/snapshots/run_file__match_mult_linearization.hvm.snap b/tests/snapshots/run_file__match_mult_linearization.hvm.snap index 5e86ba220..4cd7db522 100644 --- a/tests/snapshots/run_file__match_mult_linearization.hvm.snap +++ b/tests/snapshots/run_file__match_mult_linearization.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/match_mult_linearization.hvm --- -λa match a { 0: λb λc λd (+ (+ b c) d); +a-1: λf λg λh (+ (+ (+ a-1 f) g) h) } +λa match a { 0: λb λc λd (+ (+ b c) d); 1+a-1: λf λg λh (+ (+ (+ a-1 f) g) h) } diff --git a/tests/snapshots/run_file__match_num_adt_tup_parser.hvm.snap b/tests/snapshots/run_file__match_num_adt_tup_parser.hvm.snap new file mode 100644 index 000000000..24e9b5fb5 --- /dev/null +++ b/tests/snapshots/run_file__match_num_adt_tup_parser.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/run_file/match_num_adt_tup_parser.hvm +--- +(40, (Err ("2", *))) diff --git a/tests/snapshots/run_file__match_num_num_to_char.hvm.snap b/tests/snapshots/run_file__match_num_num_to_char.hvm.snap new file mode 100644 index 000000000..c1c5bafbe --- /dev/null +++ b/tests/snapshots/run_file__match_num_num_to_char.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/run_file/match_num_num_to_char.hvm +--- +(([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 1152921504606846975]), [48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 0]) diff --git a/tests/snapshots/run_file__match_num_succ_complex.hvm.snap b/tests/snapshots/run_file__match_num_succ_complex.hvm.snap new file mode 100644 index 000000000..85f6bf3ed --- /dev/null +++ b/tests/snapshots/run_file__match_num_succ_complex.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/run_file/match_num_succ_complex.hvm +--- +[[5, 5, 0, 0, 0, 6], [5, 5, 0, 0, 0, 6], [5, 5, 0, 0, 0, 6]] diff --git a/tests/snapshots/run_file__multi_num_match.hvm.snap b/tests/snapshots/run_file__multi_num_match.hvm.snap new file mode 100644 index 000000000..1f43a704a --- /dev/null +++ b/tests/snapshots/run_file__multi_num_match.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/run_file/multi_num_match.hvm +--- +(([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 1152921504606846975]), [48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 0]) diff --git a/tests/snapshots/run_file__num_match_missing_var.hvm.snap b/tests/snapshots/run_file__num_match_missing_var.hvm.snap new file mode 100644 index 000000000..5051c5a14 --- /dev/null +++ b/tests/snapshots/run_file__num_match_missing_var.hvm.snap @@ -0,0 +1,9 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/run_file/num_match_missing_var.hvm +--- +In definition 'if': + Non-exhaustive pattern matching. Hint: + Case '+' not covered. +In definition 'if4': + Expected a sequence of incrementing numbers ending with '1+', found '1'. diff --git a/tests/snapshots/run_lazy__linearize_match.hvm.snap b/tests/snapshots/run_lazy__linearize_match.hvm.snap index 23a3cfd53..d7fe41f28 100644 --- a/tests/snapshots/run_lazy__linearize_match.hvm.snap +++ b/tests/snapshots/run_lazy__linearize_match.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_lazy/linearize_match.hvm --- -λa match a { 0: λb b; +a-1: λd (+ a-1 d) } +λa match a { 0: λb b; 1+a-1: λd (+ a-1 d) } diff --git a/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap b/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap index f1796c4de..8d5cef53d 100644 --- a/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap +++ b/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_lazy/match_mult_linearization.hvm --- -λa match a { 0: λb λc λd (+ (+ b c) d); +a-1: λf λg λh (+ (+ (+ a-1 f) g) h) } +λa match a { 0: λb λc λd (+ (+ b c) d); 1+a-1: λf λg λh (+ (+ (+ a-1 f) g) h) } diff --git a/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap b/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap index 47ee867f2..97758d1c5 100644 --- a/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap +++ b/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap @@ -2,7 +2,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/flatten_with_terminal.hvm --- -(Foo) = λa λb (match a { 0: λc match c { (A e): match e { (B): B } }; +*: λ* * } b) +(Foo) = λa λb (match a { 0: λc match c { (A e): match e { (B): B } }; *: λ* * } b) (main) = (Foo 2 (A B)) diff --git a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap index a0f05ce94..fc5b56eef 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 { (e, f): λg (match f { (*, i): λ* λ* i } g e) } *); 1+m: λn (match n { (o, p): λq (match p { (*, s): λ* λ* s } q o) } m) } b) (main) = * From 5f2d835a77d656c4ef63d72b1bcd6de441e5be11 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 27 Feb 2024 18:02:04 +0100 Subject: [PATCH 2/4] [sc-441] Add char patterns --- src/term/parser/parser.rs | 8 +++++--- .../encode_pattern_match/match_num_adt_tup_parser.hvm | 8 ++++---- tests/golden_tests/run_file/match_num_adt_tup_parser.hvm | 8 ++++---- tests/snapshots/compile_file__missing_pat.hvm.snap | 2 +- ...ncode_pattern_match__match_num_adt_tup_parser.hvm.snap | 4 ++-- .../snapshots/run_file__match_num_adt_tup_parser.hvm.snap | 2 +- 6 files changed, 17 insertions(+), 15 deletions(-) diff --git a/src/term/parser/parser.rs b/src/term/parser/parser.rs index 31fba38cc..6eae0d173 100644 --- a/src/term/parser/parser.rs +++ b/src/term/parser/parser.rs @@ -413,16 +413,18 @@ where }) .labelled(""); - let num_ctr = num.map(|n| Pattern::Num(NumCtr::Num(n))); + let num_pat = num.map(|n| Pattern::Num(NumCtr::Num(n))); - let succ_ctr = num + let succ_pat = num .then_ignore(just(Token::Add)) .then(name_or_era().or_not()) .map(|(num, nam)| Pattern::Num(NumCtr::Succ(num, nam))) .labelled("+") .boxed(); - choice((succ_ctr, num_ctr, var, ctr, list, tup)) + let chr_pat = select!(Token::Char(c) => Pattern::Num(NumCtr::Num(c))).labelled("").boxed(); + + choice((succ_pat, num_pat, chr_pat, var, ctr, list, tup)) }) } diff --git a/tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm b/tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm index 7348be00b..6db64f927 100644 --- a/tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm +++ b/tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm @@ -1,13 +1,13 @@ // Testing various forms of pattern matching data Result = (Ok val) | (Err err) -Parse state (String.cons 40 xs) = (Ok (40, xs, state)) -Parse state (String.cons 41 xs) = (Ok (41, xs, state)) -Parse state (String.cons 10 xs) = (Ok (0, xs, state)) +Parse state (String.cons '(' xs) = (Ok ('(', xs, state)) +Parse state (String.cons ')' xs) = (Ok (')', xs, state)) +Parse state (String.cons '\n' xs) = (Ok (0, xs, state)) Parse state xs = (Err (xs, state)) main = - let str = (String.cons 40 (String.cons 50 String.nil)); + let str = "(+"; let state = *; match (Parse state str) { (Ok (val, xs, state)): (val, (Parse state xs)) diff --git a/tests/golden_tests/run_file/match_num_adt_tup_parser.hvm b/tests/golden_tests/run_file/match_num_adt_tup_parser.hvm index 7348be00b..6db64f927 100644 --- a/tests/golden_tests/run_file/match_num_adt_tup_parser.hvm +++ b/tests/golden_tests/run_file/match_num_adt_tup_parser.hvm @@ -1,13 +1,13 @@ // Testing various forms of pattern matching data Result = (Ok val) | (Err err) -Parse state (String.cons 40 xs) = (Ok (40, xs, state)) -Parse state (String.cons 41 xs) = (Ok (41, xs, state)) -Parse state (String.cons 10 xs) = (Ok (0, xs, state)) +Parse state (String.cons '(' xs) = (Ok ('(', xs, state)) +Parse state (String.cons ')' xs) = (Ok (')', xs, state)) +Parse state (String.cons '\n' xs) = (Ok (0, xs, state)) Parse state xs = (Err (xs, state)) main = - let str = (String.cons 40 (String.cons 50 String.nil)); + let str = "(+"; let state = *; match (Parse state str) { (Ok (val, xs, state)): (val, (Parse state xs)) diff --git a/tests/snapshots/compile_file__missing_pat.hvm.snap b/tests/snapshots/compile_file__missing_pat.hvm.snap index 856adeea6..e9780f8dc 100644 --- a/tests/snapshots/compile_file__missing_pat.hvm.snap +++ b/tests/snapshots/compile_file__missing_pat.hvm.snap @@ -2,5 +2,5 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/compile_file/missing_pat.hvm --- -At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected '(', '#', '$', , '[', '{', 'λ', 'let', 'match', '*', '|', +, or +At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected '(', '#', '$', , '[', '{', 'λ', 'let', 'match', '*', '|', +, , or  2 | : * diff --git a/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap index 95d979f91..f148075a0 100644 --- a/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap +++ b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap @@ -5,7 +5,7 @@ input_file: tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm TaggedScott: (Parse) = λa λb (#String (b #String.String.cons.head λc #String.String.cons.tail λd λe (match (- c 40) { 0: λf λg (Ok (40, (g, f))); 1+: λk match k { 0: λl λm (Ok (41, (m, l))); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, (s, r))); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb))) a) -(main) = #Result ((Parse * (String.cons 40 (String.cons 50 String.nil))) #Result.Ok.val λd let (e, f) = d; (let (g, h) = f; λi (i, (Parse h g)) e) #Result.Err.err λm (Err m)) +(main) = #Result ((Parse * (String.cons 40 (String.cons 43 String.nil))) #Result.Ok.val λd let (e, f) = d; (let (g, h) = f; λi (i, (Parse h g)) e) #Result.Err.err λm (Err m)) (String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b) @@ -18,7 +18,7 @@ TaggedScott: Scott: (Parse) = λa λb (b λc λd λe (match (- c 40) { 0: λf λg (Ok (40, (g, f))); 1+: λk match k { 0: λl λm (Ok (41, (m, l))); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, (s, r))); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb)) a) -(main) = (Parse * (String.cons 40 (String.cons 50 String.nil)) λd let (e, f) = d; (let (g, h) = f; λi (i, (Parse h g)) e) λm (Err m)) +(main) = (Parse * (String.cons 40 (String.cons 43 String.nil)) λd let (e, f) = d; (let (g, h) = f; λi (i, (Parse h g)) e) λm (Err m)) (String.cons) = λa λb λc λ* (c a b) diff --git a/tests/snapshots/run_file__match_num_adt_tup_parser.hvm.snap b/tests/snapshots/run_file__match_num_adt_tup_parser.hvm.snap index 24e9b5fb5..c775db59d 100644 --- a/tests/snapshots/run_file__match_num_adt_tup_parser.hvm.snap +++ b/tests/snapshots/run_file__match_num_adt_tup_parser.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/match_num_adt_tup_parser.hvm --- -(40, (Err ("2", *))) +(40, (Err ("+", *))) From 4c8a9f915eaed4b64f64b001668db228b83c9fdb Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 27 Feb 2024 19:14:25 +0100 Subject: [PATCH 3/4] [sc-301] Fix after merge --- src/term/transform/float_combinators.rs | 2 +- src/term/transform/linearize_matches.rs | 21 +++++++-------------- src/term/transform/simplify_matches.rs | 2 +- 3 files changed, 9 insertions(+), 16 deletions(-) diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs index 8bcac0718..b0e3e427c 100644 --- a/src/term/transform/float_combinators.rs +++ b/src/term/transform/float_combinators.rs @@ -271,7 +271,7 @@ impl Term { for rule in rules.iter_mut() { for pat in &rule.pats { - debug_assert!(pat.is_detached_num_match()); + debug_assert!(pat.is_native_num_match()); } let arm_detach = match rule.body.go_float(depth + 1, term_info) { diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs index 70c3e988a..2f3650334 100644 --- a/src/term/transform/linearize_matches.rs +++ b/src/term/transform/linearize_matches.rs @@ -13,7 +13,7 @@ impl Ctx<'_> { 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, lift_all_vars); + let res = rule.body.linearize_simple_matches(lift_all_vars); self.info.take_err(res, Some(def_name)); } } @@ -23,24 +23,17 @@ impl Ctx<'_> { } impl Term { - fn linearize_simple_matches(&mut self, ctrs: &Constructors, lift_all_vars: bool) -> Result<(), MatchErr> { + fn linearize_simple_matches(&mut self, lift_all_vars: bool) -> Result<(), MatchErr> { match self { Term::Mat { args: _, rules } => { for rule in rules.iter_mut() { - rule.body.linearize_simple_matches(ctrs, lift_all_vars).unwrap(); + rule.body.linearize_simple_matches(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 => _ = lift_match_vars(self, lift_all_vars), - Type::Adt(_) => { - lift_match_vars(self, lift_all_vars); - } - } - linearize_match_free_vars(self); + lift_match_vars(self, lift_all_vars); } Term::Lam { bod, .. } | Term::Chn { bod, .. } => { - bod.linearize_simple_matches(ctrs, lift_all_vars)?; + bod.linearize_simple_matches(lift_all_vars)?; } Term::Let { pat: Pattern::Var(..), val: fst, nxt: snd } @@ -49,8 +42,8 @@ impl Term { | Term::Sup { fst, snd, .. } | Term::Opx { fst, snd, .. } | Term::App { fun: fst, arg: snd, .. } => { - fst.linearize_simple_matches(ctrs, lift_all_vars)?; - snd.linearize_simple_matches(ctrs, lift_all_vars)?; + fst.linearize_simple_matches(lift_all_vars)?; + snd.linearize_simple_matches(lift_all_vars)?; } Term::Lst { .. } => unreachable!(), diff --git a/src/term/transform/simplify_matches.rs b/src/term/transform/simplify_matches.rs index d8b53451c..c15f880f9 100644 --- a/src/term/transform/simplify_matches.rs +++ b/src/term/transform/simplify_matches.rs @@ -327,7 +327,7 @@ fn switch_rule_submatch_arm(rule: &Rule, ctr: &Pattern, nested_fields: &[Option< Pattern::Num(NumCtr::Succ(_, Some(var))) => vec![Pattern::Var(var.clone())], // Similarly for the default case in a num match Pattern::Var(var) => vec![Pattern::Var(var.clone())], - _ => rule.pats[0].children().cloned().collect::>() + _ => rule.pats[0].children().cloned().collect::>(), }; if pats.is_empty() { // We say that a unit variant always has an unused wildcard nested From 0c509b43678d3fcd7a381b5065c9cabe9b8d1598 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 27 Feb 2024 19:35:19 +0100 Subject: [PATCH 4/4] [sc-301] Some small improvements on mathing code --- src/term/mod.rs | 17 ++----- src/term/net_to_term.rs | 49 ++----------------- src/term/transform/encode_pattern_matching.rs | 2 + src/term/transform/eta_reduction.rs | 32 ++++++------ .../readback_lnet__invalid_mat_mat.hvm.snap | 2 +- tests/snapshots/readback_lnet__match.hvm.snap | 2 +- .../run_file__linearize_match.hvm.snap | 2 +- ...un_file__match_mult_linearization.hvm.snap | 2 +- .../run_lazy__linearize_match.hvm.snap | 2 +- ...un_lazy__match_mult_linearization.hvm.snap | 2 +- 10 files changed, 31 insertions(+), 81 deletions(-) diff --git a/src/term/mod.rs b/src/term/mod.rs index 9dc6dd9d7..6f60c28ce 100644 --- a/src/term/mod.rs +++ b/src/term/mod.rs @@ -298,9 +298,9 @@ impl Term { Term::Str { val: STRINGS.get(str) } } - pub fn native_num_match(arg: Term, zero: Term, succ: Term) -> Term { + pub fn native_num_match(arg: Term, zero: Term, succ: Term, succ_var: Option>) -> Term { let zero = Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: zero }; - let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, None))], body: succ }; + let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, succ_var))], body: succ }; Term::Mat { args: vec![arg], rules: vec![zero, succ] } } @@ -695,16 +695,7 @@ impl Pattern { } pub fn is_native_num_match(&self) -> bool { - if let Pattern::Num(ctr) = self { - match ctr { - NumCtr::Num(0) => true, - NumCtr::Num(_) => false, - NumCtr::Succ(1, None) => true, - NumCtr::Succ(_, _) => false, - } - } else { - false - } + matches!(self, Pattern::Num(NumCtr::Num(0) | NumCtr::Succ(1, _))) } /// True if this pattern has no nested subpatterns. @@ -758,9 +749,7 @@ impl Pattern { match (self, other) { (Pattern::Ctr(a, _), Pattern::Ctr(b, _)) if a == b => true, (Pattern::Num(NumCtr::Num(a)), Pattern::Num(NumCtr::Num(b))) if a == b => true, - (Pattern::Num(NumCtr::Num(_)), Pattern::Num(NumCtr::Num(_))) => false, (Pattern::Num(NumCtr::Succ(a, _)), Pattern::Num(NumCtr::Succ(b, _))) if a == b => true, - (Pattern::Num(NumCtr::Succ(_, _)), Pattern::Num(NumCtr::Succ(_, _))) => false, (Pattern::Tup(_, _), Pattern::Tup(_, _)) => true, (Pattern::Lst(_), Pattern::Lst(_)) => true, (Pattern::Var(_), Pattern::Var(_)) => true, diff --git a/src/term/net_to_term.rs b/src/term/net_to_term.rs index 3fbab7780..f9b8b68d7 100644 --- a/src/term/net_to_term.rs +++ b/src/term/net_to_term.rs @@ -1,7 +1,6 @@ -use super::Rule; use crate::{ net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT}, - term::{num_to_name, term_to_net::Labels, Book, Name, NumCtr, Op, Pattern, Tag, Term}, + term::{num_to_name, term_to_net::Labels, Book, Name, Op, Pattern, Tag, Term}, }; use std::collections::{BTreeSet, HashMap, HashSet}; @@ -103,16 +102,16 @@ impl<'a> Reader<'a> { if *sel_kind != (Con { lab: None }) { // TODO: Is there any case where we expect a different node type here on readback? self.error(ReadbackError::InvalidNumericMatch); - Term::new_native_match(scrutinee, Term::Era, None, Term::Era) + Term::native_num_match(scrutinee, Term::Era, Term::Era, None) } else { let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1))); let succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2))); match succ_term { - Term::Lam { nam, bod, .. } => Term::new_native_match(scrutinee, zero_term, nam, *bod), + Term::Lam { nam, bod, .. } => Term::native_num_match(scrutinee, zero_term, *bod, Some(nam)), _ => { self.error(ReadbackError::InvalidNumericMatch); - Term::new_native_match(scrutinee, zero_term, None, succ_term) + Term::native_num_match(scrutinee, zero_term, succ_term, None) } } } @@ -392,46 +391,6 @@ impl Term { Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {} } } - - /// Creates a new [`Term::Match`] from the given terms. - /// If `scrutinee` is not a `Term::Var`, creates a let binding containing the match in its body - fn new_native_match(arg: Self, zero_term: Self, mut succ_label: Option, mut succ_term: Self) -> Self { - let zero = Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: zero_term }; - - if let Term::Var { nam } = &arg { - if let Some(label) = &succ_label { - let new_label = Name::new(format!("{}-1", nam)); - succ_term.subst(label, &Term::Var { nam: new_label.clone() }); - succ_label = Some(new_label); - } - - let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, Some(succ_label)))], body: succ_term }; - Term::Mat { args: vec![arg], rules: vec![zero, succ] } - } else { - match succ_label { - Some(succ) => { - let match_bind = succ.clone(); - - let new_label = Name::new(format!("{}-1", succ)); - succ_term.subst(&succ, &Term::Var { nam: new_label.clone() }); - succ_label = Some(new_label); - - let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, Some(succ_label)))], body: succ_term }; - - Term::Let { - pat: Pattern::Var(Some(match_bind.clone())), - val: Box::new(arg), - nxt: Box::new(Term::Mat { args: vec![Term::Var { nam: match_bind }], rules: vec![zero, succ] }), - } - } - None => { - let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, None))], body: succ_term }; - - Term::Mat { args: vec![arg], rules: vec![zero, succ] } - } - } - } - } } #[derive(Default)] diff --git a/src/term/transform/encode_pattern_matching.rs b/src/term/transform/encode_pattern_matching.rs index bd386dd00..f673c630f 100644 --- a/src/term/transform/encode_pattern_matching.rs +++ b/src/term/transform/encode_pattern_matching.rs @@ -134,6 +134,7 @@ fn encode_num(arg: Term, mut rules: Vec) -> Term { Term::sub_num(arg.unwrap(), *val), rule.body, go(rules, last_rule, Some(*val), None), + None, ) } // Middle match @@ -147,6 +148,7 @@ fn encode_num(arg: Term, mut rules: Vec) -> Term { Term::sub_num(Term::Var { nam: pred_nam }, val.wrapping_sub(prev_num).wrapping_sub(1)), rule.body, go(rules, last_rule, Some(*val), None), + None, ), ) } diff --git a/src/term/transform/eta_reduction.rs b/src/term/transform/eta_reduction.rs index aa0b9e11b..a99a5760c 100644 --- a/src/term/transform/eta_reduction.rs +++ b/src/term/transform/eta_reduction.rs @@ -37,34 +37,34 @@ impl Term { _ => {} } } - Term::Lam { bod, .. } => bod.eta_reduction(), - Term::Let { pat: _, val, nxt } | Term::Dup { tag: _, fst: _, snd: _, val, nxt } => { - val.eta_reduction(); - nxt.eta_reduction(); - } - Term::App { fun: fst, arg: snd, .. } - | Term::Tup { fst, snd } - | Term::Sup { fst, snd, .. } - | Term::Opx { op: _, fst, snd } => { - fst.eta_reduction(); - snd.eta_reduction(); - } + Term::Lam { tag: _, nam: None, bod } => bod.eta_reduction(), + Term::Mat { args, rules } => { for arg in args { arg.eta_reduction(); } for rule in rules { - for pat in &rule.pats { - debug_assert!(pat.is_native_num_match()); - } rule.body.eta_reduction(); } } + Term::Lst { els } => { + for el in els { + el.eta_reduction(); + } + } + Term::Let { val: fst, nxt: snd, .. } + | Term::Dup { val: fst, nxt: snd, .. } + | Term::App { fun: fst, arg: snd, .. } + | Term::Tup { fst, snd } + | Term::Sup { fst, snd, .. } + | Term::Opx { fst, snd, .. } => { + fst.eta_reduction(); + snd.eta_reduction(); + } Term::Lnk { .. } | Term::Var { .. } | Term::Num { .. } | Term::Str { .. } - | Term::Lst { .. } | Term::Ref { .. } | Term::Era | Term::Err => {} diff --git a/tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap b/tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap index 8e712c1f4..432597a28 100644 --- a/tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap +++ b/tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap @@ -5,4 +5,4 @@ input_file: tests/golden_tests/readback_lnet/invalid_mat_mat.hvm Readback Warning: Invalid Numeric Match (4 occurrences) -λa match match { 0: 3; 1+: 4 } { 0: ; 1+: } +λa match match { 0: 3; 1+*: 4 } { 0: ; 1+: } diff --git a/tests/snapshots/readback_lnet__match.hvm.snap b/tests/snapshots/readback_lnet__match.hvm.snap index 4ffacc30f..092fa4818 100644 --- a/tests/snapshots/readback_lnet__match.hvm.snap +++ b/tests/snapshots/readback_lnet__match.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/readback_lnet/match.hvm --- -let b = 1; match b { 0: λa a; 1+b-1: b-1 } +match 1 { 0: λa a; 1+b: b } diff --git a/tests/snapshots/run_file__linearize_match.hvm.snap b/tests/snapshots/run_file__linearize_match.hvm.snap index dd151e88e..878af8629 100644 --- a/tests/snapshots/run_file__linearize_match.hvm.snap +++ b/tests/snapshots/run_file__linearize_match.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/linearize_match.hvm --- -λa match a { 0: λb b; 1+a-1: λd (+ a-1 d) } +λa match a { 0: λb b; 1+c: λd (+ c d) } diff --git a/tests/snapshots/run_file__match_mult_linearization.hvm.snap b/tests/snapshots/run_file__match_mult_linearization.hvm.snap index 4cd7db522..582ff27c8 100644 --- a/tests/snapshots/run_file__match_mult_linearization.hvm.snap +++ b/tests/snapshots/run_file__match_mult_linearization.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/match_mult_linearization.hvm --- -λa match a { 0: λb λc λd (+ (+ b c) d); 1+a-1: λf λg λh (+ (+ (+ a-1 f) g) h) } +λa match a { 0: λb λc λd (+ (+ b c) d); 1+e: λf λg λh (+ (+ (+ e f) g) h) } diff --git a/tests/snapshots/run_lazy__linearize_match.hvm.snap b/tests/snapshots/run_lazy__linearize_match.hvm.snap index d7fe41f28..5b74b2fc2 100644 --- a/tests/snapshots/run_lazy__linearize_match.hvm.snap +++ b/tests/snapshots/run_lazy__linearize_match.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_lazy/linearize_match.hvm --- -λa match a { 0: λb b; 1+a-1: λd (+ a-1 d) } +λa match a { 0: λb b; 1+c: λd (+ c d) } diff --git a/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap b/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap index 8d5cef53d..99c675ac8 100644 --- a/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap +++ b/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_lazy/match_mult_linearization.hvm --- -λa match a { 0: λb λc λd (+ (+ b c) d); 1+a-1: λf λg λh (+ (+ (+ a-1 f) g) h) } +λa match a { 0: λb λc λd (+ (+ b c) d); 1+e: λf λg λh (+ (+ (+ e f) g) h) }