Add readback of results from HVM; Refactor CLI mode

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<NodeVal>,
+}
+
+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<INode>;

src/ast/hvm_lang.rs

@@ -36,6 +36,8 @@ pub enum Term {
   Dup { fst: Name, snd: Name, val: Box<Term>, nxt: Box<Term> },
   Num { val: Number },
   NumOp { op: NumOper, fst: Box<Term>, snd: Box<Term> },
+  Sup { fst: Box<Term>, snd: Box<Term> },
+  Era,
 }
 
 // TODO: Switch to the hvm2 type when it's done
@@ -120,6 +122,17 @@ impl From<NumOper> 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)
   }
 }
 

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};
 

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<Term> {
+  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<INet> {
+  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: &LTree, 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<Port, Name>) -> 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<Port, Name>,
+    dups_vec: &mut Vec<NodeId>,
+    dups_set: &mut HashSet<NodeId>,
+    seen: &mut HashSet<Port>,
+  ) -> 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
+}

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<Book> {
+  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,
+}

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(())

src/to_core/affine.rs

@@ -137,5 +137,7 @@ fn term_to_affine(value: Term, scope: &mut Scope, def_names: &HashSet<Name>) ->
       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!(),
   }
 }

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<NodeVal>,
-}
-
-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<Name, DefId>) -> anyhow::Result<INet> {
@@ -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<Port
   }
 }
 
-fn var_id_to_name(var_id: VarId) -> 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}")
 }

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())
   })
 }

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))
   

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
   

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
   

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
   

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)))

tests/golden_tests/compile_single_terms/church_zero.golden

@@ -1 +1 @@
-$ (0 * (0 x0 x0))
+$ (0 * (0 a a))

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)

tests/golden_tests/compile_single_terms/erased_dup.golden

@@ -1 +1 @@
-$ (0 (16 * x0) x0)
+$ (0 (16 * a) a)

tests/golden_tests/compile_single_terms/id.golden

@@ -1 +1 @@
-$ (0 x0 x0)
+$ (0 a a)

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)

tests/golden_tests/run_single_files/add.golden

@@ -1 +1 @@
-$ 2
+2

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 <path to file>"
+// 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