mirror of
https://github.com/HigherOrderCO/Bend.git
synced 2024-09-11 11:56:54 +03:00
[sc-403] Change pat-match algorithm, add multi-arg matches
This commit is contained in:
parent
1876c8d6b3
commit
45447b4d51
65
Cargo.lock
generated
65
Cargo.lock
generated
@ -4,9 +4,9 @@ version = 3
|
||||
|
||||
[[package]]
|
||||
name = "ahash"
|
||||
version = "0.8.8"
|
||||
version = "0.8.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "42cd52102d3df161c77a887b608d7a4897d7cc112886a9537b738a887a03aaff"
|
||||
checksum = "d713b3834d76b85304d4d525563c1276e2e30dc97cc67bfb4585a4a29fc2c89f"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"once_cell",
|
||||
@ -16,9 +16,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "anstream"
|
||||
version = "0.6.11"
|
||||
version = "0.6.12"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6e2e1ebcb11de5c03c67de28a7df593d32191b44939c482e97702baaaa6ab6a5"
|
||||
checksum = "96b09b5178381e0874812a9b157f7fe84982617e48f71f4e3235482775e5b540"
|
||||
dependencies = [
|
||||
"anstyle",
|
||||
"anstyle-parse",
|
||||
@ -70,12 +70,9 @@ checksum = "3a8241f3ebb85c056b509d4327ad0358fbbba6ffb340bf388f26350aeda225b1"
|
||||
|
||||
[[package]]
|
||||
name = "cc"
|
||||
version = "1.0.83"
|
||||
version = "1.0.86"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0"
|
||||
dependencies = [
|
||||
"libc",
|
||||
]
|
||||
checksum = "7f9fa1897e4325be0d68d48df6aa1a71ac2ed4d27723887e7754192705350730"
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
@ -95,9 +92,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "4.5.0"
|
||||
version = "4.5.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "80c21025abd42669a92efc996ef13cfb2c5c627858421ea58d5c3b331a6c134f"
|
||||
checksum = "c918d541ef2913577a0f9566e9ce27cb35b6df072075769e0b26cb5a554520da"
|
||||
dependencies = [
|
||||
"clap_builder",
|
||||
"clap_derive",
|
||||
@ -105,9 +102,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "clap_builder"
|
||||
version = "4.5.0"
|
||||
version = "4.5.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "458bf1f341769dfcf849846f65dffdf9146daa56bcd2a47cb4e1de9915567c99"
|
||||
checksum = "9f3e7391dad68afb0c2ede1bf619f579a3dc9c2ec67f089baa397123a2f3d1eb"
|
||||
dependencies = [
|
||||
"anstream",
|
||||
"anstyle",
|
||||
@ -205,7 +202,7 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
|
||||
[[package]]
|
||||
name = "hvm-core"
|
||||
version = "0.2.19"
|
||||
source = "git+https://github.com/HigherOrderCO/hvm-core#9bdbdcbe0816345545a3adf00704f9f4f01dcfe7"
|
||||
source = "git+https://github.com/HigherOrderCO/hvm-core#c1f123210d1e918dfce12060c7f4b57b602bb02c"
|
||||
dependencies = [
|
||||
"nohash-hasher",
|
||||
]
|
||||
@ -239,9 +236,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "insta"
|
||||
version = "1.34.0"
|
||||
version = "1.35.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5d64600be34b2fcfc267740a243fa7744441bb4947a619ac4e5bb6507f35fbfc"
|
||||
checksum = "7c985c1bef99cf13c58fade470483d81a2bfe846ebde60ed28cc2dddec2df9e2"
|
||||
dependencies = [
|
||||
"console",
|
||||
"lazy_static",
|
||||
@ -403,9 +400,9 @@ checksum = "5ee073c9e4cd00e28217186dbe12796d692868f432bf2e97ee73bed0c56dfa01"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "2.0.48"
|
||||
version = "2.0.50"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0f3531638e407dfc0814761abb7c00a5b54992b849452a0646b7f65c9f770f3f"
|
||||
checksum = "74f1bdc9872430ce9b75da68329d1c1746faf50ffac5f19e02b71e37ff881ffb"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
@ -482,9 +479,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "windows-targets"
|
||||
version = "0.52.0"
|
||||
version = "0.52.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8a18201040b24831fbb9e4eb208f8892e1f50a37feb53cc7ff887feb8f50e7cd"
|
||||
checksum = "d380ba1dc7187569a8a9e91ed34b8ccfc33123bbacb8c0aed2d1ad7f3ef2dc5f"
|
||||
dependencies = [
|
||||
"windows_aarch64_gnullvm",
|
||||
"windows_aarch64_msvc",
|
||||
@ -497,45 +494,45 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_gnullvm"
|
||||
version = "0.52.0"
|
||||
version = "0.52.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cb7764e35d4db8a7921e09562a0304bf2f93e0a51bfccee0bd0bb0b666b015ea"
|
||||
checksum = "68e5dcfb9413f53afd9c8f86e56a7b4d86d9a2fa26090ea2dc9e40fba56c6ec6"
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_msvc"
|
||||
version = "0.52.0"
|
||||
version = "0.52.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "bbaa0368d4f1d2aaefc55b6fcfee13f41544ddf36801e793edbbfd7d7df075ef"
|
||||
checksum = "8dab469ebbc45798319e69eebf92308e541ce46760b49b18c6b3fe5e8965b30f"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_gnu"
|
||||
version = "0.52.0"
|
||||
version = "0.52.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a28637cb1fa3560a16915793afb20081aba2c92ee8af57b4d5f28e4b3e7df313"
|
||||
checksum = "2a4e9b6a7cac734a8b4138a4e1044eac3404d8326b6c0f939276560687a033fb"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_msvc"
|
||||
version = "0.52.0"
|
||||
version = "0.52.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ffe5e8e31046ce6230cc7215707b816e339ff4d4d67c65dffa206fd0f7aa7b9a"
|
||||
checksum = "28b0ec9c422ca95ff34a78755cfa6ad4a51371da2a5ace67500cf7ca5f232c58"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnu"
|
||||
version = "0.52.0"
|
||||
version = "0.52.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3d6fa32db2bc4a2f5abeacf2b69f7992cd09dca97498da74a151a3132c26befd"
|
||||
checksum = "704131571ba93e89d7cd43482277d6632589b18ecf4468f591fbae0a8b101614"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnullvm"
|
||||
version = "0.52.0"
|
||||
version = "0.52.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1a657e1e9d3f514745a572a6846d3c7aa7dbe1658c056ed9c3344c4109a6949e"
|
||||
checksum = "42079295511643151e98d61c38c0acc444e52dd42ab456f7ccfd5152e8ecf21c"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_msvc"
|
||||
version = "0.52.0"
|
||||
version = "0.52.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04"
|
||||
checksum = "0770833d60a970638e989b3fa9fd2bb1aaadcf88963d1659fd7d9990196ed2d6"
|
||||
|
||||
[[package]]
|
||||
name = "yaml-rust"
|
||||
|
@ -21,10 +21,10 @@ cli = ["dep:clap"]
|
||||
|
||||
[dependencies]
|
||||
# Later versions of the alpha contains bugs that changes the parser errors
|
||||
chumsky = { version = "= 1.0.0-alpha.4", features = ["label"]}
|
||||
chumsky = { version = "= 1.0.0-alpha.4", features = ["label"] }
|
||||
clap = { version = "4.4.1", features = ["derive"], optional = true }
|
||||
highlight_error = "0.1.1"
|
||||
hvm-core = { git = "https://github.com/HigherOrderCO/hvm-core" }
|
||||
hvm-core = { git = "https://github.com/HigherOrderCO/hvm-core" }
|
||||
indexmap = "2.2.3"
|
||||
interner = "0.2.1"
|
||||
itertools = "0.11.0"
|
||||
|
@ -1,12 +1,11 @@
|
||||
use crate::term::{
|
||||
check::{
|
||||
ctrs_arities::ArityErr, exhaustiveness::ExhaustivenessErr, set_entrypoint::EntryErr,
|
||||
shared_names::TopLevelErr, type_check::InferErr, unbound_pats::UnboundCtrErr,
|
||||
set_entrypoint::EntryErr, shared_names::TopLevelErr, unbound_pats::UnboundCtrErr,
|
||||
unbound_vars::UnboundVarErr,
|
||||
},
|
||||
display::DisplayFn,
|
||||
transform::{
|
||||
extract_adt_matches::MatchErr, resolve_refs::ReferencedMainErr, simplify_ref_to_ref::CyclicDefErr,
|
||||
encode_pattern_matching::MatchErr, resolve_refs::ReferencedMainErr, simplify_ref_to_ref::CyclicDefErr,
|
||||
},
|
||||
Name,
|
||||
};
|
||||
@ -67,7 +66,7 @@ impl Info {
|
||||
if self.err_counter == 0 { Ok(t) } else { Err(std::mem::take(self)) }
|
||||
}
|
||||
|
||||
pub fn display<'a>(&'a self, verbose: bool) -> impl Display + 'a {
|
||||
pub fn display(&self, verbose: bool) -> impl Display + '_ {
|
||||
DisplayFn(move |f| {
|
||||
write!(f, "{}", self.errs.iter().map(|err| err.display(verbose)).join("\n"))?;
|
||||
|
||||
@ -103,13 +102,10 @@ impl From<&str> for Info {
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum Error {
|
||||
Exhaustiveness(ExhaustivenessErr),
|
||||
MainRef(ReferencedMainErr),
|
||||
AdtMatch(MatchErr),
|
||||
Match(MatchErr),
|
||||
UnboundVar(UnboundVarErr),
|
||||
UnboundCtr(UnboundCtrErr),
|
||||
Infer(InferErr),
|
||||
Arity(ArityErr),
|
||||
Cyclic(CyclicDefErr),
|
||||
EntryPoint(EntryErr),
|
||||
TopLevel(TopLevelErr),
|
||||
@ -125,14 +121,10 @@ impl Display for Error {
|
||||
impl Error {
|
||||
pub fn display(&self, verbose: bool) -> impl Display + '_ {
|
||||
DisplayFn(move |f| match self {
|
||||
Error::Exhaustiveness(err) if verbose => write!(f, "{}", err.display_with_limit(usize::MAX)),
|
||||
Error::Exhaustiveness(err) => write!(f, "{err}"),
|
||||
Error::AdtMatch(err) => write!(f, "{err}"),
|
||||
Error::Match(err) => write!(f, "{}", err.display(verbose)),
|
||||
Error::UnboundVar(err) => write!(f, "{err}"),
|
||||
Error::UnboundCtr(err) => write!(f, "{err}"),
|
||||
Error::MainRef(err) => write!(f, "{err}"),
|
||||
Error::Infer(err) => write!(f, "{err}"),
|
||||
Error::Arity(err) => write!(f, "{err}"),
|
||||
Error::Cyclic(err) => write!(f, "{err}"),
|
||||
Error::EntryPoint(err) => write!(f, "{err}"),
|
||||
Error::TopLevel(err) => write!(f, "{err}"),
|
||||
@ -141,12 +133,6 @@ impl Error {
|
||||
}
|
||||
}
|
||||
|
||||
impl From<ExhaustivenessErr> for Error {
|
||||
fn from(value: ExhaustivenessErr) -> Self {
|
||||
Self::Exhaustiveness(value)
|
||||
}
|
||||
}
|
||||
|
||||
impl From<ReferencedMainErr> for Error {
|
||||
fn from(value: ReferencedMainErr) -> Self {
|
||||
Self::MainRef(value)
|
||||
@ -155,7 +141,7 @@ impl From<ReferencedMainErr> for Error {
|
||||
|
||||
impl From<MatchErr> for Error {
|
||||
fn from(value: MatchErr) -> Self {
|
||||
Self::AdtMatch(value)
|
||||
Self::Match(value)
|
||||
}
|
||||
}
|
||||
|
||||
@ -171,18 +157,6 @@ impl From<UnboundCtrErr> for Error {
|
||||
}
|
||||
}
|
||||
|
||||
impl From<InferErr> for Error {
|
||||
fn from(value: InferErr) -> Self {
|
||||
Self::Infer(value)
|
||||
}
|
||||
}
|
||||
|
||||
impl From<ArityErr> for Error {
|
||||
fn from(value: ArityErr) -> Self {
|
||||
Self::Arity(value)
|
||||
}
|
||||
}
|
||||
|
||||
impl From<CyclicDefErr> for Error {
|
||||
fn from(value: CyclicDefErr) -> Self {
|
||||
Self::Cyclic(value)
|
||||
|
@ -64,7 +64,7 @@ pub fn pre_reduce_book(book: &mut Book, entrypoint: &str) -> Result<(), String>
|
||||
}
|
||||
// Place the reduced net back into the def map
|
||||
dispatch_dyn_net!(&mut rt => {
|
||||
*net = host.readback(&rt);
|
||||
*net = host.readback(rt);
|
||||
});
|
||||
}
|
||||
Ok(())
|
||||
|
130
src/lib.rs
130
src/lib.rs
@ -3,7 +3,7 @@
|
||||
|
||||
use diagnostics::{Info, Warning};
|
||||
use hvmc::{
|
||||
ast::{Net, self},
|
||||
ast::{self, Net},
|
||||
dispatch_dyn_net,
|
||||
host::Host,
|
||||
run::{DynNet, Net as RtNet, Rewrites},
|
||||
@ -12,10 +12,16 @@ use hvmc::{
|
||||
use hvmc_net::{pre_reduce::pre_reduce_book, prune::prune_defs};
|
||||
use net::{hvmc_to_net::hvmc_to_net, net_to_hvmc::nets_to_hvmc};
|
||||
use std::{
|
||||
str::FromStr, sync::{Arc, Mutex}, time::Instant
|
||||
str::FromStr,
|
||||
sync::{Arc, Mutex},
|
||||
time::Instant,
|
||||
};
|
||||
use term::{
|
||||
book_to_nets, display::{display_readback_errors, DisplayJoin}, net_to_term::net_to_term, term_to_net::Labels, AdtEncoding, Book, Ctx, ReadbackError, Term
|
||||
book_to_nets,
|
||||
display::{display_readback_errors, DisplayJoin},
|
||||
net_to_term::net_to_term,
|
||||
term_to_net::Labels,
|
||||
AdtEncoding, Book, Ctx, ReadbackError, Term,
|
||||
};
|
||||
|
||||
pub mod diagnostics;
|
||||
@ -28,12 +34,12 @@ pub use term::load_book::load_file_to_book;
|
||||
pub const ENTRY_POINT: &str = "main";
|
||||
pub const HVM1_ENTRY_POINT: &str = "Main";
|
||||
|
||||
/// These are the names of builtin defs that are not in the hvm-lang book, but
|
||||
/// These are the names of builtin defs that are not in the hvm-lang book, but
|
||||
/// are present in the hvm-core book. They are implemented using Rust code by
|
||||
/// [`create_host`] and they can not be rewritten as hvm-lang functions.
|
||||
pub const CORE_BUILTINS: [&str; 2] = ["HVM.log", "HVM.black_box"];
|
||||
|
||||
/// Creates a host with the hvm-core pŕimitive definitions built-in.
|
||||
/// Creates a host with the hvm-core primitive definitions built-in.
|
||||
/// This needs the book as an Arc because the closure that logs
|
||||
/// data needs access to the book.
|
||||
pub fn create_host(hvml_book: Arc<Book>, labels: Arc<Labels>, compile_opts: CompileOpts) -> Arc<Mutex<Host>> {
|
||||
@ -69,7 +75,7 @@ pub fn check_book(book: &mut Book) -> Result<(), Info> {
|
||||
|
||||
pub fn compile_book(book: &mut Book, opts: CompileOpts) -> Result<CompileResult, Info> {
|
||||
let warns = desugar_book(book, opts)?;
|
||||
let (nets, labels) = book_to_nets(&book);
|
||||
let (nets, labels) = book_to_nets(book);
|
||||
let mut core_book = nets_to_hvmc(nets)?;
|
||||
if opts.pre_reduce {
|
||||
pre_reduce_book(&mut core_book, book.hvmc_entrypoint())?;
|
||||
@ -83,19 +89,43 @@ pub fn compile_book(book: &mut Book, opts: CompileOpts) -> Result<CompileResult,
|
||||
pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result<Vec<Warning>, Info> {
|
||||
let mut ctx = Ctx::new(book);
|
||||
|
||||
ctx.set_entrypoint();
|
||||
ctx.check_shared_names();
|
||||
ctx.set_entrypoint();
|
||||
|
||||
ctx.book.encode_adts(opts.adt_encoding);
|
||||
ctx.book.encode_builtins();
|
||||
encode_pattern_matching(&mut ctx, opts.adt_encoding)?;
|
||||
ctx.check_unbound_vars()?; // sanity check
|
||||
ctx.normalize_native_matches()?;
|
||||
|
||||
ctx.book.resolve_ctrs_in_pats();
|
||||
ctx.resolve_refs()?;
|
||||
|
||||
ctx.check_match_arity()?;
|
||||
ctx.check_unbound_pats()?;
|
||||
|
||||
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_simple_matches`]
|
||||
ctx.check_unbound_vars()?;
|
||||
|
||||
ctx.book.convert_match_def_to_term();
|
||||
ctx.simplify_matches()?;
|
||||
ctx.linearize_simple_matches()?;
|
||||
ctx.book.encode_simple_matches(opts.adt_encoding);
|
||||
|
||||
// sanity check
|
||||
ctx.check_unbound_vars()?;
|
||||
|
||||
ctx.book.make_var_names_unique();
|
||||
ctx.book.linearize_vars();
|
||||
ctx.book.eta_reduction(opts.eta);
|
||||
ctx.check_unbound_vars()?; // sanity check
|
||||
|
||||
// sanity check
|
||||
ctx.check_unbound_vars()?;
|
||||
|
||||
// Optimizing passes
|
||||
if opts.eta {
|
||||
ctx.book.eta_reduction();
|
||||
}
|
||||
if opts.supercombinators {
|
||||
ctx.book.detach_supercombinators();
|
||||
}
|
||||
@ -118,26 +148,6 @@ pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result<Vec<Warning>,
|
||||
if !ctx.info.has_errors() { Ok(ctx.info.warns) } else { Err(ctx.info) }
|
||||
}
|
||||
|
||||
pub fn encode_pattern_matching(ctx: &mut Ctx, adt_encoding: AdtEncoding) -> Result<(), Info> {
|
||||
ctx.check_arity()?;
|
||||
ctx.book.resolve_ctrs_in_pats();
|
||||
ctx.check_unbound_pats()?;
|
||||
ctx.check_ctrs_arities()?;
|
||||
ctx.resolve_refs()?;
|
||||
ctx.book.desugar_let_destructors();
|
||||
ctx.book.desugar_implicit_match_binds();
|
||||
// This call to unbound vars needs to be after desugar_implicit_match_binds,
|
||||
// since we need the generated pattern names, like `x-1`, `ctr.field`.
|
||||
ctx.check_unbound_vars()?;
|
||||
ctx.linearize_matches()?;
|
||||
ctx.extract_adt_matches()?;
|
||||
ctx.book.flatten_rules();
|
||||
let def_types = ctx.infer_def_types()?;
|
||||
ctx.check_exhaustive_patterns(&def_types)?;
|
||||
ctx.book.encode_pattern_matching_functions(&def_types, adt_encoding);
|
||||
Ok(())
|
||||
}
|
||||
|
||||
pub fn run_book(
|
||||
mut book: Book,
|
||||
mem_size: usize,
|
||||
@ -157,10 +167,10 @@ pub fn run_book(
|
||||
|
||||
// Run
|
||||
let debug_hook = run_opts.debug_hook(&book, &labels);
|
||||
let host = create_host(book.clone(), labels.clone(), compile_opts.clone());
|
||||
let host = create_host(book.clone(), labels.clone(), compile_opts);
|
||||
host.lock().unwrap().insert_book(&core_book);
|
||||
|
||||
let (res_lnet, stats) = run_compiled(host, mem_size, run_opts, debug_hook, &book.hvmc_entrypoint());
|
||||
let (res_lnet, stats) = run_compiled(host, mem_size, run_opts, debug_hook, book.hvmc_entrypoint());
|
||||
|
||||
// Readback
|
||||
let net = hvmc_to_net(&res_lnet);
|
||||
@ -173,38 +183,36 @@ pub fn run_book(
|
||||
Ok((res_term, info))
|
||||
}
|
||||
|
||||
|
||||
/// Utility function to count the amount of nodes in an hvm-core AST net
|
||||
pub fn count_nodes<'l>(net: &'l hvmc::ast::Net) -> usize {
|
||||
let mut visit: Vec<&'l hvmc::ast::Tree> = vec![&net.root];
|
||||
let mut count = 0usize;
|
||||
for (l, r) in &net.rdex {
|
||||
visit.push(&l);
|
||||
visit.push(&r);
|
||||
visit.push(l);
|
||||
visit.push(r);
|
||||
}
|
||||
while let Some(tree) = visit.pop() {
|
||||
match tree {
|
||||
ast::Tree::Ctr { lft, rgt, .. }
|
||||
| ast::Tree::Op2 { lft, rgt, .. } => {
|
||||
count += 1;
|
||||
visit.push(lft);
|
||||
visit.push(rgt);
|
||||
},
|
||||
ast::Tree::Op1 { rgt, .. } => {
|
||||
count += 1;
|
||||
visit.push(rgt);
|
||||
},
|
||||
ast::Tree::Mat { sel, ret } => {
|
||||
count += 1;
|
||||
visit.push(sel);
|
||||
visit.push(ret);
|
||||
},
|
||||
ast::Tree::Var { .. } => (),
|
||||
_ => {
|
||||
count += 1;
|
||||
}
|
||||
ast::Tree::Ctr { lft, rgt, .. } | ast::Tree::Op2 { lft, rgt, .. } => {
|
||||
count += 1;
|
||||
visit.push(lft);
|
||||
visit.push(rgt);
|
||||
}
|
||||
ast::Tree::Op1 { rgt, .. } => {
|
||||
count += 1;
|
||||
visit.push(rgt);
|
||||
}
|
||||
ast::Tree::Mat { sel, ret } => {
|
||||
count += 1;
|
||||
visit.push(sel);
|
||||
visit.push(ret);
|
||||
}
|
||||
ast::Tree::Var { .. } => (),
|
||||
_ => {
|
||||
count += 1;
|
||||
}
|
||||
};
|
||||
};
|
||||
}
|
||||
count
|
||||
}
|
||||
|
||||
@ -228,7 +236,7 @@ pub fn run_compiled(
|
||||
if let Some(mut hook) = hook {
|
||||
root.expand();
|
||||
while !root.rdex.is_empty() {
|
||||
hook(&host.lock().unwrap().readback(&root));
|
||||
hook(&host.lock().unwrap().readback(root));
|
||||
root.reduce(1);
|
||||
root.expand();
|
||||
}
|
||||
@ -241,9 +249,9 @@ pub fn run_compiled(
|
||||
}
|
||||
root.expand();
|
||||
while !root.rdex.is_empty() {
|
||||
let old_rwts = root.rwts.total() as u64;
|
||||
let old_rwts = root.rwts.total();
|
||||
root.reduce(max_rwts);
|
||||
let delta_rwts = root.rwts.total() as u64 - old_rwts;
|
||||
let delta_rwts = root.rwts.total() - old_rwts;
|
||||
if (max_rwts as u64) < delta_rwts {
|
||||
eprintln!("Warning: Exceeded max rwts");
|
||||
break;
|
||||
@ -259,7 +267,7 @@ pub fn run_compiled(
|
||||
let elapsed = start_time.elapsed().as_secs_f64();
|
||||
|
||||
|
||||
let net = host.lock().unwrap().readback(&root);
|
||||
let net = host.lock().unwrap().readback(root);
|
||||
|
||||
// TODO I don't quite understand this code
|
||||
// How would it be implemented in the new version?
|
||||
|
@ -165,7 +165,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Info> {
|
||||
let entrypoint = cli.entrypoint.take();
|
||||
|
||||
let load_book = |path: &Path| -> Result<Book, Info> {
|
||||
let mut book = load_file_to_book(&path).map_err(Info::from)?;
|
||||
let mut book = load_file_to_book(path).map_err(Info::from)?;
|
||||
book.entrypoint = entrypoint;
|
||||
|
||||
if arg_verbose {
|
||||
|
@ -49,6 +49,7 @@ fn net_tree_to_hvmc_tree(inet: &INet, tree_root: NodeId, port_to_var_id: &mut Ha
|
||||
rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id)),
|
||||
},
|
||||
NodeKind::Con { lab: Some(lab) } => Tree::Ctr {
|
||||
#[allow(clippy::identity_op)]
|
||||
lab: (*lab as u16 + 1) << 1 | 0,
|
||||
lft: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id)),
|
||||
rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id)),
|
||||
|
@ -47,11 +47,15 @@ impl Term {
|
||||
fst.encode_builtins();
|
||||
snd.encode_builtins();
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.encode_builtins();
|
||||
for (pat, arm) in arms {
|
||||
pat.encode_builtins();
|
||||
arm.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::Var { .. } | Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Era | Term::Err => {}
|
||||
@ -86,6 +90,7 @@ impl Pattern {
|
||||
snd.encode_builtins();
|
||||
}
|
||||
Pattern::Var(..) | Pattern::Num(..) => {}
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1,20 +1,11 @@
|
||||
use std::{collections::HashMap, fmt::Display};
|
||||
use std::collections::HashMap;
|
||||
|
||||
use crate::{
|
||||
diagnostics::Info,
|
||||
term::{Book, Ctx, Name, Pattern},
|
||||
term::{transform::encode_pattern_matching::MatchErr, Book, Ctx, Name, Pattern, Term},
|
||||
};
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct ArityErr(Name, usize, usize);
|
||||
|
||||
impl Display for ArityErr {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Arity error. Constructor '{}' expects {} fields, found {}.", self.0, self.1, self.2)
|
||||
}
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
impl Ctx<'_> {
|
||||
/// Checks if every constructor pattern of every definition rule has the same arity from the
|
||||
/// defined adt constructor.
|
||||
///
|
||||
@ -26,9 +17,11 @@ impl<'book> Ctx<'book> {
|
||||
for (def_name, def) in self.book.defs.iter() {
|
||||
for rule in def.rules.iter() {
|
||||
for pat in rule.pats.iter() {
|
||||
let res = pat.check(&arities);
|
||||
self.info.take_err(res, Some(&def_name));
|
||||
let res = pat.check_ctrs_arities(&arities);
|
||||
self.info.take_err(res, Some(def_name));
|
||||
}
|
||||
let res = rule.body.check_ctrs_arities(&arities);
|
||||
self.info.take_err(res, Some(def_name));
|
||||
}
|
||||
}
|
||||
|
||||
@ -52,16 +45,16 @@ impl Book {
|
||||
}
|
||||
|
||||
impl Pattern {
|
||||
fn check(&self, arities: &HashMap<Name, usize>) -> Result<(), ArityErr> {
|
||||
fn check_ctrs_arities(&self, arities: &HashMap<Name, usize>) -> Result<(), MatchErr> {
|
||||
let mut to_check = vec![self];
|
||||
|
||||
while let Some(pat) = to_check.pop() {
|
||||
match pat {
|
||||
Pattern::Ctr(name, args) => {
|
||||
let arity = arities.get(name).unwrap();
|
||||
let args = args.len();
|
||||
if *arity != args {
|
||||
return Err(ArityErr(name.clone(), *arity, args));
|
||||
let expected = arities.get(name).unwrap();
|
||||
let found = args.len();
|
||||
if *expected != found {
|
||||
return Err(MatchErr::CtrArityMismatch(name.clone(), found, *expected));
|
||||
}
|
||||
}
|
||||
Pattern::Tup(fst, snd) => {
|
||||
@ -74,8 +67,55 @@ impl Pattern {
|
||||
}
|
||||
}
|
||||
Pattern::Var(..) | Pattern::Num(..) => {}
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Term {
|
||||
pub fn check_ctrs_arities(&self, arities: &HashMap<Name, usize>) -> Result<(), MatchErr> {
|
||||
match self {
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.check_ctrs_arities(arities)?;
|
||||
}
|
||||
for rule in rules {
|
||||
for pat in &rule.pats {
|
||||
pat.check_ctrs_arities(arities)?;
|
||||
}
|
||||
rule.body.check_ctrs_arities(arities)?;
|
||||
}
|
||||
}
|
||||
Term::Let { pat, val, nxt } => {
|
||||
pat.check_ctrs_arities(arities)?;
|
||||
val.check_ctrs_arities(arities)?;
|
||||
nxt.check_ctrs_arities(arities)?;
|
||||
}
|
||||
|
||||
Term::Lst { els } => {
|
||||
for el in els {
|
||||
el.check_ctrs_arities(arities)?;
|
||||
}
|
||||
}
|
||||
Term::App { fun: fst, arg: snd, .. }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. } => {
|
||||
fst.check_ctrs_arities(arities)?;
|
||||
snd.check_ctrs_arities(arities)?;
|
||||
}
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.check_ctrs_arities(arities)?,
|
||||
Term::Var { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Str { .. }
|
||||
| Term::Ref { .. }
|
||||
| Term::Era
|
||||
| Term::Err => {}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
@ -1,152 +0,0 @@
|
||||
use super::type_check::DefinitionTypes;
|
||||
use crate::{
|
||||
diagnostics::{Info, ERR_INDENT_SIZE},
|
||||
term::{Adt, Ctx, MatchNum, Name, Pattern, Rule, Type},
|
||||
};
|
||||
use indexmap::IndexMap;
|
||||
use itertools::Itertools;
|
||||
use std::fmt::Display;
|
||||
|
||||
const PATTERN_ERROR_LIMIT: usize = 5;
|
||||
const ERROR_LIMIT_HINT: &str = "Use the --verbose option to see all cases.";
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct ExhaustivenessErr(Name, Vec<String>);
|
||||
|
||||
impl ExhaustivenessErr {
|
||||
pub fn display_with_limit(&self, limit: usize) -> String {
|
||||
let ident = ERR_INDENT_SIZE * 2;
|
||||
let hints =
|
||||
self.1.iter().take(limit).map(|pat| format!("{:ident$}({} {pat}) not covered.", "", self.0)).join("\n");
|
||||
|
||||
let mut str = format!("Non-exhaustive pattern. Hint:\n{}", hints);
|
||||
|
||||
let len = self.1.len();
|
||||
if len > limit {
|
||||
str.push_str(&format!(" ... and {} others.\n{:ident$}{}", len - limit, "", ERROR_LIMIT_HINT))
|
||||
}
|
||||
|
||||
str
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for ExhaustivenessErr {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "{}", self.display_with_limit(PATTERN_ERROR_LIMIT))
|
||||
}
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
/// For each pattern-matching definition, check that any given value will match at least one of the rules.
|
||||
/// We assume that all patterns have been type checked already.
|
||||
pub fn check_exhaustive_patterns(&mut self, def_types: &DefinitionTypes) -> Result<(), Info> {
|
||||
self.info.start_pass();
|
||||
|
||||
for (def_name, def) in &self.book.defs {
|
||||
let types = &def_types[def_name];
|
||||
let rules_to_check = (0 .. def.rules.len()).collect();
|
||||
let res = check_pattern(&[], &self.book.adts, &def.rules, types, rules_to_check, def_name);
|
||||
self.info.take_err(res, Some(&def_name));
|
||||
}
|
||||
|
||||
self.info.fatal(())
|
||||
}
|
||||
}
|
||||
|
||||
fn check_pattern(
|
||||
match_path: &[Name],
|
||||
adts: &IndexMap<Name, Adt>,
|
||||
rules: &[Rule],
|
||||
types: &[Type],
|
||||
rules_to_check: Vec<usize>,
|
||||
def_name: &Name,
|
||||
) -> Result<(), ExhaustivenessErr> {
|
||||
let mut missings = Vec::new();
|
||||
|
||||
if let Some(pat_type) = types.first() {
|
||||
// For each constructor of the pattern, which rules match with it.
|
||||
// If no rules match a given constructor, the pattern is non-exhaustive.
|
||||
// TODO: Should check if it's a constructor type and use Pattern::is_flat_subset_of.
|
||||
let rules_matching_ctrs = match pat_type {
|
||||
// We can skip non pattern matching arguments
|
||||
Type::Any => IndexMap::from([(Name::from("_"), rules_to_check)]),
|
||||
Type::Adt(adt_nam) => {
|
||||
let adt = &adts[adt_nam];
|
||||
// For each constructor, which rules do we need to check.
|
||||
let mut next_rules_to_check: IndexMap<Name, Vec<usize>> =
|
||||
adt.ctrs.keys().cloned().map(|ctr| (ctr, vec![])).collect();
|
||||
for rule_idx in rules_to_check {
|
||||
let pat = &rules[rule_idx].pats[match_path.len()];
|
||||
match pat {
|
||||
// Rules with a var pattern are relevant to all constructors.
|
||||
Pattern::Var(_) => next_rules_to_check.values_mut().for_each(|x| x.push(rule_idx)),
|
||||
Pattern::Ctr(ctr_nam, _) => next_rules_to_check.get_mut(ctr_nam).unwrap().push(rule_idx),
|
||||
// We already type checked, so no other patterns will appear here.
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
next_rules_to_check
|
||||
}
|
||||
Type::Tup => IndexMap::from([(Name::from("(_,_)"), rules_to_check)]),
|
||||
Type::Num => {
|
||||
let mut next_rules_to_check: IndexMap<Name, Vec<usize>> =
|
||||
IndexMap::from([(Name::from("0"), vec![]), (Name::from("+"), vec![])]);
|
||||
for rule_idx in rules_to_check {
|
||||
let pat = &rules[rule_idx].pats[match_path.len()];
|
||||
match pat {
|
||||
Pattern::Var(_) => next_rules_to_check.values_mut().for_each(|x| x.push(rule_idx)),
|
||||
Pattern::Num(MatchNum::Zero) => {
|
||||
next_rules_to_check.get_mut(&Name::from("0")).unwrap().push(rule_idx);
|
||||
}
|
||||
Pattern::Num(MatchNum::Succ { .. }) => {
|
||||
next_rules_to_check.get_mut(&Name::from("+")).unwrap().push(rule_idx);
|
||||
}
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
next_rules_to_check
|
||||
}
|
||||
Type::None => unreachable!(),
|
||||
};
|
||||
|
||||
// Check that each constructor matches at least one rule and then check the next pattern recursively.
|
||||
for (ctr, matching_rules) in rules_matching_ctrs {
|
||||
if matching_rules.is_empty() {
|
||||
let missing = get_missing_pattern(match_path, &ctr, &types[1 ..], adts);
|
||||
missings.push(missing);
|
||||
}
|
||||
|
||||
let mut match_path = match_path.to_owned();
|
||||
match_path.push(ctr);
|
||||
check_pattern(&match_path, adts, rules, &types[1 ..], matching_rules, def_name)?;
|
||||
}
|
||||
}
|
||||
|
||||
if missings.is_empty() { Ok(()) } else { Err(ExhaustivenessErr(def_name.clone(), missings)) }
|
||||
}
|
||||
|
||||
/// Returns a string with the first pattern not covered by the definition.
|
||||
fn get_missing_pattern(
|
||||
match_path: &[Name],
|
||||
missing_ctr: &Name,
|
||||
remaining_types: &[Type],
|
||||
adts: &IndexMap<Name, Adt>,
|
||||
) -> String {
|
||||
let mut missing_set: Vec<_> = match_path.iter().map(ToString::to_string).collect();
|
||||
missing_set.push(missing_ctr.to_string());
|
||||
for typ in remaining_types {
|
||||
missing_set.push(first_ctr_of_type(typ, adts));
|
||||
}
|
||||
missing_set.join(" ")
|
||||
}
|
||||
|
||||
// TODO: Should not reimplement builtins constructor names and instead be in terms of Type::ctrs and Pattern::ctrs.
|
||||
fn first_ctr_of_type(typ: &Type, adts: &IndexMap<Name, Adt>) -> String {
|
||||
match typ {
|
||||
Type::Any => "_".to_string(),
|
||||
Type::Tup => "(_,_)".to_string(),
|
||||
Type::Num => "0".to_string(),
|
||||
Type::Adt(adt_name) => adts[adt_name].ctrs.keys().next().unwrap().to_string(),
|
||||
Type::None => unreachable!(),
|
||||
}
|
||||
}
|
73
src/term/check/match_arity.rs
Normal file
73
src/term/check/match_arity.rs
Normal file
@ -0,0 +1,73 @@
|
||||
use crate::{
|
||||
diagnostics::Info,
|
||||
term::{transform::encode_pattern_matching::MatchErr, Ctx, Definition, Term},
|
||||
};
|
||||
|
||||
impl Ctx<'_> {
|
||||
/// Checks that the number of arguments in every pattern matching rule is consistent.
|
||||
pub fn check_match_arity(&mut self) -> Result<(), Info> {
|
||||
self.info.start_pass();
|
||||
|
||||
for (def_name, def) in self.book.defs.iter() {
|
||||
if let Err(e) = def.check_match_arity() {
|
||||
self.info.def_error(def_name.clone(), e)
|
||||
};
|
||||
}
|
||||
|
||||
self.info.fatal(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Definition {
|
||||
pub fn check_match_arity(&self) -> Result<(), MatchErr> {
|
||||
let expected_arity = self.arity();
|
||||
for rule in &self.rules {
|
||||
if rule.arity() != expected_arity {
|
||||
return Err(MatchErr::ArityMismatch(rule.arity(), expected_arity));
|
||||
}
|
||||
rule.body.check_match_arity()?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Term {
|
||||
pub fn check_match_arity(&self) -> Result<(), MatchErr> {
|
||||
match self {
|
||||
Term::Mat { args, rules } => {
|
||||
let expected = args.len();
|
||||
for rule in rules {
|
||||
let found = rule.pats.len();
|
||||
if found != expected {
|
||||
return Err(MatchErr::ArityMismatch(found, expected));
|
||||
}
|
||||
rule.body.check_match_arity()?;
|
||||
}
|
||||
}
|
||||
|
||||
Term::Lst { els } => {
|
||||
for el in els {
|
||||
el.check_match_arity()?;
|
||||
}
|
||||
}
|
||||
Term::App { fun: fst, arg: snd, .. }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. }
|
||||
| Term::Let { val: fst, nxt: snd, .. } => {
|
||||
fst.check_match_arity()?;
|
||||
snd.check_match_arity()?;
|
||||
}
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.check_match_arity()?,
|
||||
Term::Var { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Str { .. }
|
||||
| Term::Ref { .. }
|
||||
| Term::Era
|
||||
| Term::Err => {}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
@ -1,5 +1,5 @@
|
||||
pub mod ctrs_arities;
|
||||
pub mod exhaustiveness;
|
||||
pub mod match_arity;
|
||||
pub mod set_entrypoint;
|
||||
pub mod shared_names;
|
||||
pub mod type_check;
|
||||
|
@ -28,7 +28,7 @@ impl Display for EntryErr {
|
||||
}
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
impl Ctx<'_> {
|
||||
pub fn set_entrypoint(&mut self) {
|
||||
let mut entrypoint = None;
|
||||
|
||||
@ -80,7 +80,7 @@ fn validate_entry_point(entry: &Definition) -> Result<Name, EntryErr> {
|
||||
|
||||
impl Book {
|
||||
fn get_possible_entry_points(&self) -> (Option<&Definition>, Option<&Definition>, Option<&Definition>) {
|
||||
let custom = self.entrypoint.as_ref().map(|e| self.defs.get(e)).flatten();
|
||||
let custom = self.entrypoint.as_ref().and_then(|e| self.defs.get(e));
|
||||
let main = self.defs.get(&Name::from(ENTRY_POINT));
|
||||
let hvm1_main = self.defs.get(&Name::from(HVM1_ENTRY_POINT));
|
||||
(custom, main, hvm1_main)
|
||||
|
@ -11,7 +11,7 @@ impl Display for TopLevelErr {
|
||||
}
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
impl Ctx<'_> {
|
||||
/// Checks if exists shared names from definitions, adts and constructors.
|
||||
pub fn check_shared_names(&mut self) {
|
||||
let mut checked = HashMap::<&Name, usize>::new();
|
||||
|
@ -1,109 +1,27 @@
|
||||
use std::fmt::Display;
|
||||
|
||||
use crate::{
|
||||
diagnostics::Info,
|
||||
term::{Ctx, Definition, Name, Pattern, Type},
|
||||
};
|
||||
use crate::term::{transform::encode_pattern_matching::MatchErr, Constructors, Name, Pattern, Type};
|
||||
use indexmap::IndexMap;
|
||||
|
||||
pub type DefinitionTypes = IndexMap<Name, Vec<Type>>;
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum InferErr {
|
||||
TypeMismatch(Name, Name),
|
||||
ArityMismatch(usize, usize),
|
||||
}
|
||||
|
||||
impl Display for InferErr {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
match self {
|
||||
InferErr::TypeMismatch(new, old) => {
|
||||
write!(f, "Type mismatch. Found '{new}' expected {old}.")
|
||||
}
|
||||
InferErr::ArityMismatch(found, expected) => {
|
||||
write!(f, "Arity error. Found {found} arguments, expected {expected}.")
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
/// Returns a HashMap from the definition id to the inferred pattern types
|
||||
/// and checks the rules arities based on the first rule arity.
|
||||
/// Expects patterns to be flattened.
|
||||
pub fn infer_def_types(&mut self) -> Result<DefinitionTypes, Info> {
|
||||
self.info.start_pass();
|
||||
|
||||
let mut def_types = IndexMap::new();
|
||||
|
||||
for (def_name, def) in &self.book.defs {
|
||||
match def.infer_type(&self.book.ctrs) {
|
||||
Ok(def_type) => _ = def_types.insert(def_name.clone(), def_type),
|
||||
Err(e) => self.info.def_error(def_name.clone(), e),
|
||||
}
|
||||
}
|
||||
|
||||
self.info.fatal(def_types)
|
||||
}
|
||||
}
|
||||
|
||||
impl Definition {
|
||||
pub fn infer_type(&self, ctrs: &IndexMap<Name, Name>) -> Result<Vec<Type>, InferErr> {
|
||||
let mut arg_types = vec![];
|
||||
|
||||
for arg_idx in 0 .. self.arity() {
|
||||
let pats = self.rules.iter().map(|r| &r.pats[arg_idx]);
|
||||
let value = infer_arg_type(pats, ctrs)?;
|
||||
arg_types.push(value);
|
||||
}
|
||||
Ok(arg_types)
|
||||
}
|
||||
}
|
||||
|
||||
pub fn infer_arg_type<'a>(
|
||||
pats: impl Iterator<Item = &'a Pattern>,
|
||||
ctrs: &IndexMap<Name, Name>,
|
||||
) -> Result<Type, InferErr> {
|
||||
/// Infers the type of a sequence of arguments
|
||||
pub fn infer_type<'a>(
|
||||
pats: impl IntoIterator<Item = &'a Pattern>,
|
||||
ctrs: &Constructors,
|
||||
) -> Result<Type, MatchErr> {
|
||||
let mut arg_type = Type::Any;
|
||||
for pat in pats {
|
||||
unify(pat.to_type(ctrs), &mut arg_type)?;
|
||||
for pat in pats.into_iter() {
|
||||
arg_type = unify(arg_type, pat.to_type(ctrs))?;
|
||||
}
|
||||
Ok(arg_type)
|
||||
}
|
||||
|
||||
fn unify(new: Type, old: &mut Type) -> Result<(), InferErr> {
|
||||
match (new, &old) {
|
||||
(Type::Adt(new), Type::Adt(old)) if &new != old => {
|
||||
return Err(InferErr::TypeMismatch(new, old.clone()));
|
||||
}
|
||||
(new, Type::Any) => *old = new,
|
||||
_ => (),
|
||||
};
|
||||
Ok(())
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
pub fn check_arity(&mut self) -> Result<(), Info> {
|
||||
self.info.start_pass();
|
||||
|
||||
for (def_name, def) in self.book.defs.iter() {
|
||||
if let Err(e) = def.check_arity() {
|
||||
self.info.def_error(def_name.clone(), e)
|
||||
};
|
||||
}
|
||||
|
||||
self.info.fatal(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Definition {
|
||||
pub fn check_arity(&self) -> Result<(), InferErr> {
|
||||
let expected_arity = self.arity();
|
||||
for rule in &self.rules {
|
||||
if rule.arity() != expected_arity {
|
||||
return Err(InferErr::ArityMismatch(rule.arity(), expected_arity));
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
fn unify(old: Type, new: Type) -> Result<Type, MatchErr> {
|
||||
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::Tup, Type::Tup) => Ok(Type::Tup),
|
||||
(old, new) => Err(MatchErr::TypeMismatch(new, old)),
|
||||
}
|
||||
}
|
||||
|
@ -13,7 +13,7 @@ impl Display for UnboundCtrErr {
|
||||
}
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
impl Ctx<'_> {
|
||||
/// Check if the constructors in rule patterns or match patterns are defined.
|
||||
pub fn check_unbound_pats(&mut self) -> Result<(), Info> {
|
||||
self.info.start_pass();
|
||||
@ -23,11 +23,11 @@ impl<'book> Ctx<'book> {
|
||||
for rule in &def.rules {
|
||||
for pat in &rule.pats {
|
||||
let res = pat.check_unbounds(&is_ctr);
|
||||
self.info.take_err(res, Some(&def_name));
|
||||
self.info.take_err(res, Some(def_name));
|
||||
}
|
||||
|
||||
let res = rule.body.check_unbound_pats(&is_ctr);
|
||||
self.info.take_err(res, Some(&def_name));
|
||||
self.info.take_err(res, Some(def_name));
|
||||
}
|
||||
}
|
||||
|
||||
@ -59,6 +59,7 @@ impl Pattern {
|
||||
}
|
||||
Pattern::Lst(args) => args.iter().for_each(|arg| check.push(arg)),
|
||||
Pattern::Var(_) | Pattern::Num(_) => {}
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
unbounds
|
||||
@ -73,11 +74,15 @@ impl Term {
|
||||
val.check_unbound_pats(is_ctr)?;
|
||||
nxt.check_unbound_pats(is_ctr)?;
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.check_unbound_pats(is_ctr)?;
|
||||
for (pat, body) in arms {
|
||||
pat.check_unbounds(is_ctr)?;
|
||||
body.check_unbound_pats(is_ctr)?;
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.check_unbound_pats(is_ctr)?;
|
||||
}
|
||||
for rule in rules {
|
||||
for pat in &rule.pats {
|
||||
pat.check_unbounds(is_ctr)?;
|
||||
}
|
||||
rule.body.check_unbound_pats(is_ctr)?;
|
||||
}
|
||||
}
|
||||
Term::App { fun: fst, arg: snd, .. }
|
||||
|
@ -2,7 +2,10 @@ use crate::{
|
||||
diagnostics::Info,
|
||||
term::{Ctx, Name, Pattern, Term},
|
||||
};
|
||||
use std::{collections::{hash_map::Entry, HashMap}, fmt::Display};
|
||||
use std::{
|
||||
collections::{hash_map::Entry, HashMap},
|
||||
fmt::Display,
|
||||
};
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum UnboundVarErr {
|
||||
@ -27,7 +30,7 @@ impl Display for UnboundVarErr {
|
||||
}
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
impl Ctx<'_> {
|
||||
/// Checks that there are no unbound variables in all definitions.
|
||||
pub fn check_unbound_vars(&mut self) -> Result<(), Info> {
|
||||
self.info.start_pass();
|
||||
@ -37,7 +40,7 @@ impl<'book> Ctx<'book> {
|
||||
for rule in &mut def.rules {
|
||||
let mut scope = HashMap::new();
|
||||
for pat in &rule.pats {
|
||||
pat.names().for_each(|nam| push_scope(Some(nam), &mut scope));
|
||||
pat.binds().for_each(|nam| push_scope(Some(nam), &mut scope));
|
||||
}
|
||||
|
||||
rule.body.check_unbound_vars(&mut scope, &mut errs);
|
||||
@ -122,14 +125,16 @@ pub fn check_uses<'a>(
|
||||
check_uses(fst, scope, globals, errs);
|
||||
check_uses(snd, scope, globals, errs);
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
check_uses(matched, scope, globals, errs);
|
||||
for (pat, term) in arms {
|
||||
pat.names().for_each(|nam| push_scope(Some(nam), scope));
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
check_uses(arg, scope, globals, errs);
|
||||
}
|
||||
for rule in rules {
|
||||
rule.pats.iter().flat_map(|p| p.binds()).for_each(|nam| push_scope(Some(nam), scope));
|
||||
|
||||
check_uses(term, scope, globals, errs);
|
||||
check_uses(&mut rule.body, scope, globals, errs);
|
||||
|
||||
pat.names().for_each(|nam| pop_scope(Some(nam), scope));
|
||||
rule.pats.iter().flat_map(|p| p.binds()).rev().for_each(|nam| pop_scope(Some(nam), scope));
|
||||
}
|
||||
}
|
||||
Term::Lst { .. } => unreachable!(),
|
||||
|
@ -18,12 +18,12 @@ pub struct DisplayJoin<F, S>(pub F, pub S);
|
||||
impl<F, I, S> fmt::Display for DisplayJoin<F, S>
|
||||
where
|
||||
F: (Fn() -> I),
|
||||
I: Iterator,
|
||||
I: IntoIterator,
|
||||
I::Item: fmt::Display,
|
||||
S: fmt::Display,
|
||||
{
|
||||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||
for (i, x) in self.0().enumerate() {
|
||||
for (i, x) in self.0().into_iter().enumerate() {
|
||||
if i != 0 {
|
||||
self.1.fmt(f)?;
|
||||
}
|
||||
@ -59,12 +59,15 @@ impl fmt::Display for Term {
|
||||
Term::App { tag, fun, arg } => {
|
||||
write!(f, "{}({} {})", tag.display_padded(), fun.display_app(tag), arg)
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
Term::Mat { args, rules } => {
|
||||
write!(
|
||||
f,
|
||||
"match {} {{ {} }}",
|
||||
matched,
|
||||
DisplayJoin(|| arms.iter().map(|(pat, term)| display!("{}: {}", pat, term)), "; "),
|
||||
DisplayJoin(|| args, ", "),
|
||||
DisplayJoin(
|
||||
|| rules.iter().map(|rule| display!("{}: {}", DisplayJoin(|| &rule.pats, " "), rule.body)),
|
||||
"; "
|
||||
),
|
||||
)
|
||||
}
|
||||
Term::Dup { tag, fst, snd, val, nxt } => {
|
||||
@ -109,7 +112,8 @@ impl fmt::Display for Pattern {
|
||||
}
|
||||
Pattern::Num(num) => write!(f, "{num}"),
|
||||
Pattern::Tup(fst, snd) => write!(f, "({}, {})", fst, snd,),
|
||||
Pattern::Lst(pats) => write!(f, "[{}]", DisplayJoin(|| pats.iter(), ", ")),
|
||||
Pattern::Lst(pats) => write!(f, "[{}]", DisplayJoin(|| pats, ", ")),
|
||||
Pattern::Err => write!(f, "<Invalid>"),
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -185,7 +189,6 @@ impl fmt::Display for Type {
|
||||
Type::Tup => write!(f, "tup"),
|
||||
Type::Num => write!(f, "num"),
|
||||
Type::Adt(nam) => write!(f, "{nam}"),
|
||||
Type::None => unreachable!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
352
src/term/mod.rs
352
src/term/mod.rs
@ -1,3 +1,5 @@
|
||||
use self::{check::type_check::infer_type, parser::lexer::STRINGS};
|
||||
use crate::{diagnostics::Info, term::builtins::*, ENTRY_POINT};
|
||||
use indexmap::{IndexMap, IndexSet};
|
||||
use interner::global::GlobalString;
|
||||
use itertools::Itertools;
|
||||
@ -15,16 +17,13 @@ pub mod transform;
|
||||
pub use net_to_term::{net_to_term, ReadbackError};
|
||||
pub use term_to_net::{book_to_nets, term_to_compat_net};
|
||||
|
||||
use self::parser::lexer::STRINGS;
|
||||
use crate::{diagnostics::Info, term::builtins::*, ENTRY_POINT};
|
||||
|
||||
#[derive(Debug)]
|
||||
pub struct Ctx<'book> {
|
||||
pub book: &'book mut Book,
|
||||
pub info: Info,
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
impl Ctx<'_> {
|
||||
pub fn new(book: &mut Book) -> Ctx {
|
||||
Ctx { book, info: Info::default() }
|
||||
}
|
||||
@ -37,15 +36,18 @@ pub struct Book {
|
||||
pub defs: IndexMap<Name, Definition>,
|
||||
|
||||
/// The algebraic datatypes defined by the program
|
||||
pub adts: IndexMap<Name, Adt>,
|
||||
pub adts: Adts,
|
||||
|
||||
/// To which type does each constructor belong to.
|
||||
pub ctrs: IndexMap<Name, Name>,
|
||||
pub ctrs: Constructors,
|
||||
|
||||
/// A custom or default "main" entrypoint.
|
||||
pub entrypoint: Option<Name>,
|
||||
}
|
||||
|
||||
pub type Adts = IndexMap<Name, Adt>;
|
||||
pub type Constructors = IndexMap<Name, Name>;
|
||||
|
||||
/// A pattern matching function definition.
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct Definition {
|
||||
@ -55,26 +57,12 @@ pub struct Definition {
|
||||
}
|
||||
|
||||
/// A pattern matching rule of a definition.
|
||||
#[derive(Debug, Clone, Default)]
|
||||
#[derive(Debug, Clone, Default, PartialEq, Eq, Hash)]
|
||||
pub struct Rule {
|
||||
pub pats: Vec<Pattern>,
|
||||
pub body: Term,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||
pub enum MatchNum {
|
||||
Zero,
|
||||
Succ(Option<Option<Name>>),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||
pub enum Tag {
|
||||
Named(Name),
|
||||
Numeric(u32),
|
||||
Auto,
|
||||
Static,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, Default, PartialEq, Eq, Hash)]
|
||||
pub enum Term {
|
||||
Lam {
|
||||
@ -137,8 +125,8 @@ pub enum Term {
|
||||
snd: Box<Term>,
|
||||
},
|
||||
Mat {
|
||||
matched: Box<Term>,
|
||||
arms: Vec<(Pattern, Term)>,
|
||||
args: Vec<Term>,
|
||||
rules: Vec<Rule>,
|
||||
},
|
||||
Ref {
|
||||
nam: Name,
|
||||
@ -148,13 +136,29 @@ pub enum Term {
|
||||
Err,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Hash, Default)]
|
||||
pub enum Pattern {
|
||||
Var(Option<Name>),
|
||||
Ctr(Name, Vec<Pattern>),
|
||||
Num(MatchNum),
|
||||
Tup(Box<Pattern>, Box<Pattern>),
|
||||
Lst(Vec<Pattern>),
|
||||
#[default]
|
||||
Err,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||
pub enum MatchNum {
|
||||
Zero,
|
||||
Succ(Option<Option<Name>>),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||
pub enum Tag {
|
||||
Named(Name),
|
||||
Numeric(u32),
|
||||
Auto,
|
||||
Static,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
|
||||
@ -181,7 +185,6 @@ pub enum Op {
|
||||
/// Pattern types.
|
||||
#[derive(Debug, Clone, PartialEq, Eq)]
|
||||
pub enum Type {
|
||||
None,
|
||||
Any,
|
||||
Tup,
|
||||
Num,
|
||||
@ -252,6 +255,10 @@ impl Term {
|
||||
Term::Lam { tag, nam: Some(nam), bod: Box::new(bod) }
|
||||
}
|
||||
|
||||
pub fn var_or_era(nam: Option<Name>) -> Self {
|
||||
if let Some(nam) = nam { Term::Var { nam } } else { Term::Era }
|
||||
}
|
||||
|
||||
pub fn app(fun: Term, arg: Term) -> Self {
|
||||
Term::App { tag: Tag::Static, fun: Box::new(fun), arg: Box::new(arg) }
|
||||
}
|
||||
@ -296,7 +303,7 @@ impl Term {
|
||||
Term::Lnk { .. } => (),
|
||||
Term::Let { pat, val, nxt } => {
|
||||
val.subst(from, to);
|
||||
if !pat.names().contains(from) {
|
||||
if !pat.binds().contains(from) {
|
||||
nxt.subst(from, to);
|
||||
}
|
||||
}
|
||||
@ -306,20 +313,13 @@ impl Term {
|
||||
nxt.subst(from, to);
|
||||
}
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.subst(from, to);
|
||||
|
||||
for (rule, term) in arms {
|
||||
let can_subst;
|
||||
|
||||
if let Pattern::Num(MatchNum::Succ(Some(Some(nam)))) = rule {
|
||||
can_subst = nam != from;
|
||||
} else {
|
||||
can_subst = true;
|
||||
};
|
||||
|
||||
if can_subst {
|
||||
term.subst(from, to);
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.subst(from, to);
|
||||
}
|
||||
for rule in rules {
|
||||
if !rule.pats.iter().flat_map(|p| p.binds()).contains(from) {
|
||||
rule.body.subst(from, to);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -341,9 +341,9 @@ impl Term {
|
||||
Term::Lnk { nam } if nam == from => {
|
||||
*self = to.clone();
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.subst_unscoped(from, to);
|
||||
arms.iter_mut().for_each(|(_, arm)| arm.subst_unscoped(from, to));
|
||||
Term::Mat { args, rules } => {
|
||||
args.iter_mut().for_each(|arg| arg.subst_unscoped(from, to));
|
||||
rules.iter_mut().for_each(|rule| rule.body.subst_unscoped(from, to));
|
||||
}
|
||||
Term::Lst { els } => els.iter_mut().for_each(|el| el.subst_unscoped(from, to)),
|
||||
Term::Chn { bod, .. } | Term::Lam { bod, .. } => bod.subst_unscoped(from, to),
|
||||
@ -388,7 +388,7 @@ impl Term {
|
||||
let mut new_scope = Default::default();
|
||||
go(nxt, &mut new_scope);
|
||||
|
||||
for bind in pat.names() {
|
||||
for bind in pat.binds() {
|
||||
new_scope.remove(bind);
|
||||
}
|
||||
|
||||
@ -412,15 +412,16 @@ impl Term {
|
||||
go(fst, free_vars);
|
||||
go(snd, free_vars);
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
go(matched, free_vars);
|
||||
|
||||
for (rule, term) in arms {
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
go(arg, free_vars);
|
||||
}
|
||||
for rule in rules {
|
||||
let mut new_scope = Default::default();
|
||||
go(term, &mut new_scope);
|
||||
go(&rule.body, &mut new_scope);
|
||||
|
||||
for var in rule.names() {
|
||||
new_scope.remove(var);
|
||||
for nam in rule.pats.iter().flat_map(|p| p.binds()) {
|
||||
new_scope.remove(nam);
|
||||
}
|
||||
|
||||
free_vars.extend(new_scope);
|
||||
@ -453,10 +454,12 @@ impl Term {
|
||||
Term::Lnk { nam } => {
|
||||
uses.insert(nam.clone());
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
go(matched, decls, uses);
|
||||
for (_, arm) in arms {
|
||||
go(arm, decls, uses);
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
go(arg, decls, uses);
|
||||
}
|
||||
for rule in rules {
|
||||
go(&rule.body, decls, uses);
|
||||
}
|
||||
}
|
||||
Term::Lst { els } => {
|
||||
@ -486,77 +489,94 @@ impl Term {
|
||||
(decls, uses)
|
||||
}
|
||||
|
||||
/// Creates a new [`Term::Match`] from the given terms.
|
||||
/// If `scrutinee` is not a `Term::Var`, creates a let binding containing the match in its body
|
||||
pub fn new_native_match(
|
||||
scrutinee: Self,
|
||||
zero_term: Self,
|
||||
mut succ_label: Option<Name>,
|
||||
mut succ_term: Self,
|
||||
) -> Self {
|
||||
let zero = (Pattern::Num(MatchNum::Zero), zero_term);
|
||||
|
||||
if let Term::Var { nam } = &scrutinee {
|
||||
if let Some(label) = &succ_label {
|
||||
let new_label = Name::new(format!("{}-1", nam));
|
||||
succ_term.subst(label, &Term::Var { nam: new_label.clone() });
|
||||
succ_label = Some(new_label);
|
||||
}
|
||||
|
||||
let succ = (Pattern::Num(MatchNum::Succ(Some(succ_label))), succ_term);
|
||||
Term::Mat { matched: Box::new(scrutinee), arms: vec![zero, succ] }
|
||||
} else {
|
||||
match succ_label {
|
||||
Some(succ) => {
|
||||
let match_bind = succ.clone();
|
||||
|
||||
let new_label = Name::new(format!("{}-1", succ));
|
||||
succ_term.subst(&succ, &Term::Var { nam: new_label.clone() });
|
||||
succ_label = Some(new_label);
|
||||
|
||||
let succ = (Pattern::Num(MatchNum::Succ(Some(succ_label))), succ_term);
|
||||
|
||||
Term::Let {
|
||||
pat: Pattern::Var(Some(match_bind.clone())),
|
||||
val: Box::new(scrutinee),
|
||||
nxt: Box::new(Term::Mat {
|
||||
matched: Box::new(Term::Var { nam: match_bind }),
|
||||
arms: vec![zero, succ],
|
||||
}),
|
||||
}
|
||||
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_type(rules.iter().map(|r| &r.pats[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;
|
||||
}
|
||||
None => {
|
||||
let succ = (Pattern::Num(MatchNum::Succ(None)), succ_term);
|
||||
|
||||
Term::Mat { matched: Box::new(scrutinee), arms: vec![zero, succ] }
|
||||
if !matches!(rules[0].pats.as_slice(), [Pattern::Var(_)]) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
Type::Tup => {
|
||||
if rules.len() != 1 {
|
||||
return false;
|
||||
}
|
||||
if !matches!(rules[0].pats.as_slice(), [Pattern::Tup(box Pattern::Var(_), box Pattern::Var(_))]) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
Type::Num => {
|
||||
if rules.len() != 2 {
|
||||
return false;
|
||||
}
|
||||
if !matches!(rules[0].pats[0], Pattern::Num(MatchNum::Zero)) {
|
||||
return false;
|
||||
}
|
||||
if !matches!(rules[1].pats[0], Pattern::Num(MatchNum::Succ(Some(_)))) {
|
||||
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 vars(&self) -> impl DoubleEndedIterator<Item = &Option<Name>> {
|
||||
fn go<'a>(pat: &'a Pattern, set: &mut Vec<&'a Option<Name>>) {
|
||||
match pat {
|
||||
Pattern::Var(nam) => set.push(nam),
|
||||
Pattern::Ctr(_, pats) | Pattern::Lst(pats) => pats.iter().for_each(|pat| go(pat, set)),
|
||||
Pattern::Tup(fst, snd) => {
|
||||
go(fst, set);
|
||||
go(snd, set);
|
||||
}
|
||||
Pattern::Num(MatchNum::Succ(Some(nam))) => {
|
||||
set.push(nam);
|
||||
}
|
||||
Pattern::Num(_) => {}
|
||||
}
|
||||
}
|
||||
let mut set = Vec::new();
|
||||
go(self, &mut set);
|
||||
set.into_iter()
|
||||
pub fn bind_or_eras(&self) -> impl DoubleEndedIterator<Item = &Option<Name>> {
|
||||
self.iter().filter_map(|pat| match pat {
|
||||
Pattern::Var(nam) => Some(nam),
|
||||
Pattern::Num(MatchNum::Succ(nam)) => nam.as_ref(),
|
||||
_ => None,
|
||||
})
|
||||
}
|
||||
|
||||
pub fn vars_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Option<Name>> {
|
||||
pub fn bind_or_eras_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Option<Name>> {
|
||||
// Can't have a Pattern::iter_mut() since it has a tree-like structure.
|
||||
fn go<'a>(pat: &'a mut Pattern, set: &mut Vec<&'a mut Option<Name>>) {
|
||||
match pat {
|
||||
Pattern::Var(nam) => set.push(nam),
|
||||
@ -569,6 +589,7 @@ impl Pattern {
|
||||
set.push(nam);
|
||||
}
|
||||
Pattern::Num(_) => {}
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
let mut set = Vec::new();
|
||||
@ -576,43 +597,53 @@ impl Pattern {
|
||||
set.into_iter()
|
||||
}
|
||||
|
||||
pub fn names(&self) -> impl DoubleEndedIterator<Item = &Name> {
|
||||
self.vars().flatten()
|
||||
pub fn binds(&self) -> impl DoubleEndedIterator<Item = &Name> {
|
||||
self.bind_or_eras().flatten()
|
||||
}
|
||||
|
||||
pub fn names_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Name> {
|
||||
self.vars_mut().flatten()
|
||||
pub fn binds_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Name> {
|
||||
self.bind_or_eras_mut().flatten()
|
||||
}
|
||||
|
||||
pub fn ctrs(&self) -> Vec<Name> {
|
||||
fn go(pat: &Pattern, set: &mut Vec<Name>) {
|
||||
match pat {
|
||||
Pattern::Ctr(nam, pats) => {
|
||||
set.push(nam.clone());
|
||||
pats.iter().for_each(|pat| go(pat, set));
|
||||
}
|
||||
Pattern::Lst(pats) => {
|
||||
set.push(builtins::LCONS.into());
|
||||
set.push(builtins::LNIL.into());
|
||||
pats.iter().for_each(|pat| go(pat, set))
|
||||
}
|
||||
Pattern::Tup(fst, snd) => {
|
||||
set.push("(,)".into());
|
||||
go(fst, set);
|
||||
go(snd, set);
|
||||
}
|
||||
Pattern::Num(MatchNum::Zero) => {
|
||||
set.push("0".into());
|
||||
}
|
||||
Pattern::Num(MatchNum::Succ(_)) => {
|
||||
set.push("+".into());
|
||||
}
|
||||
Pattern::Var(_) => {}
|
||||
}
|
||||
/// Returns an iterator over each immediate child sub-pattern of `self`.
|
||||
/// Considers Lists as its own pattern and not a sequence of Cons.
|
||||
pub fn children<'a>(&'a self) -> Box<dyn DoubleEndedIterator<Item = &'a Pattern> + 'a> {
|
||||
match self {
|
||||
Pattern::Ctr(_, children) => Box::new(children.iter()),
|
||||
Pattern::Var(_) => Box::new([].iter()),
|
||||
Pattern::Num(_) => Box::new([].iter()),
|
||||
Pattern::Tup(fst, snd) => Box::new([fst.as_ref(), snd.as_ref()].into_iter()),
|
||||
Pattern::Lst(els) => Box::new(els.iter()),
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
let mut set = Vec::new();
|
||||
go(self, &mut set);
|
||||
set
|
||||
}
|
||||
|
||||
/// Returns an iterator over each subpattern in depth-first, left to right order.
|
||||
// TODO: Not lazy.
|
||||
pub fn iter(&self) -> impl DoubleEndedIterator<Item = &Pattern> {
|
||||
let mut to_visit = vec![self];
|
||||
let mut els = vec![];
|
||||
while let Some(pat) = to_visit.pop() {
|
||||
to_visit.extend(pat.children().rev());
|
||||
els.push(pat);
|
||||
}
|
||||
els.into_iter()
|
||||
}
|
||||
|
||||
pub fn ctr_name(&self) -> Option<Name> {
|
||||
match self {
|
||||
Pattern::Var(_) => None,
|
||||
Pattern::Ctr(nam, _) => Some(nam.clone()),
|
||||
Pattern::Num(MatchNum::Zero) => Some(Name::new("0")),
|
||||
Pattern::Num(MatchNum::Succ(_)) => Some(Name::new("+")),
|
||||
Pattern::Tup(_, _) => Some(Name::new("(,)")),
|
||||
Pattern::Lst(_) => todo!(),
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn is_wildcard(&self) -> bool {
|
||||
matches!(self, Pattern::Var(_))
|
||||
}
|
||||
|
||||
pub fn is_detached_num_match(&self) -> bool {
|
||||
@ -628,7 +659,7 @@ impl Pattern {
|
||||
}
|
||||
|
||||
/// True if this pattern has no nested subpatterns.
|
||||
pub fn is_flat(&self) -> bool {
|
||||
pub fn is_simple(&self) -> bool {
|
||||
match self {
|
||||
Pattern::Var(_) => true,
|
||||
Pattern::Ctr(_, args) | Pattern::Lst(args) => args.iter().all(|arg| matches!(arg, Pattern::Var(_))),
|
||||
@ -636,10 +667,11 @@ impl Pattern {
|
||||
Pattern::Tup(fst, snd) => {
|
||||
matches!(fst.as_ref(), Pattern::Var(_)) && matches!(snd.as_ref(), Pattern::Var(_))
|
||||
}
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn to_type(&self, ctrs: &IndexMap<Name, Name>) -> Type {
|
||||
pub fn to_type(&self, ctrs: &Constructors) -> Type {
|
||||
match self {
|
||||
Pattern::Var(_) => Type::Any,
|
||||
Pattern::Ctr(ctr_nam, _) => {
|
||||
@ -649,13 +681,13 @@ impl Pattern {
|
||||
Pattern::Tup(..) => Type::Tup,
|
||||
Pattern::Num(..) => Type::Num,
|
||||
Pattern::Lst(..) => Type::Adt(builtins::LIST.into()),
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn to_term(&self) -> Term {
|
||||
match self {
|
||||
Pattern::Var(None) => Term::Era,
|
||||
Pattern::Var(Some(nam)) => Term::Var { nam: nam.clone() },
|
||||
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()))
|
||||
}
|
||||
@ -674,11 +706,12 @@ impl Pattern {
|
||||
p.encode_builtins();
|
||||
p.to_term()
|
||||
}
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
||||
/// True if both patterns are equal (match the same expressions) without considering nested patterns.
|
||||
pub fn flat_equals(&self, other: &Pattern) -> bool {
|
||||
pub fn simple_equals(&self, other: &Pattern) -> bool {
|
||||
match (self, other) {
|
||||
(Pattern::Ctr(a, _), Pattern::Ctr(b, _)) if a == b => true,
|
||||
(Pattern::Num(MatchNum::Zero), Pattern::Num(MatchNum::Zero)) => true,
|
||||
@ -692,13 +725,13 @@ impl Pattern {
|
||||
|
||||
/// 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 is_flat_subset_of(&self, other: &Pattern) -> bool {
|
||||
self.flat_equals(other) || matches!(other, Pattern::Var(_))
|
||||
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_matches_with(&self, other: &Pattern) -> bool {
|
||||
self.flat_equals(other) || matches!(self, Pattern::Var(_)) || matches!(other, Pattern::Var(_))
|
||||
pub fn shares_simple_matches_with(&self, other: &Pattern) -> bool {
|
||||
self.simple_equals(other) || matches!(self, Pattern::Var(_)) || matches!(other, Pattern::Var(_))
|
||||
}
|
||||
}
|
||||
|
||||
@ -734,10 +767,9 @@ impl Definition {
|
||||
|
||||
impl Type {
|
||||
/// Return the constructors for a given type as patterns.
|
||||
pub fn ctrs(&self, adts: &IndexMap<Name, Adt>) -> Vec<Pattern> {
|
||||
pub fn ctrs(&self, adts: &Adts) -> Vec<Pattern> {
|
||||
match self {
|
||||
Type::None => vec![],
|
||||
Type::Any => vec![],
|
||||
Type::Any => vec![Pattern::Var(None)],
|
||||
Type::Tup => vec![Pattern::Tup(
|
||||
Box::new(Pattern::Var(Some("%fst".into()))),
|
||||
Box::new(Pattern::Var(Some("%snd".into()))),
|
||||
|
@ -1,3 +1,4 @@
|
||||
use super::Rule;
|
||||
use crate::{
|
||||
net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT},
|
||||
term::{num_to_name, term_to_net::Labels, Book, MatchNum, Name, Op, Pattern, Tag, Term},
|
||||
@ -309,10 +310,11 @@ impl Term {
|
||||
| Term::Opx { fst, snd, .. } => {
|
||||
fst.insert_split(split, threshold)? + snd.insert_split(split, threshold)?
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
let mut n = matched.insert_split(split, threshold)?;
|
||||
for arm in arms {
|
||||
n += arm.1.insert_split(split, threshold)?;
|
||||
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
|
||||
}
|
||||
@ -373,21 +375,63 @@ impl Term {
|
||||
fst.fix_names(id_counter, book);
|
||||
snd.fix_names(id_counter, book);
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.fix_names(id_counter, book);
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.fix_names(id_counter, book);
|
||||
}
|
||||
|
||||
for (rule, term) in arms {
|
||||
if let Pattern::Num(MatchNum::Succ(Some(nam))) = rule {
|
||||
fix_name(nam, id_counter, term);
|
||||
for rule in rules {
|
||||
for nam in rule.pats.iter_mut().flat_map(|p| p.bind_or_eras_mut()) {
|
||||
fix_name(nam, id_counter, &mut rule.body);
|
||||
}
|
||||
|
||||
term.fix_names(id_counter, book);
|
||||
rule.body.fix_names(id_counter, book);
|
||||
}
|
||||
}
|
||||
Term::Let { .. } | Term::Lst { .. } => unreachable!(),
|
||||
Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {}
|
||||
}
|
||||
}
|
||||
|
||||
/// Creates a new [`Term::Match`] from the given terms.
|
||||
/// If `scrutinee` is not a `Term::Var`, creates a let binding containing the match in its body
|
||||
fn new_native_match(arg: Self, zero_term: Self, mut succ_label: Option<Name>, mut succ_term: Self) -> Self {
|
||||
let zero = Rule { pats: vec![Pattern::Num(MatchNum::Zero)], body: zero_term };
|
||||
|
||||
if let Term::Var { nam } = &arg {
|
||||
if let Some(label) = &succ_label {
|
||||
let new_label = Name::new(format!("{}-1", nam));
|
||||
succ_term.subst(label, &Term::Var { nam: new_label.clone() });
|
||||
succ_label = Some(new_label);
|
||||
}
|
||||
|
||||
let succ = Rule { pats: vec![Pattern::Num(MatchNum::Succ(Some(succ_label)))], body: succ_term };
|
||||
Term::Mat { args: vec![arg], rules: vec![zero, succ] }
|
||||
} else {
|
||||
match succ_label {
|
||||
Some(succ) => {
|
||||
let match_bind = succ.clone();
|
||||
|
||||
let new_label = Name::new(format!("{}-1", succ));
|
||||
succ_term.subst(&succ, &Term::Var { nam: new_label.clone() });
|
||||
succ_label = Some(new_label);
|
||||
|
||||
let succ = Rule { pats: vec![Pattern::Num(MatchNum::Succ(Some(succ_label)))], body: succ_term };
|
||||
|
||||
Term::Let {
|
||||
pat: Pattern::Var(Some(match_bind.clone())),
|
||||
val: Box::new(arg),
|
||||
nxt: Box::new(Term::Mat { args: vec![Term::Var { nam: match_bind }], rules: vec![zero, succ] }),
|
||||
}
|
||||
}
|
||||
None => {
|
||||
let succ = Rule { pats: vec![Pattern::Num(MatchNum::Succ(None))], body: succ_term };
|
||||
|
||||
Term::Mat { args: vec![arg], rules: vec![zero, succ] }
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Default)]
|
||||
|
@ -123,7 +123,7 @@ fn name<'a, I>() -> impl Parser<'a, I, Name, extra::Err<Rich<'a, Token>>>
|
||||
where
|
||||
I: ValueInput<'a, Token = Token, Span = SimpleSpan>,
|
||||
{
|
||||
// FIXME: bug with chunsky when using with `.repeated`
|
||||
// FIXME: bug with chumsky when using with `.repeated`
|
||||
// select!(Token::Name(name) => Name::from(name)).labelled("<Name>")
|
||||
|
||||
any()
|
||||
@ -209,6 +209,7 @@ where
|
||||
);
|
||||
|
||||
let term_sep = just(Token::Semicolon).or_not();
|
||||
let list_sep = just(Token::Comma).or_not();
|
||||
|
||||
recursive(|term| {
|
||||
// *
|
||||
@ -275,25 +276,42 @@ where
|
||||
.map(|((pat, val), nxt)| Term::Let { pat, val: Box::new(val), nxt: Box::new(nxt) })
|
||||
.boxed();
|
||||
|
||||
// '|'? pat: term
|
||||
let match_arm = just(Token::Or)
|
||||
.or_not()
|
||||
.ignore_then(pattern().then_ignore(just(Token::Colon)).then(term.clone()).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::<Vec<_>>();
|
||||
|
||||
// match (scrutinee | <name> = value) { pat: term;... }
|
||||
let match_ = just(Token::Match)
|
||||
.ignore_then(name().then_ignore(just(Token::Equals)).or_not())
|
||||
// '|'? pat+: term
|
||||
let match_rule = just(Token::Or)
|
||||
.or_not()
|
||||
.ignore_then(pattern().repeated().at_least(1).collect::<Vec<_>>())
|
||||
.then_ignore(just(Token::Colon))
|
||||
.then(term.clone())
|
||||
.map(|(pats, body)| Rule { pats, body });
|
||||
let match_rules = match_rule.separated_by(term_sep.clone()).at_least(1).allow_trailing().collect();
|
||||
|
||||
// match ((scrutinee | <name> = value),?)+ { pat+: term;... }
|
||||
let match_ = just(Token::Match)
|
||||
.ignore_then(match_args)
|
||||
.then_ignore(just(Token::LBracket))
|
||||
.then(match_arm.separated_by(term_sep.clone()).allow_trailing().collect())
|
||||
.then(match_rules)
|
||||
.then_ignore(just(Token::RBracket))
|
||||
.map(|((bind, scrutinee), arms)| match bind {
|
||||
Some(nam) => Term::Let {
|
||||
pat: Pattern::Var(Some(nam.clone())),
|
||||
val: Box::new(scrutinee),
|
||||
nxt: Box::new(Term::Mat { matched: Box::new(Term::Var { nam }), arms }),
|
||||
},
|
||||
None => Term::Mat { matched: Box::new(scrutinee), arms },
|
||||
.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);
|
||||
}
|
||||
}
|
||||
let mat = Term::Mat { args: args_no_bind, rules };
|
||||
binds.into_iter().rev().fold(mat, |acc, (bind, arg)| Term::Let {
|
||||
pat: Pattern::Var(Some(bind)),
|
||||
val: Box::new(arg),
|
||||
nxt: Box::new(acc),
|
||||
})
|
||||
})
|
||||
.boxed();
|
||||
|
||||
@ -419,9 +437,9 @@ where
|
||||
}));
|
||||
|
||||
let paren_lhs = just(Token::LParen)
|
||||
.ignore_then(lhs.clone().map_err(|err| map_unexpected_eof::<I>(err, Token::Name(STRINGS.get("<Name>")))))
|
||||
.ignore_then(lhs.clone().map_err(|err| map_unexpected_eof(err, Token::Name(STRINGS.get("<Name>")))))
|
||||
.then_ignore(just(Token::RParen))
|
||||
.then_ignore(just(Token::Equals).map_err(|err| map_unexpected_eof::<I>(err, Token::Equals)));
|
||||
.then_ignore(just(Token::Equals).map_err(|err| map_unexpected_eof(err, Token::Equals)));
|
||||
|
||||
choice((just_lhs, paren_lhs))
|
||||
}
|
||||
@ -447,16 +465,13 @@ where
|
||||
let data_name = tl_name().map_with_span(|name, span| (name, span));
|
||||
|
||||
soft_keyword("data")
|
||||
.ignore_then(data_name.map_err(|err| map_unexpected_eof::<I>(err, Token::Name(STRINGS.get("<Name>")))))
|
||||
.ignore_then(data_name.map_err(|err| map_unexpected_eof(err, Token::Name(STRINGS.get("<Name>")))))
|
||||
.then_ignore(just(Token::Equals))
|
||||
.then(ctrs.map_err(|err| map_unexpected_eof::<I>(err, Token::Name(STRINGS.get("constructor")))))
|
||||
.then(ctrs.map_err(|err| map_unexpected_eof(err, Token::Name(STRINGS.get("constructor")))))
|
||||
.map(move |(name, ctrs)| TopLevel::Adt(name, ctrs))
|
||||
}
|
||||
|
||||
fn map_unexpected_eof<'a, I>(err: Rich<'a, Token>, expected_token: Token) -> Rich<'a, Token>
|
||||
where
|
||||
I: ValueInput<'a, Token = Token, Span = SimpleSpan>,
|
||||
{
|
||||
fn map_unexpected_eof(err: Rich<Token>, expected_token: Token) -> Rich<Token> {
|
||||
if err.found().is_none() {
|
||||
// Not using Error::expected_found here to not merge with other expected_found errors
|
||||
Rich::custom(*err.span(), format!("found end of input expected {}", expected_token))
|
||||
|
@ -14,11 +14,7 @@ pub fn book_to_nets(book: &Book) -> (HashMap<String, INet>, Labels) {
|
||||
for rule in def.rules.iter() {
|
||||
let net = term_to_compat_net(&rule.body, &mut labels);
|
||||
|
||||
let name = if def.name == *main {
|
||||
book.hvmc_entrypoint().to_string()
|
||||
} else {
|
||||
def.name.0.to_string()
|
||||
};
|
||||
let name = if def.name == *main { book.hvmc_entrypoint().to_string() } else { def.name.0.to_string() };
|
||||
|
||||
nets.insert(name, net);
|
||||
}
|
||||
@ -109,16 +105,19 @@ impl<'a> EncodeTermState<'a> {
|
||||
Some(Port(app, 2))
|
||||
}
|
||||
// core: & cond ~ (zero succ) ret
|
||||
Term::Mat { matched, arms } => {
|
||||
Term::Mat { args, rules } => {
|
||||
// At this point should be only simple num matches.
|
||||
let arg = args.iter().next().unwrap();
|
||||
debug_assert!(matches!(rules[0].pats[..], [Pattern::Num(MatchNum::Zero)]));
|
||||
debug_assert!(matches!(rules[1].pats[..], [Pattern::Num(MatchNum::Succ(None))]));
|
||||
|
||||
let if_ = self.inet.new_node(Mat);
|
||||
|
||||
let cond = self.encode_term(matched, Port(if_, 0));
|
||||
let cond = self.encode_term(arg, Port(if_, 0));
|
||||
self.link_local(Port(if_, 0), cond);
|
||||
|
||||
debug_assert!(matches!(arms[0].0, Pattern::Num(MatchNum::Zero)));
|
||||
debug_assert!(matches!(arms[1].0, Pattern::Num(MatchNum::Succ(None))));
|
||||
let zero = &arms[0].1;
|
||||
let succ = &arms[1].1;
|
||||
let zero = &rules[0].body;
|
||||
let succ = &rules[1].body;
|
||||
|
||||
let sel = self.inet.new_node(Con { lab: None });
|
||||
self.inet.link(Port(sel, 0), Port(if_, 1));
|
||||
|
@ -1,8 +1,9 @@
|
||||
use std::collections::{hash_map::Entry, HashMap};
|
||||
|
||||
use crate::{
|
||||
diagnostics::Warning,
|
||||
term::{Adt, AdtEncoding, Book, Ctx, Name, Tag, Term, LIST, STRING},
|
||||
diagnostics::Warning, CORE_BUILTINS,
|
||||
CORE_BUILTINS,
|
||||
};
|
||||
use indexmap::IndexSet;
|
||||
|
||||
@ -24,7 +25,7 @@ enum Used {
|
||||
|
||||
type Definitions = HashMap<Name, Used>;
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
impl Ctx<'_> {
|
||||
/// If `prune_all`, removes all unused definitions and adts starting from Main.
|
||||
/// Otherwise, prunes only the builtins not accessible from any non-built-in definition
|
||||
pub fn prune(&mut self, prune_all: bool, adt_encoding: AdtEncoding) {
|
||||
@ -107,10 +108,12 @@ impl Book {
|
||||
to_find.push(fst);
|
||||
to_find.push(snd);
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
to_find.push(matched);
|
||||
for (_, bod) in arms {
|
||||
to_find.push(bod);
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
to_find.push(arg);
|
||||
}
|
||||
for rule in rules {
|
||||
to_find.push(&rule.body);
|
||||
}
|
||||
}
|
||||
Term::Lst { els } => {
|
||||
@ -148,7 +151,7 @@ impl Book {
|
||||
fn insert_used(&self, def_name: &Name, used: Used, uses: &mut Definitions, adt_encoding: AdtEncoding) {
|
||||
if let Entry::Vacant(e) = uses.entry(def_name.clone()) {
|
||||
e.insert(used);
|
||||
if CORE_BUILTINS.contains(&def_name.0.as_ref().as_ref()) {
|
||||
if CORE_BUILTINS.contains(&def_name.0.as_ref()) {
|
||||
return;
|
||||
}
|
||||
|
||||
|
@ -1,5 +1,4 @@
|
||||
use crate::term::{Adt, Book, MatchNum, Name, Pattern, Term};
|
||||
use indexmap::IndexMap;
|
||||
use crate::term::{Adts, Book, Constructors, MatchNum, Name, Pattern, Term};
|
||||
|
||||
impl Book {
|
||||
pub fn desugar_implicit_match_binds(&mut self) {
|
||||
@ -12,58 +11,70 @@ impl Book {
|
||||
}
|
||||
|
||||
impl Term {
|
||||
pub fn desugar_implicit_match_binds(&mut self, ctrs: &IndexMap<Name, Name>, adts: &IndexMap<Name, Adt>) {
|
||||
pub fn desugar_implicit_match_binds(&mut self, ctrs: &Constructors, adts: &Adts) {
|
||||
let mut to_desugar = vec![self];
|
||||
|
||||
while let Some(term) = to_desugar.pop() {
|
||||
match term {
|
||||
Term::Mat { matched, .. } => {
|
||||
let matched = if let Term::Var { nam } = matched.as_ref() {
|
||||
nam.clone()
|
||||
} else {
|
||||
let Term::Mat { matched, arms } = std::mem::take(term) else { unreachable!() };
|
||||
|
||||
let nam = Name::from("%matched");
|
||||
|
||||
*term = Term::Let {
|
||||
pat: Pattern::Var(Some(nam.clone())),
|
||||
val: matched,
|
||||
nxt: Box::new(Term::Mat { matched: Box::new(Term::Var { nam: nam.clone() }), arms }),
|
||||
};
|
||||
|
||||
nam
|
||||
};
|
||||
|
||||
let (Term::Mat { arms, .. } | Term::Let { nxt: box Term::Mat { arms, .. }, .. }) = term else {
|
||||
unreachable!()
|
||||
};
|
||||
|
||||
for (pat, body) in arms {
|
||||
match pat {
|
||||
Pattern::Var(_) => (),
|
||||
Pattern::Ctr(nam, pat_args) => {
|
||||
let adt = ctrs.get(nam).unwrap();
|
||||
let Adt { ctrs, .. } = adts.get(adt).unwrap();
|
||||
let ctr_args = ctrs.get(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!("{matched}.{field}")))))
|
||||
.collect();
|
||||
}
|
||||
}
|
||||
Pattern::Num(MatchNum::Zero) => (),
|
||||
Pattern::Num(MatchNum::Succ(Some(_))) => (),
|
||||
Pattern::Num(MatchNum::Succ(p @ None)) => {
|
||||
// Implicit num arg
|
||||
*p = Some(Some(Name::new(format!("{matched}-1"))));
|
||||
}
|
||||
Pattern::Tup(_, _) => (),
|
||||
Pattern::Lst(..) => unreachable!(),
|
||||
Term::Mat { args, rules } => {
|
||||
// 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)));
|
||||
}
|
||||
to_desugar.push(body);
|
||||
}
|
||||
|
||||
// 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(MatchNum::Zero) => (),
|
||||
Pattern::Num(MatchNum::Succ(Some(_))) => (),
|
||||
Pattern::Num(MatchNum::Succ(p @ None)) => {
|
||||
// Implicit num arg
|
||||
*p = Some(Some(Name::new(format!("{nam}-1"))));
|
||||
}
|
||||
Pattern::Tup(_, _) => (),
|
||||
Pattern::Lst(..) => unreachable!(),
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Add the binds to the extracted term vars.
|
||||
*term = match_args.into_iter().rev().fold(std::mem::take(term), |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
|
||||
}
|
||||
});
|
||||
|
||||
// Add the next values to check
|
||||
let mut term = term;
|
||||
while let Term::Let { nxt, .. } = term {
|
||||
term = nxt;
|
||||
}
|
||||
let Term::Mat { args: _, rules } = term else { unreachable!() };
|
||||
to_desugar.extend(rules.iter_mut().map(|r| &mut r.body));
|
||||
}
|
||||
Term::Let { pat: Pattern::Var(_), val: fst, nxt: snd }
|
||||
| Term::App { fun: fst, arg: snd, .. }
|
||||
|
@ -1,4 +1,4 @@
|
||||
use crate::term::{Book, Name, Pattern, Term};
|
||||
use crate::term::{Book, Name, Pattern, Rule, Term};
|
||||
|
||||
impl Book {
|
||||
/// Convert let destructor expressions like `let (a, b) = X` into the equivalent match expression.
|
||||
@ -23,10 +23,12 @@ impl Term {
|
||||
fst.desugar_let_destructors();
|
||||
snd.desugar_let_destructors();
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.desugar_let_destructors();
|
||||
for (_, arm) in arms {
|
||||
arm.desugar_let_destructors();
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.desugar_let_destructors();
|
||||
}
|
||||
for rule in rules {
|
||||
rule.body.desugar_let_destructors();
|
||||
}
|
||||
}
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
|
||||
@ -46,15 +48,15 @@ impl Term {
|
||||
val.desugar_let_destructors();
|
||||
nxt.desugar_let_destructors();
|
||||
|
||||
let arms = vec![(pat, *nxt)];
|
||||
let rules = vec![Rule { pats: vec![pat], body: *nxt }];
|
||||
|
||||
*self = if let Term::Var { .. } = val.as_ref() {
|
||||
Term::Mat { matched: val, arms }
|
||||
Term::Mat { args: vec![*val], rules }
|
||||
} else {
|
||||
let nam = Name::from("%temp%scrutinee");
|
||||
let nam = Name::from("%matched");
|
||||
let pat = Pattern::Var(Some(nam.clone()));
|
||||
let scrutinee = Box::new(Term::Var { nam });
|
||||
Term::Let { pat, val, nxt: Box::new(Term::Mat { matched: scrutinee, arms }) }
|
||||
let args = vec![Term::Var { nam }];
|
||||
Term::Let { pat, val, nxt: Box::new(Term::Mat { args, rules }) }
|
||||
};
|
||||
}
|
||||
Term::Lst { .. } => unreachable!("Should have been desugared already"),
|
||||
|
@ -234,14 +234,19 @@ impl Term {
|
||||
|
||||
val_detach & nxt_detach
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
let mut detach = go(matched, depth + 1, term_info);
|
||||
Term::Mat { args, rules } => {
|
||||
let mut detach = Detach::Combinator;
|
||||
for arg in args {
|
||||
detach = detach & go(arg, depth + 1, term_info);
|
||||
}
|
||||
let parent_scope = term_info.replace_scope(HashSet::new());
|
||||
|
||||
for (pat, term) in arms {
|
||||
debug_assert!(pat.is_detached_num_match());
|
||||
for rule in rules {
|
||||
for pat in &rule.pats {
|
||||
debug_assert!(pat.is_detached_num_match());
|
||||
}
|
||||
|
||||
let arm_detach = match go(term, depth + 1, term_info) {
|
||||
let arm_detach = match go(&mut rule.body, depth + 1, term_info) {
|
||||
// If the recursive ref reached here, it is not in a active position
|
||||
Detach::Recursive => Detach::Combinator,
|
||||
detach => detach,
|
||||
|
@ -1,434 +1,189 @@
|
||||
use crate::term::{
|
||||
check::type_check::DefinitionTypes, transform::unique_names::UniqueNameGenerator, AdtEncoding, Book,
|
||||
Definition, MatchNum, Name, Pattern, Rule, Tag, Term, Type,
|
||||
use std::fmt::Display;
|
||||
|
||||
use itertools::Itertools;
|
||||
|
||||
use crate::{
|
||||
diagnostics::ERR_INDENT_SIZE,
|
||||
term::{
|
||||
check::type_check::infer_type, display::DisplayFn, AdtEncoding, Adts, Book, Constructors, MatchNum, Name,
|
||||
Pattern, Rule, Tag, Term, Type,
|
||||
},
|
||||
};
|
||||
|
||||
impl Book {
|
||||
pub fn encode_pattern_matching_functions(
|
||||
&mut self,
|
||||
def_types: &DefinitionTypes,
|
||||
adt_encoding: AdtEncoding,
|
||||
) {
|
||||
let def_names = self.defs.keys().cloned().collect::<Vec<_>>();
|
||||
for def_name in def_names {
|
||||
let def_type = &def_types[&def_name];
|
||||
|
||||
let is_matching_def = def_type.iter().any(|t| matches!(t, Type::Adt(_) | Type::Tup | Type::Num));
|
||||
if is_matching_def {
|
||||
make_pattern_matching_def(self, &def_name, def_type, adt_encoding);
|
||||
} else {
|
||||
// For functions with only one rule that doesn't pattern match,
|
||||
// we just move the variables from arg to body.
|
||||
make_non_pattern_matching_def(self.defs.get_mut(&def_name).unwrap());
|
||||
/// Encodes pattern matching expressions in the book functions according to the adt_encoding.
|
||||
pub fn encode_simple_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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// For functions that don't pattern match, just move the arg variables into the body.
|
||||
fn make_non_pattern_matching_def(def: &mut Definition) {
|
||||
let rule = def.rules.first_mut().unwrap();
|
||||
let body = add_non_match_arg_lams(std::mem::take(&mut rule.body), &rule.pats);
|
||||
def.rules = vec![Rule { pats: vec![], body }];
|
||||
}
|
||||
|
||||
/// For functions that do pattern match,
|
||||
/// we break them into a tree of small matching functions
|
||||
/// with the original rule bodies at the end.
|
||||
fn make_pattern_matching_def(book: &mut Book, def_name: &Name, def_type: &[Type], adt_encoding: AdtEncoding) {
|
||||
// First push the pattern bound vars into the rule body
|
||||
let rules = &mut book.defs.get_mut(def_name).unwrap().rules;
|
||||
for rule in rules.iter_mut() {
|
||||
rule.body = add_non_match_arg_lams(std::mem::take(&mut rule.body), &rule.pats);
|
||||
impl Term {
|
||||
pub fn encode_simple_matches(&mut self, ctrs: &Constructors, adts: &Adts, adt_encoding: AdtEncoding) {
|
||||
match self {
|
||||
Term::Mat { .. } => {
|
||||
debug_assert!(self.is_simple_match(ctrs, adts), "{self}");
|
||||
let Term::Mat { args, rules } = self else { unreachable!() };
|
||||
for rule in rules.iter_mut() {
|
||||
rule.body.encode_simple_matches(ctrs, adts, adt_encoding);
|
||||
}
|
||||
let arg = std::mem::take(&mut args[0]);
|
||||
let rules = std::mem::take(rules);
|
||||
*self = encode_match(arg, rules, ctrs, adts, adt_encoding);
|
||||
}
|
||||
Term::Lst { els } => els.iter_mut().for_each(|e| e.encode_simple_matches(ctrs, adts, adt_encoding)),
|
||||
Term::Let { val: fst, nxt: snd, .. }
|
||||
| Term::App { fun: fst, arg: snd, .. }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. } => {
|
||||
fst.encode_simple_matches(ctrs, adts, adt_encoding);
|
||||
snd.encode_simple_matches(ctrs, adts, adt_encoding);
|
||||
}
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.encode_simple_matches(ctrs, adts, adt_encoding),
|
||||
Term::Var { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Str { .. }
|
||||
| Term::Ref { .. }
|
||||
| Term::Era
|
||||
| Term::Err => {}
|
||||
}
|
||||
}
|
||||
|
||||
// Generate scott-encoded pattern matching
|
||||
let def = &book.defs[def_name];
|
||||
let crnt_rules = (0 .. def.rules.len()).collect();
|
||||
let mut new_body = make_pattern_matching_case(book, def, def_type, crnt_rules, vec![], adt_encoding);
|
||||
|
||||
// Simplify the generated term
|
||||
new_body.eta_reduction();
|
||||
// We have to give unique names to avoid name conflicts when beta-reducing.
|
||||
// Ex: @x (@y @x (y x) x) => @x @x (x x)
|
||||
let mut name_gen = UniqueNameGenerator::default();
|
||||
name_gen.unique_names_in_term(&mut new_body);
|
||||
beta_reduce(&mut new_body);
|
||||
|
||||
// Substitute the rule bodies into the generated term
|
||||
for (rule_idx, rule) in def.rules.iter().enumerate() {
|
||||
// TODO: We should generate this things normalized to avoid this mess.
|
||||
let subst_var = rule_body_subst_var(rule_idx);
|
||||
subst_rule_body(&mut new_body, &subst_var, &rule.body, &mut name_gen);
|
||||
}
|
||||
// This is already a mess, so I'm putting this here so that we can at least read the result if it bugs.
|
||||
UniqueNameGenerator::default().unique_names_in_term(&mut new_body);
|
||||
|
||||
// Put the new body back into the definition.
|
||||
let def = book.defs.get_mut(def_name).unwrap();
|
||||
def.rules = vec![Rule { pats: vec![], body: new_body }];
|
||||
}
|
||||
|
||||
/// Builds the encoding for the patterns in a pattern matching function.
|
||||
fn make_pattern_matching_case(
|
||||
book: &Book,
|
||||
def: &Definition,
|
||||
def_type: &[Type],
|
||||
crnt_rules: Vec<usize>,
|
||||
match_path: Vec<Pattern>,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Term {
|
||||
// This is safe since we check exhaustiveness earlier.
|
||||
let fst_rule_idx = crnt_rules[0];
|
||||
let fst_rule = &def.rules[fst_rule_idx];
|
||||
let crnt_arg_idx = match_path.len();
|
||||
|
||||
// Check if we've reached the end for this subfunction.
|
||||
// We did if all the (possibly zero) remaining patterns are variables and not matches.
|
||||
let all_args_done = crnt_arg_idx >= def.arity();
|
||||
let only_var_left = fst_rule.pats[crnt_arg_idx ..].iter().all(|p| matches!(p, Pattern::Var(_)));
|
||||
let is_fst_rule_irrefutable = all_args_done || only_var_left;
|
||||
|
||||
if is_fst_rule_irrefutable {
|
||||
// First rule will always be selected, generate leaf case.
|
||||
make_leaf_case(book, fst_rule, fst_rule_idx, match_path, adt_encoding)
|
||||
} else {
|
||||
make_match_case(book, def, def_type, crnt_rules, match_path, adt_encoding)
|
||||
}
|
||||
}
|
||||
|
||||
/// Builds the term that pattern matches on the current arg.
|
||||
/// Recursively builds the terms matching the next args.
|
||||
fn make_match_case(
|
||||
book: &Book,
|
||||
def: &Definition,
|
||||
def_type: &[Type],
|
||||
crnt_rules: Vec<usize>,
|
||||
match_path: Vec<Pattern>,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Term {
|
||||
let next_arg_idx = match_path.len();
|
||||
let next_type = &def_type[next_arg_idx];
|
||||
|
||||
// Create the subfunctions
|
||||
let mut next_cases = vec![];
|
||||
let next_ctrs = if next_type.is_var_type() {
|
||||
vec![Pattern::Var(Some(Name::from("x")))]
|
||||
} else {
|
||||
next_type.ctrs(&book.adts)
|
||||
};
|
||||
for pat in &next_ctrs {
|
||||
let next_rules = crnt_rules
|
||||
.iter()
|
||||
.copied()
|
||||
.filter(|&rule_idx| pat.is_flat_subset_of(&def.rules[rule_idx].pats[next_arg_idx]))
|
||||
.collect();
|
||||
let mut match_path = match_path.clone();
|
||||
match_path.push(pat.clone());
|
||||
let next_case = make_pattern_matching_case(book, def, def_type, next_rules, match_path, adt_encoding);
|
||||
next_cases.push(next_case);
|
||||
}
|
||||
|
||||
let (old_args, new_args) = args_from_match_path(&match_path);
|
||||
|
||||
// Encode the current pattern matching, calling the subfunctions
|
||||
let match_var = Name::from("x");
|
||||
// The match term itself
|
||||
let term = encode_match(next_type, &match_var, next_cases.into_iter(), adt_encoding);
|
||||
// The calls to the args of previous matches
|
||||
let term = old_args.iter().chain(new_args.iter()).cloned().fold(term, Term::arg_call);
|
||||
// Lambda for pattern matched value
|
||||
let term = Term::named_lam(match_var, term);
|
||||
// The bindings of the previous args
|
||||
let term = add_arg_lams(term, old_args, new_args, match_path.last(), book, adt_encoding);
|
||||
term
|
||||
}
|
||||
|
||||
fn encode_match(
|
||||
match_type: &Type,
|
||||
match_var: &Name,
|
||||
mut arms: impl Iterator<Item = Term>,
|
||||
arg: Term,
|
||||
rules: Vec<Rule>,
|
||||
ctrs: &Constructors,
|
||||
adts: &Adts,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Term {
|
||||
match match_type {
|
||||
Type::None => unreachable!(),
|
||||
// (arm[0] x)
|
||||
Type::Any => Term::arg_call(arms.next().unwrap(), match_var.clone()),
|
||||
// let (%fst, %snd) = x; (arm[0] %fst %snd)
|
||||
Type::Tup => Term::Let {
|
||||
pat: Pattern::Tup(
|
||||
Box::new(Pattern::Var(Some(Name::from("%fst")))),
|
||||
Box::new(Pattern::Var(Some(Name::from("%snd")))),
|
||||
let typ = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs).unwrap();
|
||||
match typ {
|
||||
// Just move the match into a let term
|
||||
Type::Any | Type::Tup => {
|
||||
let rule = rules.into_iter().next().unwrap();
|
||||
Term::Let { pat: rule.pats.into_iter().next().unwrap(), val: Box::new(arg), nxt: Box::new(rule.body) }
|
||||
}
|
||||
// Detach the variable from the match, converting into a native num match
|
||||
Type::Num => {
|
||||
let mut rules = rules;
|
||||
let Pattern::Num(MatchNum::Succ(Some(var))) =
|
||||
std::mem::replace(&mut rules[1].pats[0], Pattern::Num(MatchNum::Succ(None)))
|
||||
else {
|
||||
unreachable!()
|
||||
};
|
||||
rules[1].body = Term::lam(var, std::mem::take(&mut rules[1].body));
|
||||
Term::Mat { args: vec![arg], rules }
|
||||
}
|
||||
// ADT Encoding depends on compiler option
|
||||
Type::Adt(adt) => {
|
||||
match adt_encoding {
|
||||
// (x @field1 @field2 ... body1 @field1 body2 ...)
|
||||
AdtEncoding::Scott => {
|
||||
let mut arms = vec![];
|
||||
for rule in rules {
|
||||
let body = rule.body;
|
||||
let body = rule.pats[0].binds().rev().fold(body, |bod, nam| Term::named_lam(nam.clone(), bod));
|
||||
arms.push(body);
|
||||
}
|
||||
Term::call(arg, arms)
|
||||
}
|
||||
// #adt_name(x arm[0] arm[1] ...)
|
||||
AdtEncoding::TaggedScott => {
|
||||
let mut arms = vec![];
|
||||
for (rule, (ctr, fields)) in rules.into_iter().zip(&adts[&adt].ctrs) {
|
||||
let body =
|
||||
rule.pats[0].binds().rev().zip(fields.iter().rev()).fold(rule.body, |bod, (var, field)| {
|
||||
Term::tagged_lam(Tag::adt_field(&adt, ctr, field), var.clone(), bod)
|
||||
});
|
||||
arms.push(body);
|
||||
}
|
||||
Term::tagged_call(Tag::adt_name(&adt), arg, arms)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum MatchErr {
|
||||
RepeatedBind(Name),
|
||||
LetPat(Box<MatchErr>),
|
||||
Linearize(Name),
|
||||
NotExhaustive(ExhaustivenessErr),
|
||||
TypeMismatch(Type, Type),
|
||||
ArityMismatch(usize, usize),
|
||||
CtrArityMismatch(Name, usize, usize),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct ExhaustivenessErr(pub Vec<Name>);
|
||||
|
||||
const PATTERN_ERROR_LIMIT: usize = 5;
|
||||
const ERROR_LIMIT_HINT: &str = "Use the --verbose option to see all cases.";
|
||||
|
||||
impl MatchErr {
|
||||
pub fn display(&self, verbose: bool) -> impl std::fmt::Display + '_ {
|
||||
DisplayFn(move |f| match self {
|
||||
MatchErr::RepeatedBind(bind) => write!(f, "Repeated var name in a match block: {}", bind),
|
||||
MatchErr::LetPat(err) => {
|
||||
let let_err = err.to_string().replace("match block", "let bind");
|
||||
write!(f, "{let_err}")?;
|
||||
|
||||
if matches!(err.as_ref(), MatchErr::NotExhaustive(..)) {
|
||||
write!(f, "\nConsider using a match block instead")?;
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
MatchErr::Linearize(var) => write!(f, "Unable to linearize variable {var} in a match block."),
|
||||
MatchErr::NotExhaustive(err) if verbose => write!(f, "{}", err.display_with_limit(usize::MAX)),
|
||||
MatchErr::NotExhaustive(err) => write!(f, "{err}"),
|
||||
MatchErr::TypeMismatch(got, exp) => {
|
||||
write!(f, "Type mismatch in pattern matching. Expected '{exp}', found '{got}'.")
|
||||
}
|
||||
MatchErr::ArityMismatch(got, exp) => {
|
||||
write!(f, "Arity mismatch in pattern matching. Expected {exp} patterns, found {got}.")
|
||||
}
|
||||
MatchErr::CtrArityMismatch(ctr, got, exp) => write!(
|
||||
f,
|
||||
"Constructor arity mismatch in pattern matching. Constructor '{ctr}' expects {exp} fields, found {got}."
|
||||
),
|
||||
val: Box::new(Term::Var { nam: match_var.clone() }),
|
||||
nxt: Box::new(Term::call(arms.next().unwrap(), [Term::Var { nam: Name::from("%fst") }, Term::Var {
|
||||
nam: Name::from("%snd"),
|
||||
}])),
|
||||
},
|
||||
// match x {0: arm[0]; +: arm[1]}
|
||||
Type::Num => Term::Mat {
|
||||
matched: Box::new(Term::Var { nam: match_var.clone() }),
|
||||
arms: vec![
|
||||
(Pattern::Num(MatchNum::Zero), arms.next().unwrap()),
|
||||
(Pattern::Num(MatchNum::Succ(None)), arms.next().unwrap()),
|
||||
],
|
||||
},
|
||||
Type::Adt(adt_name) => match adt_encoding {
|
||||
// (x arm[0] arm[1] ...)
|
||||
AdtEncoding::Scott => Term::call(Term::Var { nam: match_var.clone() }, arms),
|
||||
// #adt_name(x arm[0] arm[1] ...)
|
||||
AdtEncoding::TaggedScott => {
|
||||
Term::tagged_call(Tag::adt_name(adt_name), Term::Var { nam: match_var.clone() }, arms)
|
||||
}
|
||||
},
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
/// Builds the function calling one of the original rule bodies.
|
||||
fn make_leaf_case(
|
||||
book: &Book,
|
||||
rule: &Rule,
|
||||
rule_idx: usize,
|
||||
match_path: Vec<Pattern>,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Term {
|
||||
let (old_args, new_args) = args_from_match_path(&match_path);
|
||||
let args = &mut old_args.iter().chain(new_args.iter()).cloned();
|
||||
|
||||
// The term we're building
|
||||
// Instead of directly pasting the rule body here (or a ref to the rule body),
|
||||
// we instead put a variable that we will substitute later with the correct term.
|
||||
// We do this to normalize the generated term but not the rule body.
|
||||
// TODO: Generate the pattern matching Term already in reduced form to avoid this jank.
|
||||
let term = Term::Var { nam: rule_body_subst_var(rule_idx) };
|
||||
|
||||
// Add the applications to call the rule body
|
||||
let term = match_path.iter().zip(&rule.pats).fold(term, |term, (matched, pat)| {
|
||||
if matched.flat_equals(pat) {
|
||||
matched.vars().fold(term, |term, _| Term::arg_call(term, args.next().unwrap()))
|
||||
} else {
|
||||
// The pattern in this rule was a Var, but we matched on a constructor.
|
||||
// Rebuild the constructor
|
||||
let mut ctr = matched.clone();
|
||||
ctr.vars_mut().for_each(|var| *var = Some(args.next().unwrap()));
|
||||
Term::app(term, ctr.to_term())
|
||||
}
|
||||
});
|
||||
// Add the lambdas for the matched args.
|
||||
let term = add_arg_lams(term, old_args, new_args, match_path.last(), book, adt_encoding);
|
||||
|
||||
term
|
||||
}
|
||||
|
||||
/// Adds the argument lambdas to the term, without considering pattern matching.
|
||||
/// Adds a lambda for each variable in the rule patterns.
|
||||
fn add_non_match_arg_lams(body: Term, pats: &[Pattern]) -> Term {
|
||||
let vars = pats.iter().flat_map(|p| p.vars().cloned());
|
||||
vars.rev().fold(body, |bod, var| Term::lam(var, bod))
|
||||
}
|
||||
|
||||
/// Adds the argument lambdas to the term, with new args followed by old args.
|
||||
fn add_arg_lams(
|
||||
term: Term,
|
||||
old_args: Vec<Name>,
|
||||
new_args: Vec<Name>,
|
||||
last_pat: Option<&Pattern>,
|
||||
book: &Book,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Term {
|
||||
// Add lams for old vars
|
||||
let term = old_args.into_iter().rev().fold(term, |term, arg| Term::named_lam(arg, term));
|
||||
|
||||
// Add lams for new vars, with named tags for Ctr fields
|
||||
match last_pat {
|
||||
// New vars from Ctr
|
||||
Some(Pattern::Ctr(ctr, args)) => {
|
||||
new_args.into_iter().rev().zip(args.iter().rev()).fold(term, |term, (new_arg, pat)| {
|
||||
let adt = &book.ctrs[ctr];
|
||||
let Pattern::Var(Some(field)) = pat else { unreachable!() };
|
||||
match adt_encoding {
|
||||
AdtEncoding::Scott => Term::Lam { tag: Tag::Static, nam: Some(new_arg), bod: Box::new(term) },
|
||||
AdtEncoding::TaggedScott => {
|
||||
Term::Lam { tag: Tag::adt_field(adt, ctr, field), nam: Some(new_arg), bod: Box::new(term) }
|
||||
}
|
||||
}
|
||||
})
|
||||
}
|
||||
// New vars from other pats
|
||||
Some(_) => new_args.into_iter().rev().fold(term, |term, new_arg| Term::named_lam(new_arg, term)),
|
||||
// First arg, no new vars.
|
||||
None => term,
|
||||
impl std::fmt::Display for MatchErr {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "{}", self.display(false))
|
||||
}
|
||||
}
|
||||
|
||||
fn args_from_match_path(match_path: &[Pattern]) -> (Vec<Name>, Vec<Name>) {
|
||||
let (new_match, old_matches) = match_path.split_last().unzip();
|
||||
let old_args: Vec<Name> = old_matches
|
||||
.unwrap_or_default()
|
||||
.iter()
|
||||
.flat_map(|pat| pat.vars())
|
||||
.enumerate()
|
||||
.map(|(i, _)| Name::new(format!("%x{i}")))
|
||||
.collect();
|
||||
let new_args: Vec<Name> = new_match
|
||||
.map(|pat| pat.vars().enumerate().map(|(i, _)| Name::new(format!("%y{i}"))).collect())
|
||||
.unwrap_or(vec![]);
|
||||
(old_args, new_args)
|
||||
}
|
||||
impl ExhaustivenessErr {
|
||||
pub fn display_with_limit(&self, limit: usize) -> String {
|
||||
let ident = ERR_INDENT_SIZE * 2;
|
||||
let hints =
|
||||
self.0.iter().take(limit).map(|pat| format!("{:ident$}Case '{pat}' not covered.", "")).join("\n");
|
||||
|
||||
/* Functions used to normalize generated part of the def */
|
||||
let mut str = format!("Non-exhaustive pattern matching. Hint:\n{}", hints);
|
||||
|
||||
/// Name for a variable to be substituted with the rule body.
|
||||
fn rule_body_subst_var(rule_idx: usize) -> Name {
|
||||
Name::new(format!("%rule_subst_{rule_idx}"))
|
||||
}
|
||||
|
||||
/// Beta reduces a term.
|
||||
/// Assumes a term in the specific format generated by the pass in this file (linear, unique names, at most one let expr in a row).
|
||||
fn beta_reduce(term: &mut Term) {
|
||||
// TODO: Very dumb, slow.
|
||||
while normal_order_step(term) {}
|
||||
}
|
||||
|
||||
/// Tries one reduction in normal order and returns whether something was reduced.
|
||||
fn normal_order_step(term: &mut Term) -> bool {
|
||||
match term {
|
||||
Term::App { tag: app_tag, fun, arg } => {
|
||||
match fun.as_mut() {
|
||||
// #tag (#tag @x bod arg) -> bod/[x -> arg]
|
||||
// #tag (#tag @* bod arg) -> bod
|
||||
Term::Lam { tag: lam_tag, nam, bod } if app_tag == lam_tag => {
|
||||
if let Some(nam) = nam {
|
||||
bod.subst(nam, arg.as_ref());
|
||||
}
|
||||
*term = std::mem::take(bod);
|
||||
true
|
||||
}
|
||||
// Reduce through let expressions.
|
||||
// #tag ( let pat = val; #tag @x bod arg) -> let pat = val; bod/[x -> arg]
|
||||
Term::Let { pat, val, nxt: box Term::Lam { tag: lam_tag, nam, bod } } if app_tag == lam_tag => {
|
||||
if let Some(nam) = nam {
|
||||
bod.subst(nam, arg.as_ref());
|
||||
}
|
||||
*term = Term::Let {
|
||||
pat: std::mem::replace(pat, Pattern::Var(None)),
|
||||
val: std::mem::take(val),
|
||||
nxt: std::mem::take(bod),
|
||||
};
|
||||
true
|
||||
}
|
||||
_ => normal_order_step(fun) || normal_order_step(arg),
|
||||
}
|
||||
let len = self.0.len();
|
||||
if len > limit {
|
||||
str.push_str(&format!(" ... and {} others.\n{:ident$}{}", len - limit, "", ERROR_LIMIT_HINT))
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
if normal_order_step(matched) {
|
||||
return true;
|
||||
}
|
||||
for (_, arm) in arms {
|
||||
if normal_order_step(arm) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
false
|
||||
}
|
||||
Term::Lst { els } => {
|
||||
for el in els {
|
||||
if normal_order_step(el) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
false
|
||||
}
|
||||
Term::Let { val: fst, nxt: snd, .. }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. } => normal_order_step(fst) || normal_order_step(snd),
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => normal_order_step(bod),
|
||||
Term::Var { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Str { .. }
|
||||
| Term::Ref { .. }
|
||||
| Term::Era
|
||||
| Term::Err => false,
|
||||
|
||||
str
|
||||
}
|
||||
}
|
||||
|
||||
/// Substitute one of the rule bodies, while making sure that the generated part is normalized.
|
||||
///
|
||||
/// Example:
|
||||
/// Assume this pattern matching function:
|
||||
/// `(foo (a, b)) = <Rule body>`
|
||||
/// If we substituted the rule body directly onto the generated pattern matching term, we'd get:
|
||||
/// `(foo) = λx let (%fst, %snd) = x; (λa λb <Rule body> %fst %snd)`
|
||||
/// Instead, we want to generate this:
|
||||
/// `(foo) = λx let (%fst, %snd) = x; <Rule body>`
|
||||
fn subst_rule_body(term: &mut Term, subst_var: &Name, body: &Term, name_gen: &mut UniqueNameGenerator) {
|
||||
fn leading_apps(term: &mut Term) -> (&mut Term, usize) {
|
||||
if let Term::App { tag: _, fun, arg: _ } = term {
|
||||
let (term, n_apps) = leading_apps(fun);
|
||||
(term, n_apps + 1)
|
||||
} else {
|
||||
(term, 0)
|
||||
}
|
||||
}
|
||||
|
||||
match term {
|
||||
term @ Term::App { .. } => {
|
||||
// Reduce the surrounding applications.
|
||||
// They should never be more than the lambdas for receiving arguments.
|
||||
let (subst_term, n_apps) = leading_apps(term);
|
||||
if let Term::Var { nam } = subst_term
|
||||
&& nam == subst_var
|
||||
{
|
||||
// Subst and reduce the surrounding application
|
||||
subst_term.subst(subst_var, body);
|
||||
// So that we don't have name conflicts with the generated term.
|
||||
name_gen.unique_names_in_term(subst_term);
|
||||
for _ in 0 .. n_apps {
|
||||
// The arg applications will always be the leftmost outermost.
|
||||
let reduced = normal_order_step(term);
|
||||
debug_assert!(reduced);
|
||||
}
|
||||
} else {
|
||||
// Normal App, not a rule body substitution
|
||||
let Term::App { tag: _, fun, arg } = term else { unreachable!() }; // to appease the borrow checker
|
||||
subst_rule_body(fun, subst_var, body, name_gen);
|
||||
subst_rule_body(arg, subst_var, body, name_gen);
|
||||
}
|
||||
}
|
||||
// Rule body not applied to anything, just subst
|
||||
Term::Var { nam } if nam == subst_var => {
|
||||
term.subst(subst_var, body);
|
||||
}
|
||||
|
||||
Term::Mat { matched, arms } => {
|
||||
subst_rule_body(matched, subst_var, body, name_gen);
|
||||
for (_, arm) in arms {
|
||||
subst_rule_body(arm, subst_var, body, name_gen);
|
||||
}
|
||||
}
|
||||
Term::Lst { els } => {
|
||||
for el in els {
|
||||
subst_rule_body(el, subst_var, body, name_gen);
|
||||
}
|
||||
}
|
||||
Term::Let { val: fst, nxt: snd, .. }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. } => {
|
||||
subst_rule_body(fst, subst_var, body, name_gen);
|
||||
subst_rule_body(snd, subst_var, body, name_gen);
|
||||
}
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => subst_rule_body(bod, subst_var, body, name_gen),
|
||||
Term::Var { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Str { .. }
|
||||
| Term::Ref { .. }
|
||||
| Term::Era
|
||||
| Term::Err => (),
|
||||
impl Display for ExhaustivenessErr {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "{}", self.display_with_limit(PATTERN_ERROR_LIMIT))
|
||||
}
|
||||
}
|
||||
|
@ -3,14 +3,9 @@ use crate::term::*;
|
||||
impl Book {
|
||||
/// Applies eta-reduction to all generated definitions, converting occurrences of `@x (f x)` into just `f`.
|
||||
/// Assumes that variables are linear (used exactly once).
|
||||
pub fn eta_reduction(&mut self, reduce_all: bool) {
|
||||
pub fn eta_reduction(&mut self) {
|
||||
for def in self.defs.values_mut() {
|
||||
let builtin = def.builtin;
|
||||
let rule = def.rule_mut();
|
||||
|
||||
if reduce_all || builtin {
|
||||
rule.body.eta_reduction();
|
||||
}
|
||||
def.rule_mut().body.eta_reduction();
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -54,11 +49,15 @@ impl Term {
|
||||
fst.eta_reduction();
|
||||
snd.eta_reduction();
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.eta_reduction();
|
||||
for (pat, term) in arms {
|
||||
debug_assert!(pat.is_detached_num_match());
|
||||
term.eta_reduction();
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.eta_reduction();
|
||||
}
|
||||
for rule in rules {
|
||||
for pat in &rule.pats {
|
||||
debug_assert!(pat.is_detached_num_match());
|
||||
}
|
||||
rule.body.eta_reduction();
|
||||
}
|
||||
}
|
||||
Term::Lnk { .. }
|
||||
|
@ -1,234 +0,0 @@
|
||||
use crate::{
|
||||
diagnostics::Info,
|
||||
term::{display::DisplayJoin, Ctx, Definition, Name, Pattern, Rule, Term, Type},
|
||||
Warning,
|
||||
};
|
||||
use indexmap::IndexMap;
|
||||
use std::collections::HashSet;
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
/// Extracts adt match terms into pattern matching functions.
|
||||
/// Creates rules with potentially nested patterns, so the flattening pass needs to be called after.
|
||||
pub fn extract_adt_matches(&mut self) -> Result<(), Info> {
|
||||
self.info.start_pass();
|
||||
|
||||
let mut new_defs = Vec::new();
|
||||
|
||||
for (def_name, def) in &mut self.book.defs {
|
||||
for rule in def.rules.iter_mut() {
|
||||
let res = rule.body.extract_adt_matches(
|
||||
def_name,
|
||||
def.builtin,
|
||||
&self.book.ctrs,
|
||||
&mut new_defs,
|
||||
&mut 0,
|
||||
&mut self.info.warns,
|
||||
);
|
||||
|
||||
self.info.take_err(res, Some(&def_name));
|
||||
}
|
||||
}
|
||||
|
||||
self.info.fatal(new_defs).map(|defs| self.book.defs.extend(defs))
|
||||
}
|
||||
}
|
||||
|
||||
impl Term {
|
||||
fn extract_adt_matches(
|
||||
&mut self,
|
||||
def_name: &Name,
|
||||
builtin: bool,
|
||||
ctrs: &IndexMap<Name, Name>,
|
||||
new_defs: &mut Vec<(Name, Definition)>,
|
||||
match_count: &mut usize,
|
||||
warnings: &mut Vec<Warning>,
|
||||
) -> Result<(), MatchErr> {
|
||||
match self {
|
||||
Term::Mat { matched: box Term::Var { .. }, arms } => {
|
||||
let all_vars = arms.iter().all(|(pat, ..)| matches!(pat, Pattern::Var(..)));
|
||||
if all_vars && arms.len() > 1 {
|
||||
warnings.push(Warning::MatchOnlyVars(def_name.clone()));
|
||||
}
|
||||
for (_, term) in arms.iter_mut() {
|
||||
term.extract_adt_matches(def_name, builtin, ctrs, new_defs, match_count, warnings)?;
|
||||
}
|
||||
Term::extract(self, def_name, builtin, ctrs, new_defs, match_count)?;
|
||||
}
|
||||
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
|
||||
bod.extract_adt_matches(def_name, builtin, ctrs, new_defs, match_count, warnings)?;
|
||||
}
|
||||
Term::App { fun: fst, arg: snd, .. }
|
||||
| Term::Let { pat: Pattern::Var(_), val: fst, nxt: snd }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. } => {
|
||||
fst.extract_adt_matches(def_name, builtin, ctrs, new_defs, match_count, warnings)?;
|
||||
snd.extract_adt_matches(def_name, builtin, ctrs, new_defs, match_count, warnings)?;
|
||||
}
|
||||
Term::Var { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Str { .. }
|
||||
| Term::Ref { .. }
|
||||
| Term::Era
|
||||
| Term::Err => {}
|
||||
|
||||
Term::Lst { .. } => unreachable!(),
|
||||
Term::Mat { .. } => unreachable!("Scrutinee of match expression should have been extracted already"),
|
||||
Term::Let { pat, .. } => {
|
||||
unreachable!("Destructor let expression should have been desugared already. {pat}")
|
||||
}
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Term {
|
||||
fn extract(
|
||||
&mut self,
|
||||
def_name: &Name,
|
||||
builtin: bool,
|
||||
ctrs: &IndexMap<Name, Name>,
|
||||
new_defs: &mut Vec<(Name, Definition)>,
|
||||
match_count: &mut usize,
|
||||
) -> Result<(), MatchErr> {
|
||||
match self {
|
||||
Term::Mat { matched: box Term::Var { .. }, arms } => {
|
||||
for (_, body) in arms.iter_mut() {
|
||||
body.extract(def_name, builtin, ctrs, new_defs, match_count)?;
|
||||
}
|
||||
let matched_type = infer_match_type(arms.iter().map(|(x, _)| x), ctrs)?;
|
||||
match matched_type {
|
||||
// Don't extract non-adt matches.
|
||||
Type::None | Type::Any | Type::Num => (),
|
||||
// TODO: Instead of extracting tuple matches, we should flatten one layer and check sub-patterns for something to extract.
|
||||
// For now, to prevent extraction we can use `let (a, b) = ...;`
|
||||
Type::Adt(_) | Type::Tup => {
|
||||
*match_count += 1;
|
||||
let Term::Mat { matched: box Term::Var { nam }, arms } = self else { unreachable!() };
|
||||
*self = match_to_def(nam, arms, def_name, builtin, new_defs, *match_count);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
|
||||
bod.extract(def_name, builtin, ctrs, new_defs, match_count)?;
|
||||
}
|
||||
|
||||
Term::Let { pat: Pattern::Var(..), val: fst, nxt: snd }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. }
|
||||
| Term::App { fun: fst, arg: snd, .. } => {
|
||||
fst.extract(def_name, builtin, ctrs, new_defs, match_count)?;
|
||||
snd.extract(def_name, builtin, ctrs, new_defs, match_count)?;
|
||||
}
|
||||
|
||||
Term::Lst { .. } => unreachable!(),
|
||||
Term::Mat { .. } => unreachable!("Scrutinee of match expression should have been extracted already"),
|
||||
Term::Let { pat, .. } => {
|
||||
unreachable!("Destructor let expression should have been desugared already. {pat}")
|
||||
}
|
||||
|
||||
Term::Str { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Var { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Ref { .. }
|
||||
| Term::Era => {}
|
||||
|
||||
Term::Err => todo!(),
|
||||
};
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
//== Common ==//
|
||||
|
||||
/// Transforms a match into a new definition with every arm of `arms` as a rule.
|
||||
/// The result is the new def applied to the scrutinee followed by the free vars of the arms.
|
||||
fn match_to_def(
|
||||
matched_var: &Name,
|
||||
arms: &[(Pattern, Term)],
|
||||
def_name: &Name,
|
||||
builtin: bool,
|
||||
new_defs: &mut Vec<(Name, Definition)>,
|
||||
match_count: usize,
|
||||
) -> Term {
|
||||
let rules = arms.iter().map(|(pat, term)| Rule { pats: vec![pat.clone()], body: term.clone() }).collect();
|
||||
let new_name = Name::new(format!("{def_name}$match${match_count}"));
|
||||
let def = Definition { name: new_name.clone(), rules, builtin };
|
||||
new_defs.push((new_name.clone(), def));
|
||||
|
||||
Term::arg_call(Term::Ref { nam: new_name }, matched_var.clone())
|
||||
}
|
||||
|
||||
/// Finds the expected type of the matched argument.
|
||||
/// Errors on incompatible types.
|
||||
/// Short-circuits if the first pattern is Type::Any.
|
||||
pub fn infer_match_type<'a>(
|
||||
pats: impl Iterator<Item = &'a Pattern>,
|
||||
ctrs: &IndexMap<Name, Name>,
|
||||
) -> Result<Type, MatchErr> {
|
||||
let mut match_type = Type::None;
|
||||
for pat in pats {
|
||||
let new_type = pat.to_type(ctrs);
|
||||
match (new_type, &mut match_type) {
|
||||
(new, Type::None) => match_type = new,
|
||||
// TODO: Should we throw a type inference error in this case?
|
||||
// Since anything else will be sort of the wrong type (expected Var).
|
||||
(_, Type::Any) => (),
|
||||
(Type::Any, _) => (),
|
||||
(Type::Tup, Type::Tup) => (),
|
||||
(Type::Num, Type::Num) => (),
|
||||
(Type::Adt(nam_new), Type::Adt(nam_old)) if &nam_new == nam_old => (),
|
||||
(new, old) => return Err(MatchErr::Infer(new, old.clone())),
|
||||
};
|
||||
}
|
||||
Ok(match_type)
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub enum MatchErr {
|
||||
Empty,
|
||||
Infer(Type, Type),
|
||||
Repeated(Name),
|
||||
Missing(HashSet<Name>),
|
||||
LetPat(Box<MatchErr>),
|
||||
Linearize(Name),
|
||||
}
|
||||
|
||||
impl std::fmt::Display for MatchErr {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
fn ctrs_plural_or_sing(n: usize) -> &'static str {
|
||||
if n > 1 { "constructors" } else { "a constructor" }
|
||||
}
|
||||
|
||||
match self {
|
||||
MatchErr::Empty => write!(f, "Empty match block found"),
|
||||
MatchErr::Infer(new, old) => write!(f, "Type mismatch. Found '{}' expected {}.", new, old),
|
||||
MatchErr::Repeated(bind) => write!(f, "Repeated var name in a match block: {}", bind),
|
||||
MatchErr::Missing(names) => {
|
||||
let constructor = ctrs_plural_or_sing(names.len());
|
||||
let missing = DisplayJoin(|| names.iter(), ", ");
|
||||
write!(f, "Missing {constructor} in a match block: {missing}")
|
||||
}
|
||||
MatchErr::LetPat(err) => {
|
||||
let let_err = err.to_string().replace("match block", "let bind");
|
||||
write!(f, "{let_err}")?;
|
||||
|
||||
if matches!(err.as_ref(), MatchErr::Missing(_)) {
|
||||
write!(f, "\nConsider using a match block instead")?;
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
MatchErr::Linearize(var) => write!(f, "Unable to linearize variable {var} in a match block."),
|
||||
}
|
||||
}
|
||||
}
|
@ -1,241 +0,0 @@
|
||||
use std::collections::HashSet;
|
||||
|
||||
use crate::term::{Book, Definition, MatchNum, Name, Op, Pattern, Rule, Term};
|
||||
|
||||
impl Book {
|
||||
pub fn flatten_rules(&mut self) {
|
||||
let mut new_defs = vec![];
|
||||
for def in self.defs.values() {
|
||||
// Since these definitions don't need further processing it's fine to insert them all at the end.
|
||||
new_defs.append(&mut flatten_def(def));
|
||||
}
|
||||
for def in new_defs {
|
||||
self.defs.insert(def.name.clone(), def);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Splits a definition with nested rule patterns into a tree of definitions
|
||||
/// with flat patterns, each matching a single layer of patterns.
|
||||
fn flatten_def(def: &Definition) -> Vec<Definition> {
|
||||
let mut skip: HashSet<usize> = HashSet::new();
|
||||
let mut new_defs: Vec<Definition> = vec![];
|
||||
|
||||
// We rebuild this definition rule by rule, with non-nested patterns
|
||||
let mut old_def = Definition { name: def.name.clone(), rules: vec![], builtin: def.builtin };
|
||||
|
||||
for i in 0 .. def.rules.len() {
|
||||
if skip.contains(&i) {
|
||||
continue;
|
||||
}
|
||||
|
||||
let rule = &def.rules[i];
|
||||
let must_split = rule.pats.iter().any(|pat| !pat.is_flat());
|
||||
if must_split {
|
||||
// Create the entry for the new definition name
|
||||
let old_name = &def.name;
|
||||
let new_name = Name::new(format!("{}$F{}", old_name, new_defs.len()));
|
||||
|
||||
// Create the rule that replaces the one being flattened.
|
||||
// Destructs one layer of the nested patterns and calls the following, forwarding the extracted fields.
|
||||
let old_rule = make_old_rule(rule, new_name.clone());
|
||||
old_def.rules.push(old_rule);
|
||||
|
||||
// Create a new definition, with one rule for each rule that overlaps patterns with this one (including itself)
|
||||
// The rule patterns have one less layer of nesting and receive the destructed fields as extra args.
|
||||
let mut new_rules = vec![];
|
||||
for (j, other) in def.rules.iter().enumerate().skip(i) {
|
||||
let share_matches = rule.pats.iter().zip(&other.pats).all(|(a, b)| a.shares_matches_with(b));
|
||||
if share_matches {
|
||||
let new_rule = make_split_rule(rule, other);
|
||||
new_rules.push(new_rule);
|
||||
|
||||
// Skip clauses that are already 100% covered by this one.
|
||||
// TODO: This is not enough to skip rules that are redundant but not a subset of any particular other rule.
|
||||
// This means that it will sometimes generate redundant, unused rules.
|
||||
let other_is_subset = other.pats.iter().zip(&rule.pats).all(|(a, b)| a.is_flat_subset_of(b));
|
||||
if other_is_subset {
|
||||
skip.insert(j);
|
||||
}
|
||||
}
|
||||
}
|
||||
let new_def = Definition { name: new_name, rules: new_rules, builtin: def.builtin };
|
||||
// Recursively split the newly created def
|
||||
for def in flatten_def(&new_def) {
|
||||
new_defs.push(def);
|
||||
}
|
||||
} else {
|
||||
// If this rule is already flat, just mark it to be inserted back as it is.
|
||||
old_def.rules.push(def.rules[i].clone());
|
||||
}
|
||||
}
|
||||
new_defs.push(old_def);
|
||||
new_defs
|
||||
}
|
||||
|
||||
/// Makes the rule that replaces the original.
|
||||
/// The new version of the rule is flat and calls the next layer of pattern matching.
|
||||
fn make_old_rule(rule: &Rule, split_def: Name) -> Rule {
|
||||
//(Foo Tic (Bar a b) (Haz c d)) = A
|
||||
//(Foo Tic x y) = B
|
||||
//---------------------------------
|
||||
//(Foo Tic (Bar a b) (Haz c d)) = B[x <- (Bar a b), y <- (Haz c d)]
|
||||
//
|
||||
//(Foo.0 a b c d) = ...
|
||||
let mut new_pats = Vec::new();
|
||||
let mut new_body_args = Vec::new();
|
||||
let mut var_count = 0;
|
||||
|
||||
for arg in &rule.pats {
|
||||
match arg {
|
||||
Pattern::Ctr(arg_name, arg_args) => {
|
||||
let mut new_arg_args = Vec::new();
|
||||
for _ in arg_args {
|
||||
let var_name = make_var_name(&mut var_count);
|
||||
new_arg_args.push(Pattern::Var(Some(var_name.clone())));
|
||||
new_body_args.push(Term::Var { nam: var_name });
|
||||
}
|
||||
new_pats.push(Pattern::Ctr(arg_name.clone(), new_arg_args));
|
||||
}
|
||||
Pattern::Tup(_, _) => {
|
||||
let fst = make_var_name(&mut var_count);
|
||||
let snd = make_var_name(&mut var_count);
|
||||
new_body_args.push(Term::Var { nam: fst.clone() });
|
||||
new_body_args.push(Term::Var { nam: snd.clone() });
|
||||
let fst = Pattern::Var(Some(fst));
|
||||
let snd = Pattern::Var(Some(snd));
|
||||
new_pats.push(Pattern::Tup(Box::new(fst), Box::new(snd)));
|
||||
}
|
||||
Pattern::Var(_) => {
|
||||
let var_name = make_var_name(&mut var_count);
|
||||
new_body_args.push(Term::Var { nam: var_name.clone() });
|
||||
new_pats.push(Pattern::Var(Some(var_name)));
|
||||
}
|
||||
|
||||
Pattern::Num(MatchNum::Zero) => {
|
||||
new_pats.push(Pattern::Num(MatchNum::Zero));
|
||||
}
|
||||
Pattern::Num(MatchNum::Succ(Some(_))) => {
|
||||
// Always flat, just pass on the variable
|
||||
let var_name = make_var_name(&mut var_count);
|
||||
new_body_args.push(Term::Var { nam: var_name.clone() });
|
||||
new_pats.push(Pattern::Num(MatchNum::Succ(Some(Some(var_name)))));
|
||||
}
|
||||
Pattern::Num(MatchNum::Succ(None)) => unreachable!(),
|
||||
Pattern::Lst(..) => unreachable!(),
|
||||
}
|
||||
}
|
||||
let new_body = Term::call(Term::Ref { nam: split_def }, new_body_args);
|
||||
Rule { pats: new_pats, body: new_body }
|
||||
}
|
||||
|
||||
/// Makes one of the new rules, flattening one layer of the original pattern.
|
||||
fn make_split_rule(old_rule: &Rule, other_rule: &Rule) -> Rule {
|
||||
// (Foo a (B x P) (C y0 y1)) = F
|
||||
// (Foo (A k) (B x Q) y ) = G
|
||||
// -----------------------------
|
||||
// (Foo a (B x u) (C y0 y1)) = (Foo.0 a x u y0 y1)
|
||||
// (Foo.0 a x P y0 y1) = F
|
||||
// (Foo.0 (A k) x Q f0 f1) = G [y <- (C f0 f1)] // f0 and f1 are fresh
|
||||
let mut new_pats = Vec::new();
|
||||
let mut new_body = other_rule.body.clone();
|
||||
let mut var_count = 0;
|
||||
for (rule_arg, other_arg) in old_rule.pats.iter().zip(&other_rule.pats) {
|
||||
match (rule_arg, other_arg) {
|
||||
// Two rules with same constructor
|
||||
(Pattern::Ctr(_, _), Pattern::Ctr(_, other_arg_args)) => {
|
||||
// We checked before that these two have the same constructor and match together
|
||||
for other_field in other_arg_args {
|
||||
new_pats.push(other_field.clone());
|
||||
}
|
||||
}
|
||||
(Pattern::Num(MatchNum::Zero), Pattern::Num(MatchNum::Zero)) => {
|
||||
// No internal fields, so nothing to forward
|
||||
}
|
||||
(Pattern::Num(MatchNum::Succ(_)), Pattern::Num(MatchNum::Succ(Some(nam)))) => {
|
||||
new_pats.push(Pattern::Var(nam.clone()))
|
||||
}
|
||||
(Pattern::Tup(_, _), Pattern::Tup(fst, snd)) => {
|
||||
new_pats.push(*fst.clone());
|
||||
new_pats.push(*snd.clone());
|
||||
}
|
||||
|
||||
// First rule has constructor, second has used var
|
||||
(Pattern::Ctr(rule_arg_name, rule_arg_args), Pattern::Var(Some(other_arg))) => {
|
||||
let mut new_ctr_args = vec![];
|
||||
for _ in 0 .. rule_arg_args.len() {
|
||||
let new_nam = make_var_name(&mut var_count);
|
||||
new_ctr_args.push(Term::Var { nam: new_nam.clone() });
|
||||
new_pats.push(Pattern::Var(Some(new_nam)));
|
||||
}
|
||||
let def_ref = Term::r#ref(rule_arg_name);
|
||||
let new_ctr = Term::call(def_ref, new_ctr_args);
|
||||
new_body.subst(other_arg, &new_ctr);
|
||||
}
|
||||
(Pattern::Num(MatchNum::Zero), Pattern::Var(Some(other_arg))) => {
|
||||
let new_ctr = Term::Num { val: 0 };
|
||||
new_body.subst(other_arg, &new_ctr);
|
||||
}
|
||||
(Pattern::Num(MatchNum::Succ(Some(_))), Pattern::Var(Some(other_arg))) => {
|
||||
// Since the other rule used the entire number, we have to recover it after the decrementing.
|
||||
let new_nam = make_var_name(&mut var_count);
|
||||
let new_var = Term::Var { nam: new_nam.clone() };
|
||||
new_pats.push(Pattern::Var(Some(new_nam)));
|
||||
let new_ctr = Term::Opx { op: Op::ADD, fst: Box::new(new_var), snd: Box::new(Term::Num { val: 1 }) };
|
||||
new_body.subst(other_arg, &new_ctr);
|
||||
}
|
||||
(Pattern::Tup(..), Pattern::Var(Some(other_arg))) => {
|
||||
let fst_nam = make_var_name(&mut var_count);
|
||||
let snd_nam = make_var_name(&mut var_count);
|
||||
let fst_arg = Term::Var { nam: fst_nam.clone() };
|
||||
let snd_arg = Term::Var { nam: snd_nam.clone() };
|
||||
new_pats.push(Pattern::Var(Some(fst_nam)));
|
||||
new_pats.push(Pattern::Var(Some(snd_nam)));
|
||||
let new_ctr = Term::Tup { fst: Box::new(fst_arg), snd: Box::new(snd_arg) };
|
||||
new_body.subst(other_arg, &new_ctr);
|
||||
}
|
||||
|
||||
// First rule has constructor, second has erased var.
|
||||
(Pattern::Ctr(_, ctr_fields), Pattern::Var(None)) => {
|
||||
for _ in ctr_fields {
|
||||
new_pats.push(Pattern::Var(None));
|
||||
}
|
||||
}
|
||||
(Pattern::Num(MatchNum::Zero), Pattern::Var(None)) => {
|
||||
// Nothing to pass forward
|
||||
}
|
||||
(Pattern::Num(MatchNum::Succ(_)), Pattern::Var(None)) => {
|
||||
new_pats.push(Pattern::Var(None));
|
||||
}
|
||||
(Pattern::Tup(..), Pattern::Var(None)) => {
|
||||
new_pats.push(Pattern::Var(None));
|
||||
new_pats.push(Pattern::Var(None));
|
||||
}
|
||||
|
||||
// First rule has var.
|
||||
(Pattern::Var(_), _) => new_pats.push(other_arg.clone()),
|
||||
|
||||
// Unreachable cases
|
||||
// We only call this function if we know the two patterns match together
|
||||
(
|
||||
Pattern::Ctr(..) | Pattern::Num(..) | Pattern::Tup(..),
|
||||
Pattern::Ctr(..) | Pattern::Num(..) | Pattern::Tup(..),
|
||||
) => {
|
||||
unreachable!()
|
||||
}
|
||||
(Pattern::Num(MatchNum::Succ(None)), _) => unreachable!(
|
||||
"In pattern matching function position, number patterns can't have their lambda detached"
|
||||
),
|
||||
(Pattern::Lst(..), _) | (_, Pattern::Lst(..)) => {
|
||||
unreachable!("List syntax should have been already desugared")
|
||||
}
|
||||
}
|
||||
}
|
||||
Rule { pats: new_pats, body: new_body }
|
||||
}
|
||||
|
||||
fn make_var_name(var_count: &mut usize) -> Name {
|
||||
let nam = format!("%x{var_count}");
|
||||
*var_count += 1;
|
||||
Name::new(nam)
|
||||
}
|
@ -43,9 +43,9 @@ impl Term {
|
||||
to_inline.push(snd);
|
||||
}
|
||||
|
||||
Term::Mat { arms, .. } => {
|
||||
for (_, bod) in arms {
|
||||
to_inline.push(bod);
|
||||
Term::Mat { rules, .. } => {
|
||||
for rule in rules {
|
||||
to_inline.push(&mut rule.body);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1,21 +1,21 @@
|
||||
use super::extract_adt_matches::{infer_match_type, MatchErr};
|
||||
use super::encode_pattern_matching::MatchErr;
|
||||
use crate::{
|
||||
diagnostics::Info,
|
||||
term::{Ctx, Name, Pattern, Term, Type},
|
||||
term::{check::type_check::infer_type, Constructors, Ctx, Name, Pattern, Term, Type},
|
||||
};
|
||||
use indexmap::{IndexMap, IndexSet};
|
||||
use indexmap::IndexSet;
|
||||
use itertools::Itertools;
|
||||
use std::collections::BTreeSet;
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
pub fn linearize_matches(&mut self) -> Result<(), Info> {
|
||||
impl Ctx<'_> {
|
||||
/// Linearizes the variables between match cases, transforming them into combinators when possible.
|
||||
pub fn linearize_simple_matches(&mut self) -> Result<(), Info> {
|
||||
self.info.start_pass();
|
||||
|
||||
for (def_name, def) in &mut self.book.defs {
|
||||
for (def_name, def) in self.book.defs.iter_mut() {
|
||||
for rule in def.rules.iter_mut() {
|
||||
let res = rule.body.linearize_matches(&self.book.ctrs);
|
||||
|
||||
self.info.take_err(res, Some(&def_name));
|
||||
let res = rule.body.linearize_simple_matches(&self.book.ctrs);
|
||||
self.info.take_err(res, Some(def_name));
|
||||
}
|
||||
}
|
||||
|
||||
@ -24,26 +24,23 @@ impl<'book> Ctx<'book> {
|
||||
}
|
||||
|
||||
impl Term {
|
||||
fn linearize_matches(&mut self, ctrs: &IndexMap<Name, Name>) -> Result<(), MatchErr> {
|
||||
fn linearize_simple_matches(&mut self, ctrs: &Constructors) -> Result<(), MatchErr> {
|
||||
match self {
|
||||
Term::Mat { matched: box Term::Var { .. }, arms } => {
|
||||
for (_, body) in arms.iter_mut() {
|
||||
body.linearize_matches(ctrs).unwrap();
|
||||
Term::Mat { args: _, rules } => {
|
||||
for rule in rules.iter_mut() {
|
||||
rule.body.linearize_simple_matches(ctrs).unwrap();
|
||||
}
|
||||
let matched_type = infer_match_type(arms.iter().map(|(x, _)| x), ctrs)?;
|
||||
let matched_type = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs)?;
|
||||
match matched_type {
|
||||
// Don't linearize non-adt matches.
|
||||
Type::None | Type::Any => (),
|
||||
Type::Num => _ = linearize_match_free_vars(self),
|
||||
Type::Adt(_) | Type::Tup => {
|
||||
let match_term = linearize_match_unscoped_vars(self)?;
|
||||
linearize_match_free_vars(match_term);
|
||||
Type::Num | Type::Tup | Type::Any => _ = linearize_match_free_vars(self),
|
||||
Type::Adt(_) => {
|
||||
linearize_match_free_vars(self);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
|
||||
bod.linearize_matches(ctrs)?;
|
||||
bod.linearize_simple_matches(ctrs)?;
|
||||
}
|
||||
|
||||
Term::Let { pat: Pattern::Var(..), val: fst, nxt: snd }
|
||||
@ -52,12 +49,11 @@ impl Term {
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. }
|
||||
| Term::App { fun: fst, arg: snd, .. } => {
|
||||
fst.linearize_matches(ctrs)?;
|
||||
snd.linearize_matches(ctrs)?;
|
||||
fst.linearize_simple_matches(ctrs)?;
|
||||
snd.linearize_simple_matches(ctrs)?;
|
||||
}
|
||||
|
||||
Term::Lst { .. } => unreachable!(),
|
||||
Term::Mat { .. } => unreachable!("Scrutinee of match expression should have been extracted already"),
|
||||
Term::Let { pat, .. } => {
|
||||
unreachable!("Destructor let expression should have been desugared already. {pat}")
|
||||
}
|
||||
@ -79,18 +75,20 @@ impl Term {
|
||||
/// Converts free vars inside the match arms into lambdas with applications to give them the external value.
|
||||
/// Makes the rules extractable and linear (no need for dups when variable used in both rules)
|
||||
pub fn linearize_match_free_vars(match_term: &mut Term) -> &mut Term {
|
||||
let Term::Mat { matched: _, arms } = match_term else { unreachable!() };
|
||||
let Term::Mat { args: _, rules } = match_term else { unreachable!() };
|
||||
// Collect the vars.
|
||||
// We need consistent iteration order.
|
||||
let free_vars: BTreeSet<Name> = arms
|
||||
let free_vars: BTreeSet<Name> = rules
|
||||
.iter()
|
||||
.flat_map(|(pat, term)| term.free_vars().into_keys().filter(|k| !pat.names().contains(k)))
|
||||
.flat_map(|r| {
|
||||
r.body.free_vars().into_keys().filter(|k| !r.pats.iter().flat_map(|p| p.binds()).contains(k))
|
||||
})
|
||||
.collect();
|
||||
|
||||
// Add lambdas to the arms
|
||||
for (_, body) in arms {
|
||||
let old_body = std::mem::take(body);
|
||||
*body = free_vars.iter().rev().fold(old_body, |body, var| Term::named_lam(var.clone(), body));
|
||||
for rule in rules {
|
||||
let old_body = std::mem::take(&mut rule.body);
|
||||
rule.body = free_vars.iter().rev().fold(old_body, |body, var| Term::named_lam(var.clone(), body));
|
||||
}
|
||||
|
||||
// Add apps to the match
|
||||
@ -101,11 +99,11 @@ pub fn linearize_match_free_vars(match_term: &mut Term) -> &mut Term {
|
||||
}
|
||||
|
||||
pub fn linearize_match_unscoped_vars(match_term: &mut Term) -> Result<&mut Term, MatchErr> {
|
||||
let Term::Mat { matched: _, arms } = match_term else { unreachable!() };
|
||||
let Term::Mat { args: _, rules } = match_term else { unreachable!() };
|
||||
// Collect the vars
|
||||
let mut free_vars = IndexSet::new();
|
||||
for (_, arm) in arms.iter_mut() {
|
||||
let (decls, uses) = arm.unscoped_vars();
|
||||
for rule in rules.iter_mut() {
|
||||
let (decls, uses) = rule.body.unscoped_vars();
|
||||
// Not allowed to declare unscoped var and not use it since we need to extract the match arm.
|
||||
if let Some(var) = decls.difference(&uses).next() {
|
||||
return Err(MatchErr::Linearize(Name::new(format!("λ${var}"))));
|
||||
@ -113,15 +111,15 @@ pub fn linearize_match_unscoped_vars(match_term: &mut Term) -> Result<&mut Term,
|
||||
// Change unscoped var to normal scoped var if it references something outside this match arm.
|
||||
let arm_free_vars = uses.difference(&decls);
|
||||
for var in arm_free_vars.clone() {
|
||||
arm.subst_unscoped(var, &Term::Var { nam: Name::new(format!("%match%unscoped%{var}")) });
|
||||
rule.body.subst_unscoped(var, &Term::Var { nam: Name::new(format!("%match%unscoped%{var}")) });
|
||||
}
|
||||
free_vars.extend(arm_free_vars.cloned());
|
||||
}
|
||||
|
||||
// Add lambdas to the arms
|
||||
for (_, body) in arms {
|
||||
let old_body = std::mem::take(body);
|
||||
*body = free_vars
|
||||
for rule in rules {
|
||||
let old_body = std::mem::take(&mut rule.body);
|
||||
rule.body = free_vars
|
||||
.iter()
|
||||
.rev()
|
||||
.fold(old_body, |body, var| Term::named_lam(Name::new(format!("%match%unscoped%{var}")), body));
|
||||
|
@ -1,4 +1,4 @@
|
||||
use crate::term::{Book, MatchNum, Name, Pattern, Tag, Term};
|
||||
use crate::term::{Book, Name, Pattern, Tag, Term};
|
||||
use std::collections::HashMap;
|
||||
|
||||
/// Erases variables that weren't used, dups the ones that were used more than once.
|
||||
@ -35,18 +35,24 @@ impl Term {
|
||||
}
|
||||
|
||||
/// Var-declaring terms
|
||||
fn term_with_bind_to_affine(term: &mut Term, nam: &mut Option<Name>, inst_count: &mut HashMap<Name, u64>) {
|
||||
fn term_with_binds_to_affine<'a>(
|
||||
term: &mut Term,
|
||||
nams: impl IntoIterator<Item = &'a mut Option<Name>>,
|
||||
inst_count: &mut HashMap<Name, u64>,
|
||||
) {
|
||||
term_to_affine(term, inst_count);
|
||||
|
||||
if nam.is_some() {
|
||||
let instantiated_count = get_var_uses(nam.as_ref(), inst_count);
|
||||
duplicate_lam(nam, term, instantiated_count);
|
||||
for nam in nams {
|
||||
if nam.is_some() {
|
||||
let instantiated_count = get_var_uses(nam.as_ref(), inst_count);
|
||||
duplicate_lam(nam, term, instantiated_count);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn term_to_affine(term: &mut Term, inst_count: &mut HashMap<Name, u64>) {
|
||||
match term {
|
||||
Term::Lam { nam, bod, .. } => term_with_bind_to_affine(bod, nam, inst_count),
|
||||
Term::Lam { nam, bod, .. } => term_with_binds_to_affine(bod, [nam], inst_count),
|
||||
|
||||
Term::Let { pat: Pattern::Var(Some(nam)), val, nxt } => {
|
||||
term_to_affine(nxt, inst_count);
|
||||
@ -115,16 +121,13 @@ fn term_to_affine(term: &mut Term, inst_count: &mut HashMap<Name, u64>) {
|
||||
term_to_affine(snd, inst_count);
|
||||
}
|
||||
|
||||
Term::Mat { matched, arms } => {
|
||||
term_to_affine(matched, inst_count);
|
||||
for (rule, term) in arms {
|
||||
match rule {
|
||||
Pattern::Num(MatchNum::Succ(Some(nam))) => {
|
||||
term_with_bind_to_affine(term, nam, inst_count);
|
||||
}
|
||||
Pattern::Num(_) => term_to_affine(term, inst_count),
|
||||
_ => unreachable!(),
|
||||
}
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
term_to_affine(arg, inst_count);
|
||||
}
|
||||
for rule in rules {
|
||||
let nams = rule.pats.iter_mut().flat_map(|p| p.bind_or_eras_mut());
|
||||
term_with_binds_to_affine(&mut rule.body, nams, inst_count)
|
||||
}
|
||||
}
|
||||
|
||||
@ -154,9 +157,7 @@ fn make_dup_tree(nam: &Name, nxt: &mut Term, uses: u64, mut dup_body: Option<&mu
|
||||
fst: Some(dup_name(nam, i)),
|
||||
snd: if i == uses - 1 { Some(dup_name(nam, uses)) } else { Some(internal_dup_name(nam, i)) },
|
||||
val: if i == 1 {
|
||||
Box::new(
|
||||
dup_body.as_deref_mut().map_or_else(|| Term::Var { nam: nam.clone() }, |x| std::mem::take(x)),
|
||||
)
|
||||
Box::new(dup_body.as_mut().map_or_else(|| Term::Var { nam: nam.clone() }, |x| std::mem::take(x)))
|
||||
} else {
|
||||
Box::new(Term::Var { nam: internal_dup_name(nam, i - 1) })
|
||||
},
|
37
src/term/transform/match_defs_to_term.rs
Normal file
37
src/term/transform/match_defs_to_term.rs
Normal file
@ -0,0 +1,37 @@
|
||||
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.
|
||||
///
|
||||
/// 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>) -> 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 }
|
||||
}
|
||||
}
|
@ -6,16 +6,15 @@ pub mod detach_supercombinators;
|
||||
pub mod encode_adts;
|
||||
pub mod encode_pattern_matching;
|
||||
pub mod eta_reduction;
|
||||
pub mod extract_adt_matches;
|
||||
pub mod flatten;
|
||||
pub mod inline;
|
||||
pub mod linearize;
|
||||
pub mod linearize_matches;
|
||||
pub mod normalize_native_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;
|
||||
|
@ -1,160 +0,0 @@
|
||||
use indexmap::IndexMap;
|
||||
|
||||
use super::extract_adt_matches::{infer_match_type, MatchErr};
|
||||
use crate::{
|
||||
diagnostics::Info,
|
||||
term::{Ctx, MatchNum, Name, Op, Pattern, Tag, Term, Type},
|
||||
};
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
/// Converts tuple and var matches into let expressions,
|
||||
/// makes num matches have exactly one rule for zero and one rule for succ.
|
||||
/// Should be run after pattern matching functions are desugared.
|
||||
pub fn normalize_native_matches(&mut self) -> Result<(), Info> {
|
||||
self.info.start_pass();
|
||||
|
||||
for (def_name, def) in self.book.defs.iter_mut() {
|
||||
let res = def.rule_mut().body.normalize_native_matches(&self.book.ctrs);
|
||||
self.info.take_err(res, Some(&def_name));
|
||||
}
|
||||
|
||||
self.info.fatal(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Term {
|
||||
fn normalize_native_matches(&mut self, ctrs: &IndexMap<Name, Name>) -> Result<(), MatchErr> {
|
||||
match self {
|
||||
Term::Mat { matched: box Term::Var { nam }, arms } => {
|
||||
for (_, body) in arms.iter_mut() {
|
||||
body.normalize_native_matches(ctrs)?;
|
||||
}
|
||||
let matched_type = infer_match_type(arms.iter().map(|(x, _)| x), ctrs)?;
|
||||
match matched_type {
|
||||
Type::None => {
|
||||
return Err(MatchErr::Empty);
|
||||
}
|
||||
// This match is useless, will always go with the first rule.
|
||||
// TODO: Throw a warning in this case
|
||||
Type::Any => {
|
||||
// Inside the match we renamed the variable, so we need to restore the name before the match to remove it.
|
||||
let fst_arm = &mut arms[0];
|
||||
let Pattern::Var(var) = &fst_arm.0 else { unreachable!() };
|
||||
let body = &mut fst_arm.1;
|
||||
if let Some(var) = var {
|
||||
body.subst(var, &Term::Var { nam: nam.clone() });
|
||||
}
|
||||
*self = std::mem::take(body);
|
||||
}
|
||||
// TODO: Don't extract tup matches earlier, only flatten earlier and then deal with them here.
|
||||
Type::Tup => unreachable!(),
|
||||
// Matching on nums is a primitive operation, we can leave it as is.
|
||||
// Not extracting into a separate definition allows us to create very specific inets with the MATCH node.
|
||||
Type::Num => normalize_num_match(self)?,
|
||||
Type::Adt(_) => unreachable!("Adt match expressions should have been removed earlier"),
|
||||
}
|
||||
}
|
||||
Term::Mat { .. } => unreachable!("Scrutinee of match expression should have been extracted already"),
|
||||
Term::Let { val: fst, nxt: snd, .. }
|
||||
| Term::App { fun: fst, arg: snd, .. }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. } => {
|
||||
fst.normalize_native_matches(ctrs)?;
|
||||
snd.normalize_native_matches(ctrs)?;
|
||||
}
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
|
||||
bod.normalize_native_matches(ctrs)?;
|
||||
}
|
||||
Term::Var { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Str { .. }
|
||||
| Term::Ref { .. }
|
||||
| Term::Era
|
||||
| Term::Err => (),
|
||||
Term::Lst { .. } => unreachable!(),
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
/// Transforms a match on Num with any possible patterns into 'match x {0: ...; +: @x-1 ...}'.
|
||||
fn normalize_num_match(term: &mut Term) -> Result<(), MatchErr> {
|
||||
let Term::Mat { matched: _, arms } = term else { unreachable!() };
|
||||
|
||||
let mut zero_arm = None;
|
||||
for (pat, body) in arms.iter_mut() {
|
||||
match pat {
|
||||
Pattern::Num(MatchNum::Zero) => {
|
||||
zero_arm = Some((Pattern::Num(MatchNum::Zero), std::mem::take(body)));
|
||||
break;
|
||||
}
|
||||
Pattern::Var(var) => {
|
||||
if let Some(var) = var {
|
||||
body.subst(var, &Term::Num { val: 0 });
|
||||
}
|
||||
zero_arm = Some((Pattern::Num(MatchNum::Zero), std::mem::take(body)));
|
||||
break;
|
||||
}
|
||||
Pattern::Num(_) => (),
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
||||
let mut succ_arm = None;
|
||||
for (pat, body) in arms.iter_mut() {
|
||||
match pat {
|
||||
// Var already detached.
|
||||
// match x {0: ...; +: ...}
|
||||
Pattern::Num(MatchNum::Succ(None)) => {
|
||||
let body = std::mem::take(body);
|
||||
succ_arm = Some((Pattern::Num(MatchNum::Succ(None)), body));
|
||||
break;
|
||||
}
|
||||
// Need to detach var.
|
||||
// match x {0: ...; +: @x-1 ...}
|
||||
Pattern::Num(MatchNum::Succ(Some(var))) => {
|
||||
let body = Term::Lam { tag: Tag::Static, nam: var.clone(), bod: Box::new(std::mem::take(body)) };
|
||||
succ_arm = Some((Pattern::Num(MatchNum::Succ(None)), body));
|
||||
break;
|
||||
}
|
||||
// Need to detach and increment again.
|
||||
// match x {0: ...; +: @x-1 let x = (+ x-1 1); ...}
|
||||
Pattern::Var(Some(var)) => {
|
||||
let body = Term::Let {
|
||||
pat: Pattern::Var(Some(var.clone())),
|
||||
val: Box::new(Term::Opx {
|
||||
op: Op::ADD,
|
||||
fst: Box::new(Term::Var { nam: Name::from("%pred") }),
|
||||
snd: Box::new(Term::Num { val: 1 }),
|
||||
}),
|
||||
nxt: Box::new(std::mem::take(body)),
|
||||
};
|
||||
|
||||
let body = Term::named_lam(Name::from("%pred"), body);
|
||||
succ_arm = Some((Pattern::Num(MatchNum::Succ(None)), body));
|
||||
break;
|
||||
}
|
||||
// Var unused, so no need to increment
|
||||
// match x {0: ...; +: @* ...}
|
||||
Pattern::Var(None) => {
|
||||
let body = Term::erased_lam(std::mem::take(body));
|
||||
succ_arm = Some((Pattern::Num(MatchNum::Succ(None)), body));
|
||||
break;
|
||||
}
|
||||
Pattern::Num(_) => (),
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
||||
let Some(zero_arm) = zero_arm else {
|
||||
return Err(MatchErr::Missing(["0".into()].into()));
|
||||
};
|
||||
let Some(succ_arm) = succ_arm else {
|
||||
return Err(MatchErr::Missing(["+".into()].into()));
|
||||
};
|
||||
*arms = vec![zero_arm, succ_arm];
|
||||
Ok(())
|
||||
}
|
@ -40,6 +40,7 @@ impl Pattern {
|
||||
to_resolve.push(fst);
|
||||
to_resolve.push(snd);
|
||||
}
|
||||
Pattern::Err => unreachable!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -56,11 +57,15 @@ impl Term {
|
||||
to_resolve.push(val);
|
||||
to_resolve.push(nxt);
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
to_resolve.push(matched);
|
||||
for (pat, body) in arms {
|
||||
pat.resolve_ctrs(is_ctr);
|
||||
to_resolve.push(body);
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
to_resolve.push(arg);
|
||||
}
|
||||
for rule in rules {
|
||||
for pat in &mut rule.pats {
|
||||
pat.resolve_ctrs(is_ctr);
|
||||
}
|
||||
to_resolve.push(&mut rule.body);
|
||||
}
|
||||
}
|
||||
Term::App { fun: fst, arg: snd, .. }
|
||||
|
@ -1,6 +1,7 @@
|
||||
use crate::{
|
||||
diagnostics::Info,
|
||||
term::{Ctx, MatchNum, Name, Pattern, Term}, CORE_BUILTINS
|
||||
term::{Ctx, Name, Pattern, Term},
|
||||
CORE_BUILTINS,
|
||||
};
|
||||
use std::{
|
||||
collections::{HashMap, HashSet},
|
||||
@ -16,7 +17,7 @@ impl Display for ReferencedMainErr {
|
||||
}
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
impl Ctx<'_> {
|
||||
/// Decides if names inside a term belong to a Var or to a Ref.
|
||||
/// Precondition: Refs are encoded as vars, Constructors are resolved.
|
||||
/// Postcondition: Refs are encoded as refs, with the correct def id.
|
||||
@ -28,12 +29,12 @@ impl<'book> Ctx<'book> {
|
||||
for rule in def.rules.iter_mut() {
|
||||
let mut scope = HashMap::new();
|
||||
|
||||
for name in rule.pats.iter().flat_map(Pattern::names) {
|
||||
for name in rule.pats.iter().flat_map(Pattern::binds) {
|
||||
push_scope(Some(name), &mut scope);
|
||||
}
|
||||
|
||||
let res = rule.body.resolve_refs(&def_names, self.book.entrypoint.as_ref(), &mut scope);
|
||||
self.info.take_err(res, Some(&def_name));
|
||||
self.info.take_err(res, Some(def_name));
|
||||
}
|
||||
}
|
||||
|
||||
@ -63,13 +64,13 @@ impl Term {
|
||||
Term::Let { pat, val, nxt } => {
|
||||
val.resolve_refs(def_names, main, scope)?;
|
||||
|
||||
for nam in pat.names() {
|
||||
for nam in pat.binds() {
|
||||
push_scope(Some(nam), scope);
|
||||
}
|
||||
|
||||
nxt.resolve_refs(def_names, main, scope)?;
|
||||
|
||||
for nam in pat.names() {
|
||||
for nam in pat.binds() {
|
||||
pop_scope(Some(nam), scope);
|
||||
}
|
||||
}
|
||||
@ -91,7 +92,7 @@ impl Term {
|
||||
}
|
||||
}
|
||||
|
||||
if def_names.contains(nam) || CORE_BUILTINS.contains(&nam.0.as_ref().as_ref()) {
|
||||
if def_names.contains(nam) || CORE_BUILTINS.contains(&nam.0.as_ref()) {
|
||||
*self = Term::r#ref(nam);
|
||||
}
|
||||
}
|
||||
@ -104,15 +105,20 @@ impl Term {
|
||||
fst.resolve_refs(def_names, main, scope)?;
|
||||
snd.resolve_refs(def_names, main, scope)?;
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.resolve_refs(def_names, main, scope)?;
|
||||
for (pat, term) in arms {
|
||||
let nam = if let Pattern::Num(MatchNum::Succ(Some(nam))) = pat { nam.as_ref() } else { None };
|
||||
push_scope(nam, scope);
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.resolve_refs(def_names, main, scope)?;
|
||||
}
|
||||
for rule in rules {
|
||||
for nam in rule.pats.iter().flat_map(|p| p.bind_or_eras()) {
|
||||
push_scope(nam.as_ref(), scope);
|
||||
}
|
||||
|
||||
term.resolve_refs(def_names, main, scope)?;
|
||||
rule.body.resolve_refs(def_names, main, scope)?;
|
||||
|
||||
pop_scope(nam, scope);
|
||||
for nam in rule.pats.iter().flat_map(|p| p.bind_or_eras()).rev() {
|
||||
pop_scope(nam.as_ref(), scope);
|
||||
}
|
||||
}
|
||||
}
|
||||
Term::Lst { .. } => unreachable!("Should have been desugared already"),
|
||||
|
@ -1,4 +1,4 @@
|
||||
use crate::term::{net_to_term::ReadbackError, Adt, AdtEncoding, Book, Name, Pattern, Tag, Term};
|
||||
use crate::term::{net_to_term::ReadbackError, Adt, AdtEncoding, Book, Name, Pattern, Rule, Tag, Term};
|
||||
|
||||
impl Term {
|
||||
pub fn resugar_adts(&mut self, book: &Book, adt_encoding: AdtEncoding) -> Vec<ReadbackError> {
|
||||
@ -41,10 +41,12 @@ impl Term {
|
||||
fst.resugar_tagged_scott(book, errs);
|
||||
snd.resugar_tagged_scott(book, errs);
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.resugar_tagged_scott(book, errs);
|
||||
for (_, arm) in arms {
|
||||
arm.resugar_tagged_scott(book, errs);
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.resugar_tagged_scott(book, errs);
|
||||
}
|
||||
for rule in rules {
|
||||
rule.body.resugar_tagged_scott(book, errs);
|
||||
}
|
||||
}
|
||||
Term::Lst { .. } => unreachable!(),
|
||||
@ -210,7 +212,7 @@ impl Term {
|
||||
}
|
||||
}
|
||||
|
||||
arms.push((Pattern::Ctr(ctr.clone(), args), arm));
|
||||
arms.push((vec![Pattern::Ctr(ctr.clone(), args)], arm));
|
||||
cur = &mut *fun;
|
||||
}
|
||||
_ => {
|
||||
@ -220,9 +222,10 @@ impl Term {
|
||||
}
|
||||
}
|
||||
|
||||
let matched = Box::new(std::mem::take(cur));
|
||||
let arms = arms.into_iter().rev().map(|(pat, term)| (pat, std::mem::take(term))).collect();
|
||||
*self = Term::Mat { matched, arms };
|
||||
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 };
|
||||
|
||||
self.resugar_tagged_scott(book, errs);
|
||||
}
|
||||
|
@ -41,10 +41,12 @@ impl Term {
|
||||
// (String.nil)
|
||||
Term::Ref { nam: def_name } if def_name == SNIL => *self = Term::str(""),
|
||||
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.resugar_strings();
|
||||
for (_, arm) in arms {
|
||||
arm.resugar_strings();
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.resugar_strings();
|
||||
}
|
||||
for rule in rules {
|
||||
rule.body.resugar_strings();
|
||||
}
|
||||
}
|
||||
Term::Lst { els } => {
|
||||
@ -102,10 +104,12 @@ impl Term {
|
||||
// (List.nil)
|
||||
Term::Ref { nam: def_name } if def_name == LNIL => *self = Term::Lst { els: vec![] },
|
||||
|
||||
Term::Mat { matched, arms } => {
|
||||
matched.resugar_lists();
|
||||
for (_, arm) in arms {
|
||||
arm.resugar_lists();
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
arg.resugar_lists();
|
||||
}
|
||||
for rule in rules {
|
||||
rule.body.resugar_lists();
|
||||
}
|
||||
}
|
||||
Term::Lst { els } => {
|
||||
|
346
src/term/transform/simplify_matches.rs
Normal file
346
src/term/transform/simplify_matches.rs
Normal file
@ -0,0 +1,346 @@
|
||||
use itertools::Itertools;
|
||||
|
||||
use crate::{
|
||||
diagnostics::Info,
|
||||
term::{
|
||||
check::type_check::infer_type,
|
||||
transform::encode_pattern_matching::{ExhaustivenessErr, MatchErr},
|
||||
Adts, Constructors, Ctx, Definition, MatchNum, Name, Pattern, Rule, Term, Type,
|
||||
},
|
||||
};
|
||||
|
||||
impl Ctx<'_> {
|
||||
pub fn simplify_matches(&mut self) -> Result<(), Info> {
|
||||
self.info.start_pass();
|
||||
|
||||
for (def_name, def) in self.book.defs.iter_mut() {
|
||||
let res = def.simplify_matches(&self.book.ctrs, &self.book.adts);
|
||||
self.info.take_err(res, Some(def_name));
|
||||
}
|
||||
|
||||
self.info.fatal(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Definition {
|
||||
pub fn simplify_matches(&mut self, ctrs: &Constructors, adts: &Adts) -> Result<(), MatchErr> {
|
||||
for rule in self.rules.iter_mut() {
|
||||
rule.body.simplify_matches(ctrs, adts)?;
|
||||
}
|
||||
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.
|
||||
///
|
||||
/// See `[simplify_match_expression]` for more information.
|
||||
pub fn simplify_matches(&mut self, ctrs: &Constructors, adts: &Adts) -> Result<(), MatchErr> {
|
||||
match self {
|
||||
Term::Mat { args, rules } => {
|
||||
let (new_args, extracted) = extract_args(args);
|
||||
|
||||
*self = simplify_match_expression(&new_args, rules, ctrs, adts)?;
|
||||
*self = bind_extracted_args(extracted, std::mem::take(self));
|
||||
}
|
||||
|
||||
Term::Lst { els } => {
|
||||
for el in els {
|
||||
el.simplify_matches(ctrs, adts)?;
|
||||
}
|
||||
}
|
||||
Term::Let { val: fst, nxt: snd, .. }
|
||||
| Term::App { fun: fst, arg: snd, .. }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. } => {
|
||||
fst.simplify_matches(ctrs, adts)?;
|
||||
snd.simplify_matches(ctrs, adts)?;
|
||||
}
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.simplify_matches(ctrs, adts)?,
|
||||
Term::Var { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Str { .. }
|
||||
| Term::Ref { .. }
|
||||
| Term::Era => (),
|
||||
Term::Err => unreachable!(),
|
||||
}
|
||||
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: &[Term],
|
||||
rules: &[Rule],
|
||||
ctrs: &Constructors,
|
||||
adts: &Adts,
|
||||
) -> Result<Term, MatchErr> {
|
||||
let fst_row_irrefutable = matches!(infer_type(&rules[0].pats, ctrs), Ok(Type::Any));
|
||||
let fst_col_type = infer_type(rules.iter().map(|r| &r.pats[0]), ctrs)?;
|
||||
|
||||
if fst_row_irrefutable {
|
||||
irrefutable_fst_row_rule(args, rules, ctrs, adts)
|
||||
} else if fst_col_type == Type::Any {
|
||||
var_rule(args, rules, ctrs, adts)
|
||||
} else {
|
||||
let adt_ctrs = fst_col_type.ctrs(adts);
|
||||
switch_rule(args, rules, adt_ctrs, ctrs, adts)
|
||||
}
|
||||
}
|
||||
|
||||
/// 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: &[Term],
|
||||
rules: &[Rule],
|
||||
ctrs: &Constructors,
|
||||
adts: &Adts,
|
||||
) -> Result<Term, MatchErr> {
|
||||
let mut term = rules[0].body.clone();
|
||||
term.simplify_matches(ctrs, adts)?;
|
||||
let term = rules[0].pats.iter().zip(args).fold(term, |term, (pat, arg)| Term::Let {
|
||||
pat: pat.clone(),
|
||||
val: Box::new(arg.clone()),
|
||||
nxt: Box::new(term),
|
||||
});
|
||||
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(args: &[Term], rules: &[Rule], ctrs: &Constructors, adts: &Adts) -> Result<Term, MatchErr> {
|
||||
let mut new_rules = vec![];
|
||||
for rule in rules {
|
||||
let body = Term::Let {
|
||||
pat: rule.pats[0].clone(),
|
||||
val: Box::new(args[0].clone()),
|
||||
nxt: Box::new(rule.body.clone()),
|
||||
};
|
||||
let new_rule = Rule { pats: rule.pats[1 ..].to_vec(), body };
|
||||
new_rules.push(new_rule);
|
||||
}
|
||||
let mut term = Term::Mat { args: args[1 ..].to_vec(), rules: new_rules };
|
||||
term.simplify_matches(ctrs, adts)?;
|
||||
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(
|
||||
args: &[Term],
|
||||
rules: &[Rule],
|
||||
adt_ctrs: Vec<Pattern>,
|
||||
ctrs: &Constructors,
|
||||
adts: &Adts,
|
||||
) -> Result<Term, MatchErr> {
|
||||
let mut new_rules = vec![];
|
||||
for ctr in adt_ctrs {
|
||||
// Create the matched constructor and the name of the bound variables.
|
||||
let Term::Var { nam: arg_nam } = &args[0] else { unreachable!() };
|
||||
let nested_fields = switch_rule_nested_fields(arg_nam, &ctr);
|
||||
let matched_ctr = switch_rule_matched_ctr(ctr, &nested_fields);
|
||||
let mut body = switch_rule_submatch(args, rules, &matched_ctr, &nested_fields)?;
|
||||
body.simplify_matches(ctrs, adts)?;
|
||||
let pats = vec![matched_ctr];
|
||||
new_rules.push(Rule { pats, body });
|
||||
}
|
||||
|
||||
let term = Term::Mat { args: vec![args[0].clone()], rules: new_rules };
|
||||
Ok(term)
|
||||
}
|
||||
|
||||
fn switch_rule_nested_fields(arg_nam: &Name, ctr: &Pattern) -> Vec<Option<Name>> {
|
||||
let mut nested_fields = vec![];
|
||||
let old_vars = ctr.bind_or_eras();
|
||||
for old_var in old_vars {
|
||||
let new_nam = if let Some(field) = old_var {
|
||||
// Name of constructor field
|
||||
Name::new(format!("{arg_nam}%{field}"))
|
||||
} 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<Name>]) -> Pattern {
|
||||
let mut nested_fields = nested_fields.iter().cloned();
|
||||
ctr.bind_or_eras_mut().for_each(|var| *var = nested_fields.next().unwrap());
|
||||
ctr
|
||||
}
|
||||
|
||||
fn switch_rule_submatch(
|
||||
args: &[Term],
|
||||
rules: &[Rule],
|
||||
ctr: &Pattern,
|
||||
nested_fields: &[Option<Name>],
|
||||
) -> Result<Term, MatchErr> {
|
||||
// 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::<Vec<_>>();
|
||||
|
||||
// Make the match cases of the nested submatch, filtering out the rules
|
||||
// that don't match the crnt ctr.
|
||||
let rules =
|
||||
rules.iter().filter_map(|rule| switch_rule_submatch_arm(rule, ctr, nested_fields)).collect::<Vec<_>>();
|
||||
|
||||
if rules.is_empty() {
|
||||
// TODO: Return the full pattern
|
||||
return Err(MatchErr::NotExhaustive(ExhaustivenessErr(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<Name>]) -> Option<Rule> {
|
||||
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 = if let Pattern::Num(MatchNum::Succ(Some(var))) = &rule.pats[0] {
|
||||
// Since the variable in the succ ctr is not a nested pattern, we need this special case.
|
||||
vec![Pattern::Var(var.clone())]
|
||||
} else {
|
||||
rule.pats[0].children().cloned().collect::<Vec<_>>()
|
||||
};
|
||||
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() {
|
||||
// Var, reconstruct the value matched in the expression above.
|
||||
// match x ... {var ...: Body; ...}
|
||||
// becomes
|
||||
// match x {
|
||||
// (Ctr x%field0 ...): match x1 ... {
|
||||
// x%field0 ...: let var = (Ctr x%field0 ...); Body;
|
||||
// ... };
|
||||
// ... }
|
||||
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();
|
||||
|
||||
let body =
|
||||
Term::Let { pat: rule.pats[0].clone(), val: Box::new(ctr.to_term()), nxt: Box::new(rule.body.clone()) };
|
||||
|
||||
Some(Rule { pats, body })
|
||||
} else {
|
||||
// Non-matching constructor. Don't include in submatch expression.
|
||||
None
|
||||
}
|
||||
}
|
||||
|
||||
fn extract_args(args: &mut [Term]) -> (Vec<Term>, Vec<(Name, Term)>) {
|
||||
let mut new_args = vec![];
|
||||
let mut extracted = vec![];
|
||||
|
||||
for (i, arg) in args.iter_mut().enumerate() {
|
||||
if matches!(arg, Term::Var { .. }) {
|
||||
new_args.push(std::mem::take(arg));
|
||||
} else {
|
||||
let nam = Name::new(format!("%match_arg{i}"));
|
||||
|
||||
let old_arg = std::mem::take(arg);
|
||||
extracted.push((nam.clone(), old_arg));
|
||||
|
||||
let new_arg = Term::Var { nam };
|
||||
new_args.push(new_arg);
|
||||
}
|
||||
}
|
||||
(new_args, extracted)
|
||||
}
|
||||
|
||||
fn bind_extracted_args(extracted: Vec<(Name, Term)>, term: Term) -> Term {
|
||||
extracted.into_iter().rev().fold(term, |term, (nam, val)| Term::Let {
|
||||
pat: Pattern::Var(Some(nam)),
|
||||
val: Box::new(val),
|
||||
nxt: Box::new(term),
|
||||
})
|
||||
}
|
@ -15,7 +15,7 @@ impl Display for CyclicDefErr {
|
||||
}
|
||||
}
|
||||
|
||||
impl<'book> Ctx<'book> {
|
||||
impl Ctx<'_> {
|
||||
// When we find a function that is simply directly calling another function,
|
||||
// substitutes all occurrences of that function to the one being called, avoiding the unnecessary redirect.
|
||||
// In case there is a long chain of ref-to-ref-to-ref, we substitute values by the last function in the chain.
|
||||
@ -71,10 +71,13 @@ pub fn subst_ref_to_ref(term: &mut Term, ref_map: &BTreeMap<Name, Name>) -> bool
|
||||
let snd_subst = subst_ref_to_ref(snd, ref_map);
|
||||
fst_subst | snd_subst
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
let mut subst = subst_ref_to_ref(matched, ref_map);
|
||||
for (_, term) in arms {
|
||||
subst |= subst_ref_to_ref(term, ref_map);
|
||||
Term::Mat { args, rules } => {
|
||||
let mut subst = false;
|
||||
for arg in args {
|
||||
subst |= subst_ref_to_ref(arg, ref_map);
|
||||
}
|
||||
for rule in rules {
|
||||
subst |= subst_ref_to_ref(&mut rule.body, ref_map);
|
||||
}
|
||||
subst
|
||||
}
|
||||
|
@ -60,12 +60,19 @@ impl UniqueNameGenerator {
|
||||
*snd = self.pop(snd.as_ref());
|
||||
*fst = self.pop(fst.as_ref());
|
||||
}
|
||||
Term::Mat { matched, arms } => {
|
||||
self.unique_names_in_term(matched);
|
||||
for (pat, term) in arms {
|
||||
pat.names().for_each(|nam| self.push(Some(nam)));
|
||||
self.unique_names_in_term(term);
|
||||
pat.names_mut().rev().for_each(|nam| *nam = self.pop(Some(nam)).unwrap());
|
||||
Term::Mat { args, rules } => {
|
||||
for arg in args {
|
||||
self.unique_names_in_term(arg);
|
||||
}
|
||||
for rule in rules {
|
||||
rule.pats.iter().flat_map(|p| p.binds()).for_each(|nam| self.push(Some(nam)));
|
||||
self.unique_names_in_term(&mut rule.body);
|
||||
rule
|
||||
.pats
|
||||
.iter_mut()
|
||||
.flat_map(|p| p.binds_mut())
|
||||
.rev()
|
||||
.for_each(|nam| *nam = self.pop(Some(nam)).unwrap());
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1,7 +1,6 @@
|
||||
use hvml::{
|
||||
compile_book, desugar_book,
|
||||
diagnostics::Info,
|
||||
encode_pattern_matching,
|
||||
net::{hvmc_to_net::hvmc_to_net, net_to_hvmc::net_to_hvmc},
|
||||
run_book,
|
||||
term::{
|
||||
@ -184,20 +183,28 @@ fn readback_lnet() {
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn flatten_rules() {
|
||||
fn simplify_matches() {
|
||||
run_golden_test_dir(function_name!(), &|code, path| {
|
||||
let mut book = do_parse_book(code, path)?;
|
||||
let mut ctx = Ctx::new(&mut book);
|
||||
ctx.set_entrypoint();
|
||||
ctx.check_shared_names();
|
||||
ctx.set_entrypoint();
|
||||
ctx.book.encode_adts(AdtEncoding::TaggedScott);
|
||||
ctx.book.encode_builtins();
|
||||
ctx.book.resolve_ctrs_in_pats();
|
||||
ctx.book.encode_adts(AdtEncoding::TaggedScott);
|
||||
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_pats()?;
|
||||
ctx.extract_adt_matches()?;
|
||||
ctx.book.flatten_rules();
|
||||
ctx.check_ctrs_arities()?;
|
||||
ctx.check_unbound_vars()?;
|
||||
ctx.simplify_matches()?;
|
||||
ctx.linearize_simple_matches()?;
|
||||
ctx.check_unbound_vars()?;
|
||||
ctx.book.make_var_names_unique();
|
||||
ctx.book.linearize_vars();
|
||||
ctx.prune(false, AdtEncoding::TaggedScott);
|
||||
Ok(ctx.book.to_string())
|
||||
})
|
||||
@ -218,13 +225,26 @@ fn encode_pattern_match() {
|
||||
for adt_encoding in [AdtEncoding::TaggedScott, AdtEncoding::Scott] {
|
||||
let mut book = do_parse_book(code, path)?;
|
||||
let mut ctx = Ctx::new(&mut book);
|
||||
ctx.set_entrypoint();
|
||||
ctx.check_shared_names();
|
||||
ctx.set_entrypoint();
|
||||
ctx.book.encode_adts(adt_encoding);
|
||||
ctx.book.encode_builtins();
|
||||
encode_pattern_matching(&mut ctx, adt_encoding)?;
|
||||
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_ctrs_arities()?;
|
||||
ctx.check_unbound_vars()?;
|
||||
ctx.simplify_matches()?;
|
||||
ctx.linearize_simple_matches()?;
|
||||
ctx.book.encode_simple_matches(adt_encoding);
|
||||
ctx.check_unbound_vars()?;
|
||||
ctx.book.make_var_names_unique();
|
||||
ctx.book.linearize_vars();
|
||||
ctx.prune(false, adt_encoding);
|
||||
ctx.book.merge_definitions();
|
||||
|
||||
writeln!(result, "{adt_encoding:?}:").unwrap();
|
||||
writeln!(result, "{}\n", ctx.book).unwrap();
|
||||
|
@ -1,9 +1,9 @@
|
||||
main = @a @b
|
||||
let a = match a {
|
||||
let a = match a {
|
||||
String.cons: 1
|
||||
String.nil : 2
|
||||
};
|
||||
let b = match b {
|
||||
let b = match b {
|
||||
(List.cons h t): 1
|
||||
(List.nil) : 2
|
||||
};
|
||||
|
40
tests/golden_tests/encode_pattern_match/match_many_args.hvm
Normal file
40
tests/golden_tests/encode_pattern_match/match_many_args.hvm
Normal file
@ -0,0 +1,40 @@
|
||||
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 = *
|
@ -1,4 +1,4 @@
|
||||
main=
|
||||
main =
|
||||
match 0 {
|
||||
| true: 1
|
||||
| false: 0
|
||||
|
@ -2,5 +2,5 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file/missing_pat.hvm
|
||||
---
|
||||
At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected '|', 0, +, <Name>, '(', '[', or '}'
|
||||
At tests/golden_tests/compile_file/missing_pat.hvm:2:3: found ':' expected '(', '#', '$', <Name>, '[', '{', 'λ', 'let', 'match', '*', '|', 0, or +
|
||||
[0m 2 | [4m[31m:[0m *[0m
|
||||
|
@ -3,5 +3,5 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file/wrong_ctr_arity.hvm
|
||||
---
|
||||
In definition 'Bar':
|
||||
Arity error. Constructor 'Box' expects 1 fields, found 2.
|
||||
Constructor arity mismatch in pattern matching. Constructor 'Box' expects 1 fields, found 2.
|
||||
|
||||
|
@ -3,5 +3,5 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file/wrong_ctr_var_arity.hvm
|
||||
---
|
||||
In definition 'foo':
|
||||
Arity error. Constructor 'pair' expects 2 fields, found 0.
|
||||
Constructor arity mismatch in pattern matching. Constructor 'pair' expects 2 fields, found 0.
|
||||
|
||||
|
@ -2,14 +2,13 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/adt_option_and.hvm
|
||||
---
|
||||
@None = {4 * {4 a a}}
|
||||
@Option.and$match$1$S0 = {2 a (b {4 {2 [b a] c} {4 * c}})}
|
||||
@Option.and$match$2 = ({4 @Option.and$match$2$S0 {4 @Option.and$match$2$S1_$_Option.and$match$1$S1 a}} a)
|
||||
@Option.and$match$2$S0 = {2 a ({4 @Option.and$match$1$S0 {4 @Option.and$match$2$S1_$_Option.and$match$1$S1 (a b)}} b)}
|
||||
@Option.and$match$2$S1_$_Option.and$match$1$S1 = (* @None)
|
||||
@Some = (a {4 {2 a b} {4 * b}})
|
||||
@None = {2 * {2 a a}}
|
||||
@Option.and = ({2 @Option.and$S2 {2 @Option.and$S3_$_Option.and$S1 a}} a)
|
||||
@Option.and$S0 = {4 a (b {2 {4 [b a] c} {2 * c}})}
|
||||
@Option.and$S2 = {4 a ({2 @Option.and$S0 {2 @Option.and$S3_$_Option.and$S1 (a b)}} b)}
|
||||
@Option.and$S3_$_Option.and$S1 = (* @None)
|
||||
@Some = (a {2 {4 a b} {2 * b}})
|
||||
@main = a
|
||||
& @Option.and$match$2 ~ (b (c a))
|
||||
& @Option.and ~ (b (c a))
|
||||
& @Some ~ (#3 c)
|
||||
& @Some ~ (#1 b)
|
||||
|
||||
|
@ -3,8 +3,7 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/let_adt_destructuring.hvm
|
||||
---
|
||||
@Box = (a {2 {4 a b} b})
|
||||
@Unbox$match$1 = ({2 {4 a a} b} b)
|
||||
@Unbox = ({2 {4 a a} b} b)
|
||||
@main = a
|
||||
& @Unbox$match$1 ~ (b a)
|
||||
& @Unbox ~ (b a)
|
||||
& @Box ~ (#1 b)
|
||||
|
||||
|
@ -2,7 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/let_adt_non_exhaustive.hvm
|
||||
---
|
||||
In definition 'main$match$1':
|
||||
Non-exhaustive pattern. Hint:
|
||||
(main$match$1 None) not covered.
|
||||
In definition 'main':
|
||||
Non-exhaustive pattern matching. Hint:
|
||||
Case 'None' not covered.
|
||||
|
||||
|
@ -5,24 +5,23 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
|
||||
@Cons = (a (b {4 {6 a {8 b c}} {4 * c}}))
|
||||
@If$S0 = (a (* a))
|
||||
@If$S1 = (* (a a))
|
||||
@Map = ({4 @Map$S0 {4 @Unpack$S1_$_MergePair$S1_$_Map$S1 a}} a)
|
||||
@Map$S0 = {6 a {8 {4 @Map$S0 {4 @Unpack$S1_$_MergePair$S1_$_Map$S1 (b c)}} ({5 (a d) b} {4 {6 d {8 c e}} {4 * e}})}}
|
||||
@Merge$S0 = {6 {7 a {9 b c}} {8 {11 d {4 @Merge$S0 {4 @Merge$S1 (e (f (g h)))}}} ({13 (i (a {2 @If$S0 {2 @If$S1 ({4 {6 j {8 k l}} {4 * l}} ({4 {6 c {8 h m}} {4 * m}} n))}})) {15 o e}} ({17 i {19 j f}} ({21 {4 @Merge$S2 {4 @Merge$S3 (o ({4 {6 b {8 d p}} {4 * p}} k))}} g} n)))}}
|
||||
@Map = ({4 @Map$S0 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 a}} a)
|
||||
@Map$S0 = {6 a {8 {4 @Map$S0 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (b c)}} ({5 (a d) b} {4 {6 d {8 c e}} {4 * e}})}}
|
||||
@Merge$S0 = {6 {9 a {11 b c}} {8 {7 d {4 @Merge$S0 {4 @Merge$S1 (e (f (g h)))}}} ({19 (i (a {2 @If$S0 {2 @If$S1 ({4 {6 j {8 k l}} {4 * l}} ({4 {6 c {8 h m}} {4 * m}} n))}})) {21 o e}} ({15 i {17 j f}} ({13 {4 @Merge$S2 {4 @Merge$S3 (o ({4 {6 b {8 d p}} {4 * p}} k))}} g} n)))}}
|
||||
@Merge$S1 = (* @Cons)
|
||||
@Merge$S2 = {6 a {8 b (c ({4 @Merge$S0 {4 @Merge$S1 (c (a (b d)))}} d))}}
|
||||
@Merge$S3 = (* (a a))
|
||||
@MergePair$F0$S0 = {6 a {8 {4 @MergePair$S0 {4 @Unpack$S1_$_MergePair$S1_$_Map$S1 (b c)}} ({23 d b} ({4 @Merge$S2 {4 @Merge$S3 (d (a e))}} {4 {6 e {8 c f}} {4 * f}}))}}
|
||||
@MergePair$F0$S1 = (a {4 {6 a {8 @Nil b}} {4 * b}})
|
||||
@MergePair$F0$S2 = (* @MergePair$F0$S1)
|
||||
@MergePair$S0 = {6 a {8 {4 @MergePair$F0$S0 {4 @MergePair$F0$S2 (b (a c))}} (b c)}}
|
||||
@MergePair$S0 = {6 a {8 {4 @MergePair$S3 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (b c)}} ({23 d b} ({4 @Merge$S2 {4 @Merge$S3 (d (a e))}} {4 {6 e {8 c f}} {4 * f}}))}}
|
||||
@MergePair$S1 = (a {4 {6 a {8 @Nil b}} {4 * b}})
|
||||
@MergePair$S2 = (* @MergePair$S1)
|
||||
@MergePair$S3 = {6 a {8 {4 @MergePair$S0 {4 @MergePair$S2 (b (a c))}} (b c)}}
|
||||
@Nil = {4 * {4 a a}}
|
||||
@Pure = (a {4 {6 a {8 @Nil b}} {4 * b}})
|
||||
@Unpack = (a ({4 @Unpack$S0 {4 @Unpack$S1_$_MergePair$S1_$_Map$S1 (a b)}} b))
|
||||
@Unpack$F0$S0 = {6 a {8 {4 @MergePair$S0 {4 @Unpack$S1_$_MergePair$S1_$_Map$S1 (b {4 @Unpack$F0$S0 {4 @Unpack$F0$S1 (c (d e))}})}} ({3 c {23 f b}} ({4 @Merge$S2 {4 @Merge$S3 (f (a d))}} e))}}
|
||||
@Unpack$F0$S1 = (* (a a))
|
||||
@Unpack$S0 = {6 a {8 {4 @Unpack$F0$S0 {4 @Unpack$F0$S1 (b (a c))}} (b c)}}
|
||||
@Unpack$S1_$_MergePair$S1_$_Map$S1 = (* @Nil)
|
||||
@Unpack = (a ({4 @Unpack$S2 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (a b)}} b))
|
||||
@Unpack$S0 = {6 a {8 {4 @MergePair$S3 {4 @Unpack$S3_$_MergePair$S4_$_Map$S1 (b {4 @Unpack$S0 {4 @Unpack$S1 (c (d e))}})}} ({3 c {23 f b}} ({4 @Merge$S2 {4 @Merge$S3 (f (a d))}} e))}}
|
||||
@Unpack$S1 = (* (a a))
|
||||
@Unpack$S2 = {6 a {8 {4 @Unpack$S0 {4 @Unpack$S1 (b (a c))}} (b c)}}
|
||||
@Unpack$S3_$_MergePair$S4_$_Map$S1 = (* @Nil)
|
||||
@main = (a (b c))
|
||||
& @Unpack ~ (a (d c))
|
||||
& @Map ~ (b (@Pure d))
|
||||
|
||||
|
@ -2,7 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/match_adt_non_exhaustive.hvm
|
||||
---
|
||||
In definition 'main$match$1$F0':
|
||||
Non-exhaustive pattern. Hint:
|
||||
(main$match$1$F0 Some) not covered.
|
||||
In definition 'main':
|
||||
Non-exhaustive pattern matching. Hint:
|
||||
Case 'Some' not covered.
|
||||
|
||||
|
@ -2,10 +2,9 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/match_dup_and_reconstruction.hvm
|
||||
---
|
||||
@Boxed = (a {4 {2 a b} b})
|
||||
@Got = ({3 {4 @Got$match$1$S0 (a b)} a} b)
|
||||
@Got$match$1$S0 = {2 a (b [b a])}
|
||||
@Boxed = (a {2 {4 a b} b})
|
||||
@Got = ({3 {2 @Got$S0 (a b)} a} b)
|
||||
@Got$S0 = {4 a (b [b a])}
|
||||
@main = a
|
||||
& @Got ~ (b a)
|
||||
& @Boxed ~ (#10 b)
|
||||
|
||||
|
@ -2,11 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/nested_adt_match.hvm
|
||||
---
|
||||
@Some = (a {4 {2 a b} {4 * b}})
|
||||
@Some = (a {2 {4 a b} {2 * b}})
|
||||
@main = a
|
||||
& @main$match$1 ~ (b a)
|
||||
& @Some ~ (c b)
|
||||
& @Some ~ (#1 c)
|
||||
@main$match$1 = ({4 @main$match$1$S0 {4 #0 a}} a)
|
||||
@main$match$1$S0 = {2 {4 {2 a a} {4 #0 b}} b}
|
||||
|
||||
& @Some ~ (b {2 {4 {2 {4 c c} {2 #0 d}} d} {2 #0 a}})
|
||||
& @Some ~ (#1 b)
|
||||
|
@ -3,6 +3,6 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/non_exhaustive_and.hvm
|
||||
---
|
||||
In definition 'Bool.and':
|
||||
Non-exhaustive pattern. Hint:
|
||||
(Bool.and T F) not covered.
|
||||
Non-exhaustive pattern matching. Hint:
|
||||
Case 'F' not covered.
|
||||
|
||||
|
@ -3,7 +3,6 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/non_exhaustive_different_types.hvm
|
||||
---
|
||||
In definition 'foo':
|
||||
Non-exhaustive pattern. Hint:
|
||||
(foo f1 f2 t3 f4) not covered.
|
||||
(foo f1 f2 t3 t4) not covered.
|
||||
Non-exhaustive pattern matching. Hint:
|
||||
Case 't3' not covered.
|
||||
|
||||
|
@ -3,9 +3,6 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/non_exhaustive_pattern.hvm
|
||||
---
|
||||
In definition 'Foo':
|
||||
Non-exhaustive pattern. Hint:
|
||||
(Foo A A A A) not covered.
|
||||
(Foo A A A B) not covered.
|
||||
(Foo A A A C) not covered.
|
||||
(Foo A A A D) not covered.
|
||||
Non-exhaustive pattern matching. Hint:
|
||||
Case 'A' not covered.
|
||||
|
||||
|
@ -3,6 +3,6 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/non_exhaustive_tree.hvm
|
||||
---
|
||||
In definition 'Warp':
|
||||
Non-exhaustive pattern. Hint:
|
||||
(Warp _ Leaf Both) not covered.
|
||||
Non-exhaustive pattern matching. Hint:
|
||||
Case 'Both' not covered.
|
||||
|
||||
|
@ -2,9 +2,9 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm
|
||||
---
|
||||
@Foo = ({2 (* #0) {2 @Foo$S1 a}} a)
|
||||
@Foo$S1 = (?<(#0 (a a)) b> b)
|
||||
@Foo = ({2 (* #0) {2 @Foo$S3 a}} a)
|
||||
@Foo$S2 = (a (* a))
|
||||
@Foo$S3 = (?<((* #0) @Foo$S2) (* a)> a)
|
||||
@main = a
|
||||
& @Foo ~ (@true (#3 a))
|
||||
@true = {2 * {2 a a}}
|
||||
|
||||
|
@ -2,13 +2,12 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/scrutinee_reconstruction.hvm
|
||||
---
|
||||
@None = {4 * {4 a a}}
|
||||
@Option.or = ({3 {4 @Option.or$match$1$S1 {4 @Option.or$match$1$S2 (a b)}} a} b)
|
||||
@Option.or$match$1$S0 = (a (* a))
|
||||
@Option.or$match$1$S1 = {2 * @Option.or$match$1$S0}
|
||||
@Option.or$match$1$S2 = (* (a a))
|
||||
@Some = (a {4 {2 a b} {4 * b}})
|
||||
@None = {2 * {2 a a}}
|
||||
@Option.or = ({3 {2 @Option.or$S1 {2 @Option.or$S2 (a b)}} a} b)
|
||||
@Option.or$S0 = (a (* a))
|
||||
@Option.or$S1 = {4 * @Option.or$S0}
|
||||
@Option.or$S2 = (* (a a))
|
||||
@Some = (a {2 {4 a b} {2 * b}})
|
||||
@main = a
|
||||
& @Option.or ~ (b (@None a))
|
||||
& @Some ~ (#5 b)
|
||||
|
||||
|
@ -3,6 +3,5 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/compile_file_o_all/snd.hvm
|
||||
---
|
||||
@main = a
|
||||
& @snd$match$1 ~ ([#0 #42] a)
|
||||
@snd$match$1 = ([* a] a)
|
||||
|
||||
& @snd ~ ([#0 #42] a)
|
||||
@snd = ([* a] a)
|
||||
|
@ -3,11 +3,6 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/desugar_file/non_exaustive_limit.hvm
|
||||
---
|
||||
In definition 'Bar':
|
||||
Non-exhaustive pattern. Hint:
|
||||
(Bar A A B) not covered.
|
||||
(Bar A A C) not covered.
|
||||
(Bar A A D) not covered.
|
||||
(Bar A A E) not covered.
|
||||
(Bar A A F) not covered. ... and 2 others.
|
||||
Use the --verbose option to see all cases.
|
||||
Non-exhaustive pattern matching. Hint:
|
||||
Case 'B' not covered.
|
||||
|
||||
|
@ -2,6 +2,6 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/desugar_file/used_once_names.hvm
|
||||
---
|
||||
(foo) = λa λb λc let {c c_2} = c; (a b (c c_2))
|
||||
(foo) = λa λb λc let {d d_2} = c; (a b (d d_2))
|
||||
|
||||
(main) = (foo 2 3 λa a)
|
||||
|
@ -3,21 +3,17 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/adt_tup_era.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(Foo) = λa #Tuple (a #Tuple.Pair.a λb #Tuple.Pair.b λc (Foo$F0 b c))
|
||||
(Foo) = λa #Tuple (a #Tuple.Pair.a λb #Tuple.Pair.b λc (#Tuple (b #Tuple.Pair.a λd #Tuple.Pair.b λ* λ* d) c))
|
||||
|
||||
(Main) = (Foo (Pair 1 5))
|
||||
|
||||
(Foo$F0) = λa #Tuple (a #Tuple.Pair.a λb #Tuple.Pair.b λc λd b)
|
||||
|
||||
(Pair) = λa λb #Tuple λPair #Tuple.Pair.b (#Tuple.Pair.a (Pair a) b)
|
||||
(Pair) = λa λb #Tuple λc #Tuple.Pair.b (#Tuple.Pair.a (c a) b)
|
||||
|
||||
Scott:
|
||||
(Foo) = λa (a λb λc (Foo$F0 b c))
|
||||
(Foo) = λa (a λb λc (b λd λ* λ* d c))
|
||||
|
||||
(Main) = (Foo (Pair 1 5))
|
||||
|
||||
(Foo$F0) = λa (a λb λc λd b)
|
||||
|
||||
(Pair) = λa λb λPair (Pair a b)
|
||||
(Pair) = λa λb λc (c a b)
|
||||
|
||||
|
||||
|
@ -3,29 +3,21 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/and3.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(And) = λa let (b, c) = a; (And$F0 b c)
|
||||
(And) = λa let (b, c) = a; (#Bool (b λd let (f, g) = d; (#Bool (f λh #Bool (h T F) λ* F) g) λ* F) c)
|
||||
|
||||
(main) = (And (F, (T, F)))
|
||||
|
||||
(And$F0) = λa #Bool (a λb let (c, d) = b; (And$F0$F0 c d) λ* F)
|
||||
(F) = #Bool λ* #Bool λb b
|
||||
|
||||
(And$F0$F0) = λa #Bool (a λb #Bool (b T F) λ* F)
|
||||
|
||||
(F) = #Bool λT #Bool λF F
|
||||
|
||||
(T) = #Bool λT #Bool λF T
|
||||
(T) = #Bool λa #Bool λ* a
|
||||
|
||||
Scott:
|
||||
(And) = λa let (b, c) = a; (And$F0 b c)
|
||||
(And) = λa let (b, c) = a; (b λd let (f, g) = d; (f λh (h T F) λ* F g) λ* F c)
|
||||
|
||||
(main) = (And (F, (T, F)))
|
||||
|
||||
(And$F0) = λa (a λb let (c, d) = b; (And$F0$F0 c d) λ* F)
|
||||
(F) = λ* λb b
|
||||
|
||||
(And$F0$F0) = λa (a λb (b T F) λ* F)
|
||||
|
||||
(F) = λT λF F
|
||||
|
||||
(T) = λT λF T
|
||||
(T) = λa λ* a
|
||||
|
||||
|
||||
|
@ -5,27 +5,31 @@ input_file: tests/golden_tests/encode_pattern_match/bool.hvm
|
||||
TaggedScott:
|
||||
(not) = λa #bool (a false true)
|
||||
|
||||
(and) = λa #bool (a λb #bool (b true false) λc #bool (c false false))
|
||||
(and) = λa λb (#bool (a λc #bool (c true false) λg #bool (g false false)) b)
|
||||
|
||||
(and2) = λa #bool (a λb b λc false)
|
||||
(and2) = λa λb (#bool (a λc c λ* false) b)
|
||||
|
||||
(and3_$_and4) = λa #bool (a λb #bool (b true false) λc false)
|
||||
(and3) = λa λb (#bool (a λc #bool (c true false) λ* false) b)
|
||||
|
||||
(true) = #bool λtrue #bool λfalse true
|
||||
(and4) = λa λb (#bool (a λc #bool (c true false) λ* false) b)
|
||||
|
||||
(false) = #bool λtrue #bool λfalse false
|
||||
(false) = #bool λ* #bool λb b
|
||||
|
||||
(true) = #bool λa #bool λ* a
|
||||
|
||||
Scott:
|
||||
(not) = λa (a false true)
|
||||
|
||||
(and) = λa (a λb (b true false) λc (c false false))
|
||||
(and) = λa λb (a λc (c true false) λg (g false false) b)
|
||||
|
||||
(and2) = λa (a λb b λc false)
|
||||
(and2) = λa λb (a λc c λ* false b)
|
||||
|
||||
(and3_$_and4) = λa (a λb (b true false) λc false)
|
||||
(and3) = λa λb (a λc (c true false) λ* false b)
|
||||
|
||||
(true) = λtrue λfalse true
|
||||
(and4) = λa λb (a λc (c true false) λ* false b)
|
||||
|
||||
(false) = λtrue λfalse false
|
||||
(false) = λ* λb b
|
||||
|
||||
(true) = λa λ* a
|
||||
|
||||
|
||||
|
@ -3,25 +3,21 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/bool_tup.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(foo) = λa let (b, c) = a; (foo$F0 b c)
|
||||
(foo) = λa let (b, c) = a; (#Bool (b λd d λ* F) c)
|
||||
|
||||
(main) = (foo (F, T))
|
||||
|
||||
(foo$F0) = λa #Bool (a λb b λ* F)
|
||||
(F) = #Bool λ* #Bool λb b
|
||||
|
||||
(F) = #Bool λT #Bool λF F
|
||||
|
||||
(T) = #Bool λT #Bool λF T
|
||||
(T) = #Bool λa #Bool λ* a
|
||||
|
||||
Scott:
|
||||
(foo) = λa let (b, c) = a; (foo$F0 b c)
|
||||
(foo) = λa let (b, c) = a; (b λd d λ* F c)
|
||||
|
||||
(main) = (foo (F, T))
|
||||
|
||||
(foo$F0) = λa (a λb b λ* F)
|
||||
(F) = λ* λb b
|
||||
|
||||
(F) = λT λF F
|
||||
|
||||
(T) = λT λF T
|
||||
(T) = λa λ* a
|
||||
|
||||
|
||||
|
@ -5,11 +5,11 @@ input_file: tests/golden_tests/encode_pattern_match/box.hvm
|
||||
TaggedScott:
|
||||
(unbox) = λa #box (a #box.new.val λb b)
|
||||
|
||||
(new) = λval #box λnew #box.new.val (new val)
|
||||
(new) = λa #box λb #box.new.val (b a)
|
||||
|
||||
Scott:
|
||||
(unbox) = λa (a λb b)
|
||||
|
||||
(new) = λval λnew (new val)
|
||||
(new) = λa λb (b a)
|
||||
|
||||
|
||||
|
@ -3,73 +3,73 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/common.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(West) = #Direction λNorth #Direction λSouth #Direction λEast #Direction λWest West
|
||||
(West) = #Direction λ* #Direction λ* #Direction λ* #Direction λd d
|
||||
|
||||
(East) = #Direction λNorth #Direction λSouth #Direction λEast #Direction λWest East
|
||||
(East) = #Direction λ* #Direction λ* #Direction λc #Direction λ* c
|
||||
|
||||
(South) = #Direction λNorth #Direction λSouth #Direction λEast #Direction λWest South
|
||||
(South) = #Direction λ* #Direction λb #Direction λ* #Direction λ* b
|
||||
|
||||
(North) = #Direction λNorth #Direction λSouth #Direction λEast #Direction λWest North
|
||||
(North) = #Direction λa #Direction λ* #Direction λ* #Direction λ* a
|
||||
|
||||
(Filled) = λvalue #Box λFilled #Box λEmpty #Box.Filled.value (Filled value)
|
||||
(Filled) = λa #Box λb #Box λ* #Box.Filled.value (b a)
|
||||
|
||||
(Empty) = #Box λFilled #Box λEmpty Empty
|
||||
(Empty) = #Box λ* #Box λb b
|
||||
|
||||
(Some) = λx #Option λSome #Option λNone #Option.Some.x (Some x)
|
||||
(Some) = λa #Option λb #Option λ* #Option.Some.x (b a)
|
||||
|
||||
(None) = #Option λSome #Option λNone None
|
||||
(None) = #Option λ* #Option λb b
|
||||
|
||||
(Ok) = λa #Result λOk #Result λErr #Result.Ok.a (Ok a)
|
||||
(Ok) = λa #Result λb #Result λ* #Result.Ok.a (b a)
|
||||
|
||||
(Err) = λb #Result λOk #Result λErr #Result.Err.b (Err b)
|
||||
(Err) = λa #Result λ* #Result λc #Result.Err.b (c a)
|
||||
|
||||
(Cons) = λx λxs #List_ λCons #List_ λNil #List_.Cons.xs (#List_.Cons.x (Cons x) xs)
|
||||
(Cons) = λa λb #List_ λc #List_ λ* #List_.Cons.xs (#List_.Cons.x (c a) b)
|
||||
|
||||
(Nil) = #List_ λCons #List_ λNil Nil
|
||||
(Nil) = #List_ λ* #List_ λb b
|
||||
|
||||
(True) = #Bool λTrue #Bool λFalse True
|
||||
(True) = #Bool λa #Bool λ* a
|
||||
|
||||
(False) = #Bool λTrue #Bool λFalse False
|
||||
(False) = #Bool λ* #Bool λb b
|
||||
|
||||
(Red) = #Light λRed #Light λYellow #Light λGreen Red
|
||||
(Red) = #Light λa #Light λ* #Light λ* a
|
||||
|
||||
(Yellow) = #Light λRed #Light λYellow #Light λGreen Yellow
|
||||
(Yellow) = #Light λ* #Light λb #Light λ* b
|
||||
|
||||
(Green) = #Light λRed #Light λYellow #Light λGreen Green
|
||||
(Green) = #Light λ* #Light λ* #Light λc c
|
||||
|
||||
Scott:
|
||||
(West) = λNorth λSouth λEast λWest West
|
||||
(West) = λ* λ* λ* λd d
|
||||
|
||||
(East) = λNorth λSouth λEast λWest East
|
||||
(East) = λ* λ* λc λ* c
|
||||
|
||||
(South) = λNorth λSouth λEast λWest South
|
||||
(South) = λ* λb λ* λ* b
|
||||
|
||||
(North) = λNorth λSouth λEast λWest North
|
||||
(North) = λa λ* λ* λ* a
|
||||
|
||||
(Filled) = λvalue λFilled λEmpty (Filled value)
|
||||
(Filled) = λa λb λ* (b a)
|
||||
|
||||
(Empty) = λFilled λEmpty Empty
|
||||
(Empty) = λ* λb b
|
||||
|
||||
(Some) = λx λSome λNone (Some x)
|
||||
(Some) = λa λb λ* (b a)
|
||||
|
||||
(None) = λSome λNone None
|
||||
(None) = λ* λb b
|
||||
|
||||
(Ok) = λa λOk λErr (Ok a)
|
||||
(Ok) = λa λb λ* (b a)
|
||||
|
||||
(Err) = λb λOk λErr (Err b)
|
||||
(Err) = λa λ* λc (c a)
|
||||
|
||||
(Cons) = λx λxs λCons λNil (Cons x xs)
|
||||
(Cons) = λa λb λc λ* (c a b)
|
||||
|
||||
(Nil) = λCons λNil Nil
|
||||
(Nil) = λ* λb b
|
||||
|
||||
(True) = λTrue λFalse True
|
||||
(True) = λa λ* a
|
||||
|
||||
(False) = λTrue λFalse False
|
||||
(False) = λ* λb b
|
||||
|
||||
(Red) = λRed λYellow λGreen Red
|
||||
(Red) = λa λ* λ* a
|
||||
|
||||
(Yellow) = λRed λYellow λGreen Yellow
|
||||
(Yellow) = λ* λb λ* b
|
||||
|
||||
(Green) = λRed λYellow λGreen Green
|
||||
(Green) = λ* λ* λc c
|
||||
|
||||
|
||||
|
@ -3,25 +3,21 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/concat.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(String.concat) = λa λb (String.concat$match$1 a b)
|
||||
(String.concat) = λa λb (#String (a #String.String.cons.head λc #String.String.cons.tail λd λe (String.cons c (String.concat d e)) λh h) b)
|
||||
|
||||
(main) = (String.concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
|
||||
|
||||
(String.cons) = λhead λtail #String λString.cons #String λString.nil #String.String.cons.tail (#String.String.cons.head (String.cons head) tail)
|
||||
(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b)
|
||||
|
||||
(String.nil) = #String λString.cons #String λString.nil String.nil
|
||||
|
||||
(String.concat$match$1) = λa #String (a #String.String.cons.head λb #String.String.cons.tail λc λd (String.cons b (String.concat c d)) λe e)
|
||||
(String.nil) = #String λ* #String λb b
|
||||
|
||||
Scott:
|
||||
(String.concat) = λa λb (String.concat$match$1 a b)
|
||||
(String.concat) = λa λb (a λc λd λe (String.cons c (String.concat d e)) λh h b)
|
||||
|
||||
(main) = (String.concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
|
||||
|
||||
(String.cons) = λhead λtail λString.cons λString.nil (String.cons head tail)
|
||||
(String.cons) = λa λb λc λ* (c a b)
|
||||
|
||||
(String.nil) = λString.cons λString.nil String.nil
|
||||
|
||||
(String.concat$match$1) = λa (a λb λc λd (String.cons b (String.concat c d)) λe e)
|
||||
(String.nil) = λ* λb b
|
||||
|
||||
|
||||
|
@ -3,21 +3,21 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/concat_def.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(concat) = λa #String (a #String.String.cons.head λb #String.String.cons.tail λc λd (String.cons b (concat c d)) λe e)
|
||||
(concat) = λa λb (#String (a #String.String.cons.head λc #String.String.cons.tail λd λe (String.cons c (concat d e)) λi i) b)
|
||||
|
||||
(main) = (concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
|
||||
|
||||
(String.cons) = λhead λtail #String λString.cons #String λString.nil #String.String.cons.tail (#String.String.cons.head (String.cons head) tail)
|
||||
(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b)
|
||||
|
||||
(String.nil) = #String λString.cons #String λString.nil String.nil
|
||||
(String.nil) = #String λ* #String λb b
|
||||
|
||||
Scott:
|
||||
(concat) = λa (a λb λc λd (String.cons b (concat c d)) λe e)
|
||||
(concat) = λa λb (a λc λd λe (String.cons c (concat d e)) λi i b)
|
||||
|
||||
(main) = (concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
|
||||
|
||||
(String.cons) = λhead λtail λString.cons λString.nil (String.cons head tail)
|
||||
(String.cons) = λa λb λc λ* (c a b)
|
||||
|
||||
(String.nil) = λString.cons λString.nil String.nil
|
||||
(String.nil) = λ* λb b
|
||||
|
||||
|
||||
|
@ -3,25 +3,13 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/def_tups.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(go) = λa let (b, c) = a; (go$F0 b c)
|
||||
(go) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, h) = e; λi λj (let (k, l) = h; λm λn λo (+ (+ (+ (+ l k) o) n) m) i j g) f d) b)
|
||||
|
||||
(main) = (go (1, (2, (3, (4, 5)))))
|
||||
|
||||
(go$F0) = λa λb let (c, d) = b; (go$F0$F0 a c d)
|
||||
|
||||
(go$F0$F0) = λa λb λc let (d, e) = c; (go$F0$F0$F0 a b d e)
|
||||
|
||||
(go$F0$F0$F0) = λa λb λc λd let (e, f) = d; (+ (+ (+ (+ f e) c) b) a)
|
||||
|
||||
Scott:
|
||||
(go) = λa let (b, c) = a; (go$F0 b c)
|
||||
(go) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, h) = e; λi λj (let (k, l) = h; λm λn λo (+ (+ (+ (+ l k) o) n) m) i j g) f d) b)
|
||||
|
||||
(main) = (go (1, (2, (3, (4, 5)))))
|
||||
|
||||
(go$F0) = λa λb let (c, d) = b; (go$F0$F0 a c d)
|
||||
|
||||
(go$F0$F0) = λa λb λc let (d, e) = c; (go$F0$F0$F0 a b d e)
|
||||
|
||||
(go$F0$F0$F0) = λa λb λc λd let (e, f) = d; (+ (+ (+ (+ f e) c) b) a)
|
||||
|
||||
|
||||
|
@ -3,37 +3,25 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/definition_merge.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(Foo) = λa #Either (a #Either.Left.value λb λc (#Either (c #Either.Left.value λd λe (Foo$F0 e d) #Either.Right.value λf λg (Foo$F1 g f)) b) #Either.Right.value λh λi (#Either (i #Either.Left.value λj λk (Foo$F3_$_Foo$F2 k j) #Either.Right.value λl λm (Foo$F3_$_Foo$F2 m l)) h))
|
||||
(Foo) = λa λb (#Either (a #Either.Left.value λc λd (#Bool (c λe #Either (e #Either.Left.value λg #Bool (g 1 1) #Either.Right.value λj #Bool (j 2 2)) λm #Either (m #Either.Left.value λo #Bool (o 1 1) #Either.Right.value λr #Bool (r 2 2))) d) #Either.Right.value λu λv (#Bool (u λw #Either (w #Either.Left.value λy #Bool (y 3 3) #Either.Right.value λbb #Bool (bb 3 3)) λeb #Either (eb #Either.Left.value λgb #Bool (gb 3 3) #Either.Right.value λjb #Bool (jb 3 3))) v)) b)
|
||||
|
||||
(Foo$F3_$_Foo$F2) = λa #Bool (a λb #Bool (b 3 3) λc #Bool (c 3 3))
|
||||
(False) = #Bool λ* #Bool λb b
|
||||
|
||||
(False) = #Bool λTrue #Bool λFalse False
|
||||
(True) = #Bool λa #Bool λ* a
|
||||
|
||||
(Foo$F1) = λa #Bool (a λb #Bool (b 2 2) λc #Bool (c 2 2))
|
||||
(Right) = λa #Either λ* #Either λc #Either.Right.value (c a)
|
||||
|
||||
(Foo$F0) = λa #Bool (a λb #Bool (b 1 1) λc #Bool (c 1 1))
|
||||
|
||||
(Left) = λvalue #Either λLeft #Either λRight #Either.Left.value (Left value)
|
||||
|
||||
(Right) = λvalue #Either λLeft #Either λRight #Either.Right.value (Right value)
|
||||
|
||||
(True) = #Bool λTrue #Bool λFalse True
|
||||
(Left) = λa #Either λb #Either λ* #Either.Left.value (b a)
|
||||
|
||||
Scott:
|
||||
(Foo) = λa (a λb λc (c λd λe (Foo$F0 e d) λf λg (Foo$F1 g f) b) λh λi (i λj λk (Foo$F3_$_Foo$F2 k j) λl λm (Foo$F3_$_Foo$F2 m l) h))
|
||||
(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$F3_$_Foo$F2) = λa (a λb (b 3 3) λc (c 3 3))
|
||||
(False) = λ* λb b
|
||||
|
||||
(False) = λTrue λFalse False
|
||||
(True) = λa λ* a
|
||||
|
||||
(Foo$F1) = λa (a λb (b 2 2) λc (c 2 2))
|
||||
(Right) = λa λ* λc (c a)
|
||||
|
||||
(Foo$F0) = λa (a λb (b 1 1) λc (c 1 1))
|
||||
|
||||
(Left) = λvalue λLeft λRight (Left value)
|
||||
|
||||
(Right) = λvalue λLeft λRight (Right value)
|
||||
|
||||
(True) = λTrue λFalse True
|
||||
(Left) = λa λb λ* (b a)
|
||||
|
||||
|
||||
|
@ -3,57 +3,57 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/expr.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(Div) = #Op λAdd #Op λSub #Op λMul #Op λDiv Div
|
||||
(Div) = #Op λ* #Op λ* #Op λ* #Op λd d
|
||||
|
||||
(Mul) = #Op λAdd #Op λSub #Op λMul #Op λDiv Mul
|
||||
(Mul) = #Op λ* #Op λ* #Op λc #Op λ* c
|
||||
|
||||
(Sub) = #Op λAdd #Op λSub #Op λMul #Op λDiv Sub
|
||||
(Sub) = #Op λ* #Op λb #Op λ* #Op λ* b
|
||||
|
||||
(Add) = #Op λAdd #Op λSub #Op λMul #Op λDiv Add
|
||||
(Add) = #Op λa #Op λ* #Op λ* #Op λ* a
|
||||
|
||||
(Var) = λname #Expr λVar #Expr λNum #Expr λApp #Expr λFun #Expr λIf #Expr λLet #Expr λDup #Expr λTup #Expr λOp2 #Expr.Var.name (Var name)
|
||||
(Var) = λa #Expr λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.Var.name (b a)
|
||||
|
||||
(Num) = λval #Expr λVar #Expr λNum #Expr λApp #Expr λFun #Expr λIf #Expr λLet #Expr λDup #Expr λTup #Expr λOp2 #Expr.Num.val (Num val)
|
||||
(Num) = λa #Expr λ* #Expr λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.Num.val (c a)
|
||||
|
||||
(App) = λfun λarg #Expr λVar #Expr λNum #Expr λApp #Expr λFun #Expr λIf #Expr λLet #Expr λDup #Expr λTup #Expr λOp2 #Expr.App.arg (#Expr.App.fun (App fun) arg)
|
||||
(App) = λa λb #Expr λ* #Expr λ* #Expr λe #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.App.arg (#Expr.App.fun (e a) b)
|
||||
|
||||
(Fun) = λname λbody #Expr λVar #Expr λNum #Expr λApp #Expr λFun #Expr λIf #Expr λLet #Expr λDup #Expr λTup #Expr λOp2 #Expr.Fun.body (#Expr.Fun.name (Fun name) body)
|
||||
(Fun) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λf #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.Fun.body (#Expr.Fun.name (f a) b)
|
||||
|
||||
(If) = λcond λthen λelse #Expr λVar #Expr λNum #Expr λApp #Expr λFun #Expr λIf #Expr λLet #Expr λDup #Expr λTup #Expr λOp2 #Expr.If.else (#Expr.If.then (#Expr.If.cond (If cond) then) else)
|
||||
(If) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λh #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr.If.else (#Expr.If.then (#Expr.If.cond (h a) b) c)
|
||||
|
||||
(Let) = λbind λval λnext #Expr λVar #Expr λNum #Expr λApp #Expr λFun #Expr λIf #Expr λLet #Expr λDup #Expr λTup #Expr λOp2 #Expr.Let.next (#Expr.Let.val (#Expr.Let.bind (Let bind) val) next)
|
||||
(Let) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λi #Expr λ* #Expr λ* #Expr λ* #Expr.Let.next (#Expr.Let.val (#Expr.Let.bind (i a) b) c)
|
||||
|
||||
(Dup) = λfst λsnd λval λnext #Expr λVar #Expr λNum #Expr λApp #Expr λFun #Expr λIf #Expr λLet #Expr λDup #Expr λTup #Expr λOp2 #Expr.Dup.next (#Expr.Dup.val (#Expr.Dup.snd (#Expr.Dup.fst (Dup fst) snd) val) next)
|
||||
(Dup) = λa λb λc λd #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λk #Expr λ* #Expr λ* #Expr.Dup.next (#Expr.Dup.val (#Expr.Dup.snd (#Expr.Dup.fst (k a) b) c) d)
|
||||
|
||||
(Tup) = λfst λsnd #Expr λVar #Expr λNum #Expr λApp #Expr λFun #Expr λIf #Expr λLet #Expr λDup #Expr λTup #Expr λOp2 #Expr.Tup.snd (#Expr.Tup.fst (Tup fst) snd)
|
||||
(Tup) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λj #Expr λ* #Expr.Tup.snd (#Expr.Tup.fst (j a) b)
|
||||
|
||||
(Op2) = λop λfst λsnd #Expr λVar #Expr λNum #Expr λApp #Expr λFun #Expr λIf #Expr λLet #Expr λDup #Expr λTup #Expr λOp2 #Expr.Op2.snd (#Expr.Op2.fst (#Expr.Op2.op (Op2 op) fst) snd)
|
||||
(Op2) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λl #Expr.Op2.snd (#Expr.Op2.fst (#Expr.Op2.op (l a) b) c)
|
||||
|
||||
Scott:
|
||||
(Div) = λAdd λSub λMul λDiv Div
|
||||
(Div) = λ* λ* λ* λd d
|
||||
|
||||
(Mul) = λAdd λSub λMul λDiv Mul
|
||||
(Mul) = λ* λ* λc λ* c
|
||||
|
||||
(Sub) = λAdd λSub λMul λDiv Sub
|
||||
(Sub) = λ* λb λ* λ* b
|
||||
|
||||
(Add) = λAdd λSub λMul λDiv Add
|
||||
(Add) = λa λ* λ* λ* a
|
||||
|
||||
(Var) = λname λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Var name)
|
||||
(Var) = λa λb λ* λ* λ* λ* λ* λ* λ* λ* (b a)
|
||||
|
||||
(Num) = λval λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Num val)
|
||||
(Num) = λa λ* λc λ* λ* λ* λ* λ* λ* λ* (c a)
|
||||
|
||||
(App) = λfun λarg λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (App fun arg)
|
||||
(App) = λa λb λ* λ* λe λ* λ* λ* λ* λ* λ* (e a b)
|
||||
|
||||
(Fun) = λname λbody λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Fun name body)
|
||||
(Fun) = λa λb λ* λ* λ* λf λ* λ* λ* λ* λ* (f a b)
|
||||
|
||||
(If) = λcond λthen λelse λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (If cond then else)
|
||||
(If) = λa λb λc λ* λ* λ* λ* λh λ* λ* λ* λ* (h a b c)
|
||||
|
||||
(Let) = λbind λval λnext λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Let bind val next)
|
||||
(Let) = λa λb λc λ* λ* λ* λ* λ* λi λ* λ* λ* (i a b c)
|
||||
|
||||
(Dup) = λfst λsnd λval λnext λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Dup fst snd val next)
|
||||
(Dup) = λa λb λc λd λ* λ* λ* λ* λ* λ* λk λ* λ* (k a b c d)
|
||||
|
||||
(Tup) = λfst λsnd λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Tup fst snd)
|
||||
(Tup) = λa λb λ* λ* λ* λ* λ* λ* λ* λj λ* (j a b)
|
||||
|
||||
(Op2) = λop λfst λsnd λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Op2 op fst snd)
|
||||
(Op2) = λa λb λc λ* λ* λ* λ* λ* λ* λ* λ* λl (l a b c)
|
||||
|
||||
|
||||
|
@ -3,37 +3,21 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(Fn1) = λa let (b, c) = a; λd (Fn1$F0 b c d)
|
||||
(Fn1) = λa λb (let (c, d) = a; λe (let (f, *) = d; λ* λ* f c e) b)
|
||||
|
||||
(Fn2) = λa let (b, c) = a; (Fn2$F0 b c)
|
||||
(Fn2) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, *) = e; λ* λ* g f d) b)
|
||||
|
||||
(Fn3) = λa let (b, c) = a; λd (Fn3$F0 b c d)
|
||||
(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; +: λi λ* λ* i } d e) b)
|
||||
|
||||
(main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
|
||||
|
||||
(Fn3$F0) = λa match a { 0: λ* λ* 0; +: λb λ* λ* b }
|
||||
|
||||
(Fn2$F0) = λa λb let (c, d) = b; (Fn2$F0$F0 a c d)
|
||||
|
||||
(Fn2$F0$F0) = λa λb λc let (d, e) = c; d
|
||||
|
||||
(Fn1$F0) = λa λb let (c, d) = b; λ* c
|
||||
|
||||
Scott:
|
||||
(Fn1) = λa let (b, c) = a; λd (Fn1$F0 b c d)
|
||||
(Fn1) = λa λb (let (c, d) = a; λe (let (f, *) = d; λ* λ* f c e) b)
|
||||
|
||||
(Fn2) = λa let (b, c) = a; (Fn2$F0 b c)
|
||||
(Fn2) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, *) = e; λ* λ* g f d) b)
|
||||
|
||||
(Fn3) = λa let (b, c) = a; λd (Fn3$F0 b c d)
|
||||
(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; +: λi λ* λ* i } d e) b)
|
||||
|
||||
(main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
|
||||
|
||||
(Fn3$F0) = λa match a { 0: λ* λ* 0; +: λb λ* λ* b }
|
||||
|
||||
(Fn2$F0) = λa λb let (c, d) = b; (Fn2$F0$F0 a c d)
|
||||
|
||||
(Fn2$F0$F0) = λa λb λc let (d, e) = c; d
|
||||
|
||||
(Fn1$F0) = λa λb let (c, d) = b; λ* c
|
||||
|
||||
|
||||
|
@ -3,25 +3,21 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/is_some_some.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(some_some) = λa #Option (a #Option.Some.x λb (some_some$F0 b) 0)
|
||||
(some_some) = λa #Option (a #Option.Some.x λb #Option (b #Option.Some.x λ* 1 0) 0)
|
||||
|
||||
(main) = (some_some (Some 1))
|
||||
|
||||
(some_some$F0) = λa #Option (a #Option.Some.x λb 1 0)
|
||||
(None) = #Option λ* #Option λb b
|
||||
|
||||
(None) = #Option λSome #Option λNone None
|
||||
|
||||
(Some) = λx #Option λSome #Option λNone #Option.Some.x (Some x)
|
||||
(Some) = λa #Option λb #Option λ* #Option.Some.x (b a)
|
||||
|
||||
Scott:
|
||||
(some_some) = λa (a λb (some_some$F0 b) 0)
|
||||
(some_some) = λa (a λb (b λ* 1 0) 0)
|
||||
|
||||
(main) = (some_some (Some 1))
|
||||
|
||||
(some_some$F0) = λa (a λb 1 0)
|
||||
(None) = λ* λb b
|
||||
|
||||
(None) = λSome λNone None
|
||||
|
||||
(Some) = λx λSome λNone (Some x)
|
||||
(Some) = λa λb λ* (b a)
|
||||
|
||||
|
||||
|
@ -3,57 +3,49 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/list_merge_sort.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(If) = λa #Bool (a λb λc b λd λe e)
|
||||
(If) = λa λb λc (#Bool (a λd λ* d λ* λj j) b c)
|
||||
|
||||
(Pure) = λx (Cons x Nil)
|
||||
(Pure) = λa (Cons a Nil)
|
||||
|
||||
(Map) = λa #List_ (a #List_.Cons.head λb #List_.Cons.tail λc λd (Cons (d b) (Map c d)) λe Nil)
|
||||
(Map) = λa λb (#List_ (a #List_.Cons.head λc #List_.Cons.tail λd λe let {f f_2} = e; (Cons (f c) (Map d f_2)) λ* Nil) b)
|
||||
|
||||
(MergeSort) = λcmp λxs (Unpack cmp (Map xs Pure))
|
||||
(MergeSort) = λa λb (Unpack a (Map b Pure))
|
||||
|
||||
(Unpack) = λa λb (#List_ (b #List_.Cons.head λc #List_.Cons.tail λd λe (Unpack$F0 e c d) λf Nil) a)
|
||||
(Unpack) = λa λb (#List_ (b #List_.Cons.head λc #List_.Cons.tail λd λe (#List_ (d #List_.Cons.head λf #List_.Cons.tail λg λh λi let {o o_2} = h; (Unpack o (MergePair o_2 (Cons i (Cons f g)))) λ* λq q) e c) λ* Nil) a)
|
||||
|
||||
(MergePair) = λa λb (#List_ (b #List_.Cons.head λc #List_.Cons.tail λd λe (MergePair$F0 e c d) λf Nil) a)
|
||||
(MergePair) = λa λb (#List_ (b #List_.Cons.head λc #List_.Cons.tail λd λe (#List_ (d #List_.Cons.head λf #List_.Cons.tail λg λh λi let {m m_2} = h; (Cons (Merge m i f) (MergePair m_2 g)) λ* λo (Cons o Nil)) e c) λ* Nil) a)
|
||||
|
||||
(Merge) = λa λb (#List_ (b #List_.Cons.head λc #List_.Cons.tail λd λe λf (#List_ (f #List_.Cons.head λg #List_.Cons.tail λh λi λj λk (If (i j g) let l = (Cons g h); (Cons j (Merge i k l)) let m = (Cons j k); (Cons g (Merge i m h))) λn λo λp (Cons o p)) e c d) λq λr r) a)
|
||||
(Merge) = λa λb λc (#List_ (b #List_.Cons.head λd #List_.Cons.tail λe λf λg (#List_ (g #List_.Cons.head λh #List_.Cons.tail λi λj λk λl let {m m_2} = i; let {n n_dup} = h; let {n_2 n_3} = n_dup; let {o o_2} = l; let {p p_dup} = k; let {p_2 p_3} = p_dup; let {q q_dup} = j; let {q_2 q_3} = q_dup; (If (q p n) (Cons p_2 (Merge q_2 o (Cons n_2 m))) (Cons n_3 (Merge q_3 (Cons p_3 o_2) m_2))) λ* λu λv (Cons u v)) f d e) λ* λcb cb) a c)
|
||||
|
||||
(MergePair$F0) = λa λb λc (#List_ (c #List_.Cons.head λd #List_.Cons.tail λe λf λg (Cons (Merge f g d) (MergePair f e)) λh λi (Cons i Nil)) a b)
|
||||
(Nil) = #List_ λ* #List_ λb b
|
||||
|
||||
(Unpack$F0) = λa λb λc (#List_ (c #List_.Cons.head λd #List_.Cons.tail λe λf λg (Unpack f (MergePair f (Cons g (Cons d e)))) λh λi i) a b)
|
||||
(Cons) = λa λb #List_ λc #List_ λ* #List_.Cons.tail (#List_.Cons.head (c a) b)
|
||||
|
||||
(Nil) = #List_ λCons #List_ λNil Nil
|
||||
(False) = #Bool λ* #Bool λb b
|
||||
|
||||
(Cons) = λhead λtail #List_ λCons #List_ λNil #List_.Cons.tail (#List_.Cons.head (Cons head) tail)
|
||||
|
||||
(True) = #Bool λTrue #Bool λFalse True
|
||||
|
||||
(False) = #Bool λTrue #Bool λFalse False
|
||||
(True) = #Bool λa #Bool λ* a
|
||||
|
||||
Scott:
|
||||
(If) = λa (a λb λc b λd λe e)
|
||||
(If) = λa λb λc (a λd λ* d λ* λj j b c)
|
||||
|
||||
(Pure) = λx (Cons x Nil)
|
||||
(Pure) = λa (Cons a Nil)
|
||||
|
||||
(Map) = λa (a λb λc λd (Cons (d b) (Map c d)) λe Nil)
|
||||
(Map) = λa λb (a λc λd λe let {f f_2} = e; (Cons (f c) (Map d f_2)) λ* Nil b)
|
||||
|
||||
(MergeSort) = λcmp λxs (Unpack cmp (Map xs Pure))
|
||||
(MergeSort) = λa λb (Unpack a (Map b Pure))
|
||||
|
||||
(Unpack) = λa λb (b λc λd λe (Unpack$F0 e c d) λf Nil a)
|
||||
(Unpack) = λa λb (b λc λd λe (d λf λg λh λi let {o o_2} = h; (Unpack o (MergePair o_2 (Cons i (Cons f g)))) λ* λq q e c) λ* Nil a)
|
||||
|
||||
(MergePair) = λa λb (b λc λd λe (MergePair$F0 e c d) λf Nil a)
|
||||
(MergePair) = λa λb (b λc λd λe (d λf λg λh λi let {m m_2} = h; (Cons (Merge m i f) (MergePair m_2 g)) λ* λo (Cons o Nil) e c) λ* Nil a)
|
||||
|
||||
(Merge) = λa λb (b λc λd λe λf (f λg λh λi λj λk (If (i j g) let l = (Cons g h); (Cons j (Merge i k l)) let m = (Cons j k); (Cons g (Merge i m h))) λn λo λp (Cons o p) e c d) λq λr r a)
|
||||
(Merge) = λa λb λc (b λd λe λf λg (g λh λi λj λk λl let {m m_2} = i; let {n n_dup} = h; let {n_2 n_3} = n_dup; let {o o_2} = l; let {p p_dup} = k; let {p_2 p_3} = p_dup; let {q q_dup} = j; let {q_2 q_3} = q_dup; (If (q p n) (Cons p_2 (Merge q_2 o (Cons n_2 m))) (Cons n_3 (Merge q_3 (Cons p_3 o_2) m_2))) λ* λu λv (Cons u v) f d e) λ* λcb cb a c)
|
||||
|
||||
(MergePair$F0) = λa λb λc (c λd λe λf λg (Cons (Merge f g d) (MergePair f e)) λh λi (Cons i Nil) a b)
|
||||
(Nil) = λ* λb b
|
||||
|
||||
(Unpack$F0) = λa λb λc (c λd λe λf λg (Unpack f (MergePair f (Cons g (Cons d e)))) λh λi i a b)
|
||||
(Cons) = λa λb λc λ* (c a b)
|
||||
|
||||
(Nil) = λCons λNil Nil
|
||||
(False) = λ* λb b
|
||||
|
||||
(Cons) = λhead λtail λCons λNil (Cons head tail)
|
||||
|
||||
(True) = λTrue λFalse True
|
||||
|
||||
(False) = λTrue λFalse False
|
||||
(True) = λa λ* a
|
||||
|
||||
|
||||
|
@ -1,17 +0,0 @@
|
||||
---
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared.hvm
|
||||
---
|
||||
(main) = λa λb let a = (main$match$1 a); let b = (main$match$2 b); (a, b)
|
||||
|
||||
(SCons) = λhead λtail #String λSCons #String λSNil #String.SCons.tail (#String.SCons.head (SCons head) tail)
|
||||
|
||||
(SNil) = #String λSCons #String λSNil SNil
|
||||
|
||||
(LCons) = λhead λtail #List λLCons #List λLNil #List.LCons.tail (#List.LCons.head (LCons head) tail)
|
||||
|
||||
(LNil) = #List λLCons #List λLNil LNil
|
||||
|
||||
(main$match$1) = λa #String (a #String.SCons.head λb #String.SCons.tail λc 1 2)
|
||||
|
||||
(main$match$2) = λa #List (a #List.LCons.head λb #List.LCons.tail λc 1 2)
|
@ -5,23 +5,23 @@ input_file: tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared
|
||||
TaggedScott:
|
||||
(main) = *
|
||||
|
||||
(Foo) = λa #String (a #String.String.cons.head λb #String.String.cons.tail λc 1 0)
|
||||
(Foo) = λa #String (a #String.String.cons.head λ* #String.String.cons.tail λ* 1 0)
|
||||
|
||||
(Bar) = λa #List (a #List.List.cons.head λb #List.List.cons.tail λc 0 1)
|
||||
(Bar) = λa #List (a #List.List.cons.head λ* #List.List.cons.tail λ* 0 1)
|
||||
|
||||
(String.cons) = λhead λtail #String λString.cons #String λString.nil #String.String.cons.tail (#String.String.cons.head (String.cons head) tail)
|
||||
(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b)
|
||||
|
||||
(String.nil) = #String λString.cons #String λString.nil String.nil
|
||||
(String.nil) = #String λ* #String λb b
|
||||
|
||||
(List.cons) = λhead λtail #List λList.cons #List λList.nil #List.List.cons.tail (#List.List.cons.head (List.cons head) tail)
|
||||
(List.cons) = λa λb #List λc #List λ* #List.List.cons.tail (#List.List.cons.head (c a) b)
|
||||
|
||||
(List.nil) = #List λList.cons #List λList.nil List.nil
|
||||
(List.nil) = #List λ* #List λb b
|
||||
|
||||
Scott:
|
||||
(main) = *
|
||||
|
||||
(Foo) = λa (a λb λc 1 0)
|
||||
(Foo) = λa (a λ* λ* 1 0)
|
||||
|
||||
(Bar) = λa (a λb λc 0 1)
|
||||
(Bar) = λa (a λ* λ* 0 1)
|
||||
|
||||
|
||||
|
@ -3,23 +3,17 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared_map.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = λa λb let a = (main$match$1 a); let b = (main$match$2 b); (a, b)
|
||||
(main) = λa λb (#String (a #String.String.cons.head λ* #String.String.cons.tail λ* 1 2), #List (b #List.List.cons.head λ* #List.List.cons.tail λ* 1 2))
|
||||
|
||||
(String.cons) = λhead λtail #String λString.cons #String λString.nil #String.String.cons.tail (#String.String.cons.head (String.cons head) tail)
|
||||
(String.cons) = λa λb #String λc #String λ* #String.String.cons.tail (#String.String.cons.head (c a) b)
|
||||
|
||||
(String.nil) = #String λString.cons #String λString.nil String.nil
|
||||
(String.nil) = #String λ* #String λb b
|
||||
|
||||
(List.cons) = λhead λtail #List λList.cons #List λList.nil #List.List.cons.tail (#List.List.cons.head (List.cons head) tail)
|
||||
(List.cons) = λa λb #List λc #List λ* #List.List.cons.tail (#List.List.cons.head (c a) b)
|
||||
|
||||
(List.nil) = #List λList.cons #List λList.nil List.nil
|
||||
|
||||
(main$match$1) = λa #String (a #String.String.cons.head λb #String.String.cons.tail λc 1 2)
|
||||
|
||||
(main$match$2) = λa #List (a #List.List.cons.head λb #List.List.cons.tail λc 1 2)
|
||||
(List.nil) = #List λ* #List λb b
|
||||
|
||||
Scott:
|
||||
(main) = λa λb let a = (main$match$2_$_main$match$1 a); let b = (main$match$2_$_main$match$1 b); (a, b)
|
||||
|
||||
(main$match$2_$_main$match$1) = λa (a λb λc 1 2)
|
||||
(main) = λa λb ((a λ* λ* 1 2), (b λ* λ* 1 2))
|
||||
|
||||
|
||||
|
@ -3,21 +3,17 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_in_arm.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = λx (main$match$1 x)
|
||||
(main) = λa #bool (a λ$x $x λd d)
|
||||
|
||||
(main$match$1) = λa #bool (a λ$x $x λb b)
|
||||
(F) = #bool λ* #bool λb b
|
||||
|
||||
(F) = #bool λT #bool λF F
|
||||
|
||||
(T) = #bool λT #bool λF T
|
||||
(T) = #bool λa #bool λ* a
|
||||
|
||||
Scott:
|
||||
(main) = λx (main$match$1 x)
|
||||
(main) = λa (a λ$x $x λd d)
|
||||
|
||||
(main$match$1) = λa (a λ$x $x λb b)
|
||||
(F) = λ* λb b
|
||||
|
||||
(F) = λT λF F
|
||||
|
||||
(T) = λT λF T
|
||||
(T) = λa λ* a
|
||||
|
||||
|
||||
|
@ -2,6 +2,18 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hvm
|
||||
---
|
||||
In definition 'main':
|
||||
Unable to linearize variable λ$x in a match block.
|
||||
TaggedScott:
|
||||
(main) = (#Maybe ((Some 1) λ$x * #Maybe.Some.val λc c) $x)
|
||||
|
||||
(Some) = λa #Maybe λ* #Maybe λc #Maybe.Some.val (c a)
|
||||
|
||||
(None) = #Maybe λa #Maybe λ* a
|
||||
|
||||
Scott:
|
||||
(main) = (Some 1 λ$x * λc c $x)
|
||||
|
||||
(Some) = λa λ* λc (c a)
|
||||
|
||||
(None) = λa λ* a
|
||||
|
||||
|
||||
|
@ -3,29 +3,25 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(Foo) = λ$x let %matched = (Some 1); (Bar$match$1_$_Foo$match$1 %matched $x)
|
||||
(Foo) = λ$x #Maybe ((Some 1) $x #Maybe.Some.val λc c)
|
||||
|
||||
(Bar) = (let %matched = (Some 1); (Bar$match$1_$_Foo$match$1 %matched $x) λ$x *)
|
||||
(Bar) = (#Maybe ((Some 1) $x #Maybe.Some.val λc c) λ$x *)
|
||||
|
||||
(main) = *
|
||||
|
||||
(Bar$match$1_$_Foo$match$1) = λa #Maybe (a λb b #Maybe.Some.val λc λd c)
|
||||
(Some) = λa #Maybe λ* #Maybe λc #Maybe.Some.val (c a)
|
||||
|
||||
(None) = #Maybe λNone #Maybe λSome None
|
||||
|
||||
(Some) = λval #Maybe λNone #Maybe λSome #Maybe.Some.val (Some val)
|
||||
(None) = #Maybe λa #Maybe λ* a
|
||||
|
||||
Scott:
|
||||
(Foo) = λ$x let %matched = (Some 1); (Bar$match$1_$_Foo$match$1 %matched $x)
|
||||
(Foo) = λ$x (Some 1 $x λc c)
|
||||
|
||||
(Bar) = (let %matched = (Some 1); (Bar$match$1_$_Foo$match$1 %matched $x) λ$x *)
|
||||
(Bar) = (Some 1 $x λc c λ$x *)
|
||||
|
||||
(main) = *
|
||||
|
||||
(Bar$match$1_$_Foo$match$1) = λa (a λb b λc λd c)
|
||||
(Some) = λa λ* λc (c a)
|
||||
|
||||
(None) = λNone λSome None
|
||||
|
||||
(Some) = λval λNone λSome (Some val)
|
||||
(None) = λa λ* a
|
||||
|
||||
|
||||
|
@ -3,12 +3,12 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_bind.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(cheese) = let num = (+ 2 3); (match num { 0: λnum 653323; +num-1: λnum (+ num num-1) } num)
|
||||
(cheese) = let {a a_2} = (+ 2 3); (match a { 0: λ* 653323; +: λd λe (+ e d) } a_2)
|
||||
|
||||
(main) = cheese
|
||||
|
||||
Scott:
|
||||
(cheese) = let num = (+ 2 3); (match num { 0: λnum 653323; +num-1: λnum (+ num num-1) } num)
|
||||
(cheese) = let {a a_2} = (+ 2 3); (match a { 0: λ* 653323; +: λd λe (+ e d) } a_2)
|
||||
|
||||
(main) = cheese
|
||||
|
||||
|
@ -3,21 +3,17 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_list_sugar.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = let %matched = List.nil; (main$match$1 %matched)
|
||||
(main) = #List (List.nil #List.List.cons.head λ* #List.List.cons.tail λ* 1 0)
|
||||
|
||||
(main$match$1) = λa #List (a #List.List.cons.head λb #List.List.cons.tail λc 1 0)
|
||||
(List.nil) = #List λ* #List λb b
|
||||
|
||||
(List.nil) = #List λList.cons #List λList.nil List.nil
|
||||
|
||||
(List.cons) = λhead λtail #List λList.cons #List λList.nil #List.List.cons.tail (#List.List.cons.head (List.cons head) tail)
|
||||
(List.cons) = λa λb #List λc #List λ* #List.List.cons.tail (#List.List.cons.head (c a) b)
|
||||
|
||||
Scott:
|
||||
(main) = let %matched = List.nil; (main$match$1 %matched)
|
||||
(main) = (List.nil λ* λ* 1 0)
|
||||
|
||||
(main$match$1) = λa (a λb λc 1 0)
|
||||
(List.nil) = λ* λb b
|
||||
|
||||
(List.nil) = λList.cons λList.nil List.nil
|
||||
|
||||
(List.cons) = λhead λtail λList.cons λList.nil (List.cons head tail)
|
||||
(List.cons) = λa λb λc λ* (c a b)
|
||||
|
||||
|
||||
|
@ -0,0 +1,55 @@
|
||||
---
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_many_args.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(tail_tail) = λa #L (a #L.C.h λb #L.C.t λc (#L (c #L.C.h λ* #L.C.t λe λ* e λ* N) b) N)
|
||||
|
||||
(or) = λa λb (#Option (b #Option.Some.val λc λ* c λf f) a)
|
||||
|
||||
(or2) = λa λb (#Option (a #Option.Some.val λc λ* c λf f) b)
|
||||
|
||||
(map) = λa λb (#Option (b #Option.Some.val λc λd (d c) λ* None) a)
|
||||
|
||||
(map2) = λa λb (#Option (b #Option.Some.val λc λd (d c) λ* None) a)
|
||||
|
||||
(flatten) = λa #Option (a #Option.Some.val λb #Option (b #Option.Some.val λc (Some c) None) None)
|
||||
|
||||
(map_pair) = λa λb λc (#L (b #L.C.h λd #L.C.t λe λf λg (#L (g #L.C.h λh #L.C.t λi λj λk λl (C (j k h) (map_pair l i)) λ* λ* λ* N) f d e) λ* λ* N) a c)
|
||||
|
||||
(main) = *
|
||||
|
||||
(None) = #Option λ* #Option λb b
|
||||
|
||||
(Some) = λa #Option λb #Option λ* #Option.Some.val (b a)
|
||||
|
||||
(N) = #L λ* #L λb b
|
||||
|
||||
(C) = λa λb #L λc #L λ* #L.C.t (#L.C.h (c a) b)
|
||||
|
||||
Scott:
|
||||
(tail_tail) = λa (a λb λc (c λ* λe λ* e λ* N b) N)
|
||||
|
||||
(or) = λa λb (b λc λ* c λf f a)
|
||||
|
||||
(or2) = λa λb (a λc λ* c λf f b)
|
||||
|
||||
(map) = λa λb (b λc λd (d c) λ* None a)
|
||||
|
||||
(map2) = λa λb (b λc λd (d c) λ* None a)
|
||||
|
||||
(flatten) = λa (a λb (b λc (Some c) None) None)
|
||||
|
||||
(map_pair) = λa λb λc (b λd λe λf λg (g λh λi λj λk λl (C (j k h) (map_pair l i)) λ* λ* λ* N f d e) λ* λ* N a c)
|
||||
|
||||
(main) = *
|
||||
|
||||
(None) = λ* λb b
|
||||
|
||||
(Some) = λa λb λ* (b a)
|
||||
|
||||
(N) = λ* λb b
|
||||
|
||||
(C) = λa λb λc λ* (c a b)
|
||||
|
||||
|
@ -3,21 +3,17 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_syntax.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(head) = λx (head$match$1 x)
|
||||
(head) = λa #List_ (a #List_.Cons.x λc #List_.Cons.xs λ* c Nil)
|
||||
|
||||
(head$match$1) = λa #List_ (a #List_.Cons.x λb #List_.Cons.xs λc b Nil)
|
||||
(Nil) = #List_ λ* #List_ λb b
|
||||
|
||||
(Nil) = #List_ λCons #List_ λNil Nil
|
||||
|
||||
(Cons) = λx λxs #List_ λCons #List_ λNil #List_.Cons.xs (#List_.Cons.x (Cons x) xs)
|
||||
(Cons) = λa λb #List_ λc #List_ λ* #List_.Cons.xs (#List_.Cons.x (c a) b)
|
||||
|
||||
Scott:
|
||||
(head) = λx (head$match$1 x)
|
||||
(head) = λa (a λc λ* c Nil)
|
||||
|
||||
(head$match$1) = λa (a λb λc b Nil)
|
||||
(Nil) = λ* λb b
|
||||
|
||||
(Nil) = λCons λNil Nil
|
||||
|
||||
(Cons) = λx λxs λCons λNil (Cons x xs)
|
||||
(Cons) = λa λb λc λ* (c a b)
|
||||
|
||||
|
||||
|
@ -3,13 +3,21 @@ source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/merge_recursive.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(foo_1_$_bar_1) = λx (x foo_2_$_bar_2)
|
||||
(foo_1) = λa (a foo_2)
|
||||
|
||||
(foo_2_$_bar_2) = λa λb (a, b)
|
||||
(foo_2) = λa λb (a, b)
|
||||
|
||||
(bar_1) = λa (a bar_2)
|
||||
|
||||
(bar_2) = λa λb (a, b)
|
||||
|
||||
Scott:
|
||||
(foo_1_$_bar_1) = λx (x foo_2_$_bar_2)
|
||||
(foo_1) = λa (a foo_2)
|
||||
|
||||
(foo_2_$_bar_2) = λa λb (a, b)
|
||||
(foo_2) = λa λb (a, b)
|
||||
|
||||
(bar_1) = λa (a bar_2)
|
||||
|
||||
(bar_2) = λa λb (a, b)
|
||||
|
||||
|
||||
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user