From ecb213e91b9b92261f394da8466faa1ccb74d135 Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Tue, 5 Mar 2024 20:37:20 +0100 Subject: [PATCH] [sc-495][sc-494] Update for new hvmc num ops and pre_reduce --- Cargo.lock | 23 +++--- src/hvmc_net/mod.rs | 1 - src/hvmc_net/pre_reduce.rs | 71 ------------------- src/hvmc_net/prune.rs | 5 +- src/lib.rs | 11 +-- src/net/hvmc_to_net.rs | 20 ++---- src/net/net_to_hvmc.rs | 8 +-- src/term/display.rs | 33 +++++---- src/term/mod.rs | 37 +++++----- src/term/net_to_term.rs | 53 +++++++++----- src/term/parser/parser.rs | 33 +++++---- src/term/term_to_net.rs | 33 +++++---- .../run_file__lam_op2_nested.hvm.snap | 2 +- 13 files changed, 129 insertions(+), 201 deletions(-) delete mode 100644 src/hvmc_net/pre_reduce.rs diff --git a/Cargo.lock b/Cargo.lock index 7fcae8bcb..607411317 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,9 +4,9 @@ version = 3 [[package]] name = "ahash" -version = "0.8.10" +version = "0.8.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8b79b82693f705137f8fb9b37871d99e4f9a7df12b917eed79c3d3954830a60b" +checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011" dependencies = [ "cfg-if", "once_cell", @@ -70,9 +70,9 @@ checksum = "3a8241f3ebb85c056b509d4327ad0358fbbba6ffb340bf388f26350aeda225b1" [[package]] name = "cc" -version = "1.0.88" +version = "1.0.89" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "02f341c093d19155a6e41631ce5971aac4e9a868262212153124c15fa22d1cdc" +checksum = "a0ba8f7aaa012f30d5b2861462f6708eccd49c3c39863fe083a308035f63d723" [[package]] name = "cfg-if" @@ -202,10 +202,11 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03" [[package]] name = "hvm-core" version = "0.2.19" -source = "git+https://github.com/HigherOrderCO/hvm-core#0433f52cd51f3b9c8db3630bf338d378d5b2908d" +source = "git+https://github.com/HigherOrderCO/hvm-core#32f80ba12145a318d6c84047576c4b4cd01a1760" dependencies = [ "clap", "nohash-hasher", + "stacker", ] [[package]] @@ -228,9 +229,9 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.2.4" +version = "2.2.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "967d6dd42f16dbf0eb8040cb9e477933562684d3918f7d253f2ff9087fb3e7a3" +checksum = "7b0b929d511467233429c45a44ac1dcaa21ba0f5ba11e4879e6ed28ddb4f9df4" dependencies = [ "equivalent", "hashbrown 0.14.3", @@ -238,9 +239,9 @@ dependencies = [ [[package]] name = "insta" -version = "1.35.1" +version = "1.36.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7c985c1bef99cf13c58fade470483d81a2bfe846ebde60ed28cc2dddec2df9e2" +checksum = "0a7c22c4d34ef4788c351e971c52bfdfe7ea2766f8c5466bc175dd46e52ac22e" dependencies = [ "console", "lazy_static", @@ -431,9 +432,9 @@ checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" [[package]] name = "walkdir" -version = "2.4.0" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d71d857dc86794ca4c280d616f7da00d2dbfd8cd788846559a6813e6aa4b54ee" +checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b" dependencies = [ "same-file", "winapi-util", diff --git a/src/hvmc_net/mod.rs b/src/hvmc_net/mod.rs index e5032db29..570504b6a 100644 --- a/src/hvmc_net/mod.rs +++ b/src/hvmc_net/mod.rs @@ -1,2 +1 @@ -pub mod pre_reduce; pub mod prune; diff --git a/src/hvmc_net/pre_reduce.rs b/src/hvmc_net/pre_reduce.rs deleted file mode 100644 index 2f4e4e831..000000000 --- a/src/hvmc_net/pre_reduce.rs +++ /dev/null @@ -1,71 +0,0 @@ -// Reduce the compiled networks, solving any annihilations and commutations. -// This is a useful optimization on its own, but also required by an hvm-core optimization. - -use std::sync::Mutex; - -use hvmc::{ast::Book, dispatch_dyn_net, host::Host, run::Def}; - -use crate::CORE_BUILTINS; -use hvmc::run::Port; - -/// A Def that pushes all interactions to its inner Vec. -struct InertDef(Mutex>); - -impl hvmc::run::AsDef for InertDef { - unsafe fn call( - def: *const hvmc::run::Def, - _: &mut hvmc::run::Net, - port: Port, - ) { - let def = unsafe { &*def }; - def.data.0.lock().unwrap().push((Port::new_ref(def), port)); - } -} - -/// Reduces the definitions in the book individually, except for main. -/// -/// It does not reduce interactions that use builtin defs, as they are -/// assumed to be side-effectful -pub fn pre_reduce_book(book: &mut Book, entrypoint: &str) -> Result<(), String> { - /// Maximum amount of rewrites that - const MAX_RWTS: usize = 100_000; - // Create a host - // with inert definitions in the place - // of core builtins, to prevent them from being reduced - let mut host = Host::default(); - for builtin in CORE_BUILTINS { - let def = InertDef(Default::default()); - host.insert_def(builtin, hvmc::host::DefRef::Owned(Box::new(Def::new(hvmc::run::LabSet::ALL, def)))); - } - host.insert_book(book); - - for (nam, net) in book.iter_mut() { - // Skip unnecessary work - if net.redexes.is_empty() || *nam == entrypoint { - continue; - } - - 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.")); - rt.expand(); - rt.reduce(MAX_RWTS); - }); - - // 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.redexes.extend(core::mem::take(&mut *stored_redexes)); - }) - } - } - // Place the reduced net back into the def map - dispatch_dyn_net!(&mut rt => { - *net = host.readback(rt); - }); - } - Ok(()) -} diff --git a/src/hvmc_net/prune.rs b/src/hvmc_net/prune.rs index 76d4904a0..7a1c2f4aa 100644 --- a/src/hvmc_net/prune.rs +++ b/src/hvmc_net/prune.rs @@ -27,13 +27,10 @@ fn used_defs_in_tree(tree: &Tree, used_defs: &mut HashSet, to_visit: &mu to_visit.push(nam.clone()); } } - Tree::Ctr { lft, rgt, .. } | Tree::Op2 { lft, rgt, .. } | Tree::Mat { sel: lft, ret: rgt } => { + Tree::Ctr { lft, rgt, .. } | Tree::Op { rhs: lft, out: rgt, .. } | Tree::Mat { sel: lft, ret: rgt } => { used_defs_in_tree(lft, used_defs, to_visit); used_defs_in_tree(rgt, used_defs, to_visit); } - Tree::Op1 { rgt, .. } => { - used_defs_in_tree(rgt, used_defs, to_visit); - } Tree::Var { .. } | Tree::Num { .. } | Tree::Era => (), } } diff --git a/src/lib.rs b/src/lib.rs index 60b035f59..8bb5723c6 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -9,7 +9,7 @@ use hvmc::{ run::{DynNet, Heap, Rewrites}, stdlib::LogDef, }; -use hvmc_net::{pre_reduce::pre_reduce_book, prune::prune_defs}; +use hvmc_net::prune::prune_defs; use net::{hvmc_to_net::hvmc_to_net, net_to_hvmc::nets_to_hvmc}; use std::{ str::FromStr, @@ -99,7 +99,7 @@ pub fn compile_book( let mut core_book = nets_to_hvmc(nets)?; if opts.pre_reduce { - pre_reduce_book(&mut core_book, book.hvmc_entrypoint())?; + core_book.pre_reduce(&|x| x == book.hvmc_entrypoint(), 1 << 24, 100_000)?; } if opts.prune { prune_defs(&mut core_book, book.hvmc_entrypoint().to_string()); @@ -220,14 +220,15 @@ pub fn count_nodes<'l>(net: &'l hvmc::ast::Net) -> usize { } while let Some(tree) = visit.pop() { match tree { - ast::Tree::Ctr { lft, rgt, .. } | ast::Tree::Op2 { lft, rgt, .. } => { + ast::Tree::Ctr { lft, rgt, .. } => { count += 1; visit.push(lft); visit.push(rgt); } - ast::Tree::Op1 { rgt, .. } => { + ast::Tree::Op { rhs, out, .. } => { count += 1; - visit.push(rgt); + visit.push(rhs); + visit.push(out); } ast::Tree::Mat { sel, ret } => { count += 1; diff --git a/src/net/hvmc_to_net.rs b/src/net/hvmc_to_net.rs index 2257580f5..11ffc9a8b 100644 --- a/src/net/hvmc_to_net.rs +++ b/src/net/hvmc_to_net.rs @@ -85,21 +85,11 @@ fn tree_to_inodes(tree: &Tree, tree_root: String, net_root: &str, n_vars: &mut N let var = new_var(n_vars); inodes.push(INode { kind, ports: [subtree_root, var.clone(), var] }); } - Tree::Op1 { opr, lft, rgt } => { - // Add port 1 as a new Num node. - let lft_name = new_var(n_vars); - let num_name = new_var(n_vars); - inodes.push(INode { kind: Num { val: *lft }, ports: [lft_name.clone(), num_name.clone(), num_name] }); - // Swap ports 0 and 1 and transform into OP2. - let kind = Op2 { opr: *opr }; - let rgt = process_node_subtree(rgt, net_root, &mut subtrees, n_vars); - inodes.push(INode { kind, ports: [lft_name, subtree_root, rgt] }); - } - Tree::Op2 { opr, lft, rgt } => { - let kind = Op2 { opr: *opr }; - 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, ports: [subtree_root, lft, rgt] }); + Tree::Op { op, rhs, out } => { + let kind = Op2 { opr: *op }; + let rhs = process_node_subtree(rhs, net_root, &mut subtrees, n_vars); + let out = process_node_subtree(out, net_root, &mut subtrees, n_vars); + inodes.push(INode { kind, ports: [subtree_root, rhs, out] }); } Tree::Mat { sel, ret } => { let kind = Mat; diff --git a/src/net/net_to_hvmc.rs b/src/net/net_to_hvmc.rs index 8eeefb164..8c0471ef7 100644 --- a/src/net/net_to_hvmc.rs +++ b/src/net/net_to_hvmc.rs @@ -61,10 +61,10 @@ fn net_tree_to_hvmc_tree(inet: &INet, tree_root: NodeId, port_to_var_id: &mut Ha }, NodeKind::Ref { def_name } => Tree::Ref { nam: def_name.to_string() }, NodeKind::Num { val } => Tree::Num { val: *val }, - NodeKind::Op2 { opr } => Tree::Op2 { - opr: *opr, - lft: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id)), - rgt: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id)), + NodeKind::Op2 { opr } => Tree::Op { + op: *opr, + rhs: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id)), + out: Box::new(var_or_subtree(inet, Port(tree_root, 2), port_to_var_id)), }, NodeKind::Mat => Tree::Mat { sel: Box::new(var_or_subtree(inet, Port(tree_root, 1), port_to_var_id)), diff --git a/src/term/display.rs b/src/term/display.rs index 225f1ed49..9ba9e258b 100644 --- a/src/term/display.rs +++ b/src/term/display.rs @@ -151,23 +151,22 @@ impl fmt::Display for NumCtr { impl fmt::Display for Op { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - Op::ADD => write!(f, "+"), - Op::SUB => write!(f, "-"), - Op::MUL => write!(f, "*"), - Op::DIV => write!(f, "/"), - Op::MOD => write!(f, "%"), - Op::EQ => write!(f, "=="), - Op::NE => write!(f, "!="), - Op::LT => write!(f, "<"), - Op::GT => write!(f, ">"), - Op::LTE => write!(f, "<="), - Op::GTE => write!(f, ">="), - Op::AND => write!(f, "&"), - Op::OR => write!(f, "|"), - Op::XOR => write!(f, "^"), - Op::LSH => write!(f, "<<"), - Op::RSH => write!(f, ">>"), - Op::NOT => write!(f, "~"), + Op::Add => write!(f, "+"), + Op::Sub => write!(f, "-"), + Op::Mul => write!(f, "*"), + Op::Div => write!(f, "/"), + Op::Mod => write!(f, "%"), + Op::Eq => write!(f, "=="), + Op::Ne => write!(f, "!="), + Op::Lt => write!(f, "<"), + Op::Gt => write!(f, ">"), + Op::Lte => write!(f, "<="), + Op::Gte => write!(f, ">="), + Op::And => write!(f, "&"), + Op::Or => write!(f, "|"), + Op::Xor => write!(f, "^"), + Op::Shl => write!(f, "<<"), + Op::Shr => write!(f, ">>"), } } } diff --git a/src/term/mod.rs b/src/term/mod.rs index a5c1a5b45..ca54d68c3 100644 --- a/src/term/mod.rs +++ b/src/term/mod.rs @@ -163,23 +163,22 @@ pub enum Tag { #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum Op { - ADD, - SUB, - MUL, - DIV, - MOD, - EQ, - NE, - LT, - GT, - LTE, - GTE, - AND, - OR, - XOR, - LSH, - RSH, - NOT, + Add, + Sub, + Mul, + Div, + Mod, + Eq, + Ne, + Lt, + Gt, + Lte, + Gte, + And, + Or, + Xor, + Shl, + Shr, } /// Pattern types. @@ -387,7 +386,7 @@ impl Term { if val == 0 { arg } else { - Term::Opx { op: Op::SUB, fst: Box::new(arg), snd: Box::new(Term::Num { val }) } + Term::Opx { op: Op::Sub, fst: Box::new(arg), snd: Box::new(Term::Num { val }) } } } @@ -395,7 +394,7 @@ impl Term { if val == 0 { arg } else { - Term::Opx { op: Op::ADD, fst: Box::new(arg), snd: Box::new(Term::Num { val }) } + Term::Opx { op: Op::Add, fst: Box::new(arg), snd: Box::new(Term::Num { val }) } } } diff --git a/src/term/net_to_term.rs b/src/term/net_to_term.rs index e2fecfbc9..38b794c60 100644 --- a/src/term/net_to_term.rs +++ b/src/term/net_to_term.rs @@ -186,8 +186,8 @@ impl<'a> Reader<'a> { 2 => { let fst = self.read_term(self.net.enter_port(Port(node, 0))); let snd = self.read_term(self.net.enter_port(Port(node, 1))); - - Term::Opx { op: Op::from_hvmc_label(*opr), fst: Box::new(fst), snd: Box::new(snd) } + let (opr, fst, snd) = if is_op_swapped(*opr) { (opr.swap(), snd, fst) } else { (*opr, fst, snd) }; + Term::Opx { op: Op::from_hvmc_label(opr), fst: Box::new(fst), snd: Box::new(snd) } } _ => { self.error(ReadbackError::InvalidNumericOp); @@ -437,27 +437,42 @@ impl Op { pub fn from_hvmc_label(value: hvmc::ops::Op) -> Op { use hvmc::ops::Op as RtOp; match value { - RtOp::Add => Op::ADD, - RtOp::Sub => Op::SUB, - RtOp::Mul => Op::MUL, - RtOp::Div => Op::DIV, - RtOp::Mod => Op::MOD, - RtOp::Eq => Op::EQ, - RtOp::Ne => Op::NE, - RtOp::Lt => Op::LT, - RtOp::Gt => Op::GT, - RtOp::Lte => Op::LTE, - RtOp::Gte => Op::GTE, - RtOp::And => Op::AND, - RtOp::Or => Op::OR, - RtOp::Xor => Op::XOR, - RtOp::Lsh => Op::LSH, - RtOp::Rsh => Op::RSH, - RtOp::Not => Op::NOT, + RtOp::Add => Op::Add, + RtOp::Sub => Op::Sub, + RtOp::Mul => Op::Mul, + RtOp::Div => Op::Div, + RtOp::Mod => Op::Mod, + RtOp::Eq => Op::Eq, + RtOp::Ne => Op::Ne, + RtOp::Lt => Op::Lt, + RtOp::Gt => Op::Gt, + RtOp::Lte => Op::Lte, + RtOp::Gte => Op::Gte, + RtOp::And => Op::And, + RtOp::Or => Op::Or, + RtOp::Xor => Op::Xor, + RtOp::Shl => Op::Shl, + RtOp::Shr => Op::Shr, + RtOp::SubS => unreachable!(), + RtOp::DivS => unreachable!(), + RtOp::ModS => unreachable!(), + RtOp::ShlS => unreachable!(), + RtOp::ShrS => unreachable!(), } } } +fn is_op_swapped(op: hvmc::ops::Op) -> bool { + matches!( + op, + hvmc::ops::Op::ShlS + | hvmc::ops::Op::ShrS + | hvmc::ops::Op::SubS + | hvmc::ops::Op::DivS + | hvmc::ops::Op::ModS + ) +} + #[derive(Debug)] pub enum ReadbackError { InvalidNumericMatch, diff --git a/src/term/parser/parser.rs b/src/term/parser/parser.rs index 11d26f9f2..f48f1c06f 100644 --- a/src/term/parser/parser.rs +++ b/src/term/parser/parser.rs @@ -174,23 +174,22 @@ where I: ValueInput<'a, Token = Token, Span = SimpleSpan>, { select! { - Token::Add => Op::ADD, - Token::Sub => Op::SUB, - Token::Asterisk => Op::MUL, - Token::Div => Op::DIV, - Token::Mod => Op::MOD, - Token::EqualsEquals => Op::EQ, - Token::NotEquals => Op::NE, - Token::Ltn => Op::LT, - Token::Gtn => Op::GT, - Token::Lte => Op::LTE, - Token::Gte => Op::GTE, - Token::And => Op::AND, - Token::Or => Op::OR, - Token::Xor => Op::XOR, - Token::Tilde => Op::NOT, - Token::Shl => Op::LSH, - Token::Shr => Op::RSH, + Token::Add => Op::Add, + Token::Sub => Op::Sub, + Token::Asterisk => Op::Mul, + Token::Div => Op::Div, + Token::Mod => Op::Mod, + Token::EqualsEquals => Op::Eq, + Token::NotEquals => Op::Ne, + Token::Ltn => Op::Lt, + Token::Gtn => Op::Gt, + Token::Lte => Op::Lte, + Token::Gte => Op::Gte, + Token::And => Op::And, + Token::Or => Op::Or, + Token::Xor => Op::Xor, + Token::Shl => Op::Shl, + Token::Shr => Op::Shr, } } diff --git a/src/term/term_to_net.rs b/src/term/term_to_net.rs index 573f57d96..6c24f6f6b 100644 --- a/src/term/term_to_net.rs +++ b/src/term/term_to_net.rs @@ -312,23 +312,22 @@ impl Op { pub fn to_hvmc_label(self) -> hvmc::ops::Op { use hvmc::ops::Op as RtOp; match self { - Op::ADD => RtOp::Add, - Op::SUB => RtOp::Sub, - Op::MUL => RtOp::Mul, - Op::DIV => RtOp::Div, - Op::MOD => RtOp::Mod, - Op::EQ => RtOp::Eq, - Op::NE => RtOp::Ne, - Op::LT => RtOp::Lt, - Op::GT => RtOp::Gt, - Op::LTE => RtOp::Lte, - Op::GTE => RtOp::Gte, - Op::AND => RtOp::And, - Op::OR => RtOp::Or, - Op::XOR => RtOp::Xor, - Op::LSH => RtOp::Lsh, - Op::RSH => RtOp::Rsh, - Op::NOT => RtOp::Not, + Op::Add => RtOp::Add, + Op::Sub => RtOp::Sub, + Op::Mul => RtOp::Mul, + Op::Div => RtOp::Div, + Op::Mod => RtOp::Mod, + Op::Eq => RtOp::Eq, + Op::Ne => RtOp::Ne, + Op::Lt => RtOp::Lt, + Op::Gt => RtOp::Gt, + Op::Lte => RtOp::Lte, + Op::Gte => RtOp::Gte, + Op::And => RtOp::And, + Op::Or => RtOp::Or, + Op::Xor => RtOp::Xor, + Op::Shl => RtOp::Shl, + Op::Shr => RtOp::Shr, } } } diff --git a/tests/snapshots/run_file__lam_op2_nested.hvm.snap b/tests/snapshots/run_file__lam_op2_nested.hvm.snap index 303f9dab3..641835492 100644 --- a/tests/snapshots/run_file__lam_op2_nested.hvm.snap +++ b/tests/snapshots/run_file__lam_op2_nested.hvm.snap @@ -2,4 +2,4 @@ source: tests/golden_tests.rs input_file: tests/golden_tests/run_file/lam_op2_nested.hvm --- -λa (+ (* a a) (+ (+ 2 a) 3)) +λa (+ (* a a) (+ (+ a 2) 3))