From 94c3b449f59e10a2ac67cded01a1f0eaee62a98b Mon Sep 17 00:00:00 2001 From: tjjfvi Date: Thu, 29 Feb 2024 10:38:39 -0500 Subject: [PATCH 1/2] bump hvmc --- Cargo.lock | 3 ++- cspell.json | 1 - src/hvmc_net/pre_reduce.rs | 8 ++++---- src/hvmc_net/prune.rs | 2 +- src/lib.rs | 14 +++++++------- src/main.rs | 3 +-- src/net/hvmc_to_net.rs | 2 +- src/net/net_to_hvmc.rs | 14 +++++++------- 8 files changed, 23 insertions(+), 24 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index b9e1fba0f..df20db785 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -202,8 +202,9 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03" [[package]] name = "hvm-core" version = "0.2.19" -source = "git+https://github.com/HigherOrderCO/hvm-core#c1f123210d1e918dfce12060c7f4b57b602bb02c" +source = "git+https://github.com/HigherOrderCO/hvm-core#0433f52cd51f3b9c8db3630bf338d378d5b2908d" dependencies = [ + "clap", "nohash-hasher", ] diff --git a/cspell.json b/cspell.json index 7bd1f52e8..495185188 100644 --- a/cspell.json +++ b/cspell.json @@ -48,7 +48,6 @@ "oprune", "oref", "postcondition", - "rdex", "redex", "redexes", "readback", diff --git a/src/hvmc_net/pre_reduce.rs b/src/hvmc_net/pre_reduce.rs index f2606b66a..2f4e4e831 100644 --- a/src/hvmc_net/pre_reduce.rs +++ b/src/hvmc_net/pre_reduce.rs @@ -41,11 +41,11 @@ pub fn pre_reduce_book(book: &mut Book, entrypoint: &str) -> Result<(), String> for (nam, net) in book.iter_mut() { // Skip unnecessary work - if net.rdex.is_empty() || *nam == entrypoint { + if net.redexes.is_empty() || *nam == entrypoint { continue; } - let area = hvmc::run::Net::::init_heap(1 << 18); + let area = hvmc::run::Heap::new_words(1 << 18); let mut rt = hvmc::run::DynNet::new(&area, false); dispatch_dyn_net!(&mut rt => { rt.boot(host.defs.get(nam).expect("No function.")); @@ -53,12 +53,12 @@ pub fn pre_reduce_book(book: &mut Book, entrypoint: &str) -> Result<(), String> rt.reduce(MAX_RWTS); }); - // Move interactions with inert defs back into the net rdex array + // Move interactions with inert defs back into the net redexes array for def in host.defs.values() { if let Some(def) = def.downcast_ref::() { let mut stored_redexes = def.data.0.lock().unwrap(); dispatch_dyn_net!(&mut rt => { - rt.rdex.extend(core::mem::take(&mut *stored_redexes)); + rt.redexes.extend(core::mem::take(&mut *stored_redexes)); }) } } diff --git a/src/hvmc_net/prune.rs b/src/hvmc_net/prune.rs index a5af93944..76d4904a0 100644 --- a/src/hvmc_net/prune.rs +++ b/src/hvmc_net/prune.rs @@ -11,7 +11,7 @@ pub fn prune_defs(book: &mut Book, entrypoint: String) { while let Some(nam) = to_visit.pop() { let def = &book[&nam]; used_defs_in_tree(&def.root, &mut used_defs, &mut to_visit); - for (a, b) in &def.rdex { + for (a, b) in &def.redexes { used_defs_in_tree(a, &mut used_defs, &mut to_visit); used_defs_in_tree(b, &mut used_defs, &mut to_visit); } diff --git a/src/lib.rs b/src/lib.rs index fff01d99f..df68be3ce 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -6,7 +6,7 @@ use hvmc::{ ast::{self, Net}, dispatch_dyn_net, host::Host, - run::{DynNet, Net as RtNet, Rewrites}, + run::{DynNet, Heap, Rewrites}, stdlib::LogDef, }; use hvmc_net::{pre_reduce::pre_reduce_book, prune::prune_defs}; @@ -53,7 +53,7 @@ pub fn create_host(book: Arc, labels: Arc, compile_opts: CompileOp move |wire| { let host = host.lock().unwrap(); let tree = host.readback_tree(&wire); - let net = hvmc::ast::Net { root: tree, rdex: vec![] }; + let net = hvmc::ast::Net { root: tree, redexes: vec![] }; let net = hvmc_to_net(&net); let (mut term, mut readback_errors) = net_to_term(&net, &book, &labels, false); let resugar_errs = term.resugar_adts(&book, compile_opts.adt_encoding); @@ -73,7 +73,7 @@ pub fn create_host(book: Arc, labels: Arc, compile_opts: CompileOp move |wire| { let host = host.lock().unwrap(); let tree = host.readback_tree(&wire); - let net = hvmc::ast::Net { root: tree, rdex: vec![] }; + let net = hvmc::ast::Net { root: tree, redexes: vec![] }; let net = hvmc_to_net(&net); let (mut term, mut readback_errors) = net_to_term(&net, &book, &labels, false); let resugar_errs = term.resugar_adts(&book, compile_opts.adt_encoding); @@ -217,7 +217,7 @@ pub fn run_book( pub fn count_nodes<'l>(net: &'l hvmc::ast::Net) -> usize { let mut visit: Vec<&'l hvmc::ast::Tree> = vec![&net.root]; let mut count = 0usize; - for (l, r) in &net.rdex { + for (l, r) in &net.redexes { visit.push(l); visit.push(r); } @@ -253,7 +253,7 @@ pub fn run_compiled( hook: Option, entrypoint: &str, ) -> (Net, RunStats) { - let heap = RtNet::::init_heap(mem_size); + let heap = Heap::new_bytes(mem_size); let mut root = DynNet::new(&heap, run_opts.lazy_mode); let max_rwts = run_opts.max_rewrites.map(|x| x.clamp(usize::MIN as u64, usize::MAX as u64) as usize); // Expect won't be reached because there's @@ -265,7 +265,7 @@ pub fn run_compiled( if let Some(mut hook) = hook { root.expand(); - while !root.rdex.is_empty() { + while !root.redexes.is_empty() { hook(&host.lock().unwrap().readback(root)); root.reduce(1); root.expand(); @@ -278,7 +278,7 @@ pub fn run_compiled( panic!("Parallel mode does not yet support rewrite limit"); } root.expand(); - while !root.rdex.is_empty() { + while !root.redexes.is_empty() { let old_rwts = root.rwts.total(); root.reduce(max_rwts); let delta_rwts = root.rwts.total() - old_rwts; diff --git a/src/main.rs b/src/main.rs index 6afe45f8e..7f4f5d2a7 100644 --- a/src/main.rs +++ b/src/main.rs @@ -232,9 +232,8 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Info> { let book = load_book(&path)?; - let mem_size = max_mem / std::mem::size_of::() as u64; let run_opts = - RunOpts { single_core, debug, linear, lazy_mode, max_memory: mem_size, max_rewrites: max_rwts }; + RunOpts { single_core, debug, linear, lazy_mode, max_memory: max_mem, max_rewrites: max_rwts }; let (res_term, RunInfo { stats, readback_errors, net, book: _, labels: _ }) = run_book(book, max_mem as usize, run_opts, warning_opts, opts)?; diff --git a/src/net/hvmc_to_net.rs b/src/net/hvmc_to_net.rs index 6968f1989..2257580f5 100644 --- a/src/net/hvmc_to_net.rs +++ b/src/net/hvmc_to_net.rs @@ -18,7 +18,7 @@ fn hvmc_to_inodes(net: &Net) -> INodes { inodes.append(&mut root); } // Convert all the trees forming active pairs. - for (i, (tree1, tree2)) in net.rdex.iter().enumerate() { + for (i, (tree1, tree2)) in net.redexes.iter().enumerate() { let tree_root = format!("a{i}"); let mut tree1 = tree_to_inodes(tree1, tree_root.clone(), net_root, &mut n_vars); inodes.append(&mut tree1); diff --git a/src/net/net_to_hvmc.rs b/src/net/net_to_hvmc.rs index 917da0b6d..8eeefb164 100644 --- a/src/net/net_to_hvmc.rs +++ b/src/net/net_to_hvmc.rs @@ -16,7 +16,7 @@ pub fn nets_to_hvmc(nets: HashMap) -> Result { /// Convert an inet-encoded definition into an hvmc AST inet. pub fn net_to_hvmc(inet: &INet) -> Result { - let (net_root, redexes) = get_tree_roots(inet)?; + let (net_root, net_redexes) = get_tree_roots(inet)?; let mut port_to_var_id: HashMap = HashMap::new(); let root = if let Some(net_root) = net_root { // If there is a root tree connected to the root node @@ -26,13 +26,13 @@ pub fn net_to_hvmc(inet: &INet) -> Result { port_to_var_id.insert(inet.enter_port(ROOT), 0); Tree::Var { nam: num_to_name(0) } }; - let mut rdex = vec![]; - for [root0, root1] in redexes { - let rdex0 = net_tree_to_hvmc_tree(inet, root0, &mut port_to_var_id); - let rdex1 = net_tree_to_hvmc_tree(inet, root1, &mut port_to_var_id); - rdex.push((rdex0, rdex1)); + let mut redexes = vec![]; + for [root0, root1] in net_redexes { + let root0 = net_tree_to_hvmc_tree(inet, root0, &mut port_to_var_id); + let root1 = net_tree_to_hvmc_tree(inet, root1, &mut port_to_var_id); + redexes.push((root0, root1)); } - Ok(Net { root, rdex }) + Ok(Net { root, redexes }) } fn net_tree_to_hvmc_tree(inet: &INet, tree_root: NodeId, port_to_var_id: &mut HashMap) -> Tree { From 1880c8c8f261f9c47f25c76d84db4c2b3adb1c45 Mon Sep 17 00:00:00 2001 From: tjjfvi Date: Thu, 29 Feb 2024 10:45:26 -0500 Subject: [PATCH 2/2] fix test memory sizes --- tests/golden_tests.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs index 6b6b28beb..e4e54c347 100644 --- a/tests/golden_tests.rs +++ b/tests/golden_tests.rs @@ -143,14 +143,14 @@ fn run_file() { let book = do_parse_book(code, path)?; // 1 million nodes for the test runtime. Smaller doesn't seem to make it any faster let (res, info) = - run_book(book, 1 << 20, RunOpts::lazy(), WarningOpts::deny_all(), CompileOpts::heavy())?; + run_book(book, 1 << 24, RunOpts::lazy(), WarningOpts::deny_all(), CompileOpts::heavy())?; Ok(format!("{}{}", display_readback_errors(&info.readback_errors), res)) }), (&|code, path| { let book = do_parse_book(code, path)?; // 1 million nodes for the test runtime. Smaller doesn't seem to make it any faster let (res, info) = - run_book(book, 1 << 20, RunOpts::default(), WarningOpts::deny_all(), CompileOpts::heavy())?; + run_book(book, 1 << 24, RunOpts::default(), WarningOpts::deny_all(), CompileOpts::heavy())?; Ok(format!("{}{}", display_readback_errors(&info.readback_errors), res)) }), ]) @@ -166,7 +166,7 @@ fn run_lazy() { desugar_opts.lazy_mode(); // 1 million nodes for the test runtime. Smaller doesn't seem to make it any faster - let (res, info) = run_book(book, 1 << 20, run_opts, WarningOpts::deny_all(), desugar_opts)?; + let (res, info) = run_book(book, 1 << 24, run_opts, WarningOpts::deny_all(), desugar_opts)?; Ok(format!("{}{}", display_readback_errors(&info.readback_errors), res)) }) } @@ -299,7 +299,7 @@ fn run_entrypoint() { book.entrypoint = Some(Name::from("foo")); // 1 million nodes for the test runtime. Smaller doesn't seem to make it any faster let (res, info) = - run_book(book, 1 << 20, RunOpts::default(), WarningOpts::deny_all(), CompileOpts::heavy())?; + run_book(book, 1 << 24, RunOpts::default(), WarningOpts::deny_all(), CompileOpts::heavy())?; Ok(format!("{}{}", display_readback_errors(&info.readback_errors), res)) }) }