mirror of
https://github.com/HigherOrderCO/Bend.git
synced 2024-08-16 15:20:40 +03:00
[sc-410] Add untagged scott encoding option for ADTs
This commit is contained in:
Nicolas Abril
parent
291ff8ce10
commit
3e9b3d7e58
48
Cargo.lock
generated
48
Cargo.lock
generated
@ -68,12 +68,6 @@ version = "0.5.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3a8241f3ebb85c056b509d4327ad0358fbbba6ffb340bf388f26350aeda225b1"
|
||||
|
||||
[[package]]
|
||||
name = "bitflags"
|
||||
version = "1.3.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
|
||||
|
||||
[[package]]
|
||||
name = "cc"
|
||||
version = "1.0.83"
|
||||
@ -130,7 +124,7 @@ dependencies = [
|
||||
"heck",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn 2.0.48",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
@ -226,9 +220,8 @@ dependencies = [
|
||||
"hvm-core",
|
||||
"indexmap",
|
||||
"insta",
|
||||
"itertools 0.11.0",
|
||||
"itertools",
|
||||
"logos",
|
||||
"shrinkwraprs",
|
||||
"stdext",
|
||||
"walkdir",
|
||||
]
|
||||
@ -256,15 +249,6 @@ dependencies = [
|
||||
"yaml-rust",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "itertools"
|
||||
version = "0.8.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f56a2d0bc861f9165be4eb3442afd3c236d8a98afd426f65d92324ae1091a484"
|
||||
dependencies = [
|
||||
"either",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "itertools"
|
||||
version = "0.11.0"
|
||||
@ -312,7 +296,7 @@ dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"regex-syntax",
|
||||
"syn 2.0.48",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
@ -378,19 +362,6 @@ dependencies = [
|
||||
"winapi-util",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "shrinkwraprs"
|
||||
version = "0.3.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e63e6744142336dfb606fe2b068afa2e1cca1ee6a5d8377277a92945d81fa331"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
"itertools 0.8.2",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn 1.0.109",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "similar"
|
||||
version = "2.4.0"
|
||||
@ -422,17 +393,6 @@ version = "0.10.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "1.0.109"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"unicode-ident",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "2.0.48"
|
||||
@ -595,5 +555,5 @@ checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn 2.0.48",
|
||||
"syn",
|
||||
]
|
||||
|
||||
@ -27,9 +27,8 @@ hvm-core = { git = "https://github.com/HigherOrderCO/hvm-core" }
|
||||
indexmap = "2.1.0"
|
||||
itertools = "0.11.0"
|
||||
logos = "0.13.0"
|
||||
shrinkwraprs = "0.3.0"
|
||||
|
||||
[dev-dependencies]
|
||||
insta = "1.34.0"
|
||||
stdext = "0.3.1"
|
||||
walkdir = "2.3.3"
|
||||
insta = "1.34.0"
|
||||
|
||||
2
justfile
2
justfile
@ -10,7 +10,7 @@ rustup-show:
|
||||
rustup show
|
||||
|
||||
test:
|
||||
cargo test --workspace
|
||||
cargo insta test --workspace
|
||||
|
||||
clippy:
|
||||
cargo clippy
|
||||
|
||||
32
src/lib.rs
32
src/lib.rs
@ -10,10 +10,10 @@ use itertools::Itertools;
|
||||
use net::{hvmc_to_net::hvmc_to_net, net_to_hvmc::nets_to_hvmc};
|
||||
use std::time::Instant;
|
||||
use term::{
|
||||
book_to_nets, net_to_term,
|
||||
net_to_term::ReadbackErrors,
|
||||
book_to_nets,
|
||||
net_to_term::{net_to_term, ReadbackErrors},
|
||||
term_to_net::{HvmcNames, Labels},
|
||||
Book, DefName, Name, Term,
|
||||
AdtEncoding, Book, DefName, Name, Term,
|
||||
};
|
||||
|
||||
pub mod hvmc_net;
|
||||
@ -56,9 +56,9 @@ pub fn desugar_book(
|
||||
let mut warnings = Vec::new();
|
||||
let main = book.check_has_entrypoint(entrypoint)?;
|
||||
book.check_shared_names()?;
|
||||
book.generate_scott_adts();
|
||||
book.encode_adts(opts.adt_encoding);
|
||||
book.encode_builtins();
|
||||
encode_pattern_matching(book, &mut warnings)?;
|
||||
encode_pattern_matching(book, &mut warnings, opts.adt_encoding)?;
|
||||
// sanity check
|
||||
book.check_unbound_vars()?;
|
||||
book.normalize_native_matches()?;
|
||||
@ -77,7 +77,7 @@ pub fn desugar_book(
|
||||
if opts.simplify_main {
|
||||
book.simplify_main_ref(&main);
|
||||
}
|
||||
book.prune(Some(&main), opts.prune, &mut warnings);
|
||||
book.prune(Some(&main), opts.prune, opts.adt_encoding, &mut warnings);
|
||||
if opts.inline {
|
||||
book.inline();
|
||||
}
|
||||
@ -87,7 +87,11 @@ pub fn desugar_book(
|
||||
Ok((main, warnings))
|
||||
}
|
||||
|
||||
pub fn encode_pattern_matching(book: &mut Book, warnings: &mut Vec<Warning>) -> Result<(), String> {
|
||||
pub fn encode_pattern_matching(
|
||||
book: &mut Book,
|
||||
warnings: &mut Vec<Warning>,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Result<(), String> {
|
||||
book.check_arity()?;
|
||||
book.resolve_ctrs_in_pats();
|
||||
book.check_unbound_pats()?;
|
||||
@ -102,7 +106,7 @@ pub fn encode_pattern_matching(book: &mut Book, warnings: &mut Vec<Warning>) ->
|
||||
book.flatten_rules();
|
||||
let def_types = book.infer_def_types()?;
|
||||
book.check_exhaustive_patterns(&def_types)?;
|
||||
book.encode_pattern_matching_functions(&def_types);
|
||||
book.encode_pattern_matching_functions(&def_types, adt_encoding);
|
||||
Ok(())
|
||||
}
|
||||
|
||||
@ -119,10 +123,11 @@ pub fn run_book(
|
||||
|
||||
display_warnings(warning_opts, &warnings)?;
|
||||
|
||||
let debug_hook = run_opts.debug_hook(&book, &hvmc_names, &labels);
|
||||
let debug_hook = run_opts.debug_hook(&book, &hvmc_names, &labels, &compile_opts.adt_encoding);
|
||||
let (res_lnet, stats) = run_compiled(&core_book, mem_size, run_opts, debug_hook, &book.hvmc_entrypoint());
|
||||
let net = hvmc_to_net(&res_lnet, &hvmc_names.hvmc_to_hvml);
|
||||
let (res_term, readback_errors) = net_to_term(&net, &book, &labels, run_opts.linear);
|
||||
let (res_term, readback_errors) =
|
||||
net_to_term(&net, &book, &labels, run_opts.linear, compile_opts.adt_encoding);
|
||||
let info = RunInfo { stats, readback_errors, net: res_lnet };
|
||||
Ok((res_term, info))
|
||||
}
|
||||
@ -199,11 +204,12 @@ impl RunOpts {
|
||||
book: &'a Book,
|
||||
hvmc_names: &'a HvmcNames,
|
||||
labels: &'a Labels,
|
||||
adt_encoding: &'a AdtEncoding,
|
||||
) -> Option<impl FnMut(&Net) + 'a> {
|
||||
self.debug.then_some({
|
||||
|net: &_| {
|
||||
let net = hvmc_to_net(net, &hvmc_names.hvmc_to_hvml);
|
||||
let (res_term, errors) = net_to_term(&net, book, labels, self.linear);
|
||||
let (res_term, errors) = net_to_term(&net, book, labels, self.linear, *adt_encoding);
|
||||
println!("{}{}\n---------------------------------------", errors.display(), res_term.display())
|
||||
}
|
||||
})
|
||||
@ -212,6 +218,9 @@ impl RunOpts {
|
||||
|
||||
#[derive(Clone, Copy, Debug, Default)]
|
||||
pub struct CompileOpts {
|
||||
/// Selects the encoding for the ADT syntax.
|
||||
pub adt_encoding: AdtEncoding,
|
||||
|
||||
/// Enables [term::transform::eta_reduction].
|
||||
pub eta: bool,
|
||||
|
||||
@ -253,6 +262,7 @@ impl CompileOpts {
|
||||
pre_reduce_refs: true,
|
||||
merge: true,
|
||||
inline: true,
|
||||
adt_encoding: Default::default(),
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@ -1,8 +1,9 @@
|
||||
use clap::{Args, CommandFactory, Parser, Subcommand};
|
||||
use hvmc::ast::{show_book, show_net};
|
||||
use hvml::{
|
||||
check_book, compile_book, desugar_book, load_file_to_book, run_book, term::Name, CompileOpts, RunInfo,
|
||||
RunOpts, WarnState, WarningOpts,
|
||||
check_book, compile_book, desugar_book, load_file_to_book, run_book,
|
||||
term::{AdtEncoding, Name},
|
||||
CompileOpts, RunInfo, RunOpts, WarnState, WarningOpts,
|
||||
};
|
||||
use std::{path::PathBuf, vec::IntoIter};
|
||||
|
||||
@ -267,6 +268,8 @@ pub enum OptArgs {
|
||||
NoMerge,
|
||||
Inline,
|
||||
NoInline,
|
||||
AdtScott,
|
||||
AdtTaggedScott,
|
||||
}
|
||||
|
||||
impl OptArgs {
|
||||
@ -295,6 +298,8 @@ impl OptArgs {
|
||||
NoMerge => opts.merge = false,
|
||||
Inline => opts.inline = true,
|
||||
NoInline => opts.inline = false,
|
||||
AdtScott => opts.adt_encoding = AdtEncoding::Scott,
|
||||
AdtTaggedScott => opts.adt_encoding = AdtEncoding::TaggedScott,
|
||||
}
|
||||
}
|
||||
opts
|
||||
|
||||
@ -19,10 +19,7 @@ pub fn nets_to_hvmc(nets: HashMap<String, INet>, hvmc_names: &HvmcNames) -> Resu
|
||||
}
|
||||
|
||||
/// Convert an inet-encoded definition into an hvmc AST inet.
|
||||
pub fn net_to_hvmc(
|
||||
inet: &INet,
|
||||
hvml_to_hvmc_name: &HashMap<DefName, Val>,
|
||||
) -> Result<Net, String> {
|
||||
pub fn net_to_hvmc(inet: &INet, hvml_to_hvmc_name: &HashMap<DefName, Val>) -> Result<Net, String> {
|
||||
let (net_root, redxs) = get_tree_roots(inet)?;
|
||||
let mut port_to_var_id: HashMap<Port, VarId> = HashMap::new();
|
||||
let root = if let Some(net_root) = net_root {
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
use super::{parser::parse_definition_book, Book, DefName, Origin, Pattern, Tag, TagName, Term, VarName};
|
||||
use super::{parser::parse_definition_book, Book, DefName, Origin, Pattern, Term};
|
||||
use hvmc::run::Val;
|
||||
|
||||
const BUILTINS: &str = include_str!(concat!(env!("CARGO_MANIFEST_DIR"), "/src/term/builtins.hvm"));
|
||||
@ -105,21 +105,3 @@ impl Pattern {
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
impl Tag {
|
||||
pub fn string() -> Self {
|
||||
Tag::adt_name(&TagName::new(STRING))
|
||||
}
|
||||
|
||||
pub fn string_scons_head() -> Self {
|
||||
Tag::adt_field(&DefName::new(STRING), &DefName::new(SCONS), &VarName::new(HEAD))
|
||||
}
|
||||
|
||||
pub fn list() -> Self {
|
||||
Tag::adt_name(&TagName::new(LIST))
|
||||
}
|
||||
|
||||
pub fn list_lcons_head() -> Self {
|
||||
Tag::adt_field(&DefName::new(LIST), &DefName::new(LCONS), &VarName::new(HEAD))
|
||||
}
|
||||
}
|
||||
|
||||
@ -248,7 +248,7 @@ impl ReadbackError {
|
||||
ReadbackError::InvalidBind => write!(f, "Invalid Bind"),
|
||||
ReadbackError::InvalidAdt => write!(f, "Invalid Adt"),
|
||||
ReadbackError::UnexpectedTag(exp, fnd) => {
|
||||
write!(f, "Unexpected tag found during Adt readback, expected '#{}', but found ", exp)?;
|
||||
write!(f, "Unexpected tag found during Adt readback, expected '{}', but found ", exp.display())?;
|
||||
|
||||
match fnd {
|
||||
Tag::Static => write!(f, "no tag"),
|
||||
|
||||
@ -192,6 +192,14 @@ pub struct Adt {
|
||||
pub origin: Origin,
|
||||
}
|
||||
|
||||
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
|
||||
pub enum AdtEncoding {
|
||||
Scott,
|
||||
|
||||
#[default]
|
||||
TaggedScott,
|
||||
}
|
||||
|
||||
#[derive(Debug, PartialEq, Eq, Clone, Hash, PartialOrd, Ord, Default)]
|
||||
pub struct Name(pub Arc<String>);
|
||||
|
||||
@ -730,11 +738,11 @@ impl Type {
|
||||
Type::None => vec![],
|
||||
Type::Any => vec![],
|
||||
Type::Tup => vec![Pattern::Tup(
|
||||
Box::new(Pattern::Var(Some(Name::new("fst")))),
|
||||
Box::new(Pattern::Var(Some(Name::new("snd")))),
|
||||
Box::new(Pattern::Var(Some(Name::new("%fst")))),
|
||||
Box::new(Pattern::Var(Some(Name::new("%snd")))),
|
||||
)],
|
||||
Type::Num => {
|
||||
vec![Pattern::Num(MatchNum::Zero), Pattern::Num(MatchNum::Succ(Some(Some(Name::new("pred")))))]
|
||||
vec![Pattern::Num(MatchNum::Zero), Pattern::Num(MatchNum::Succ(Some(Some(Name::new("%pred")))))]
|
||||
}
|
||||
Type::Adt(adt) => {
|
||||
// TODO: Should return just a ref to ctrs and not clone.
|
||||
|
||||
@ -1,6 +1,8 @@
|
||||
use crate::{
|
||||
net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT},
|
||||
term::{num_to_name, term_to_net::Labels, Book, MatchNum, Op, Pattern, Tag, TagName, Term, Val, VarName},
|
||||
term::{
|
||||
num_to_name, term_to_net::Labels, AdtEncoding, Book, MatchNum, Op, Pattern, Tag, Term, Val, VarName,
|
||||
},
|
||||
};
|
||||
use hvmc::run::Loc;
|
||||
use indexmap::IndexSet;
|
||||
@ -8,7 +10,13 @@ use std::collections::{HashMap, HashSet};
|
||||
|
||||
// TODO: Display scopeless lambdas as such
|
||||
/// Converts an Interaction-INet to a Lambda Calculus term
|
||||
pub fn net_to_term(net: &INet, book: &Book, labels: &Labels, linear: bool) -> (Term, ReadbackErrors) {
|
||||
pub fn net_to_term(
|
||||
net: &INet,
|
||||
book: &Book,
|
||||
labels: &Labels,
|
||||
linear: bool,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> (Term, ReadbackErrors) {
|
||||
let mut reader = Reader {
|
||||
net,
|
||||
labels,
|
||||
@ -40,7 +48,7 @@ pub fn net_to_term(net: &INet, book: &Book, labels: &Labels, linear: bool) -> (T
|
||||
debug_assert_eq!(result, None);
|
||||
}
|
||||
|
||||
reader.resugar_adts(&mut term);
|
||||
reader.resugar_adts(&mut term, adt_encoding);
|
||||
|
||||
(term, reader.errors)
|
||||
}
|
||||
@ -467,7 +475,7 @@ pub enum ReadbackError {
|
||||
InvalidAdt,
|
||||
InvalidAdtMatch,
|
||||
InvalidStrTerm(Term),
|
||||
UnexpectedTag(TagName, Tag),
|
||||
UnexpectedTag(Tag, Tag),
|
||||
}
|
||||
|
||||
impl ReadbackError {
|
||||
|
||||
@ -1,17 +1,26 @@
|
||||
use super::{
|
||||
net_to_term::{ReadbackError, Reader}, transform::encode_adts::adt_field_tag, Adt, DefName, Pattern, Tag, Term, LIST, LNIL, SNIL, STRING
|
||||
net_to_term::{ReadbackError, Reader},
|
||||
Adt, AdtEncoding, DefName, Pattern, Tag, Term, LCONS, LIST, LNIL, SNIL, STRING,
|
||||
};
|
||||
use std::borrow::BorrowMut;
|
||||
|
||||
impl<'a> Reader<'a> {
|
||||
pub fn resugar_adts(&mut self, term: &mut Term) {
|
||||
pub fn resugar_adts(&mut self, term: &mut Term, adt_encoding: AdtEncoding) {
|
||||
match adt_encoding {
|
||||
// No way of resugaring simple scott encoded terms.
|
||||
AdtEncoding::Scott => (),
|
||||
AdtEncoding::TaggedScott => self.resugar_tagged_scott(term),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn resugar_tagged_scott(&mut self, term: &mut Term) {
|
||||
match term {
|
||||
Term::Lam { tag: Tag::Named(adt_name), bod, .. } | Term::Chn { tag: Tag::Named(adt_name), bod, .. } => {
|
||||
let Some((adt_name, adt)) = self.book.adts.get_key_value(adt_name) else {
|
||||
return self.resugar_adts(bod);
|
||||
return self.resugar_tagged_scott(bod);
|
||||
};
|
||||
|
||||
self.resugar_adt_cons(term, adt, adt_name);
|
||||
self.resugar_ctr_tagged_scott(term, adt, adt_name);
|
||||
|
||||
match adt_name.0.as_str() {
|
||||
STRING => {
|
||||
@ -24,16 +33,16 @@ impl<'a> Reader<'a> {
|
||||
}
|
||||
}
|
||||
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => self.resugar_adts(bod),
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => self.resugar_tagged_scott(bod),
|
||||
|
||||
Term::App { tag: Tag::Named(adt_name), fun, arg } => {
|
||||
let Some((adt_name, adt)) = self.book.adts.get_key_value(adt_name) else {
|
||||
self.resugar_adts(fun);
|
||||
self.resugar_adts(arg);
|
||||
self.resugar_tagged_scott(fun);
|
||||
self.resugar_tagged_scott(arg);
|
||||
return;
|
||||
};
|
||||
|
||||
self.resugar_adt_match(term, adt_name, adt);
|
||||
self.resugar_match_tagged_scott(term, adt_name, adt);
|
||||
}
|
||||
|
||||
Term::App { fun: fst, arg: snd, .. }
|
||||
@ -42,14 +51,14 @@ impl<'a> Reader<'a> {
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Opx { fst, snd, .. } => {
|
||||
self.resugar_adts(fst);
|
||||
self.resugar_adts(snd);
|
||||
self.resugar_tagged_scott(fst);
|
||||
self.resugar_tagged_scott(snd);
|
||||
}
|
||||
|
||||
Term::Match { scrutinee, arms } => {
|
||||
self.resugar_adts(scrutinee);
|
||||
self.resugar_tagged_scott(scrutinee);
|
||||
for (_, arm) in arms {
|
||||
self.resugar_adts(arm);
|
||||
self.resugar_tagged_scott(arm);
|
||||
}
|
||||
}
|
||||
|
||||
@ -80,7 +89,7 @@ impl<'a> Reader<'a> {
|
||||
/// // Which gets resugared as:
|
||||
/// (Some (Some None))
|
||||
/// ```
|
||||
fn resugar_adt_cons(&mut self, term: &mut Term, adt: &Adt, adt_name: &DefName) {
|
||||
fn resugar_ctr_tagged_scott(&mut self, term: &mut Term, adt: &Adt, adt_name: &DefName) {
|
||||
let mut app = &mut *term;
|
||||
let mut current_arm = None;
|
||||
|
||||
@ -108,15 +117,15 @@ impl<'a> Reader<'a> {
|
||||
|
||||
for field in ctr_args.iter().rev() {
|
||||
self.deref(cur);
|
||||
let adt_field_tag = adt_field_tag(adt_name, ctr, field);
|
||||
let expected_tag = Tag::adt_field(adt_name, ctr, field);
|
||||
|
||||
match cur {
|
||||
Term::App { tag: Tag::Named(tag_name), .. } if tag_name == &adt_field_tag => {
|
||||
Term::App { tag, .. } if tag == &expected_tag => {
|
||||
let Term::App { tag, fun, .. } = cur.borrow_mut() else { unreachable!() };
|
||||
*tag = Tag::Static;
|
||||
cur = fun;
|
||||
}
|
||||
Term::App { tag, .. } => return self.error(ReadbackError::UnexpectedTag(adt_field_tag, tag.clone())),
|
||||
Term::App { tag, .. } => return self.error(ReadbackError::UnexpectedTag(expected_tag, tag.clone())),
|
||||
_ => return self.error(ReadbackError::InvalidAdt),
|
||||
}
|
||||
}
|
||||
@ -129,7 +138,7 @@ impl<'a> Reader<'a> {
|
||||
*cur = Term::r#ref(ctr);
|
||||
*term = std::mem::take(app);
|
||||
|
||||
self.resugar_adts(term);
|
||||
self.resugar_tagged_scott(term);
|
||||
}
|
||||
|
||||
/// Reconstructs adt-tagged applications as a match term
|
||||
@ -160,7 +169,7 @@ impl<'a> Reader<'a> {
|
||||
/// (None): λ* 3
|
||||
/// } b)
|
||||
/// ```
|
||||
fn resugar_adt_match(&mut self, term: &mut Term, adt_name: &DefName, adt: &Adt) {
|
||||
fn resugar_match_tagged_scott(&mut self, term: &mut Term, adt_name: &DefName, adt: &Adt) {
|
||||
let mut cur = &mut *term;
|
||||
let mut arms = Vec::new();
|
||||
|
||||
@ -174,10 +183,10 @@ impl<'a> Reader<'a> {
|
||||
for field in ctr_args {
|
||||
self.deref(arm);
|
||||
|
||||
let adt_field_tag = adt_field_tag(adt_name, ctr, field);
|
||||
let expected_tag = Tag::adt_field(adt_name, ctr, field);
|
||||
|
||||
match arm {
|
||||
Term::Lam { tag: Tag::Named(tag), .. } if tag == &adt_field_tag => {
|
||||
Term::Lam { tag, .. } if tag == &expected_tag => {
|
||||
let Term::Lam { nam, bod, .. } = arm.borrow_mut() else { unreachable!() };
|
||||
|
||||
args.push(nam.clone().map_or(Pattern::Var(None), |x| Pattern::Var(Some(x))));
|
||||
@ -185,13 +194,12 @@ impl<'a> Reader<'a> {
|
||||
}
|
||||
_ => {
|
||||
if let Term::Lam { tag, .. } = arm {
|
||||
self.error(ReadbackError::UnexpectedTag(adt_field_tag.clone(), tag.clone()));
|
||||
self.error(ReadbackError::UnexpectedTag(expected_tag.clone(), tag.clone()));
|
||||
}
|
||||
|
||||
let nam = self.namegen.unique();
|
||||
args.push(Pattern::Var(Some(nam.clone())));
|
||||
let tag = Tag::Named(adt_field_tag);
|
||||
*arm = Term::tagged_app(tag, std::mem::take(arm), Term::Var { nam });
|
||||
*arm = Term::tagged_app(expected_tag, std::mem::take(arm), Term::Var { nam });
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -207,7 +215,7 @@ impl<'a> Reader<'a> {
|
||||
let arms = arms.into_iter().rev().map(|(pat, term)| (pat, std::mem::take(term))).collect();
|
||||
*term = Term::Match { scrutinee, arms };
|
||||
|
||||
self.resugar_adts(term);
|
||||
self.resugar_tagged_scott(term);
|
||||
}
|
||||
|
||||
fn resugar_string(term: &mut Term) -> Term {
|
||||
@ -236,16 +244,19 @@ impl<'a> Reader<'a> {
|
||||
fn resugar_list(term: &mut Term) -> Term {
|
||||
match term {
|
||||
// (LCons el tail)
|
||||
Term::App { fun: box Term::App { fun: ctr, arg: el, .. }, arg: tail, .. } => {
|
||||
Term::App {
|
||||
fun: box Term::App { fun: box Term::Ref { def_name: ctr }, arg: el, .. },
|
||||
arg: tail,
|
||||
..
|
||||
} => {
|
||||
let tail = Self::resugar_list(tail);
|
||||
if let Term::List { els: tail } = tail {
|
||||
if ctr.as_str() == LCONS && let Term::List { els: tail } = tail {
|
||||
let mut els = vec![*el.clone()];
|
||||
els.extend(tail);
|
||||
Term::List { els }
|
||||
} else {
|
||||
// Make the constructor again
|
||||
let fun = Term::App { tag: Tag::Static, fun: ctr.clone(), arg: el.clone() };
|
||||
Term::App { tag: Tag::Static, fun: Box::new(fun), arg: Box::new(tail) }
|
||||
Term::call(Term::Ref { def_name: ctr.clone() }, [*el.clone(), tail])
|
||||
}
|
||||
}
|
||||
// (LNil)
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
use std::collections::{hash_map::Entry, HashMap};
|
||||
|
||||
use crate::{
|
||||
term::{Adt, Book, DefName, Origin, Tag, Term},
|
||||
term::{Adt, AdtEncoding, Book, DefName, Origin, Tag, Term, LCONS, LNIL, SCONS, SNIL},
|
||||
Warning,
|
||||
};
|
||||
use indexmap::IndexSet;
|
||||
@ -27,13 +27,19 @@ type Definitions = HashMap<DefName, Used>;
|
||||
impl Book {
|
||||
/// 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, main: Option<&DefName>, prune_all: bool, warnings: &mut Vec<Warning>) {
|
||||
pub fn prune(
|
||||
&mut self,
|
||||
main: Option<&DefName>,
|
||||
prune_all: bool,
|
||||
adt_encoding: AdtEncoding,
|
||||
warnings: &mut Vec<Warning>,
|
||||
) {
|
||||
let mut used = Definitions::new();
|
||||
|
||||
if let Some(main) = main {
|
||||
let def = self.defs.get(main).unwrap();
|
||||
used.insert(main.clone(), Used::Main);
|
||||
self.find_used_definitions(&def.rule().body, Used::Main, &mut used);
|
||||
self.find_used_definitions(&def.rule().body, Used::Main, &mut used, adt_encoding);
|
||||
}
|
||||
|
||||
// Even if we don't prune all the defs, we need check what built-ins are accessible through user code
|
||||
@ -49,18 +55,17 @@ impl Book {
|
||||
_ => {}
|
||||
}
|
||||
|
||||
self.find_used_definitions(&rule.body, Used::Unused, &mut used);
|
||||
self.find_used_definitions(&rule.body, Used::Unused, &mut used, adt_encoding);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
let names = self.defs.keys().cloned().collect::<IndexSet<DefName>>();
|
||||
|
||||
// Filter defs from the 'used' hashmap that are not accessible from main
|
||||
let filter = |(name, used)| if used == Used::Unused { None } else { Some(name) };
|
||||
let used: IndexSet<DefName> = used.into_iter().filter_map(filter).collect();
|
||||
|
||||
let names = self.defs.keys().cloned().collect::<IndexSet<DefName>>();
|
||||
let unused = names.difference(&used).cloned();
|
||||
|
||||
self.prune_unused(unused, prune_all, warnings);
|
||||
@ -83,69 +88,88 @@ impl Book {
|
||||
}
|
||||
|
||||
/// Finds all used definitions on every term that can have a def_id.
|
||||
fn find_used_definitions(&self, term: &Term, used: Used, uses: &mut Definitions) {
|
||||
fn find_used_definitions(
|
||||
&self,
|
||||
term: &Term,
|
||||
used: Used,
|
||||
uses: &mut Definitions,
|
||||
adt_encoding: AdtEncoding,
|
||||
) {
|
||||
self.find_manual_adt_encoding(term, uses, adt_encoding);
|
||||
|
||||
match term {
|
||||
Term::Ref { def_name } => match self.ctrs.get(def_name) {
|
||||
Some(name) => self.insert_ctrs_used(name, uses),
|
||||
None => self.insert_used(def_name, used, uses),
|
||||
Some(name) => self.insert_ctrs_used(name, uses, adt_encoding),
|
||||
None => self.insert_used(def_name, used, uses, adt_encoding),
|
||||
},
|
||||
|
||||
Term::Lam { tag: Tag::Named(name), bod, .. } | Term::Chn { tag: Tag::Named(name), bod, .. } => {
|
||||
// mark constructors of the Adt with same name as the tag in case of the user
|
||||
// manually encoded a constructor with tagged lambdas
|
||||
self.insert_ctrs_used(name, uses);
|
||||
self.find_used_definitions(bod, used, uses);
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
|
||||
self.find_used_definitions(bod, used, uses, adt_encoding)
|
||||
}
|
||||
Term::Lam { bod, .. } | Term::Chn { bod, .. } => self.find_used_definitions(bod, used, uses),
|
||||
Term::Let { val, nxt, .. } | Term::Dup { val, nxt, .. } => {
|
||||
self.find_used_definitions(val, used, uses);
|
||||
self.find_used_definitions(nxt, used, uses);
|
||||
}
|
||||
Term::App { tag, fun, arg } => {
|
||||
// mark constructors of the Adt with same name as the tag in case of the user
|
||||
// manually encoded a pattern matching with tagged applications
|
||||
if let Tag::Named(name) = tag {
|
||||
self.insert_ctrs_used(name, uses);
|
||||
}
|
||||
|
||||
self.find_used_definitions(fun, used, uses);
|
||||
self.find_used_definitions(arg, used, uses);
|
||||
}
|
||||
Term::Sup { fst, snd, .. } | Term::Tup { fst, snd } | Term::Opx { fst, snd, .. } => {
|
||||
self.find_used_definitions(fst, used, uses);
|
||||
self.find_used_definitions(snd, used, uses);
|
||||
Term::Let { val: fst, nxt: snd, .. }
|
||||
| Term::Dup { val: fst, nxt: snd, .. }
|
||||
| Term::App { fun: fst, arg: snd, .. }
|
||||
| Term::Sup { fst, snd, .. }
|
||||
| Term::Tup { fst, snd }
|
||||
| Term::Opx { fst, snd, .. } => {
|
||||
self.find_used_definitions(fst, used, uses, adt_encoding);
|
||||
self.find_used_definitions(snd, used, uses, adt_encoding);
|
||||
}
|
||||
Term::Match { scrutinee, arms } => {
|
||||
self.find_used_definitions(scrutinee, used, uses);
|
||||
self.find_used_definitions(scrutinee, used, uses, adt_encoding);
|
||||
for (_, term) in arms {
|
||||
self.find_used_definitions(term, used, uses);
|
||||
self.find_used_definitions(term, used, uses, adt_encoding);
|
||||
}
|
||||
}
|
||||
Term::Var { .. }
|
||||
| Term::Lnk { .. }
|
||||
| Term::Num { .. }
|
||||
| Term::Str { .. }
|
||||
| Term::List { .. }
|
||||
| Term::Era
|
||||
| Term::Invalid => (),
|
||||
Term::List { els } => {
|
||||
self.insert_ctrs_used(&DefName::new(LCONS), uses, adt_encoding);
|
||||
self.insert_ctrs_used(&DefName::new(LNIL), uses, adt_encoding);
|
||||
for term in els {
|
||||
self.find_used_definitions(term, used, uses, adt_encoding);
|
||||
}
|
||||
}
|
||||
Term::Str { .. } => {
|
||||
self.insert_ctrs_used(&DefName::new(SCONS), uses, adt_encoding);
|
||||
self.insert_ctrs_used(&DefName::new(SNIL), uses, adt_encoding);
|
||||
}
|
||||
Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Era | Term::Invalid => (),
|
||||
}
|
||||
}
|
||||
|
||||
fn insert_used(&self, def_name: &DefName, used: Used, uses: &mut Definitions) {
|
||||
let Entry::Vacant(e) = uses.entry(def_name.clone()) else { return };
|
||||
e.insert(used);
|
||||
|
||||
// This needs to be done for each rule in case the pass it's ran from has not encoded the pattern match
|
||||
// E.g.: the `flatten_rules` golden test
|
||||
for rule in &self.defs[def_name].rules {
|
||||
self.find_used_definitions(&rule.body, used, uses);
|
||||
/// If the current term is a manual encoding of a constructor or adt, we marked it as used.
|
||||
fn find_manual_adt_encoding(&self, term: &Term, uses: &mut Definitions, adt_encoding: AdtEncoding) {
|
||||
match adt_encoding {
|
||||
AdtEncoding::Scott => (),
|
||||
// If using the tagged scott encoding of ADTs, we also mark a constructor
|
||||
// as used if the user manually encoded a ctr or match (or any other use of the ctr tags).
|
||||
AdtEncoding::TaggedScott => match term {
|
||||
Term::Lam { tag: Tag::Named(name), .. }
|
||||
| Term::Chn { tag: Tag::Named(name), .. }
|
||||
| Term::App { tag: Tag::Named(name), .. } => {
|
||||
// We don't check dup/sup tags because they use a separate label scope.
|
||||
self.insert_ctrs_used(name, uses, adt_encoding);
|
||||
}
|
||||
_ => (),
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
fn insert_ctrs_used(&self, name: &DefName, uses: &mut Definitions) {
|
||||
fn insert_used(&self, def_name: &DefName, used: Used, uses: &mut Definitions, adt_encoding: AdtEncoding) {
|
||||
if let Entry::Vacant(e) = uses.entry(def_name.clone()) {
|
||||
e.insert(used);
|
||||
|
||||
// This needs to be done for each rule in case the pass it's ran from has not encoded the pattern match
|
||||
// E.g.: the `flatten_rules` golden test
|
||||
for rule in &self.defs[def_name].rules {
|
||||
self.find_used_definitions(&rule.body, used, uses, adt_encoding);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn insert_ctrs_used(&self, name: &DefName, uses: &mut Definitions, adt_encoding: AdtEncoding) {
|
||||
if let Some(Adt { ctrs, .. }) = self.adts.get(name) {
|
||||
for (ctr, _) in ctrs {
|
||||
self.insert_used(ctr, Used::Adt, uses);
|
||||
self.insert_used(ctr, Used::Adt, uses, adt_encoding);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -1,15 +1,15 @@
|
||||
use crate::term::{Book, DefName, Definition, Rule, Tag, TagName, Term, VarName};
|
||||
use crate::term::{AdtEncoding, Book, DefName, Definition, Rule, Tag, Term, VarName};
|
||||
|
||||
impl Book {
|
||||
pub fn generate_scott_adts(&mut self) {
|
||||
pub fn encode_adts(&mut self, adt_encoding: AdtEncoding) {
|
||||
let mut defs = vec![];
|
||||
for (adt_name, adt) in &self.adts {
|
||||
for (ctr_name, args) in &adt.ctrs {
|
||||
let ctrs: Vec<_> = adt.ctrs.keys().cloned().collect();
|
||||
|
||||
let lam = make_lam(adt_name, args.clone(), ctrs, ctr_name);
|
||||
let body = encode_ctr(adt_name, args.clone(), ctrs, ctr_name, adt_encoding);
|
||||
|
||||
let rules = vec![Rule { pats: vec![], body: lam, origin: adt.origin }];
|
||||
let rules = vec![Rule { pats: vec![], body, origin: adt.origin }];
|
||||
let def = Definition { name: ctr_name.clone(), rules };
|
||||
defs.push((ctr_name.clone(), def));
|
||||
}
|
||||
@ -18,22 +18,33 @@ impl Book {
|
||||
}
|
||||
}
|
||||
|
||||
fn make_lam(adt_name: &DefName, ctr_args: Vec<VarName>, ctrs: Vec<DefName>, ctr_name: &DefName) -> Term {
|
||||
let ctr = Term::Var { nam: ctr_name.clone() };
|
||||
|
||||
let app = ctr_args.iter().cloned().fold(ctr, |acc, nam| {
|
||||
let tag = Tag::Named(adt_field_tag(adt_name, ctr_name, &nam));
|
||||
Term::tagged_app(tag, acc, Term::Var { nam })
|
||||
});
|
||||
|
||||
let lam = ctrs
|
||||
.into_iter()
|
||||
.rev()
|
||||
.fold(app, |acc, arg| Term::tagged_lam(Tag::Named(adt_name.clone()), arg.clone(), acc));
|
||||
|
||||
ctr_args.into_iter().rev().fold(lam, |acc, arg| Term::named_lam(arg, acc))
|
||||
}
|
||||
|
||||
pub fn adt_field_tag(adt_name: &DefName, ctr_name: &DefName, field_name: &VarName) -> TagName {
|
||||
format!("{}.{}.{}", adt_name, ctr_name, field_name).into()
|
||||
fn encode_ctr(
|
||||
adt_name: &DefName,
|
||||
ctr_args: Vec<VarName>,
|
||||
ctrs: Vec<DefName>,
|
||||
ctr_name: &DefName,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Term {
|
||||
match adt_encoding {
|
||||
// λarg1 λarg2 λarg3 λctr1 λctr2 (ctr2 arg1 arg2 arg3)
|
||||
AdtEncoding::Scott => {
|
||||
let ctr = Term::Var { nam: ctr_name.clone() };
|
||||
let app = ctr_args.iter().cloned().fold(ctr, Term::arg_call);
|
||||
let lam = ctrs.into_iter().rev().fold(app, |acc, arg| Term::named_lam(arg.clone(), acc));
|
||||
ctr_args.into_iter().rev().fold(lam, |acc, arg| Term::named_lam(arg, acc))
|
||||
}
|
||||
// λarg1 λarg2 #type λctr1 #type λctr2 #type.ctr2.arg2(#type.ctr2.arg1(ctr2 arg1) arg2)
|
||||
AdtEncoding::TaggedScott => {
|
||||
let ctr = Term::Var { nam: ctr_name.clone() };
|
||||
let app = ctr_args.iter().cloned().fold(ctr, |acc, nam| {
|
||||
let tag = Tag::adt_field(adt_name, ctr_name, &nam);
|
||||
Term::tagged_app(tag, acc, Term::Var { nam })
|
||||
});
|
||||
let lam = ctrs
|
||||
.into_iter()
|
||||
.rev()
|
||||
.fold(app, |acc, arg| Term::tagged_lam(Tag::adt_name(adt_name), arg.clone(), acc));
|
||||
ctr_args.into_iter().rev().fold(lam, |acc, arg| Term::named_lam(arg, acc))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -1,17 +1,21 @@
|
||||
use crate::term::{
|
||||
check::type_check::DefinitionTypes, transform::unique_names::UniqueNameGenerator, Book, DefName,
|
||||
Definition, MatchNum, Pattern, Rule, Tag, Term, Type, VarName,
|
||||
check::type_check::DefinitionTypes, transform::unique_names::UniqueNameGenerator, AdtEncoding, Book,
|
||||
DefName, Definition, MatchNum, Pattern, Rule, Tag, Term, Type, VarName,
|
||||
};
|
||||
|
||||
impl Book {
|
||||
pub fn encode_pattern_matching_functions(&mut self, def_types: &DefinitionTypes) {
|
||||
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);
|
||||
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.
|
||||
@ -31,7 +35,12 @@ fn make_non_pattern_matching_def(def: &mut Definition) {
|
||||
/// 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: &DefName, def_type: &[Type]) {
|
||||
fn make_pattern_matching_def(
|
||||
book: &mut Book,
|
||||
def_name: &DefName,
|
||||
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() {
|
||||
@ -42,7 +51,7 @@ fn make_pattern_matching_def(book: &mut Book, def_name: &DefName, def_type: &[Ty
|
||||
// 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![]);
|
||||
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();
|
||||
@ -73,6 +82,7 @@ fn make_pattern_matching_case(
|
||||
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];
|
||||
@ -100,9 +110,9 @@ fn make_pattern_matching_case(
|
||||
|
||||
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, old_args, new_args)
|
||||
make_leaf_case(book, fst_rule, fst_rule_idx, match_path, old_args, new_args, adt_encoding)
|
||||
} else {
|
||||
make_match_case(book, def, def_type, crnt_rules, match_path, old_args, new_args)
|
||||
make_match_case(book, def, def_type, crnt_rules, match_path, old_args, new_args, adt_encoding)
|
||||
}
|
||||
}
|
||||
|
||||
@ -116,6 +126,7 @@ fn make_match_case(
|
||||
match_path: Vec<Pattern>,
|
||||
old_args: Vec<VarName>,
|
||||
new_args: Vec<VarName>,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Term {
|
||||
let next_arg_idx = match_path.len();
|
||||
let next_type = &def_type[next_arg_idx];
|
||||
@ -135,45 +146,61 @@ fn make_match_case(
|
||||
.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);
|
||||
let next_case = make_pattern_matching_case(book, def, def_type, next_rules, match_path, adt_encoding);
|
||||
next_cases.push(next_case);
|
||||
}
|
||||
|
||||
// Encode the current pattern matching, calling the subfunctions
|
||||
let match_var = VarName::new("x");
|
||||
// The match term itself
|
||||
let term = match next_type {
|
||||
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: &VarName,
|
||||
mut arms: impl Iterator<Item = Term>,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Term {
|
||||
match match_type {
|
||||
Type::None => unreachable!(),
|
||||
Type::Any => Term::arg_call(std::mem::take(&mut next_cases[0]), match_var.clone()),
|
||||
// (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(VarName::new("%fst")))),
|
||||
Box::new(Pattern::Var(Some(VarName::new("%snd")))),
|
||||
),
|
||||
val: Box::new(Term::Var { nam: match_var.clone() }),
|
||||
nxt: Box::new(Term::call(std::mem::take(&mut next_cases[0]), [
|
||||
Term::Var { nam: VarName::new("%fst") },
|
||||
Term::Var { nam: VarName::new("%snd") },
|
||||
])),
|
||||
nxt: Box::new(Term::call(arms.next().unwrap(), [Term::Var { nam: VarName::new("%fst") }, Term::Var {
|
||||
nam: VarName::new("%snd"),
|
||||
}])),
|
||||
},
|
||||
// match x {0: arm[0]; +: arm[1]}
|
||||
Type::Num => Term::Match {
|
||||
scrutinee: Box::new(Term::Var { nam: match_var.clone() }),
|
||||
arms: vec![
|
||||
(Pattern::Num(MatchNum::Zero), std::mem::take(&mut next_cases[0])),
|
||||
(Pattern::Num(MatchNum::Succ(None)), std::mem::take(&mut next_cases[1])),
|
||||
(Pattern::Num(MatchNum::Zero), arms.next().unwrap()),
|
||||
(Pattern::Num(MatchNum::Succ(None)), arms.next().unwrap()),
|
||||
],
|
||||
},
|
||||
Type::Adt(adt_name) => {
|
||||
Term::tagged_call(Tag::Named(adt_name.clone()), Term::Var { nam: match_var.clone() }, next_cases)
|
||||
}
|
||||
};
|
||||
// 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);
|
||||
term
|
||||
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.
|
||||
@ -184,6 +211,7 @@ fn make_leaf_case(
|
||||
match_path: Vec<Pattern>,
|
||||
old_args: Vec<VarName>,
|
||||
new_args: Vec<VarName>,
|
||||
adt_encoding: AdtEncoding,
|
||||
) -> Term {
|
||||
let args = &mut old_args.iter().chain(new_args.iter()).cloned();
|
||||
|
||||
@ -207,7 +235,7 @@ fn make_leaf_case(
|
||||
}
|
||||
});
|
||||
// Add the lambdas for the matched args.
|
||||
let term = add_arg_lams(term, old_args, new_args, match_path.last(), book);
|
||||
let term = add_arg_lams(term, old_args, new_args, match_path.last(), book, adt_encoding);
|
||||
|
||||
term
|
||||
}
|
||||
@ -226,6 +254,7 @@ fn add_arg_lams(
|
||||
new_args: Vec<VarName>,
|
||||
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));
|
||||
@ -237,8 +266,12 @@ fn add_arg_lams(
|
||||
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!() };
|
||||
let tag = Tag::Named(format!("{adt}.{ctr}.{field}").into());
|
||||
Term::Lam { tag, nam: Some(new_arg), bod: Box::new(term) }
|
||||
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
|
||||
|
||||
@ -5,7 +5,7 @@ use hvml::{
|
||||
run_book,
|
||||
term::{
|
||||
load_book::do_parse_book, net_to_term::net_to_term, parser::parse_term, term_to_compat_net,
|
||||
term_to_net::Labels, Book, Name, Term,
|
||||
term_to_net::Labels, AdtEncoding, Book, Name, Term,
|
||||
},
|
||||
CompileOpts, RunOpts, WarningOpts,
|
||||
};
|
||||
@ -13,6 +13,7 @@ use insta::assert_snapshot;
|
||||
use itertools::Itertools;
|
||||
use std::{
|
||||
collections::HashMap,
|
||||
fmt::Write,
|
||||
fs,
|
||||
path::{Path, PathBuf},
|
||||
sync::{Arc, RwLock},
|
||||
@ -141,7 +142,8 @@ fn readback_lnet() {
|
||||
let net = do_parse_net(code)?;
|
||||
let book = Book::default();
|
||||
let compat_net = hvmc_to_net(&net, &Default::default());
|
||||
let (term, errors) = net_to_term(&compat_net, &book, &Labels::default(), false);
|
||||
let (term, errors) =
|
||||
net_to_term(&compat_net, &book, &Labels::default(), false, hvml::term::AdtEncoding::TaggedScott);
|
||||
Ok(format!("{}{}", errors.display(), term.display()))
|
||||
})
|
||||
}
|
||||
@ -154,13 +156,13 @@ fn flatten_rules() {
|
||||
book.check_shared_names()?;
|
||||
book.encode_builtins();
|
||||
book.resolve_ctrs_in_pats();
|
||||
book.generate_scott_adts();
|
||||
book.encode_adts(AdtEncoding::TaggedScott);
|
||||
book.desugar_let_destructors();
|
||||
book.desugar_implicit_match_binds();
|
||||
book.check_unbound_pats()?;
|
||||
book.extract_adt_matches(&mut Vec::new())?;
|
||||
book.flatten_rules();
|
||||
book.prune(main.as_ref(), false, &mut Vec::new());
|
||||
book.prune(main.as_ref(), false, AdtEncoding::TaggedScott, &mut Vec::new());
|
||||
Ok(book.to_string())
|
||||
})
|
||||
}
|
||||
@ -176,15 +178,21 @@ fn parse_file() {
|
||||
#[test]
|
||||
fn encode_pattern_match() {
|
||||
run_golden_test_dir(function_name!(), &|code, path| {
|
||||
let mut book = do_parse_book(code, path)?;
|
||||
let main = book.check_has_entrypoint(None).ok();
|
||||
book.check_shared_names()?;
|
||||
book.generate_scott_adts();
|
||||
book.encode_builtins();
|
||||
encode_pattern_matching(&mut book, &mut Vec::new())?;
|
||||
book.prune(main.as_ref(), false, &mut Vec::new());
|
||||
book.merge_definitions(&main.unwrap_or_default());
|
||||
Ok(book.to_string())
|
||||
let mut result = String::new();
|
||||
for adt_encoding in [AdtEncoding::TaggedScott, AdtEncoding::Scott] {
|
||||
let mut book = do_parse_book(code, path)?;
|
||||
let main = book.check_has_entrypoint(None).ok();
|
||||
book.check_shared_names()?;
|
||||
book.encode_adts(adt_encoding);
|
||||
book.encode_builtins();
|
||||
encode_pattern_matching(&mut book, &mut Vec::new(), adt_encoding)?;
|
||||
book.prune(main.as_ref(), false, adt_encoding, &mut Vec::new());
|
||||
book.merge_definitions(&main.clone().unwrap_or_default());
|
||||
|
||||
writeln!(result, "{adt_encoding:?}:").unwrap();
|
||||
writeln!(result, "{book}\n").unwrap();
|
||||
}
|
||||
Ok(result)
|
||||
})
|
||||
}
|
||||
|
||||
@ -198,7 +206,7 @@ fn desugar_file() {
|
||||
}
|
||||
|
||||
#[test]
|
||||
#[ignore = "To not delay golden tests execution"]
|
||||
#[ignore = "to not delay golden tests execution"]
|
||||
fn hangs() {
|
||||
let expected_normalization_time = 1;
|
||||
|
||||
|
||||
@ -2,3 +2,6 @@ main = *
|
||||
|
||||
Foo SNil = 0
|
||||
Foo * = 1
|
||||
|
||||
Bar (LCons h t) = 0
|
||||
Bar * = 1
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/adt_tup_era.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(Main) = (Foo (Pair 1 5))
|
||||
|
||||
(Foo) = λa #Tuple (a #Tuple.Pair.a λb #Tuple.Pair.b λc (Foo$F0 b c))
|
||||
@ -9,3 +10,14 @@ input_file: tests/golden_tests/encode_pattern_match/adt_tup_era.hvm
|
||||
(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)
|
||||
|
||||
Scott:
|
||||
(Main) = (Foo (Pair 1 5))
|
||||
|
||||
(Foo) = λa (a λb λc (Foo$F0 b c))
|
||||
|
||||
(Foo$F0) = λa (a λb λc λd b)
|
||||
|
||||
(Pair) = λa λb λPair (Pair a b)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/and3.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (And (F, (T, F)))
|
||||
|
||||
(And) = λa let (b, c) = a; (And$F0 b c)
|
||||
@ -13,3 +14,18 @@ input_file: tests/golden_tests/encode_pattern_match/and3.hvm
|
||||
(F) = #Bool λT #Bool λF F
|
||||
|
||||
(T) = #Bool λT #Bool λF T
|
||||
|
||||
Scott:
|
||||
(main) = (And (F, (T, F)))
|
||||
|
||||
(And) = λa let (b, c) = a; (And$F0 b c)
|
||||
|
||||
(And$F0) = λa (a λb let (c, d) = b; (And$F0$F0 c d) λ* F)
|
||||
|
||||
(And$F0$F0) = λa (a λb (b T F) λ* F)
|
||||
|
||||
(F) = λT λF F
|
||||
|
||||
(T) = λT λF T
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
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))
|
||||
@ -13,3 +14,18 @@ input_file: tests/golden_tests/encode_pattern_match/bool.hvm
|
||||
(false) = #bool λtrue #bool λfalse false
|
||||
|
||||
(true) = #bool λtrue #bool λfalse true
|
||||
|
||||
Scott:
|
||||
(not) = λa (a false true)
|
||||
|
||||
(and) = λa (a λb (b true false) λc (c false false))
|
||||
|
||||
(and2) = λa (a λb b λc false)
|
||||
|
||||
(and3_$_and4) = λa (a λb (b true false) λc false)
|
||||
|
||||
(false) = λtrue λfalse false
|
||||
|
||||
(true) = λtrue λfalse true
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/bool_tup.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (foo (F, T))
|
||||
|
||||
(foo) = λa let (b, c) = a; (foo$F0 b c)
|
||||
@ -11,3 +12,16 @@ input_file: tests/golden_tests/encode_pattern_match/bool_tup.hvm
|
||||
(F) = #Bool λT #Bool λF F
|
||||
|
||||
(T) = #Bool λT #Bool λF T
|
||||
|
||||
Scott:
|
||||
(main) = (foo (F, T))
|
||||
|
||||
(foo) = λa let (b, c) = a; (foo$F0 b c)
|
||||
|
||||
(foo$F0) = λa (a λb b λ* F)
|
||||
|
||||
(F) = λT λF F
|
||||
|
||||
(T) = λT λF T
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,14 @@
|
||||
source: tests/golden_tests.rs
|
||||
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)
|
||||
|
||||
Scott:
|
||||
(unbox) = λa (a λb b)
|
||||
|
||||
(new) = λval λnew (new val)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
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
|
||||
|
||||
(East) = #Direction λNorth #Direction λSouth #Direction λEast #Direction λWest East
|
||||
@ -35,3 +36,40 @@ input_file: tests/golden_tests/encode_pattern_match/common.hvm
|
||||
(Yellow) = #Light λRed #Light λYellow #Light λGreen Yellow
|
||||
|
||||
(Green) = #Light λRed #Light λYellow #Light λGreen Green
|
||||
|
||||
Scott:
|
||||
(West) = λNorth λSouth λEast λWest West
|
||||
|
||||
(East) = λNorth λSouth λEast λWest East
|
||||
|
||||
(South) = λNorth λSouth λEast λWest South
|
||||
|
||||
(North) = λNorth λSouth λEast λWest North
|
||||
|
||||
(Filled) = λvalue λFilled λEmpty (Filled value)
|
||||
|
||||
(Empty) = λFilled λEmpty Empty
|
||||
|
||||
(Some) = λx λSome λNone (Some x)
|
||||
|
||||
(None) = λSome λNone None
|
||||
|
||||
(Ok) = λa λOk λErr (Ok a)
|
||||
|
||||
(Err) = λb λOk λErr (Err b)
|
||||
|
||||
(Cons) = λx λxs λCons λNil (Cons x xs)
|
||||
|
||||
(Nil) = λCons λNil Nil
|
||||
|
||||
(True) = λTrue λFalse True
|
||||
|
||||
(False) = λTrue λFalse False
|
||||
|
||||
(Red) = λRed λYellow λGreen Red
|
||||
|
||||
(Yellow) = λRed λYellow λGreen Yellow
|
||||
|
||||
(Green) = λRed λYellow λGreen Green
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/concat.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (String.concat (SCons 97 (SCons 98 SNil)) (SCons 99 (SCons 100 SNil)))
|
||||
|
||||
(String.concat) = λa λb (String.concat$match$1 a b)
|
||||
@ -11,3 +12,16 @@ input_file: tests/golden_tests/encode_pattern_match/concat.hvm
|
||||
(SNil) = #String λSCons #String λSNil SNil
|
||||
|
||||
(String.concat$match$1) = λa #String (a #String.SCons.head λb #String.SCons.tail λc λd (SCons b (String.concat c d)) λe e)
|
||||
|
||||
Scott:
|
||||
(main) = (String.concat (SCons 97 (SCons 98 SNil)) (SCons 99 (SCons 100 SNil)))
|
||||
|
||||
(String.concat) = λa λb (String.concat$match$1 a b)
|
||||
|
||||
(SCons) = λhead λtail λSCons λSNil (SCons head tail)
|
||||
|
||||
(SNil) = λSCons λSNil SNil
|
||||
|
||||
(String.concat$match$1) = λa (a λb λc λd (SCons b (String.concat c d)) λe e)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/concat_def.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (concat (SCons 97 (SCons 98 SNil)) (SCons 99 (SCons 100 SNil)))
|
||||
|
||||
(concat) = λa #String (a #String.SCons.head λb #String.SCons.tail λc λd (SCons b (concat c d)) λe e)
|
||||
@ -9,3 +10,14 @@ input_file: tests/golden_tests/encode_pattern_match/concat_def.hvm
|
||||
(SCons) = λhead λtail #String λSCons #String λSNil #String.SCons.tail (#String.SCons.head (SCons head) tail)
|
||||
|
||||
(SNil) = #String λSCons #String λSNil SNil
|
||||
|
||||
Scott:
|
||||
(main) = (concat (SCons 97 (SCons 98 SNil)) (SCons 99 (SCons 100 SNil)))
|
||||
|
||||
(concat) = λa (a λb λc λd (SCons b (concat c d)) λe e)
|
||||
|
||||
(SCons) = λhead λtail λSCons λSNil (SCons head tail)
|
||||
|
||||
(SNil) = λSCons λSNil SNil
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/def_tups.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (go (1, (2, (3, (4, 5)))))
|
||||
|
||||
(go) = λa let (b, c) = a; (go$F0 b c)
|
||||
@ -11,3 +12,16 @@ input_file: tests/golden_tests/encode_pattern_match/def_tups.hvm
|
||||
(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:
|
||||
(main) = (go (1, (2, (3, (4, 5)))))
|
||||
|
||||
(go) = λa let (b, c) = a; (go$F0 b c)
|
||||
|
||||
(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)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/definition_merge.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(False) = #Bool λTrue #Bool λFalse False
|
||||
|
||||
(Foo$F3_$_Foo$F2) = λa #Bool (a λb #Bool (b 3 3) λc #Bool (c 3 3))
|
||||
@ -17,3 +18,22 @@ input_file: tests/golden_tests/encode_pattern_match/definition_merge.hvm
|
||||
(True) = #Bool λTrue #Bool λFalse True
|
||||
|
||||
(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))
|
||||
|
||||
Scott:
|
||||
(False) = λTrue λFalse False
|
||||
|
||||
(Foo$F3_$_Foo$F2) = λa (a λb (b 3 3) λc (c 3 3))
|
||||
|
||||
(Foo$F1) = λa (a λb (b 2 2) λc (c 2 2))
|
||||
|
||||
(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
|
||||
|
||||
(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))
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
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
|
||||
|
||||
(Mul) = #Op λAdd #Op λSub #Op λMul #Op λDiv Mul
|
||||
@ -27,3 +28,32 @@ input_file: tests/golden_tests/encode_pattern_match/expr.hvm
|
||||
(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)
|
||||
|
||||
(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)
|
||||
|
||||
Scott:
|
||||
(Div) = λAdd λSub λMul λDiv Div
|
||||
|
||||
(Mul) = λAdd λSub λMul λDiv Mul
|
||||
|
||||
(Sub) = λAdd λSub λMul λDiv Sub
|
||||
|
||||
(Add) = λAdd λSub λMul λDiv Add
|
||||
|
||||
(Var) = λname λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Var name)
|
||||
|
||||
(Num) = λval λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Num val)
|
||||
|
||||
(App) = λfun λarg λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (App fun arg)
|
||||
|
||||
(Fun) = λname λbody λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Fun name body)
|
||||
|
||||
(If) = λcond λthen λelse λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (If cond then else)
|
||||
|
||||
(Let) = λbind λval λnext λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Let bind val next)
|
||||
|
||||
(Dup) = λfst λsnd λval λnext λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Dup fst snd val next)
|
||||
|
||||
(Tup) = λfst λsnd λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Tup fst snd)
|
||||
|
||||
(Op2) = λop λfst λsnd λVar λNum λApp λFun λIf λLet λDup λTup λOp2 (Op2 op fst snd)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
|
||||
|
||||
(Fn1) = λa let (b, c) = a; λd (Fn1$F0 b c d)
|
||||
@ -17,3 +18,22 @@ input_file: tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm
|
||||
(Fn2$F0$F0) = λa λb λc let (d, e) = c; d
|
||||
|
||||
(Fn1$F0) = λa λb let (c, d) = b; λ* c
|
||||
|
||||
Scott:
|
||||
(main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
|
||||
|
||||
(Fn1) = λa let (b, c) = a; λd (Fn1$F0 b c d)
|
||||
|
||||
(Fn2) = λa let (b, c) = a; (Fn2$F0 b c)
|
||||
|
||||
(Fn3) = λa let (b, c) = a; λd (Fn3$F0 b c d)
|
||||
|
||||
(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
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/is_some_some.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (some_some (Some 1))
|
||||
|
||||
(some_some) = λa #Option (a #Option.Some.x λb (some_some$F0 b) 0)
|
||||
@ -11,3 +12,16 @@ input_file: tests/golden_tests/encode_pattern_match/is_some_some.hvm
|
||||
(None) = #Option λSome #Option λNone None
|
||||
|
||||
(Some) = λx #Option λSome #Option λNone #Option.Some.x (Some x)
|
||||
|
||||
Scott:
|
||||
(main) = (some_some (Some 1))
|
||||
|
||||
(some_some) = λa (a λb (some_some$F0 b) 0)
|
||||
|
||||
(some_some$F0) = λa (a λb 1 0)
|
||||
|
||||
(None) = λSome λNone None
|
||||
|
||||
(Some) = λx λSome λNone (Some x)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
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)
|
||||
|
||||
(Pure) = λx (Cons x Nil)
|
||||
@ -27,3 +28,32 @@ input_file: tests/golden_tests/encode_pattern_match/list_merge_sort.hvm
|
||||
(True) = #Bool λTrue #Bool λFalse True
|
||||
|
||||
(False) = #Bool λTrue #Bool λFalse False
|
||||
|
||||
Scott:
|
||||
(If) = λa (a λb λc b λd λe e)
|
||||
|
||||
(Pure) = λx (Cons x Nil)
|
||||
|
||||
(Map) = λa (a λb λc λd (Cons (d b) (Map c d)) λe Nil)
|
||||
|
||||
(MergeSort) = λcmp λxs (Unpack cmp (Map xs Pure))
|
||||
|
||||
(Unpack) = λa λb (b λc λd λe (Unpack$F0 e c d) λf Nil a)
|
||||
|
||||
(MergePair) = λa λb (b λc λd λe (MergePair$F0 e c d) λf 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)
|
||||
|
||||
(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)
|
||||
|
||||
(Unpack$F0) = λa λb λc (c λd λe λf λg (Unpack f (MergePair f (Cons g (Cons d e)))) λh λi i a b)
|
||||
|
||||
(Nil) = λCons λNil Nil
|
||||
|
||||
(Cons) = λhead λtail λCons λNil (Cons head tail)
|
||||
|
||||
(True) = λTrue λFalse True
|
||||
|
||||
(False) = λTrue λFalse False
|
||||
|
||||
|
||||
|
||||
@ -0,0 +1,27 @@
|
||||
---
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared_fn.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = *
|
||||
|
||||
(Foo) = λa #String (a #String.SCons.head λb #String.SCons.tail λc 1 0)
|
||||
|
||||
(Bar) = λa #List (a #List.LCons.head λb #List.LCons.tail λc 0 1)
|
||||
|
||||
(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
|
||||
|
||||
Scott:
|
||||
(main) = *
|
||||
|
||||
(Foo) = λa (a λb λc 1 0)
|
||||
|
||||
(Bar) = λa (a λb λc 0 1)
|
||||
|
||||
|
||||
@ -0,0 +1,25 @@
|
||||
---
|
||||
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)
|
||||
|
||||
(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)
|
||||
|
||||
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)
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
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$match$1) = λa #bool (a λ$x $x λb b)
|
||||
@ -9,3 +10,14 @@ input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_in_arm.hv
|
||||
(F) = #bool λT #bool λF F
|
||||
|
||||
(T) = #bool λT #bool λF T
|
||||
|
||||
Scott:
|
||||
(main) = λx (main$match$1 x)
|
||||
|
||||
(main$match$1) = λa (a λ$x $x λb b)
|
||||
|
||||
(F) = λT λF F
|
||||
|
||||
(T) = λT λF T
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = *
|
||||
|
||||
(None) = #Maybe λNone #Maybe λSome None
|
||||
@ -13,3 +14,18 @@ input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm
|
||||
(Foo) = λ$x let %temp%scrutinee = (Some 1); (Bar$match$1_$_Foo$match$1 %temp%scrutinee $x)
|
||||
|
||||
(Bar) = (let %temp%scrutinee = (Some 1); (Bar$match$1_$_Foo$match$1 %temp%scrutinee $x) λ$x *)
|
||||
|
||||
Scott:
|
||||
(main) = *
|
||||
|
||||
(None) = λNone λSome None
|
||||
|
||||
(Some) = λval λNone λSome (Some val)
|
||||
|
||||
(Bar$match$1_$_Foo$match$1) = λa (a λb b λc λd c)
|
||||
|
||||
(Foo) = λ$x let %temp%scrutinee = (Some 1); (Bar$match$1_$_Foo$match$1 %temp%scrutinee $x)
|
||||
|
||||
(Bar) = (let %temp%scrutinee = (Some 1); (Bar$match$1_$_Foo$match$1 %temp%scrutinee $x) λ$x *)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,14 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_bind.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = cheese
|
||||
|
||||
(cheese) = let num = (+ 2 3); match num { 0: 653323; +num-1: (+ num num-1) }
|
||||
|
||||
Scott:
|
||||
(main) = cheese
|
||||
|
||||
(cheese) = let num = (+ 2 3); match num { 0: 653323; +num-1: (+ num num-1) }
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_list_sugar.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = let %temp%scrutinee = LNil; (main$match$1 %temp%scrutinee)
|
||||
|
||||
(main$match$1) = λa #List (a #List.LCons.head λb #List.LCons.tail λc 1 0)
|
||||
@ -9,3 +10,14 @@ input_file: tests/golden_tests/encode_pattern_match/match_list_sugar.hvm
|
||||
(LNil) = #List λLCons #List λLNil LNil
|
||||
|
||||
(LCons) = λhead λtail #List λLCons #List λLNil #List.LCons.tail (#List.LCons.head (LCons head) tail)
|
||||
|
||||
Scott:
|
||||
(main) = let %temp%scrutinee = LNil; (main$match$1 %temp%scrutinee)
|
||||
|
||||
(main$match$1) = λa (a λb λc 1 0)
|
||||
|
||||
(LNil) = λLCons λLNil LNil
|
||||
|
||||
(LCons) = λhead λtail λLCons λLNil (LCons head tail)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/match_syntax.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(head) = λx (head$match$1 x)
|
||||
|
||||
(head$match$1) = λa #List_ (a #List_.Cons.x λb #List_.Cons.xs λc b Nil)
|
||||
@ -9,3 +10,14 @@ input_file: tests/golden_tests/encode_pattern_match/match_syntax.hvm
|
||||
(Nil) = #List_ λCons #List_ λNil Nil
|
||||
|
||||
(Cons) = λx λxs #List_ λCons #List_ λNil #List_.Cons.xs (#List_.Cons.x (Cons x) xs)
|
||||
|
||||
Scott:
|
||||
(head) = λx (head$match$1 x)
|
||||
|
||||
(head$match$1) = λa (a λb λc b Nil)
|
||||
|
||||
(Nil) = λCons λNil Nil
|
||||
|
||||
(Cons) = λx λxs λCons λNil (Cons x xs)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,14 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/merge_recursive.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(foo_2_$_bar_2) = λa λb (a, b)
|
||||
|
||||
(foo_1_$_bar_1) = λx (x foo_2_$_bar_2)
|
||||
|
||||
Scott:
|
||||
(foo_2_$_bar_2) = λa λb (a, b)
|
||||
|
||||
(foo_1_$_bar_1) = λx (x foo_2_$_bar_2)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/nested_let_tup.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = let %temp%scrutinee = let %temp%scrutinee = (10, ((1, ((2, 3), 4)), 3)); (main$match$1 %temp%scrutinee); (main$match$3 %temp%scrutinee)
|
||||
|
||||
(main$match$3$F0) = λa λb let (c, d) = b; (main$match$2 c)
|
||||
@ -13,3 +14,18 @@ input_file: tests/golden_tests/encode_pattern_match/nested_let_tup.hvm
|
||||
(main$match$2) = λa let (b, c) = a; b
|
||||
|
||||
(main$match$1) = λa let (b, c) = a; (main$match$1$F0 b c)
|
||||
|
||||
Scott:
|
||||
(main) = let %temp%scrutinee = let %temp%scrutinee = (10, ((1, ((2, 3), 4)), 3)); (main$match$1 %temp%scrutinee); (main$match$3 %temp%scrutinee)
|
||||
|
||||
(main$match$3$F0) = λa λb let (c, d) = b; (main$match$2 c)
|
||||
|
||||
(main$match$1$F0) = λa λb let (c, d) = b; c
|
||||
|
||||
(main$match$3) = λa let (b, c) = a; (main$match$3$F0 b c)
|
||||
|
||||
(main$match$2) = λa let (b, c) = a; b
|
||||
|
||||
(main$match$1) = λa let (b, c) = a; (main$match$1$F0 b c)
|
||||
|
||||
|
||||
|
||||
@ -1,11 +0,0 @@
|
||||
---
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/no_literal_builtin.hvm
|
||||
---
|
||||
(main) = *
|
||||
|
||||
(Foo) = λa #String (a #String.SCons.head λb #String.SCons.tail λc 1 0)
|
||||
|
||||
(SCons) = λhead λtail #String λSCons #String λSNil #String.SCons.tail (#String.SCons.head (SCons head) tail)
|
||||
|
||||
(SNil) = #String λSCons #String λSNil SNil
|
||||
@ -2,6 +2,14 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/no_patterns.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(Id_$_Id2) = λx x
|
||||
|
||||
(Pair) = λa λb (a, b)
|
||||
|
||||
Scott:
|
||||
(Id_$_Id2) = λx x
|
||||
|
||||
(Pair) = λa λb (a, b)
|
||||
|
||||
|
||||
|
||||
@ -2,8 +2,18 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/non_matching_fst_arg.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(Foo) = λa λb (#bool (b λc (Foo c c) λd d) a)
|
||||
|
||||
(false) = #bool λtrue #bool λfalse false
|
||||
|
||||
(true) = #bool λtrue #bool λfalse true
|
||||
|
||||
Scott:
|
||||
(Foo) = λa λb (b λc (Foo c c) λd d a)
|
||||
|
||||
(false) = λtrue λfalse false
|
||||
|
||||
(true) = λtrue λfalse true
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/ntup_sum.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (ntupSum ((1, 3), (3, (2, 1))))
|
||||
|
||||
(ntupSum) = λa let (b, c) = a; (ntupSum$F0 b c)
|
||||
@ -9,3 +10,14 @@ input_file: tests/golden_tests/encode_pattern_match/ntup_sum.hvm
|
||||
(ntupSum$F0) = λa let (b, c) = a; λd let (e, f) = d; (ntupSum$F0$F0 b c e f)
|
||||
|
||||
(ntupSum$F0$F0) = λa λb λc λd let (e, f) = d; (+ a (+ b (+ c (+ e f))))
|
||||
|
||||
Scott:
|
||||
(main) = (ntupSum ((1, 3), (3, (2, 1))))
|
||||
|
||||
(ntupSum) = λa let (b, c) = a; (ntupSum$F0 b c)
|
||||
|
||||
(ntupSum$F0) = λa let (b, c) = a; λd let (e, f) = d; (ntupSum$F0$F0 b c e f)
|
||||
|
||||
(ntupSum$F0$F0) = λa λb λc λd let (e, f) = d; (+ a (+ b (+ c (+ e f))))
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/pattern_match_encoding.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (Foo A 2)
|
||||
|
||||
(Foo) = λa #MyType (a #MyType.A.a λb 100 #MyType.B.b λc 200 #MyType.C.c λd 200 #MyType.D.d1 λe #MyType.D.d2 λf 200 #MyType.E.e1 λg #MyType.E.e2 λh 200)
|
||||
@ -15,3 +16,20 @@ input_file: tests/golden_tests/encode_pattern_match/pattern_match_encoding.hvm
|
||||
(B) = λb #MyType λA #MyType λB #MyType λC #MyType λD #MyType λE #MyType.B.b (B b)
|
||||
|
||||
(A) = λa #MyType λA #MyType λB #MyType λC #MyType λD #MyType λE #MyType.A.a (A a)
|
||||
|
||||
Scott:
|
||||
(main) = (Foo A 2)
|
||||
|
||||
(Foo) = λa (a λb 100 λc 200 λd 200 λe λf 200 λg λh 200)
|
||||
|
||||
(E) = λe1 λe2 λA λB λC λD λE (E e1 e2)
|
||||
|
||||
(D) = λd1 λd2 λA λB λC λD λE (D d1 d2)
|
||||
|
||||
(C) = λc λA λB λC λD λE (C c)
|
||||
|
||||
(B) = λb λA λB λC λD λE (B b)
|
||||
|
||||
(A) = λa λA λB λC λD λE (A a)
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/var_only.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = λx match x { false: Foo; true: False }
|
||||
|
||||
(Foo) = λa λb λf (f a)
|
||||
@ -9,3 +10,14 @@ input_file: tests/golden_tests/encode_pattern_match/var_only.hvm
|
||||
(True) = #Bool λFalse #Bool λTrue True
|
||||
|
||||
(False) = #Bool λFalse #Bool λTrue False
|
||||
|
||||
Scott:
|
||||
(main) = λx match x { false: Foo; true: False }
|
||||
|
||||
(Foo) = λa λb λf (f a)
|
||||
|
||||
(True) = λFalse λTrue True
|
||||
|
||||
(False) = λFalse λTrue False
|
||||
|
||||
|
||||
|
||||
@ -2,6 +2,7 @@
|
||||
source: tests/golden_tests.rs
|
||||
input_file: tests/golden_tests/encode_pattern_match/weekday.hvm
|
||||
---
|
||||
TaggedScott:
|
||||
(main) = (λx x Saturday)
|
||||
|
||||
(Sunday) = #Weekday λMonday #Weekday λTuesday #Weekday λWednesday #Weekday λThursday #Weekday λFriday #Weekday λSaturday #Weekday λSunday Sunday
|
||||
@ -17,3 +18,22 @@ input_file: tests/golden_tests/encode_pattern_match/weekday.hvm
|
||||
(Tuesday) = #Weekday λMonday #Weekday λTuesday #Weekday λWednesday #Weekday λThursday #Weekday λFriday #Weekday λSaturday #Weekday λSunday Tuesday
|
||||
|
||||
(Wednesday) = #Weekday λMonday #Weekday λTuesday #Weekday λWednesday #Weekday λThursday #Weekday λFriday #Weekday λSaturday #Weekday λSunday Wednesday
|
||||
|
||||
Scott:
|
||||
(main) = (λx x Saturday)
|
||||
|
||||
(Sunday) = λMonday λTuesday λWednesday λThursday λFriday λSaturday λSunday Sunday
|
||||
|
||||
(Saturday) = λMonday λTuesday λWednesday λThursday λFriday λSaturday λSunday Saturday
|
||||
|
||||
(Friday) = λMonday λTuesday λWednesday λThursday λFriday λSaturday λSunday Friday
|
||||
|
||||
(Thursday) = λMonday λTuesday λWednesday λThursday λFriday λSaturday λSunday Thursday
|
||||
|
||||
(Monday) = λMonday λTuesday λWednesday λThursday λFriday λSaturday λSunday Monday
|
||||
|
||||
(Tuesday) = λMonday λTuesday λWednesday λThursday λFriday λSaturday λSunday Tuesday
|
||||
|
||||
(Wednesday) = λMonday λTuesday λWednesday λThursday λFriday λSaturday λSunday Wednesday
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user