Merge pull request #542 from HigherOrderCO/call-expand-generated-for-succ-term

Call expand_generated for succ_term
This commit is contained in:
Nicolas Abril 2024-06-04 19:22:18 +00:00 committed by GitHub
commit d382c7a60e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
7 changed files with 26 additions and 39 deletions

2
Cargo.lock generated
View File

@ -62,7 +62,7 @@ dependencies = [
[[package]]
name = "bend-lang"
version = "0.2.30"
version = "0.2.31"
dependencies = [
"TSPL",
"clap",

View File

@ -2,7 +2,7 @@
name = "bend-lang"
description = "A high-level, massively parallel programming language"
license = "Apache-2.0"
version = "0.2.30"
version = "0.2.31"
edition = "2021"
rust-version = "1.74"
exclude = ["tests/"]

View File

@ -19,6 +19,7 @@ pub fn net_to_term(
net,
labels,
book,
recursive_defs: &book.recursive_defs(),
dup_paths: if linear { None } else { Some(Default::default()) },
scope: Default::default(),
seen_fans: Default::default(),
@ -72,6 +73,7 @@ pub struct Reader<'a> {
seen_fans: Scope,
seen: HashSet<Port>,
errors: Vec<ReadbackError>,
recursive_defs: &'a BTreeSet<Name>,
}
impl Reader<'_> {
@ -140,6 +142,8 @@ impl Reader<'_> {
let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1)));
let mut succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2)));
// Call expand_generated in case of succ_term be a lifted term
succ_term.expand_generated(self.book, self.recursive_defs);
// Succ term should be a lambda
let (zero, succ) = match &mut succ_term {

View File

@ -16,21 +16,11 @@ impl Book {
let body = match adt_encoding {
AdtEncoding::Scott => encode_ctr_scott(fields.iter().map(|f| &f.nam), ctrs, ctr_name),
AdtEncoding::NumScott => {
let is_object = adt_name == ctr_name;
if is_object {
let tag = Name::new(format!("{ctr_name}/tag"));
let body = encode_ctr_num_scott(fields.iter().map(|f| &f.nam), &tag);
let tag_def = make_tag_def(ctr_idx, &tag, adt);
tags.push((tag, tag_def));
body
} else {
let (typ, ctr) = ctr_name.rsplit_once('/').expect("To split at '/'");
let tag = Name::new(format!("{typ}/{ctr}/tag"));
let body = encode_ctr_num_scott(fields.iter().map(|f| &f.nam), &tag);
let tag_def = make_tag_def(ctr_idx, &tag, adt);
tags.push((tag, tag_def));
body
}
let tag = make_tag(adt_name == ctr_name, ctr_name);
let body = encode_ctr_num_scott(fields.iter().map(|f| &f.nam), &tag);
let tag_def = make_tag_def(ctr_idx, &tag, adt);
tags.push((tag, tag_def));
body
}
};
@ -44,6 +34,15 @@ impl Book {
}
}
fn make_tag(is_object: bool, ctr_name: &Name) -> Name {
if is_object {
Name::new(format!("{ctr_name}/tag"))
} else {
let (typ, ctr) = ctr_name.rsplit_once('/').expect("To split at '/'");
Name::new(format!("{typ}/{ctr}/tag"))
}
}
fn encode_ctr_scott<'a>(
ctr_args: impl DoubleEndedIterator<Item = &'a Name> + Clone,
ctrs: Vec<Name>,

View File

@ -191,8 +191,8 @@ pub fn readback_hvm_net(
let mut diags = Diagnostics::default();
let net = hvm_to_net(net);
let mut term = net_to_term(&net, book, labels, linear, &mut diags);
let recursive_cycles = book.recursive_defs();
term.expand_generated(book, &recursive_cycles);
let recursive_defs = book.recursive_defs();
term.expand_generated(book, &recursive_defs);
term.resugar_strings(adt_encoding);
term.resugar_lists(adt_encoding);
(term, diags)

View File

@ -3,15 +3,7 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/linearize_match.bend
---
NumScott:
Warnings:
During readback:
Encountered an invalid 'switch'.
λa switch a = a { 0: λb b; _: λa λb (+ a b); }
λa switch a = a { 0: λb b; _: λb (+ a-1 b); }
Scott:
Warnings:
During readback:
Encountered an invalid 'switch'.
λa switch a = a { 0: λb b; _: λa λb (+ a b); }
λa switch a = a { 0: λb b; _: λb (+ a-1 b); }

View File

@ -3,15 +3,7 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/match_mult_linearization.bend
---
NumScott:
Warnings:
During readback:
Encountered an invalid 'switch'.
λa switch a = a { 0: λa λb λc (+ (+ a b) c); _: λa λb λc λd (+ (+ (+ a b) c) d); }
λa switch a = a { 0: λa λb λc (+ (+ a b) c); _: λb λc λd (+ (+ (+ a-1 b) c) d); }
Scott:
Warnings:
During readback:
Encountered an invalid 'switch'.
λa switch a = a { 0: λa λb λc (+ (+ a b) c); _: λa λb λc λd (+ (+ (+ a b) c) d); }
λa switch a = a { 0: λa λb λc (+ (+ a b) c); _: λb λc λd (+ (+ (+ a-1 b) c) d); }