diff --git a/Cargo.toml b/Cargo.toml index 323015b0..d4040117 100644 --- a/Cargo.toml +++ b/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" diff --git a/src/ast/compat.rs b/src/ast/compat.rs index 41a79d61..3f6ffe81 100644 --- a/src/ast/compat.rs +++ b/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; -#[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 { match value { 0x1 => Some(Op::ADD), diff --git a/src/ast/hvm_lang.rs b/src/ast/hvm_lang.rs index 98d25f8f..82e769e2 100644 --- a/src/ast/hvm_lang.rs +++ b/src/ast/hvm_lang.rs @@ -32,7 +32,6 @@ pub struct Rule { pub enum Pattern { Ctr(Name, Vec), Var(Option), - #[cfg(feature = "nums")] Num(u32), } @@ -66,6 +65,11 @@ pub enum Term { fun: Box, arg: Box, }, + If { + cond: Box, + then: Box, + els_: Box, + }, Dup { fst: Option, snd: Option, @@ -77,11 +81,9 @@ pub enum Term { snd: Box, }, 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}"), } } diff --git a/src/from_core/mod.rs b/src/from_core/mod.rs index b842c605..b60489aa 100644 --- a/src/from_core/mod.rs +++ b/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: <ree, 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), diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs index ed0c3df9..9afd7a67 100644 --- a/src/parser/lexer.rs +++ b/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, "+"), diff --git a/src/parser/parser.rs b/src/parser/parser.rs index 2c24404e..127e2558 100644 --- a/src/parser/parser.rs +++ b/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 Result>> { 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>> 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()) diff --git a/src/semantic/combinators.rs b/src/semantic/combinators.rs index 1a640a1f..dded7d57 100644 --- a/src/semantic/combinators.rs +++ b/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, } } diff --git a/src/semantic/pattern/flatten.rs b/src/semantic/pattern/flatten.rs index 2b5c10f7..70a7756e 100644 --- a/src/semantic/pattern/flatten.rs +++ b/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()); } diff --git a/src/semantic/pattern/mod.rs b/src/semantic/pattern/mod.rs index 3217c3c7..dca30790 100644 --- a/src/semantic/pattern/mod.rs +++ b/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, } diff --git a/src/semantic/pattern/type_inference.rs b/src/semantic/pattern/type_inference.rs index 044c2564..793f06ac 100644 --- a/src/semantic/pattern/type_inference.rs +++ b/src/semantic/pattern/type_inference.rs @@ -4,13 +4,16 @@ use anyhow::anyhow; use itertools::Itertools; use std::collections::HashMap; +type Adts = HashMap; +type Types = Vec>; + 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, Vec>)> { + 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"), } } diff --git a/src/semantic/vars.rs b/src/semantic/vars.rs index 180fb40d..a1a87498 100644 --- a/src/semantic/vars.rs +++ b/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) } diff --git a/src/to_core/compat_net.rs b/src/to_core/compat_net.rs index 2e8c83d5..0e263bba 100644 --- a/src/to_core/compat_net.rs +++ b/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 ~ > 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}"), } } diff --git a/tests/golden_tests/compile_single_files/example.golden b/tests/golden_tests/compile_single_files/example.golden new file mode 100644 index 00000000..173f3b26 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/tests/golden_tests/compile_single_files/nums/example.hvm b/tests/golden_tests/compile_single_files/example.hvm similarity index 100% rename from tests/golden_tests/compile_single_files/nums/example.hvm rename to tests/golden_tests/compile_single_files/example.hvm diff --git a/tests/golden_tests/compile_single_files/nums/add_negative.golden b/tests/golden_tests/compile_single_files/nums/add_negative.golden deleted file mode 100644 index d6b0fb4c..00000000 --- a/tests/golden_tests/compile_single_files/nums/add_negative.golden +++ /dev/null @@ -1,5 +0,0 @@ -1 (Main) = - $ a - & {+ -2 a} - ~ +1 - \ No newline at end of file diff --git a/tests/golden_tests/compile_single_files/nums/add_negative.hvm b/tests/golden_tests/compile_single_files/nums/add_negative.hvm deleted file mode 100644 index 899b3a65..00000000 --- a/tests/golden_tests/compile_single_files/nums/add_negative.hvm +++ /dev/null @@ -1 +0,0 @@ -(Main) = (+ +1 -2) \ No newline at end of file diff --git a/tests/golden_tests/compile_single_files/nums/example.golden b/tests/golden_tests/compile_single_files/nums/example.golden deleted file mode 100644 index 2bdad15f..00000000 --- a/tests/golden_tests/compile_single_files/nums/example.golden +++ /dev/null @@ -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 - \ No newline at end of file diff --git a/tests/golden_tests/compile_single_terms/addition.golden b/tests/golden_tests/compile_single_terms/addition.golden new file mode 100644 index 00000000..a49ce800 --- /dev/null +++ b/tests/golden_tests/compile_single_terms/addition.golden @@ -0,0 +1,4 @@ +a +& (#8 a) ~ (b c) +& > ~ #1 +& <#1 <#1 d>> ~ #1 \ No newline at end of file diff --git a/tests/golden_tests/compile_single_terms/addition.hvm b/tests/golden_tests/compile_single_terms/addition.hvm new file mode 100644 index 00000000..c42085bf --- /dev/null +++ b/tests/golden_tests/compile_single_terms/addition.hvm @@ -0,0 +1 @@ +λx (+ (+ 1 1) x) 8 \ No newline at end of file diff --git a/tests/golden_tests/compile_single_terms/if.golden b/tests/golden_tests/compile_single_terms/if.golden new file mode 100644 index 00000000..7f8a1518 --- /dev/null +++ b/tests/golden_tests/compile_single_terms/if.golden @@ -0,0 +1,2 @@ +a +& <#0 <#1 ? ((b (c b)) (d (e e))) a>> ~ #1 \ No newline at end of file diff --git a/tests/golden_tests/compile_single_terms/if.hvm b/tests/golden_tests/compile_single_terms/if.hvm new file mode 100644 index 00000000..aeedb644 --- /dev/null +++ b/tests/golden_tests/compile_single_terms/if.hvm @@ -0,0 +1 @@ +if (+ 0 1) then λt λf t else λt λf f \ No newline at end of file diff --git a/tests/golden_tests/compile_single_terms/nums/signed.hvm b/tests/golden_tests/compile_single_terms/nums/signed.hvm deleted file mode 100644 index c6be2721..00000000 --- a/tests/golden_tests/compile_single_terms/nums/signed.hvm +++ /dev/null @@ -1 +0,0 @@ -(+ -31 +2) \ No newline at end of file diff --git a/tests/golden_tests/compile_single_terms/op2.golden b/tests/golden_tests/compile_single_terms/op2.golden new file mode 100644 index 00000000..6b151c74 --- /dev/null +++ b/tests/golden_tests/compile_single_terms/op2.golden @@ -0,0 +1,11 @@ +a +& > ~ #1 +& > ~ #2 +& > ~ #3 +& > ~ #4 +& > ~ #15 +& > ~ #14 +& > ~ #8 +& > ~ #9 +& > ~ #11 +& <#1 <#2 j>> ~ #10 \ No newline at end of file diff --git a/tests/golden_tests/compile_single_terms/nums/op2.hvm b/tests/golden_tests/compile_single_terms/op2.hvm similarity index 100% rename from tests/golden_tests/compile_single_terms/nums/op2.hvm rename to tests/golden_tests/compile_single_terms/op2.hvm diff --git a/tests/golden_tests/readback_lnet/nums/addition.golden b/tests/golden_tests/readback_lnet/addition.golden similarity index 100% rename from tests/golden_tests/readback_lnet/nums/addition.golden rename to tests/golden_tests/readback_lnet/addition.golden diff --git a/tests/golden_tests/readback_lnet/addition.hvm b/tests/golden_tests/readback_lnet/addition.hvm new file mode 100644 index 00000000..200cbda2 --- /dev/null +++ b/tests/golden_tests/readback_lnet/addition.hvm @@ -0,0 +1,2 @@ +a +& <#2 <#1 a>> ~ #1 \ No newline at end of file diff --git a/tests/golden_tests/readback_lnet/nums/addition.hvm b/tests/golden_tests/readback_lnet/nums/addition.hvm deleted file mode 100644 index f0d4df51..00000000 --- a/tests/golden_tests/readback_lnet/nums/addition.hvm +++ /dev/null @@ -1,3 +0,0 @@ -$ a -& {+ 1 a} -~ 2 \ No newline at end of file diff --git a/tests/golden_tests/readback_lnet/nums/signed.golden b/tests/golden_tests/readback_lnet/nums/signed.golden deleted file mode 100644 index c6be2721..00000000 --- a/tests/golden_tests/readback_lnet/nums/signed.golden +++ /dev/null @@ -1 +0,0 @@ -(+ -31 +2) \ No newline at end of file diff --git a/tests/golden_tests/readback_lnet/nums/signed.hvm b/tests/golden_tests/readback_lnet/nums/signed.hvm deleted file mode 100644 index da7e5bab..00000000 --- a/tests/golden_tests/readback_lnet/nums/signed.hvm +++ /dev/null @@ -1,3 +0,0 @@ -$ a -& {+ +2 a} -~ -31 diff --git a/tests/golden_tests/run_single_files/nums/addition.golden b/tests/golden_tests/run_single_files/addition.golden similarity index 100% rename from tests/golden_tests/run_single_files/nums/addition.golden rename to tests/golden_tests/run_single_files/addition.golden diff --git a/tests/golden_tests/run_single_files/nums/addition.hvm b/tests/golden_tests/run_single_files/addition.hvm similarity index 100% rename from tests/golden_tests/run_single_files/nums/addition.hvm rename to tests/golden_tests/run_single_files/addition.hvm diff --git a/tests/golden_tests/run_single_files/nums/example.golden b/tests/golden_tests/run_single_files/example.golden similarity index 100% rename from tests/golden_tests/run_single_files/nums/example.golden rename to tests/golden_tests/run_single_files/example.golden diff --git a/tests/golden_tests/run_single_files/nums/example.hvm b/tests/golden_tests/run_single_files/example.hvm similarity index 100% rename from tests/golden_tests/run_single_files/nums/example.hvm rename to tests/golden_tests/run_single_files/example.hvm diff --git a/tests/golden_tests/run_single_files/if.golden b/tests/golden_tests/run_single_files/if.golden new file mode 100644 index 00000000..70ae05fe --- /dev/null +++ b/tests/golden_tests/run_single_files/if.golden @@ -0,0 +1,2 @@ +Invalid readback +λa λb a \ No newline at end of file diff --git a/tests/golden_tests/run_single_files/if.hvm b/tests/golden_tests/run_single_files/if.hvm new file mode 100644 index 00000000..f147cc34 --- /dev/null +++ b/tests/golden_tests/run_single_files/if.hvm @@ -0,0 +1 @@ +Main = if (+ 0 1) then λt λf t else λt λf f \ No newline at end of file diff --git a/tests/golden_tests/run_single_files/nums/add_negative.golden b/tests/golden_tests/run_single_files/nums/add_negative.golden deleted file mode 100644 index d7d17fcb..00000000 --- a/tests/golden_tests/run_single_files/nums/add_negative.golden +++ /dev/null @@ -1 +0,0 @@ --1 \ No newline at end of file diff --git a/tests/golden_tests/run_single_files/nums/add_negative.hvm b/tests/golden_tests/run_single_files/nums/add_negative.hvm deleted file mode 100644 index 899b3a65..00000000 --- a/tests/golden_tests/run_single_files/nums/add_negative.hvm +++ /dev/null @@ -1 +0,0 @@ -(Main) = (+ +1 -2) \ No newline at end of file diff --git a/tests/golden_tests/run_single_files/nums/queue.golden b/tests/golden_tests/run_single_files/queue.golden similarity index 100% rename from tests/golden_tests/run_single_files/nums/queue.golden rename to tests/golden_tests/run_single_files/queue.golden diff --git a/tests/golden_tests/run_single_files/nums/queue.hvm b/tests/golden_tests/run_single_files/queue.hvm similarity index 100% rename from tests/golden_tests/run_single_files/nums/queue.hvm rename to tests/golden_tests/run_single_files/queue.hvm