Revert unlabeled dups/sups being 0

This commit is contained in:
LunaAmora 2024-02-02 19:11:20 -03:00
parent d5196e0e97
commit 6a500bcf1e
9 changed files with 51 additions and 83 deletions

4
Cargo.lock generated
View File

@ -210,8 +210,8 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
[[package]]
name = "hvm-core"
version = "0.2.15"
source = "git+https://github.com/HigherOrderCO/hvm-core#8d031c4896c678421238574fdb694bad13089953"
version = "0.2.18"
source = "git+https://github.com/HigherOrderCO/hvm-core#56f62fd7342988e9887eb0996b19a2fdab4709bb"
dependencies = [
"nohash-hasher",
]

View File

@ -25,14 +25,14 @@ use crate::term::net_to_term::ReadbackErrors;
pub fn check_book(mut book: Book) -> Result<(), String> {
// TODO: Do the checks without having to do full compilation
compile_book(&mut book, CompileOpts::light(), false)?;
compile_book(&mut book, CompileOpts::light())?;
Ok(())
}
pub fn compile_book(book: &mut Book, opts: CompileOpts, lazy_mode: bool) -> Result<CompileResult, String> {
pub fn compile_book(book: &mut Book, opts: CompileOpts) -> Result<CompileResult, String> {
let (main, warnings) = desugar_book(book, opts)?;
let (nets, hvmc_names, labels) = book_to_nets(book, main, lazy_mode);
let mut core_book = nets_to_hvmc(nets, &hvmc_names, lazy_mode)?;
let (nets, hvmc_names, labels) = book_to_nets(book, main);
let mut core_book = nets_to_hvmc(nets, &hvmc_names)?;
if opts.pre_reduce {
pre_reduce_book(&mut core_book, opts.pre_reduce_refs)?;
}
@ -100,14 +100,13 @@ pub fn run_book(
warning_opts: WarningOpts,
compile_opts: CompileOpts,
) -> Result<(Term, DefNames, RunInfo), String> {
let CompileResult { core_book, hvmc_names, labels, warnings } =
compile_book(&mut book, compile_opts, run_opts.lazy_mode)?;
let CompileResult { core_book, hvmc_names, labels, warnings } = compile_book(&mut book, compile_opts)?;
display_warnings(warning_opts, &warnings)?;
let debug_hook = run_opts.debug_hook(&book, &hvmc_names, &labels);
let (res_lnet, stats) = run_compiled(&core_book, mem_size, run_opts, debug_hook);
let net = hvmc_to_net(&res_lnet, &|id| hvmc_names.hvmc_name_to_id[&id], run_opts.lazy_mode);
let net = hvmc_to_net(&res_lnet, &|id| hvmc_names.hvmc_name_to_id[&id]);
let (res_term, readback_errors) = net_to_term(&net, &book, &labels, run_opts.linear);
let info = RunInfo { stats, readback_errors, net: res_lnet };
Ok((res_term, book.def_names, info))
@ -170,7 +169,7 @@ impl RunOpts {
) -> Option<impl FnMut(&Net) + 'a> {
self.debug.then_some({
|net: &_| {
let net = hvmc_to_net(net, &|id| hvmc_names.hvmc_name_to_id[&id], self.lazy_mode);
let net = hvmc_to_net(net, &|id| hvmc_names.hvmc_name_to_id[&id]);
let (res_term, errors) = net_to_term(&net, book, labels, self.linear);
println!(
"{}{}\n---------------------------------------",

View File

@ -60,7 +60,7 @@ enum Mode {
#[arg(short = 'l', help = "Linear readback (show explicit dups)")]
linear: bool,
#[arg(short, long = "stats", help = "Shows runtime stats and rewrite counts")]
#[arg(short = 's', long = "stats", help = "Shows runtime stats and rewrite counts")]
arg_stats: bool,
#[arg(help = "Path to the input file")]
@ -168,7 +168,7 @@ fn execute_cli_mode(cli: Cli, verbose: &dyn Fn(&hvml::term::Book)) -> Result<(),
let mut book = load_file_to_book(&path)?;
verbose(&book);
let compiled = compile_book(&mut book, opts, lazy_mode)?;
let compiled = compile_book(&mut book, opts)?;
hvml::display_warnings(warning_opts, &compiled.warnings)?;
print!("{}", show_book(&compiled.core_book));
}

View File

@ -5,27 +5,27 @@ use hvmc::{
run::Val,
};
pub fn hvmc_to_net(net: &Net, hvmc_name_to_id: &impl Fn(Val) -> DefId, lazy: bool) -> INet {
let inodes = hvmc_to_inodes(net, hvmc_name_to_id, lazy);
pub fn hvmc_to_net(net: &Net, hvmc_name_to_id: &impl Fn(Val) -> DefId) -> INet {
let inodes = hvmc_to_inodes(net, hvmc_name_to_id);
inodes_to_inet(&inodes)
}
fn hvmc_to_inodes(net: &Net, hvmc_name_to_id: &impl Fn(Val) -> DefId, lazy: bool) -> INodes {
fn hvmc_to_inodes(net: &Net, hvmc_name_to_id: &impl Fn(Val) -> DefId) -> INodes {
let mut inodes = vec![];
let mut n_vars = 0;
let net_root = if let Tree::Var { nam } = &net.root { nam } else { "" };
// If we have a tree attached to the net root, convert that first
if !matches!(&net.root, Tree::Var { .. }) {
let mut root = tree_to_inodes(&net.root, "_".to_string(), net_root, &mut n_vars, hvmc_name_to_id, lazy);
let mut root = tree_to_inodes(&net.root, "_".to_string(), net_root, &mut n_vars, hvmc_name_to_id);
inodes.append(&mut root);
}
// Convert all the trees forming active pairs.
for (i, (tree1, tree2)) in net.rdex.iter().enumerate() {
let tree_root = format!("a{i}");
let mut tree1 = tree_to_inodes(tree1, tree_root.clone(), net_root, &mut n_vars, hvmc_name_to_id, lazy);
let mut tree1 = tree_to_inodes(tree1, tree_root.clone(), net_root, &mut n_vars, hvmc_name_to_id);
inodes.append(&mut tree1);
let mut tree2 = tree_to_inodes(tree2, tree_root, net_root, &mut n_vars, hvmc_name_to_id, lazy);
let mut tree2 = tree_to_inodes(tree2, tree_root, net_root, &mut n_vars, hvmc_name_to_id);
inodes.append(&mut tree2);
}
inodes
@ -37,7 +37,6 @@ fn tree_to_inodes(
net_root: &str,
n_vars: &mut NodeId,
hvmc_name_to_id: &impl Fn(Val) -> DefId,
lazy: bool,
) -> INodes {
fn new_var(n_vars: &mut NodeId) -> String {
let new_var = format!("x{n_vars}");
@ -82,15 +81,7 @@ 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: match (lazy, *lab) {
(true, 0) => Dup { lab: 0 },
(true, lab) if lab & 1 == 0 => Con { lab: Some(lab >> 1) },
(false, lab) if lab & 1 == 0 => Con { lab: Some((lab >> 1) - 1) },
(true, _) => Dup { lab: lab >> 1 },
(false, _) => Dup { lab: (lab >> 1) - 1 },
},
kind: if lab & 1 == 0 { Con { lab: Some((lab >> 1) - 1) } } else { Dup { lab: (lab >> 1) - 1 } },
ports: [subtree_root, lft, rgt],
});
}

View File

@ -7,22 +7,22 @@ use hvmc::{
use std::collections::{HashMap, HashSet};
/// Converts the inet-encoded definitions into an hvmc AST Book.
pub fn nets_to_hvmc(nets: HashMap<String, INet>, hvmc_names: &HvmcNames, lazy: bool) -> Result<Book, String> {
pub fn nets_to_hvmc(nets: HashMap<String, INet>, hvmc_names: &HvmcNames) -> Result<Book, String> {
let mut book = Book::new();
for (name, inet) in nets {
let net = net_to_hvmc(&inet, &|id| hvmc_names.id_to_hvmc_name[&id], lazy)?;
let net = net_to_hvmc(&inet, &|id| hvmc_names.id_to_hvmc_name[&id])?;
book.insert(name, net);
}
Ok(book)
}
/// Convert an inet-encoded definition into an hvmc AST inet.
pub fn net_to_hvmc(inet: &INet, id_to_hvmc_name: &impl Fn(DefId) -> Val, lazy: bool) -> Result<Net, String> {
pub fn net_to_hvmc(inet: &INet, id_to_hvmc_name: &impl Fn(DefId) -> 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 {
// If there is a root tree connected to the root node
net_tree_to_hvmc_tree(inet, net_root, &mut port_to_var_id, id_to_hvmc_name, lazy)
net_tree_to_hvmc_tree(inet, net_root, &mut port_to_var_id, id_to_hvmc_name)
} else {
// If the root node points to some aux port (application)
port_to_var_id.insert(inet.enter_port(ROOT), 0);
@ -30,8 +30,8 @@ pub fn net_to_hvmc(inet: &INet, id_to_hvmc_name: &impl Fn(DefId) -> Val, lazy: b
};
let mut rdex = vec![];
for [root0, root1] in redxs {
let rdex0 = net_tree_to_hvmc_tree(inet, root0, &mut port_to_var_id, id_to_hvmc_name, lazy);
let rdex1 = net_tree_to_hvmc_tree(inet, root1, &mut port_to_var_id, id_to_hvmc_name, lazy);
let rdex0 = net_tree_to_hvmc_tree(inet, root0, &mut port_to_var_id, id_to_hvmc_name);
let rdex1 = net_tree_to_hvmc_tree(inet, root1, &mut port_to_var_id, id_to_hvmc_name);
rdex.push((rdex0, rdex1));
}
Ok(Net { root, rdex })
@ -42,45 +42,40 @@ fn net_tree_to_hvmc_tree(
tree_root: NodeId,
port_to_var_id: &mut HashMap<Port, VarId>,
id_to_hvmc_name: &impl Fn(DefId) -> Val,
lazy: bool,
) -> Tree {
match inet.node(tree_root).kind {
NodeKind::Era => Tree::Era,
NodeKind::Con { lab: None } => Tree::Con {
lft: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id, id_to_hvmc_name, lazy)),
rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id, id_to_hvmc_name, lazy)),
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::Tup => Tree::Tup {
lft: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id, id_to_hvmc_name, lazy)),
rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id, id_to_hvmc_name, lazy)),
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::Con { lab: Some(lab) } => Tree::Dup {
#[allow(clippy::identity_op)]
// label shifted left with bit 0 set as 0
lab: (if lazy { lab } else { lab + 1 }) << 1 | 0,
lft: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id, id_to_hvmc_name, lazy)),
rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id, id_to_hvmc_name, lazy)),
lab: (lab + 1) << 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: if lazy {
if lab == 0 { 0 } else { lab << 1 | 1 }
} else {
(lab + 1) << 1 | 1
},
lft: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id, id_to_hvmc_name, lazy)),
rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id, id_to_hvmc_name, lazy)),
lab: (lab + 1) << 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)),
},
NodeKind::Ref { def_id } => Tree::Ref { nam: id_to_hvmc_name(def_id) },
NodeKind::Num { val } => Tree::Num { val },
NodeKind::Op2 { opr } => Tree::Op2 {
opr,
lft: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id, id_to_hvmc_name, lazy)),
rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id, id_to_hvmc_name, lazy)),
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::Mat => Tree::Mat {
sel: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id, id_to_hvmc_name, lazy)),
ret: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id, id_to_hvmc_name, lazy)),
sel: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id, id_to_hvmc_name)),
ret: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id, id_to_hvmc_name)),
},
NodeKind::Rot => unreachable!(),
}
@ -91,12 +86,11 @@ fn var_or_subtree(
src_port: Port,
port_to_var_id: &mut HashMap<Port, VarId>,
id_to_hvmc_name: &impl Fn(DefId) -> Val,
lazy: bool,
) -> Tree {
let dst_port = inet.enter_port(src_port);
if dst_port.slot() == 0 {
// Subtree
net_tree_to_hvmc_tree(inet, dst_port.node(), port_to_var_id, id_to_hvmc_name, lazy)
net_tree_to_hvmc_tree(inet, dst_port.node(), port_to_var_id, id_to_hvmc_name)
} else {
// Var
if let Some(&var_id) = port_to_var_id.get(&src_port) {

View File

@ -1,7 +1,7 @@
pub mod ctrs_arities;
pub mod exhaustiveness;
pub mod has_main;
pub mod shared_names;
pub mod type_check;
pub mod unbound_pats;
pub mod unbound_vars;
pub mod ctrs_arities;

View File

@ -15,10 +15,10 @@ pub struct HvmcNames {
pub hvmc_name_to_id: HashMap<Val, DefId>,
}
pub fn book_to_nets(book: &Book, main: DefId, lazy: bool) -> (HashMap<String, INet>, HvmcNames, Labels) {
pub fn book_to_nets(book: &Book, main: DefId) -> (HashMap<String, INet>, HvmcNames, Labels) {
let mut nets = HashMap::new();
let mut hvmc_names = HvmcNames::default();
let mut labels = Labels::new(lazy);
let mut labels = Labels::default();
for def in book.defs.values() {
for rule in def.rules.iter() {
@ -341,32 +341,19 @@ impl Op {
}
}
#[derive(Debug)]
#[derive(Debug, Default)]
pub struct Labels {
pub con: LabelGenerator,
pub dup: LabelGenerator,
}
impl Labels {
pub fn new(lazy: bool) -> Self {
Self { con: LabelGenerator::default(lazy), dup: LabelGenerator::default(lazy) }
}
}
#[derive(Debug)]
#[derive(Debug, Default)]
pub struct LabelGenerator {
pub lazy: bool,
pub next: u32,
pub name_to_label: HashMap<Name, u32>,
pub label_to_name: HashMap<u32, Name>,
}
impl LabelGenerator {
fn default(lazy: bool) -> Self {
Self { lazy, next: lazy.into(), 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.
@ -386,7 +373,6 @@ impl LabelGenerator {
}
},
Tag::Numeric(lab) => Some(*lab),
Tag::Auto if self.lazy => Some(0),
Tag::Auto => Some(unique()),
Tag::Static => None,
}

View File

@ -85,9 +85,8 @@ fn compile_term() {
term.make_var_names_unique();
term.linearize_vars();
let lazy_mode = false;
let compat_net = term_to_compat_net(&term, &mut Labels::new(lazy_mode));
let net = net_to_hvmc(&compat_net, &|def_id| def_id.to_internal(), lazy_mode)?;
let compat_net = term_to_compat_net(&term, &mut Labels::default());
let net = net_to_hvmc(&compat_net, &|def_id| def_id.to_internal())?;
Ok(show_net(&net))
})
@ -97,7 +96,7 @@ fn compile_term() {
fn compile_file_o_all() {
run_golden_test_dir(function_name!(), &|code, path| {
let mut book = do_parse_book(code, path)?;
let compiled = compile_book(&mut book, CompileOpts::heavy(), false)?;
let compiled = compile_book(&mut book, CompileOpts::heavy())?;
Ok(format!("{:?}", compiled))
})
}
@ -105,7 +104,7 @@ fn compile_file_o_all() {
fn compile_file() {
run_golden_test_dir(function_name!(), &|code, path| {
let mut book = do_parse_book(code, path)?;
let compiled = compile_book(&mut book, CompileOpts::light(), false)?;
let compiled = compile_book(&mut book, CompileOpts::light())?;
Ok(format!("{:?}", compiled))
})
}
@ -141,9 +140,8 @@ fn readback_lnet() {
run_golden_test_dir(function_name!(), &|code, _| {
let net = do_parse_net(code)?;
let book = Book::default();
let lazy_mode = false;
let compat_net = hvmc_to_net(&net, &DefId::from_internal, lazy_mode);
let (term, errors) = net_to_term(&compat_net, &book, &Labels::new(lazy_mode), false);
let compat_net = hvmc_to_net(&net, &DefId::from_internal);
let (term, errors) = net_to_term(&compat_net, &book, &Labels::default(), false);
Ok(format!("{}{}", errors.display(&book.def_names), term.display(&book.def_names)))
})
}

View File

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