Re-add unlabeled sup/dup compiling to tag 0

This commit is contained in:
LunaAmora 2024-01-18 15:36:25 -03:00
parent 7580bd09c3
commit 8771b9ae0e
16 changed files with 72 additions and 18 deletions

2
Cargo.lock generated
View File

@ -211,7 +211,7 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
[[package]]
name = "hvm-core"
version = "0.2.14"
source = "git+https://github.com/HigherOrderCO/hvm-core?branch=lazy_mode#8c44696f1a8075e0cb8af85e2d7a0d567ca29d06"
source = "git+https://github.com/HigherOrderCO/hvm-core?branch=lazy_mode#0e3ac49550bd900f51d3bdc7ee6c35f1e212dbd6"
dependencies = [
"nohash-hasher",
]

42
error.hvm Normal file
View File

@ -0,0 +1,42 @@
data Bool
= True
| False
data Tree
= (N x y)
| L
(And a b) = match a {
True: b
False: False
}
(equal a b) = match a {
N: match b {
N: (And (equal a.x b.x) (equal a.y b.y))
L: False
}
L: match b {
N: False
L: True
}
}
data Maybe
= None
| (Some value)
(join None b) = b
(join (Some a) b) = (Some a)
(view n) = (n λx λe match e { False: None; True: (Some x) })
(B n) = match n {
0: L
+: {L (N (B n-1) (B n-1))}
}
main =
let a = (N L (N L L))
let b = (B 4)
(view λt(t b (equal a b)))

View File

@ -332,7 +332,7 @@ fn expand(net: &mut hvmc::run::Net, book: &hvmc::run::Book) {
fn reduce(net: &mut hvmc::run::Net, book: &hvmc::run::Book, limit: usize) -> usize {
match net {
hvmc::run::Net::Eager(net) => net.net.reduce(book, limit),
_ => panic!("Unsuported configuration, disable debug mode `-D` or enable less optimzations `-O=0`"),
_ => panic!("Unsupported configuration, disable debug mode `-D` or enable less optimizations `-O=0`"),
}
}

View File

@ -81,7 +81,13 @@ fn tree_to_inodes(
let lft = process_node_subtree(lft, net_root, &mut subtrees, n_vars);
let rgt = process_node_subtree(rgt, net_root, &mut subtrees, n_vars);
inodes.push(INode {
kind: if lab & 1 == 0 { Con { lab: Some((lab >> 1) - 1) } } else { Dup { lab: (lab >> 1) - 1 } },
kind: if *lab == 0 {
Dup { lab: 0 }
} else if lab & 1 != 0 {
Dup { lab: lab >> 1 }
} else {
Con { lab: Some(lab >> 1) }
},
ports: [subtree_root, lft, rgt],
});
}

View File

@ -56,13 +56,13 @@ fn net_tree_to_hvmc_tree(
NodeKind::Con { lab: Some(lab) } => Tree::Dup {
#[allow(clippy::identity_op)]
// label shifted left with bit 0 set as 0
lab: (lab + 1) << 1 | 0,
lab: lab << 1 | 0,
lft: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id, id_to_hvmc_name)),
rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id, id_to_hvmc_name)),
},
NodeKind::Dup { lab } => Tree::Dup {
// label shifted left with bit 0 set as 1
lab: (lab + 1) << 1 | 1,
lab: if lab == 0 { 0 } else { lab << 1 | 1 },
lft: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id, id_to_hvmc_name)),
rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id, id_to_hvmc_name)),
},

View File

@ -203,7 +203,7 @@ where
.boxed();
// #tag {fst snd}
let sup = tag(Tag::Auto)
let sup = tag(Tag::Numeric(0))
.then_ignore(just(Token::LBracket))
.then(term.clone())
.then(term.clone())
@ -213,7 +213,7 @@ where
// let #tag? {x1 x2} = body; next
let dup = just(Token::Let)
.ignore_then(tag(Tag::Auto))
.ignore_then(tag(Tag::Numeric(0)))
.then_ignore(just(Token::LBracket))
.then(name_or_era())
.then(name_or_era())

View File

@ -347,13 +347,19 @@ pub struct Labels {
pub dup: LabelGenerator,
}
#[derive(Debug, Default)]
#[derive(Debug)]
pub struct LabelGenerator {
pub next: u32,
pub name_to_label: HashMap<Name, u32>,
pub label_to_name: HashMap<u32, Name>,
}
impl Default for LabelGenerator {
fn default() -> Self {
Self { next: 1, name_to_label: Default::default(), label_to_name: Default::default() }
}
}
impl LabelGenerator {
// If some tag and new generate a new label, otherwise return the generated label.
// If none use the implicit label counter.

View File

@ -2,7 +2,7 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/ex0.hvm
---
@C_2 = ({3 (a b) (c a)} (c b))
@C_2 = ({0 (a b) (c a)} (c b))
@S = (a ((a b) (* b)))
@Z = (* (a a))
@main = a

View File

@ -5,7 +5,7 @@ input_file: tests/golden_tests/compile_file_o_all/ex2.hvm
@E = (* @J)
@I = (a (* ((a b) (* b))))
@J = (* (a a))
@c2 = ({3 (a b) (c a)} (c b))
@c2 = ({0 (a b) (c a)} (c b))
@decO = ((@decO (@low (@E a))) (* ((a b) (* b))))
@low = ((@lowO (@lowI (@E a))) a)
@lowI = (a (((* ((a b) (* b))) c) (* (* c))))

View File

@ -3,7 +3,7 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm
---
@7 = (a (* a))
@Foo = (?<({3 @Foo @Foo} @7) a> a)
@Foo = (?<({0 @Foo @Foo} @7) a> a)
@main = a
& @Foo ~ (#0 a)

View File

@ -3,4 +3,4 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_term/church_one.hvm
---
a
& ((b (c d)) ({3 (d e) b} (c e))) ~ ((* (f f)) a)
& ((b (c d)) ({0 (d e) b} (c e))) ~ ((* (f f)) a)

View File

@ -2,5 +2,5 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_term/complicated_dup.hvm
---
({5 (a b) (c d)} e)
& ((f {3 a c}) b) ~ ((f d) e)
({0 (a b) (c d)} e)
& ((f {0 a c}) b) ~ ((f d) e)

View File

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_term/dup_apply.hvm
---
({3 (a b) a} b)
({0 (a b) a} b)

View File

@ -3,4 +3,4 @@ source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_term/dup_global_lam.hvm
---
a
& ({3 (b c) b} (d d)) ~ (c a)
& ({0 (b c) b} (d d)) ~ (c a)

View File

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/compile_term/erased_dup.hvm
---
({3 * a} a)
({0 * a} a)

View File

@ -2,4 +2,4 @@
source: tests/golden_tests.rs
input_file: tests/golden_tests/run_file/superposed_is_even.hvm
---
#0 {#1 {T F} #2 {T F}}
#0 {#0 {T F} #0 {T F}}