From 846b823270627eb223eb85f59647a0b33d8b5d6c Mon Sep 17 00:00:00 2001 From: Nicolas Abril Date: Thu, 7 Sep 2023 21:26:20 +0200 Subject: [PATCH] Add readback of results from HVM; Refactor CLI mode --- src/ast/compat.rs | 81 ++++++ src/ast/hvm_lang.rs | 17 +- src/ast/mod.rs | 2 +- src/from_core/mod.rs | 234 ++++++++++++++++++ src/lib.rs | 48 +++- src/main.rs | 71 +++--- src/to_core/affine.rs | 2 + src/to_core/compat_net.rs | 91 ++----- tests/golden_tests.rs | 10 +- .../compile_single_files/bool.golden | 10 +- .../compile_single_files/ex0.golden | 16 +- .../compile_single_files/ex2.golden | 58 ++--- .../var_shadows_ref.golden | 6 +- .../compile_single_terms/church_one.golden | 6 +- .../compile_single_terms/church_zero.golden | 2 +- .../compile_single_terms/dup_apply.golden | 2 +- .../compile_single_terms/erased_dup.golden | 2 +- .../compile_single_terms/id.golden | 2 +- .../compile_single_terms/infer_dup.golden | 2 +- .../golden_tests/run_single_files/add.golden | 2 +- .../golden_tests/run_single_files/example.hvm | 24 ++ 21 files changed, 511 insertions(+), 177 deletions(-) create mode 100644 src/ast/compat.rs create mode 100644 src/from_core/mod.rs create mode 100644 tests/golden_tests/run_single_files/example.hvm diff --git a/src/ast/compat.rs b/src/ast/compat.rs new file mode 100644 index 00000000..48a6ac48 --- /dev/null +++ b/src/ast/compat.rs @@ -0,0 +1,81 @@ +use crate::ast::core::Tag; + +// TODO: Refactor to not use this intermediate form + +#[derive(Clone, Debug)] +/// Net representation used only as an intermediate for converting to hvm-core format +pub struct INet { + pub nodes: Vec, +} + +pub type NodeVal = u64; +pub type NodeKind = NodeVal; +pub type Port = NodeVal; +pub type NodeId = NodeVal; +pub type SlotId = NodeVal; + +/// The ROOT port is on the deadlocked root node at address 0. +pub const ROOT: Port = 1; +pub const TAG_WIDTH: u32 = Tag::BITS; +pub const TAG: u32 = 64 - TAG_WIDTH; +pub const ERA: NodeKind = 0 << TAG; +pub const CON: NodeKind = 1 << TAG; +pub const DUP: NodeKind = 2 << TAG; +pub const REF: NodeKind = 3 << TAG; +pub const NUM: NodeKind = 4 << TAG; +pub const NUMOP: NodeKind = 5 << TAG; +pub const LABEL_MASK: NodeKind = (1 << TAG) - 1; +pub const TAG_MASK: NodeKind = !LABEL_MASK; + +/// Create a new net, with a deadlocked root node. +pub fn new_inet() -> INet { + INet { + nodes: vec![2, 1, 0, ERA], // p2 points to p0, p1 points to net + } +} + +/// Allocates a new node, reclaiming a freed space if possible. +pub fn new_node(inet: &mut INet, kind: NodeKind) -> NodeId { + let node = addr(inet.nodes.len() as Port); + inet.nodes.extend([port(node, 0), port(node, 1), port(node, 2), kind]); + node +} + +/// Builds a port (an address / slot pair). +pub fn port(node: NodeId, slot: SlotId) -> Port { + (node << 2) | slot +} + +/// Returns the address of a port (TODO: rename). +pub fn addr(port: Port) -> NodeId { + port >> 2 +} + +/// Returns the slot of a port. +pub fn slot(port: Port) -> SlotId { + port & 3 +} + +/// Enters a port, returning the port on the other side. +pub fn enter(inet: &INet, port: Port) -> Port { + inet.nodes[port as usize] +} + +/// Kind of the node. +pub fn kind(inet: &INet, node: NodeId) -> NodeKind { + inet.nodes[port(node, 3) as usize] +} + +/// Links two ports. +pub fn link(inet: &mut INet, ptr_a: Port, ptr_b: Port) { + inet.nodes[ptr_a as usize] = ptr_b; + inet.nodes[ptr_b as usize] = ptr_a; +} + +#[derive(Debug)] +pub struct INode { + pub kind: NodeKind, + pub ports: [String; 3], +} + +pub type INodes = Vec; diff --git a/src/ast/hvm_lang.rs b/src/ast/hvm_lang.rs index db7fe9a3..bcdd6875 100644 --- a/src/ast/hvm_lang.rs +++ b/src/ast/hvm_lang.rs @@ -36,6 +36,8 @@ pub enum Term { Dup { fst: Name, snd: Name, val: Box, nxt: Box }, Num { val: Number }, NumOp { op: NumOper, fst: Box, snd: Box }, + Sup { fst: Box, snd: Box }, + Era, } // TODO: Switch to the hvm2 type when it's done @@ -120,6 +122,17 @@ impl From for OP { } } +impl From<&OP> for NumOper { + fn from(value: &OP) -> Self { + match value { + OP::ADD => NumOper::Add, + OP::MUL => NumOper::Mul, + OP::DIV => NumOper::Div, + OP::SUB => NumOper::Sub, + } + } +} + impl DefinitionBook { pub fn new() -> Self { Default::default() @@ -170,6 +183,8 @@ impl fmt::Display for Term { Term::Dup { fst, snd, val, nxt } => write!(f, "dup {fst} {snd} = {val}; {nxt}"), Term::Num { val } => write!(f, "{val}"), Term::NumOp { op, fst, snd } => write!(f, "({op} {fst} {snd})"), + Term::Sup { fst, snd } => write!(f, "{{{fst} {snd}}}"), + Term::Era => write!(f, "*"), } } } @@ -183,7 +198,7 @@ impl fmt::Display for Pattern { impl fmt::Display for Rule { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let Rule { name, pats, body } = self; - writeln!(f, "({}{}) = {}", name, pats.into_iter().map(|x| format!(" {x}")).join(""), body) + writeln!(f, "({}{}) = {}", name, pats.iter().map(|x| format!(" {x}")).join(""), body) } } diff --git a/src/ast/mod.rs b/src/ast/mod.rs index 11513931..8af2dd0a 100644 --- a/src/ast/mod.rs +++ b/src/ast/mod.rs @@ -1,6 +1,6 @@ +pub mod compat; pub mod core; pub mod hvm_lang; -pub mod compat; pub use hvm_lang::{Definition, DefinitionBook, NumOper, Rule, Term}; diff --git a/src/from_core/mod.rs b/src/from_core/mod.rs new file mode 100644 index 00000000..337d2126 --- /dev/null +++ b/src/from_core/mod.rs @@ -0,0 +1,234 @@ +use std::collections::{HashMap, HashSet}; + +use crate::ast::{ + compat::{ + addr, enter, kind, link, new_inet, new_node, port, slot, INet, INode, INodes, NodeId, NodeKind, Port, + SlotId, CON, DUP, ERA, LABEL_MASK, NUM, NUMOP, REF, ROOT, TAG_MASK, + }, + Name, NumOper, Number, Term, +}; +use hvm2::lang::{u64_to_name, LNet, LTree}; + +pub fn readback_net(net: &LNet) -> anyhow::Result { + let core_net = core_net_to_compat(net)?; + let term = readback_compat(&core_net); + Ok(term) +} + +fn core_net_to_compat(net: &LNet) -> anyhow::Result { + let mut inodes = vec![]; + let mut n_vars = 0; + let net_root = if let LTree::Var { nam } = &net.root { nam } else { "" }; + + if !matches!(&net.root, LTree::Var { .. }) { + let mut root = tree_to_inodes(&net.root, "_".to_string(), net_root, &mut n_vars); + inodes.append(&mut root); + } + + for (i, (tree1, tree2)) in net.acts.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); + let mut tree2 = tree_to_inodes(tree2, tree_root, net_root, &mut n_vars); + inodes.append(&mut tree2); + } + + let compat_net = inodes_to_inet(&inodes); + Ok(compat_net) +} + +fn new_var(n_vars: &mut NodeId) -> String { + let new_var = format!("x{n_vars}"); + *n_vars += 1; + new_var +} + +fn tree_to_inodes(tree: <ree, tree_root: String, net_root: &str, n_vars: &mut NodeId) -> INodes { + fn process_node_subtree<'a>( + subtree: &'a LTree, + net_root: &str, + subtrees: &mut Vec<(String, &'a LTree)>, + n_vars: &mut NodeId, + ) -> String { + if let LTree::Var { nam } = subtree { + if nam == net_root { "_".to_string() } else { nam.clone() } + } else { + let var = new_var(n_vars); + subtrees.push((var.clone(), subtree)); + var + } + } + + let mut inodes = vec![]; + let mut subtrees = vec![(tree_root, tree)]; + while let Some((subtree_root, subtree)) = subtrees.pop() { + match subtree { + LTree::Era => { + let var = new_var(n_vars); + inodes.push(INode { kind: ERA, ports: [subtree_root, var.clone(), var] }); + } + LTree::Nod { tag, lft, rgt } => { + let kind = if *tag == hvm2::core::CON { CON } else { DUP | (*tag - hvm2::core::DUP) as NodeKind }; + let var_lft = process_node_subtree(lft, net_root, &mut subtrees, n_vars); + let var_rgt = process_node_subtree(rgt, net_root, &mut subtrees, n_vars); + inodes.push(INode { kind, ports: [subtree_root, var_lft, var_rgt] }) + } + LTree::Var { .. } => unreachable!(), + LTree::Ref { nam } => { + let kind = REF | (*nam as NodeKind); + let var = new_var(n_vars); + inodes.push(INode { kind, ports: [subtree_root, var.clone(), var] }); + } + LTree::NUM { val } => { + let kind = NUM | (*val as NodeKind); + let var = new_var(n_vars); + inodes.push(INode { kind, ports: [subtree_root, var.clone(), var] }); + } + LTree::Opx { opx, lft, rgt } => { + let kind = NUMOP | u8::from(NumOper::from(opx)) as NodeKind; + let var_lft = process_node_subtree(lft, net_root, &mut subtrees, n_vars); + let var_rgt = process_node_subtree(rgt, net_root, &mut subtrees, n_vars); + inodes.push(INode { kind, ports: [subtree_root, var_lft, var_rgt] }) + } + } + } + inodes +} + +// Converts INodes to an INet by linking ports based on names. +fn inodes_to_inet(inodes: &INodes) -> INet { + let mut inet = new_inet(); + let mut name_map = std::collections::HashMap::new(); + + for inode in inodes.iter() { + let node = new_node(&mut inet, inode.kind); + for (j, name) in inode.ports.iter().enumerate() { + let p = port(node, j as SlotId); + if name == "_" { + link(&mut inet, p, ROOT); + } else if let Some(&q) = name_map.get(name) { + link(&mut inet, p, q); + name_map.remove(name); + } else { + name_map.insert(name.clone(), p); + } + } + } + + inet +} + +// Converts an Interaction-INet node to an Interaction Calculus term. +fn readback_compat(net: &INet) -> Term { + // Given a port, returns its name, or assigns one if it wasn't named yet. + fn name_of(net: &INet, var_port: Port, var_name: &mut HashMap) -> Name { + // If port is linked to an erase node, return an unused variable + if kind(net, addr(enter(net, var_port))) == ERA { + return Name("*".to_string()); + } + if !var_name.contains_key(&var_port) { + let nam = Name(u64_to_name(var_name.len() as u64 + 1)); + var_name.insert(var_port, nam.clone()); + } + var_name.get(&var_port).unwrap().clone() + } + + // Reads a term recursively by starting at root node. + fn reader( + net: &INet, + next: Port, + var_name: &mut HashMap, + dups_vec: &mut Vec, + dups_set: &mut HashSet, + seen: &mut HashSet, + ) -> Term { + if seen.contains(&next) { + return Term::Var { nam: Name("...".to_string()) }; + } + + seen.insert(next); + + let kind_ = kind(net, addr(next)); + let tag = kind_ & TAG_MASK; + let label = kind_ & LABEL_MASK; + + match tag { + // If we're visiting a set... + ERA => Term::Era, + // If we're visiting a con node... + CON => match slot(next) { + // If we're visiting a port 0, then it is a lambda. + 0 => { + let nam = name_of(net, port(addr(next), 1), var_name); + let prt = enter(net, port(addr(next), 2)); + let bod = reader(net, prt, var_name, dups_vec, dups_set, seen); + Term::Lam { nam, bod: Box::new(bod) } + } + // If we're visiting a port 1, then it is a variable. + 1 => { + Term::Var { nam: name_of(net, next, var_name) } + //Var{nam: format!("{}@{}", String::from_utf8_lossy(&name_of(net, next, var_name)), addr(next)).into()} + } + // If we're visiting a port 2, then it is an application. + _ => { + let prt = enter(net, port(addr(next), 0)); + let fun = reader(net, prt, var_name, dups_vec, dups_set, seen); + let prt = enter(net, port(addr(next), 1)); + let arg = reader(net, prt, var_name, dups_vec, dups_set, seen); + Term::App { fun: Box::new(fun), arg: Box::new(arg) } + } + }, + REF => Term::Var { nam: Name(u64_to_name(label)) }, + // If we're visiting a fan node... + DUP => match slot(next) { + // If we're visiting a port 0, then it is a pair. + 0 => { + let prt = enter(net, port(addr(next), 1)); + let fst = reader(net, prt, var_name, dups_vec, dups_set, seen); + let prt = enter(net, port(addr(next), 2)); + let snd = reader(net, prt, var_name, dups_vec, dups_set, seen); + Term::Sup { fst: Box::new(fst), snd: Box::new(snd) } + } + // If we're visiting a port 1 or 2, then it is a variable. + // Also, that means we found a dup, so we store it to read later. + _ => { + if !dups_set.contains(&addr(next)) { + dups_set.insert(addr(next)); + dups_vec.push(addr(next)); + } + //Var{nam: format!("{}@{}", String::from_utf8_lossy(&name_of(net, next, var_name)), addr(next)).into()} + Term::Var { nam: name_of(net, next, var_name) } + } + }, + NUM => Term::Num { val: Number(label) }, + NUMOP => todo!(), + _ => unreachable!(), + } + } + + // A hashmap linking ports to binder names. Those ports have names: + // Port 1 of a con node (λ), ports 1 and 2 of a fan node (let). + let mut binder_name = HashMap::new(); + + // Dup aren't scoped. We find them when we read one of the variables + // introduced by them. Thus, we must store the dups we find to read later. + // We have a vec for .pop(). and a set to avoid storing duplicates. + let mut dups_vec = Vec::new(); + let mut dups_set = HashSet::new(); + let mut seen = HashSet::new(); + + // Reads the main term from the net + let mut main = reader(net, enter(net, ROOT), &mut binder_name, &mut dups_vec, &mut dups_set, &mut seen); + + // Reads let founds by starting the reader function from their 0 ports. + while let Some(dup) = dups_vec.pop() { + let val = + reader(net, enter(net, port(dup, 0)), &mut binder_name, &mut dups_vec, &mut dups_set, &mut seen); + let fst = name_of(net, port(dup, 1), &mut binder_name); + let snd = name_of(net, port(dup, 2), &mut binder_name); + let val = Box::new(val); + let nxt = Box::new(main); + main = Term::Dup { fst, snd, val, nxt }; + } + main +} diff --git a/src/lib.rs b/src/lib.rs index 85ba43e6..10ad8963 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,7 +1,53 @@ #![feature(slice_group_by)] pub mod ast; +pub mod from_core; pub mod loader; pub mod parser; pub mod to_core; -pub mod from_core; + +use ast::{core::Book, DefinitionBook, Term}; +use from_core::readback_net; +use hvm2::lang::{readback_lnet, LNet}; +use std::time::Instant; + +pub use loader::load_file_to_book; + +pub fn check_book(book: &DefinitionBook) -> anyhow::Result<()> { + // TODO: Do the checks without having to do full compilation + compile_book(book)?; + Ok(()) +} + +pub fn compile_book(book: &DefinitionBook) -> anyhow::Result { + to_core::book_to_hvm_core(book) +} + +pub fn run_compiled(book: &Book) -> anyhow::Result<(LNet, RunStats)> { + let (mut root, runtime_book) = to_core::book_to_hvm_internal(book)?; + + let start_time = Instant::now(); + + // Computes its normal form + root.normalize(&runtime_book); + + let elapsed = start_time.elapsed().as_secs_f64(); + + let stats = RunStats { rewrites: root.rwts, size: root.node.len(), used: root.used, run_time: elapsed }; + let net = readback_lnet(&root); + Ok((net, stats)) +} + +pub fn run_book(book: &DefinitionBook) -> anyhow::Result<(Term, RunStats)> { + let compiled = compile_book(book)?; + let (res, stats) = run_compiled(&compiled)?; + let res = readback_net(&res)?; + Ok((res, stats)) +} + +pub struct RunStats { + pub rewrites: usize, + pub size: usize, + pub used: usize, + pub run_time: f64, +} diff --git a/src/main.rs b/src/main.rs index 86f7204f..22a110a8 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,25 +1,14 @@ #![feature(slice_group_by)] -use clap::Parser; -use hvm2::lang::show_net; -use std::{path::PathBuf, time::Instant}; - -pub mod ast; -pub mod loader; -pub mod parser; -pub mod to_core; +use clap::{Parser, ValueEnum}; +use hvm_lang::{check_book, compile_book, load_file_to_book, run_book}; +use std::path::PathBuf; #[derive(Parser, Debug)] #[command(author, version, about, long_about = None)] struct Args { - #[arg(long, default_value = "true", help = "Just checks if the file ok. Default mode", group = "mode")] - pub check: bool, - - #[arg(short, long, group = "mode", help = "Compiles to HVM-core and prints to stdout")] - pub compile: bool, - - #[arg(short, long, group = "mode", help = "Runs the hvm-lang file.")] - pub run: bool, + #[arg(value_enum)] + pub mode: Mode, #[arg(short, long)] pub verbose: bool, @@ -28,39 +17,37 @@ struct Args { pub path: PathBuf, } +#[derive(ValueEnum, Clone, Debug)] +enum Mode { + Check, + Compile, + Run, +} + fn main() -> anyhow::Result<()> { let args = Args::parse(); - let book = loader::load_file_to_book(&args.path)?; - + let book = load_file_to_book(&args.path)?; if args.verbose { println!("{book:?}"); } - let core_book = to_core::book_to_hvm_core(&book)?; - - if args.compile { - println!("{core_book}"); - } - - if args.run { - let (mut root, runtime_book) = to_core::book_to_hvm_internal(&core_book)?; - - let start_time = Instant::now(); - // Computes its normal form - root.normalize(&runtime_book); - - let elapsed = start_time.elapsed().as_secs_f64(); - // Shows results and stats - - println!("[net]\n{}", show_net(&root)); - println!("size: {}", root.node.len()); - println!("used: {}", root.used); - let cost = root.rwts; - - let rps = cost as f64 / elapsed / 1_000_000.0; - - println!("Time: {elapsed:.3}s | Rwts: {cost} | RPS: {rps:.3}m"); + match args.mode { + Mode::Check => { + check_book(&book)?; + } + Mode::Compile => { + let compiled = compile_book(&book)?; + println!("{compiled}"); + } + Mode::Run => { + let (res, stats) = run_book(&book)?; + let rps = stats.rewrites as f64 / stats.run_time / 1_000_000.0; + println!("\n{}\n", res); + println!("size: {}", stats.size); + println!("used: {}", stats.used); + println!("Time: {:.3}s | Rwts: {} | RPS: {:.3}m", stats.run_time, stats.rewrites, rps); + } } Ok(()) diff --git a/src/to_core/affine.rs b/src/to_core/affine.rs index c79efd91..0330b2c2 100644 --- a/src/to_core/affine.rs +++ b/src/to_core/affine.rs @@ -137,5 +137,7 @@ fn term_to_affine(value: Term, scope: &mut Scope, def_names: &HashSet) -> fst: Box::new(term_to_affine(*fst, scope, def_names)?), snd: Box::new(term_to_affine(*snd, scope, def_names)?), }), + Term::Sup { .. } => unreachable!(), + Term::Era => unreachable!(), } } diff --git a/src/to_core/compat_net.rs b/src/to_core/compat_net.rs index 524198e6..5f784190 100644 --- a/src/to_core/compat_net.rs +++ b/src/to_core/compat_net.rs @@ -1,78 +1,13 @@ use crate::ast::{ self, + compat::{ + addr, enter, kind, link, new_inet, new_node, port, slot, INet, NodeId, NodeKind, Port, CON, DUP, ERA, + LABEL_MASK, NUM, NUMOP, REF, ROOT, TAG_MASK, + }, core::{LNet, LTree, Tag, OP}, DefId, Name, NumOper, Term, }; use std::collections::HashMap; -#[derive(Clone, Debug)] -/// Net representation used only as an intermediate for converting to hvm-core format -pub struct INet { - pub nodes: Vec, -} - -type NodeVal = u64; -type NodeKind = NodeVal; -type Port = NodeVal; -type NodeId = NodeVal; -type SlotId = NodeVal; - -/// The ROOT port is on the deadlocked root node at address 0. -const ROOT: Port = 1; -const TAG_WIDTH: u32 = Tag::BITS; -const TAG: u32 = 64 - TAG_WIDTH; -const ERA: NodeKind = 0 << TAG; -const CON: NodeKind = 1 << TAG; -const DUP: NodeKind = 2 << TAG; -const REF: NodeKind = 3 << TAG; -const NUM: NodeKind = 4 << TAG; -const NUMOP: NodeKind = 5 << TAG; -const LABEL_MASK: NodeKind = (1 << TAG) - 1; -const TAG_MASK: NodeKind = !LABEL_MASK; - -/// Create a new net, with a deadlocked root node. -pub fn new_inet() -> INet { - INet { - nodes: vec![2, 1, 0, ERA], // p2 points to p0, p1 points to net - } -} - -/// Allocates a new node, reclaiming a freed space if possible. -pub fn new_node(inet: &mut INet, kind: NodeKind) -> NodeId { - let node = addr(inet.nodes.len() as Port); - inet.nodes.extend([port(node, 0), port(node, 1), port(node, 2), kind]); - node -} - -/// Builds a port (an address / slot pair). -pub fn port(node: NodeId, slot: SlotId) -> Port { - (node << 2) | slot -} - -/// Returns the address of a port (TODO: rename). -pub fn addr(port: Port) -> NodeId { - port >> 2 -} - -/// Returns the slot of a port. -pub fn slot(port: Port) -> SlotId { - port & 3 -} - -/// Enters a port, returning the port on the other side. -pub fn enter(inet: &INet, port: Port) -> Port { - inet.nodes[port as usize] -} - -/// Kind of the node. -pub fn kind(inet: &INet, node: NodeId) -> NodeKind { - inet.nodes[port(node, 3) as usize] -} - -/// Links two ports. -pub fn link(inet: &mut INet, ptr_a: Port, ptr_b: Port) { - inet.nodes[ptr_a as usize] = ptr_b; - inet.nodes[ptr_b as usize] = ptr_a; -} /// Converts an IC term into an IC net. pub fn term_to_compat_net(term: &Term, def_to_id: &HashMap) -> anyhow::Result { @@ -205,6 +140,8 @@ fn encode_term( link(inet, port(node, 1), snd); Ok(port(node, 2)) } + Term::Sup { .. } => unreachable!(), + Term::Era => unreachable!(), } } @@ -270,7 +207,7 @@ fn go_down_tree(inet: &INet, root: NodeId, explored_nodes: &mut [bool], side_lin debug_assert!(!explored_nodes[root as usize], "Explored same tree twice"); let mut nodes_to_check = vec![root]; while let Some(node) = nodes_to_check.pop() { - debug_assert!(explored_nodes[node as usize] == false); + debug_assert!(!explored_nodes[node as usize]); explored_nodes[node as usize] = true; for down_slot in [1, 2] { let down_port = enter(inet, port(node, down_slot)); @@ -346,6 +283,16 @@ fn var_or_subtree(inet: &INet, src_port: Port, port_to_var_id: &mut HashMap String { - format!("x{var_id}") +fn var_id_to_name(mut var_id: VarId) -> String { + let mut name = String::new(); + loop { + let c = (var_id % 26) as u8 + b'a'; + name.push(c as char); + var_id /= 26; + if var_id == 0 { + break; + } + } + name + // format!("x{var_id}") } diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs index bae7e651..9a8edda2 100644 --- a/tests/golden_tests.rs +++ b/tests/golden_tests.rs @@ -1,9 +1,9 @@ -use hvm2::lang::readback_lnet; use hvm_lang::{ ast::core::show_lnet, loader::print_err_reports, parser::{parse_definition_book, parse_term}, - to_core::{book_to_hvm_core, book_to_hvm_internal, term_to_hvm_core}, + run_book, + to_core::{book_to_hvm_core, term_to_hvm_core}, }; use pretty_assertions::assert_eq; use std::{collections::HashMap, fs, io::Write, path::Path}; @@ -74,9 +74,7 @@ fn run_single_files() { print_err_reports(&path.to_string_lossy(), code, errs); anyhow::anyhow!("Parsing error") })?; - let core_book = book_to_hvm_core(&book)?; - let (mut root, runtime_book) = book_to_hvm_internal(&core_book)?; - root.normalize(&runtime_book); - Ok(show_lnet(&readback_lnet(&root))) + let (res, _) = run_book(&book)?; + Ok(res.to_string()) }) } diff --git a/tests/golden_tests/compile_single_files/bool.golden b/tests/golden_tests/compile_single_files/bool.golden index 94c75780..71f1bae4 100644 --- a/tests/golden_tests/compile_single_files/bool.golden +++ b/tests/golden_tests/compile_single_files/bool.golden @@ -1,14 +1,14 @@ Not = - $ (0 (0 @fals (0 @true x0)) x0) + $ (0 (0 @fals (0 @true a)) a) Main = - $ x0 - & (0 @true x0) + $ a + & (0 @true a) ~ @Not fals = - $ (0 * (0 x0 x0)) + $ (0 * (0 a a)) true = - $ (0 x0 (0 * x0)) + $ (0 a (0 * a)) diff --git a/tests/golden_tests/compile_single_files/ex0.golden b/tests/golden_tests/compile_single_files/ex0.golden index 3b8f7e7f..085b9250 100644 --- a/tests/golden_tests/compile_single_files/ex0.golden +++ b/tests/golden_tests/compile_single_files/ex0.golden @@ -1,23 +1,23 @@ S = - $ (0 x0 (0 (0 x0 x1) (0 * x1))) + $ (0 a (0 (0 a b) (0 * b))) Z = - $ (0 * (0 x0 x0)) + $ (0 * (0 a a)) C_1 = - $ (0 (0 x0 x1) (0 x0 x1)) + $ (0 (0 a b) (0 a b)) C_2 = - $ (0 (16 (0 x0 x1) (0 x2 x0)) (0 x2 x1)) + $ (0 (16 (0 a b) (0 c a)) (0 c b)) C_s = - $ (0 (0 x0 (0 x1 x2)) (0 (16 (0 x2 x3) x0) (0 x1 x3))) + $ (0 (0 a (0 b c)) (0 (16 (0 c d) a) (0 b d))) C_z = - $ (0 * (0 x0 x0)) + $ (0 * (0 a a)) Main = - $ x0 - & (0 @S (0 @Z x0)) + $ a + & (0 @S (0 @Z a)) ~ @C_2 diff --git a/tests/golden_tests/compile_single_files/ex2.golden b/tests/golden_tests/compile_single_files/ex2.golden index 895106ce..9b2f83ee 100644 --- a/tests/golden_tests/compile_single_files/ex2.golden +++ b/tests/golden_tests/compile_single_files/ex2.golden @@ -1,72 +1,72 @@ E = - $ (0 * (0 * (0 x0 x0))) + $ (0 * (0 * (0 a a))) I = - $ (0 x0 (0 * (0 (0 x0 x1) (0 * x1)))) + $ (0 a (0 * (0 (0 a b) (0 * b)))) O = - $ (0 x0 (0 (0 x0 x1) (0 * (0 * x1)))) + $ (0 a (0 (0 a b) (0 * (0 * b)))) c2 = - $ (0 (16 (0 x0 x1) (0 x2 x0)) (0 x2 x1)) + $ (0 (16 (0 a b) (0 c a)) (0 c b)) Ex2 = - $ x0 - & (0 x1 x0) + $ a + & (0 b a) ~ @run - & (0 @I (0 @E x1)) + & (0 @I (0 @E b)) ~ @c2 dec = - $ (0 (0 @decO (0 @decI (0 @E x0))) x0) + $ (0 (0 @decO (0 @decI (0 @E a))) a) low = - $ (0 (0 @lowO (0 @lowI (0 @E x0))) x0) + $ (0 (0 @lowO (0 @lowI (0 @E a))) a) run = - $ (0 (0 @runO (0 @runI (0 @E x0))) x0) + $ (0 (0 @runO (0 @runI (0 @E a))) a) decI = - $ (0 x0 x1) - & (0 x0 x1) + $ (0 a b) + & (0 a b) ~ @low decO = - $ (0 x0 x1) - & (0 x2 x1) + $ (0 a b) + & (0 c b) ~ @I - & (0 x0 x2) + & (0 a c) ~ @dec lowI = - $ (0 x0 x1) - & (0 x2 x1) + $ (0 a b) + & (0 c b) ~ @O - & (0 x0 x2) + & (0 a c) ~ @I lowO = - $ (0 x0 x1) - & (0 x2 x1) + $ (0 a b) + & (0 c b) ~ @O - & (0 x0 x2) + & (0 a c) ~ @O runI = - $ (0 x0 x1) - & (0 x2 x1) + $ (0 a b) + & (0 c b) ~ @run - & (0 x3 x2) + & (0 d c) ~ @dec - & (0 x0 x3) + & (0 a d) ~ @I runO = - $ (0 x0 x1) - & (0 x2 x1) + $ (0 a b) + & (0 c b) ~ @run - & (0 x3 x2) + & (0 d c) ~ @dec - & (0 x0 x3) + & (0 a d) ~ @O diff --git a/tests/golden_tests/compile_single_files/var_shadows_ref.golden b/tests/golden_tests/compile_single_files/var_shadows_ref.golden index 2302bda4..bb0fe34f 100644 --- a/tests/golden_tests/compile_single_files/var_shadows_ref.golden +++ b/tests/golden_tests/compile_single_files/var_shadows_ref.golden @@ -1,8 +1,8 @@ a = - $ (0 x0 x0) + $ (0 a a) b = - $ x0 - & (0 (0 x1 x1) x0) + $ a + & (0 (0 b b) a) ~ @a diff --git a/tests/golden_tests/compile_single_terms/church_one.golden b/tests/golden_tests/compile_single_terms/church_one.golden index fcae073f..1848d1f6 100644 --- a/tests/golden_tests/compile_single_terms/church_one.golden +++ b/tests/golden_tests/compile_single_terms/church_one.golden @@ -1,3 +1,3 @@ -$ x0 -& (0 (0 * (0 x1 x1)) x0) -~ (0 (0 x2 (0 x3 x4)) (0 (16 (0 x4 x5) x2) (0 x3 x5))) +$ a +& (0 (0 * (0 b b)) a) +~ (0 (0 c (0 d e)) (0 (16 (0 e f) c) (0 d f))) diff --git a/tests/golden_tests/compile_single_terms/church_zero.golden b/tests/golden_tests/compile_single_terms/church_zero.golden index 5bcabefc..c45e52ec 100644 --- a/tests/golden_tests/compile_single_terms/church_zero.golden +++ b/tests/golden_tests/compile_single_terms/church_zero.golden @@ -1 +1 @@ -$ (0 * (0 x0 x0)) +$ (0 * (0 a a)) diff --git a/tests/golden_tests/compile_single_terms/dup_apply.golden b/tests/golden_tests/compile_single_terms/dup_apply.golden index 5224c61f..74eb596e 100644 --- a/tests/golden_tests/compile_single_terms/dup_apply.golden +++ b/tests/golden_tests/compile_single_terms/dup_apply.golden @@ -1 +1 @@ -$ (0 (16 (0 x0 x1) x0) x1) +$ (0 (16 (0 a b) a) b) diff --git a/tests/golden_tests/compile_single_terms/erased_dup.golden b/tests/golden_tests/compile_single_terms/erased_dup.golden index 5fe49da3..c79fac5b 100644 --- a/tests/golden_tests/compile_single_terms/erased_dup.golden +++ b/tests/golden_tests/compile_single_terms/erased_dup.golden @@ -1 +1 @@ -$ (0 (16 * x0) x0) +$ (0 (16 * a) a) diff --git a/tests/golden_tests/compile_single_terms/id.golden b/tests/golden_tests/compile_single_terms/id.golden index 09c59c92..91dccf4f 100644 --- a/tests/golden_tests/compile_single_terms/id.golden +++ b/tests/golden_tests/compile_single_terms/id.golden @@ -1 +1 @@ -$ (0 x0 x0) +$ (0 a a) diff --git a/tests/golden_tests/compile_single_terms/infer_dup.golden b/tests/golden_tests/compile_single_terms/infer_dup.golden index 5224c61f..74eb596e 100644 --- a/tests/golden_tests/compile_single_terms/infer_dup.golden +++ b/tests/golden_tests/compile_single_terms/infer_dup.golden @@ -1 +1 @@ -$ (0 (16 (0 x0 x1) x0) x1) +$ (0 (16 (0 a b) a) b) diff --git a/tests/golden_tests/run_single_files/add.golden b/tests/golden_tests/run_single_files/add.golden index 174bc33f..d8263ee9 100644 --- a/tests/golden_tests/run_single_files/add.golden +++ b/tests/golden_tests/run_single_files/add.golden @@ -1 +1 @@ -$ 2 +2 \ No newline at end of file diff --git a/tests/golden_tests/run_single_files/example.hvm b/tests/golden_tests/run_single_files/example.hvm new file mode 100644 index 00000000..5c50490b --- /dev/null +++ b/tests/golden_tests/run_single_files/example.hvm @@ -0,0 +1,24 @@ +// Write definitions like this +(Def1) = (λa a) (λb b) + +// You can call a definition by just referencing its name +// It will be substituted in place of the reference +(Def2) = (λa a) Def1 + +// Definitions and variables can have names in upper and lower case and contain numbers +// Names defined in a more inner position shadow names in an outer position +(def3) = (λDef1 Def1) (λx λx x) + +// The language is affine, but if you use a variable more than once the compiler inserts duplications for you +// Of course you can always do them manually +(def4) = λz dup z1 z2 = z; z1 ((λx x x x x x) z2) + +// You can use machine numbers and some native numeric operations +// Numeric operations can only reduce numbers, doing (+ (λx x) 1) will not do anything +(nums) = λx1 λx2 (* (+ x1 1) (/ (- x2 2) 1)) + +// All files must have a main definition to be run. +// You can execute a program in HVM with "cargo run -- --run " +// Other options are "--check" (the default mode) to just see if the file is well formed +// and "--compile" to output hvm-core code. +(Main) = nums 1 4