Implement If term, partial fix for op2, stabilize nums!

Cargo.toml

@@ -11,9 +11,8 @@ name = "hvm-lang"
 required-features = ["cli"]
 
 [features]
-default = ["cli", "nums"]
+default = ["cli"]
 cli = ["dep:clap", "dep:byte-unit"]
-nums = []
 
 [dependencies]
 anyhow = "1.0.72"

src/ast/compat.rs

@@ -1,6 +1,5 @@
 // TODO: Refactor to not use this intermediate form
 
-#[cfg(feature = "nums")]
 use super::hvm_lang::Op;
 use hvmc::Val;
 
@@ -25,6 +24,7 @@ pub const DUP: NodeKind = 2 << TAG;
 pub const REF: NodeKind = 3 << TAG;
 pub const NUM: NodeKind = 4 << TAG;
 pub const OP2: NodeKind = 6 << TAG;
+pub const ITE: NodeKind = 7 << TAG;
 pub const LABEL_MASK: NodeKind = (1 << TAG) - 1;
 pub const TAG_MASK: NodeKind = !LABEL_MASK;
 
@@ -81,7 +81,6 @@ pub struct INode {
 
 pub type INodes = Vec<INode>;
 
-#[cfg(feature = "nums")]
 pub fn op_to_label(value: Op) -> NodeKind {
   match value {
     Op::ADD => 0x1,
@@ -102,7 +101,6 @@ pub fn op_to_label(value: Op) -> NodeKind {
   }
 }
 
-#[cfg(feature = "nums")]
 pub fn label_to_op(value: NodeKind) -> Option<Op> {
   match value {
     0x1 => Some(Op::ADD),

src/ast/hvm_lang.rs

@@ -32,7 +32,6 @@ pub struct Rule {
 pub enum Pattern {
   Ctr(Name, Vec<Pattern>),
   Var(Option<Name>),
-  #[cfg(feature = "nums")]
   Num(u32),
 }
 
@@ -66,6 +65,11 @@ pub enum Term {
     fun: Box<Term>,
     arg: Box<Term>,
   },
+  If {
+    cond: Box<Term>,
+    then: Box<Term>,
+    els_: Box<Term>,
+  },
   Dup {
     fst: Option<Name>,
     snd: Option<Name>,
@@ -77,11 +81,9 @@ pub enum Term {
     snd: Box<Term>,
   },
   Era,
-  #[cfg(feature = "nums")]
   Num {
     val: u32,
   },
-  #[cfg(feature = "nums")]
   /// A numeric operation between built-in numbers.
   Opx {
     op: Op,
@@ -160,6 +162,14 @@ impl Term {
       }
       Term::Ref { def_id } => format!("{}", def_names.name(def_id).unwrap()),
       Term::App { fun, arg } => format!("({} {})", fun.to_string(def_names), arg.to_string(def_names)),
+      Term::If { cond, then, els_ } => {
+        format!(
+          "if {} then {} else {}",
+          cond.to_string(def_names),
+          then.to_string(def_names),
+          els_.to_string(def_names)
+        )
+      }
       Term::Dup { fst, snd, val, nxt } => format!(
         "dup {} {} = {}; {}",
         fst.as_ref().map(|x| x.as_str()).unwrap_or("*"),
@@ -169,9 +179,7 @@ impl Term {
       ),
       Term::Sup { fst, snd } => format!("{{{} {}}}", fst.to_string(def_names), snd.to_string(def_names)),
       Term::Era => "*".to_string(),
-      #[cfg(feature = "nums")]
       Term::Num { val } => format!("{val}"),
-      #[cfg(feature = "nums")]
       Term::Opx { op, fst, snd } => {
         format!("({} {} {})", op, fst.to_string(def_names), snd.to_string(def_names))
       }
@@ -199,6 +207,11 @@ impl Term {
           nxt.subst(from, to);
         }
       }
+      Term::If { cond, then, els_ } => {
+        cond.subst(from, to);
+        then.subst(from, to);
+        els_.subst(from, to);
+      }
       Term::Ref { .. } => (),
       Term::App { fun, arg } => {
         fun.subst(from, to);
@@ -215,9 +228,7 @@ impl Term {
         snd.subst(from, to);
       }
       Term::Era => (),
-      #[cfg(feature = "nums")]
       Term::Num { .. } => (),
-      #[cfg(feature = "nums")]
       Term::Opx { fst, snd, .. } => {
         fst.subst(from, to);
         snd.subst(from, to);
@@ -257,7 +268,6 @@ impl From<&Pattern> for Term {
     match value {
       Pattern::Ctr(nam, args) => Term::call(Term::Var { nam: nam.clone() }, args.iter().map(Term::from)),
       Pattern::Var(nam) => Term::Var { nam: Name::new(nam.as_ref().map(|x| x.as_str()).unwrap_or("_")) },
-      #[cfg(feature = "nums")]
       Pattern::Num(num) => Term::Num { val: *num },
     }
   }
@@ -274,7 +284,6 @@ impl fmt::Display for Pattern {
     match self {
       Pattern::Ctr(name, pats) => write!(f, "({}{})", name, pats.iter().map(|p| format!(" {p}")).join("")),
       Pattern::Var(nam) => write!(f, "{}", nam.as_ref().map(|x| x.as_str()).unwrap_or("*")),
-      #[cfg(feature = "nums")]
       Pattern::Num(num) => write!(f, "{num}"),
     }
   }

src/from_core/mod.rs

@@ -1,7 +1,7 @@
 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, REF, ROOT, TAG_MASK,
+    SlotId, CON, DUP, ERA, ITE, LABEL_MASK, REF, ROOT, TAG_MASK,
   },
   hvm_lang::Op,
   var_id_to_name, DefId, Name, Term,
@@ -9,7 +9,6 @@ use crate::ast::{
 use hvmc::{LNet, LTree, Val};
 use std::collections::{HashMap, HashSet};
 
-#[cfg(feature = "nums")]
 use crate::ast::compat::{label_to_op, NUM, OP2};
 
 pub fn readback_net(net: &LNet) -> anyhow::Result<(Term, bool)> {
@@ -88,13 +87,11 @@ fn tree_to_inodes(tree: &LTree, tree_root: String, net_root: &str, n_vars: &mut
         let var = new_var(n_vars);
         inodes.push(INode { kind, ports: [subtree_root, var.clone(), var] });
       }
-      #[cfg(feature = "nums")]
       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] });
       }
-      #[cfg(feature = "nums")]
       LTree::Op2 { lft, rgt } => {
         let kind = OP2;
         let lft = process_node_subtree(lft, net_root, &mut subtrees, n_vars);
@@ -201,6 +198,38 @@ fn readback_compat(net: &INet) -> (Term, bool) {
         }
         _ => unreachable!(),
       },
+      ITE => match slot(next) {
+        2 => {
+          seen.insert(port(node, 0));
+          seen.insert(port(node, 1));
+          let cond_port = enter(net, port(node, 0));
+          let (cond_term, cond_valid) = reader(net, cond_port, var_port_to_name, dups_vec, dups_set, seen);
+          let branches_port = enter(net, port(node, 0));
+          let branches_node = addr(branches_port);
+          let branches_kind = kind(net, branches_node);
+          if branches_kind & TAG_MASK == CON {
+            seen.insert(port(branches_node, 0));
+            seen.insert(port(branches_node, 1));
+            seen.insert(port(branches_node, 2));
+            let then_port = enter(net, port(node, 0));
+            let (then_term, then_valid) = reader(net, then_port, var_port_to_name, dups_vec, dups_set, seen);
+            let else_port = enter(net, port(node, 0));
+            let (else_term, else_valid) = reader(net, else_port, var_port_to_name, dups_vec, dups_set, seen);
+            let valid = cond_valid && then_valid && else_valid;
+            (
+              Term::If { cond: Box::new(cond_term), then: Box::new(then_term), els_: Box::new(else_term) },
+              valid,
+            )
+          } else {
+            // TODO: Is there any case where we expect a different node type here on readback
+            (
+              Term::If { cond: Box::new(cond_term), then: Box::new(Term::Era), els_: Box::new(Term::Era) },
+              false,
+            )
+          }
+        }
+        _ => unreachable!(),
+      },
       REF => (Term::Ref { def_id: DefId(label) }, true),
       // If we're visiting a fan node...
       DUP => match slot(next) {
@@ -228,9 +257,7 @@ fn readback_compat(net: &INet) -> (Term, bool) {
         }
         _ => unreachable!(),
       },
-      #[cfg(feature = "nums")]
       NUM => (Term::Num { val: label as u32 }, true),
-      #[cfg(feature = "nums")]
       OP2 => match slot(next) {
         2 => {
           seen.insert(port(node, 0));
@@ -244,10 +271,18 @@ fn readback_compat(net: &INet) -> (Term, bool) {
             Term::Num { val } => {
               let (val, op) = split_num_with_op(val);
               if let Some(op) = op {
+                // This is Num + Op in the same value
                 (Term::Opx { op, fst: Box::new(Term::Num { val }), snd: Box::new(arg_term) }, valid)
               } else {
-                // TODO: is this possible?
-                todo!()
+                // This is just Op as value
+                (
+                  Term::Opx {
+                    op: label_to_op(val).unwrap(),
+                    fst: Box::new(arg_term),
+                    snd: Box::new(Term::Era),
+                  },
+                  valid,
+                )
               }
             }
             Term::Opx { op, fst: _, snd } => (Term::Opx { op, fst: snd, snd: Box::new(arg_term) }, valid),

src/parser/lexer.rs

@@ -19,6 +19,9 @@ pub enum Token {
   #[token("dup")]
   Dup,
 
+  #[token("if")]
+  If,
+
   #[token("=")]
   Equals,
 
@@ -153,6 +156,7 @@ impl fmt::Display for Token {
       Self::Dollar => write!(f, "$"),
       Self::Let => write!(f, "let"),
       Self::Dup => write!(f, "dup"),
+      Self::If => write!(f, "if"),
       Self::Equals => write!(f, "="),
       Self::Num(num) => write!(f, "{num}"),
       Self::Add => write!(f, "+"),

src/parser/parser.rs

@@ -17,7 +17,6 @@ use itertools::Itertools;
 use logos::{Logos, SpannedIter};
 use std::{iter::Map, ops::Range};
 
-#[cfg(feature = "nums")]
 use crate::ast::hvm_lang::Op;
 
 // TODO: Pattern matching on rules
@@ -47,18 +46,13 @@ pub fn parse_definition_book(code: &str) -> Result<DefinitionBook, Vec<Rich<Toke
 pub fn parse_term(code: &str) -> Result<Term, Vec<Rich<Token>>> {
   let inline_app =
     term().foldl(term().repeated(), |fun, arg| Term::App { fun: Box::new(fun), arg: Box::new(arg) });
-  #[cfg(feature = "nums")]
   let inline_num_oper = num_oper().then(term()).then(term()).map(|((op, fst), snd)| Term::Opx {
     op,
     fst: Box::new(fst),
     snd: Box::new(snd),
   });
-  #[cfg(feature = "nums")]
   let standalone_term = choice((inline_app, inline_num_oper))
     .delimited_by(just(Token::NewLine).repeated(), just(Token::NewLine).repeated());
-  #[cfg(not(feature = "nums"))]
-  let standalone_term =
-    inline_app.delimited_by(just(Token::NewLine).repeated(), just(Token::NewLine).repeated());
 
   // TODO: Make a function that calls a parser. I couldn't figure out how to type it correctly.
   standalone_term.parse(token_stream(code)).into_result()
@@ -99,7 +93,6 @@ where
   choice((select!(Token::Asterisk => None), name().map(Some)))
 }
 
-#[cfg(feature = "nums")]
 fn num_oper<'a, I>() -> impl Parser<'a, I, Op, extra::Err<Rich<'a, Token>>>
 where
   I: ValueInput<'a, Token = Token, Span = SimpleSpan>,
@@ -132,7 +125,6 @@ where
   let global_var = just(Token::Dollar).ignore_then(name()).map(|name| Term::Lnk { nam: name }).boxed();
   let term_sep = choice((just(Token::NewLine), just(Token::Semicolon)));
 
-  #[cfg(feature = "nums")]
   let unsigned = select!(Token::Num(num) => Term::Num{val: num});
 
   recursive(|term| {
@@ -186,6 +178,19 @@ where
       .map(|((nam, val), nxt)| Term::Let { nam, val: Box::new(val), nxt: Box::new(nxt) })
       .boxed();
 
+    let if_ = just(Token::If)
+      .ignore_then(new_line())
+      .ignore_then(term.clone())
+      .then_ignore(select!(Token::Name(nam) if nam == "then" => ()))
+      .then(term.clone())
+      .then_ignore(select!(Token::Name(nam) if nam == "else" => ()))
+      .then(term.clone())
+      .map(|((cond, then), els_)| Term::If {
+        cond: Box::new(cond),
+        then: Box::new(then),
+        els_: Box::new(els_),
+      });
+
     // (f arg1 arg2 ...)
     let app = term
       .clone()
@@ -197,7 +202,6 @@ where
       .delimited_by(just(Token::LParen), just(Token::RParen))
       .boxed();
 
-    #[cfg(feature = "nums")]
     let num_op = num_oper()
       .then_ignore(new_line())
       .then(term.clone())
@@ -208,15 +212,7 @@ where
       .map(|((op, fst), snd)| Term::Opx { op, fst: Box::new(fst), snd: Box::new(snd) })
       .boxed();
 
-    #[cfg(feature = "nums")]
-    {
-      choice((global_var, var, unsigned, global_lam, lam, dup, let_, num_op, app))
-    }
-
-    #[cfg(not(feature = "nums"))]
-    {
-      choice((global_var, var, global_lam, lam, dup, let_, app))
-    }
+    choice((global_var, var, unsigned, global_lam, lam, dup, let_, if_, num_op, app))
   })
 }
 
@@ -231,18 +227,8 @@ where
       .map(|(name, pats)| Pattern::Ctr(name, pats))
       .boxed();
     let var = name_or_era().map(Pattern::Var).boxed();
-
-    #[cfg(feature = "nums")]
     let num = select!(Token::Num(num) => Pattern::Num(num)).boxed();
-
-    #[cfg(feature = "nums")]
-    {
-      choice((ctr, num, var))
-    }
-    #[cfg(not(feature = "nums"))]
-    {
-      choice((ctr, var))
-    }
+    choice((ctr, num, var))
   })
 }
 
@@ -252,7 +238,6 @@ where
 {
   let inline_app =
     term().foldl(term().repeated(), |fun, arg| Term::App { fun: Box::new(fun), arg: Box::new(arg) });
-  #[cfg(feature = "nums")]
   let inline_num_oper = num_oper().then(term()).then(term()).map(|((op, fst), snd)| Term::Opx {
     op,
     fst: Box::new(fst),
@@ -262,10 +247,7 @@ where
   let lhs = name().then(pattern().repeated().collect()).boxed();
   let lhs = choice((lhs.clone(), lhs.delimited_by(just(Token::LParen), just(Token::RParen))));
 
-  #[cfg(feature = "nums")]
   let rhs = choice((inline_num_oper, inline_app));
-  #[cfg(not(feature = "nums"))]
-  let rhs = inline_app;
 
   lhs
     .then_ignore(just(Token::NewLine).repeated())

src/semantic/combinators.rs

@@ -117,6 +117,12 @@ impl Term {
 
           fun_is_super && arg_is_super
         }
+        Term::If { cond, then, els_ } => {
+          let cond_is_super = go(cond, depth + 1, term_info);
+          let then_is_super = go(then, depth + 1, term_info);
+          let else_is_super = go(els_, depth + 1, term_info);
+          cond_is_super && then_is_super && else_is_super
+        }
         Term::Dup { fst, snd, val, nxt } => {
           let val_is_super = go(val, depth + 1, term_info);
           let nxt_is_supper = go(nxt, depth + 1, term_info);
@@ -133,10 +139,7 @@ impl Term {
 
         Term::Sup { .. } => todo!(),
         Term::Era => true,
-
-        #[cfg(feature = "nums")]
         Term::Num { .. } => true,
-        #[cfg(feature = "nums")]
         Term::Opx { .. } => true,
       }
     }

src/semantic/pattern/flatten.rs

@@ -58,11 +58,7 @@ fn must_split(rule: &Rule) -> bool {
   for pat in &rule.pats {
     if let Pattern::Ctr(_, args) = &pat {
       for arg in args {
-        if matches!(arg, Pattern::Ctr(..)) {
-          return true;
-        }
-        #[cfg(feature = "nums")]
-        if matches!(arg, Pattern::Num(..)) {
+        if matches!(arg, Pattern::Ctr(..) | Pattern::Num(..)) {
           return true;
         }
       }
@@ -86,9 +82,7 @@ fn matches_together(a: &Rule, b: &Rule) -> bool {
         a_implies_b = false;
         break;
       }
-      #[cfg(feature = "nums")]
       (Pattern::Num(a), Pattern::Num(b)) if a == b => (),
-      #[cfg(feature = "nums")]
       (Pattern::Num(..), Pattern::Num(..)) => {
         a_implies_b = false;
         break;
@@ -120,7 +114,6 @@ fn split_rule(
   let new_def_id = make_split_def_name(rules[rule_idx].def_id, name_count, def_names);
   let new_def = make_split_def(rules, rule_idx, new_def_id, &mut var_count, skip);
   let old_rule = make_rule_calling_split(&rules[rule_idx], new_def_id);
-  eprintln!("x {}", new_def.to_string(def_names));
   // Recursively flatten the newly created definition
   let (new_def, split_defs) = flatten_def(&new_def, def_names);
   (old_rule, new_def, split_defs)
@@ -176,15 +169,12 @@ fn make_split_def(
           (Pattern::Var(..), other_pat) => {
             new_rule_pats.push(other_pat.clone());
           }
-          #[cfg(feature = "nums")]
           (Pattern::Num(..), Pattern::Num(..)) => (),
-          #[cfg(feature = "nums")]
           (Pattern::Num(num), Pattern::Var(name)) => {
             if let Some(name) = name {
               new_rule_body.subst(name, &Term::Num { val: *num });
             }
           }
-          #[cfg(feature = "nums")]
           // Not possible since we know it matches
           _ => {
             panic!("Internal error. Please report.");
@@ -224,7 +214,6 @@ fn make_rule_calling_split(old_rule: &Rule, new_def_id: DefId) -> Rule {
               Pattern::Var(Some(nam))
             }
             Pattern::Var(..) => field.clone(),
-            #[cfg(feature = "nums")]
             Pattern::Num(..) => {
               let nam = Name(format!(".x{}", var_count));
               var_count += 1;
@@ -237,7 +226,6 @@ fn make_rule_calling_split(old_rule: &Rule, new_def_id: DefId) -> Rule {
 
         old_rule_pats.push(Pattern::Ctr(name.clone(), new_pat_args));
       }
-      #[cfg(feature = "nums")]
       Pattern::Num(..) => {
         old_rule_pats.push(pat.clone());
       }

src/semantic/pattern/mod.rs

@@ -31,9 +31,7 @@ impl DefinitionBook {
 pub enum Type {
   Any,
   Adt(AdtId),
-  #[cfg(feature = "nums")]
   U32,
-  #[cfg(feature = "nums")]
   I32,
 }
 

src/semantic/pattern/type_inference.rs

@@ -4,13 +4,16 @@ use anyhow::anyhow;
 use itertools::Itertools;
 use std::collections::HashMap;
 
+type Adts = HashMap<AdtId, Adt>;
+type Types = Vec<Vec<Type>>;
+
 impl DefinitionBook {
   /// Infers ADTs from the patterns of the rules in a book.
   /// Returns the infered type of the patterns of each definition.
   /// Returns an error if rules use the types in a inconsistent way.
   /// These could be same name in different types, different arities or mixing numbers and ADTs.
   /// Precondition: Rules have been flattened, rule arity is correct.
-  pub fn get_types_from_patterns(&self) -> anyhow::Result<(HashMap<AdtId, Adt>, Vec<Vec<Type>>)> {
+  pub fn get_types_from_patterns(&self) -> anyhow::Result<(Adts, Types)> {
     // TODO: This algorithm does a lot of unnecessary copying, checking and moving around of data.
     // There's a lot of space for optimizing.
 
@@ -117,7 +120,7 @@ impl Definition {
           }
         }
         Pattern::Var(_) => adt.others = true,
-        #[cfg(feature = "nums")]
+
         _ => panic!("Expected only Ctr and Var patterns to be called here"),
       }
     }

src/semantic/vars.rs

@@ -91,6 +91,11 @@ fn check_uses(term: &Term, def_names: &DefNames) -> anyhow::Result<()> {
         go(fun, scope, globals, def_names)?;
         go(arg, scope, globals, def_names)?;
       }
+      Term::If { cond, then, els_ } => {
+        go(cond, scope, globals, def_names)?;
+        go(then, scope, globals, def_names)?;
+        go(els_, scope, globals, def_names)?;
+      }
       Term::Dup { fst, snd, val, nxt } => {
         go(val, scope, globals, def_names)?;
         if let Some(fst) = fst {
@@ -112,12 +117,10 @@ fn check_uses(term: &Term, def_names: &DefNames) -> anyhow::Result<()> {
         go(snd, scope, globals, def_names)?;
       }
       Term::Ref { .. } | Term::Era => (),
-      #[cfg(feature = "nums")]
       Term::Opx { fst, snd, .. } => {
         go(fst, scope, globals, def_names)?;
         go(snd, scope, globals, def_names)?;
       }
-      #[cfg(feature = "nums")]
       Term::Num { .. } => (),
     }
     Ok(())
@@ -242,13 +245,18 @@ fn unique_var_names(term: &Term, def_names: &DefNames) -> anyhow::Result<(Term,
         let snd = go(snd, name_map, name_count, var_uses, def_names)?;
         Term::Sup { fst: Box::new(fst), snd: Box::new(snd) }
       }
-      #[cfg(feature = "nums")]
       Term::Opx { op, fst, snd } => {
         let fst = go(fst, name_map, name_count, var_uses, def_names)?;
         let snd = go(snd, name_map, name_count, var_uses, def_names)?;
         Term::Opx { op: *op, fst: Box::new(fst), snd: Box::new(snd) }
       }
-      t => t.clone(),
+      Term::If { cond, then, els_ } => {
+        let cond = go(cond, name_map, name_count, var_uses, def_names)?;
+        let then = go(then, name_map, name_count, var_uses, def_names)?;
+        let els_ = go(els_, name_map, name_count, var_uses, def_names)?;
+        Term::If { cond: Box::new(cond), then: Box::new(then), els_: Box::new(els_) }
+      }
+      t @ (Term::Lnk { .. } | Term::Ref { .. } | Term::Era | Term::Num { .. }) => t.clone(),
     };
     Ok(term)
   }
@@ -361,13 +369,14 @@ fn term_to_affine(
       fst: Box::new(term_to_affine(*fst, var_uses, let_bodies)?),
       snd: Box::new(term_to_affine(*snd, var_uses, let_bodies)?),
     },
-    #[cfg(feature = "nums")]
     Term::Opx { op, fst, snd } => Term::Opx {
       op,
       fst: Box::new(term_to_affine(*fst, var_uses, let_bodies)?),
       snd: Box::new(term_to_affine(*snd, var_uses, let_bodies)?),
     },
-    t => t,
+    t @ (Term::Era | Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. }) => t,
+
+    Term::If { cond, then, els_ } => todo!(),
   };
   Ok(term)
 }

src/to_core/compat_net.rs

@@ -1,14 +1,13 @@
 use crate::ast::{
   compat::{
-    addr, enter, kind, link, new_inet, new_node, port, slot, INet, NodeId, Port, CON, DUP, ERA, LABEL_MASK,
-    REF, ROOT, TAG_MASK,
+    addr, enter, kind, link, new_inet, new_node, port, slot, INet, NodeId, Port, CON, DUP, ERA, ITE,
+    LABEL_MASK, REF, ROOT, TAG_MASK,
   },
   var_id_to_name, DefId, Name, Term,
 };
 use hvmc::{LNet, LTree, Tag};
 use std::collections::{HashMap, HashSet};
 
-#[cfg(feature = "nums")]
 use crate::ast::compat::{op_to_label, NodeKind, NUM, OP2};
 
 /// Converts an IC term into an IC net.
@@ -48,6 +47,7 @@ fn encode_term(
     // - 0: points to where the lambda occurs.
     // - 1: points to the lambda variable.
     // - 2: points to the lambda body.
+    // core: (var_use bod)
     Term::Lam { nam, bod } => {
       let fun = new_node(inet, CON);
       push_scope(nam, port(fun, 1), scope, vars);
@@ -56,6 +56,7 @@ fn encode_term(
       link_local(inet, port(fun, 2), bod);
       Ok(Some(port(fun, 0)))
     }
+    // core: (var_use bod)
     Term::Chn { nam, bod } => {
       let fun = new_node(inet, CON);
       global_vars.entry(nam.clone()).or_default().0 = port(fun, 1);
@@ -67,6 +68,7 @@ fn encode_term(
     // - 0: points to the function being applied.
     // - 1: points to the function's argument.
     // - 2: points to where the application occurs.
+    // core: & fun ~ (arg ret) (fun not necessarily main port)
     Term::App { fun, arg } => {
       let app = new_node(inet, CON);
       let fun = encode_term(inet, fun, port(app, 0), scope, vars, global_vars, dups)?;
@@ -75,10 +77,29 @@ fn encode_term(
       link_local(inet, port(app, 1), arg);
       Ok(Some(port(app, 2)))
     }
+    // core: & cond ~ ? (then els_) ret
+    Term::If { cond, then, els_ } => {
+      let if_ = new_node(inet, ITE);
+
+      let cond = encode_term(inet, cond, port(if_, 0), scope, vars, global_vars, dups)?;
+      link_local(inet, port(if_, 0), cond);
+
+      let branches = new_node(inet, CON);
+      link(inet, port(if_, 1), port(branches, 0));
+
+      let then = encode_term(inet, then, port(branches, 1), scope, vars, global_vars, dups)?;
+      link_local(inet, port(branches, 1), then);
+
+      let els_ = encode_term(inet, els_, port(branches, 2), scope, vars, global_vars, dups)?;
+      link_local(inet, port(branches, 2), els_);
+
+      Ok(Some(port(if_, 2)))
+    }
     // A dup becomes a dup node too. Ports:
     // - 0: points to the value projected.
     // - 1: points to the occurrence of the first variable.
     // - 2: points to the occurrence of the second variable.
+    // core: & val ~ {lab fst snd} (val not necessarily main port)
     Term::Dup { fst, snd, val, nxt } => {
       let dup = new_node(inet, DUP | *dups);
       *dups += 1;
@@ -112,6 +133,7 @@ fn encode_term(
       global_vars.entry(nam.clone()).or_default().1 = up;
       Ok(None)
     }
+    // core: @def_id
     Term::Ref { def_id } => {
       let node = new_node(inet, REF | **def_id);
       link(inet, port(node, 1), port(node, 2));
@@ -121,7 +143,7 @@ fn encode_term(
     Term::Let { .. } => unreachable!(), // Removed in earlier poss
     Term::Sup { .. } => unreachable!(), // Not supported in syntax
     Term::Era => unreachable!(),        // Not supported in syntax
-    #[cfg(feature = "nums")]
+    // core: #val
     Term::Num { val } => {
       debug_assert!(*val as NodeKind <= LABEL_MASK);
       let node = new_node(inet, NUM | *val as NodeKind);
@@ -129,18 +151,20 @@ fn encode_term(
       link(inet, port(node, 1), port(node, 2));
       Ok(Some(port(node, 0)))
     }
-    #[cfg(feature = "nums")]
+    // core: & #op ~ <fst <snd ret>>
     Term::Opx { op, fst, snd } => {
       let op_node = new_node(inet, NUM | op_to_label(*op));
       link(inet, port(op_node, 1), port(op_node, 2));
 
       let fst_node = new_node(inet, OP2);
-      link(inet, port(op_node, 1), port(fst_node, 0));
+      link(inet, port(op_node, 0), port(fst_node, 0));
+
       let fst = encode_term(inet, fst, port(fst_node, 1), scope, vars, global_vars, dups)?;
       link_local(inet, port(fst_node, 1), fst);
 
       let snd_node = new_node(inet, OP2);
-      link(inet, port(fst_node, 1), port(snd_node, 0));
+      link(inet, port(fst_node, 2), port(snd_node, 0));
+
       let snd = encode_term(inet, snd, port(snd_node, 1), scope, vars, global_vars, dups)?;
       link_local(inet, port(snd_node, 1), snd);
 
@@ -298,13 +322,15 @@ fn compat_tree_to_hvm_tree(inet: &INet, root: NodeId, port_to_var_id: &mut HashM
       rgt: Box::new(var_or_subtree(inet, port(root, 2), port_to_var_id)),
     },
     REF => LTree::Ref { nam: DefId(label).to_internal() },
-    #[cfg(feature = "nums")]
     NUM => LTree::Num { val: label as u32 },
-    #[cfg(feature = "nums")]
     OP2 => LTree::Op2 {
       lft: Box::new(var_or_subtree(inet, port(root, 1), port_to_var_id)),
       rgt: Box::new(var_or_subtree(inet, port(root, 2), port_to_var_id)),
     },
+    ITE => LTree::Ite {
+      sel: Box::new(var_or_subtree(inet, port(root, 1), port_to_var_id)),
+      ret: Box::new(var_or_subtree(inet, port(root, 2), port_to_var_id)),
+    },
     _ => unreachable!("Invalid tag in compat tree {tag:x}"),
   }
 }

tests/golden_tests/compile_single_files/example.golden

@@ -0,0 +1,29 @@
+@1 (Def1) =
+  a
+  & (@7 a) ~ @6
+@2 (Def2) =
+  a
+  & (@1 a) ~ @8
+@3 (def3) =
+  a
+  & (@B a) ~ @9
+@4 (def4) =
+  ([(a b) c] b)
+  & (c a) ~ @C
+@5 (Main) =
+  a
+  & (#1 a) ~ @2
+@6 (Def1$0) =
+  (a a)
+@7 (Def1$1) =
+  (a a)
+@8 (Def2$0) =
+  (a a)
+@9 (def3$0) =
+  (a a)
+@A (def3$1) =
+  (a a)
+@B (def3$2) =
+  (* @A)
+@C (def4$0) =
+  ([a {2 b {3 c {4 d (d (c (b (a e))))}}}] e)

tests/golden_tests/compile_single_files/nums/add_negative.golden

@@ -1,5 +0,0 @@
-1 (Main) =
-  $ a
-  & {+ -2 a}
-  ~ +1
-  

tests/golden_tests/compile_single_files/nums/add_negative.hvm

@@ -1 +0,0 @@
-(Main) = (+ +1 -2)

tests/golden_tests/compile_single_files/nums/example.golden

@@ -1,25 +0,0 @@
-1 (Def1) =
-  $ a
-  & (0 (0 b b) a)
-  ~ (0 c c)
-  
-2 (Def2) =
-  $ a
-  & (0 @1 a)
-  ~ (0 b b)
-  
-3 (def3) =
-  $ a
-  & (0 (0 * (0 b b)) a)
-  ~ (0 c c)
-  
-4 (def4) =
-  $ (0 (1 (0 a b) c) b)
-  & (0 c a)
-  ~ (0 (2 d (3 e (4 f (5 g (0 g (0 f (0 e (0 d h)))))))) h)
-  
-5 (Main) =
-  $ a
-  & (0 1 a)
-  ~ @2
-  

tests/golden_tests/compile_single_terms/addition.golden

@@ -0,0 +1,4 @@
+a
+& (#8 a) ~ (b c)
+& <d <b c>> ~ #1
+& <#1 <#1 d>> ~ #1

tests/golden_tests/compile_single_terms/addition.hvm

@@ -0,0 +1 @@
+λx (+ (+ 1 1) x) 8

tests/golden_tests/compile_single_terms/if.golden

@@ -0,0 +1,2 @@
+a
+& <#0 <#1 ? ((b (c b)) (d (e e))) a>> ~ #1

tests/golden_tests/compile_single_terms/if.hvm

@@ -0,0 +1 @@
+if (+ 0 1) then λt λf t else λt λf f

tests/golden_tests/compile_single_terms/nums/signed.hvm

@@ -1 +0,0 @@
-(+ -31 +2)

tests/golden_tests/compile_single_terms/op2.golden

@@ -0,0 +1,11 @@
+a
+& <b <#11 a>> ~ #1
+& <c <#10 b>> ~ #2
+& <d <#9 c>> ~ #3
+& <e <#8 d>> ~ #4
+& <f <#7 e>> ~ #15
+& <g <#6 f>> ~ #14
+& <h <#5 g>> ~ #8
+& <i <#4 h>> ~ #9
+& <j <#3 i>> ~ #11
+& <#1 <#2 j>> ~ #10

tests/golden_tests/readback_lnet/addition.hvm

@@ -0,0 +1,2 @@
+a
+& <#2 <#1 a>> ~ #1

tests/golden_tests/readback_lnet/nums/addition.hvm

@@ -1,3 +0,0 @@
-$ a
-& {+ 1 a}
-~ 2

tests/golden_tests/readback_lnet/nums/signed.golden

@@ -1 +0,0 @@
-(+ -31 +2)

tests/golden_tests/readback_lnet/nums/signed.hvm

@@ -1,3 +0,0 @@
-$ a
-& {+ +2 a}
-~ -31

tests/golden_tests/run_single_files/if.golden

@@ -0,0 +1,2 @@
+Invalid readback
+λa λb a

tests/golden_tests/run_single_files/if.hvm

@@ -0,0 +1 @@
+Main = if (+ 0 1) then λt λf t else λt λf f

tests/golden_tests/run_single_files/nums/add_negative.golden

@@ -1 +0,0 @@
--1

tests/golden_tests/run_single_files/nums/add_negative.hvm

@@ -1 +0,0 @@
-(Main) = (+ +1 -2)