diff --git a/.gitignore b/.gitignore index ea8c4bf7..811e6f6e 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ /target +*.snap.new diff --git a/cspell.json b/cspell.json index 42bdc6ae..fa3e07e3 100644 --- a/cspell.json +++ b/cspell.json @@ -15,6 +15,7 @@ "ctrs", "Dall", "datatypes", + "Deque", "desugared", "desugars", "dref", @@ -85,6 +86,13 @@ "walkdir", "wopts" ], - "files": ["**/*.rs", "**/*.md"], - "ignoreRegExpList": ["HexValues", "/λ/g", "/-O/g"] + "files": [ + "**/*.rs", + "**/*.md" + ], + "ignoreRegExpList": [ + "HexValues", + "/λ/g", + "/-O/g" + ] } diff --git a/src/diagnostics.rs b/src/diagnostics.rs index e1995f24..811e867b 100644 --- a/src/diagnostics.rs +++ b/src/diagnostics.rs @@ -16,7 +16,9 @@ pub struct Diagnostics { #[derive(Debug, Clone, Copy)] pub struct DiagnosticsConfig { pub verbose: bool, - pub match_only_vars: Severity, + pub irrefutable_match: Severity, + pub redundant_match: Severity, + pub unreachable_match: Severity, pub unused_definition: Severity, pub repeated_bind: Severity, pub mutual_recursion_cycle: Severity, @@ -49,7 +51,9 @@ pub enum Severity { #[derive(Debug, Clone, Copy)] pub enum WarningType { - MatchOnlyVars, + IrrefutableMatch, + RedundantMatch, + UnreachableMatch, UnusedDefinition, RepeatedBind, MutualRecursionCycle, @@ -221,7 +225,9 @@ impl From for Diagnostics { impl DiagnosticsConfig { pub fn new(severity: Severity, verbose: bool) -> Self { Self { - match_only_vars: severity, + irrefutable_match: severity, + redundant_match: severity, + unreachable_match: severity, unused_definition: severity, repeated_bind: severity, mutual_recursion_cycle: severity, @@ -231,10 +237,12 @@ impl DiagnosticsConfig { pub fn warning_severity(&self, warn: WarningType) -> Severity { match warn { - WarningType::MatchOnlyVars => self.match_only_vars, WarningType::UnusedDefinition => self.unused_definition, WarningType::RepeatedBind => self.repeated_bind, WarningType::MutualRecursionCycle => self.mutual_recursion_cycle, + WarningType::IrrefutableMatch => self.irrefutable_match, + WarningType::RedundantMatch => self.redundant_match, + WarningType::UnreachableMatch => self.unreachable_match, } } } @@ -256,3 +264,9 @@ impl ToStringVerbose for &str { self.to_string() } } + +impl ToStringVerbose for String { + fn to_string_verbose(&self, _verbose: bool) -> String { + self.clone() + } +} diff --git a/src/lib.rs b/src/lib.rs index 318ccad2..939fe460 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -66,55 +66,32 @@ pub fn desugar_book( let mut ctx = Ctx::new(book, diagnostics_cfg); ctx.check_shared_names(); + ctx.set_entrypoint(); + + ctx.book.encode_adts(opts.adt_encoding); + + ctx.book.resolve_ctrs_in_pats(); + ctx.check_unbound_ctr()?; + ctx.check_ctrs_arities()?; + ctx.apply_args(args)?; ctx.book.apply_use(); - ctx.book.encode_adts(opts.adt_encoding); ctx.book.encode_builtins(); - ctx.book.resolve_ctrs_in_pats(); ctx.resolve_refs()?; - ctx.check_repeated_binds(); - ctx.check_match_arity()?; - ctx.check_unbound_pats()?; + ctx.fix_match_terms()?; + ctx.desugar_match_defs()?; - ctx.book.desugar_let_destructors(); - ctx.book.desugar_implicit_match_binds(); - - ctx.check_ctrs_arities()?; - // Must be between [`Book::desugar_implicit_match_binds`] and [`Ctx::linearize_matches`] ctx.check_unbound_vars()?; - ctx.book.convert_match_def_to_term(); - - // TODO: We give variables fresh names before the match - // simplification to avoid `foo a a = a` binding to the wrong - // variable (it should be the second `a`). Ideally we'd like this - // pass to create the binds in the correct order, but to do that we - // have to reverse the order of the created let expressions when we - // have multiple consecutive var binds without a match in between, - // and I couldn't think of a simple way of doing that. - // - // In the paper this is not a problem because all var matches are - // pushed to the end, so it only needs to fix it in the irrefutable - // rule case. We could maybe do the opposite and do all var matches - // first, when it would also become easy to deal with. But this - // would potentially generate suboptimal lambda terms, need to think - // more about it. - // - // We technically still generate the let bindings in the wrong order - // but since lets can float between the binds it uses in its body - // and the places where its variable is used, this is not a problem. - ctx.book.make_var_names_unique(); - ctx.simplify_matches()?; - if opts.linearize_matches.enabled() { - ctx.book.linearize_simple_matches(opts.linearize_matches.is_extra()); + ctx.book.linearize_matches(opts.linearize_matches.is_extra()); } - ctx.book.encode_simple_matches(opts.adt_encoding); + ctx.book.encode_matches(opts.adt_encoding); // sanity check ctx.check_unbound_vars()?; diff --git a/src/main.rs b/src/main.rs index c62dc27a..a28e74f1 100644 --- a/src/main.rs +++ b/src/main.rs @@ -213,8 +213,10 @@ impl OptArgs { #[derive(clap::ValueEnum, Clone, Debug)] pub enum WarningArgs { All, - UnusedDefs, - MatchOnlyVars, + IrrefutableMatch, + RedundantMatch, + UnreachableMatch, + UnusedDefinition, RepeatedBind, MutualRecursionCycle, } @@ -250,6 +252,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> { let mut book = load_book(&path)?; check_book(&mut book)?; } + Mode::Compile { path, comp_opts, warn_opts, lazy_mode } => { let diagnostics_cfg = set_warning_cfg_from_cli( DiagnosticsConfig::new(Severity::Warning, arg_verbose), @@ -268,6 +271,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> { eprint!("{}", compile_res.diagnostics); println!("{}", compile_res.core_book); } + Mode::Desugar { path, comp_opts, warn_opts, lazy_mode } => { let diagnostics_cfg = set_warning_cfg_from_cli( DiagnosticsConfig::new(Severity::Warning, arg_verbose), @@ -286,6 +290,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> { eprint!("{diagnostics}"); println!("{book}"); } + Mode::Run { path, max_memory, @@ -369,15 +374,19 @@ fn set_warning_cfg_from_cli( fn set(cfg: &mut DiagnosticsConfig, severity: Severity, cli_val: WarningArgs, lazy_mode: bool) { match cli_val { WarningArgs::All => { + cfg.irrefutable_match = severity; + cfg.redundant_match = severity; + cfg.unreachable_match = severity; cfg.unused_definition = severity; - cfg.match_only_vars = severity; cfg.repeated_bind = severity; if !lazy_mode { cfg.mutual_recursion_cycle = severity; } } - WarningArgs::UnusedDefs => cfg.unused_definition = severity, - WarningArgs::MatchOnlyVars => cfg.match_only_vars = severity, + WarningArgs::IrrefutableMatch => cfg.irrefutable_match = severity, + WarningArgs::RedundantMatch => cfg.redundant_match = severity, + WarningArgs::UnreachableMatch => cfg.unreachable_match = severity, + WarningArgs::UnusedDefinition => cfg.unused_definition = severity, WarningArgs::RepeatedBind => cfg.repeated_bind = severity, WarningArgs::MutualRecursionCycle => cfg.mutual_recursion_cycle = severity, } diff --git a/src/term/builtins.rs b/src/term/builtins.rs index 2d8f580b..e14941d1 100644 --- a/src/term/builtins.rs +++ b/src/term/builtins.rs @@ -1,4 +1,4 @@ -use super::{parser::parse_book, Book, Name, NumCtr, Pattern, Term}; +use super::{parser::parse_book, Book, Name, Pattern, Term}; const BUILTINS: &str = include_str!(concat!(env!("CARGO_MANIFEST_DIR"), "/src/term/builtins.hvm")); @@ -38,46 +38,16 @@ impl Book { impl Term { fn encode_builtins(&mut self) { - match self { + Term::recursive_call(move || match self { Term::Lst { els } => *self = Term::encode_list(std::mem::take(els)), Term::Str { val } => *self = Term::encode_str(val), Term::Nat { val } => *self = Term::encode_nat(*val), - Term::Let { pat, val, nxt } => { - pat.encode_builtins(); - val.encode_builtins(); - nxt.encode_builtins(); - } - Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.encode_builtins(), - Term::App { fun: fst, arg: snd, .. } - | Term::Opx { fst, snd, .. } - | Term::Dup { val: fst, nxt: snd, .. } => { - fst.encode_builtins(); - snd.encode_builtins(); - } - Term::Sup { els, .. } | Term::Tup { els } => { - for el in els { - el.encode_builtins(); + _ => { + for child in self.children_mut() { + child.encode_builtins(); } } - Term::Mat { args, rules } => { - for arg in args { - arg.encode_builtins(); - } - for rule in rules { - for pat in &mut rule.pats { - pat.encode_builtins(); - } - rule.body.encode_builtins(); - } - } - Term::Use { .. } - | Term::Var { .. } - | Term::Lnk { .. } - | Term::Ref { .. } - | Term::Num { .. } - | Term::Era - | Term::Err => {} - } + }) } fn encode_list(elements: Vec) -> Term { @@ -133,7 +103,7 @@ impl Pattern { let lnil = Pattern::Ctr(Name::from(SNIL), vec![]); str.chars().rfold(lnil, |tail, head| { - let head = Pattern::Num(NumCtr::Num(head as u64)); + let head = Pattern::Num(head as u64); Pattern::Ctr(Name::from(SCONS), vec![head, tail]) }) } diff --git a/src/term/check/ctrs_arities.rs b/src/term/check/ctrs_arities.rs index 5cdcbd58..bdf785bf 100644 --- a/src/term/check/ctrs_arities.rs +++ b/src/term/check/ctrs_arities.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use crate::{ diagnostics::{Diagnostics, ToStringVerbose}, - term::{Book, Ctx, Name, Pattern, Term}, + term::{Book, Ctx, Name, Pattern}, }; pub struct CtrArityMismatchErr { @@ -26,8 +26,6 @@ impl Ctx<'_> { let res = pat.check_ctrs_arities(&arities); self.info.take_rule_err(res, def_name.clone()); } - let res = rule.body.check_ctrs_arities(&arities); - self.info.take_rule_err(res, def_name.clone()); } } @@ -70,20 +68,6 @@ impl Pattern { } } -impl Term { - pub fn check_ctrs_arities(&self, arities: &HashMap) -> Result<(), CtrArityMismatchErr> { - Term::recursive_call(move || { - for pat in self.patterns() { - pat.check_ctrs_arities(arities)?; - } - for child in self.children() { - child.check_ctrs_arities(arities)?; - } - Ok(()) - }) - } -} - impl ToStringVerbose for CtrArityMismatchErr { fn to_string_verbose(&self, _verbose: bool) -> String { format!( diff --git a/src/term/check/match_arity.rs b/src/term/check/match_arity.rs deleted file mode 100644 index 72b038e3..00000000 --- a/src/term/check/match_arity.rs +++ /dev/null @@ -1,64 +0,0 @@ -use crate::{ - diagnostics::{Diagnostics, ToStringVerbose}, - term::{Ctx, Definition, Term}, -}; - -pub struct MatchArityMismatchErr { - expected: usize, - found: usize, -} - -impl Ctx<'_> { - /// Checks that the number of arguments in every pattern matching rule is consistent. - pub fn check_match_arity(&mut self) -> Result<(), Diagnostics> { - self.info.start_pass(); - - for (def_name, def) in self.book.defs.iter() { - let res = def.check_match_arity(); - self.info.take_rule_err(res, def_name.clone()); - } - - self.info.fatal(()) - } -} - -impl Definition { - pub fn check_match_arity(&self) -> Result<(), MatchArityMismatchErr> { - let expected = self.arity(); - for rule in &self.rules { - let found = rule.arity(); - if found != expected { - return Err(MatchArityMismatchErr { found, expected }); - } - rule.body.check_match_arity()?; - } - Ok(()) - } -} - -impl Term { - pub fn check_match_arity(&self) -> Result<(), MatchArityMismatchErr> { - Term::recursive_call(move || { - if let Term::Mat { args, rules } = self { - let expected = args.len(); - for rule in rules { - let found = rule.pats.len(); - if found != expected { - return Err(MatchArityMismatchErr { found, expected }); - } - } - } - - for child in self.children() { - child.check_match_arity()?; - } - Ok(()) - }) - } -} - -impl ToStringVerbose for MatchArityMismatchErr { - fn to_string_verbose(&self, _verbose: bool) -> String { - format!("Arity mismatch in pattern matching. Expected {} patterns, found {}.", self.expected, self.found) - } -} diff --git a/src/term/check/mod.rs b/src/term/check/mod.rs index f5913fa4..150d68f9 100644 --- a/src/term/check/mod.rs +++ b/src/term/check/mod.rs @@ -1,8 +1,5 @@ pub mod ctrs_arities; -pub mod match_arity; -pub mod repeated_bind; pub mod set_entrypoint; pub mod shared_names; -pub mod type_check; -pub mod unbound_pats; +pub mod unbound_ctrs; pub mod unbound_vars; diff --git a/src/term/check/repeated_bind.rs b/src/term/check/repeated_bind.rs deleted file mode 100644 index 60c74b5d..00000000 --- a/src/term/check/repeated_bind.rs +++ /dev/null @@ -1,77 +0,0 @@ -use crate::{ - diagnostics::{ToStringVerbose, WarningType}, - term::{Ctx, Name, Term}, -}; -use std::collections::HashSet; - -#[derive(Debug, Clone)] -pub enum RepeatedBindWarn { - Rule(Name), - Match(Name), -} - -impl Ctx<'_> { - /// Checks that there are no unbound variables in all definitions. - pub fn check_repeated_binds(&mut self) { - for (def_name, def) in &self.book.defs { - for rule in &def.rules { - let mut binds = HashSet::new(); - for pat in &rule.pats { - for nam in pat.binds().flatten() { - if !binds.insert(nam) { - self.info.add_rule_warning( - RepeatedBindWarn::Rule(nam.clone()), - WarningType::RepeatedBind, - def_name.clone(), - ); - } - } - } - - let mut repeated_in_matches = Vec::new(); - rule.body.check_repeated_binds(&mut repeated_in_matches); - - for warn in repeated_in_matches { - self.info.add_rule_warning(warn, WarningType::RepeatedBind, def_name.clone()); - } - } - } - } -} - -impl Term { - pub fn check_repeated_binds(&self, repeated: &mut Vec) { - Term::recursive_call(|| match self { - Term::Mat { args, rules } => { - for arg in args { - arg.check_repeated_binds(repeated); - } - - for rule in rules { - let mut binds = HashSet::new(); - for pat in &rule.pats { - for nam in pat.binds().flatten() { - if !binds.insert(nam) { - repeated.push(RepeatedBindWarn::Match(nam.clone())); - } - } - } - } - } - _ => { - for child in self.children() { - child.check_repeated_binds(repeated); - } - } - }) - } -} - -impl ToStringVerbose for RepeatedBindWarn { - fn to_string_verbose(&self, _verbose: bool) -> String { - match self { - RepeatedBindWarn::Rule(bind) => format!("Repeated bind inside rule pattern: '{bind}'."), - RepeatedBindWarn::Match(bind) => format!("Repeated bind inside match arm: '{bind}'."), - } - } -} diff --git a/src/term/check/type_check.rs b/src/term/check/type_check.rs deleted file mode 100644 index e903693a..00000000 --- a/src/term/check/type_check.rs +++ /dev/null @@ -1,58 +0,0 @@ -use crate::{ - diagnostics::ToStringVerbose, - term::{Constructors, Name, Pattern, Rule, Type}, -}; -use indexmap::IndexMap; - -pub type DefinitionTypes = IndexMap>; - -#[derive(Debug)] -pub struct TypeMismatchErr { - expected: Type, - found: Type, -} - -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, - ctrs: &Constructors, -) -> Result { - let mut arg_type = Type::Any; - for pat in pats.into_iter() { - arg_type = unify(arg_type, pat.to_type(ctrs))?; - } - Ok(arg_type) -} - -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(a), Type::Tup(b)) if a == b => Ok(Type::Tup(a)), - - (old, new) => Err(TypeMismatchErr { found: new, expected: old }), - } -} - -impl ToStringVerbose for TypeMismatchErr { - fn to_string_verbose(&self, _verbose: bool) -> String { - format!("Type mismatch in pattern matching. Expected '{}', found '{}'.", self.expected, self.found) - } -} diff --git a/src/term/check/unbound_pats.rs b/src/term/check/unbound_ctrs.rs similarity index 69% rename from src/term/check/unbound_pats.rs rename to src/term/check/unbound_ctrs.rs index 9dcb6a16..59e0bf62 100644 --- a/src/term/check/unbound_pats.rs +++ b/src/term/check/unbound_ctrs.rs @@ -1,6 +1,6 @@ use crate::{ diagnostics::{Diagnostics, ToStringVerbose}, - term::{Ctx, Name, Pattern, Term}, + term::{Ctx, Name, Pattern}, }; use std::collections::HashSet; @@ -8,8 +8,9 @@ use std::collections::HashSet; pub struct UnboundCtrErr(Name); impl Ctx<'_> { - /// Check if the constructors in rule patterns or match patterns are defined. - pub fn check_unbound_pats(&mut self) -> Result<(), Diagnostics> { + /// Check if the constructors in rule patterns are defined. + /// Match terms are not checked since unbounds there are treated as vars. + pub fn check_unbound_ctr(&mut self) -> Result<(), Diagnostics> { self.info.start_pass(); let is_ctr = |nam: &Name| self.book.ctrs.contains_key(nam); @@ -19,9 +20,6 @@ impl Ctx<'_> { let res = pat.check_unbounds(&is_ctr); self.info.take_rule_err(res, def_name.clone()); } - - let res = rule.body.check_unbound_pats(&is_ctr); - self.info.take_rule_err(res, def_name.clone()); } } @@ -51,20 +49,6 @@ impl Pattern { } } -impl Term { - pub fn check_unbound_pats(&self, is_ctr: &impl Fn(&Name) -> bool) -> Result<(), UnboundCtrErr> { - Term::recursive_call(move || { - for pat in self.patterns() { - pat.check_unbounds(is_ctr)?; - } - for child in self.children() { - child.check_unbound_pats(is_ctr)?; - } - Ok(()) - }) - } -} - impl ToStringVerbose for UnboundCtrErr { fn to_string_verbose(&self, _verbose: bool) -> String { format!("Unbound constructor '{}'.", self.0) diff --git a/src/term/display.rs b/src/term/display.rs index 5dc647d3..21af4e52 100644 --- a/src/term/display.rs +++ b/src/term/display.rs @@ -1,4 +1,4 @@ -use super::{Book, Definition, Name, NumCtr, Op, Pattern, Rule, Tag, Term, Type}; +use super::{Book, Definition, Name, NumCtr, Op, Pattern, Rule, Tag, Term}; use std::{fmt, ops::Deref}; /* Some aux structures for things that are not so simple to display */ @@ -50,8 +50,8 @@ impl fmt::Display for Term { write!(f, "{}λ${} {}", tag.display_padded(), var_as_str(nam), bod) } Term::Lnk { nam } => write!(f, "${nam}"), - Term::Let { pat, val, nxt } => { - write!(f, "let {} = {}; {}", pat, val, nxt) + Term::Let { nam, val, nxt } => { + write!(f, "let {} = {}; {}", var_as_str(nam), val, nxt) } Term::Use { nam, val, nxt } => { write!(f, "use {} = {}; {}", nam, val, nxt) @@ -60,17 +60,26 @@ impl fmt::Display for Term { Term::App { tag, fun, arg } => { write!(f, "{}({} {})", tag.display_padded(), fun.display_app(tag), arg) } - Term::Mat { args, rules } => { + Term::Mat { arg, rules } => { write!( f, "match {} {{ {} }}", - DisplayJoin(|| args, ", "), - DisplayJoin( - || rules.iter().map(|rule| display!("{}: {}", DisplayJoin(|| &rule.pats, " "), rule.body)), - "; " - ), + arg, + DisplayJoin(|| rules.iter().map(|rule| display!("{}: {}", var_as_str(&rule.0), rule.2)), "; "), ) } + Term::Swt { arg, rules } => { + write!( + f, + "switch {} {{ {} }}", + arg, + DisplayJoin(|| rules.iter().map(|rule| display!("{}: {}", rule.0, rule.1)), "; "), + ) + } + Term::Ltp { bnd, val, nxt } => { + write!(f, "let ({}) = {}; {}", DisplayJoin(|| bnd.iter().map(var_as_str), ", "), val, nxt) + } + Term::Tup { els } => write!(f, "({})", DisplayJoin(|| els.iter(), ", "),), Term::Dup { tag, bnd, val, nxt } => { write!(f, "let {}{{{}}} = {}; {}", tag, DisplayJoin(|| bnd.iter().map(var_as_str), " "), val, nxt) } @@ -84,7 +93,6 @@ impl fmt::Display for Term { Term::Opx { op, fst, snd } => { write!(f, "({} {} {})", op, fst, snd) } - Term::Tup { els } => write!(f, "({})", DisplayJoin(|| els.iter(), ", "),), Term::Lst { els } => write!(f, "[{}]", DisplayJoin(|| els.iter(), ", "),), Term::Err => write!(f, ""), }) @@ -145,9 +153,7 @@ impl fmt::Display for NumCtr { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { 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}"), + NumCtr::Succ(_) => write!(f, "_"), } } } @@ -181,18 +187,6 @@ impl fmt::Display for Name { } } -impl fmt::Display for Type { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - match self { - Type::Any => write!(f, "any"), - Type::Tup(n) => write!(f, "tup{n}"), - Type::Num => write!(f, "num"), - Type::NumSucc(n) => write!(f, "{n}+"), - Type::Adt(nam) => write!(f, "{nam}"), - } - } -} - impl Term { fn display_app<'a>(&'a self, tag: &'a Tag) -> impl fmt::Display + 'a { DisplayFn(move |f| match self { diff --git a/src/term/mod.rs b/src/term/mod.rs index f3f4fcd2..a35d5345 100644 --- a/src/term/mod.rs +++ b/src/term/mod.rs @@ -1,4 +1,4 @@ -use self::{check::type_check::infer_match_arg_type, parser::lexer::STRINGS}; +use self::parser::lexer::STRINGS; use crate::{ diagnostics::{Diagnostics, DiagnosticsConfig}, term::builtins::*, @@ -7,11 +7,7 @@ use crate::{ use indexmap::{IndexMap, IndexSet}; use interner::global::GlobalString; use itertools::Itertools; -use std::{ - borrow::Cow, - collections::{HashMap, HashSet}, - ops::Deref, -}; +use std::{borrow::Cow, collections::HashMap, ops::Deref}; pub mod builtins; pub mod check; @@ -92,7 +88,7 @@ pub enum Term { nam: Name, }, Let { - pat: Pattern, + nam: Option, val: Box, nxt: Box, }, @@ -106,6 +102,12 @@ pub enum Term { fun: Box, arg: Box, }, + /// "let tup" tuple destructor + Ltp { + bnd: Vec>, + val: Box, + nxt: Box, + }, Tup { els: Vec, }, @@ -137,9 +139,15 @@ pub enum Term { fst: Box, snd: Box, }, + /// Pattern matching on an ADT. Mat { - args: Vec, - rules: Vec, + arg: Box, + rules: Vec<(Option, Vec>, Term)>, + }, + /// Native pattern matching on numbers + Swt { + arg: Box, + rules: Vec<(NumCtr, Term)>, }, Ref { nam: Name, @@ -153,16 +161,16 @@ pub enum Term { pub enum Pattern { Var(Option), Ctr(Name, Vec), - Num(NumCtr), + Num(u64), Tup(Vec), Lst(Vec), Str(GlobalString), } -#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] pub enum NumCtr { Num(u64), - Succ(u64, Option>), + Succ(Option), } #[derive(Debug, Clone, PartialEq, Eq, Hash)] @@ -193,21 +201,6 @@ pub enum Op { Shr, } -/// Pattern types. -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum Type { - /// Variables/wildcards. - Any, - /// A native tuple. - Tup(usize), - /// 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), -} - /// A user defined datatype #[derive(Debug, Clone, Default)] pub struct Adt { @@ -273,6 +266,12 @@ impl PartialEq for Name { } } +impl PartialEq<&str> for Name { + fn eq(&self, other: &&str) -> bool { + self == other + } +} + impl PartialEq> for Name { fn eq(&self, other: &Option) -> bool { if let Some(other) = other.as_ref() { self == other } else { false } @@ -311,9 +310,10 @@ impl Clone for Term { Self::Var { nam } => Self::Var { nam: nam.clone() }, Self::Chn { tag, nam, bod } => Self::Chn { tag: tag.clone(), nam: nam.clone(), bod: bod.clone() }, Self::Lnk { nam } => Self::Lnk { nam: nam.clone() }, - Self::Let { pat, val, nxt } => Self::Let { pat: pat.clone(), val: val.clone(), nxt: nxt.clone() }, + Self::Let { nam, val, nxt } => Self::Let { nam: nam.clone(), val: val.clone(), nxt: nxt.clone() }, Self::Use { nam, val, nxt } => Self::Use { nam: nam.clone(), val: val.clone(), nxt: nxt.clone() }, Self::App { tag, fun, arg } => Self::App { tag: tag.clone(), fun: fun.clone(), arg: arg.clone() }, + Self::Ltp { bnd, val, nxt } => Self::Ltp { bnd: bnd.clone(), val: val.clone(), nxt: nxt.clone() }, Self::Tup { els } => Self::Tup { els: els.clone() }, Self::Dup { tag, bnd, val, nxt } => { Self::Dup { tag: tag.clone(), bnd: bnd.clone(), val: val.clone(), nxt: nxt.clone() } @@ -324,7 +324,8 @@ impl Clone for Term { Self::Str { val } => Self::Str { val: val.clone() }, Self::Lst { els } => Self::Lst { els: els.clone() }, Self::Opx { op, fst, snd } => Self::Opx { op: *op, fst: fst.clone(), snd: snd.clone() }, - Self::Mat { args, rules } => Self::Mat { args: args.clone(), rules: rules.clone() }, + Self::Mat { arg, rules } => Self::Mat { arg: arg.clone(), rules: rules.clone() }, + Self::Swt { arg, rules } => Self::Swt { arg: arg.clone(), rules: rules.clone() }, Self::Ref { nam } => Self::Ref { nam: nam.clone() }, Self::Era => Self::Era, Self::Err => Self::Err, @@ -348,12 +349,15 @@ impl Drop for Term { stack.push(std::mem::take(fst.as_mut())); stack.push(std::mem::take(snd.as_mut())); } - Term::Mat { args, rules } => { - for arg in std::mem::take(args).into_iter() { - stack.push(arg); + Term::Mat { arg, rules } => { + stack.push(std::mem::take(arg)); + for (_ctr, _fields, body) in std::mem::take(rules).into_iter() { + stack.push(body); } - - for Rule { body, .. } in std::mem::take(rules).into_iter() { + } + Term::Swt { arg, rules } => { + stack.push(std::mem::take(arg)); + for (_nam, body) in std::mem::take(rules).into_iter() { stack.push(body); } } @@ -432,10 +436,10 @@ impl Term { Term::Str { val: STRINGS.get(str) } } - 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, succ_var))], body: succ }; - Term::Mat { args: vec![arg], rules: vec![zero, succ] } + pub fn switch(arg: Term, zero: Term, succ: Term, succ_var: Option) -> Term { + let zero = (NumCtr::Num(0), zero); + let succ = (NumCtr::Succ(succ_var), succ); + Term::Swt { arg: Box::new(arg), rules: vec![zero, succ] } } pub fn sub_num(arg: Term, val: u64) -> Term { @@ -456,13 +460,19 @@ impl Term { /* Iterators */ pub fn children(&self) -> impl DoubleEndedIterator + Clone { - multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat }); + multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt }); match self { - Term::Mat { args, rules } => ChildrenIter::Mat(args.iter().chain(rules.iter().map(|r| &r.body))), + Term::Mat { arg, rules } => { + ChildrenIter::Mat([arg.as_ref()].into_iter().chain(rules.iter().map(|r| &r.2))) + } + Term::Swt { arg, rules } => { + ChildrenIter::Swt([arg.as_ref()].into_iter().chain(rules.iter().map(|r| &r.1))) + } Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => ChildrenIter::Vec(els), Term::Let { val: fst, nxt: snd, .. } | Term::Use { val: fst, nxt: snd, .. } | Term::App { fun: fst, arg: snd, .. } + | Term::Ltp { val: fst, nxt: snd, .. } | Term::Dup { val: fst, nxt: snd, .. } | Term::Opx { fst, snd, .. } => ChildrenIter::Two([fst.as_ref(), snd.as_ref()]), Term::Lam { bod, .. } | Term::Chn { bod, .. } => ChildrenIter::One([bod.as_ref()]), @@ -478,15 +488,19 @@ impl Term { } pub fn children_mut(&mut self) -> impl DoubleEndedIterator { - multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat }); + multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt }); match self { - Term::Mat { args, rules } => { - ChildrenIter::Mat(args.iter_mut().chain(rules.iter_mut().map(|r| &mut r.body))) + Term::Mat { arg, rules } => { + ChildrenIter::Mat([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.2))) + } + Term::Swt { arg, rules } => { + ChildrenIter::Swt([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.1))) } Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => ChildrenIter::Vec(els), Term::Let { val: fst, nxt: snd, .. } | Term::Use { val: fst, nxt: snd, .. } | Term::App { fun: fst, arg: snd, .. } + | Term::Ltp { val: fst, nxt: snd, .. } | Term::Dup { val: fst, nxt: snd, .. } | Term::Opx { fst, snd, .. } => ChildrenIter::Two([fst.as_mut(), snd.as_mut()]), Term::Lam { bod, .. } | Term::Chn { bod, .. } => ChildrenIter::One([bod.as_mut()]), @@ -511,23 +525,30 @@ impl Term { &self, ) -> impl DoubleEndedIterator> + Clone)> + Clone { - multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat }); - multi_iterator!(BindsIter { Zero, One, Dup, Pat, Rule }); + multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt }); + multi_iterator!(BindsIter { Zero, One, Dup, Mat }); match self { - Term::Mat { args, rules } => ChildrenIter::Mat( - args - .iter() - .map(|arg| (arg, BindsIter::Zero([]))) - .chain(rules.iter().map(|r| (&r.body, BindsIter::Rule(r.pats.iter().flat_map(|p| p.binds()))))), + Term::Mat { arg, rules } => ChildrenIter::Mat( + [(arg.as_ref(), BindsIter::Zero([]))] + .into_iter() + .chain(rules.iter().map(|r| (&r.2, BindsIter::Mat(r.1.iter())))), ), + Term::Swt { arg, rules } => { + ChildrenIter::Swt([(arg.as_ref(), BindsIter::Zero([]))].into_iter().chain(rules.iter().map(|r| { + match &r.0 { + NumCtr::Num(_) => (&r.1, BindsIter::Zero([])), + NumCtr::Succ(nam) => (&r.1, BindsIter::One([nam])), + } + }))) + } Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => { ChildrenIter::Vec(els.iter().map(|el| (el, BindsIter::Zero([])))) } - Term::Let { pat, val, nxt, .. } => { - ChildrenIter::Two([(val.as_ref(), BindsIter::Zero([])), (nxt.as_ref(), BindsIter::Pat(pat.binds()))]) + Term::Let { nam, val, nxt, .. } => { + ChildrenIter::Two([(val.as_ref(), BindsIter::Zero([])), (nxt.as_ref(), BindsIter::One([nam]))]) } - Term::Use { .. } => ChildrenIter::Zero([]), - Term::Dup { bnd, val, nxt, .. } => { + Term::Use { .. } => todo!(), + Term::Ltp { bnd, val, nxt, .. } | Term::Dup { bnd, val, nxt, .. } => { ChildrenIter::Two([(val.as_ref(), BindsIter::Zero([])), (nxt.as_ref(), BindsIter::Dup(bnd))]) } Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => { @@ -550,22 +571,28 @@ impl Term { &mut self, ) -> impl DoubleEndedIterator> + Clone)> { - multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat }); - multi_iterator!(BindsIter { Zero, One, Dup, Pat, Rule }); + multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt }); + multi_iterator!(BindsIter { Zero, One, Dup, Mat }); match self { - Term::Mat { args, rules } => { - ChildrenIter::Mat(args.iter_mut().map(|arg| (arg, BindsIter::Zero([]))).chain( - rules.iter_mut().map(|r| (&mut r.body, BindsIter::Rule(r.pats.iter().flat_map(|p| p.binds())))), - )) - } + Term::Mat { arg, rules } => ChildrenIter::Mat( + [(arg.as_mut(), BindsIter::Zero([]))] + .into_iter() + .chain(rules.iter_mut().map(|r| (&mut r.2, BindsIter::Mat(r.1.iter())))), + ), + Term::Swt { arg, rules } => ChildrenIter::Swt([(arg.as_mut(), BindsIter::Zero([]))].into_iter().chain( + rules.iter_mut().map(|r| match &r.0 { + NumCtr::Num(_) => (&mut r.1, BindsIter::Zero([])), + NumCtr::Succ(nam) => (&mut r.1, BindsIter::One([nam])), + }), + )), Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => { ChildrenIter::Vec(els.iter_mut().map(|el| (el, BindsIter::Zero([])))) } - Term::Let { pat, val, nxt, .. } => { - ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::Pat(pat.binds()))]) + Term::Let { nam, val, nxt, .. } => { + ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::One([&*nam]))]) } - Term::Use { .. } => ChildrenIter::Zero([]), - Term::Dup { bnd, val, nxt, .. } => { + Term::Use { .. } => todo!(), + Term::Ltp { bnd, val, nxt, .. } | Term::Dup { bnd, val, nxt, .. } => { ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::Dup(bnd.iter()))]) } Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => { @@ -587,25 +614,28 @@ impl Term { pub fn children_mut_with_binds_mut( &mut self, ) -> impl DoubleEndedIterator>)> { - multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat }); - multi_iterator!(BindsIter { Zero, One, Dup, Pat, Rule }); + multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt }); + multi_iterator!(BindsIter { Zero, One, Dup, Mat }); match self { - Term::Mat { args, rules } => ChildrenIter::Mat( - args.iter_mut().map(|arg| (arg, BindsIter::Zero([]))).chain( - rules - .iter_mut() - .map(|r| (&mut r.body, BindsIter::Rule(r.pats.iter_mut().flat_map(|p| p.binds_mut())))), - ), + Term::Mat { arg, rules } => ChildrenIter::Mat( + [(arg.as_mut(), BindsIter::Zero([]))] + .into_iter() + .chain(rules.iter_mut().map(|r| (&mut r.2, BindsIter::Mat(r.1.iter_mut())))), ), + Term::Swt { arg, rules } => ChildrenIter::Swt([(arg.as_mut(), BindsIter::Zero([]))].into_iter().chain( + rules.iter_mut().map(|r| match &mut r.0 { + NumCtr::Num(_) => (&mut r.1, BindsIter::Zero([])), + NumCtr::Succ(nam) => (&mut r.1, BindsIter::One([nam])), + }), + )), Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => { ChildrenIter::Vec(els.iter_mut().map(|el| (el, BindsIter::Zero([])))) } - Term::Let { pat, val, nxt, .. } => ChildrenIter::Two([ - (val.as_mut(), BindsIter::Zero([])), - (nxt.as_mut(), BindsIter::Pat(pat.binds_mut())), - ]), - Term::Use { .. } => ChildrenIter::Zero([]), - Term::Dup { bnd, val, nxt, .. } => { + Term::Use { .. } => todo!(), + Term::Let { nam, val, nxt, .. } => { + ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::One([nam]))]) + } + Term::Ltp { bnd, val, nxt, .. } | Term::Dup { bnd, val, nxt, .. } => { ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::Dup(bnd))]) } Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => { @@ -624,56 +654,6 @@ impl Term { } } - pub fn patterns(&self) -> impl DoubleEndedIterator + Clone { - multi_iterator!(PatternsIter { Zero, Let, Mat }); - match self { - Term::Mat { rules, .. } => PatternsIter::Mat(rules.iter().flat_map(|r| r.pats.iter())), - Term::Let { pat, .. } => PatternsIter::Let([pat]), - Term::Tup { .. } - | Term::Sup { .. } - | Term::Lst { .. } - | Term::Dup { .. } - | Term::Use { .. } - | Term::App { .. } - | Term::Opx { .. } - | Term::Lam { .. } - | Term::Chn { .. } - | Term::Var { .. } - | Term::Lnk { .. } - | Term::Num { .. } - | Term::Nat { .. } - | Term::Str { .. } - | Term::Ref { .. } - | Term::Era - | Term::Err => PatternsIter::Zero([]), - } - } - - pub fn patterns_mut(&mut self) -> impl DoubleEndedIterator { - multi_iterator!(PatternsIter { Zero, Let, Mat }); - match self { - Term::Mat { rules, .. } => PatternsIter::Mat(rules.iter_mut().flat_map(|r| r.pats.iter_mut())), - Term::Let { pat, .. } => PatternsIter::Let([pat]), - Term::Tup { .. } - | Term::Sup { .. } - | Term::Lst { .. } - | Term::Dup { .. } - | Term::Use { .. } - | Term::App { .. } - | Term::Opx { .. } - | Term::Lam { .. } - | Term::Chn { .. } - | Term::Var { .. } - | Term::Lnk { .. } - | Term::Num { .. } - | Term::Nat { .. } - | Term::Str { .. } - | Term::Ref { .. } - | Term::Era - | Term::Err => PatternsIter::Zero([]), - } - } - /* Common checks and transformations */ pub fn recursive_call(f: F) -> R where @@ -683,8 +663,12 @@ impl Term { } /// 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). + /// Ex: Using subst to beta-reduce `(@a @b a b)` converting it into `@b b`. + /// + /// Expects var bind information to be properly stored in match expressions, + /// so it must run AFTER `fix_match_terms`. pub fn subst(&mut self, from: &Name, to: &Term) { Term::recursive_call(move || match self { Term::Var { nam } if nam == from => *self = to.clone(), @@ -765,108 +749,12 @@ impl Term { go(self, &mut decls, &mut uses); (decls, uses) } - - pub fn is_simple_match(&self, ctrs: &Constructors, adts: &Adts) -> bool { - // A match term - let Term::Mat { args, rules } = self else { - return false; - }; - // With 1 argument - if args.len() != 1 { - return false; - } - // The argument is a variable - if !matches!(args[0], Term::Var { .. }) { - return false; - } - // Each arm only has 1 pattern for the 1 argument - if rules.iter().any(|r| r.pats.len() != 1) { - return false; - } - // The match is over a valid type - 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 - match typ { - Type::Any => { - if rules.len() != 1 { - return false; - } - if !matches!(rules[0].pats.as_slice(), [Pattern::Var(_)]) { - return false; - } - } - Type::Tup(_) => { - if rules.len() != 1 { - return false; - } - let Pattern::Tup(args) = &rules[0].pats[0] else { return false }; - if args.iter().any(|p| !matches!(p, Pattern::Var(_))) { - return false; - } - } - Type::Num => { - 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); - } - } - } - Type::NumSucc(n) => { - if rules.len() as u64 != n + 1 { - 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) => { - let ctrs = &adts[&adt].ctrs; - if rules.len() != ctrs.len() { - return false; - } - for (rule, (ctr, args)) in rules.iter().zip(ctrs.iter()) { - if let Pattern::Ctr(rule_ctr, rule_args) = &rule.pats[0] { - if ctr != rule_ctr { - return false; - } - if rule_args.len() != args.len() { - return false; - } - if rule_args.iter().any(|arg| !matches!(arg, Pattern::Var(_))) { - return false; - } - } else { - return false; - } - } - } - } - - true - } } impl Pattern { pub fn binds(&self) -> impl DoubleEndedIterator> + Clone { self.iter().filter_map(|pat| match pat { Pattern::Var(nam) => Some(nam), - Pattern::Num(NumCtr::Succ(_, nam)) => nam.as_ref(), _ => None, }) } @@ -877,7 +765,7 @@ impl Pattern { let mut to_visit = vec![self]; while let Some(pat) = to_visit.pop() { match pat { - Pattern::Var(nam) | Pattern::Num(NumCtr::Succ(_, Some(nam))) => binds.push(nam), + Pattern::Var(nam) => binds.push(nam), _ => to_visit.extend(pat.children_mut().rev()), } } @@ -914,90 +802,21 @@ impl Pattern { els.into_iter() } - pub fn ctr_name(&self) -> Option { - match self { - Pattern::Var(_) => None, - Pattern::Ctr(nam, _) => Some(nam.clone()), - Pattern::Num(NumCtr::Num(num)) => Some(Name::new(format!("{num}"))), - Pattern::Num(NumCtr::Succ(num, _)) => Some(Name::new(format!("{num}+"))), - Pattern::Tup(pats) => Some(Name::new(format!("({})", ",".repeat(pats.len())))), - Pattern::Lst(_) => todo!(), - Pattern::Str(_) => todo!(), - } - } - pub fn is_wildcard(&self) -> bool { matches!(self, Pattern::Var(_)) } - pub fn is_native_num_match(&self) -> bool { - matches!(self, Pattern::Num(NumCtr::Num(0) | NumCtr::Succ(1, _))) - } - - /// True if this pattern has no nested subpatterns. - pub fn is_simple(&self) -> bool { - match self { - Pattern::Var(_) => true, - Pattern::Ctr(_, args) | Pattern::Tup(args) => args.iter().all(|arg| matches!(arg, Pattern::Var(_))), - Pattern::Num(_) => true, - Pattern::Lst(_) | Pattern::Str(_) => todo!(), - } - } - - pub fn to_type(&self, ctrs: &Constructors) -> Type { - match self { - Pattern::Var(_) => Type::Any, - Pattern::Ctr(ctr_nam, _) => { - let adt_nam = ctrs.get(ctr_nam).expect("Unknown constructor '{ctr_nam}'"); - Type::Adt(adt_nam.clone()) - } - Pattern::Tup(args) => Type::Tup(args.len()), - Pattern::Num(NumCtr::Num(_)) => Type::Num, - Pattern::Num(NumCtr::Succ(n, _)) => Type::NumSucc(*n), - Pattern::Lst(..) => Type::Adt(builtins::LIST.into()), - Pattern::Str(..) => Type::Adt(builtins::STRING.into()), - } - } - pub fn to_term(&self) -> Term { match self { Pattern::Var(nam) => Term::var_or_era(nam.clone()), Pattern::Ctr(ctr, args) => { Term::call(Term::Ref { nam: ctr.clone() }, args.iter().map(|arg| arg.to_term())) } - 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(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::Num(val) => Term::Num { val: *val }, Pattern::Tup(args) => Term::Tup { els: args.iter().map(|p| p.to_term()).collect() }, Pattern::Lst(_) | Pattern::Str(_) => todo!(), } } - - /// True if both patterns are equal (match the same expressions) without considering nested patterns. - pub fn simple_equals(&self, other: &Pattern) -> bool { - 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::Succ(a, _)), Pattern::Num(NumCtr::Succ(b, _))) if a == b => true, - (Pattern::Tup(a), Pattern::Tup(b)) if a.len() == b.len() => true, - (Pattern::Lst(_), Pattern::Lst(_)) => true, - (Pattern::Var(_), Pattern::Var(_)) => true, - _ => false, - } - } - - /// True if this pattern matches a subset of the other pattern, without considering nested patterns. - /// That is, when something matches the ctr of self if it also matches other. - pub fn simple_subset_of(&self, other: &Pattern) -> bool { - self.simple_equals(other) || matches!(other, Pattern::Var(_)) - } - - /// True if the two pattern will match some common expressions. - pub fn shares_simple_matches_with(&self, other: &Pattern) -> bool { - self.simple_equals(other) || matches!(self, Pattern::Var(_)) || matches!(other, Pattern::Var(_)) - } } impl Rule { @@ -1030,43 +849,6 @@ impl Definition { } } -impl Type { - /// Return the constructors for a given type as patterns. - pub fn ctrs(&self, adts: &Adts) -> Vec { - match self { - Type::Any => vec![Pattern::Var(None)], - Type::Tup(len) => { - vec![Pattern::Tup((0 .. *len).map(|i| Pattern::Var(Some(Name::new(format!("%x{i}"))))).collect())] - } - 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] - .ctrs - .iter() - .map(|(nam, args)| { - Pattern::Ctr(nam.clone(), args.iter().map(|x| Pattern::Var(Some(x.clone()))).collect()) - }) - .collect() - } - } - } - - /// True if the type is an ADT or a builtin equivalent of an ADT (like tups and numbers) - pub fn is_ctr_type(&self) -> bool { - matches!(self, Type::Adt(_) | Type::Num | Type::Tup(_)) - } - - pub fn is_var_type(&self) -> bool { - matches!(self, Type::Any) - } -} - impl Name { pub fn new<'a, V: Into>>(value: V) -> Name { Name(STRINGS.get(value)) diff --git a/src/term/net_to_term.rs b/src/term/net_to_term.rs index 2f683a36..8eda11ab 100644 --- a/src/term/net_to_term.rs +++ b/src/term/net_to_term.rs @@ -1,7 +1,7 @@ use crate::{ diagnostics::{DiagnosticOrigin, Diagnostics, Severity}, net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT}, - term::{num_to_name, term_to_net::Labels, Book, Name, Op, Pattern, Tag, Term}, + term::{num_to_name, term_to_net::Labels, Book, Name, Op, Tag, Term}, }; use std::collections::{BTreeSet, HashMap, HashSet}; @@ -59,6 +59,7 @@ pub struct Reader<'a> { net: &'a INet, labels: &'a Labels, dup_paths: Option>>, + /// Store for floating/unscoped terms, like dups and let tups. scope: Scope, seen_fans: Scope, seen: HashSet, @@ -102,7 +103,7 @@ impl Reader<'_> { Mat => match next.slot() { 2 => { // Read the matched expression - let scrutinee = self.read_term(self.net.enter_port(Port(node, 0))); + let mut arg = self.read_term(self.net.enter_port(Port(node, 0))); // Read the pattern matching node let sel_node = self.net.enter_port(Port(node, 1)).node(); @@ -112,20 +113,38 @@ impl Reader<'_> { 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::native_num_match(scrutinee, Term::Era, Term::Era, None) + Term::switch(arg, Term::Era, Term::Era, None) } else { let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1))); let mut succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2))); match &mut succ_term { Term::Lam { nam, bod, .. } => { + // Extract non-var args so we can refer to the pred. + let (arg, bind) = if let Term::Var { nam } = &mut arg { + (std::mem::replace(nam, Name::from("")), None) + } else { + (self.namegen.unique(), Some(arg)) + }; + let nam = std::mem::take(nam); - let bod = std::mem::take(bod); - Term::native_num_match(scrutinee, zero_term, *bod, Some(nam)) + let mut bod = std::mem::take(bod); + + // Rename the pred variable to indicate it's arg-1. + if let Some(nam) = &nam { + bod.subst(nam, &Term::Var { nam: Name::new(format!("{arg}-1")) }); + } + + let swt = Term::switch(Term::Var { nam: arg.clone() }, zero_term, *bod, nam); + if let Some(bind) = bind { + Term::Let { nam: Some(arg), val: Box::new(bind), nxt: Box::new(swt) } + } else { + swt + } } _ => { self.error(ReadbackError::InvalidNumericMatch); - Term::native_num_match(scrutinee, zero_term, succ_term, None) + Term::switch(arg, zero_term, succ_term, None) } } } @@ -322,48 +341,27 @@ impl Term { /// This has the effect of inserting the split at the lowest common ancestor /// of all of the uses of `fst` and `snd`. fn insert_split(&mut self, split: &mut Split, threshold: usize) -> Option { - let n = match self { - Term::Var { nam } => usize::from(split.fst.as_ref() == Some(nam) || split.snd.as_ref() == Some(nam)), - Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.insert_split(split, threshold)?, - Term::Let { val: fst, nxt: snd, .. } - | Term::App { fun: fst, arg: snd, .. } - | Term::Dup { val: fst, nxt: snd, .. } - | Term::Opx { fst, snd, .. } => { - fst.insert_split(split, threshold)? + snd.insert_split(split, threshold)? - } - Term::Use { .. } => unreachable!(), - Term::Sup { els, .. } | Term::Tup { els } => { - let mut n = 0; - for el in els { - n += el.insert_split(split, threshold)?; - } - n - } - Term::Mat { args, rules } => { - debug_assert_eq!(args.len(), 1); - let mut n = args[0].insert_split(split, threshold)?; - for rule in rules { - n += rule.body.insert_split(split, threshold)?; - } - n - } - Term::Nat { .. } | Term::Lst { .. } => unreachable!(), - Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Ref { .. } | Term::Era | Term::Err => 0, - }; - - if n >= threshold { - let Split { tag, fst, snd, val } = std::mem::take(split); - let nxt = Box::new(std::mem::take(self)); - *self = match tag { - None => { - Term::Let { pat: Pattern::Tup(vec![Pattern::Var(fst), Pattern::Var(snd)]), val: Box::new(val), nxt } - } - Some(tag) => Term::Dup { tag, bnd: vec![fst, snd], val: Box::new(val), nxt }, + Term::recursive_call(move || { + let mut n = match self { + Term::Var { nam } => usize::from(split.fst.as_ref() == Some(nam) || split.snd.as_ref() == Some(nam)), + _ => 0, }; - None - } else { - Some(n) - } + for child in self.children_mut() { + n += child.insert_split(split, threshold)?; + } + + if n >= threshold { + let Split { tag, fst, snd, val } = std::mem::take(split); + let nxt = Box::new(std::mem::take(self)); + *self = match tag { + None => Term::Ltp { bnd: vec![fst, snd], val: Box::new(val), nxt }, + Some(tag) => Term::Dup { tag, bnd: vec![fst, snd], val: Box::new(val), nxt }, + }; + None + } else { + Some(n) + } + }) } pub fn fix_names(&mut self, id_counter: &mut u64, book: &Book) { @@ -376,11 +374,7 @@ impl Term { } } - match self { - Term::Lam { nam, bod, .. } => { - fix_name(nam, id_counter, bod); - bod.fix_names(id_counter, book); - } + Term::recursive_call(move || match self { Term::Ref { nam: def_name } => { if def_name.is_generated() { let def = book.defs.get(def_name).unwrap(); @@ -389,39 +383,15 @@ impl Term { *self = term; } } - Term::Dup { bnd, val, nxt, .. } => { - val.fix_names(id_counter, book); - for bnd in bnd { - fix_name(bnd, id_counter, nxt); - } - nxt.fix_names(id_counter, book); - } - Term::Chn { bod, .. } => bod.fix_names(id_counter, book), - Term::App { fun: fst, arg: snd, .. } | Term::Opx { op: _, fst, snd } => { - fst.fix_names(id_counter, book); - snd.fix_names(id_counter, book); - } - Term::Sup { els, .. } | Term::Tup { els } => { - for el in els { - el.fix_names(id_counter, book); - } - } - Term::Mat { args, rules } => { - for arg in args { - arg.fix_names(id_counter, book); - } - - for rule in rules { - for nam in rule.pats.iter_mut().flat_map(|p| p.binds_mut()) { - fix_name(nam, id_counter, &mut rule.body); + _ => { + for (child, bnd) in self.children_mut_with_binds_mut() { + for bnd in bnd { + fix_name(bnd, id_counter, child); + child.fix_names(id_counter, book); } - - rule.body.fix_names(id_counter, book); } } - Term::Let { .. } | Term::Use { .. } | Term::Nat { .. } | Term::Lst { .. } => unreachable!(), - Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {} - } + }) } } diff --git a/src/term/parser/lexer.rs b/src/term/parser/lexer.rs index 3f639d2e..6548880f 100644 --- a/src/term/parser/lexer.rs +++ b/src/term/parser/lexer.rs @@ -26,6 +26,9 @@ pub enum Token { #[token("match")] Match, + #[token("switch")] + Switch, + #[token("=")] Equals, @@ -270,6 +273,7 @@ impl fmt::Display for Token { Self::Let => write!(f, "let"), Self::Use => write!(f, "use"), Self::Match => write!(f, "match"), + Self::Switch => write!(f, "switch"), Self::Equals => write!(f, "="), Self::Num(num) => write!(f, "{num}"), Self::Str(s) => write!(f, "\"{s}\""), diff --git a/src/term/parser/parser.rs b/src/term/parser/parser.rs index bf5f92b2..84646ff3 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, Name, NumCtr, Op, Pattern, Rule, Tag, Term, + Adt, Book, Definition, Name, NumCtr, Op, Pattern, Rule, Tag, Term, LNIL, SNIL, }; use chumsky::{ error::{Error, RichReason}, @@ -198,24 +198,27 @@ where I: ValueInput<'a, Token = Token, Span = SimpleSpan>, { let var = name().map(|name| Term::Var { nam: name }).boxed(); - let global_var = just(Token::Dollar).ignore_then(name()).map(|name| Term::Lnk { nam: name }).boxed(); + let unscoped_var = just(Token::Dollar).ignore_then(name()).map(|name| Term::Lnk { nam: name }).boxed(); - let number = select!(Token::Num(num) => Term::Num{val: num}).or( + let number = select!(Token::Num(num) => num).or( select!(Token::Error(LexingError::InvalidNumberLiteral) => ()).validate(|_, span, emit| { emit.emit(Rich::custom(span, "found invalid number literal expected number")); - Term::Num { val: 0 } + 0 }), ); - let nat = just(Token::Hash).ignore_then(select!(Token::Num(num) => Term::Nat { val: num }).or( - select!(Token::Error(LexingError::InvalidNumberLiteral) => ()).validate(|_, span, emit| { - emit.emit(Rich::custom(span, "found invalid nat literal expected number")); - Term::Nat { val: 0 } - }), - )); + let nat: chumsky::Boxed>> = just(Token::Hash) + .ignore_then(select!(Token::Num(num) => Term::Nat { val: num }).or( + select!(Token::Error(LexingError::InvalidNumberLiteral) => ()).validate(|_, span, emit| { + emit.emit(Rich::custom(span, "found invalid nat literal expected number")); + Term::Nat { val: 0 } + }), + )) + .boxed(); + + let num_term = number.map(|val| Term::Num { val }); let term_sep = just(Token::Semicolon).or_not(); - let list_sep = just(Token::Comma).or_not(); recursive(|term| { // * @@ -230,7 +233,7 @@ where .boxed(); // #tag? λ$x body - let global_lam = tag(Tag::Static) + let unscoped_lam = tag(Tag::Static) .then_ignore(just(Token::Lambda)) .then(just(Token::Dollar).ignore_then(name_or_era())) .then(term.clone()) @@ -240,7 +243,7 @@ where // #tag {fst snd} let sup = tag(Tag::Auto) .then_ignore(just(Token::LBracket)) - .then(term.clone().separated_by(list_sep.clone()).at_least(2).collect()) + .then(term.clone().separated_by(just(Token::Comma).or_not()).at_least(2).collect()) .then_ignore(just(Token::RBracket)) .map(|(tag, els)| Term::Sup { tag, els }) .boxed(); @@ -249,7 +252,7 @@ where let dup = just(Token::Let) .ignore_then(tag(Tag::Auto)) .then_ignore(just(Token::LBracket)) - .then(name_or_era().separated_by(list_sep.clone()).at_least(2).collect()) + .then(name_or_era().separated_by(just(Token::Comma).or_not()).at_least(2).collect()) .then_ignore(just(Token::RBracket)) .then_ignore(just(Token::Equals)) .then(term.clone()) @@ -258,20 +261,14 @@ where .map(|(((tag, bnd), val), next)| Term::Dup { tag, bnd, val: Box::new(val), nxt: Box::new(next) }) .boxed(); - // let a = ... - // let (a, b) = ... + // let nam = term; term let let_ = just(Token::Let) - .ignore_then(pattern().validate(|pat, span, emit| { - if matches!(&pat, Pattern::Num(..)) { - emit.emit(Rich::custom(span, "Numbers not supported in let.")); - } - pat - })) + .ignore_then(name_or_era()) .then_ignore(just(Token::Equals)) .then(term.clone()) .then_ignore(term_sep.clone()) .then(term.clone()) - .map(|((pat, val), nxt)| Term::Let { pat, val: Box::new(val), nxt: Box::new(nxt) }) + .map(|((nam, val), nxt)| Term::Let { nam, val: Box::new(val), nxt: Box::new(nxt) }) .boxed(); // use a = val ';'? nxt @@ -284,42 +281,69 @@ where .map(|((nam, val), nxt)| Term::Use { nam, val: Box::new(val), nxt: Box::new(nxt) }) .boxed(); - let match_arg = name().then_ignore(just(Token::Equals)).or_not().then(term.clone()); - let match_args = - match_arg.separated_by(list_sep.clone()).at_least(1).allow_trailing().collect::>(); + // (name '=')? term + let match_arg = name().then_ignore(just(Token::Equals)).or_not().then(term.clone()).boxed(); - // '|'? pat+: term + let lnil = just(Token::LBrace) + .ignore_then(just(Token::RBrace)) + .ignored() + .map(|_| Some(Name::from(LNIL))) + .labelled("List.nil"); + let snil = + select!(Token::Str(s) if s.is_empty() => ()).map(|_| Some(Name::from(SNIL))).labelled("String.nil"); + let match_pat = choice((name_or_era(), lnil, snil)); + + // '|'? name: term let match_rule = just(Token::Or) .or_not() - .ignore_then(pattern().repeated().at_least(1).collect::>()) + .ignore_then(match_pat) + .labelled("") .then_ignore(just(Token::Colon)) .then(term.clone()) - .map(|(pats, body)| Rule { pats, body }); + .map(|(nam, body)| (nam, vec![], body)); let match_rules = match_rule.separated_by(term_sep.clone()).at_least(1).allow_trailing().collect(); // match ((scrutinee | = value),?)+ { pat+: term;... } let match_ = just(Token::Match) - .ignore_then(match_args) + .ignore_then(match_arg.clone()) .then_ignore(just(Token::LBracket)) .then(match_rules) .then_ignore(just(Token::RBracket)) - .map(|(args, rules)| { - let mut args_no_bind = vec![]; - let mut binds = vec![]; - for (bind, arg) in args { - if let Some(bind) = bind { - args_no_bind.push(Term::Var { nam: bind.clone() }); - binds.push((bind, arg)); - } else { - args_no_bind.push(arg); + .map(|((bind, arg), rules)| { + if let Some(bind) = bind { + Term::Let { + nam: Some(bind.clone()), + val: Box::new(arg), + nxt: Box::new(Term::Mat { arg: Box::new(Term::Var { nam: bind }), rules }), } + } else { + Term::Mat { arg: Box::new(arg), rules } + } + }) + .boxed(); + + let switch_ctr = choice((number.map(NumCtr::Num), soft_keyword("_").map(|_| NumCtr::Succ(None)))) + .labelled(""); + + let switch_rule = + just(Token::Or).or_not().ignore_then(switch_ctr).then_ignore(just(Token::Colon)).then(term.clone()); + let switch_rules = switch_rule.separated_by(term_sep.clone()).at_least(1).allow_trailing().collect(); + + let switch = just(Token::Switch) + .ignore_then(match_arg) + .then_ignore(just(Token::LBracket)) + .then(switch_rules) + .then_ignore(just(Token::RBracket)) + .map(|((bind, arg), rules)| { + if let Some(bind) = bind { + Term::Let { + nam: Some(bind.clone()), + val: Box::new(arg), + nxt: Box::new(Term::Swt { arg: Box::new(Term::Var { nam: bind }), rules }), + } + } else { + Term::Swt { arg: Box::new(arg), rules } } - let mat = Term::Mat { args: args_no_bind, rules }; - binds.into_iter().rfold(mat, |acc, (bind, arg)| Term::Let { - pat: Pattern::Var(Some(bind)), - val: Box::new(arg), - nxt: Box::new(acc), - }) }) .boxed(); @@ -351,6 +375,18 @@ where .map(|els| Term::Tup { els }) .boxed(); + // let (x, ..n) = term; term + let let_tup = just(Token::Let) + .ignore_then(just(Token::LParen)) + .ignore_then(name_or_era().separated_by(just(Token::Comma)).at_least(2).collect()) + .then_ignore(just(Token::RParen)) + .then_ignore(just(Token::Equals)) + .then(term.clone()) + .then_ignore(term_sep.clone()) + .then(term.clone()) + .map(|((bnd, val), next)| Term::Ltp { bnd, val: Box::new(val), nxt: Box::new(next) }) + .boxed(); + let str = select!(Token::Str(s) => Term::Str { val: s }).boxed(); let chr = select!(Token::Char(c) => Term::Num { val: c }).boxed(); @@ -363,16 +399,32 @@ where .boxed(); choice(( - // OBS: `num_op` has to be before app, idk why? - // OBS: `app` has to be before `tup` to not overflow on huge app terms - // TODO: What happens on huge `tup` and other terms? - num_op, app, tup, global_var, var, number, nat, list, str, chr, sup, global_lam, lam, dup, let_, use_, - match_, era, + num_op, + app, + tup, + unscoped_var, + var, + nat, + num_term, + list, + str, + chr, + sup, + unscoped_lam, + lam, + dup, + use_, + let_tup, + let_, + match_, + switch, + era, )) + .labelled("term") }) } -fn pattern<'a, I>() -> impl Parser<'a, I, Pattern, extra::Err>> +fn rule_pattern<'a, I>() -> impl Parser<'a, I, Pattern, extra::Err>> where I: ValueInput<'a, Token = Token, Span = SimpleSpan>, { @@ -407,28 +459,22 @@ where n }); - let num = num_val.map(|n| Pattern::Num(NumCtr::Num(n))).labelled(""); + let num = num_val.map(Pattern::Num).labelled(""); - let succ = num_val - .then_ignore(just(Token::Add)) - .then(name_or_era().or_not()) - .map(|(num, nam)| Pattern::Num(NumCtr::Succ(num, nam))) - .labelled("+") - .boxed(); - - let chr = select!(Token::Char(c) => Pattern::Num(NumCtr::Num(c))).labelled("").boxed(); + let chr = select!(Token::Char(c) => Pattern::Num(c)).labelled("").boxed(); let str = select!(Token::Str(s) => Pattern::Str(s)).labelled("").boxed(); - choice((succ, num, chr, str, var, ctr, list, tup)) + choice((num, chr, str, var, ctr, list, tup)) }) + .labelled("") } -fn rule_pattern<'a, I>() -> impl Parser<'a, I, (Name, Vec), extra::Err>> +fn rule_lhs<'a, I>() -> impl Parser<'a, I, (Name, Vec), extra::Err>> where I: ValueInput<'a, Token = Token, Span = SimpleSpan>, { - let lhs = tl_name().then(pattern().repeated().collect()).boxed(); + let lhs = tl_name().then(rule_pattern().repeated().collect()).boxed(); let just_lhs = lhs.clone().then_ignore(just(Token::Equals).map_err(|err: Rich<'a, Token>| { Error::::expected_found( @@ -455,7 +501,7 @@ fn rule<'a, I>() -> impl Parser<'a, I, TopLevel, extra::Err>> where I: ValueInput<'a, Token = Token, Span = SimpleSpan>, { - rule_pattern().then(term()).map(move |((name, pats), body)| TopLevel::Rule((name, Rule { pats, body }))) + rule_lhs().then(term()).map(move |((name, pats), body)| TopLevel::Rule((name, Rule { pats, body }))) } fn datatype<'a, I>() -> impl Parser<'a, I, TopLevel, extra::Err>> diff --git a/src/term/term_to_net.rs b/src/term/term_to_net.rs index e68a29b6..619a7be5 100644 --- a/src/term/term_to_net.rs +++ b/src/term/term_to_net.rs @@ -4,7 +4,7 @@ use crate::{ NodeKind::{self, *}, Port, ROOT, }, - term::{Book, Name, NumCtr, Op, Pattern, Tag, Term}, + term::{Book, Name, NumCtr, Op, Tag, Term}, }; use std::collections::{hash_map::Entry, HashMap}; @@ -111,30 +111,31 @@ impl EncodeTermState<'_> { Some(Port(app, 2)) } - // core: & cond ~ (zero succ) ret - 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(NumCtr::Num(0))])); - debug_assert!(matches!(rules[1].pats[..], [Pattern::Num(NumCtr::Succ(1, None))])); + Term::Mat { .. } => unreachable!("Should've been desugared already"), + // core: & arg ~ ?<(zero succ) ret> + Term::Swt { arg, rules } => { + // At this point should be only num matches of 0 and succ. + debug_assert!(rules.len() == 2); + debug_assert!(matches!(rules[0].0, NumCtr::Num(0))); + debug_assert!(matches!(rules[1].0, NumCtr::Succ(None))); - let if_ = self.inet.new_node(Mat); + let mat = self.inet.new_node(Mat); - let cond = self.encode_term(arg, Port(if_, 0)); - self.link_local(Port(if_, 0), cond); + let arg = self.encode_term(arg, Port(mat, 0)); + self.link_local(Port(mat, 0), arg); - let zero = &rules[0].body; - let succ = &rules[1].body; + let zero = &rules[0].1; + let succ = &rules[1].1; let sel = self.inet.new_node(Con { lab: None }); - self.inet.link(Port(sel, 0), Port(if_, 1)); + self.inet.link(Port(sel, 0), Port(mat, 1)); let zero = self.encode_term(zero, Port(sel, 1)); self.link_local(Port(sel, 1), zero); let succ = self.encode_term(succ, Port(sel, 2)); self.link_local(Port(sel, 2), succ); - Some(Port(if_, 2)) + Some(Port(mat, 2)) } // A dup becomes a dup node too. Ports for dups of size 2: // - 0: points to the value projected. @@ -189,24 +190,23 @@ impl EncodeTermState<'_> { self.inet.link(up, Port(node, 0)); Some(Port(node, 0)) } - Term::Let { pat: Pattern::Tup(args), val, nxt } => { - let nams = args.iter().map(|arg| if let Pattern::Var(nam) = arg { nam } else { unreachable!() }); - let (main, aux) = self.make_node_list(Tup, args.len()); + Term::Ltp { bnd, val, nxt } => { + let (main, aux) = self.make_node_list(Tup, bnd.len()); let val = self.encode_term(val, main); self.link_local(main, val); - for (nam, aux) in nams.clone().zip(aux.iter()) { + for (nam, aux) in bnd.iter().zip(aux.iter()) { self.push_scope(nam, *aux); } let nxt = self.encode_term(nxt, up); - for (nam, aux) in nams.rev().zip(aux.iter().rev()) { + for (nam, aux) in bnd.iter().rev().zip(aux.iter().rev()) { self.pop_scope(nam, *aux); } nxt } - Term::Let { pat: Pattern::Var(None), val, nxt } => { + Term::Let { nam: None, val, nxt } => { let nod = self.inet.new_node(Era); let val = self.encode_term(val, Port(nod, 0)); diff --git a/src/term/transform/apply_args.rs b/src/term/transform/apply_args.rs index f496e467..d465c362 100644 --- a/src/term/transform/apply_args.rs +++ b/src/term/transform/apply_args.rs @@ -1,10 +1,8 @@ use crate::{ - diagnostics::{Diagnostics, ToStringVerbose}, - term::{Ctx, Pattern, Term}, + diagnostics::Diagnostics, + term::{Ctx, Pattern, Rule, Term}, }; -struct PatternArgError(Pattern); - impl Ctx<'_> { /// Applies the arguments to the program being run by applying them to the main function. /// @@ -22,26 +20,35 @@ impl Ctx<'_> { if let Some(entrypoint) = &self.book.entrypoint { let main_def = &mut self.book.defs[entrypoint]; - for pat in &main_def.rules[0].pats { - if !matches!(pat, Pattern::Var(Some(..))) { - self.info.add_rule_error(PatternArgError(pat.clone()), entrypoint.clone()); + // Since we fatal error, no need to exit early + let n_rules = main_def.rules.len(); + if n_rules != 1 { + self.info.add_rule_error( + format!("Expected the entrypoint function to have only one rule, found {n_rules}."), + entrypoint.clone(), + ); + } + + let mut main_body = std::mem::take(&mut main_def.rules[0].body); + + for pat in main_def.rules[0].pats.iter().rev() { + if let Pattern::Var(var) = pat { + main_body = Term::lam(var.clone(), main_body); + } else { + self.info.add_rule_error( + format!("Expected the entrypoint function to only have variable patterns, found '{pat}'."), + entrypoint.clone(), + ); } } if let Some(args) = args { - main_def.convert_match_def_to_term(); - let main_body = &mut self.book.defs[entrypoint].rule_mut().body; - - *main_body = Term::call(main_body.clone(), args); + main_body = Term::call(main_body, args); } + + main_def.rules = vec![Rule { pats: vec![], body: main_body }]; } self.info.fatal(()) } } - -impl ToStringVerbose for PatternArgError { - fn to_string_verbose(&self, _verbose: bool) -> String { - format!("Expected the entrypoint to only have variable pattern, found '{}'.", self.0) - } -} diff --git a/src/term/transform/desugar_implicit_match_binds.rs b/src/term/transform/desugar_implicit_match_binds.rs deleted file mode 100644 index 079c8c13..00000000 --- a/src/term/transform/desugar_implicit_match_binds.rs +++ /dev/null @@ -1,97 +0,0 @@ -use crate::term::{Adts, Book, Constructors, Name, NumCtr, Pattern, Term}; - -impl Book { - /// Converts implicit match binds into explicit ones, using the - /// field names specified in the ADT declaration or the default - /// names for builtin constructors. - /// - /// Example: - /// ```hvm - /// data MyList = (Cons h t) | Nil - /// match x y { - /// 0 Nil: (A) - /// 0 Cons: (B y.h y.t) - /// 1+ Nil: (C x-1) - /// 1+p (Cons x xs): (D p x xs) - /// } - /// ``` - /// becomes - /// ```hvm - /// match x y { - /// 0 Nil: (A) - /// 0 (Cons y.h y.t): (B y.h y.t) - /// 1+x-1 Nil: (C x-1) - /// 1+p (Cons x xs): (D p x xs) - /// } - /// ``` - pub fn desugar_implicit_match_binds(&mut self) { - for def in self.defs.values_mut() { - for rule in &mut def.rules { - rule.body.desugar_implicit_match_binds(&self.ctrs, &self.adts); - } - } - } -} - -impl Term { - pub fn desugar_implicit_match_binds(&mut self, ctrs: &Constructors, adts: &Adts) { - Term::recursive_call(move || { - for child in self.children_mut() { - child.desugar_implicit_match_binds(ctrs, adts); - } - - if let Term::Mat { args, rules } = self { - // Make all the matched terms variables - let mut match_args = vec![]; - for arg in args.iter_mut() { - if let Term::Var { nam } = arg { - match_args.push((nam.clone(), None)) - } else { - let nam = Name::new(format!("%matched_{}", match_args.len())); - let arg = std::mem::replace(arg, Term::Var { nam: nam.clone() }); - match_args.push((nam, Some(arg))); - } - } - - // Make implicit match binds explicit - for rule in rules.iter_mut() { - for ((nam, _), pat) in match_args.iter().zip(rule.pats.iter_mut()) { - match pat { - Pattern::Var(_) => (), - Pattern::Ctr(ctr_nam, pat_args) => { - let adt = &adts[ctrs.get(ctr_nam).unwrap()]; - let ctr_args = adt.ctrs.get(ctr_nam).unwrap(); - if pat_args.is_empty() && !ctr_args.is_empty() { - // Implicit ctr args - *pat_args = ctr_args - .iter() - .map(|field| Pattern::Var(Some(Name::new(format!("{nam}.{field}"))))) - .collect(); - } - } - 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}-{n}")))); - } - Pattern::Tup(..) => (), - Pattern::Lst(..) => (), - Pattern::Str(..) => (), - } - } - } - - // Add the binds to the extracted term vars. - *self = match_args.into_iter().rfold(std::mem::take(self), |nxt, (nam, val)| { - if let Some(val) = val { - // Non-Var term that was extracted. - Term::Let { pat: Pattern::Var(Some(nam)), val: Box::new(val), nxt: Box::new(nxt) } - } else { - nxt - } - }); - } - }) - } -} diff --git a/src/term/transform/desugar_let_destructors.rs b/src/term/transform/desugar_let_destructors.rs deleted file mode 100644 index 6d840f39..00000000 --- a/src/term/transform/desugar_let_destructors.rs +++ /dev/null @@ -1,41 +0,0 @@ -use crate::term::{Book, Name, Pattern, Rule, Term}; - -impl Book { - /// Convert let destructor expressions like `let (a, b) = X` into the equivalent match expression. - pub fn desugar_let_destructors(&mut self) { - for def in self.defs.values_mut() { - for rule in &mut def.rules { - rule.body.desugar_let_destructors(); - } - } - } -} - -impl Term { - pub fn desugar_let_destructors(&mut self) { - Term::recursive_call(move || { - for child in self.children_mut() { - child.desugar_let_destructors(); - } - - if let Term::Let { pat, val, nxt } = self - && !pat.is_wildcard() - { - let pat = std::mem::replace(pat, Pattern::Var(None)); - let val = std::mem::take(val); - let nxt = std::mem::take(nxt); - - let rules = vec![Rule { pats: vec![pat], body: *nxt }]; - - *self = if let Term::Var { .. } = val.as_ref() { - Term::Mat { args: vec![*val], rules } - } else { - let nam = Name::from("%matched"); - let pat = Pattern::Var(Some(nam.clone())); - let args = vec![Term::Var { nam }]; - Term::Let { pat, val, nxt: Box::new(Term::Mat { args, rules }) } - }; - } - }) - } -} diff --git a/src/term/transform/desugar_match_defs.rs b/src/term/transform/desugar_match_defs.rs new file mode 100644 index 00000000..cf09983c --- /dev/null +++ b/src/term/transform/desugar_match_defs.rs @@ -0,0 +1,522 @@ +use std::collections::{BTreeSet, HashSet}; + +use crate::{ + diagnostics::{Diagnostics, ToStringVerbose, WarningType}, + term::{builtins, Adts, Constructors, Ctx, Definition, Name, NumCtr, Pattern, Rule, Term}, +}; + +pub enum DesugarMatchDefErr { + AdtNotExhaustive { adt: Name, ctr: Name }, + NumMissingDefault, + TypeMismatch { expected: Type, found: Type, pat: Pattern }, + RepeatedBind { bind: Name }, +} + +impl Ctx<'_> { + pub fn desugar_match_defs(&mut self) -> Result<(), Diagnostics> { + self.info.start_pass(); + + for (def_name, def) in self.book.defs.iter_mut() { + let errs = def.desugar_match_def(&self.book.ctrs, &self.book.adts); + for err in errs { + match err { + DesugarMatchDefErr::AdtNotExhaustive { .. } + | DesugarMatchDefErr::NumMissingDefault + | DesugarMatchDefErr::TypeMismatch { .. } => self.info.add_rule_error(err, def_name.clone()), + DesugarMatchDefErr::RepeatedBind { .. } => { + self.info.add_rule_warning(err, WarningType::RepeatedBind, def_name.clone()) + } + } + } + } + + self.info.fatal(()) + } +} + +impl Definition { + pub fn desugar_match_def(&mut self, ctrs: &Constructors, adts: &Adts) -> Vec { + let mut errs = vec![]; + + let repeated_bind_errs = fix_repeated_binds(&mut self.rules); + errs.extend(repeated_bind_errs); + + let args = (0 .. self.arity()).map(|i| Name::new(format!("%arg{i}"))).collect::>(); + let rules = std::mem::take(&mut self.rules); + match simplify_rule_match(args.clone(), rules, ctrs, adts) { + Ok(body) => { + let body = args.into_iter().rfold(body, |body, arg| Term::lam(Some(arg), body)); + self.rules = vec![Rule { pats: vec![], body }]; + } + Err(e) => errs.push(e), + } + errs + } +} + +/// When a rule has repeated bind, the only one that is actually useful is the last one. +/// +/// Example: In `(Foo x x x x) = x`, the function should return the fourth argument. +/// +/// To avoid having to deal with this, we can just erase any repeated binds. +/// ```hvm +/// (Foo a (Succ a) (Cons a)) = (a a) +/// // After this transformation, becomes: +/// (Foo * (Succ *) (Cons a)) = (a a) +/// ``` +fn fix_repeated_binds(rules: &mut [Rule]) -> Vec { + let mut errs = vec![]; + for rule in rules { + let mut binds = HashSet::new(); + rule.pats.iter_mut().flat_map(|p| p.binds_mut()).rev().for_each(|nam| { + if binds.contains(nam) { + // Repeated bind, not reachable and can be erased. + if let Some(nam) = nam { + errs.push(DesugarMatchDefErr::RepeatedBind { bind: nam.clone() }); + } + *nam = None; + // TODO: Send a repeated bind warning + } else { + binds.insert(&*nam); + } + }); + } + errs +} + +/// Creates the match tree for a given pattern matching function definition. +/// For each constructor, a match case is created. +/// +/// The match cases follow the same order as the order the constructors are in +/// the ADT declaration. +/// +/// If there are constructors of different types for the same arg, returns a type error. +/// +/// If no patterns match one of the constructors, returns a non-exhaustive match error. +/// +/// =========================================================================== +/// + +/// +/// Any nested subpatterns are extracted and moved into a nested match +/// expression, together with the remaining match arguments. +fn simplify_rule_match( + args: Vec, + mut rules: Vec, + ctrs: &Constructors, + adts: &Adts, +) -> Result { + if args.is_empty() { + Ok(std::mem::take(&mut rules[0].body)) + } else if rules[0].pats.iter().all(|p| p.is_wildcard()) { + Ok(irrefutable_fst_row_rule(args, std::mem::take(&mut rules[0]))) + } else { + let typ = Type::infer_from_def_arg(&rules, 0, ctrs)?; + match typ { + Type::Any => var_rule(args, rules, ctrs, adts), + Type::Tup(tup_len) => tup_rule(args, rules, tup_len, ctrs, adts), + Type::Num => num_rule(args, rules, ctrs, adts), + Type::Adt(adt_name) => switch_rule(args, rules, adt_name, ctrs, adts), + } + } +} + +/// Irrefutable first row rule. +/// Short-circuits the encoding in case the first rule always matches. +/// This is useful to avoid unnecessary pattern matching. +fn irrefutable_fst_row_rule(args: Vec, rule: Rule) -> Term { + let mut term = rule.body; + for (arg, pat) in args.into_iter().zip(rule.pats.into_iter()) { + let Pattern::Var(var) = pat else { unreachable!() }; + if let Some(var) = var { + term.subst(&var, &Term::Var { nam: arg }); + } + } + term +} + +/// Var rule. +/// `case x0 ... xN { var p1 ... pN: (Body var p1 ... pN) }` +/// becomes +/// `case x1 ... xN { p1 ... pN: use var = x0; (Body var p1 ... pN) }` +fn var_rule( + mut args: Vec, + rules: Vec, + ctrs: &Constructors, + adts: &Adts, +) -> Result { + let arg = args[0].clone(); + let new_args = args.split_off(1); + + let mut new_rules = vec![]; + for mut rule in rules { + let new_pats = rule.pats.split_off(1); + let pat = rule.pats.pop().unwrap(); + + if let Pattern::Var(Some(nam)) = &pat { + rule.body.subst(nam, &Term::Var { nam: arg.clone() }); + } + + let new_rule = Rule { pats: new_pats, body: rule.body }; + new_rules.push(new_rule); + } + + simplify_rule_match(new_args, new_rules, ctrs, adts) +} + +/// Tuple rule. +/// ```hvm +/// case x0 ... xN { +/// (p0_0, ... p0_M) p1 ... pN: +/// (Body p0_0 ... p0_M p1 ... pN) +/// } +/// ``` +/// becomes +/// ```hvm +/// let (x0.0, ... x0.M) = x0; +/// case x0.0 ... x0.M x1 ... xN { +/// p0_0 ... p0_M p1 ... pN: +/// (Body p0_0 ... p0_M p1 ... pN) +/// } +/// ``` +fn tup_rule( + mut args: Vec, + rules: Vec, + tup_len: usize, + ctrs: &Constructors, + adts: &Adts, +) -> Result { + let arg = args[0].clone(); + let old_args = args.split_off(1); + let new_args = (0 .. tup_len).map(|i| Name::new(format!("{arg}.{i}"))); + + let mut new_rules = vec![]; + for mut rule in rules { + let pat = rule.pats[0].clone(); + let old_pats = rule.pats.split_off(1); + + // Extract subpats from the tuple pattern + let mut new_pats = match pat { + Pattern::Tup(sub_pats) => sub_pats, + Pattern::Var(var) => { + if let Some(var) = var { + // Rebuild the tuple if it was a var pattern + let tup = Term::Tup { els: new_args.clone().map(|nam| Term::Var { nam }).collect() }; + rule.body.subst(&var, &tup); + } + new_args.clone().map(|nam| Pattern::Var(Some(nam))).collect() + } + _ => unreachable!(), + }; + new_pats.extend(old_pats); + + let new_rule = Rule { pats: new_pats, body: rule.body }; + new_rules.push(new_rule); + } + + let bnd = new_args.clone().map(Some).collect(); + let args = new_args.chain(old_args).collect(); + let nxt = simplify_rule_match(args, new_rules, ctrs, adts)?; + let term = Term::Ltp { bnd, val: Box::new(Term::Var { nam: arg }), nxt: Box::new(nxt) }; + + Ok(term) +} + +fn num_rule( + mut args: Vec, + rules: Vec, + ctrs: &Constructors, + adts: &Adts, +) -> Result { + // Number match must always have a default case + if !rules.iter().any(|r| r.pats[0].is_wildcard()) { + return Err(DesugarMatchDefErr::NumMissingDefault); + } + + let arg = args[0].clone(); + let args = args.split_off(1); + + let match_var = Name::new(format!("{arg}%matched")); + let pred_var = Name::new(format!("{arg}%matched-1")); + + // Since numbers have infinite (2^60) constructors, they require special treatment. + // We first iterate over each present number then get the default. + let nums = rules + .iter() + .filter_map(|r| if let Pattern::Num(n) = r.pats[0] { Some(n) } else { None }) + .collect::>() + .into_iter() + .collect::>(); + + // Number cases + let mut bodies = vec![]; + for num in nums.iter() { + let mut new_rules = vec![]; + for rule in rules.iter() { + match &rule.pats[0] { + Pattern::Num(n) if n == num => { + let body = rule.body.clone(); + let rule = Rule { pats: rule.pats[1 ..].to_vec(), body }; + new_rules.push(rule); + } + Pattern::Var(var) => { + let mut body = rule.body.clone(); + if let Some(var) = var { + body.subst(var, &Term::Num { val: *num }); + } + let rule = Rule { pats: rule.pats[1 ..].to_vec(), body }; + new_rules.push(rule); + } + _ => (), + } + } + let body = simplify_rule_match(args.clone(), new_rules, ctrs, adts)?; + bodies.push(body); + } + + // Default case + let mut new_rules = vec![]; + for rule in rules { + if let Pattern::Var(var) = &rule.pats[0] { + let mut body = rule.body.clone(); + if let Some(var) = var { + let last_num = *nums.last().unwrap(); + let var_recovered = Term::add_num(Term::Var { nam: pred_var.clone() }, 1 + last_num); + body.subst(var, &var_recovered); + } + let rule = Rule { pats: rule.pats[1 ..].to_vec(), body }; + new_rules.push(rule); + } + } + let default_body = simplify_rule_match(args, new_rules, ctrs, adts)?; + + let term = bodies.into_iter().enumerate().rfold(default_body, |term, (i, body)| { + let zero = (NumCtr::Num(0), body); + let succ = (NumCtr::Succ(Some(pred_var.clone())), term); + let mut swt = Term::Swt { arg: Box::new(Term::Var { nam: match_var.clone() }), rules: vec![zero, succ] }; + + let val = if i > 0 { + // let %matched = (%matched-1 +1 +num_i-1 - num_i) + // switch %matched { 0: body_i; _: acc } + // nums[i] >= nums[i-1]+1, so we do a sub here. + Term::sub_num(Term::Var { nam: pred_var.clone() }, nums[i] - 1 - nums[i - 1]) + } else { + // let %matched = (arg -num_0); + // switch %matched { 0: body_0; _: acc} + Term::sub_num(Term::Var { nam: arg.clone() }, nums[i]) + }; + + if let Term::Var { .. } = &val { + // No need to create a let expression if it's just a rename. + // We know that the bound value is a uniquely named var, so we can subst. + swt.subst(&match_var, &val); + swt + } else { + Term::Let { nam: Some(match_var.clone()), val: Box::new(val), nxt: Box::new(swt) } + } + }); + + Ok(term) +} + +/// When the first column has constructors, create a branch on the constructors +/// of the first arg. +/// +/// The extracted nested patterns and remaining args are handled recursively in +/// a nested expression for each match arm. +/// +/// If we imagine a complex match expression representing what's left of the +/// encoding of a pattern matching function: +/// ```hvm +/// data MyType = (CtrA ctrA_field0 ... ctrA_fieldA) | (CtrB ctrB_field0 ... ctrB_fieldB) | CtrC | ... +/// +/// case x0 ... xN { +/// (CtrA p0_0_0 ... p0_A) p0_1 ... p0_N : (Body0 p0_0_0 ... p0_0_A p0_1 ... p0_N) +/// ... +/// varI pI_1 ... pI_N: (BodyI varI pI_1 ... pI_N) +/// ... +/// (CtrB pJ_0_0 ... pJ_0_B) pJ_1 ... pJ_N: (BodyJ pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N) +/// ... +/// (CtrC) pK_1 ... pK_N: (BodyK p_1 ... pK_N) +/// ... +/// } +/// ``` +/// is converted into +/// ```hvm +/// match x0 { +/// CtrA: case x.ctrA_field0 ... x.ctrA_fieldA x1 ... xN { +/// p0_0_0 ... p0_0_B p0_1 ... p0_N : +/// (Body0 p0_0_0 ... p0_0_B ) +/// x.ctrA_field0 ... x.ctrA_fieldA pI_1 ... pI_N: +/// use varI = (CtrA x.ctrA_field0 ... x.ctrA_fieldN); (BodyI varI pI_1 ... pI_N) +/// ... +/// } +/// CtrB: case x.ctrB_field0 ... x.ctrB_fieldB x1 ... xN { +/// x.ctrB_field0 ... x.ctrB_fieldB pI_1 ... pI_N: +/// use varI = (CtrB x.ctrB_field0 ... x.ctrB_fieldB); (BodyI varI pI_1 ... pI_N) +/// pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N : +/// (BodyJ pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N) +/// ... +/// } +/// CtrC: case * x1 ... xN { +/// * pI_1 ... pI_N: +/// use varI = CtrC; (BodyI varI pI_1 ... pI_N) +/// * pK_1 ... pK_N: +/// (BodyK p_1 ... pK_N) +/// ... +/// } +/// ... +/// } +/// ``` +/// Where `case` represents a call of the [`simplify_rule_match`] function. +fn switch_rule( + mut args: Vec, + rules: Vec, + adt_name: Name, + ctrs: &Constructors, + adts: &Adts, +) -> Result { + let arg = args[0].clone(); + let old_args = args.split_off(1); + + let mut new_arms = vec![]; + for (ctr, fields) in &adts[&adt_name].ctrs { + let new_args = fields.iter().map(|f| Name::new(format!("{arg}.{f}"))); + let args = new_args.clone().chain(old_args.clone()).collect(); + + let mut new_rules = vec![]; + for rule in &rules { + let old_pats = rule.pats[1 ..].to_vec(); + match &rule.pats[0] { + // Same ctr, extract subpats. + // (Ctr pat0_0 ... pat0_m) pat1 ... patN: body + // becomes + // pat0_0 ... pat0_m pat1 ... patN: body + Pattern::Ctr(found_ctr, new_pats) if ctr == found_ctr => { + let pats = new_pats.iter().cloned().chain(old_pats).collect(); + let body = rule.body.clone(); + let rule = Rule { pats, body }; + new_rules.push(rule); + } + // Var, match and rebuild the constructor. + // var pat1 ... patN: body + // becomes + // arg0.field0 ... arg0.fieldM pat1 ... patN: + // use var = (Ctr arg0.field0 ... arg0.fieldM); body + Pattern::Var(var) => { + let new_pats = new_args.clone().map(|n| Pattern::Var(Some(n))); + let pats = new_pats.chain(old_pats.clone()).collect(); + let mut body = rule.body.clone(); + let reconstructed_var = + Term::call(Term::Ref { nam: ctr.clone() }, new_args.clone().map(|nam| Term::Var { nam })); + if let Some(var) = var { + body.subst(var, &reconstructed_var); + } + let rule = Rule { pats, body }; + new_rules.push(rule); + } + _ => (), + } + } + + if new_rules.is_empty() { + return Err(DesugarMatchDefErr::AdtNotExhaustive { adt: adt_name, ctr: ctr.clone() }); + } + + let body = simplify_rule_match(args, new_rules, ctrs, adts)?; + new_arms.push((Some(ctr.clone()), new_args.map(Some).collect(), body)); + } + let term = Term::Mat { arg: Box::new(Term::Var { nam: arg }), rules: new_arms }; + Ok(term) +} + +/// Pattern types. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Type { + /// Variables/wildcards. + Any, + /// A native tuple. + Tup(usize), + /// A sequence of arbitrary numbers ending in a variable. + Num, + /// Adt constructors declared with the `data` syntax. + Adt(Name), +} + +impl Type { + // Infers the type of a column of a pattern matrix, from the rules of a function def. + fn infer_from_def_arg( + rules: &[Rule], + arg_idx: usize, + ctrs: &Constructors, + ) -> Result { + let pats = rules.iter().map(|r| &r.pats[arg_idx]); + let mut arg_type = Type::Any; + for pat in pats { + arg_type = match (arg_type, pat.to_type(ctrs)) { + (Type::Any, found) => found, + (expected, Type::Any) => expected, + + (Type::Adt(expected), Type::Adt(found)) if found == expected => Type::Adt(expected), + + (Type::Num, Type::Num) => Type::Num, + + (Type::Tup(a), Type::Tup(b)) if a == b => Type::Tup(a), + + (expected, found) => { + return Err(DesugarMatchDefErr::TypeMismatch { expected, found, pat: pat.clone() }); + } + }; + } + Ok(arg_type) + } +} + +impl Pattern { + fn to_type(&self, ctrs: &Constructors) -> Type { + match self { + Pattern::Var(_) => Type::Any, + Pattern::Ctr(ctr_nam, _) => { + let adt_nam = ctrs.get(ctr_nam).expect("Unknown constructor '{ctr_nam}'"); + Type::Adt(adt_nam.clone()) + } + Pattern::Tup(args) => Type::Tup(args.len()), + Pattern::Num(_) => Type::Num, + Pattern::Lst(..) => Type::Adt(builtins::LIST.into()), + Pattern::Str(..) => Type::Adt(builtins::STRING.into()), + } + } +} + +impl std::fmt::Display for Type { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + Type::Any => write!(f, "any"), + Type::Tup(n) => write!(f, "{n}-tuple"), + Type::Num => write!(f, "number"), + Type::Adt(nam) => write!(f, "{nam}"), + } + } +} + +impl ToStringVerbose for DesugarMatchDefErr { + fn to_string_verbose(&self, _verbose: bool) -> String { + match self { + DesugarMatchDefErr::AdtNotExhaustive { adt, ctr } => { + format!("Non-exhaustive pattern matching rule. Constructor '{ctr}' of type '{adt}' not covered") + } + DesugarMatchDefErr::TypeMismatch { expected, found, pat } => { + format!( + "Type mismatch in pattern matching rule. Expected a constructor of type '{}', found '{}' with type '{}'.", + expected, pat, found + ) + } + DesugarMatchDefErr::NumMissingDefault => { + "Non-exhaustive pattern matching rule. Default case of number type not covered.".to_string() + } + DesugarMatchDefErr::RepeatedBind { bind } => { + format!("Repeated bind in pattern matching rule: '{bind}'.") + } + } + } +} diff --git a/src/term/transform/encode_adts.rs b/src/term/transform/encode_adts.rs index a4a51f40..9759880f 100644 --- a/src/term/transform/encode_adts.rs +++ b/src/term/transform/encode_adts.rs @@ -1,6 +1,7 @@ use crate::term::{AdtEncoding, Book, Definition, Name, Rule, Tag, Term}; impl Book { + /// Defines a function for each constructor in each ADT in the book. pub fn encode_adts(&mut self, adt_encoding: AdtEncoding) { let mut defs = vec![]; for (adt_name, adt) in &self.adts { diff --git a/src/term/transform/encode_pattern_matching.rs b/src/term/transform/encode_match_terms.rs similarity index 53% rename from src/term/transform/encode_pattern_matching.rs rename to src/term/transform/encode_match_terms.rs index 6cccd5c3..917a4dae 100644 --- a/src/term/transform/encode_pattern_matching.rs +++ b/src/term/transform/encode_match_terms.rs @@ -1,96 +1,103 @@ -use crate::term::{ - check::type_check::infer_match_arg_type, AdtEncoding, Adts, Book, Constructors, Name, NumCtr, Pattern, - Rule, Tag, Term, Type, -}; +use crate::term::{AdtEncoding, Book, Constructors, Name, NumCtr, Tag, Term}; impl Book { - /// Encodes simple pattern matching expressions in the book into - /// their native/core form. - /// See [`super::simplify_matches::simplify_match_expression`] for - /// the meaning of "simple" used here. + /// Encodes pattern matching expressions in the book into their + /// native/core form. Must be run after [`Ctr::fix_match_terms`]. /// /// ADT matches are encoded based on `adt_encoding`. /// /// Num matches are encoded as a sequence of native num matches (on 0 and 1+). /// /// Var and pair matches become a let expression. - pub fn encode_simple_matches(&mut self, adt_encoding: AdtEncoding) { + pub fn encode_matches(&mut self, adt_encoding: AdtEncoding) { for def in self.defs.values_mut() { for rule in &mut def.rules { - rule.body.encode_simple_matches(&self.ctrs, &self.adts, adt_encoding); + rule.body.encode_matches(&self.ctrs, adt_encoding); } } } } impl Term { - pub fn encode_simple_matches(&mut self, ctrs: &Constructors, adts: &Adts, adt_encoding: AdtEncoding) { + pub fn encode_matches(&mut self, ctrs: &Constructors, adt_encoding: AdtEncoding) { Term::recursive_call(move || { for child in self.children_mut() { - child.encode_simple_matches(ctrs, adts, adt_encoding) + child.encode_matches(ctrs, adt_encoding) } - if let Term::Mat { .. } = self { - debug_assert!(self.is_simple_match(ctrs, adts), "{self}"); - let Term::Mat { args, rules } = self else { unreachable!() }; - let arg = std::mem::take(&mut args[0]); + if let Term::Mat { arg, rules } = self { + let arg = std::mem::take(arg.as_mut()); let rules = std::mem::take(rules); *self = encode_match(arg, rules, ctrs, adt_encoding); + } else if let Term::Swt { arg, rules } = self { + let arg = std::mem::take(arg.as_mut()); + let rules = std::mem::take(rules); + *self = encode_switch(arg, rules); } }) } } -fn encode_match(arg: Term, rules: Vec, ctrs: &Constructors, adt_encoding: AdtEncoding) -> Term { - let typ = infer_match_arg_type(&rules, 0, ctrs).unwrap(); - match typ { - Type::Any | Type::Tup(_) => { - 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) => encode_adt(arg, rules, adt, adt_encoding), - } -} +fn encode_match( + arg: Term, + rules: Vec<(Option, Vec>, Term)>, + ctrs: &Constructors, + adt_encoding: AdtEncoding, +) -> Term { + let adt = ctrs.get(rules[0].0.as_ref().unwrap()).unwrap(); -/// 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) } + // ADT Encoding depends on compiler option + match adt_encoding { + // (x @field1 @field2 ... body1 @field1 body2 ...) + AdtEncoding::Scott => { + let mut arms = vec![]; + for rule in rules { + let body = rule.1.iter().cloned().rfold(rule.2, |bod, nam| Term::lam(nam, bod)); + arms.push(body); + } + Term::call(arg, arms) + } + // #adt_name(x arm[0] arm[1] ...) + AdtEncoding::TaggedScott => { + let mut arms = vec![]; + for rule in rules.into_iter() { + let body = + rule.1.iter().cloned().rfold(rule.2, |bod, nam| Term::tagged_lam(Tag::adt_name(adt), nam, bod)); + arms.push(body); + } + Term::tagged_call(Tag::adt_name(adt), arg, arms) + } + } } /// 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 { +fn encode_switch(arg: Term, mut rules: Vec<(NumCtr, Term)>) -> 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); + let NumCtr::Succ(last_var) = last_rule.0 else { unreachable!() }; + let last_arm = Term::lam(last_var, last_rule.1); rules.into_iter().rfold(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 zero = (NumCtr::Num(0), rule.1); + let one = (NumCtr::Succ(None), term); + let rules = vec![zero, one]; - let Pattern::Num(NumCtr::Num(num)) = rule.pats.into_iter().next().unwrap() else { unreachable!() }; + let NumCtr::Num(num) = rule.0 else { unreachable!() }; if num == 0 { - Term::Mat { args: vec![arg.clone()], rules } + Term::Swt { arg: Box::new(arg.clone()), rules } } else { - let mat = Term::Mat { args: vec![Term::Var { nam: match_var.clone() }], rules }; - Term::named_lam(match_var.clone(), mat) + let swt = Term::Swt { arg: Box::new(Term::Var { nam: match_var.clone() }), rules }; + Term::named_lam(match_var.clone(), swt) } }) } -/// Convert into a sequence of native matches on (- n num_case) +/* /// 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 { @@ -109,7 +116,7 @@ fn encode_num(arg: Term, mut rules: Vec) -> Term { // 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::switch( Term::sub_num(arg.unwrap(), *val), rule.body, go(rules, last_rule, Some(*val), None), @@ -123,7 +130,7 @@ fn encode_num(arg: Term, mut rules: Vec) -> Term { let pred_nam = Name::from("%p"); Term::named_lam( pred_nam.clone(), - Term::native_num_match( + Term::switch( 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), @@ -147,29 +154,4 @@ fn encode_num(arg: Term, mut rules: Vec) -> Term { 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) -> Term { - match adt_encoding { - // (x @field1 @field2 ... body1 @field1 body2 ...) - AdtEncoding::Scott => { - let mut arms = vec![]; - for rule in rules { - let body = rule.pats[0].binds().cloned().rfold(rule.body, |bod, nam| Term::lam(nam, bod)); - arms.push(body); - } - Term::call(arg, arms) - } - // #adt_name(x arm[0] arm[1] ...) - AdtEncoding::TaggedScott => { - let mut arms = vec![]; - for rule in rules.into_iter() { - let body = rule.pats[0] - .binds() - .cloned() - .rfold(rule.body, |bod, nam| Term::tagged_lam(Tag::adt_name(&adt), nam, bod)); - arms.push(body); - } - Term::tagged_call(Tag::adt_name(&adt), arg, arms) - } - } -} + */ diff --git a/src/term/transform/fix_match_terms.rs b/src/term/transform/fix_match_terms.rs new file mode 100644 index 00000000..904d7359 --- /dev/null +++ b/src/term/transform/fix_match_terms.rs @@ -0,0 +1,278 @@ +use crate::{ + diagnostics::{Diagnostics, ToStringVerbose, WarningType}, + term::{Adts, Constructors, Ctx, Name, NumCtr, Term}, +}; +use std::collections::HashMap; + +enum FixMatchErr { + AdtMismatch { expected: Name, found: Name, ctr: Name }, + NonExhaustiveMatch { typ: Name, missing: Name }, + NumMismatch { expected: NumCtr, found: NumCtr }, + IrrefutableMatch { var: Option }, + UnreachableMatchArms { var: Option }, + ExtraSwitchArms, + RedundantArm { ctr: Name }, +} + +impl Ctx<'_> { + /// Convert all match and switch expressions to a normalized form. + /// * For matches, resolve the constructors and create the name of the field variables. + /// * For switches, resolve the succ case ("_") and create the name of the pred variable. + /// * If the match arg is not a variable, it is separated into a let expression and bound to "%matched" + /// * Check for redundant arms and non-exhaustive matches. + /// + /// Example: + /// For the program + /// ```hvm + /// data MyList = (Cons h t) | Nil + /// match x { + /// Cons: (A x.h x.t) + /// Nil: switch (Foo y) { 0: B; 1: C; _: D } + /// } + /// ``` + /// The following AST transformations will be made: + /// * The binds `x.h` and `x.t` will be generated and stored in the match term. + /// * `(Foo y)`` will be put in a let expression, bound to the variable `%matched`; + /// * The bind `%matched-2` will be generated and stored in the switch term. + /// * If either was missing one of the match cases (a number or a constructor), we'd get an error. + /// * If either included one of the cases more than once (including wildcard patterns), we'd get a warning. + /// ```hvm + /// match x { + /// Cons: (A x.h x.t) + /// Nil: let %matched = (Foo y); switch %matched { 0: B; 1: C; _: D } + /// } + /// ``` + pub fn fix_match_terms(&mut self) -> Result<(), Diagnostics> { + self.info.start_pass(); + + for def in self.book.defs.values_mut() { + for rule in def.rules.iter_mut() { + let errs = rule.body.fix_match_terms(&self.book.ctrs, &self.book.adts); + + for err in errs { + match err { + FixMatchErr::ExtraSwitchArms { .. } + | FixMatchErr::AdtMismatch { .. } + | FixMatchErr::NumMismatch { .. } + | FixMatchErr::NonExhaustiveMatch { .. } => self.info.add_rule_error(err, def.name.clone()), + + FixMatchErr::IrrefutableMatch { .. } => { + self.info.add_rule_warning(err, WarningType::IrrefutableMatch, def.name.clone()) + } + FixMatchErr::UnreachableMatchArms { .. } => { + self.info.add_rule_warning(err, WarningType::UnreachableMatch, def.name.clone()) + } + FixMatchErr::RedundantArm { .. } => { + self.info.add_rule_warning(err, WarningType::RedundantMatch, def.name.clone()) + } + } + } + } + } + + self.info.fatal(()) + } +} + +impl Term { + fn fix_match_terms(&mut self, ctrs: &Constructors, adts: &Adts) -> Vec { + Term::recursive_call(move || { + let mut errs = Vec::new(); + + for child in self.children_mut() { + let mut e = child.fix_match_terms(ctrs, adts); + errs.append(&mut e); + } + + if let Term::Mat { .. } = self { + self.fix_match(&mut errs, ctrs, adts); + } else if let Term::Swt { .. } = self { + self.fix_switch(&mut errs); + } + + errs + }) + } + + fn fix_match(&mut self, errs: &mut Vec, ctrs: &Constructors, adts: &Adts) { + let Term::Mat { arg, rules } = self else { unreachable!() }; + + let (arg_nam, arg) = extract_match_arg(arg); + + // Normalize arms + if let Some(ctr_nam) = &rules[0].0 + && let Some(adt_nam) = ctrs.get(ctr_nam) + { + let adt_ctrs = &adts[adt_nam].ctrs; + + // For each arm, decide to which arm of the fixed match they map to. + let mut bodies = HashMap::<&Name, Option>::from_iter(adt_ctrs.iter().map(|(ctr, _)| (ctr, None))); + for rule_idx in 0 .. rules.len() { + if let Some(ctr_nam) = &rules[rule_idx].0 + && let Some(found_adt) = ctrs.get(ctr_nam) + { + // Ctr arm + if found_adt == adt_nam { + let body = bodies.get_mut(ctr_nam).unwrap(); + if body.is_none() { + // Use this rule for this constructor + *body = Some(rules[rule_idx].2.clone()); + } else { + errs.push(FixMatchErr::RedundantArm { ctr: ctr_nam.clone() }); + } + } else { + errs.push(FixMatchErr::AdtMismatch { + expected: adt_nam.clone(), + found: found_adt.clone(), + ctr: ctr_nam.clone(), + }) + } + } else { + // Var arm + if rule_idx != rules.len() - 1 { + errs.push(FixMatchErr::UnreachableMatchArms { var: rules[rule_idx].0.clone() }); + rules.truncate(rule_idx + 1); + } + // Use this rule for all remaining constructors + for (ctr, body) in bodies.iter_mut() { + if body.is_none() { + let mut new_body = rules[rule_idx].2.clone(); + if let Some(var) = &rules[rule_idx].0 { + new_body.subst(var, &rebuild_ctr(&arg_nam, ctr, &adts[adt_nam].ctrs[&**ctr])); + } + *body = Some(new_body); + } + } + + break; + } + } + + // Build the match arms, with all constructors + let mut new_rules = vec![]; + for (ctr, fields) in adt_ctrs.iter() { + let fields = fields.iter().map(|f| Some(match_field(&arg_nam, f))).collect::>(); + let body = if let Some(Some(body)) = bodies.remove(ctr) { + body + } else { + errs.push(FixMatchErr::NonExhaustiveMatch { typ: adt_nam.clone(), missing: ctr.clone() }); + Term::Err + }; + new_rules.push((Some(ctr.clone()), fields, body)); + } + *rules = new_rules; + } else { + errs.push(FixMatchErr::IrrefutableMatch { var: rules[0].0.clone() }); + + let match_var = rules[0].0.take(); + *self = std::mem::take(&mut rules[0].2); + if let Some(var) = match_var { + self.subst(&var, &Term::Var { nam: arg_nam.clone() }); + } + } + + *self = apply_arg(std::mem::take(self), arg_nam, arg); + } + + /// For switches, the only necessary change is to add the implicit pred bind to the AST. + /// + /// Check that all numbers are in order and no cases are skipped. + /// Also check that we have a default case at the end, binding the pred. + fn fix_switch(&mut self, errs: &mut Vec) { + let Term::Swt { arg, rules } = self else { unreachable!() }; + + let (arg_nam, arg) = extract_match_arg(arg); + + let mut has_num = false; + let len = rules.len(); + for i in 0 .. len { + let ctr = &mut rules[i].0; + match ctr { + NumCtr::Num(n) if i as u64 == *n => { + has_num = true; + } + NumCtr::Num(n) => { + errs.push(FixMatchErr::NumMismatch { expected: NumCtr::Num(i as u64), found: NumCtr::Num(*n) }); + break; + } + NumCtr::Succ(pred) => { + if !has_num { + errs.push(FixMatchErr::NumMismatch { + expected: NumCtr::Num(i as u64), + found: NumCtr::Succ(pred.clone()), + }); + break; + } + *pred = Some(Name::new(format!("{arg_nam}-{i}"))); + if i != len - 1 { + errs.push(FixMatchErr::ExtraSwitchArms); + rules.truncate(i + 1); + break; + } + } + } + } + + *self = apply_arg(std::mem::take(self), arg_nam, arg); + } +} + +fn extract_match_arg(arg: &mut Term) -> (Name, Option) { + if let Term::Var { nam } = arg { + (nam.clone(), None) + } else { + let nam = Name::from("%matched"); + let arg = std::mem::replace(arg, Term::Var { nam: nam.clone() }); + (nam, Some(arg)) + } +} + +fn apply_arg(term: Term, arg_nam: Name, arg: Option) -> Term { + if let Some(arg) = arg { + Term::Let { nam: Some(arg_nam), val: Box::new(arg), nxt: Box::new(term) } + } else { + term + } +} + +fn match_field(arg: &Name, field: &Name) -> Name { + Name::new(format!("{arg}.{field}")) +} + +fn rebuild_ctr(arg: &Name, ctr: &Name, fields: &[Name]) -> Term { + let ctr = Term::Ref { nam: ctr.clone() }; + let fields = fields.iter().map(|f| Term::Var { nam: match_field(arg, f) }); + Term::call(ctr, fields) +} + +impl ToStringVerbose for FixMatchErr { + fn to_string_verbose(&self, _verbose: bool) -> String { + match self { + FixMatchErr::AdtMismatch { expected, found, ctr } => format!( + "Type mismatch in 'match' expression: Expected a constructor of type '{expected}', found '{ctr}' of type '{found}'" + ), + FixMatchErr::NonExhaustiveMatch { typ, missing } => { + format!("Non-exhaustive 'match' expression of type '{typ}'. Case '{missing}' not covered.") + } + FixMatchErr::NumMismatch { expected, found } => { + format!( + "Malformed 'switch' expression. Expected case '{expected}', found '{found}'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case." + ) + } + FixMatchErr::IrrefutableMatch { var } => format!( + "Irrefutable 'match' expression. All cases after '{}' will be ignored. If this is not a mistake, consider using a 'let' expression instead.", + var.as_ref().unwrap_or(&Name::new("*")) + ), + FixMatchErr::UnreachableMatchArms { var } => format!( + "Unreachable arms in 'match' expression. All cases after '{}' will be ignored.", + var.as_ref().unwrap_or(&Name::new("*")) + ), + FixMatchErr::ExtraSwitchArms => { + "Extra arms in 'switch' expression. No rules should come after the default.".to_string() + } + FixMatchErr::RedundantArm { ctr } => { + format!("Redundant arm in 'match' expression. Case '{ctr}' appears more than once.") + } + } + } +} diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs index 3a3aae3d..de8d57ce 100644 --- a/src/term/transform/float_combinators.rs +++ b/src/term/transform/float_combinators.rs @@ -141,7 +141,7 @@ impl Term { impl Term { pub fn float_children_mut(&mut self) -> impl DoubleEndedIterator { - multi_iterator!(FloatIter { Zero, Two, Vec, Mat, App }); + multi_iterator!(FloatIter { Zero, Two, Vec, Mat, App, Swt }); match self { Term::App { fun, arg, .. } => { let mut args = vec![arg.as_mut()]; @@ -153,11 +153,15 @@ impl Term { args.push(app); FloatIter::App(args) } - Term::Mat { args, rules } => { - FloatIter::Mat(args.iter_mut().chain(rules.iter_mut().map(|r| &mut r.body))) + Term::Mat { arg, rules } => { + FloatIter::Mat([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.2))) + } + Term::Swt { arg, rules } => { + FloatIter::Swt([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.1))) } Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => FloatIter::Vec(els), - Term::Let { val: fst, nxt: snd, .. } + Term::Ltp { val: fst, nxt: snd, .. } + | Term::Let { val: fst, nxt: snd, .. } | Term::Use { val: fst, nxt: snd, .. } | Term::Dup { val: fst, nxt: snd, .. } | Term::Opx { fst, snd, .. } => FloatIter::Two([fst.as_mut(), snd.as_mut()]), diff --git a/src/term/transform/inline.rs b/src/term/transform/inline.rs index 9b822d7c..cd75fec1 100644 --- a/src/term/transform/inline.rs +++ b/src/term/transform/inline.rs @@ -53,9 +53,9 @@ impl Term { Term::Chn { .. } | Term::Lnk { .. } => false, Term::Let { .. } => false, Term::App { .. } => false, - Term::Dup { .. } => false, + Term::Dup { .. } | Term::Ltp { .. } => false, Term::Opx { .. } => false, - Term::Mat { .. } => false, + Term::Mat { .. } | Term::Swt { .. } => false, Term::Ref { .. } => false, Term::Nat { .. } | Term::Str { .. } | Term::Lst { .. } | Term::Use { .. } => unreachable!(), diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs index c899e28c..12c0ace4 100644 --- a/src/term/transform/linearize_matches.rs +++ b/src/term/transform/linearize_matches.rs @@ -1,26 +1,25 @@ -use crate::term::{Book, Name, Term}; -use itertools::Itertools; +use crate::term::{Book, Name, NumCtr, Term}; use std::collections::{BTreeMap, BTreeSet}; impl Book { /// Linearizes the variables between match cases, transforming them into combinators when possible. - pub fn linearize_simple_matches(&mut self, lift_all_vars: bool) { + pub fn linearize_matches(&mut self, lift_all_vars: bool) { for def in self.defs.values_mut() { for rule in def.rules.iter_mut() { - rule.body.linearize_simple_matches(lift_all_vars); + rule.body.linearize_matches(lift_all_vars); } } } } impl Term { - fn linearize_simple_matches(&mut self, lift_all_vars: bool) { + fn linearize_matches(&mut self, lift_all_vars: bool) { Term::recursive_call(move || { for child in self.children_mut() { - child.linearize_simple_matches(lift_all_vars); + child.linearize_matches(lift_all_vars); } - if let Term::Mat { .. } = self { + if matches!(self, Term::Mat { .. } | Term::Swt { .. }) { lift_match_vars(self, lift_all_vars); } }) @@ -33,43 +32,71 @@ impl Term { /// If `lift_all_vars`, acts on all variables found in the arms, /// Otherwise, only lift vars that are used on more than one arm. /// -/// Obs: This does not interact unscoped variables +/// Obs: This does not modify unscoped variables pub fn lift_match_vars(match_term: &mut Term, lift_all_vars: bool) -> &mut Term { - let Term::Mat { args: _, rules } = match_term else { unreachable!() }; - - let free = rules.iter().flat_map(|rule| { - rule - .body - .free_vars() - .into_iter() - .filter(|(name, _)| !rule.pats.iter().any(|p| p.binds().flatten().contains(name))) - }); - - // Collect the vars. - // We need consistent iteration order. - let free_vars: BTreeSet = if lift_all_vars { - free.map(|(name, _)| name).collect() - } else { - free - .fold(BTreeMap::new(), |mut acc, (name, count)| { - *acc.entry(name).or_insert(0) += count.min(1); - acc + // Collect match arms with binds + let arms: Vec<_> = match match_term { + Term::Mat { arg: _, rules } => { + rules.iter().map(|(_, binds, body)| (binds.iter().flatten().cloned().collect(), body)).collect() + } + Term::Swt { arg: _, rules } => rules + .iter() + .map(|(ctr, body)| match ctr { + NumCtr::Num(_) => (vec![], body), + NumCtr::Succ(None) => (vec![], body), + NumCtr::Succ(Some(var)) => (vec![var.clone()], body), }) + .collect(), + _ => unreachable!(), + }; + + // Collect all free vars in the match arms + let mut free_vars = Vec::>::new(); + for (binds, body) in arms { + let mut arm_free_vars = body.free_vars(); + for bind in binds { + arm_free_vars.remove(&bind); + } + free_vars.push(arm_free_vars.into_keys().collect()); + } + + // Collect the vars to lift + // We need consistent iteration order. + let vars_to_lift: BTreeSet = if lift_all_vars { + free_vars.into_iter().flatten().collect() + } else { + // If not lifting all vars, lift only those that are used in more than one arm. + let mut vars_to_lift = BTreeMap::::new(); + for free_vars in free_vars { + for free_var in free_vars { + *vars_to_lift.entry(free_var).or_default() += 1; + } + } + vars_to_lift .into_iter() - .filter(|(_, count)| *count >= 2) - .map(|(name, _)| name) + .filter_map(|(var, arm_count)| if arm_count >= 2 { Some(var) } else { None }) .collect() }; // Add lambdas to the arms - for rule in rules { - let old_body = std::mem::take(&mut rule.body); - rule.body = free_vars.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body)); + match match_term { + Term::Mat { arg: _, rules } => { + for rule in rules { + let old_body = std::mem::take(&mut rule.2); + rule.2 = vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body)); + } + } + Term::Swt { arg: _, rules } => { + for rule in rules { + let old_body = std::mem::take(&mut rule.1); + rule.1 = vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body)); + } + } + _ => unreachable!(), } // Add apps to the match - let old_match = std::mem::take(match_term); - *match_term = free_vars.into_iter().fold(old_match, Term::arg_call); + *match_term = vars_to_lift.into_iter().fold(std::mem::take(match_term), Term::arg_call); get_match_reference(match_term) } @@ -81,7 +108,7 @@ fn get_match_reference(mut match_term: &mut Term) -> &mut Term { loop { match match_term { Term::App { tag: _, fun, arg: _ } => match_term = fun.as_mut(), - Term::Mat { .. } => return match_term, + Term::Swt { .. } | Term::Mat { .. } => return match_term, _ => unreachable!(), } } diff --git a/src/term/transform/linearize_vars.rs b/src/term/transform/linearize_vars.rs index fb1a0fbf..d1181862 100644 --- a/src/term/transform/linearize_vars.rs +++ b/src/term/transform/linearize_vars.rs @@ -1,4 +1,4 @@ -use crate::term::{Book, Name, Pattern, Tag, Term}; +use crate::term::{Book, Name, Tag, Term}; use std::collections::HashMap; /// Erases variables that weren't used, dups the ones that were used more than once. @@ -36,7 +36,7 @@ impl Term { fn term_to_affine(term: &mut Term, var_uses: &mut HashMap) { Term::recursive_call(move || match term { - Term::Let { pat: Pattern::Var(Some(nam)), val, nxt } => { + Term::Let { nam: Some(nam), val, nxt } => { // TODO: This is swapping the order of how the bindings are // used, since it's not following the usual AST order (first // val, then nxt). Doesn't change behaviour, but looks strange. @@ -51,7 +51,7 @@ fn term_to_affine(term: &mut Term, var_uses: &mut HashMap) { let val = std::mem::take(val); let nxt = std::mem::take(nxt); - *term = Term::Let { pat: Pattern::Var(None), val, nxt }; + *term = Term::Let { nam: None, val, nxt }; } else { *term = std::mem::take(nxt.as_mut()); } @@ -69,7 +69,7 @@ fn term_to_affine(term: &mut Term, var_uses: &mut HashMap) { } } - Term::Let { pat: Pattern::Var(None), val, nxt } => { + Term::Let { nam: None, val, nxt } => { term_to_affine(nxt, var_uses); if val.has_unscoped() { diff --git a/src/term/transform/match_defs_to_term.rs b/src/term/transform/match_defs_to_term.rs deleted file mode 100644 index 97c603ad..00000000 --- a/src/term/transform/match_defs_to_term.rs +++ /dev/null @@ -1,55 +0,0 @@ -use crate::term::{Book, Definition, Name, Rule, Term}; - -impl Book { - /// See [`Definition::convert_match_def_to_term`]. - pub fn convert_match_def_to_term(&mut self) { - for def in self.defs.values_mut() { - def.convert_match_def_to_term(); - } - } -} - -impl Definition { - /// Converts a pattern matching function with multiple rules and args, into a - /// single rule without pattern matching. - /// - /// Moves the pattern matching of the rules into a complex match expression. - /// - /// Example: - /// - /// ```hvm - /// if True then else = then - /// if False then else = else - /// ``` - /// - /// becomes - /// - /// ```hvm - /// if = @%x0 @%x1 @%x2 match %x0, %x1, %x2 { - /// True then else: then - /// False then else: else - /// } - /// ``` - /// - /// Preconditions: Rule arities must be correct. - pub fn convert_match_def_to_term(&mut self) { - let rule = def_rules_to_match(std::mem::take(&mut self.rules)); - self.rules = vec![rule]; - } -} - -fn def_rules_to_match(rules: Vec) -> Rule { - let arity = rules[0].arity(); - - if arity == 0 { - // If no args, not pattern matching function, nothings needs to be done. - rules.into_iter().next().unwrap() - } else { - let nams = (0 .. arity).map(|i| Name::new(format!("%x{i}"))); - - let args = nams.clone().map(|nam| Term::Var { nam }).collect(); - let mat = Term::Mat { args, rules }; - let body = nams.rfold(mat, |bod, nam| Term::named_lam(nam, bod)); - Rule { pats: vec![], body } - } -} diff --git a/src/term/transform/mod.rs b/src/term/transform/mod.rs index 5dbc48e9..81d8b427 100644 --- a/src/term/transform/mod.rs +++ b/src/term/transform/mod.rs @@ -2,21 +2,19 @@ pub mod apply_args; pub mod apply_use; pub mod definition_merge; pub mod definition_pruning; -pub mod desugar_implicit_match_binds; -pub mod desugar_let_destructors; +pub mod desugar_match_defs; pub mod encode_adts; -pub mod encode_pattern_matching; +pub mod encode_match_terms; pub mod eta_reduction; +pub mod fix_match_terms; pub mod float_combinators; pub mod inline; pub mod linearize_matches; pub mod linearize_vars; -pub mod match_defs_to_term; pub mod resolve_ctrs_in_pats; pub mod resolve_refs; pub mod resugar_adts; pub mod resugar_builtins; pub mod simplify_main_ref; -pub mod simplify_matches; pub mod simplify_ref_to_ref; pub mod unique_names; diff --git a/src/term/transform/resolve_ctrs_in_pats.rs b/src/term/transform/resolve_ctrs_in_pats.rs index 39a8a155..7e89de87 100644 --- a/src/term/transform/resolve_ctrs_in_pats.rs +++ b/src/term/transform/resolve_ctrs_in_pats.rs @@ -1,4 +1,4 @@ -use crate::term::{Book, Name, Pattern, Term}; +use crate::term::{Book, Name, Pattern}; impl Book { /// Resolve Constructor names inside rule patterns and match patterns, @@ -15,7 +15,6 @@ impl Book { for pat in &mut rule.pats { pat.resolve_ctrs(&is_ctr); } - rule.body.resolve_ctrs_in_pats(&is_ctr); } } } @@ -36,18 +35,3 @@ impl Pattern { } } } - -impl Term { - pub fn resolve_ctrs_in_pats(&mut self, is_ctr: &impl Fn(&Name) -> bool) { - let mut to_resolve = vec![self]; - - while let Some(term) = to_resolve.pop() { - for pat in term.patterns_mut() { - pat.resolve_ctrs(is_ctr); - } - for child in term.children_mut() { - to_resolve.push(child); - } - } - } -} diff --git a/src/term/transform/resugar_adts.rs b/src/term/transform/resugar_adts.rs index 9b0a21cf..f40b3dbd 100644 --- a/src/term/transform/resugar_adts.rs +++ b/src/term/transform/resugar_adts.rs @@ -1,11 +1,13 @@ +use std::collections::VecDeque; + use crate::{ diagnostics::ToStringVerbose, - term::{Adt, AdtEncoding, Book, Name, Pattern, Rule, Tag, Term}, + term::{Adt, AdtEncoding, Book, Name, Tag, Term}, }; pub enum AdtReadbackError { - InvalidAdt, - InvalidAdtMatch, + MalformedCtr(Name), + MalformedMatch(Name), UnexpectedTag(Tag, Tag), } @@ -73,12 +75,13 @@ impl Term { let mut app = &mut *self; let mut current_arm = None; + // One lambda per ctr of this adt for ctr in &adt.ctrs { match app { Term::Lam { tag: Tag::Named(tag), nam, bod } if tag == adt_name => { if let Some(nam) = nam { if current_arm.is_some() { - errs.push(AdtReadbackError::InvalidAdt); + errs.push(AdtReadbackError::MalformedCtr(adt_name.clone())); return; } current_arm = Some((nam.clone(), ctr)); @@ -86,19 +89,20 @@ impl Term { app = bod; } _ => { - errs.push(AdtReadbackError::InvalidAdt); + errs.push(AdtReadbackError::MalformedCtr(adt_name.clone())); return; } } } let Some((arm_name, (ctr, ctr_args))) = current_arm else { - errs.push(AdtReadbackError::InvalidAdt); + errs.push(AdtReadbackError::MalformedCtr(adt_name.clone())); return; }; let mut cur = &mut *app; + // One app per field of this constructor for _ in ctr_args.iter().rev() { let expected_tag = Tag::adt_name(adt_name); @@ -113,7 +117,7 @@ impl Term { return; } _ => { - errs.push(AdtReadbackError::InvalidAdt); + errs.push(AdtReadbackError::MalformedCtr(adt_name.clone())); return; } } @@ -122,7 +126,7 @@ impl Term { match cur { Term::Var { nam } if nam == &arm_name => {} _ => { - errs.push(AdtReadbackError::InvalidAdt); + errs.push(AdtReadbackError::MalformedCtr(adt_name.clone())); return; } } @@ -140,7 +144,7 @@ impl Term { /// ```hvm /// data Option = (Some val) | None /// - /// // This match expression: + /// // Compiling this match expression: /// Option.and = @a @b match a { /// Some: match b { /// Some: 1 @@ -154,11 +158,11 @@ impl Term { /// /// // Which gets resugared as: /// λa λb (match a { - /// (Some *): λc match c { - /// (Some *): 1; - /// (None) : 2 + /// Some: λc match c { + /// Some: 1; + /// None: 2 /// }; - /// (None): λ* 3 + /// None: λ* 3 /// } b) /// ``` fn resugar_match_tagged_scott( @@ -168,61 +172,119 @@ impl Term { adt: &Adt, errs: &mut Vec, ) { - let mut cur = &mut *self; - let mut arms = Vec::new(); + // TODO: This is too complex, refactor this. + let mut cur = &mut *self; + let mut arms = VecDeque::new(); + // Since we don't have access to the match arg when first reading + // the arms, we must store the position of the fields that have + // to be applied to the arm body. + let expected_tag = Tag::adt_name(adt_name); + + // For each match arm, we expect an application where the arm body is the app arg. + // If matching a constructor with N fields, the body should start with N tagged lambdas. for (ctr, ctr_args) in adt.ctrs.iter().rev() { match cur { Term::App { tag: Tag::Named(tag), fun, arg } if tag == adt_name => { - let mut args = Vec::new(); + // We expect a lambda for each field. If we got anything + // else, we have to create an eta-reducible match to get + // the same behaviour. + let mut has_all_fields = true; + let mut fields = Vec::new(); let mut arm = arg.as_mut(); - - for field in ctr_args { - let expected_tag = Tag::adt_name(adt_name); - + for _ in ctr_args.iter() { match arm { Term::Lam { tag, .. } if tag == &expected_tag => { let Term::Lam { nam, bod, .. } = arm else { unreachable!() }; + fields.push(nam.clone()); + arm = bod; + } - args.push(nam.clone().map_or(Pattern::Var(None), |x| Pattern::Var(Some(x)))); - arm = bod.as_mut(); + Term::Lam { tag, .. } => { + errs.push(AdtReadbackError::UnexpectedTag(expected_tag.clone(), tag.clone())); + has_all_fields = false; + break; } _ => { - if let Term::Lam { tag, .. } = arm { - errs.push(AdtReadbackError::UnexpectedTag(expected_tag.clone(), tag.clone())); - } - - let arg = Name::new(format!("{ctr}.{field}")); - args.push(Pattern::Var(Some(arg.clone()))); - *arm = Term::tagged_app(expected_tag, std::mem::take(arm), Term::Var { nam: arg }); + has_all_fields = false; + break; } } } - arms.push((vec![Pattern::Ctr(ctr.clone(), args)], arm)); + if has_all_fields { + arm.resugar_tagged_scott(book, errs); + arms.push_front((Some(ctr.clone()), fields, std::mem::take(arm))); + } else { + // If we didn't find lambdas for all the fields, create the eta-reducible match. + arg.resugar_tagged_scott(book, errs); + let fields = ctr_args.iter().map(|f| Name::new(format!("%{f}"))); + let applied_arm = Term::tagged_call( + expected_tag.clone(), + std::mem::take(arg.as_mut()), + fields.clone().map(|f| Term::Var { nam: f }), + ); + arms.push_front((Some(ctr.clone()), fields.map(Some).collect(), applied_arm)); + } + cur = &mut *fun; } _ => { - errs.push(AdtReadbackError::InvalidAdtMatch); + // Looked like a match but doesn't cover all constructors. + errs.push(AdtReadbackError::MalformedMatch(adt_name.clone())); return; } } } - let args = vec![std::mem::take(cur)]; - let rules = - arms.into_iter().rev().map(|(pats, term)| Rule { pats, body: std::mem::take(term) }).collect(); - *self = Term::Mat { args, rules }; + // Resugar the argument. + cur.resugar_tagged_scott(book, errs); - self.resugar_tagged_scott(book, errs); + // If the match is on a non-var we have to extract it to get usable ctr fields. + // Here we get the arg name and separate the term if it's not a variable. + let (arg, bind) = if let Term::Var { nam } = cur { + (nam.clone(), None) + } else { + (Name::from("%matched"), Some(std::mem::take(cur))) + }; + + // Subst the unique readback names for the field names. + // ex: reading `@a(a @b@c(b c))` we create `@a match a{A: (a.field1 a.field2)}`, + // changing `b` to `a.field1` and `c` to `a.field2`. + for (ctr, fields, body) in arms.iter_mut() { + let mut new_fields = vec![]; + for (field_idx, field) in fields.iter().enumerate() { + if let Some(old_field) = field { + let field_name = &adt.ctrs[ctr.as_ref().unwrap()][field_idx]; + let new_field = Name::new(format!("{arg}.{field_name}")); + new_fields.push(Some(new_field.clone())); + body.subst(old_field, &Term::Var { nam: new_field }); + } + } + *fields = new_fields; + } + + let arms = arms.into_iter().collect::>(); + + *self = if let Some(bind) = bind { + Term::Let { + nam: Some(arg.clone()), + val: Box::new(bind), + nxt: Box::new(Term::Mat { arg: Box::new(Term::Var { nam: arg }), rules: arms }), + } + } else { + Term::Mat { arg: Box::new(Term::Var { nam: arg }), rules: arms } + }; } } impl ToStringVerbose for AdtReadbackError { fn to_string_verbose(&self, _verbose: bool) -> String { match self { - AdtReadbackError::InvalidAdt => "Invalid Adt.".to_string(), - AdtReadbackError::InvalidAdtMatch => "Invalid Adt Match.".to_string(), + AdtReadbackError::MalformedCtr(adt) => format!("Encountered malformed constructor of type '{adt}'."), + AdtReadbackError::MalformedMatch(adt) => { + format!("Encountered malformed 'match' expression of type '{adt}'") + } AdtReadbackError::UnexpectedTag(expected, found) => { let found = if let Tag::Static = found { "no tag".to_string() } else { format!("'{found}'") }; format!("Unexpected tag found during Adt readback, expected '{}', but found {}.", expected, found) diff --git a/src/term/transform/simplify_matches.rs b/src/term/transform/simplify_matches.rs deleted file mode 100644 index 880f2b88..00000000 --- a/src/term/transform/simplify_matches.rs +++ /dev/null @@ -1,459 +0,0 @@ -use crate::{ - diagnostics::{Diagnostics, ToStringVerbose, ERR_INDENT_SIZE}, - term::{ - check::type_check::{infer_match_arg_type, TypeMismatchErr}, - display::{DisplayFn, DisplayJoin}, - Adts, Constructors, Ctx, Definition, Name, NumCtr, Pattern, Rule, Term, Type, - }, -}; -use indexmap::IndexSet; -use itertools::Itertools; - -pub enum SimplifyMatchErr { - NotExhaustive(Vec), - TypeMismatch(TypeMismatchErr), - MalformedNumSucc(Pattern, Pattern), -} - -impl Ctx<'_> { - pub fn simplify_matches(&mut self) -> Result<(), Diagnostics> { - self.info.start_pass(); - let name_gen = &mut 0; - - for (def_name, def) in self.book.defs.iter_mut() { - let res = def.simplify_matches(&self.book.ctrs, &self.book.adts, name_gen); - self.info.take_rule_err(res, def_name.clone()); - } - - self.info.fatal(()) - } -} - -impl Definition { - pub fn simplify_matches( - &mut self, - ctrs: &Constructors, - adts: &Adts, - name_gen: &mut usize, - ) -> Result<(), SimplifyMatchErr> { - for rule in self.rules.iter_mut() { - rule.body.simplify_matches(ctrs, adts, name_gen)?; - } - Ok(()) - } -} - -impl Term { - /// Converts match expressions with multiple matched arguments and - /// arbitrary patterns into matches on a single value, with only - /// simple (non-nested) patterns, and one rule for each constructor. - /// - /// The `name_gen` is used to generate fresh variable names for - /// substitution to avoid name clashes. - /// - /// See `[simplify_match_expression]` for more information. - pub fn simplify_matches( - &mut self, - ctrs: &Constructors, - adts: &Adts, - name_gen: &mut usize, - ) -> Result<(), SimplifyMatchErr> { - Term::recursive_call(move || { - match self { - Term::Mat { args, rules } => { - let extracted = extract_args(args); - let args = std::mem::take(args); - let rules = std::mem::take(rules); - let term = simplify_match_expression(args, rules, ctrs, adts, name_gen)?; - *self = bind_extracted_args(extracted, term); - } - - _ => { - for child in self.children_mut() { - child.simplify_matches(ctrs, adts, name_gen)?; - } - } - } - Ok(()) - }) - } -} - -/// Given the values held by a match expression, separates a simple, non-nested -/// match out of the first argument of the given match. -/// -/// If there are constructors of different types, returns a type error. -/// -/// If no patterns match one of the constructors, returns a non-exhaustive match error. -/// -/// Invariant: All the match arg terms are variables. -/// -/// =========================================================================== -/// -/// For each constructor, a match case is created. It has only a single simple -/// pattern with the constructor and no subpatterns. -/// -/// The match cases follow the same order as the order the constructors are in -/// the ADT declaration. -/// -/// Any nested subpatterns are extracted and moved into a nested match -/// expression, together with the remaining match arguments. -/// -/// For Var matches, we skip creating the surrounding match term since it's -/// redundant. (would be simply match x {x: ...}) -fn simplify_match_expression( - args: Vec, - rules: Vec, - ctrs: &Constructors, - adts: &Adts, - name_gen: &mut usize, -) -> Result { - 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, name_gen) - } else if fst_col_type == Type::Any { - var_rule(args, rules, ctrs, adts, name_gen) - } else { - switch_rule(args, rules, fst_col_type, ctrs, adts, name_gen) - } -} - -/// Irrefutable row rule. -/// An optimization to not generate unnecessary pattern matching when we -/// know the first case always matches. -fn irrefutable_fst_row_rule( - args: Vec, - mut rules: Vec, - ctrs: &Constructors, - adts: &Adts, - name_gen: &mut usize, -) -> Result { - rules.truncate(1); - - let Rule { pats, body: mut term } = rules.pop().unwrap(); - term.simplify_matches(ctrs, adts, name_gen)?; - - for (pat, arg) in pats.iter().zip(args.iter()) { - for bind in pat.binds().flatten() { - term.subst(bind, arg); - } - } - - Ok(term) -} - -/// Var rule. -/// Could be merged with the ctr rule, but this is slightly simpler. -/// `match x0 ... xN { var p1 ... pN: (Body var p1 ... pN) }` -/// becomes -/// `match x1 ... xN { p1 ... pN: let var = x0; (Body var p1 ... pN) }` -fn var_rule( - mut args: Vec, - rules: Vec, - ctrs: &Constructors, - adts: &Adts, - name_gen: &mut usize, -) -> Result { - let mut new_rules = vec![]; - for mut rule in rules { - let rest = rule.pats.split_off(1); - - let pat = rule.pats.pop().unwrap(); - let mut body = rule.body; - if let Pattern::Var(Some(nam)) = &pat { - body.subst(nam, &args[0]); - } - - let new_rule = Rule { pats: rest, body }; - new_rules.push(new_rule); - } - - let rest = args.split_off(1); - let mut term = Term::Mat { args: rest, rules: new_rules }; - term.simplify_matches(ctrs, adts, name_gen)?; - Ok(term) -} - -/// When the first column has constructors, create a branch on the constructors -/// of the first match arg. -/// -/// Each created match case has another nested match -/// expression to deal with the extracted nested patterns and remaining args. -/// -/// ```hvm -/// match x0 ... xN { -/// (CtrA p0_0_0 ... p0_A) p0_1 ... p0_N : (Body0 p0_0_0 ... p0_0_A p0_1 ... p0_N) -/// ... -/// varI pI_1 ... pI_N: (BodyI varI pI_1 ... pI_N) -/// ... -/// (CtrB pJ_0_0 ... pJ_0_B) pJ_1 ... pJ_N: (BodyJ pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N) -/// ... -/// (CtrC) pK_1 ... pK_N: (BodyK p_1 ... pK_N) -/// ... -/// } -/// ``` -/// is converted into -/// ```hvm -/// match x0 { -/// (CtrA x0%ctrA_field0 ... x%ctrA_fieldA): match x%ctrA_field0 ... x%ctrA_fieldN x1 ... xN { -/// p0_0_0 ... p0_0_B p0_1 ... p0_N : -/// (Body0 p0_0_0 ... p0_0_B ) -/// x%ctrA_field0 ... x%ctrA_fieldA pI_1 ... pI_N: -/// let varI = (CtrA x%ctrA_field0 ... x%ctrA_fieldN); (BodyI varI pI_1 ... pI_N) -/// ... -/// } -/// (CtrB x%ctrB_field0 ... x%ctrB_fieldB): match x%ctrB_field0 ... x%ctrB_fieldB x1 ... xN { -/// x%ctrB_field0 ... x%ctrB_fieldB pI_1 ... pI_N: -/// let varI = (CtrB x%ctrB_field0 ... x%ctrB_fieldB); (BodyI varI pI_1 ... pI_N) -/// pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N : -/// (BodyJ pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N) -/// ... -/// } -/// (CtrC): match * x1 ... xN { -/// * pI_1 ... pI_N: -/// let varI = CtrC; (BodyI varI pI_1 ... pI_N) -/// * pK_1 ... pK_N: -/// (BodyK p_1 ... pK_N) -/// ... -/// } -/// ... -/// } -/// ``` -fn switch_rule( - mut args: Vec, - rules: Vec, - typ: Type, - ctrs: &Constructors, - adts: &Adts, - name_gen: &mut usize, -) -> 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(SimplifyMatchErr::NotExhaustive(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(SimplifyMatchErr::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, name_gen); - 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, name_gen)?; - let pats = vec![matched_ctr]; - new_rules.push(Rule { pats, body }); - } - args.truncate(1); - let term = Term::Mat { args, rules: new_rules }; - Ok(term) -} - -fn switch_rule_nested_fields(arg_nam: &Name, ctr: &Pattern, name_gen: &mut usize) -> Vec> { - let mut nested_fields = vec![]; - let old_vars = ctr.binds(); - for old_var in old_vars { - *name_gen += 1; - let new_nam = if let Some(field) = old_var { - // Name of constructor field - Name::new(format!("{arg_nam}%{field}%{name_gen}")) - } else { - // Name of var pattern - arg_nam.clone() - }; - nested_fields.push(Some(new_nam)); - } - if nested_fields.is_empty() { - // We say that a unit variant always has an unused wildcard nested - nested_fields.push(None); - } - nested_fields -} - -fn switch_rule_matched_ctr(mut ctr: Pattern, nested_fields: &[Option]) -> Pattern { - let mut nested_fields = nested_fields.iter().cloned(); - ctr.binds_mut().for_each(|var| *var = nested_fields.next().unwrap()); - ctr -} - -fn switch_rule_submatch( - args: &[Term], - rules: &[Rule], - ctr: &Pattern, - nested_fields: &[Option], -) -> Result { - // Create the nested match expression. - let new_args = nested_fields.iter().cloned().map(Term::var_or_era); - let old_args = args[1 ..].iter().cloned(); - let args = new_args.clone().chain(old_args).collect::>(); - - // Make the match cases of the nested submatch, filtering out the rules - // that don't match the current ctr. - let rules = - rules.iter().filter_map(|rule| switch_rule_submatch_arm(rule, ctr, nested_fields)).collect::>(); - - if rules.is_empty() { - // TODO: Return the full pattern - return Err(SimplifyMatchErr::NotExhaustive(vec![ctr.ctr_name().unwrap()])); - } - - let mat = Term::Mat { args, rules }; - Ok(mat) -} - -/// Make one of the cases of the nested submatch of a switch case. -/// Returns None if the rule doesn't match the constructor. -fn switch_rule_submatch_arm(rule: &Rule, ctr: &Pattern, nested_fields: &[Option]) -> Option { - if rule.pats[0].simple_equals(ctr) { - // Same ctr, extract the patterns. - // match x ... {(Ctr p0_0...) ...: Body; ...} - // becomes - // match x {(Ctr x%field0 ...): match x1 ... {p0_0 ...: Body; ...}; ...} - let mut pats = match &rule.pats[0] { - // Since the variable in the succ ctr is not a nested pattern, we need this special case. - 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 - pats.push(Pattern::Var(None)); - } - pats.extend(rule.pats[1 ..].iter().cloned()); - let body = rule.body.clone(); - Some(Rule { pats, body }) - } else if rule.pats[0].is_wildcard() { - // Use `subst` to replace the pattern variable in the body - // of the rule with the term that represents the matched constructor. - let mut body = rule.body.clone(); - if let Pattern::Var(Some(nam)) = &rule.pats[0] { - body.subst(nam, &ctr.to_term()); - } - - let nested_var_pats = nested_fields.iter().cloned().map(Pattern::Var); - let old_pats = rule.pats[1 ..].iter().cloned(); - let pats = nested_var_pats.chain(old_pats).collect_vec(); - - Some(Rule { pats, body }) - } else { - // Non-matching constructor. Don't include in submatch expression. - None - } -} - -/// Swaps non-Var arguments in a match by vars with generated names, -/// returning a vec with the extracted args and what they were replaced by. -/// -/// `match Term {...}` => `match %match_arg0 {...}` + `vec![(%match_arg0, Term)])` -fn extract_args(args: &mut [Term]) -> Vec<(Name, Term)> { - let mut extracted = vec![]; - - for (i, arg) in args.iter_mut().enumerate() { - if !matches!(arg, Term::Var { .. }) { - let nam = Name::new(format!("%match_arg{i}")); - let new_arg = Term::Var { nam: nam.clone() }; - let old_arg = std::mem::replace(arg, new_arg); - extracted.push((nam, old_arg)); - } - } - extracted -} - -/// Binds the arguments that were extracted from a match with [`extract_args`]; -/// -/// `vec![(%match_arg0, arg)]` + `term` => `let %match_arg0 = arg; term` -fn bind_extracted_args(extracted: Vec<(Name, Term)>, term: Term) -> Term { - extracted.into_iter().rfold(term, |term, (nam, val)| Term::Let { - pat: Pattern::Var(Some(nam)), - val: Box::new(val), - nxt: Box::new(term), - }) -} - -const PATTERN_ERROR_LIMIT: usize = 5; -const ERROR_LIMIT_HINT: &str = "Use the --verbose option to see all cases."; - -impl SimplifyMatchErr { - pub fn display(&self, verbose: bool) -> impl std::fmt::Display + '_ { - let limit = if verbose { usize::MAX } else { PATTERN_ERROR_LIMIT }; - DisplayFn(move |f| match self { - SimplifyMatchErr::NotExhaustive(cases) => { - let ident = ERR_INDENT_SIZE * 2; - let hints = DisplayJoin( - || { - cases - .iter() - .take(limit) - .map(|pat| DisplayFn(move |f| write!(f, "{:ident$}Case '{pat}' not covered.", ""))) - }, - "\n", - ); - write!(f, "Non-exhaustive pattern matching. Hint:\n{}", hints)?; - - let len = cases.len(); - if len > limit { - write!(f, " ... and {} others.\n{:ident$}{}", len - limit, "", ERROR_LIMIT_HINT)?; - } - - Ok(()) - } - SimplifyMatchErr::TypeMismatch(err) => { - write!(f, "{}", err.to_string_verbose(verbose)) - } - SimplifyMatchErr::MalformedNumSucc(got, exp) => { - write!(f, "Expected a sequence of incrementing numbers ending with '{exp}', found '{got}'.") - } - }) - } -} - -impl ToStringVerbose for SimplifyMatchErr { - fn to_string_verbose(&self, verbose: bool) -> String { - format!("{}", self.display(verbose)) - } -} - -impl From for SimplifyMatchErr { - fn from(value: TypeMismatchErr) -> Self { - SimplifyMatchErr::TypeMismatch(value) - } -} diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs index df4ea2ca..f3164513 100644 --- a/tests/golden_tests.rs +++ b/tests/golden_tests.rs @@ -92,6 +92,14 @@ fn run_golden_test_dir_multiple(test_name: &str, run: &[&RunFn]) { } } +/* Snapshot/regression/golden tests + + Each tests runs all the files in tests/golden_tests/. + + The test functions decide how exactly to process the test programs + and what to save as a snapshot. +*/ + #[test] fn compile_term() { run_golden_test_dir(function_name!(), &|code, _| { @@ -147,6 +155,7 @@ fn linear_readback() { Ok(format!("{}{}", info.diagnostics, res)) }); } + #[test] fn run_file() { run_golden_test_dir_multiple(function_name!(), &[ @@ -206,25 +215,22 @@ fn simplify_matches() { let diagnostics_cfg = DiagnosticsConfig::new(Severity::Error, true); let mut book = do_parse_book(code, path)?; let mut ctx = Ctx::new(&mut book, diagnostics_cfg); + ctx.check_shared_names(); ctx.set_entrypoint(); ctx.book.encode_adts(AdtEncoding::TaggedScott); - ctx.book.encode_builtins(); ctx.book.resolve_ctrs_in_pats(); - ctx.resolve_refs()?; - ctx.check_match_arity()?; - ctx.check_unbound_pats()?; - ctx.book.convert_match_def_to_term(); - ctx.book.desugar_let_destructors(); - ctx.book.desugar_implicit_match_binds(); + ctx.check_unbound_ctr()?; ctx.check_ctrs_arities()?; + ctx.book.encode_builtins(); + ctx.resolve_refs()?; + ctx.fix_match_terms()?; + ctx.desugar_match_defs()?; ctx.check_unbound_vars()?; - ctx.simplify_matches()?; - ctx.book.linearize_simple_matches(true); + ctx.book.linearize_matches(true); ctx.check_unbound_vars()?; - ctx.book.make_var_names_unique(); - ctx.book.linearize_vars(); ctx.prune(false, AdtEncoding::TaggedScott); + Ok(ctx.book.to_string()) }) } @@ -242,25 +248,22 @@ fn encode_pattern_match() { run_golden_test_dir(function_name!(), &|code, path| { let mut result = String::new(); for adt_encoding in [AdtEncoding::TaggedScott, AdtEncoding::Scott] { - let diagnostics_cfg = DiagnosticsConfig::new(Severity::Error, true); + let diagnostics_cfg = DiagnosticsConfig::new(Severity::Warning, true); let mut book = do_parse_book(code, path)?; let mut ctx = Ctx::new(&mut book, diagnostics_cfg); ctx.check_shared_names(); ctx.set_entrypoint(); ctx.book.encode_adts(adt_encoding); - ctx.book.encode_builtins(); ctx.book.resolve_ctrs_in_pats(); - ctx.resolve_refs()?; - ctx.check_match_arity()?; - ctx.check_unbound_pats()?; - ctx.book.convert_match_def_to_term(); - ctx.book.desugar_let_destructors(); - ctx.book.desugar_implicit_match_binds(); + ctx.check_unbound_ctr()?; ctx.check_ctrs_arities()?; + ctx.book.encode_builtins(); + ctx.resolve_refs()?; + ctx.fix_match_terms()?; + ctx.desugar_match_defs()?; ctx.check_unbound_vars()?; - ctx.simplify_matches()?; - ctx.book.linearize_simple_matches(true); - ctx.book.encode_simple_matches(adt_encoding); + ctx.book.linearize_matches(true); + ctx.book.encode_matches(adt_encoding); ctx.check_unbound_vars()?; ctx.book.make_var_names_unique(); ctx.book.linearize_vars(); diff --git a/tests/golden_tests/cli/debug_u60_to_nat.hvm b/tests/golden_tests/cli/debug_u60_to_nat.hvm index 3bd4686e..fa3e1c04 100644 --- a/tests/golden_tests/cli/debug_u60_to_nat.hvm +++ b/tests/golden_tests/cli/debug_u60_to_nat.hvm @@ -1,6 +1,8 @@ data Nat_ = (Z) | (S nat) -(U60ToNat 0) = Z -(U60ToNat 1+p) = (S (U60ToNat p)) +U60ToNat n = switch n { + 0: Z + _: (S (U60ToNat n-1)) +} (Main n) = (U60ToNat n) diff --git a/tests/golden_tests/cli/desugar_linearize_matches.hvm b/tests/golden_tests/cli/desugar_linearize_matches.hvm index 3980330a..20ba4325 100644 --- a/tests/golden_tests/cli/desugar_linearize_matches.hvm +++ b/tests/golden_tests/cli/desugar_linearize_matches.hvm @@ -1 +1 @@ -main = λa λb match a { 0: b; 1+: b } +main = λa λb switch a { 0: b; _: b } diff --git a/tests/golden_tests/cli/desugar_linearize_matches_extra.hvm b/tests/golden_tests/cli/desugar_linearize_matches_extra.hvm index 64a20adb..6a9334aa 100644 --- a/tests/golden_tests/cli/desugar_linearize_matches_extra.hvm +++ b/tests/golden_tests/cli/desugar_linearize_matches_extra.hvm @@ -1 +1 @@ -main = λa λb λc match a { 0: b; 1+: c } +main = λa λb λc switch a { 0: b; _: c } diff --git a/tests/golden_tests/compile_file/implicit_match_in_match_arg.hvm b/tests/golden_tests/compile_file/implicit_match_in_match_arg.hvm deleted file mode 100644 index 64175374..00000000 --- a/tests/golden_tests/compile_file/implicit_match_in_match_arg.hvm +++ /dev/null @@ -1,4 +0,0 @@ -main x = match (match x {0: 0; 1+: x-1}) { - 0: 0 - 1+x-2: x-2 -} \ No newline at end of file diff --git a/tests/golden_tests/compile_file/match_num_all_patterns.hvm b/tests/golden_tests/compile_file/match_num_all_patterns.hvm deleted file mode 100644 index ad033339..00000000 --- a/tests/golden_tests/compile_file/match_num_all_patterns.hvm +++ /dev/null @@ -1,60 +0,0 @@ -zero_succ = @x match x { - 0: 0 - 1+: x-1 -} -succ_zero = @x match x { - 1+: x-1 - 0: 0 -} - -var_zero = @x match x { - var: var - 0: 0 -} - -var_succ = @x match x { - var: var - 1+: x-1 -} - -zero_var = @x match x { - 0: 0 - var: (- var 1) -} - -succ_var = @x match x { - 1+: x-1 - var: 0 -} - -zero_var_succ = @x match x { - 0: 0 - var: (- var 1) - 1+: x-1 -} - -succ_var_zero = @x match x { - 1+: (+ x-1 2) - var: (+ var 1) - 0: 1 -} - -zero_succ_var = @x match x { - 0: 0 - 1+: x-1 - var: (- var 1) -} - -succ_zero_var = @x match x { - 1+: x-1 - 0: 0 - var: (- var 1) -} - -succ_zero_succ = @x match x { - 1+: x-1 - 0: 0 - 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 deleted file mode 100644 index fe3be08e..00000000 --- a/tests/golden_tests/compile_file/match_num_unscoped_lambda.hvm +++ /dev/null @@ -1,11 +0,0 @@ -lambda_out = @x @$y match x { - 0: $y - 1+: x-1 -} - -lambda_in = @x (match x { - 0: @x x - 1+: @$y x-1 -} $y) - -main = * \ No newline at end of file diff --git a/tests/golden_tests/compile_file/repeated_bind_match.hvm b/tests/golden_tests/compile_file/repeated_bind_match.hvm deleted file mode 100644 index e6e0cb51..00000000 --- a/tests/golden_tests/compile_file/repeated_bind_match.hvm +++ /dev/null @@ -1,4 +0,0 @@ -main = @a match a { - (List.cons x x): x - (List.nil) : * -} diff --git a/tests/golden_tests/compile_file/switch_all_patterns.hvm b/tests/golden_tests/compile_file/switch_all_patterns.hvm new file mode 100644 index 00000000..3b1e0bb9 --- /dev/null +++ b/tests/golden_tests/compile_file/switch_all_patterns.hvm @@ -0,0 +1,43 @@ +zero_succ = @x switch x { + 0: 0 + _: x-1 +} + +succ_zero = @x switch x { + _: x-1 + 0: 0 +} + +zero = @x switch x { + 0: 0 +} + +succ = @x switch x { + _: x-1 +} + +succ_zero_succ = @x switch x { + _: x-1 + 0: 0 + _: (+ x-1 1) +} + +zero_succ_zero = @x switch x { + 0: 0 + _: x-1 + 0: 1 +} + +zero_zero_succ = @x switch x { + 0: 0 + 0: 1 + _: x-1 +} + +zero_succ_succ = @x switch x { + 0: 0 + _: x-1 + _: (+ x-1 1) +} + +main = 0 \ No newline at end of file diff --git a/tests/golden_tests/compile_file/switch_in_switch_arg.hvm b/tests/golden_tests/compile_file/switch_in_switch_arg.hvm new file mode 100644 index 00000000..2e0cc52b --- /dev/null +++ b/tests/golden_tests/compile_file/switch_in_switch_arg.hvm @@ -0,0 +1,4 @@ +main x = switch (switch x {0: 0; _: x-1}) { + 0: 0 + _: x +} \ No newline at end of file diff --git a/tests/golden_tests/compile_file/switch_unscoped_lambda.hvm b/tests/golden_tests/compile_file/switch_unscoped_lambda.hvm new file mode 100644 index 00000000..10087ae1 --- /dev/null +++ b/tests/golden_tests/compile_file/switch_unscoped_lambda.hvm @@ -0,0 +1,11 @@ +lambda_out = @x @$y switch x { + 0: $y + _: x-1 +} + +lambda_in = @x (switch x { + 0: @x x + _: @$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 7f368aa9..27b0e940 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; 1+: (valS n-1) }) +val = λn (switch n { 0: valZ; _: (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/let_adt_destructuring.hvm b/tests/golden_tests/compile_file_o_all/let_adt_destructuring.hvm deleted file mode 100644 index 25c9c8ae..00000000 --- a/tests/golden_tests/compile_file_o_all/let_adt_destructuring.hvm +++ /dev/null @@ -1,7 +0,0 @@ -data Boxed = (Box val) - -// Both rules should have the same compiled net structure -// (Unbox (Box val)) = val -(Unbox x) = let (Box val) = x; val - -main = (Unbox (Box 1)) \ No newline at end of file diff --git a/tests/golden_tests/compile_file_o_all/let_adt_non_exhaustive.hvm b/tests/golden_tests/compile_file_o_all/let_adt_non_exhaustive.hvm deleted file mode 100644 index 20b645c6..00000000 --- a/tests/golden_tests/compile_file_o_all/let_adt_non_exhaustive.hvm +++ /dev/null @@ -1,6 +0,0 @@ -data Maybe = (Some val) | None - -main = - let maybe = (Some 1) - let (Some value) = maybe - value \ 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 e950ba58..5d001346 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 { +main = @a @b let c = (+ a a); switch a { 0: b; - 1+: (+ a-1 b); + _: (+ a-1 b); } diff --git a/tests/golden_tests/compile_file_o_all/match_adt_non_exhaustive.hvm b/tests/golden_tests/compile_file_o_all/match_adt_non_exhaustive.hvm index b0548cbd..877ea8fc 100644 --- a/tests/golden_tests/compile_file_o_all/match_adt_non_exhaustive.hvm +++ b/tests/golden_tests/compile_file_o_all/match_adt_non_exhaustive.hvm @@ -2,6 +2,8 @@ data Maybe = (Some val) | None main = @maybe match maybe { - (None): 0 - (Some (None)): 0 + None: 0 + Some: match maybe.val { + None: 0 + } } \ No newline at end of file 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 f2d8723f..189e5ba2 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 { +main = @a @b @c @d switch a { 0: (+ (+ b c) d); - 1+: (+ (+ (+ a-1 b) c) d); + _: (+ (+ (+ 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 4b167c1b..4b6b8685 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 { +pred = @n switch n { 0: 0 - 1+: n-1 + _: n-1 } main = (pred 4) \ No newline at end of file diff --git a/tests/golden_tests/compile_file_o_all/nested_adt_match.hvm b/tests/golden_tests/compile_file_o_all/nested_adt_match.hvm deleted file mode 100644 index f032fc37..00000000 --- a/tests/golden_tests/compile_file_o_all/nested_adt_match.hvm +++ /dev/null @@ -1,8 +0,0 @@ -data Maybe = (Some val) | None - -main = - match (Some (Some 1)) { - (None): 0 - (Some (None)): 0 - (Some (Some v)): v - } \ 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 e01d13e8..8af4329e 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 1+n) = n +(Foo true 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 f4adf83d..726d159b 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}; 1+p: @* p } +Foo = @a switch a { 0: {Foo Foo}; _: @* a-1 } 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 30b30164..a767df68 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 { +sum_pred = @a @b switch a { + 0: switch b { 0: 0 - 1+: b-1 + _: b-1 }; - 1+: match b { + _: switch b { 0: a-1 - 1+: (+ a-1 b-1) + _: (+ a-1 b-1) } } diff --git a/tests/golden_tests/compile_term/match.hvm b/tests/golden_tests/compile_term/match.hvm index 65340556..738e3736 100644 --- a/tests/golden_tests/compile_term/match.hvm +++ b/tests/golden_tests/compile_term/match.hvm @@ -1,4 +1,4 @@ -match (+ 0 1) { +switch (+ 0 1) { 0: λt λf t - 1+: λ* λt λf f // The term to hvmc function assumes the pred variable is already detached from the match + _: λ* λ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/desugar_file/combinators.hvm b/tests/golden_tests/desugar_file/combinators.hvm index bbbc458d..fb56fcdb 100644 --- a/tests/golden_tests/desugar_file/combinators.hvm +++ b/tests/golden_tests/desugar_file/combinators.hvm @@ -4,8 +4,8 @@ (List.ignore list ignore) = match list { - (List.cons): (List.ignore list.tail (List.ignore)) - (List.nil): 0 + List.cons: (List.ignore list.tail (List.ignore)) + List.nil: 0 } (baz) = {0 1 2 3 λa a foo} diff --git a/tests/golden_tests/encode_pattern_match/concat.hvm b/tests/golden_tests/encode_pattern_match/concat.hvm index 84318028..f83473e7 100644 --- a/tests/golden_tests/encode_pattern_match/concat.hvm +++ b/tests/golden_tests/encode_pattern_match/concat.hvm @@ -1,7 +1,7 @@ String.concat = @a @b match a { String.nil: b; - (String.cons hd tl): (String.cons hd (String.concat tl b)) + String.cons: (String.cons a.head (String.concat a.tail b)) } main = (String.concat "ab" "cd") \ 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 c87283a5..400a663e 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 (1+a,*) *) = a +(Fn3 (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/list_str_encoding_undeclared_map.hvm b/tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared_map.hvm index 2b479136..c57f66fb 100644 --- a/tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared_map.hvm +++ b/tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared_map.hvm @@ -4,7 +4,7 @@ main = @a @b String.nil : 2 }; let b = match b { - (List.cons h t): 1 - (List.nil) : 2 + List.cons: 1 + List.nil : 2 }; (a, b) \ No newline at end of file diff --git a/tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hvm b/tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hvm index a4afdb29..c0ffcbef 100644 --- a/tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hvm +++ b/tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hvm @@ -1,6 +1,6 @@ data Maybe = None | (Some val) -main = (match (Some 1) { +main = (match x = (Some 1) { None: @$x * - (Some x): x + Some: x.val } $x) \ No newline at end of file diff --git a/tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm b/tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm index 78f2efc9..4d34fe2c 100644 --- a/tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm +++ b/tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm @@ -1,13 +1,13 @@ data Maybe = None | (Some val) -Foo = @$x match (Some 1) { +Foo = @$x match x = (Some 1) { None: $x - (Some x): x + Some: x.val } -Bar = (match (Some 1) { +Bar = (match x = (Some 1) { None: $x - (Some x): x + Some: x.val } @$x *) main = * \ 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 15e0621a..70e8c3d8 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) { + switch num = (+ 2 3) { | 0: 653323 - | 1+: (+ num num-1) + | _: (+ num num-1) } main = cheese \ No newline at end of file diff --git a/tests/golden_tests/encode_pattern_match/match_many_args.hvm b/tests/golden_tests/encode_pattern_match/match_many_args.hvm deleted file mode 100644 index 0b939d4b..00000000 --- a/tests/golden_tests/encode_pattern_match/match_many_args.hvm +++ /dev/null @@ -1,40 +0,0 @@ -data L = (C h t) | N -data Option = (Some val) | None - -tail_tail = @xs match xs { - (C * (C * t)): t - *: N -} - -or = @dflt @opt match dflt opt { - * (Some val): val - dflt *: dflt -} - -or2 = @opt @dflt match opt dflt { - (Some val) *: val - * dflt: dflt -} - -map = @f @opt match f opt { - f (Some val): (f val) - * None: None -} - -map2 = @f @opt match f opt { - f (Some val): (f val) - * val: val -} - -flatten = @opt match opt { - (Some (Some val)): (Some val) - *: None -} - -map_pair = @f @xs @ys match f xs ys { - * N *: N - * * N: N - f (C x xs) (C y ys): (C (f x y) (map_pair xs ys)) -} - -main = * \ 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 index 6ec488ed..70a7172a 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 @@ -9,7 +9,7 @@ Parse state xs = (Err (xs, state)) main = let str = "(+"; let state = *; - match (Parse state str) { - (Ok (val, xs, state)): (val, (Parse state xs)) + match res = (Parse state str) { + Ok: let (val, xs, state) = res.val; (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 index 008014b7..018b560f 100644 --- a/tests/golden_tests/encode_pattern_match/match_num_pred.hvm +++ b/tests/golden_tests/encode_pattern_match/match_num_pred.hvm @@ -1,18 +1,21 @@ -pred 0 = 0 -pred 1+x = x +pred = @n switch n { + 0: 0 + _: n-1 +} -pred2 2+x = x -pred2 * = 0 +pred2 n = switch n { + 0: 0 + 1: 0 + _: n-2 +} pred3 0 = 0 pred3 1 = 0 pred3 2 = 0 -pred3 3+x-3 = x-3 +pred3 x = (- x 3) -pred4 0 = 0 -pred4 1 = 0 -pred4 2 = 0 -pred4 3 = 0 -pred4 n = (- n 4) +zero 0 = 1 +zero 1 = 0 +zero * = 0 main = * \ No newline at end of file diff --git a/tests/golden_tests/encode_pattern_match/nested_let_tup.hvm b/tests/golden_tests/encode_pattern_match/nested_let_tup.hvm deleted file mode 100644 index 585abd33..00000000 --- a/tests/golden_tests/encode_pattern_match/nested_let_tup.hvm +++ /dev/null @@ -1,6 +0,0 @@ -main = - let (a, (b, c)) = - let (i, (j, k)) = (10, ((1, ((2, 3), 4)), 3)); - j; - let (x, y) = b; - x \ 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 c128f459..ee95d882 100644 --- a/tests/golden_tests/run_file/bitonic_sort.hvm +++ b/tests/golden_tests/run_file/bitonic_sort.hvm @@ -2,9 +2,9 @@ data Tree = (Leaf a) | (Both a b) data Error = Err // Atomic Swapper -(Swap n a b) = match n { +(Swap n a b) = switch n { 0: (Both a b) - 1+: (Both b a) + _: (Both b a) } // Swaps distant values in parallel; corresponds to a Red Box @@ -29,9 +29,9 @@ data Error = Err (Sort s (Both a b)) = (Flow s (Both (Sort 0 a) (Sort 1 b))) // Generates a tree of depth `n` -(Gen n x) = match n { +(Gen n x) = switch n { 0: (Leaf x) - 1+: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 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 8cf31606..1d5ddb5b 100644 --- a/tests/golden_tests/run_file/bitonic_sort_lam.hvm +++ b/tests/golden_tests/run_file/bitonic_sort_lam.hvm @@ -2,9 +2,9 @@ Leaf = λx #Tree λl #Tree λn (l x) Node = λx0 λx1 #Tree λl #Tree λn (n x0 x1) -swap = λn match n { +swap = λn switch n { 0: λx0 λx1 (Node x0 x1) - 1+: λx0 λx1 (Node x1 x0) + _: λx0 λx1 (Node x1 x0) } warp = λa @@ -41,9 +41,9 @@ sort = λa let a_node = λa0 λa1 λs (flow (Node (sort a0 0) (sort a1 1)) s) #Tree (a a_leaf a_node) -gen = λn match n { +gen = λn switch n { 0: λx (Leaf x) - 1+: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 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 e7740bff..628f80dd 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 1+* to = to +Box.subst.go a * 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 deleted file mode 100644 index bbfa4138..00000000 --- a/tests/golden_tests/run_file/box2.hvm +++ /dev/null @@ -1,7 +0,0 @@ -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 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 3573534a..134eaa7f 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 1+* = 0 +go true 0 = 1 +go false _ = 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 ca7fe5a4..3bbaa0cb 100644 --- a/tests/golden_tests/run_file/example.hvm +++ b/tests/golden_tests/run_file/example.hvm @@ -20,9 +20,9 @@ // You can use numbers on the native match expression // The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1 (Num.pred) = λn - match n { + switch n { 0: 0 - 1+: n-1 + _: n-1 } // Write new data types like this @@ -51,9 +51,9 @@ data Boxed = (Box val) // Types with only one constructor can be destructured using `let` or a single matching definition (Box.map (Box val) f) = (Box (f val)) -(Box.unbox) = λbox - let (Box val) = box - val +(Box.unbox) = λbox match box { + Box: box.val +} // Use tuples to store two values together without needing to create a new data type (Tuple.new fst snd) = @@ -68,9 +68,9 @@ data Boxed = (Box val) snd // All files must have a main definition to be run. -// You can execute a program in HVM with "cargo run -- --run " -// Other options are "--check" (the default mode) to just see if the file is well formed -// and "--compile" to output hvm-core code. +// You can execute a program in HVM with "cargo run -- run " +// Other options are "check" (the default mode) to just see if the file is well formed +// and "compile" to output hvm-core code. (main) = let tup = (Tuple.new None (Num.pred 5)) diff --git a/tests/golden_tests/run_file/extracted_match_pred.hvm b/tests/golden_tests/run_file/extracted_match_pred.hvm index 7de90538..26ed5f13 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; 1+: (valS n-1) }) +val = λn (switch n { 0: valZ; _: (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 e950ba58..5d001346 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 { +main = @a @b let c = (+ a a); switch a { 0: b; - 1+: (+ a-1 b); + _: (+ a-1 b); } diff --git a/tests/golden_tests/run_file/list_take.hvm b/tests/golden_tests/run_file/list_take.hvm index 68a1c8b4..8befd00b 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) { + switch (== 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 7a3e7e4b..fb248552 100644 --- a/tests/golden_tests/run_file/list_to_tree.hvm +++ b/tests/golden_tests/run_file/list_to_tree.hvm @@ -3,17 +3,17 @@ List.len.go [] count = count List.len.go (List.cons x xs) count = (List.len.go xs (+ count 1)) Take.go n list = - match (== n 0) { + switch (== n 0) { | 0: (Take n list) - | 1+: [] + | _: [] } Take n [] = [] Take n (List.cons x xs) = (List.cons x (Take.go (- n 1) xs)) Drop.go n list = - match (== n 0) { + switch (== n 0) { | 0: (Drop n list) - | 1+: list + | _: 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 a0e97264..a4e1e130 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) { + switch (+ 0 1) { 0: λt λf t - 1+: λt λf f + _: λ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 f2d8723f..189e5ba2 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 { +main = @a @b @c @d switch a { 0: (+ (+ b c) d); - 1+: (+ (+ (+ a-1 b) c) d); + _: (+ (+ (+ 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 index 6ec488ed..70a7172a 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 @@ -9,7 +9,7 @@ Parse state xs = (Err (xs, state)) main = let str = "(+"; let state = *; - match (Parse state str) { - (Ok (val, xs, state)): (val, (Parse state xs)) + match res = (Parse state str) { + Ok: let (val, xs, state) = res.val; (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 4b167c1b..4b6b8685 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 { +pred = @n switch n { 0: 0 - 1+: n-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 index acbeef56..da2a2c39 100644 --- a/tests/golden_tests/run_file/match_num_num_to_char.hvm +++ b/tests/golden_tests/run_file/match_num_num_to_char.hvm @@ -1,4 +1,4 @@ -num_to_char n = match n { +num_to_char n = switch n { 0: '0' 1: '1' 2: '2' @@ -9,22 +9,20 @@ num_to_char n = match n { 7: '7' 8: '8' 9: '9' - 10+: '\0' + _: '\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) -} +char_to_num '9' = 9 +char_to_num '8' = 8 +char_to_num '7' = 7 +char_to_num '6' = 6 +char_to_num '5' = 5 +char_to_num '4' = 4 +char_to_num '3' = 3 +char_to_num '2' = 2 +char_to_num '1' = 1 +char_to_num '0' = 0 +char_to_num _ = (- 0 1) map f List.nil = List.nil map f (List.cons x xs) = (List.cons (f x) (map f xs)) diff --git a/tests/golden_tests/run_file/match_num_succ_complex.hvm b/tests/golden_tests/run_file/match_num_succ_complex.hvm index 9fd73097..a29072d2 100644 --- a/tests/golden_tests/run_file/match_num_succ_complex.hvm +++ b/tests/golden_tests/run_file/match_num_succ_complex.hvm @@ -1,16 +1,16 @@ -min1 * 0 = 0 -min1 0 * = 0 -min1 1+a 1+b = (+ 1 (min1 a b)) +min1 * 0 = 0 +min1 0 * = 0 +min1 a b = (+ 1 (min1 (- a 1) (- b 1))) -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 +min2 a b = switch a { + 0: 0 + _: switch b { + 0: 0 + _: (+ 1 (min2 a-1 b-1)) + } +} 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 000d2856..dce3c1ae 100644 --- a/tests/golden_tests/run_file/match_sup.hvm +++ b/tests/golden_tests/run_file/match_sup.hvm @@ -1,4 +1,6 @@ -main = let k = #a{0 1}; match k { +main = + let k = #a{0 1}; + switch k { 0: 1 - 1+p: (+ p 2) -} \ No newline at end of file + _: (+ k-1 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 cf62c944..0288b329 100644 --- a/tests/golden_tests/run_file/merge_sort.hvm +++ b/tests/golden_tests/run_file/merge_sort.hvm @@ -7,9 +7,9 @@ sort (Node a b) = (merge (sort a) (sort b)) merge (Nil) b = b merge (Cons x xs) (Nil) = (Cons x xs) merge (Cons x xs) (Cons y ys) = - let t = match (< x y) { + let t = switch (< x y) { 0: λaλbλcλt(t c a b) - 1+: λaλbλcλt(t a b c) + _: λaλbλcλt(t a b c) } let t = (t (Cons x) λx(x) (Cons y)) @@ -19,9 +19,9 @@ merge (Cons x xs) (Cons y ys) = sum Nil = 0 sum (Cons h t) = (+ h (sum t)) -range n = match n { +range n = switch n { 0: λx (Leaf x) - 1+: λx (Node (range n-1 (+ (* x 2) 1)) (range n-1 (* x 2))) + _: λ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 16e20f19..5e21e3e0 100644 --- a/tests/golden_tests/run_file/names_hyphen.hvm +++ b/tests/golden_tests/run_file/names_hyphen.hvm @@ -3,9 +3,9 @@ id cool-var-name = cool-var-name data Done_ = (Done done-var) toZero n = - match n { + switch n { 0: (Done 1) - 1+: (toZero n-1) + _: (toZero n-1) } main = diff --git a/tests/golden_tests/run_file/nested_let_tup.hvm b/tests/golden_tests/run_file/nested_let_tup.hvm deleted file mode 100644 index 775a06eb..00000000 --- a/tests/golden_tests/run_file/nested_let_tup.hvm +++ /dev/null @@ -1,6 +0,0 @@ -main = - let (a, (b, c)) = - let (i, (j, k)) = (10, ((1, ((2, 3), 4)), 3)); - j; - let (x, y) = b; - x diff --git a/tests/golden_tests/run_file/num_match_missing_var.hvm b/tests/golden_tests/run_file/num_match_missing_var.hvm index 07847485..22ef01e2 100644 --- a/tests/golden_tests/run_file/num_match_missing_var.hvm +++ b/tests/golden_tests/run_file/num_match_missing_var.hvm @@ -1,21 +1,15 @@ if 0 t f = f if 1 t f = t -if2 n t f = match n { +if2 n t f = switch n { 0: f - 1+: t - n: f + _: t + _: f } -if3 n t f = match n { +if3 n t f = switch n { 0: f - *: t - 1+: t -} - -if4 n t f = match n { - 0: f - 1+: t + _: t 1: t } diff --git a/tests/golden_tests/run_file/num_pred.hvm b/tests/golden_tests/run_file/num_pred.hvm index bea29e05..4d91708c 100644 --- a/tests/golden_tests/run_file/num_pred.hvm +++ b/tests/golden_tests/run_file/num_pred.hvm @@ -1,4 +1,6 @@ -Pred 0 = 0 -Pred 1+pred = pred +Pred n = switch n { + 0: 0 + _: n-1 +} 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 809517b7..0bfe1583 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 { +Pred = λt switch t { 0: 0 - 1+: t-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 acd51dec..8052e3dd 100644 --- a/tests/golden_tests/run_file/radix_sort_ctr.hvm +++ b/tests/golden_tests/run_file/radix_sort_ctr.hvm @@ -1,9 +1,9 @@ data Map = Free | Used | (Both a b) data Arr = Null | (Leaf x) | (Node a b) -(Swap s a b) = match s { +(Swap s a b) = switch s { 0: (Both a b) - 1+: (Both b a) + _: (Both b a) } // Sort : Arr -> Arr @@ -74,9 +74,9 @@ data Arr = Null | (Leaf x) | (Node a b) // Gen : U60 -> Arr (Gen n) = (Gen.go n 0) - (Gen.go n x) = match n { + (Gen.go n x) = switch 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 131cca0a..b70dcf51 100644 --- a/tests/golden_tests/run_file/recursive_combinator_nested.hvm +++ b/tests/golden_tests/run_file/recursive_combinator_nested.hvm @@ -1,4 +1,7 @@ // 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); 1+p: p } +Foo = @a switch a { + 0: (#a {Foo @* a} 9); + _: a-1 +} 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 a3223cb6..8113eddc 100644 --- a/tests/golden_tests/run_file/recursive_match_native.hvm +++ b/tests/golden_tests/run_file/recursive_match_native.hvm @@ -1,8 +1,8 @@ add = λa λb (+ a b) -sum = λn match n { +sum = λn switch n { 0: 1 - 1+: (add (sum n-1) (sum n-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 268a479d..8b3a324f 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 1+x (head, tail)) = ((+ 1 head), (StrGo x tail)) +(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) 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 22279b4d..31b4fb58 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 1+x (head, tail)) = ((+ 1 head), (StrGo x tail)) +(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) 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 5feee56e..112e6dc9 100644 --- a/tests/golden_tests/run_file/sum_tree.hvm +++ b/tests/golden_tests/run_file/sum_tree.hvm @@ -2,9 +2,9 @@ data Tree = (Leaf x) | (Node x0 x1) add = λa λb (+ a b) -gen = λn match n { +gen = λn switch n { 0: (Leaf 1) - 1+: (Node (gen n-1) (gen n-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 c8d83c62..5db50747 100644 --- a/tests/golden_tests/run_file/tuple_rots.hvm +++ b/tests/golden_tests/run_file/tuple_rots.hvm @@ -2,9 +2,9 @@ MkTup8 = @a @b @c @d @e @f @g @h @MkTup8 (MkTup8 a b c d e f g h) rot = λx (x λa λb λc λd λe λf λg λh (MkTup8 b c d e f g h a)) -app = λn match n { +app = λn switch n { 0: λf λx x - 1+: λf λx (app n-1 f (f x)) + _: λ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 c128f459..ee95d882 100644 --- a/tests/golden_tests/run_lazy/bitonic_sort.hvm +++ b/tests/golden_tests/run_lazy/bitonic_sort.hvm @@ -2,9 +2,9 @@ data Tree = (Leaf a) | (Both a b) data Error = Err // Atomic Swapper -(Swap n a b) = match n { +(Swap n a b) = switch n { 0: (Both a b) - 1+: (Both b a) + _: (Both b a) } // Swaps distant values in parallel; corresponds to a Red Box @@ -29,9 +29,9 @@ data Error = Err (Sort s (Both a b)) = (Flow s (Both (Sort 0 a) (Sort 1 b))) // Generates a tree of depth `n` -(Gen n x) = match n { +(Gen n x) = switch n { 0: (Leaf x) - 1+: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 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 8cf31606..1d5ddb5b 100644 --- a/tests/golden_tests/run_lazy/bitonic_sort_lam.hvm +++ b/tests/golden_tests/run_lazy/bitonic_sort_lam.hvm @@ -2,9 +2,9 @@ Leaf = λx #Tree λl #Tree λn (l x) Node = λx0 λx1 #Tree λl #Tree λn (n x0 x1) -swap = λn match n { +swap = λn switch n { 0: λx0 λx1 (Node x0 x1) - 1+: λx0 λx1 (Node x1 x0) + _: λx0 λx1 (Node x1 x0) } warp = λa @@ -41,9 +41,9 @@ sort = λa let a_node = λa0 λa1 λs (flow (Node (sort a0 0) (sort a1 1)) s) #Tree (a a_leaf a_node) -gen = λn match n { +gen = λn switch n { 0: λx (Leaf x) - 1+: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 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 e7740bff..628f80dd 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 1+* to = to +Box.subst.go a * 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 bbfa4138..e35f18c4 100644 --- a/tests/golden_tests/run_lazy/box2.hvm +++ b/tests/golden_tests/run_lazy/box2.hvm @@ -1,7 +1,7 @@ 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 1+* to = to +Box.subst.go a 0 to = (Box a) +Box.subst.go a * 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 ca7fe5a4..bf67976a 100644 --- a/tests/golden_tests/run_lazy/example.hvm +++ b/tests/golden_tests/run_lazy/example.hvm @@ -20,9 +20,9 @@ // You can use numbers on the native match expression // The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1 (Num.pred) = λn - match n { + switch n { 0: 0 - 1+: n-1 + _: n-1 } // Write new data types like this @@ -51,9 +51,9 @@ data Boxed = (Box val) // Types with only one constructor can be destructured using `let` or a single matching definition (Box.map (Box val) f) = (Box (f val)) -(Box.unbox) = λbox - let (Box val) = box - val +(Box.unbox) = λbox match box { + Box: box.val +} // Use tuples to store two values together without needing to create a new data type (Tuple.new fst snd) = diff --git a/tests/golden_tests/run_lazy/extracted_match_pred.hvm b/tests/golden_tests/run_lazy/extracted_match_pred.hvm index 7de90538..26ed5f13 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; 1+: (valS n-1) }) +val = λn (switch n { 0: valZ; _: (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 e950ba58..5d001346 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 { +main = @a @b let c = (+ a a); switch a { 0: b; - 1+: (+ a-1 b); + _: (+ a-1 b); } diff --git a/tests/golden_tests/run_lazy/list_take.hvm b/tests/golden_tests/run_lazy/list_take.hvm index 68a1c8b4..8befd00b 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) { + switch (== 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 7a3e7e4b..fb248552 100644 --- a/tests/golden_tests/run_lazy/list_to_tree.hvm +++ b/tests/golden_tests/run_lazy/list_to_tree.hvm @@ -3,17 +3,17 @@ List.len.go [] count = count List.len.go (List.cons x xs) count = (List.len.go xs (+ count 1)) Take.go n list = - match (== n 0) { + switch (== n 0) { | 0: (Take n list) - | 1+: [] + | _: [] } Take n [] = [] Take n (List.cons x xs) = (List.cons x (Take.go (- n 1) xs)) Drop.go n list = - match (== n 0) { + switch (== n 0) { | 0: (Drop n list) - | 1+: list + | _: 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 a0e97264..a4e1e130 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) { + switch (+ 0 1) { 0: λt λf t - 1+: λt λf f + _: λ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 f2d8723f..189e5ba2 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 { +main = @a @b @c @d switch a { 0: (+ (+ b c) d); - 1+: (+ (+ (+ a-1 b) c) d); + _: (+ (+ (+ 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 4b167c1b..4b6b8685 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 { +pred = @n switch n { 0: 0 - 1+: n-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 cf62c944..0288b329 100644 --- a/tests/golden_tests/run_lazy/merge_sort.hvm +++ b/tests/golden_tests/run_lazy/merge_sort.hvm @@ -7,9 +7,9 @@ sort (Node a b) = (merge (sort a) (sort b)) merge (Nil) b = b merge (Cons x xs) (Nil) = (Cons x xs) merge (Cons x xs) (Cons y ys) = - let t = match (< x y) { + let t = switch (< x y) { 0: λaλbλcλt(t c a b) - 1+: λaλbλcλt(t a b c) + _: λaλbλcλt(t a b c) } let t = (t (Cons x) λx(x) (Cons y)) @@ -19,9 +19,9 @@ merge (Cons x xs) (Cons y ys) = sum Nil = 0 sum (Cons h t) = (+ h (sum t)) -range n = match n { +range n = switch n { 0: λx (Leaf x) - 1+: λx (Node (range n-1 (+ (* x 2) 1)) (range n-1 (* x 2))) + _: λ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/nested_let_tup.hvm b/tests/golden_tests/run_lazy/nested_let_tup.hvm deleted file mode 100644 index 775a06eb..00000000 --- a/tests/golden_tests/run_lazy/nested_let_tup.hvm +++ /dev/null @@ -1,6 +0,0 @@ -main = - let (a, (b, c)) = - let (i, (j, k)) = (10, ((1, ((2, 3), 4)), 3)); - j; - let (x, y) = b; - x diff --git a/tests/golden_tests/run_lazy/num_pred.hvm b/tests/golden_tests/run_lazy/num_pred.hvm index bea29e05..4d91708c 100644 --- a/tests/golden_tests/run_lazy/num_pred.hvm +++ b/tests/golden_tests/run_lazy/num_pred.hvm @@ -1,4 +1,6 @@ -Pred 0 = 0 -Pred 1+pred = pred +Pred n = switch n { + 0: 0 + _: n-1 +} 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 acd51dec..8052e3dd 100644 --- a/tests/golden_tests/run_lazy/radix_sort_ctr.hvm +++ b/tests/golden_tests/run_lazy/radix_sort_ctr.hvm @@ -1,9 +1,9 @@ data Map = Free | Used | (Both a b) data Arr = Null | (Leaf x) | (Node a b) -(Swap s a b) = match s { +(Swap s a b) = switch s { 0: (Both a b) - 1+: (Both b a) + _: (Both b a) } // Sort : Arr -> Arr @@ -74,9 +74,9 @@ data Arr = Null | (Leaf x) | (Node a b) // Gen : U60 -> Arr (Gen n) = (Gen.go n 0) - (Gen.go n x) = match n { + (Gen.go n x) = switch 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 a3223cb6..8113eddc 100644 --- a/tests/golden_tests/run_lazy/recursive_match_native.hvm +++ b/tests/golden_tests/run_lazy/recursive_match_native.hvm @@ -1,8 +1,8 @@ add = λa λb (+ a b) -sum = λn match n { +sum = λn switch n { 0: 1 - 1+: (add (sum n-1) (sum n-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 268a479d..8b3a324f 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 1+x (head, tail)) = ((+ 1 head), (StrGo x tail)) +(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) 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 22279b4d..deadade9 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 1+x (head, tail)) = ((+ 1 head), (StrGo x tail)) +(StrGo 0 (head, tail)) = (head, tail) +(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) 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 5feee56e..112e6dc9 100644 --- a/tests/golden_tests/run_lazy/sum_tree.hvm +++ b/tests/golden_tests/run_lazy/sum_tree.hvm @@ -2,9 +2,9 @@ data Tree = (Leaf x) | (Node x0 x1) add = λa λb (+ a b) -gen = λn match n { +gen = λn switch n { 0: (Leaf 1) - 1+: (Node (gen n-1) (gen n-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 c8d83c62..5db50747 100644 --- a/tests/golden_tests/run_lazy/tuple_rots.hvm +++ b/tests/golden_tests/run_lazy/tuple_rots.hvm @@ -2,9 +2,9 @@ MkTup8 = @a @b @c @d @e @f @g @h @MkTup8 (MkTup8 a b c d e f g h) rot = λx (x λa λb λc λd λe λf λg λh (MkTup8 b c d e f g h a)) -app = λn match n { +app = λn switch n { 0: λf λx x - 1+: λf λx (app n-1 f (f x)) + _: λ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 427b8d99..0926e1e7 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 1+a *) = a +(Fn2 a *) = (- a 1) main = * diff --git a/tests/snapshots/cli__debug_u60_to_nat.hvm.snap b/tests/snapshots/cli__debug_u60_to_nat.hvm.snap index 2a340055..792394d5 100644 --- a/tests/snapshots/cli__debug_u60_to_nat.hvm.snap +++ b/tests/snapshots/cli__debug_u60_to_nat.hvm.snap @@ -4,9 +4,9 @@ input_file: tests/golden_tests/cli/debug_u60_to_nat.hvm --- (λa (U60ToNat a) 4) --------------------------------------- -(λa match a { 0: Z; 1+b: (S (U60ToNat b)) } 4) +(λa switch a { 0: Z; _: (S (U60ToNat a-1)) } 4) --------------------------------------- -match 4 { 0: Z; 1+a: (S (U60ToNat a)) } +let b = 4; switch b { 0: Z; _: (S (U60ToNat b-1)) } --------------------------------------- (λa λb (S (U60ToNat b)) * 3) --------------------------------------- diff --git a/tests/snapshots/cli__desugar_linearize_matches.hvm.snap b/tests/snapshots/cli__desugar_linearize_matches.hvm.snap index 571a93b1..70e400d4 100644 --- a/tests/snapshots/cli__desugar_linearize_matches.hvm.snap +++ b/tests/snapshots/cli__desugar_linearize_matches.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/cli/desugar_linearize_matches.hvm --- -(main) = λa λb (match a { 0: λc c; 1+: λ* λf f } b) +(main) = λa λb (switch a { 0: λc c; _: λ* λe e } b) diff --git a/tests/snapshots/cli__desugar_linearize_matches_extra.hvm.snap b/tests/snapshots/cli__desugar_linearize_matches_extra.hvm.snap index 47e44987..a7cc7307 100644 --- a/tests/snapshots/cli__desugar_linearize_matches_extra.hvm.snap +++ b/tests/snapshots/cli__desugar_linearize_matches_extra.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/cli/desugar_linearize_matches_extra.hvm --- -(main) = λa λb λc (match a { 0: λd λ* d; 1+: λ* λ* λi i } b c) +(main) = λa λb λc (switch a { 0: λd λ* d; _: λ* λ* λh h } b c) diff --git a/tests/snapshots/cli__warn_and_err.hvm.snap b/tests/snapshots/cli__warn_and_err.hvm.snap index 8ccfed5a..fa9307bf 100644 --- a/tests/snapshots/cli__warn_and_err.hvm.snap +++ b/tests/snapshots/cli__warn_and_err.hvm.snap @@ -4,7 +4,7 @@ input_file: tests/golden_tests/cli/warn_and_err.hvm --- Warnings: In definition 'Foo': - Repeated bind inside rule pattern: 'a'. + Repeated bind in pattern matching rule: 'a'. Errors: In definition 'Main': diff --git a/tests/snapshots/compile_file__missing_pat.hvm.snap b/tests/snapshots/compile_file__missing_pat.hvm.snap index f43931c2..ec0beb56 100644 --- a/tests/snapshots/compile_file__missing_pat.hvm.snap +++ b/tests/snapshots/compile_file__missing_pat.hvm.snap @@ -3,5 +3,5 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/compile_file/missing_pat.hvm --- Errors: -At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected '(', '#', '$', , '[', '{', 'λ', 'let', 'use', 'match', '*', '|', +, , , or +At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected  2 | : * diff --git a/tests/snapshots/compile_file__repeated_bind_rule.hvm.snap b/tests/snapshots/compile_file__repeated_bind_rule.hvm.snap index 0f0ed045..1f359a81 100644 --- a/tests/snapshots/compile_file__repeated_bind_rule.hvm.snap +++ b/tests/snapshots/compile_file__repeated_bind_rule.hvm.snap @@ -4,7 +4,7 @@ input_file: tests/golden_tests/compile_file/repeated_bind_rule.hvm --- Warnings: In definition 'Foo': - Repeated bind inside rule pattern: 'a'. + Repeated bind in pattern matching rule: 'a'. @Foo = (* (a a)) diff --git a/tests/snapshots/compile_file__switch_all_patterns.hvm.snap b/tests/snapshots/compile_file__switch_all_patterns.hvm.snap new file mode 100644 index 00000000..7c7f70e7 --- /dev/null +++ b/tests/snapshots/compile_file__switch_all_patterns.hvm.snap @@ -0,0 +1,17 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/compile_file/switch_all_patterns.hvm +--- +Errors: +In definition 'succ': + Malformed 'switch' expression. Expected case '0', found '_'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case. +In definition 'succ_zero': + Malformed 'switch' expression. Expected case '0', found '_'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case. +In definition 'succ_zero_succ': + Malformed 'switch' expression. Expected case '0', found '_'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case. +In definition 'zero_succ_succ': + Extra arms in 'switch' expression. No rules should come after the default. +In definition 'zero_succ_zero': + Extra arms in 'switch' expression. No rules should come after the default. +In definition 'zero_zero_succ': + Malformed 'switch' expression. Expected case '1', found '0'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case. diff --git a/tests/snapshots/compile_file__switch_in_switch_arg.hvm.snap b/tests/snapshots/compile_file__switch_in_switch_arg.hvm.snap new file mode 100644 index 00000000..314fe687 --- /dev/null +++ b/tests/snapshots/compile_file__switch_in_switch_arg.hvm.snap @@ -0,0 +1,5 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/compile_file/switch_in_switch_arg.hvm +--- +@main = ({3 a ?<#0 (b b) ?<(* #0) (* (c c)) (a d)>>} d) diff --git a/tests/snapshots/compile_file__switch_unscoped_lambda.hvm.snap b/tests/snapshots/compile_file__switch_unscoped_lambda.hvm.snap new file mode 100644 index 00000000..365d587f --- /dev/null +++ b/tests/snapshots/compile_file__switch_unscoped_lambda.hvm.snap @@ -0,0 +1,15 @@ +--- +source: tests/golden_tests.rs +input_file: tests/golden_tests/compile_file/switch_unscoped_lambda.hvm +--- +Warnings: +In definition 'lambda_in': + Definition is unused. +In definition 'lambda_out': + Definition is unused. + +@lambda_in = (?<(a a) (b (c b)) (c d)> d) + +@lambda_out = (? (a c)) + +@main = * diff --git a/tests/snapshots/compile_file__warn_and_err.hvm.snap b/tests/snapshots/compile_file__warn_and_err.hvm.snap index 38a42ccb..7de1287e 100644 --- a/tests/snapshots/compile_file__warn_and_err.hvm.snap +++ b/tests/snapshots/compile_file__warn_and_err.hvm.snap @@ -4,7 +4,7 @@ input_file: tests/golden_tests/compile_file/warn_and_err.hvm --- Warnings: In definition 'Foo': - Repeated bind inside rule pattern: 'a'. + Repeated bind in pattern matching rule: 'a'. Errors: In definition 'Main': diff --git a/tests/snapshots/compile_file_o_all__match_adt_non_exhaustive.hvm.snap b/tests/snapshots/compile_file_o_all__match_adt_non_exhaustive.hvm.snap index c23745ef..de97799e 100644 --- a/tests/snapshots/compile_file_o_all__match_adt_non_exhaustive.hvm.snap +++ b/tests/snapshots/compile_file_o_all__match_adt_non_exhaustive.hvm.snap @@ -4,5 +4,4 @@ input_file: tests/golden_tests/compile_file_o_all/match_adt_non_exhaustive.hvm --- Errors: In definition 'main': - Non-exhaustive pattern matching. Hint: - Case 'Some' not covered. + Non-exhaustive 'match' expression of type 'Maybe'. Case 'Some' not covered. diff --git a/tests/snapshots/compile_file_o_all__non_exhaustive_and.hvm.snap b/tests/snapshots/compile_file_o_all__non_exhaustive_and.hvm.snap index 7bbbad94..277368b9 100644 --- a/tests/snapshots/compile_file_o_all__non_exhaustive_and.hvm.snap +++ b/tests/snapshots/compile_file_o_all__non_exhaustive_and.hvm.snap @@ -4,5 +4,4 @@ input_file: tests/golden_tests/compile_file_o_all/non_exhaustive_and.hvm --- Errors: In definition 'Bool.and': - Non-exhaustive pattern matching. Hint: - Case 'F' not covered. + Non-exhaustive pattern matching rule. Constructor 'F' of type 'Bool' not covered diff --git a/tests/snapshots/compile_file_o_all__non_exhaustive_different_types.hvm.snap b/tests/snapshots/compile_file_o_all__non_exhaustive_different_types.hvm.snap index e40de091..4a77847f 100644 --- a/tests/snapshots/compile_file_o_all__non_exhaustive_different_types.hvm.snap +++ b/tests/snapshots/compile_file_o_all__non_exhaustive_different_types.hvm.snap @@ -4,5 +4,4 @@ input_file: tests/golden_tests/compile_file_o_all/non_exhaustive_different_types --- Errors: In definition 'foo': - Non-exhaustive pattern matching. Hint: - Case 't3' not covered. + Non-exhaustive pattern matching rule. Constructor 't3' of type 'b3' not covered diff --git a/tests/snapshots/compile_file_o_all__non_exhaustive_pattern.hvm.snap b/tests/snapshots/compile_file_o_all__non_exhaustive_pattern.hvm.snap index 0e3f9afd..57ac8214 100644 --- a/tests/snapshots/compile_file_o_all__non_exhaustive_pattern.hvm.snap +++ b/tests/snapshots/compile_file_o_all__non_exhaustive_pattern.hvm.snap @@ -4,5 +4,4 @@ input_file: tests/golden_tests/compile_file_o_all/non_exhaustive_pattern.hvm --- Errors: In definition 'Foo': - Non-exhaustive pattern matching. Hint: - Case 'A' not covered. + Non-exhaustive pattern matching rule. Constructor 'A' of type 'Type' not covered diff --git a/tests/snapshots/compile_file_o_all__non_exhaustive_tree.hvm.snap b/tests/snapshots/compile_file_o_all__non_exhaustive_tree.hvm.snap index 8bcc44b4..95f5dfb9 100644 --- a/tests/snapshots/compile_file_o_all__non_exhaustive_tree.hvm.snap +++ b/tests/snapshots/compile_file_o_all__non_exhaustive_tree.hvm.snap @@ -4,5 +4,4 @@ input_file: tests/golden_tests/compile_file_o_all/non_exhaustive_tree.hvm --- Errors: In definition 'Warp': - Non-exhaustive pattern matching. Hint: - Case 'Both' not covered. + Non-exhaustive pattern matching rule. Constructor 'Both' of type 'Tree' not covered diff --git a/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap b/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap index 1acbbb86..08270e38 100644 --- a/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap +++ b/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap @@ -2,9 +2,11 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm --- -@Foo = ({2 (* #0) {2 @Foo$C0 a}} a) +@Foo = ({2 (* #0) {2 @Foo$C1 a}} a) -@Foo$C0 = (?<#0 (a a) b> b) +@Foo$C0 = (<+ #1 a> a) + +@Foo$C1 = (?<#0 @Foo$C0 a> a) @main = a & @Foo ~ (@true (#3 a)) diff --git a/tests/snapshots/desugar_file__combinators.hvm.snap b/tests/snapshots/desugar_file__combinators.hvm.snap index 062a8a5f..0e62c232 100644 --- a/tests/snapshots/desugar_file__combinators.hvm.snap +++ b/tests/snapshots/desugar_file__combinators.hvm.snap @@ -30,7 +30,7 @@ input_file: tests/golden_tests/desugar_file/combinators.hvm (A$C0) = let {b c} = A; λd (b c d) -(B$C0) = let (c, d) = B; λe (c d e) +(B$C0) = let (b, c) = B; λd (b c d) (List.ignore$C0) = #List λ* #List λd (List.ignore d List.ignore) diff --git a/tests/snapshots/desugar_file__non_exaustive_limit.hvm.snap b/tests/snapshots/desugar_file__non_exaustive_limit.hvm.snap index 0e234604..b690525d 100644 --- a/tests/snapshots/desugar_file__non_exaustive_limit.hvm.snap +++ b/tests/snapshots/desugar_file__non_exaustive_limit.hvm.snap @@ -4,5 +4,4 @@ input_file: tests/golden_tests/desugar_file/non_exaustive_limit.hvm --- Errors: In definition 'Bar': - Non-exhaustive pattern matching. Hint: - Case 'B' not covered. + Non-exhaustive pattern matching rule. Constructor 'B' of type 'Foo' not covered diff --git a/tests/snapshots/encode_pattern_match__and3.hvm.snap b/tests/snapshots/encode_pattern_match__and3.hvm.snap index 64dc16ec..e335d039 100644 --- a/tests/snapshots/encode_pattern_match__and3.hvm.snap +++ b/tests/snapshots/encode_pattern_match__and3.hvm.snap @@ -3,7 +3,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/and3.hvm --- TaggedScott: -(And) = λa let (b, c, d) = a; (#Bool (b λe λf (#Bool (e λh #Bool (h T F) λ* F) f) λ* λ* F) c d) +(And) = λa let (b, c, d) = a; (#Bool (b λe λf (#Bool (e λg #Bool (g T F) λ* F) f) λ* λ* F) c d) (main) = (And (F, T, F)) @@ -12,7 +12,7 @@ TaggedScott: (F) = #Bool λ* #Bool λb b Scott: -(And) = λa let (b, c, d) = a; (b λe λf (e λh (h T F) λ* F f) λ* λ* F c d) +(And) = λa let (b, c, d) = a; (b λe λf (e λg (g T F) λ* F f) λ* λ* F c d) (main) = (And (F, T, F)) diff --git a/tests/snapshots/encode_pattern_match__bool.hvm.snap b/tests/snapshots/encode_pattern_match__bool.hvm.snap index cd43bb09..12db8b3d 100644 --- a/tests/snapshots/encode_pattern_match__bool.hvm.snap +++ b/tests/snapshots/encode_pattern_match__bool.hvm.snap @@ -5,7 +5,7 @@ input_file: tests/golden_tests/encode_pattern_match/bool.hvm TaggedScott: (not) = λa #bool (a false true) -(and) = λa λb (#bool (a λc #bool (c true false) λg #bool (g false false)) b) +(and) = λa λb (#bool (a λc #bool (c true false) λd #bool (d false false)) b) (and2) = λa λb (#bool (a λc c λ* false) b) @@ -20,7 +20,7 @@ TaggedScott: Scott: (not) = λa (a false true) -(and) = λa λb (a λc (c true false) λg (g false false) b) +(and) = λa λb (a λc (c true false) λd (d false false) b) (and2) = λa λb (a λc c λ* false b) diff --git a/tests/snapshots/encode_pattern_match__def_tups.hvm.snap b/tests/snapshots/encode_pattern_match__def_tups.hvm.snap index 3bee9584..c9f5fdb0 100644 --- a/tests/snapshots/encode_pattern_match__def_tups.hvm.snap +++ b/tests/snapshots/encode_pattern_match__def_tups.hvm.snap @@ -3,11 +3,11 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/def_tups.hvm --- TaggedScott: -(go) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, h) = e; λi λj (let (k, l) = h; λm λn λo (+ (+ (+ (+ l k) o) n) m) i j g) f d) b) +(go) = λa let (b, c) = a; let (d, e) = c; let (f, g) = e; let (h, i) = g; (+ (+ (+ (+ i h) f) d) b) (main) = (go (1, (2, (3, (4, 5))))) Scott: -(go) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, h) = e; λi λj (let (k, l) = h; λm λn λo (+ (+ (+ (+ l k) o) n) m) i j g) f d) b) +(go) = λa let (b, c) = a; let (d, e) = c; let (f, g) = e; let (h, i) = g; (+ (+ (+ (+ i h) f) d) b) (main) = (go (1, (2, (3, (4, 5))))) diff --git a/tests/snapshots/encode_pattern_match__definition_merge.hvm.snap b/tests/snapshots/encode_pattern_match__definition_merge.hvm.snap index 9c8497d0..1c68ff61 100644 --- a/tests/snapshots/encode_pattern_match__definition_merge.hvm.snap +++ b/tests/snapshots/encode_pattern_match__definition_merge.hvm.snap @@ -3,7 +3,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/definition_merge.hvm --- TaggedScott: -(Foo) = λa λb (#Either (a #Either λc λd (#Bool (c λe #Either (e #Either λg #Bool (g 1 1) #Either λj #Bool (j 2 2)) λm #Either (m #Either λo #Bool (o 1 1) #Either λr #Bool (r 2 2))) d) #Either λu λv (#Bool (u λw #Either (w #Either λy #Bool (y 3 3) #Either λbb #Bool (bb 3 3)) λeb #Either (eb #Either λgb #Bool (gb 3 3) #Either λjb #Bool (jb 3 3))) v)) b) +(Foo) = λa λb (#Either (a #Either λc λd (#Bool (c λe #Either (e #Either λf #Bool (f 1 1) #Either λg #Bool (g 2 2)) λh #Either (h #Either λi #Bool (i 1 1) #Either λj #Bool (j 2 2))) d) #Either λk λl (#Bool (k λm #Either (m #Either λn #Bool (n 3 3) #Either λo #Bool (o 3 3)) λp #Either (p #Either λq #Bool (q 3 3) #Either λr #Bool (r 3 3))) l)) b) (Left) = λa #Either λb #Either λ* #Either (b a) @@ -14,7 +14,7 @@ TaggedScott: (False) = #Bool λ* #Bool λb b Scott: -(Foo) = λa λb (a λc λd (c λe (e λg (g 1 1) λj (j 2 2)) λm (m λo (o 1 1) λr (r 2 2)) d) λu λv (u λw (w λy (y 3 3) λbb (bb 3 3)) λeb (eb λgb (gb 3 3) λjb (jb 3 3)) v) b) +(Foo) = λa λb (a λc λd (c λe (e λf (f 1 1) λg (g 2 2)) λh (h λi (i 1 1) λj (j 2 2)) d) λk λl (k λm (m λn (n 3 3) λo (o 3 3)) λp (p λq (q 3 3) λr (r 3 3)) l) b) (Left) = λa λb λ* (b a) 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 8f341af1..a57e5792 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 (*, c) = a; let (*, e) = c; let (f, *) = e; f -(Fn3) = λa λ* let (c, *) = a; match c { 0: 0; 1+: λf f } +(Fn3) = λa λ* let (c, *) = a; switch c { 0: 0; _: λe (+ e 1) } (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0) @@ -16,6 +16,6 @@ Scott: (Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f -(Fn3) = λa λ* let (c, *) = a; match c { 0: 0; 1+: λf f } +(Fn3) = λa λ* let (c, *) = a; switch c { 0: 0; _: λe (+ e 1) } (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0) diff --git a/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap b/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap index 3ba0d155..98bf30e2 100644 --- a/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap +++ b/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap @@ -3,7 +3,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/list_merge_sort.hvm --- TaggedScott: -(If) = λa λb λc (#Bool (a λd λ* d λ* λh h) b c) +(If) = λa λb λc (#Bool (a λd λ* d λ* λg g) b c) (Pure) = λa (Cons a Nil) @@ -15,7 +15,7 @@ TaggedScott: (MergePair) = λa λb (#List_ (b #List_ λc #List_ λd λe (#List_ (d #List_ λf #List_ λg λh let {h h_2} = h; λi (Cons (Merge h i f) (MergePair h_2 g)) λ* λk (Cons k Nil)) e c) λ* Nil) a) -(Merge) = λa λb λc (#List_ (b #List_ λd #List_ λe λf λg (#List_ (g #List_ λh let {h h_2 h_3} = h; #List_ λi let {i i_2} = i; λj let {j j_2 j_3} = j; λk let {k k_2 k_3} = k; λl let {l l_2} = l; (If (j k h) (Cons k_2 (Merge j_2 l (Cons h_2 i))) (Cons h_3 (Merge j_3 (Cons k_3 l_2) i_2))) λ* λp λq (Cons p q)) f d e) λ* λt t) a c) +(Merge) = λa λb λc (#List_ (b #List_ λd #List_ λe λf λg (#List_ (g #List_ λh let {h h_2 h_3} = h; #List_ λi let {i i_2} = i; λj let {j j_2 j_3} = j; λk let {k k_2 k_3} = k; λl let {l l_2} = l; (If (j k h) (Cons k_2 (Merge j_2 l (Cons h_2 i))) (Cons h_3 (Merge j_3 (Cons k_3 l_2) i_2))) λ* λp λq (Cons p q)) f d e) λ* λs s) a c) (True) = #Bool λa #Bool λ* a @@ -26,7 +26,7 @@ TaggedScott: (Nil) = #List_ λ* #List_ λb b Scott: -(If) = λa λb λc (a λd λ* d λ* λh h b c) +(If) = λa λb λc (a λd λ* d λ* λg g b c) (Pure) = λa (Cons a Nil) @@ -38,7 +38,7 @@ Scott: (MergePair) = λa λb (b λc λd λe (d λf λg λh let {h h_2} = h; λi (Cons (Merge h i f) (MergePair h_2 g)) λ* λk (Cons k Nil) e c) λ* Nil a) -(Merge) = λa λb λc (b λd λe λf λg (g λh let {h h_2 h_3} = h; λi let {i i_2} = i; λj let {j j_2 j_3} = j; λk let {k k_2 k_3} = k; λl let {l l_2} = l; (If (j k h) (Cons k_2 (Merge j_2 l (Cons h_2 i))) (Cons h_3 (Merge j_3 (Cons k_3 l_2) i_2))) λ* λp λq (Cons p q) f d e) λ* λt t a c) +(Merge) = λa λb λc (b λd λe λf λg (g λh let {h h_2 h_3} = h; λi let {i i_2} = i; λj let {j j_2 j_3} = j; λk let {k k_2 k_3} = k; λl let {l l_2} = l; (If (j k h) (Cons k_2 (Merge j_2 l (Cons h_2 i))) (Cons h_3 (Merge j_3 (Cons k_3 l_2) i_2))) λ* λp λq (Cons p q) f d e) λ* λs s a c) (True) = λa λ* a diff --git a/tests/snapshots/encode_pattern_match__match_adt_unscoped_in_arm.hvm.snap b/tests/snapshots/encode_pattern_match__match_adt_unscoped_in_arm.hvm.snap index 964d40a2..7f749fe3 100644 --- a/tests/snapshots/encode_pattern_match__match_adt_unscoped_in_arm.hvm.snap +++ b/tests/snapshots/encode_pattern_match__match_adt_unscoped_in_arm.hvm.snap @@ -3,14 +3,14 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_in_arm.hvm --- TaggedScott: -(main) = λa #bool (a λ$x $x λd d) +(main) = λa #bool (a λ$x $x λb b) (T) = #bool λa #bool λ* a (F) = #bool λ* #bool λb b Scott: -(main) = λa (a λ$x $x λd d) +(main) = λa (a λ$x $x λb b) (T) = λa λ* a diff --git a/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap b/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap index 63a423e2..2523dd83 100644 --- a/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap +++ b/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap @@ -3,14 +3,14 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hvm --- TaggedScott: -(main) = (#Maybe ((Some 1) λ$x * #Maybe λc c) $x) +(main) = (#Maybe ((Some 1) λ$x * #Maybe λb b) $x) (None) = #Maybe λa #Maybe λ* a (Some) = λa #Maybe λ* #Maybe λc #Maybe (c a) Scott: -(main) = (Some 1 λ$x * λc c $x) +(main) = (Some 1 λ$x * λb b $x) (None) = λa λ* a diff --git a/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap b/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap index 26852bb2..ed3896e9 100644 --- a/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap +++ b/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap @@ -3,9 +3,9 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm --- TaggedScott: -(Foo) = λ$x #Maybe ((Some 1) $x #Maybe λc c) +(Foo) = λ$x #Maybe ((Some 1) $x #Maybe λb b) -(Bar) = (#Maybe ((Some 1) $x #Maybe λc c) λ$x *) +(Bar) = (#Maybe ((Some 1) $x #Maybe λb b) λ$x *) (main) = * @@ -14,9 +14,9 @@ TaggedScott: (Some) = λa #Maybe λ* #Maybe λc #Maybe (c a) Scott: -(Foo) = λ$x (Some 1 $x λc c) +(Foo) = λ$x (Some 1 $x λb b) -(Bar) = (Some 1 $x λc c λ$x *) +(Bar) = (Some 1 $x λb b λ$x *) (main) = * diff --git a/tests/snapshots/encode_pattern_match__match_bind.hvm.snap b/tests/snapshots/encode_pattern_match__match_bind.hvm.snap index 44810496..63bb24be 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; 1+: λd λe (+ e d) } a_2) +(cheese) = let {a a_2} = (+ 2 3); (switch a { 0: λ* 653323; _: λc λd (+ d c) } a_2) (main) = cheese Scott: -(cheese) = let {a a_2} = (+ 2 3); (match a { 0: λ* 653323; 1+: λd λe (+ e d) } a_2) +(cheese) = let {a a_2} = (+ 2 3); (switch a { 0: λ* 653323; _: λc λd (+ d c) } 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 index 0d8cf886..87cbd0a6 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 @@ -3,7 +3,7 @@ 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 λc #String λd λe (match (- c 40) { 0: λf λg (Ok (40, g, f)); 1+: λi match i { 0: λj λk (Ok (41, k, j)); 1+: λm match (- m 18446744073709551584) { 0: λn λo (Ok (0, o, n)); 1+: λq λs λt (Err ((String.cons (+ q 11) t), s)) } } } e d) λu (Err (String.nil, u))) a) +(Parse) = λa λb (#String (b #String λc #String λd λe (switch (- c 10) { 0: λg λh (Ok (0, h, g)); _: λi λj λk (switch (- i 29) { 0: λm λn (Ok (40, n, m)); _: λo λp λq (switch o { 0: λr λs (Ok (41, s, r)); _: λt λu λv (Err ((String.cons (+ t 42) v), u)) } p q) } j k) } e d) λw (Err (String.nil, w))) a) (main) = #Result_ ((Parse * (String.cons 40 (String.cons 43 String.nil))) #Result_ λd let (e, f, g) = d; (e, (Parse g f)) #Result_ λh (Err h)) @@ -16,7 +16,7 @@ TaggedScott: (Err) = λa #Result_ λ* #Result_ λc #Result_ (c a) Scott: -(Parse) = λa λb (b λc λd λe (match (- c 40) { 0: λf λg (Ok (40, g, f)); 1+: λi match i { 0: λj λk (Ok (41, k, j)); 1+: λm match (- m 18446744073709551584) { 0: λn λo (Ok (0, o, n)); 1+: λq λs λt (Err ((String.cons (+ q 11) t), s)) } } } e d) λu (Err (String.nil, u)) a) +(Parse) = λa λb (b λc λd λe (switch (- c 10) { 0: λg λh (Ok (0, h, g)); _: λi λj λk (switch (- i 29) { 0: λm λn (Ok (40, n, m)); _: λo λp λq (switch o { 0: λr λs (Ok (41, s, r)); _: λt λu λv (Err ((String.cons (+ t 42) v), u)) } p q) } j k) } e d) λw (Err (String.nil, w)) a) (main) = (Parse * (String.cons 40 (String.cons 43 String.nil)) λd let (e, f, g) = d; (e, (Parse g f)) λh (Err h)) diff --git a/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap b/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap index 56425e05..858d4f8c 100644 --- a/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap +++ b/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap @@ -3,23 +3,23 @@ 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 } +(pred) = λa switch a { 0: 0; _: λb b } -(pred2) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe e } } +(pred2) = λa switch a { 0: 0; _: λb switch b { 0: 0; _: λc c } } -(pred3) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe match e { 0: 0; 1+: λg g } } } +(pred3) = λa switch a { 0: 0; _: λb switch b { 0: 0; _: λc switch c { 0: 0; _: λd (- (+ d 3) 3) } } } -(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) } } } } +(zero) = λa switch a { 0: 1; _: λb switch b { 0: 0; _: λ* 0 } } (main) = * Scott: -(pred) = λa match a { 0: 0; 1+: λc c } +(pred) = λa switch a { 0: 0; _: λb b } -(pred2) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe e } } +(pred2) = λa switch a { 0: 0; _: λb switch b { 0: 0; _: λc c } } -(pred3) = λa match a { 0: 0; 1+: λc match c { 0: 0; 1+: λe match e { 0: 0; 1+: λg g } } } +(pred3) = λa switch a { 0: 0; _: λb switch b { 0: 0; _: λc switch c { 0: 0; _: λd (- (+ d 3) 3) } } } -(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) } } } } +(zero) = λa switch a { 0: 1; _: λb switch b { 0: 0; _: λ* 0 } } (main) = * diff --git a/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap b/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap index 3968b94e..bffee9fe 100644 --- a/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap +++ b/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap @@ -3,14 +3,14 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/encode_pattern_match/non_matching_fst_arg.hvm --- TaggedScott: -(Foo) = λa λb (#bool (b λc let {c c_2} = c; (Foo c c_2) λe e) a) +(Foo) = λa λb (#bool (b λc let {c c_2} = c; (Foo c c_2) λd d) a) (true) = #bool λa #bool λ* a (false) = #bool λ* #bool λb b Scott: -(Foo) = λa λb (b λc let {c c_2} = c; (Foo c c_2) λe e a) +(Foo) = λa λb (b λc let {c c_2} = c; (Foo c c_2) λd d a) (true) = λa λ* a diff --git a/tests/snapshots/readback_lnet__match.hvm.snap b/tests/snapshots/readback_lnet__match.hvm.snap index 092fa481..28aa43d6 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 --- -match 1 { 0: λa a; 1+b: b } +let c = 1; switch c { 0: λa a; _: c-1 } diff --git a/tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap b/tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap index 66d0d02c..233193f7 100644 --- a/tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap +++ b/tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap @@ -6,14 +6,12 @@ Lazy mode: Warnings: During readback: Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'. - Invalid Adt Match. -λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * } +λa match a { Some: #Option (#wrong_tag λb b a.val); None: * } Strict mode: Warnings: During readback: Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'. - Invalid Adt Match. -λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * } +λa match a { Some: #Option (#wrong_tag λb b a.val); None: * } diff --git a/tests/snapshots/run_file__adt_option_and.hvm.snap b/tests/snapshots/run_file__adt_option_and.hvm.snap index 2b6ec01d..c35b0a45 100644 --- a/tests/snapshots/run_file__adt_option_and.hvm.snap +++ b/tests/snapshots/run_file__adt_option_and.hvm.snap @@ -3,7 +3,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/adt_option_and.hvm --- Lazy mode: -λa λb match a { (Some c): match b { (Some d): (Some (c, d)); (None): None }; (None): None } +λa λb match a { Some: match b { Some: (Some (a.val, b.val)); None: None }; None: None } Strict mode: -λa match a { (Some b): λc (match c { (Some d): λe (Some (e, d)); (None): λ* None } b); (None): λ* None } +λa match a { Some: λc (match c { Some: λe (Some (e, c.val)); None: λ* None } a.val); None: λ* None } diff --git a/tests/snapshots/run_file__adt_wrong_tag.hvm.snap b/tests/snapshots/run_file__adt_wrong_tag.hvm.snap index efc9ce81..59263545 100644 --- a/tests/snapshots/run_file__adt_wrong_tag.hvm.snap +++ b/tests/snapshots/run_file__adt_wrong_tag.hvm.snap @@ -6,14 +6,12 @@ Lazy mode: Warnings: During readback: Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'. - Invalid Adt Match. -λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * } +λa match a { Some: #Option (#wrong_tag λb b a.val); None: * } Strict mode: Warnings: During readback: Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'. - Invalid Adt Match. -λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * } +λa match a { Some: #Option (#wrong_tag λb b a.val); None: * } diff --git a/tests/snapshots/run_file__def_bool_num.hvm.snap b/tests/snapshots/run_file__def_bool_num.hvm.snap index 0bd2a05e..6df449aa 100644 --- a/tests/snapshots/run_file__def_bool_num.hvm.snap +++ b/tests/snapshots/run_file__def_bool_num.hvm.snap @@ -5,12 +5,10 @@ input_file: tests/golden_tests/run_file/def_bool_num.hvm Lazy mode: Errors: In definition 'go': - Non-exhaustive pattern matching. Hint: - Case '+' not covered. + Non-exhaustive pattern matching rule. Default case of number type not covered. Strict mode: Errors: In definition 'go': - Non-exhaustive pattern matching. Hint: - Case '+' not covered. + Non-exhaustive pattern matching rule. Default case of number type not covered. diff --git a/tests/snapshots/run_file__def_num_bool.hvm.snap b/tests/snapshots/run_file__def_num_bool.hvm.snap index 59302bb0..686fba45 100644 --- a/tests/snapshots/run_file__def_num_bool.hvm.snap +++ b/tests/snapshots/run_file__def_num_bool.hvm.snap @@ -5,12 +5,10 @@ input_file: tests/golden_tests/run_file/def_num_bool.hvm Lazy mode: Errors: In definition 'go': - Non-exhaustive pattern matching. Hint: - Case '+' not covered. + Non-exhaustive pattern matching rule. Default case of number type not covered. Strict mode: Errors: In definition 'go': - Non-exhaustive pattern matching. Hint: - Case '+' not covered. + Non-exhaustive pattern matching rule. Default case of number type not covered. diff --git a/tests/snapshots/run_file__linearize_match.hvm.snap b/tests/snapshots/run_file__linearize_match.hvm.snap index 614a80e0..21ba762f 100644 --- a/tests/snapshots/run_file__linearize_match.hvm.snap +++ b/tests/snapshots/run_file__linearize_match.hvm.snap @@ -3,7 +3,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/linearize_match.hvm --- Lazy mode: -λa match a { 0: λb b; 1+c: λd (+ c d) } +λa switch a { 0: λb b; _: λd (+ a-1 d) } Strict mode: -λa match a { 0: λb b; 1+c: λd (+ c d) } +λa switch a { 0: λb b; _: λ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 34d59d8a..fba3bfcc 100644 --- a/tests/snapshots/run_file__match_mult_linearization.hvm.snap +++ b/tests/snapshots/run_file__match_mult_linearization.hvm.snap @@ -3,7 +3,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/match_mult_linearization.hvm --- Lazy mode: -λa match a { 0: λb λc λd (+ (+ b c) d); 1+e: λf λg λh (+ (+ (+ e f) g) h) } +λa switch a { 0: λb λc λd (+ (+ b c) d); _: λf λg λh (+ (+ (+ a-1 f) g) h) } Strict mode: -λa match a { 0: λb λc λd (+ (+ b c) d); 1+e: λf λg λh (+ (+ (+ e f) g) h) } +λa switch a { 0: λb λc λd (+ (+ b c) d); _: λf λg λh (+ (+ (+ a-1 f) g) h) } diff --git a/tests/snapshots/run_file__match_num_succ_complex.hvm.snap b/tests/snapshots/run_file__match_num_succ_complex.hvm.snap index 0ff5b6fb..e529a26b 100644 --- a/tests/snapshots/run_file__match_num_succ_complex.hvm.snap +++ b/tests/snapshots/run_file__match_num_succ_complex.hvm.snap @@ -3,7 +3,7 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/match_num_succ_complex.hvm --- Lazy mode: -[[5, 5, 0, 0, 0, 6], [5, 5, 0, 0, 0, 6], [5, 5, 0, 0, 0, 6]] +[[5, 5, 0, 0, 0, 6], [5, 5, 0, 0, 0, 6]] Strict mode: -[[5, 5, 0, 0, 0, 6], [5, 5, 0, 0, 0, 6], [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__match_vars.hvm.snap b/tests/snapshots/run_file__match_vars.hvm.snap index 42120c47..1995e596 100644 --- a/tests/snapshots/run_file__match_vars.hvm.snap +++ b/tests/snapshots/run_file__match_vars.hvm.snap @@ -3,7 +3,12 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/match_vars.hvm --- Lazy mode: -1 +Errors: +In definition 'main': + Irrefutable 'match' expression. All cases after 'true' will be ignored. If this is not a mistake, consider using a 'let' expression instead. + Strict mode: -1 +Errors: +In definition 'main': + Irrefutable 'match' expression. All cases after 'true' will be ignored. If this is not a mistake, consider using a 'let' expression instead. diff --git a/tests/snapshots/run_file__num_match_missing_var.hvm.snap b/tests/snapshots/run_file__num_match_missing_var.hvm.snap index eb5a4fbe..02e15097 100644 --- a/tests/snapshots/run_file__num_match_missing_var.hvm.snap +++ b/tests/snapshots/run_file__num_match_missing_var.hvm.snap @@ -4,17 +4,15 @@ input_file: tests/golden_tests/run_file/num_match_missing_var.hvm --- Lazy mode: Errors: -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'. +In definition 'if2': + Extra arms in 'switch' expression. No rules should come after the default. +In definition 'if3': + Extra arms in 'switch' expression. No rules should come after the default. Strict mode: Errors: -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'. +In definition 'if2': + Extra arms in 'switch' expression. No rules should come after the default. +In definition 'if3': + Extra arms in 'switch' expression. No rules should come after the default. diff --git a/tests/snapshots/run_lazy__adt_match_wrong_tag.hvm.snap b/tests/snapshots/run_lazy__adt_match_wrong_tag.hvm.snap index 22701d72..9562beb4 100644 --- a/tests/snapshots/run_lazy__adt_match_wrong_tag.hvm.snap +++ b/tests/snapshots/run_lazy__adt_match_wrong_tag.hvm.snap @@ -5,6 +5,5 @@ input_file: tests/golden_tests/run_lazy/adt_match_wrong_tag.hvm Warnings: During readback: Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'. - Invalid Adt Match. -λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * } +λa match a { Some: #Option (#wrong_tag λb b a.val); None: * } diff --git a/tests/snapshots/run_lazy__adt_option_and.hvm.snap b/tests/snapshots/run_lazy__adt_option_and.hvm.snap index e86516c8..1aecf2a0 100644 --- a/tests/snapshots/run_lazy__adt_option_and.hvm.snap +++ b/tests/snapshots/run_lazy__adt_option_and.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_lazy/adt_option_and.hvm --- -λa λb match a { (Some c): match b { (Some d): (Some (c, d)); (None): None }; (None): None } +λa λb match a { Some: match b { Some: (Some (a.val, b.val)); None: None }; None: None } diff --git a/tests/snapshots/run_lazy__adt_wrong_tag.hvm.snap b/tests/snapshots/run_lazy__adt_wrong_tag.hvm.snap index c790c89e..e5d8d336 100644 --- a/tests/snapshots/run_lazy__adt_wrong_tag.hvm.snap +++ b/tests/snapshots/run_lazy__adt_wrong_tag.hvm.snap @@ -5,6 +5,5 @@ input_file: tests/golden_tests/run_lazy/adt_wrong_tag.hvm Warnings: During readback: Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'. - Invalid Adt Match. -λa match a { (Some Some.val): #Option (#wrong_tag λb b Some.val); (None): * } +λa match a { Some: #Option (#wrong_tag λb b a.val); None: * } diff --git a/tests/snapshots/run_lazy__linearize_match.hvm.snap b/tests/snapshots/run_lazy__linearize_match.hvm.snap index 5b74b2fc..11ed24c3 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+c: λd (+ c d) } +λa switch a { 0: λb b; _: λ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 99c675ac..0138d26a 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+e: λf λg λh (+ (+ (+ e f) g) h) } +λa switch a { 0: λb λc λd (+ (+ b c) d); _: λf λg λh (+ (+ (+ a-1 f) g) h) } diff --git a/tests/snapshots/simplify_matches__already_flat.hvm.snap b/tests/snapshots/simplify_matches__already_flat.hvm.snap index 725ffb1d..f6df7efe 100644 --- a/tests/snapshots/simplify_matches__already_flat.hvm.snap +++ b/tests/snapshots/simplify_matches__already_flat.hvm.snap @@ -2,32 +2,32 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/already_flat.hvm --- -(Rule1) = λa a +(Rule1) = λx x -(Rule2) = λ* λb b +(Rule2) = λ%arg0 λx x -(Rule3) = λa λb λc λd (a b c d) +(Rule3) = λ%arg0 λ%arg1 λ%arg2 λ%arg3 (%arg0 %arg1 %arg2 %arg3) -(Rule4) = λa match a { (CtrA): λc c; (CtrB d): d } +(Rule4) = λ%arg0 match %arg0 { CtrA: λx x; CtrB: %arg0.x } -(Rule5) = λa λb (match a { (CtrA1 c): λd (c d); (CtrA2 e f): λg (e f g); (CtrA3 h): λi (match i { (CtrB0): λj (CtrA3 j); (CtrB1 l): λm (CtrA3 m l); (CtrB2 n): λo (CtrA3 o (CtrB2 n)); (CtrB3 p): λq (q p) } h) } b) +(Rule5) = λ%arg0 λ%arg1 (match %arg0 { CtrA1: λ%arg1 (%arg0.a %arg1); CtrA2: λ%arg1 (%arg0.a1 %arg0.a2 %arg1); CtrA3: λ%arg1 (match %arg1 { CtrB0: λ%arg0.a (CtrA3 %arg0.a); CtrB1: λ%arg0.a (CtrA3 %arg0.a %arg1.b); CtrB2: λ%arg0.a (CtrA3 %arg0.a (CtrB2 %arg1.b)); CtrB3: λ%arg0.a (%arg0.a %arg1.b) } %arg0.a) } %arg1) -(Rule6) = λa a +(Rule6) = λ%arg0 %arg0 -(CtrA) = #Foo λa #Foo λ* a +(CtrA) = #Foo λCtrA #Foo λCtrB CtrA -(CtrB) = λa #Foo λ* #Foo λc #Foo (c a) +(CtrB) = λx #Foo λCtrA #Foo λCtrB #Foo (CtrB x) -(CtrA1) = λa #Bar λb #Bar λ* #Bar λ* #Bar (b a) +(CtrA1) = λa #Bar λCtrA1 #Bar λCtrA2 #Bar λCtrA3 #Bar (CtrA1 a) -(CtrA2) = λa λb #Bar λ* #Bar λd #Bar λ* #Bar (d a b) +(CtrA2) = λa1 λa2 #Bar λCtrA1 #Bar λCtrA2 #Bar λCtrA3 #Bar (CtrA2 a1 a2) -(CtrA3) = λa #Bar λ* #Bar λ* #Bar λd #Bar (d a) +(CtrA3) = λa #Bar λCtrA1 #Bar λCtrA2 #Bar λCtrA3 #Bar (CtrA3 a) -(CtrB0) = #Baz λa #Baz λ* #Baz λ* #Baz λ* a +(CtrB0) = #Baz λCtrB0 #Baz λCtrB1 #Baz λCtrB2 #Baz λCtrB3 CtrB0 -(CtrB1) = λa #Baz λ* #Baz λc #Baz λ* #Baz λ* #Baz (c a) +(CtrB1) = λb #Baz λCtrB0 #Baz λCtrB1 #Baz λCtrB2 #Baz λCtrB3 #Baz (CtrB1 b) -(CtrB2) = λa #Baz λ* #Baz λ* #Baz λd #Baz λ* #Baz (d a) +(CtrB2) = λb #Baz λCtrB0 #Baz λCtrB1 #Baz λCtrB2 #Baz λCtrB3 #Baz (CtrB2 b) -(CtrB3) = λa #Baz λ* #Baz λ* #Baz λ* #Baz λe #Baz (e a) +(CtrB3) = λb #Baz λCtrB0 #Baz λCtrB1 #Baz λCtrB2 #Baz λCtrB3 #Baz (CtrB3 b) diff --git a/tests/snapshots/simplify_matches__bits_dec.hvm.snap b/tests/snapshots/simplify_matches__bits_dec.hvm.snap index a55750e2..abfa7927 100644 --- a/tests/snapshots/simplify_matches__bits_dec.hvm.snap +++ b/tests/snapshots/simplify_matches__bits_dec.hvm.snap @@ -2,10 +2,10 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/bits_dec.hvm --- -(Data.Bits.dec) = λa match a { (Data.Bits.e): Data.Bits.e; (Data.Bits.o c): match c { (Data.Bits.e): Data.Bits.e; (Data.Bits.o e): (Data.Bits.i (Data.Bits.dec e)); (Data.Bits.i f): (Data.Bits.i (Data.Bits.dec f)) }; (Data.Bits.i g): match g { (Data.Bits.e): (Data.Bits.o Data.Bits.e); (Data.Bits.o i): (Data.Bits.o i); (Data.Bits.i j): (Data.Bits.o j) } } +(Data.Bits.dec) = λ%arg0 match %arg0 { Data.Bits.e: Data.Bits.e; Data.Bits.o: match %arg0.t { Data.Bits.e: Data.Bits.e; Data.Bits.o: (Data.Bits.i (Data.Bits.dec %arg0.t.t)); Data.Bits.i: (Data.Bits.i (Data.Bits.dec %arg0.t.t)) }; Data.Bits.i: match %arg0.t { Data.Bits.e: (Data.Bits.o Data.Bits.e); Data.Bits.o: (Data.Bits.o %arg0.t.t); Data.Bits.i: (Data.Bits.o %arg0.t.t) } } -(Data.Bits.e) = #Data.Bits λa #Data.Bits λ* #Data.Bits λ* a +(Data.Bits.e) = #Data.Bits λData.Bits.e #Data.Bits λData.Bits.o #Data.Bits λData.Bits.i Data.Bits.e -(Data.Bits.o) = λa #Data.Bits λ* #Data.Bits λc #Data.Bits λ* #Data.Bits (c a) +(Data.Bits.o) = λt #Data.Bits λData.Bits.e #Data.Bits λData.Bits.o #Data.Bits λData.Bits.i #Data.Bits (Data.Bits.o t) -(Data.Bits.i) = λa #Data.Bits λ* #Data.Bits λ* #Data.Bits λd #Data.Bits (d a) +(Data.Bits.i) = λt #Data.Bits λData.Bits.e #Data.Bits λData.Bits.o #Data.Bits λData.Bits.i #Data.Bits (Data.Bits.i t) diff --git a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap index 8162ac24..f90e03a2 100644 --- a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap +++ b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap @@ -2,8 +2,8 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/double_unwrap_box.hvm --- -(DoubleUnbox) = λa λ* match a { (Box c): match c { (Box d): d } } +(DoubleUnbox) = λ%arg0 λ%arg1 match %arg0 { Box: match %arg0.x { Box: %arg0.x.x } } (Main) = (DoubleUnbox (Box (Box 0)) 5) -(Box) = λa #Boxed λb #Boxed (b a) +(Box) = λx #Boxed λBox #Boxed (Box x) diff --git a/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap b/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap index f652b843..4c61e3aa 100644 --- a/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap +++ b/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap @@ -2,10 +2,10 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/double_unwrap_maybe.hvm --- -(DoubleUnwrap) = λa λb (match a { (Some c): λd (match c { (Some e): λ* e; (None): λg g } d); (None): λi i } b) +(DoubleUnwrap) = λ%arg0 λ%arg1 (match %arg0 { Some: λ%arg1 (match %arg0.x { Some: λ%arg1 %arg0.x.x; None: λ%arg1 %arg1 } %arg1); None: λ%arg1 %arg1 } %arg1) (Main) = (DoubleUnwrap (Some None) 5) -(Some) = λa #Maybe λb #Maybe λ* #Maybe (b a) +(Some) = λx #Maybe λSome #Maybe λNone #Maybe (Some x) -(None) = #Maybe λ* #Maybe λb b +(None) = #Maybe λSome #Maybe λNone None diff --git a/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap b/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap index e4b9d1c7..fb192341 100644 --- a/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap +++ b/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap @@ -2,10 +2,10 @@ 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) = λ%arg0 λ%arg1 (switch %arg0 { 0: λ%arg1 match %arg1 { A: match %arg1.b { B: B } }; _: λ%arg1 * } %arg1) (main) = (Foo 2 (A B)) -(A) = λa #A_t λb #A_t (b a) +(A) = λb #A_t λA #A_t (A b) -(B) = #B_t λa a +(B) = #B_t λB B diff --git a/tests/snapshots/simplify_matches__match_str.hvm.snap b/tests/snapshots/simplify_matches__match_str.hvm.snap index 12f4c553..d24852e0 100644 --- a/tests/snapshots/simplify_matches__match_str.hvm.snap +++ b/tests/snapshots/simplify_matches__match_str.hvm.snap @@ -2,6 +2,6 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/match_str.hvm --- -(is_as) = λa match a { (String.cons b c): (match b { 65: λd match d { (String.cons f g): (match f { 115: λh match h { (String.cons * *): 0; (String.nil): 2 }; *: λ* 0 } g); (String.nil): 0 }; 97: λp match p { (String.cons r s): (match r { 115: λt match t { (String.cons * *): 0; (String.nil): 2 }; *: λ* 0 } s); (String.nil): 0 }; *: λ* 0 } c); (String.nil): 1 } +(is_as) = λ%arg0 match %arg0 { String.cons: let %arg0.head%matched = (- %arg0.head 65); (switch %arg0.head%matched { 0: λ%arg0.tail match %arg0.tail { String.cons: let %arg0.tail.head%matched = (- %arg0.tail.head 115); (switch %arg0.tail.head%matched { 0: λ%arg0.tail.tail match %arg0.tail.tail { String.cons: 0; String.nil: 2 }; _: λ%arg0.tail.tail 0 } %arg0.tail.tail); String.nil: 0 }; _: λ%arg0.tail let %arg0.head%matched = (- %arg0.head%matched-1 31); (switch %arg0.head%matched { 0: λ%arg0.tail match %arg0.tail { String.cons: let %arg0.tail.head%matched = (- %arg0.tail.head 115); (switch %arg0.tail.head%matched { 0: λ%arg0.tail.tail match %arg0.tail.tail { String.cons: 0; String.nil: 2 }; _: λ%arg0.tail.tail 0 } %arg0.tail.tail); String.nil: 0 }; _: λ%arg0.tail 0 } %arg0.tail) } %arg0.tail); String.nil: 1 } (main) = * diff --git a/tests/snapshots/simplify_matches__nested.hvm.snap b/tests/snapshots/simplify_matches__nested.hvm.snap index 35d5439d..f2f8977e 100644 --- a/tests/snapshots/simplify_matches__nested.hvm.snap +++ b/tests/snapshots/simplify_matches__nested.hvm.snap @@ -2,14 +2,14 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/nested.hvm --- -(Rule) = λa match a { (CtrA b c): (match c { (CtrB1 d): λe (e d); (CtrB2 f g): λh (match f { (CtrC): λi λj (i j) } h g) } b); (CtrB l): l } +(Rule) = λ%arg0 match %arg0 { CtrA: (match %arg0.b { CtrB1: λ%arg0.a (%arg0.a %arg0.b.b); CtrB2: λ%arg0.a (match %arg0.b.a { CtrC: λ%arg0.a λ%arg0.b.b (%arg0.a %arg0.b.b) } %arg0.a %arg0.b.b) } %arg0.a); CtrB: %arg0.a } -(CtrA) = λa λb #Foo λc #Foo λ* #Foo (c a b) +(CtrA) = λa λb #Foo λCtrA #Foo λCtrB #Foo (CtrA a b) -(CtrB) = λa #Foo λ* #Foo λc #Foo (c a) +(CtrB) = λa #Foo λCtrA #Foo λCtrB #Foo (CtrB a) -(CtrB1) = λa #Bar λb #Bar λ* #Bar (b a) +(CtrB1) = λb #Bar λCtrB1 #Bar λCtrB2 #Bar (CtrB1 b) -(CtrB2) = λa λb #Bar λ* #Bar λd #Bar (d a b) +(CtrB2) = λa λb #Bar λCtrB1 #Bar λCtrB2 #Bar (CtrB2 a b) -(CtrC) = #Baz λa a +(CtrC) = #Baz λCtrC CtrC diff --git a/tests/snapshots/simplify_matches__nested2.hvm.snap b/tests/snapshots/simplify_matches__nested2.hvm.snap index 73c35073..a6e1410c 100644 --- a/tests/snapshots/simplify_matches__nested2.hvm.snap +++ b/tests/snapshots/simplify_matches__nested2.hvm.snap @@ -2,8 +2,8 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/nested2.hvm --- -(Foo) = λa λb (match b { (List.cons c d): λe (match d { (List.cons f g): λh λi (h i f g); (List.nil): λj λk (j (List.cons k List.nil)) } e c); (List.nil): λm (m List.nil) } a) +(Foo) = λ%arg0 λ%arg1 (match %arg1 { List.cons: λ%arg0 (match %arg1.tail { List.cons: λ%arg0 λ%arg1.head (%arg0 %arg1.head %arg1.tail.head %arg1.tail.tail); List.nil: λ%arg0 λ%arg1.head (%arg0 (List.cons %arg1.head List.nil)) } %arg0 %arg1.head); List.nil: λ%arg0 (%arg0 List.nil) } %arg0) -(List.cons) = λa λb #List λc #List λ* #List (c a b) +(List.cons) = λhead λtail #List λList.cons #List λList.nil #List (List.cons head tail) -(List.nil) = #List λ* #List λb b +(List.nil) = #List λList.cons #List λList.nil List.nil diff --git a/tests/snapshots/simplify_matches__nested_0ary.hvm.snap b/tests/snapshots/simplify_matches__nested_0ary.hvm.snap index 8cbee279..29a71677 100644 --- a/tests/snapshots/simplify_matches__nested_0ary.hvm.snap +++ b/tests/snapshots/simplify_matches__nested_0ary.hvm.snap @@ -2,8 +2,8 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/nested_0ary.hvm --- -(Unpack) = λa λb (match b { (Cons c d): λe (match d { (Cons f g): λh λi (h (Cons i (Cons f g))); (Nil): λ* λk k } e c); (Nil): λ* Nil } a) +(Unpack) = λ%arg0 λ%arg1 (match %arg1 { Cons: λ%arg0 (match %arg1.tail { Cons: λ%arg0 λ%arg1.head (%arg0 (Cons %arg1.head (Cons %arg1.tail.head %arg1.tail.tail))); Nil: λ%arg0 λ%arg1.head %arg1.head } %arg0 %arg1.head); Nil: λ%arg0 Nil } %arg0) -(Cons) = λa λb #list λc #list λ* #list (c a b) +(Cons) = λhead λtail #list λCons #list λNil #list (Cons head tail) -(Nil) = #list λ* #list λb b +(Nil) = #list λCons #list λNil Nil diff --git a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap index e7c9c75b..6c568921 100644 --- a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap +++ b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap @@ -2,6 +2,6 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/simplify_matches/redundant_with_era.hvm --- -(Fn2) = λa λb (match a { 0: λc match c { (*, f): match f { (*, h): h } }; 1+*: λj match j { (*, l): match l { (*, n): n } } } b) +(Fn2) = λ%arg0 λ%arg1 (switch %arg0 { 0: λ%arg1 let (%arg1.0, %arg1.1) = %arg1; let (%arg1.1.0, %arg1.1.1) = %arg1.1; %arg1.1.1; _: λ%arg1 let (%arg1.0, %arg1.1) = %arg1; let (%arg1.1.0, %arg1.1.1) = %arg1.1; %arg1.1.1 } %arg1) (main) = *