From 0647ea9bc7f657364cd87db6b7674796b4daf027 Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Fri, 15 Mar 2024 18:51:25 -0300 Subject: [PATCH] implicits args and stuff --- .gitignore | 1 + book/.hvm/Cargo.lock | 16 + book/.hvm/Cargo.toml | 31 + book/.hvm/src/ast.rs | 799 ++++++++++ book/.hvm/src/fns.rs | 355 +++++ book/.hvm/src/jit.rs | 452 ++++++ book/.hvm/src/lib.rs | 14 + book/.hvm/src/main.rs | 256 +++ book/.hvm/src/run.rs | 1389 +++++++++++++++++ book/.hvm/src/u60.rs | 113 ++ book/.hvm/target/.rustc_info.json | 1 + book/.hvm/target/CACHEDIR.TAG | 3 + book/.hvm/target/release/.cargo-lock | 0 .../invoked.timestamp | 1 + .../hvm-core-5d3b356175a8b321/output-lib-hvmc | 5 + .../dep-lib-nohash-hasher | Bin 0 -> 8 bytes .../invoked.timestamp | 1 + .../lib-nohash-hasher | 1 + .../lib-nohash-hasher.json | 1 + .../release/deps/hvmc-5d3b356175a8b321.d | 12 + .../libnohash_hasher-dc8a50f19f38f70e.rlib | Bin 0 -> 23504 bytes .../libnohash_hasher-dc8a50f19f38f70e.rmeta | Bin 0 -> 21101 bytes .../deps/nohash_hasher-dc8a50f19f38f70e.d | 7 + book/Bool.and.kind2 | 8 +- book/Bool.false.kind2 | 2 +- book/Bool.lemma.notnot.kind2 | 2 +- book/Equal.apply.kind2 | 3 +- book/List.Church.cons.kind2 | 3 + book/List.Church.kind2 | 5 + book/List.Church.nil.kind2 | 3 + book/List.Folder.cons.kind2 | 5 - book/List.Folder.kind2 | 7 - book/List.Folder.nil.kind2 | 3 - book/List.cons.kind2 | 5 +- book/List.fold.kind2 | 14 +- book/List.map.kind2 | 16 + book/List.nil.kind2 | 5 +- book/Nat.lemma.bft.kind2 | 2 +- book/_main.hvm2 | 21 + book/_main.hvmc | 17 + book/_main.kind2 | 38 +- book/_tmp.hvm2 | 14 + book/_tmp.kind2 | 19 + kind2.ts | 436 ------ package.json | 22 - src/book/compile.rs | 2 +- src/book/mod.rs | 14 + src/book/parse.rs | 87 +- src/main.rs | 39 +- src/sugar/mod.rs | 112 +- src/term/compile.rs | 48 +- src/term/mod.rs | 245 ++- src/term/parse.rs | 102 +- src/term/show.rs | 6 +- 54 files changed, 4079 insertions(+), 684 deletions(-) create mode 100644 book/.hvm/Cargo.lock create mode 100644 book/.hvm/Cargo.toml create mode 100644 book/.hvm/src/ast.rs create mode 100644 book/.hvm/src/fns.rs create mode 100644 book/.hvm/src/jit.rs create mode 100644 book/.hvm/src/lib.rs create mode 100644 book/.hvm/src/main.rs create mode 100644 book/.hvm/src/run.rs create mode 100644 book/.hvm/src/u60.rs create mode 100644 book/.hvm/target/.rustc_info.json create mode 100644 book/.hvm/target/CACHEDIR.TAG create mode 100644 book/.hvm/target/release/.cargo-lock create mode 100644 book/.hvm/target/release/.fingerprint/hvm-core-5d3b356175a8b321/invoked.timestamp create mode 100644 book/.hvm/target/release/.fingerprint/hvm-core-5d3b356175a8b321/output-lib-hvmc create mode 100644 book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/dep-lib-nohash-hasher create mode 100644 book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/invoked.timestamp create mode 100644 book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/lib-nohash-hasher create mode 100644 book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/lib-nohash-hasher.json create mode 100644 book/.hvm/target/release/deps/hvmc-5d3b356175a8b321.d create mode 100644 book/.hvm/target/release/deps/libnohash_hasher-dc8a50f19f38f70e.rlib create mode 100644 book/.hvm/target/release/deps/libnohash_hasher-dc8a50f19f38f70e.rmeta create mode 100644 book/.hvm/target/release/deps/nohash_hasher-dc8a50f19f38f70e.d create mode 100644 book/List.Church.cons.kind2 create mode 100644 book/List.Church.kind2 create mode 100644 book/List.Church.nil.kind2 delete mode 100644 book/List.Folder.cons.kind2 delete mode 100644 book/List.Folder.kind2 delete mode 100644 book/List.Folder.nil.kind2 create mode 100644 book/List.map.kind2 create mode 100644 book/_main.hvm2 create mode 100644 book/_main.hvmc create mode 100644 book/_tmp.hvm2 create mode 100644 book/_tmp.kind2 delete mode 100755 kind2.ts delete mode 100644 package.json diff --git a/.gitignore b/.gitignore index a58c2a9fc..50f3795aa 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,4 @@ demo/ .fill.tmp .check.hs guide.txt +.hvm diff --git a/book/.hvm/Cargo.lock b/book/.hvm/Cargo.lock new file mode 100644 index 000000000..15bca0d60 --- /dev/null +++ b/book/.hvm/Cargo.lock @@ -0,0 +1,16 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "hvm-core" +version = "0.2.18" +dependencies = [ + "nohash-hasher", +] + +[[package]] +name = "nohash-hasher" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2bf50223579dc7cdcfb3bfcacf7069ff68243f8c363f62ffa99cf000a6b9c451" diff --git a/book/.hvm/Cargo.toml b/book/.hvm/Cargo.toml new file mode 100644 index 000000000..0374a49cb --- /dev/null +++ b/book/.hvm/Cargo.toml @@ -0,0 +1,31 @@ +[package] +name = "hvm-core" +version = "0.2.18" +edition = "2021" +description = "HVM-Core is a massively parallel Interaction Combinator evaluator." +license = "MIT" + +[[bin]] +name = "hvmc" +path = "src/main.rs" +bench = false + +[lib] +name = "hvmc" +path = "src/lib.rs" +bench = false + +[profile.release] +codegen-units = 1 +lto = "fat" +opt-level = 3 +panic = "abort" + +[features] +default = [] +hvm_cli_options = [] +lazy_mode = [] + +[dependencies] +nohash-hasher = "0.2.0" + diff --git a/book/.hvm/src/ast.rs b/book/.hvm/src/ast.rs new file mode 100644 index 000000000..a6c3a601e --- /dev/null +++ b/book/.hvm/src/ast.rs @@ -0,0 +1,799 @@ +// An interaction combinator language +// ---------------------------------- +// This file implements a textual syntax to interact with the runtime. It includes a pure AST for +// nets, as well as functions for parsing, stringifying, and converting pure ASTs to runtime nets. +// On the runtime, a net is represented by a list of active trees, plus a root tree. The textual +// syntax reflects this representation. The grammar is specified on this repo's README. + +use crate::run; +use std::collections::BTreeMap; +use std::collections::HashMap; +use std::collections::HashSet; +use std::iter::Peekable; +use std::str::Chars; + +// AST +// --- + +#[derive(Clone, Hash, PartialEq, Eq, Debug)] +pub enum Tree { + Era, + Con { lft: Box, rgt: Box }, + Tup { lft: Box, rgt: Box }, + Dup { lab: run::Lab, lft: Box, rgt: Box }, + Var { nam: String }, + Ref { nam: run::Val }, + Num { val: run::Val }, + Op1 { opr: run::Lab, lft: run::Val, rgt: Box }, + Op2 { opr: run::Lab, lft: Box, rgt: Box }, + Mat { sel: Box, ret: Box }, +} + +type Redex = Vec<(Tree, Tree)>; + +#[derive(Clone, Hash, PartialEq, Eq, Debug)] +pub struct Net { + pub root: Tree, + pub rdex: Redex, +} + +pub type Book = BTreeMap; + +// Parser +// ------ + +// FIXME: remove after skip is fixed +fn skip_spaces(chars: &mut Peekable) { + while let Some(c) = chars.peek() { + if !c.is_ascii_whitespace() { + break; + } else { + chars.next(); + } + } +} + +// FIXME: detect two '/' for comments, allowing us to remove 'skip_spaces' +fn skip(chars: &mut Peekable) { + while let Some(c) = chars.peek() { + if *c == '/' { + chars.next(); + while let Some(c) = chars.peek() { + if *c == '\n' { + break; + } + chars.next(); + } + } else if !c.is_ascii_whitespace() { + break; + } else { + chars.next(); + } + } +} + +pub fn consume(chars: &mut Peekable, text: &str) -> Result<(), String> { + skip(chars); + for c in text.chars() { + if chars.next() != Some(c) { + return Err(format!("Expected '{}', found {:?}", text, chars.peek())); + } + } + return Ok(()); +} + +pub fn parse_decimal(chars: &mut Peekable) -> Result { + let mut num: u64 = 0; + skip(chars); + if !chars.peek().map_or(false, |c| c.is_digit(10)) { + return Err(format!("Expected a decimal number, found {:?}", chars.peek())); + } + while let Some(c) = chars.peek() { + if !c.is_digit(10) { + break; + } + num = num * 10 + c.to_digit(10).unwrap() as u64; + chars.next(); + } + Ok(num) +} + +pub fn parse_name(chars: &mut Peekable) -> Result { + let mut txt = String::new(); + skip(chars); + if !chars.peek().map_or(false, |c| c.is_alphanumeric() || *c == '_' || *c == '.') { + return Err(format!("Expected a name character, found {:?}", chars.peek())) + } + while let Some(c) = chars.peek() { + if !c.is_alphanumeric() && *c != '_' && *c != '.' { + break; + } + txt.push(*c); + chars.next(); + } + Ok(txt) +} + +pub fn parse_opx_lit(chars: &mut Peekable) -> Result { + let mut opx = String::new(); + skip_spaces(chars); + while let Some(c) = chars.peek() { + if !"+-=*/%<>|&^!?".contains(*c) { + break; + } + opx.push(*c); + chars.next(); + } + Ok(opx) +} + +fn parse_opr(chars: &mut Peekable) -> Result { + let opx = parse_opx_lit(chars)?; + match opx.as_str() { + "+" => Ok(run::ADD), + "-" => Ok(run::SUB), + "*" => Ok(run::MUL), + "/" => Ok(run::DIV), + "%" => Ok(run::MOD), + "==" => Ok(run::EQ), + "!=" => Ok(run::NE), + "<" => Ok(run::LT), + ">" => Ok(run::GT), + "<=" => Ok(run::LTE), + ">=" => Ok(run::GTE), + "&&" => Ok(run::AND), + "||" => Ok(run::OR), + "^" => Ok(run::XOR), + "!" => Ok(run::NOT), + "<<" => Ok(run::LSH), + ">>" => Ok(run::RSH), + _ => Err(format!("Unknown operator: {}", opx)), + } +} + +pub fn parse_tree(chars: &mut Peekable) -> Result { + skip(chars); + match chars.peek() { + Some('*') => { + chars.next(); + Ok(Tree::Era) + } + Some('(') => { + chars.next(); + let lft = Box::new(parse_tree(chars)?); + let rgt = Box::new(parse_tree(chars)?); + consume(chars, ")")?; + Ok(Tree::Con { lft, rgt }) + } + Some('[') => { + chars.next(); + let lab = 1; + let lft = Box::new(parse_tree(chars)?); + let rgt = Box::new(parse_tree(chars)?); + consume(chars, "]")?; + Ok(Tree::Tup { lft, rgt }) + } + Some('{') => { + chars.next(); + let lab = parse_decimal(chars)? as run::Lab; + let lft = Box::new(parse_tree(chars)?); + let rgt = Box::new(parse_tree(chars)?); + consume(chars, "}")?; + Ok(Tree::Dup { lab, lft, rgt }) + } + Some('@') => { + chars.next(); + skip(chars); + let name = parse_name(chars)?; + Ok(Tree::Ref { nam: name_to_val(&name) }) + } + Some('#') => { + chars.next(); + Ok(Tree::Num { val: parse_decimal(chars)? }) + } + Some('<') => { + chars.next(); + if chars.peek().map_or(false, |c| c.is_digit(10)) { + let lft = parse_decimal(chars)?; + let opr = parse_opr(chars)?; + let rgt = Box::new(parse_tree(chars)?); + consume(chars, ">")?; + Ok(Tree::Op1 { opr, lft, rgt }) + } else { + let opr = parse_opr(chars)?; + let lft = Box::new(parse_tree(chars)?); + let rgt = Box::new(parse_tree(chars)?); + consume(chars, ">")?; + Ok(Tree::Op2 { opr, lft, rgt }) + } + } + Some('?') => { + chars.next(); + consume(chars, "<")?; + let sel = Box::new(parse_tree(chars)?); + let ret = Box::new(parse_tree(chars)?); + consume(chars, ">")?; + Ok(Tree::Mat { sel, ret }) + } + _ => { + Ok(Tree::Var { nam: parse_name(chars)? }) + }, + } +} + +pub fn parse_net(chars: &mut Peekable) -> Result { + let mut rdex = Vec::new(); + let root = parse_tree(chars)?; + while let Some(c) = { skip(chars); chars.peek() } { + if *c == '&' { + chars.next(); + let tree1 = parse_tree(chars)?; + consume(chars, "~")?; + let tree2 = parse_tree(chars)?; + rdex.push((tree1, tree2)); + } else { + break; + } + } + Ok(Net { root, rdex }) +} + +pub fn parse_book(chars: &mut Peekable) -> Result { + let mut book = BTreeMap::new(); + while let Some(c) = { skip(chars); chars.peek() } { + if *c == '@' { + chars.next(); + let name = parse_name(chars)?; + consume(chars, "=")?; + let net = parse_net(chars)?; + book.insert(name, net); + } else { + break; + } + } + Ok(book) +} + +fn do_parse(code: &str, parse_fn: impl Fn(&mut Peekable) -> Result) -> T { + let chars = &mut code.chars().peekable(); + match parse_fn(chars) { + Ok(result) => { + if chars.next().is_none() { + result + } else { + eprintln!("Unable to parse the whole input. Is this not an hvmc file?"); + std::process::exit(1); + } + } + Err(err) => { + eprintln!("{}", err); + std::process::exit(1); + } + } +} + +pub fn do_parse_tree(code: &str) -> Tree { + do_parse(code, parse_tree) +} + +pub fn do_parse_net(code: &str) -> Net { + do_parse(code, parse_net) +} + +pub fn do_parse_book(code: &str) -> Book { + do_parse(code, parse_book) +} + +// Stringifier +// ----------- + +pub fn show_opr(opr: run::Lab) -> String { + match opr { + run::ADD => "+".to_string(), + run::SUB => "-".to_string(), + run::MUL => "*".to_string(), + run::DIV => "/".to_string(), + run::MOD => "%".to_string(), + run::EQ => "==".to_string(), + run::NE => "!=".to_string(), + run::LT => "<".to_string(), + run::GT => ">".to_string(), + run::LTE => "<=".to_string(), + run::GTE => ">=".to_string(), + run::AND => "&&".to_string(), + run::OR => "||".to_string(), + run::XOR => "^".to_string(), + run::NOT => "!".to_string(), + run::LSH => "<<".to_string(), + run::RSH => ">>".to_string(), + _ => panic!("Unknown operator label."), + } +} + +pub fn show_tree(tree: &Tree) -> String { + match tree { + Tree::Era => { + "*".to_string() + } + Tree::Con { lft, rgt } => { + format!("({} {})", show_tree(&*lft), show_tree(&*rgt)) + } + Tree::Tup { lft, rgt } => { + format!("[{} {}]", show_tree(&*lft), show_tree(&*rgt)) + } + Tree::Dup { lab, lft, rgt } => { + format!("{{{} {} {}}}", lab, show_tree(&*lft), show_tree(&*rgt)) + } + Tree::Var { nam } => { + nam.clone() + } + Tree::Ref { nam } => { + format!("@{}", val_to_name(*nam)) + } + Tree::Num { val } => { + format!("#{}", (*val).to_string()) + } + Tree::Op1 { opr, lft, rgt } => { + format!("<{}{} {}>", lft, show_opr(*opr), show_tree(rgt)) + } + Tree::Op2 { opr, lft, rgt } => { + format!("<{} {} {}>", show_opr(*opr), show_tree(&*lft), show_tree(&*rgt)) + } + Tree::Mat { sel, ret } => { + format!("?<{} {}>", show_tree(&*sel), show_tree(&*ret)) + } + } +} + +pub fn show_net(net: &Net) -> String { + let mut result = String::new(); + result.push_str(&format!("{}", show_tree(&net.root))); + for (a, b) in &net.rdex { + result.push_str(&format!("\n& {} ~ {}", show_tree(a), show_tree(b))); + } + return result; +} + +pub fn show_book(book: &Book) -> String { + let mut result = String::new(); + for (name, net) in book { + result.push_str(&format!("@{} = {}\n", name, show_net(net))); + } + return result; +} + +pub fn show_runtime_tree(rt_net: &run::NetFields, ptr: run::Ptr) -> String where [(); LAZY as usize]:{ + show_tree(&tree_from_runtime_go(rt_net, ptr, PARENT_ROOT, &mut HashMap::new(), &mut 0)) +} + +pub fn show_runtime_net(rt_net: &run::NetFields) -> String where [(); LAZY as usize]:{ + show_net(&net_from_runtime(rt_net)) +} + +pub fn show_runtime_book(book: &run::Book) -> String { + show_book(&book_from_runtime(book)) +} + +// Conversion +// ---------- + +pub fn num_to_str(mut num: usize) -> String { + let mut txt = String::new(); + num += 1; + while num > 0 { + num -= 1; + let c = ((num % 26) as u8 + b'a') as char; + txt.push(c); + num /= 26; + } + return txt.chars().rev().collect(); +} + +pub const fn tag_to_port(tag: run::Tag) -> run::Port { + match tag { + run::VR1 => run::P1, + run::VR2 => run::P2, + _ => unreachable!(), + } +} + +pub fn port_to_tag(port: run::Port) -> run::Tag { + match port { + run::P1 => run::VR1, + run::P2 => run::VR2, + _ => unreachable!(), + } +} + +pub fn name_to_letters(name: &str) -> Vec { + let mut letters = Vec::new(); + for c in name.chars() { + letters.push(match c { + '0'..='9' => c as u8 - '0' as u8 + 0, + 'A'..='Z' => c as u8 - 'A' as u8 + 10, + 'a'..='z' => c as u8 - 'a' as u8 + 36, + '_' => 62, + '.' => 63, + _ => panic!("Invalid character in name"), + }); + } + return letters; +} + +pub fn letters_to_name(letters: Vec) -> String { + let mut name = String::new(); + for letter in letters { + name.push(match letter { + 0..= 9 => (letter - 0 + '0' as u8) as char, + 10..=35 => (letter - 10 + 'A' as u8) as char, + 36..=61 => (letter - 36 + 'a' as u8) as char, + 62 => '_', + 63 => '.', + _ => panic!("Invalid letter in name"), + }); + } + return name; +} + +pub fn val_to_letters(num: run::Val) -> Vec { + let mut letters = Vec::new(); + let mut num = num; + while num > 0 { + letters.push((num % 64) as u8); + num /= 64; + } + letters.reverse(); + return letters; +} + +pub fn letters_to_val(letters: Vec) -> run::Val { + let mut num = 0; + for letter in letters { + num = num * 64 + letter as run::Val; + } + return num; +} + +pub fn name_to_val(name: &str) -> run::Val { + letters_to_val(name_to_letters(name)) +} + +pub fn val_to_name(num: run::Val) -> String { + letters_to_name(val_to_letters(num)) +} + +// Injection and Readback +// ---------------------- + +// To runtime + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +pub enum Parent { + Redex, + Node { loc: run::Loc, port: run::Port }, +} +const PARENT_ROOT: Parent = Parent::Node { loc: run::ROOT.loc(), port: tag_to_port(run::ROOT.tag()) }; + +pub fn tree_to_runtime_go(rt_net: &mut run::NetFields, tree: &Tree, vars: &mut HashMap, parent: Parent) -> run::Ptr where [(); LAZY as usize]: { + match tree { + Tree::Era => { + run::ERAS + } + Tree::Con { lft, rgt } => { + let loc = rt_net.alloc(); + let p1 = tree_to_runtime_go(rt_net, &*lft, vars, Parent::Node { loc, port: run::P1 }); + rt_net.heap.set(loc, run::P1, p1); + let p2 = tree_to_runtime_go(rt_net, &*rgt, vars, Parent::Node { loc, port: run::P2 }); + rt_net.heap.set(loc, run::P2, p2); + run::Ptr::new(run::LAM, 0, loc) + } + Tree::Tup { lft, rgt } => { + let loc = rt_net.alloc(); + let p1 = tree_to_runtime_go(rt_net, &*lft, vars, Parent::Node { loc, port: run::P1 }); + rt_net.heap.set(loc, run::P1, p1); + let p2 = tree_to_runtime_go(rt_net, &*rgt, vars, Parent::Node { loc, port: run::P2 }); + rt_net.heap.set(loc, run::P2, p2); + run::Ptr::new(run::TUP, 1, loc) + } + Tree::Dup { lab, lft, rgt } => { + let loc = rt_net.alloc(); + let p1 = tree_to_runtime_go(rt_net, &*lft, vars, Parent::Node { loc, port: run::P1 }); + rt_net.heap.set(loc, run::P1, p1); + let p2 = tree_to_runtime_go(rt_net, &*rgt, vars, Parent::Node { loc, port: run::P2 }); + rt_net.heap.set(loc, run::P2, p2); + run::Ptr::new(run::DUP, *lab, loc) + } + Tree::Var { nam } => { + if let Parent::Redex = parent { + panic!("By definition, can't have variable on active pairs."); + }; + match vars.get(nam) { + Some(Parent::Redex) => { + unreachable!(); + } + Some(Parent::Node { loc: other_loc, port: other_port }) => { + match parent { + Parent::Redex => { unreachable!(); } + Parent::Node { loc, port } => rt_net.heap.set(*other_loc, *other_port, run::Ptr::new(port_to_tag(port), 0, loc)), + } + return run::Ptr::new(port_to_tag(*other_port), 0, *other_loc); + } + None => { + vars.insert(nam.clone(), parent); + run::NULL + } + } + } + Tree::Ref { nam } => { + run::Ptr::big(run::REF, *nam) + } + Tree::Num { val } => { + run::Ptr::big(run::NUM, *val) + } + Tree::Op1 { opr, lft, rgt } => { + let loc = rt_net.alloc(); + let p1 = run::Ptr::big(run::NUM, *lft); + rt_net.heap.set(loc, run::P1, p1); + let p2 = tree_to_runtime_go(rt_net, rgt, vars, Parent::Node { loc, port: run::P2 }); + rt_net.heap.set(loc, run::P2, p2); + run::Ptr::new(run::OP1, *opr, loc) + } + Tree::Op2 { opr, lft, rgt } => { + let loc = rt_net.alloc(); + let p1 = tree_to_runtime_go(rt_net, &*lft, vars, Parent::Node { loc, port: run::P1 }); + rt_net.heap.set(loc, run::P1, p1); + let p2 = tree_to_runtime_go(rt_net, &*rgt, vars, Parent::Node { loc, port: run::P2 }); + rt_net.heap.set(loc, run::P2, p2); + run::Ptr::new(run::OP2, *opr, loc) + } + Tree::Mat { sel, ret } => { + let loc = rt_net.alloc(); + let p1 = tree_to_runtime_go(rt_net, &*sel, vars, Parent::Node { loc, port: run::P1 }); + rt_net.heap.set(loc, run::P1, p1); + let p2 = tree_to_runtime_go(rt_net, &*ret, vars, Parent::Node { loc, port: run::P2 }); + rt_net.heap.set(loc, run::P2, p2); + run::Ptr::new(run::MAT, 0, loc) + } + } +} + +pub fn tree_to_runtime(rt_net: &mut run::NetFields, tree: &Tree) -> run::Ptr where [(); LAZY as usize]: { + tree_to_runtime_go(rt_net, tree, &mut HashMap::new(), PARENT_ROOT) +} + +pub fn net_to_runtime(rt_net: &mut run::NetFields, net: &Net) where [(); LAZY as usize]: { + let mut vars = HashMap::new(); + let root = tree_to_runtime_go(rt_net, &net.root, &mut vars, PARENT_ROOT); + rt_net.heap.set_root(root); + for (tree1, tree2) in &net.rdex { + let ptr1 = tree_to_runtime_go(rt_net, tree1, &mut vars, Parent::Redex); + let ptr2 = tree_to_runtime_go(rt_net, tree2, &mut vars, Parent::Redex); + rt_net.rdex.push((ptr1, ptr2)); + } +} + +// Holds dup labels and ref ids used by a definition +type InsideLabs = HashSet>; +type InsideRefs = HashSet; +#[derive(Debug)] +pub struct Inside { + labs: InsideLabs, + refs: InsideRefs, +} + +// Collects dup labels and ref ids used by a definition +pub fn runtime_def_get_inside(def: &run::Def) -> Inside { + let mut inside = Inside { + labs: HashSet::with_hasher(std::hash::BuildHasherDefault::default()), + refs: HashSet::new(), + }; + fn register(inside: &mut Inside, ptr: run::Ptr) { + if ptr.is_dup() { + inside.labs.insert(ptr.lab()); + } + if ptr.is_ref() { + inside.refs.insert(ptr.val()); + } + } + for i in 0 .. def.node.len() { + register(&mut inside, def.node[i].1); + register(&mut inside, def.node[i].2); + } + for i in 0 .. def.rdex.len() { + register(&mut inside, def.rdex[i].0); + register(&mut inside, def.rdex[i].1); + } + return inside; +} + +// Computes all dup labels used by a definition, direct or not. +// FIXME: memoize to avoid duplicated work +pub fn runtime_def_get_all_labs(labs: &mut InsideLabs, insides: &HashMap, fid: run::Val, seen: &mut HashSet) { + if seen.contains(&fid) { + return; + } else { + seen.insert(fid); + if let Some(fid_insides) = insides.get(&fid) { + for dup in &fid_insides.labs { + labs.insert(*dup); + } + for child_fid in &fid_insides.refs { + runtime_def_get_all_labs(labs, insides, *child_fid, seen); + } + } + } +} + +// Converts a book from the pure AST representation to the runtime representation. +pub fn book_to_runtime(book: &Book) -> run::Book { + let mut rt_book = run::Book::new(); + + // Convert each net in 'book' to a runtime net and add to 'rt_book' + for (name, net) in book { + let fid = name_to_val(name); + let nodes = run::Heap::::init(1 << 16); + let mut rt = run::NetFields::new(&nodes); + net_to_runtime(&mut rt, net); + rt_book.def(fid, runtime_net_to_runtime_def(&rt)); + } + + // Calculate the 'insides' of each runtime definition + let mut insides = HashMap::new(); + for (fid, def) in &rt_book.defs { + insides.insert(*fid, runtime_def_get_inside(&def)); + } + + // Compute labs labels used in each runtime definition + let mut labs_by_fid = HashMap::new(); + for (fid, _) in &rt_book.defs { + let mut labs = HashSet::with_hasher(std::hash::BuildHasherDefault::default()); + let mut seen = HashSet::new(); + runtime_def_get_all_labs(&mut labs, &insides, *fid, &mut seen); + labs_by_fid.insert(*fid, labs); + } + + // Set the 'labs' field for each definition + for (fid, def) in &mut rt_book.defs { + def.labs = labs_by_fid.get(fid).unwrap().clone(); + //println!("{} {:?}", val_to_name(*fid), def.labs); + } + + rt_book +} + +// Converts to a def. +pub fn runtime_net_to_runtime_def(net: &run::NetFields) -> run::Def where [(); LAZY as usize]: { + let mut node = vec![]; + let mut rdex = vec![]; + let labs = HashSet::with_hasher(std::hash::BuildHasherDefault::default()); + for i in 0 .. net.heap.nodes.len() { + let p0 = run::APtr::new(run::Ptr(0)); + let p1 = net.heap.get(node.len() as run::Loc, run::P1); + let p2 = net.heap.get(node.len() as run::Loc, run::P2); + if p1 != run::NULL || p2 != run::NULL { + node.push(((), p1, p2)); + } else { + break; + } + } + for i in 0 .. net.rdex.len() { + let p1 = net.rdex[i].0; + let p2 = net.rdex[i].1; + rdex.push((p1, p2)); + } + return run::Def { labs, rdex, node }; +} + +// Reads back from a def. +pub fn runtime_def_to_runtime_net<'a, const LAZY: bool>(nodes: &'a run::Nodes, def: &run::Def) -> run::NetFields<'a, LAZY> where [(); LAZY as usize]: { + let mut net = run::NetFields::new(&nodes); + for (i, &(p0, p1, p2)) in def.node.iter().enumerate() { + net.heap.set(i as run::Loc, run::P1, p1); + net.heap.set(i as run::Loc, run::P2, p2); + } + net.rdex = def.rdex.clone(); + net +} + +pub fn tree_from_runtime_go(rt_net: &run::NetFields, ptr: run::Ptr, parent: Parent, vars: &mut HashMap, fresh: &mut usize) -> Tree where [(); LAZY as usize]: { + match ptr.tag() { + run::ERA => { + Tree::Era + } + run::REF => { + Tree::Ref { nam: ptr.val() } + } + run::NUM => { + Tree::Num { val: ptr.val() } + } + run::OP1 => { + let opr = ptr.lab(); + let lft = tree_from_runtime_go(rt_net, rt_net.heap.get(ptr.loc(), run::P1), Parent::Node { loc: ptr.loc(), port: run::P1 }, vars, fresh); + let Tree::Num { val } = lft else { unreachable!() }; + let rgt = tree_from_runtime_go(rt_net, rt_net.heap.get(ptr.loc(), run::P2), Parent::Node { loc: ptr.loc(), port: run::P2 }, vars, fresh); + Tree::Op1 { opr, lft: val, rgt: Box::new(rgt) } + } + run::OP2 => { + let opr = ptr.lab(); + let lft = tree_from_runtime_go(rt_net, rt_net.heap.get(ptr.loc(), run::P1), Parent::Node { loc: ptr.loc(), port: run::P1 }, vars, fresh); + let rgt = tree_from_runtime_go(rt_net, rt_net.heap.get(ptr.loc(), run::P2), Parent::Node { loc: ptr.loc(), port: run::P2 }, vars, fresh); + Tree::Op2 { opr, lft: Box::new(lft), rgt: Box::new(rgt) } + } + run::MAT => { + let sel = tree_from_runtime_go(rt_net, rt_net.heap.get(ptr.loc(), run::P1), Parent::Node { loc: ptr.loc(), port: run::P1 }, vars, fresh); + let ret = tree_from_runtime_go(rt_net, rt_net.heap.get(ptr.loc(), run::P2), Parent::Node { loc: ptr.loc(), port: run::P2 }, vars, fresh); + Tree::Mat { sel: Box::new(sel), ret: Box::new(ret) } + } + run::VR1 | run::VR2 => { + let key = match ptr.tag() { + run::VR1 => Parent::Node { loc: ptr.loc(), port: run::P1 }, + run::VR2 => Parent::Node { loc: ptr.loc(), port: run::P2 }, + _ => unreachable!(), + }; + if let Some(nam) = vars.get(&key) { + Tree::Var { nam: nam.clone() } + } else { + let nam = num_to_str(*fresh); + *fresh += 1; + vars.insert(parent, nam.clone()); + Tree::Var { nam } + } + } + run::LAM => { + let p1 = rt_net.heap.get(ptr.loc(), run::P1); + let p2 = rt_net.heap.get(ptr.loc(), run::P2); + let lft = tree_from_runtime_go(rt_net, p1, Parent::Node { loc: ptr.loc(), port: run::P1 }, vars, fresh); + let rgt = tree_from_runtime_go(rt_net, p2, Parent::Node { loc: ptr.loc(), port: run::P2 }, vars, fresh); + Tree::Con { lft: Box::new(lft), rgt: Box::new(rgt) } + } + run::TUP => { + let p1 = rt_net.heap.get(ptr.loc(), run::P1); + let p2 = rt_net.heap.get(ptr.loc(), run::P2); + let lft = tree_from_runtime_go(rt_net, p1, Parent::Node { loc: ptr.loc(), port: run::P1 }, vars, fresh); + let rgt = tree_from_runtime_go(rt_net, p2, Parent::Node { loc: ptr.loc(), port: run::P2 }, vars, fresh); + Tree::Tup { lft: Box::new(lft), rgt: Box::new(rgt) } + } + run::DUP => { + let p1 = rt_net.heap.get(ptr.loc(), run::P1); + let p2 = rt_net.heap.get(ptr.loc(), run::P2); + let lft = tree_from_runtime_go(rt_net, p1, Parent::Node { loc: ptr.loc(), port: run::P1 }, vars, fresh); + let rgt = tree_from_runtime_go(rt_net, p2, Parent::Node { loc: ptr.loc(), port: run::P2 }, vars, fresh); + Tree::Dup { lab: ptr.lab(), lft: Box::new(lft), rgt: Box::new(rgt) } + } + _ => { + unreachable!() + } + } +} + +pub fn tree_from_runtime(rt_net: &run::NetFields, ptr: run::Ptr) -> Tree where [(); LAZY as usize]: { + let mut vars = HashMap::new(); + let mut fresh = 0; + tree_from_runtime_go(rt_net, ptr, PARENT_ROOT, &mut vars, &mut fresh) +} + +pub fn net_from_runtime(rt_net: &run::NetFields) -> Net where [(); LAZY as usize]: { + let mut vars = HashMap::new(); + let mut fresh = 0; + let mut rdex = Vec::new(); + let root = tree_from_runtime_go(rt_net, rt_net.heap.get_root(), PARENT_ROOT, &mut vars, &mut fresh); + for &(a, b) in &rt_net.rdex { + let tree_a = tree_from_runtime_go(rt_net, a, Parent::Redex, &mut vars, &mut fresh); + let tree_b = tree_from_runtime_go(rt_net, b, Parent::Redex, &mut vars, &mut fresh); + rdex.push((tree_a, tree_b)); + } + Net { root, rdex } +} + +pub fn book_from_runtime(rt_book: &run::Book) -> Book { + let mut book = BTreeMap::new(); + for (fid, def) in rt_book.defs.iter() { + if def.node.len() > 0 { + let name = val_to_name(*fid); + let nodes = run::Heap::::init(def.node.len()); + let net = net_from_runtime(&runtime_def_to_runtime_net(&nodes, &def)); + book.insert(name, net); + } + } + book +} diff --git a/book/.hvm/src/fns.rs b/book/.hvm/src/fns.rs new file mode 100644 index 000000000..848c4b97f --- /dev/null +++ b/book/.hvm/src/fns.rs @@ -0,0 +1,355 @@ +use crate::run::{*}; + +pub const F___main : Val = 0xfbec24b31; +pub const F___foo : Val = 0x3efa9cb2; +pub const F_main : Val = 0xc24b31; +pub const F_a : Val = 0x000024; +pub const F__U60.fib : Val = 0xf9e180fe9b25; +pub const F_b : Val = 0x000025; +pub const F_d : Val = 0x000027; +pub const F_c : Val = 0x000026; + +impl<'a, const LAZY: bool> NetFields<'a, LAZY> where [(); LAZY as usize]: { + + pub fn call_native(&mut self, book: &Book, ptr: Ptr, x: Ptr) -> bool { + match ptr.val() { + F___main => { return self.F___main(ptr, Trg::Ptr(x)); } + F___foo => { return self.F___foo(ptr, Trg::Ptr(x)); } + F_main => { return self.F_main(ptr, Trg::Ptr(x)); } + F_a => { return self.F_a(ptr, Trg::Ptr(x)); } + F__U60.fib => { return self.F__U60.fib(ptr, Trg::Ptr(x)); } + F_b => { return self.F_b(ptr, Trg::Ptr(x)); } + F_d => { return self.F_d(ptr, Trg::Ptr(x)); } + F_c => { return self.F_c(ptr, Trg::Ptr(x)); } + _ => { return false; } + } + } + + pub fn L___main(&mut self, lab: Lab) -> bool { + if lab == 0x5 { return true; } + if lab == 0x3 { return true; } + return false; + } + pub fn F___main(&mut self, ptr: Ptr, trg: Trg) -> bool { + if self.get(trg).is_dup() && !self.L___main(self.get(trg).lab()) { + self.copy(self.swap(trg, NULL), ptr); + return true; + } + let _k1 : Trg = Trg::Ptr(Ptr::big(REF, F__U60.fib)); + let _k1x : Trg; + let _k1y : Trg; + // fast apply + if self.get(_k1).tag() == LAM { + self.rwts.anni += 1; + let got = self.swap(_k1, NULL); + _k1x = Trg::Dir(Ptr::new(VR1, 0, got.loc())); + _k1y = Trg::Dir(Ptr::new(VR2, 0, got.loc())); + } else { + let k2 = self.alloc(); + _k1x = Trg::Ptr(Ptr::new(VR1, 0, k2)); + _k1y = Trg::Ptr(Ptr::new(VR2, 0, k2)); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k2)), _k1); + } + // fast erase + if self.get(_k1x).is_skp() { + self.swap(_k1x, NULL); + self.rwts.eras += 1; + } else { + self.safe_link(_k1x, Trg::Ptr(Ptr::new(NUM, 0x6, 0x0))); + } + self.safe_link(trg, _k1y); + return true; + } + + pub fn L___foo(&mut self, lab: Lab) -> bool { + return false; + } + pub fn F___foo(&mut self, ptr: Ptr, trg: Trg) -> bool { + if self.get(trg).is_dup() && !self.L___foo(self.get(trg).lab()) { + self.copy(self.swap(trg, NULL), ptr); + return true; + } + // fast erase + if self.get(trg).is_skp() { + self.swap(trg, NULL); + self.rwts.eras += 1; + } else { + self.safe_link(trg, Trg::Ptr(Ptr::new(NUM, 0x2d, 0x0))); + } + return true; + } + + pub fn L_main(&mut self, lab: Lab) -> bool { + if lab == 0x5 { return true; } + if lab == 0x3 { return true; } + return false; + } + pub fn F_main(&mut self, ptr: Ptr, trg: Trg) -> bool { + if self.get(trg).is_dup() && !self.L_main(self.get(trg).lab()) { + self.copy(self.swap(trg, NULL), ptr); + return true; + } + self.safe_link(trg, Trg::Ptr(Ptr::big(REF, F___main))); + return true; + } + + pub fn L_a(&mut self, lab: Lab) -> bool { + if lab == 0x5 { return true; } + if lab == 0x3 { return true; } + return false; + } + pub fn F_a(&mut self, ptr: Ptr, trg: Trg) -> bool { + if self.get(trg).is_dup() && !self.L_a(self.get(trg).lab()) { + self.copy(self.swap(trg, NULL), ptr); + return true; + } + let trgx : Trg; + let trgy : Trg; + // fast apply + if self.get(trg).tag() == LAM { + self.rwts.anni += 1; + let got = self.swap(trg, NULL); + trgx = Trg::Dir(Ptr::new(VR1, 0, got.loc())); + trgy = Trg::Dir(Ptr::new(VR2, 0, got.loc())); + } else { + let k1 = self.alloc(); + trgx = Trg::Ptr(Ptr::new(VR1, 0, k1)); + trgy = Trg::Ptr(Ptr::new(VR2, 0, k1)); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k1)), trg); + } + let trgxx : Trg; + let trgxy : Trg; + // fast copy + if self.get(trgx).tag() == NUM { + self.rwts.comm += 1; + let got = self.swap(trgx, NULL); + trgxx = Trg::Ptr(got); + trgxy = Trg::Ptr(got); + } else { + let k2 = self.alloc(); + trgxx = Trg::Ptr(Ptr::new(VR1, 0, k2)); + trgxy = Trg::Ptr(Ptr::new(VR2, 0, k2)); + self.safe_link(Trg::Ptr(Ptr::new(DUP, 3, k2)), trgx); + } + let k3 = self.alloc(); + let k4 = self.alloc(); + self.safe_link(Trg::Ptr(Ptr::new(VR2, 0, k4)), trgy); + self.safe_link(Trg::Ptr(Ptr::new(VR1, 0, k4)), trgxy); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k4)), Trg::Ptr(Ptr::new(VR2, 0, k3))); + let k5 = self.alloc(); + self.safe_link(Trg::Ptr(Ptr::new(VR2, 0, k5)), Trg::Ptr(Ptr::big(REF, F_b))); + self.safe_link(Trg::Ptr(Ptr::new(VR1, 0, k5)), Trg::Ptr(Ptr::big(REF, F_d))); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k5)), Trg::Ptr(Ptr::new(VR1, 0, k3))); + self.safe_link(Trg::Ptr(Ptr::new(MAT, 0, k3)), trgxx); + return true; + } + + pub fn L__U60.fib(&mut self, lab: Lab) -> bool { + if lab == 0x5 { return true; } + if lab == 0x3 { return true; } + return false; + } + pub fn F__U60.fib(&mut self, ptr: Ptr, trg: Trg) -> bool { + if self.get(trg).is_dup() && !self.L__U60.fib(self.get(trg).lab()) { + self.copy(self.swap(trg, NULL), ptr); + return true; + } + let k1 : Trg; + let k2 : Trg; + // fast match + if self.get(trg).tag() == LAM && self.heap.get(self.get(trg).loc(), P1).is_num() { + self.rwts.anni += 2; + self.rwts.oper += 1; + let got = self.swap(trg, NULL); + let trgx = Trg::Dir(Ptr::new(VR1, 0, got.loc())); + let trgy = Trg::Dir(Ptr::new(VR2, 0, got.loc())); + if self.get(trgx).val() == 0 { + self.swap(trgx, NULL); + k1 = trgy; + k2 = Trg::Ptr(ERAS); + } else { + self.swap(trgx, Ptr::big(NUM, self.get(trgx).val() - 1)); + k1 = Trg::Ptr(ERAS); + k2 = trg; + } + } else { + let k3 = self.alloc(); + let k4 = self.alloc(); + let k5 = self.alloc(); + self.heap.set(k3, P1, Ptr::new(MAT, 0, k4)); + self.heap.set(k3, P2, Ptr::new(VR2, 0, k4)); + self.heap.set(k4, P1, Ptr::new(LAM, 0, k5)); + self.heap.set(k4, P2, Ptr::new(VR2, 0, k3)); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k3)), trg); + k1 = Trg::Ptr(Ptr::new(VR1, 0, k5)); + k2 = Trg::Ptr(Ptr::new(VR2, 0, k5)); + } + // fast erase + if self.get(k1).is_skp() { + self.swap(k1, NULL); + self.rwts.eras += 1; + } else { + self.safe_link(k1, Trg::Ptr(Ptr::new(NUM, 0x0, 0x0))); + } + self.safe_link(k2, Trg::Ptr(Ptr::big(REF, F_a))); + return true; + } + + pub fn L_b(&mut self, lab: Lab) -> bool { + if lab == 0x5 { return true; } + if lab == 0x3 { return true; } + return false; + } + pub fn F_b(&mut self, ptr: Ptr, trg: Trg) -> bool { + if self.get(trg).is_dup() && !self.L_b(self.get(trg).lab()) { + self.copy(self.swap(trg, NULL), ptr); + return true; + } + let trgx : Trg; + let trgy : Trg; + // fast apply + if self.get(trg).tag() == LAM { + self.rwts.anni += 1; + let got = self.swap(trg, NULL); + trgx = Trg::Dir(Ptr::new(VR1, 0, got.loc())); + trgy = Trg::Dir(Ptr::new(VR2, 0, got.loc())); + } else { + let k1 = self.alloc(); + trgx = Trg::Ptr(Ptr::new(VR1, 0, k1)); + trgy = Trg::Ptr(Ptr::new(VR2, 0, k1)); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k1)), trg); + } + self.safe_link(trgy, Trg::Ptr(Ptr::big(REF, F_c))); + // fast erase + if self.get(trgx).is_skp() { + self.swap(trgx, NULL); + self.rwts.eras += 1; + } else { + self.safe_link(trgx, Trg::Ptr(Ptr::new(ERA, 0x0, 0x0))); + } + return true; + } + + pub fn L_d(&mut self, lab: Lab) -> bool { + return false; + } + pub fn F_d(&mut self, ptr: Ptr, trg: Trg) -> bool { + if self.get(trg).is_dup() && !self.L_d(self.get(trg).lab()) { + self.copy(self.swap(trg, NULL), ptr); + return true; + } + let trgx : Trg; + let trgy : Trg; + // fast apply + if self.get(trg).tag() == LAM { + self.rwts.anni += 1; + let got = self.swap(trg, NULL); + trgx = Trg::Dir(Ptr::new(VR1, 0, got.loc())); + trgy = Trg::Dir(Ptr::new(VR2, 0, got.loc())); + } else { + let k1 = self.alloc(); + trgx = Trg::Ptr(Ptr::new(VR1, 0, k1)); + trgy = Trg::Ptr(Ptr::new(VR2, 0, k1)); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k1)), trg); + } + // fast erase + if self.get(trgy).is_skp() { + self.swap(trgy, NULL); + self.rwts.eras += 1; + } else { + self.safe_link(trgy, Trg::Ptr(Ptr::new(NUM, 0x1, 0x0))); + } + // fast erase + if self.get(trgx).is_skp() { + self.swap(trgx, NULL); + self.rwts.eras += 1; + } else { + self.safe_link(trgx, Trg::Ptr(Ptr::new(ERA, 0x0, 0x0))); + } + return true; + } + + pub fn L_c(&mut self, lab: Lab) -> bool { + if lab == 0x5 { return true; } + if lab == 0x3 { return true; } + return false; + } + pub fn F_c(&mut self, ptr: Ptr, trg: Trg) -> bool { + if self.get(trg).is_dup() && !self.L_c(self.get(trg).lab()) { + self.copy(self.swap(trg, NULL), ptr); + return true; + } + let _k1 : Trg = Trg::Ptr(Ptr::big(REF, F__U60.fib)); + let _k1x : Trg; + let _k1y : Trg; + // fast apply + if self.get(_k1).tag() == LAM { + self.rwts.anni += 1; + let got = self.swap(_k1, NULL); + _k1x = Trg::Dir(Ptr::new(VR1, 0, got.loc())); + _k1y = Trg::Dir(Ptr::new(VR2, 0, got.loc())); + } else { + let k2 = self.alloc(); + _k1x = Trg::Ptr(Ptr::new(VR1, 0, k2)); + _k1y = Trg::Ptr(Ptr::new(VR2, 0, k2)); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k2)), _k1); + } + let k3 = self.alloc(); + self.safe_link(Trg::Ptr(Ptr::new(OP2, 0, k3)), _k1y); + let _k4 : Trg = Trg::Ptr(Ptr::big(REF, F__U60.fib)); + let _k4x : Trg; + let _k4y : Trg; + // fast apply + if self.get(_k4).tag() == LAM { + self.rwts.anni += 1; + let got = self.swap(_k4, NULL); + _k4x = Trg::Dir(Ptr::new(VR1, 0, got.loc())); + _k4y = Trg::Dir(Ptr::new(VR2, 0, got.loc())); + } else { + let k5 = self.alloc(); + _k4x = Trg::Ptr(Ptr::new(VR1, 0, k5)); + _k4y = Trg::Ptr(Ptr::new(VR2, 0, k5)); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k5)), _k4); + } + self.safe_link(_k4y, Trg::Ptr(Ptr::new(VR1, 0, k3))); + let trgx : Trg; + let trgy : Trg; + // fast apply + if self.get(trg).tag() == LAM { + self.rwts.anni += 1; + let got = self.swap(trg, NULL); + trgx = Trg::Dir(Ptr::new(VR1, 0, got.loc())); + trgy = Trg::Dir(Ptr::new(VR2, 0, got.loc())); + } else { + let k6 = self.alloc(); + trgx = Trg::Ptr(Ptr::new(VR1, 0, k6)); + trgy = Trg::Ptr(Ptr::new(VR2, 0, k6)); + self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, k6)), trg); + } + self.safe_link(trgy, Trg::Ptr(Ptr::new(VR2, 0, k3))); + let trgxx : Trg; + let trgxy : Trg; + // fast copy + if self.get(trgx).tag() == NUM { + self.rwts.comm += 1; + let got = self.swap(trgx, NULL); + trgxx = Trg::Ptr(got); + trgxy = Trg::Ptr(got); + } else { + let k7 = self.alloc(); + trgxx = Trg::Ptr(Ptr::new(VR1, 0, k7)); + trgxy = Trg::Ptr(Ptr::new(VR2, 0, k7)); + self.safe_link(Trg::Ptr(Ptr::new(DUP, 5, k7)), trgx); + } + let k8 = self.alloc(); + self.safe_link(Trg::Ptr(Ptr::new(VR2, 0, k8)), _k4x); + self.safe_link(Trg::Ptr(Ptr::new(VR1, 0, k8)), Trg::Ptr(Ptr::new(NUM, 0x2, 0x0))); + self.safe_link(Trg::Ptr(Ptr::new(OP2, 1, k8)), trgxy); + let k9 = self.alloc(); + self.safe_link(Trg::Ptr(Ptr::new(VR2, 0, k9)), _k1x); + self.safe_link(Trg::Ptr(Ptr::new(VR1, 0, k9)), Trg::Ptr(Ptr::new(NUM, 0x1, 0x0))); + self.safe_link(Trg::Ptr(Ptr::new(OP2, 1, k9)), trgxx); + return true; + } + +} \ No newline at end of file diff --git a/book/.hvm/src/jit.rs b/book/.hvm/src/jit.rs new file mode 100644 index 000000000..139a86c70 --- /dev/null +++ b/book/.hvm/src/jit.rs @@ -0,0 +1,452 @@ +// Despite the file name, this is not actually a JIT (yet). + +use crate::run; +use crate::ast; + +use std::collections::HashMap; + +pub fn compile_book(book: &run::Book) -> String { + let mut code = String::new(); + + code.push_str(&format!("use crate::run::{{*}};\n")); + code.push_str(&format!("\n")); + + for (fid, def) in book.defs.iter() { + if def.node.len() > 0 { + let name = &ast::val_to_name(*fid as run::Val); + code.push_str(&format!("pub const F_{:4} : Val = 0x{:06x};\n", name, fid)); + } + } + + code.push_str(&format!("\n")); + + code.push_str(&format!("impl<'a, const LAZY: bool> NetFields<'a, LAZY> where [(); LAZY as usize]: {{\n")); + code.push_str(&format!("\n")); + + code.push_str(&format!("{}pub fn call_native(&mut self, book: &Book, ptr: Ptr, x: Ptr) -> bool {{\n", ident(1))); + code.push_str(&format!("{}match ptr.val() {{\n", ident(2))); + for (fid, def) in book.defs.iter() { + if def.node.len() > 0 { + let fun = ast::val_to_name(*fid); + code.push_str(&format!("{}F_{} => {{ return self.F_{}(ptr, Trg::Ptr(x)); }}\n", ident(3), fun, fun)); + } + } + code.push_str(&format!("{}_ => {{ return false; }}\n", ident(3))); + code.push_str(&format!("{}}}\n", ident(2))); + code.push_str(&format!("{}}}\n", ident(1))); + code.push_str(&format!("\n")); + + for (fid, def) in book.defs.iter() { + if def.node.len() > 0 { + code.push_str(&compile_term(&book, 1, *fid)); + code.push_str(&format!("\n")); + } + } + + code.push_str(&format!("}}")); + + return code; + +} + +pub fn ident(tab: usize) -> String { + return " ".repeat(tab); +} + +pub fn tag(tag: run::Tag) -> &'static str { + match tag { + run::VR1 => "VR1", + run::VR2 => "VR2", + run::RD1 => "RD1", + run::RD2 => "RD2", + run::REF => "REF", + run::ERA => "ERA", + run::NUM => "NUM", + run::OP2 => "OP2", + run::OP1 => "OP1", + run::MAT => "MAT", + run::LAM => "LAM", + run::TUP => "TUP", + run::DUP => "DUP", + _ => unreachable!(), + } +} + +pub fn atom(ptr: run::Ptr) -> String { + if ptr.is_ref() { + return format!("Ptr::big(REF, F_{})", ast::val_to_name(ptr.val())); + } else { + return format!("Ptr::new({}, 0x{:x}, 0x{:x})", tag(ptr.tag()), ptr.lab(), ptr.loc()); + } +} + +struct Target { + nam: String +} + +impl Target { + fn show(&self) -> String { + format!("{}", self.nam) + } + + fn get(&self) -> String { + format!("self.get({})", self.nam) + } + + fn swap(&self, value: &str) -> String { + format!("self.swap({}, {})", self.nam, value) + } + + fn take(&self) -> String { + self.swap(&"NULL") + } +} + +pub fn compile_term(book: &run::Book, tab: usize, fid: run::Val) -> String { + + // returns a fresh variable: 'v' + fn fresh(newx: &mut usize) -> String { + *newx += 1; + format!("k{}", newx) + } + + fn call_redex( + book : &run::Book, + tab : usize, + newx : &mut usize, + vars : &mut HashMap, + def : &run::Def, + rdex : (run::Ptr, run::Ptr), + ) -> String { + let (rf, rx) = adjust_redex(rdex.0, rdex.1); + let rf_name = format!("_{}", fresh(newx)); + let mut code = String::new(); + code.push_str(&format!("{}let {} : Trg = Trg::Ptr({});\n", ident(tab), rf_name, &atom(rf))); + code.push_str(&burn(book, tab, None, newx, vars, def, rx, &Target { nam: rf_name })); + return code; + } + + fn call( + book : &run::Book, + tab : usize, + tail : Option, + newx : &mut usize, + vars : &mut HashMap, + fid : run::Val, + trg : &Target, + ) -> String { + //let newx = &mut 0; + //let vars = &mut HashMap::new(); + + let def = &book.get(fid).unwrap(); + + // Tail call + // TODO: when I manually edited a file to implement tail call, the single-core performance + // increased a lot, but it resulted in a single thread withholding all redexes and, thus, + // the program went single-core mode again. I believe a smarter redex sharing structure is + // necessary for us to implement tail calls in a way that doesn't sacrify parallelism. + //if tail.is_some() && def.rdex.len() > 0 && def.rdex[0].0.is_ref() && def.rdex[0].0.loc() == tail.unwrap() { + //println!("tco {}", ast::val_to_name(tail.unwrap() as run::Val)); + //let mut code = String::new(); + //for rdex in &def.rdex[1..] { + //code.push_str(&call_redex(book, tab, newx, vars, def, *rdex)); + //} + //code.push_str(&burn(book, tab, Some(fid), newx, vars, def, def.node[0].1, &trg)); + //code.push_str(&call_redex(book, tab, newx, vars, def, def.rdex[0])); + //return code; + //} + + // Normal call + let mut code = String::new(); + for rdex in &def.rdex { + code.push_str(&call_redex(book, tab, newx, vars, def, *rdex)); + } + code.push_str(&burn(book, tab, Some(fid), newx, vars, def, def.node[0].2, &trg)); + return code; + } + + fn burn( + book : &run::Book, + tab : usize, + tail : Option, + newx : &mut usize, + vars : &mut HashMap, + def : &run::Def, + ptr : run::Ptr, + trg : &Target, + ) -> String { + //println!("burn {:08x} {}", ptr.0, x); + let mut code = String::new(); + + // ( ret) ~ (#X R) + // ------------------------------- fast match + // if X == 0: + // ifz ~ R + // ifs ~ * + // else: + // ifz ~ * + // ifs ~ (#(X-1) R) + // When ifs is REF, tail-call optimization is applied. + if ptr.tag() == run::LAM { + let mat = def.node[ptr.loc() as usize].1; + let rty = def.node[ptr.loc() as usize].2; + if mat.tag() == run::MAT { + let cse = def.node[mat.loc() as usize].1; + let rtx = def.node[mat.loc() as usize].2; + let got = def.node[rty.loc() as usize]; + let rtz = if rty.tag() == run::VR1 { got.1 } else { got.2 }; + if cse.tag() == run::LAM && rtx.is_var() && rtx == rtz { + let ifz = def.node[cse.loc() as usize].1; + let ifs = def.node[cse.loc() as usize].2; + let c_z = Target { nam: fresh(newx) }; + let c_s = Target { nam: fresh(newx) }; + let num = Target { nam: format!("{}x", trg.show()) }; + let res = Target { nam: format!("{}y", trg.show()) }; + let lam = fresh(newx); + let mat = fresh(newx); + let cse = fresh(newx); + code.push_str(&format!("{}let {} : Trg;\n", ident(tab), &c_z.show())); + code.push_str(&format!("{}let {} : Trg;\n", ident(tab), &c_s.show())); + code.push_str(&format!("{}// fast match\n", ident(tab))); + code.push_str(&format!("{}if {}.tag() == LAM && self.heap.get({}.loc(), P1).is_num() {{\n", ident(tab), trg.get(), trg.get())); + code.push_str(&format!("{}self.rwts.anni += 2;\n", ident(tab+1))); + code.push_str(&format!("{}self.rwts.oper += 1;\n", ident(tab+1))); + code.push_str(&format!("{}let got = {};\n", ident(tab+1), trg.take())); + code.push_str(&format!("{}let {} = Trg::Dir(Ptr::new(VR1, 0, got.loc()));\n", ident(tab+1), num.show())); + code.push_str(&format!("{}let {} = Trg::Dir(Ptr::new(VR2, 0, got.loc()));\n", ident(tab+1), res.show())); + code.push_str(&format!("{}if {}.val() == 0 {{\n", ident(tab+1), num.get())); + code.push_str(&format!("{}{};\n", ident(tab+2), num.take())); + code.push_str(&format!("{}{} = {};\n", ident(tab+2), &c_z.show(), res.show())); + code.push_str(&format!("{}{} = Trg::Ptr({});\n", ident(tab+2), &c_s.show(), "ERAS")); + code.push_str(&format!("{}}} else {{\n", ident(tab+1))); + code.push_str(&format!("{}{};\n", ident(tab+2), num.swap(&format!("Ptr::big(NUM, {}.val() - 1)", num.get())))); + code.push_str(&format!("{}{} = Trg::Ptr({});\n", ident(tab+2), &c_z.show(), "ERAS")); + code.push_str(&format!("{}{} = {};\n", ident(tab+2), &c_s.show(), trg.show())); + code.push_str(&format!("{}}}\n", ident(tab+1))); + code.push_str(&format!("{}}} else {{\n", ident(tab))); + code.push_str(&format!("{}let {} = self.alloc();\n", ident(tab+1), lam)); + code.push_str(&format!("{}let {} = self.alloc();\n", ident(tab+1), mat)); + code.push_str(&format!("{}let {} = self.alloc();\n", ident(tab+1), cse)); + code.push_str(&format!("{}self.heap.set({}, P1, Ptr::new(MAT, 0, {}));\n", ident(tab+1), lam, mat)); + code.push_str(&format!("{}self.heap.set({}, P2, Ptr::new(VR2, 0, {}));\n", ident(tab+1), lam, mat)); + code.push_str(&format!("{}self.heap.set({}, P1, Ptr::new(LAM, 0, {}));\n", ident(tab+1), mat, cse)); + code.push_str(&format!("{}self.heap.set({}, P2, Ptr::new(VR2, 0, {}));\n", ident(tab+1), mat, lam)); + code.push_str(&format!("{}self.safe_link(Trg::Ptr(Ptr::new(LAM, 0, {})), {});\n", ident(tab+1), lam, trg.show())); + code.push_str(&format!("{}{} = Trg::Ptr(Ptr::new(VR1, 0, {}));\n", ident(tab+1), &c_z.show(), cse)); + code.push_str(&format!("{}{} = Trg::Ptr(Ptr::new(VR2, 0, {}));\n", ident(tab+1), &c_s.show(), cse)); + code.push_str(&format!("{}}}\n", ident(tab))); + code.push_str(&burn(book, tab, None, newx, vars, def, ifz, &c_z)); + code.push_str(&burn(book, tab, tail, newx, vars, def, ifs, &c_s)); + return code; + } + } + } + + // #A ~ <+ #B r> + // ----------------- fast op + // r <~ #(op(+,A,B)) + if ptr.is_op2() { + let val = def.node[ptr.loc() as usize].1; + let ret = def.node[ptr.loc() as usize].2; + if let Some(val) = got(vars, def, val) { + let val = Target { nam: val }; + let nxt = Target { nam: fresh(newx) }; + let op2 = fresh(newx); + code.push_str(&format!("{}let {} : Trg;\n", ident(tab), &nxt.show())); + code.push_str(&format!("{}// fast op\n", ident(tab))); + code.push_str(&format!("{}if {}.is_num() && {}.is_num() {{\n", ident(tab), trg.get(), val.get())); + code.push_str(&format!("{}self.rwts.oper += 2;\n", ident(tab+1))); // OP2 + OP1 + code.push_str(&format!("{}let vx = {};\n", ident(tab+1), trg.take())); + code.push_str(&format!("{}let vy = {};\n", ident(tab+1), val.take())); + code.push_str(&format!("{}{} = Trg::Ptr(Ptr::big(NUM, self.op({},vx.val(),vy.val())));\n", ident(tab+1), &nxt.show(), ptr.lab())); + code.push_str(&format!("{}}} else {{\n", ident(tab))); + code.push_str(&format!("{}let {} = self.alloc();\n", ident(tab+1), op2)); + code.push_str(&format!("{}self.safe_link(Trg::Ptr(Ptr::new(VR1, 0, {})), {});\n", ident(tab+1), op2, val.show())); + code.push_str(&format!("{}self.safe_link(Trg::Ptr(Ptr::new(OP2, {}, {})), {});\n", ident(tab+1), ptr.lab(), op2, trg.show())); + code.push_str(&format!("{}{} = Trg::Ptr(Ptr::new(VR2, 0, {}));\n", ident(tab+1), &nxt.show(), op2)); + code.push_str(&format!("{}}}\n", ident(tab))); + code.push_str(&burn(book, tab, None, newx, vars, def, ret, &nxt)); + return code; + } + } + + // {p1 p2} <~ #N + // ------------- fast copy + // p1 <~ #N + // p2 <~ #N + if ptr.is_dup() { + let x1 = Target { nam: format!("{}x", trg.show()) }; + let x2 = Target { nam: format!("{}y", trg.show()) }; + let p1 = def.node[ptr.loc() as usize].1; + let p2 = def.node[ptr.loc() as usize].2; + let lc = fresh(newx); + code.push_str(&format!("{}let {} : Trg;\n", ident(tab), &x1.show())); + code.push_str(&format!("{}let {} : Trg;\n", ident(tab), &x2.show())); + code.push_str(&format!("{}// fast copy\n", ident(tab))); + code.push_str(&format!("{}if {}.tag() == NUM {{\n", ident(tab), trg.get())); + code.push_str(&format!("{}self.rwts.comm += 1;\n", ident(tab+1))); + code.push_str(&format!("{}let got = {};\n", ident(tab+1), trg.take())); + code.push_str(&format!("{}{} = Trg::Ptr(got);\n", ident(tab+1), &x1.show())); + code.push_str(&format!("{}{} = Trg::Ptr(got);\n", ident(tab+1), &x2.show())); + code.push_str(&format!("{}}} else {{\n", ident(tab))); + code.push_str(&format!("{}let {} = self.alloc();\n", ident(tab+1), lc)); + code.push_str(&format!("{}{} = Trg::Ptr(Ptr::new(VR1, 0, {}));\n", ident(tab+1), &x1.show(), lc)); + code.push_str(&format!("{}{} = Trg::Ptr(Ptr::new(VR2, 0, {}));\n", ident(tab+1), &x2.show(), lc)); + code.push_str(&format!("{}self.safe_link(Trg::Ptr(Ptr::new({}, {}, {})), {});\n", ident(tab+1), tag(ptr.tag()), ptr.lab(), lc, trg.show())); + code.push_str(&format!("{}}}\n", ident(tab))); + code.push_str(&burn(book, tab, None, newx, vars, def, p2, &x2)); + code.push_str(&burn(book, tab, None, newx, vars, def, p1, &x1)); + return code; + } + + // (p1 p2) <~ (x1 x2) + // ------------------ fast apply + // p1 <~ x1 + // p2 <~ x2 + if ptr.is_ctr() && ptr.tag() == run::LAM { + let x1 = Target { nam: format!("{}x", trg.show()) }; + let x2 = Target { nam: format!("{}y", trg.show()) }; + let p1 = def.node[ptr.loc() as usize].1; + let p2 = def.node[ptr.loc() as usize].2; + let lc = fresh(newx); + code.push_str(&format!("{}let {} : Trg;\n", ident(tab), &x1.show())); + code.push_str(&format!("{}let {} : Trg;\n", ident(tab), &x2.show())); + code.push_str(&format!("{}// fast apply\n", ident(tab))); + code.push_str(&format!("{}if {}.tag() == {} {{\n", ident(tab), trg.get(), tag(ptr.tag()))); + code.push_str(&format!("{}self.rwts.anni += 1;\n", ident(tab+1))); + code.push_str(&format!("{}let got = {};\n", ident(tab+1), trg.take())); + code.push_str(&format!("{}{} = Trg::Dir(Ptr::new(VR1, 0, got.loc()));\n", ident(tab+1), &x1.show())); + code.push_str(&format!("{}{} = Trg::Dir(Ptr::new(VR2, 0, got.loc()));\n", ident(tab+1), &x2.show())); + code.push_str(&format!("{}}} else {{\n", ident(tab))); + code.push_str(&format!("{}let {} = self.alloc();\n", ident(tab+1), lc)); + code.push_str(&format!("{}{} = Trg::Ptr(Ptr::new(VR1, 0, {}));\n", ident(tab+1), &x1.show(), lc)); + code.push_str(&format!("{}{} = Trg::Ptr(Ptr::new(VR2, 0, {}));\n", ident(tab+1), &x2.show(), lc)); + code.push_str(&format!("{}self.safe_link(Trg::Ptr(Ptr::new({}, 0, {})), {});\n", ident(tab+1), tag(ptr.tag()), lc, trg.show())); + code.push_str(&format!("{}}}\n", ident(tab))); + code.push_str(&burn(book, tab, None, newx, vars, def, p2, &x2)); + code.push_str(&burn(book, tab, None, newx, vars, def, p1, &x1)); + return code; + } + + //// TODO: implement inlining correctly + //// NOTE: enabling this makes dec_bits_tree hang; investigate + //if ptr.is_ref() && tail.is_some() { + //code.push_str(&format!("{}// inline @{}\n", ident(tab), ast::val_to_name(ptr.loc() as run::Val))); + //code.push_str(&format!("{}if !{}.is_skp() {{\n", ident(tab), trg.get())); + //code.push_str(&format!("{}self.rwts.dref += 1;\n", ident(tab+1))); + //code.push_str(&call(book, tab+1, tail, newx, &mut HashMap::new(), ptr.loc(), trg)); + //code.push_str(&format!("{}}} else {{\n", ident(tab))); + //code.push_str(&make(tab+1, newx, vars, def, ptr, &trg.show())); + //code.push_str(&format!("{}}}\n", ident(tab))); + //return code; + //} + + // ATOM <~ * + // --------- fast erase + // nothing + if ptr.is_num() || ptr.is_era() { + code.push_str(&format!("{}// fast erase\n", ident(tab))); + code.push_str(&format!("{}if {}.is_skp() {{\n", ident(tab), trg.get())); + code.push_str(&format!("{}{};\n", ident(tab+1), trg.take())); + code.push_str(&format!("{}self.rwts.eras += 1;\n", ident(tab+1))); + code.push_str(&format!("{}}} else {{\n", ident(tab))); + code.push_str(&make(tab+1, newx, vars, def, ptr, &trg.show())); + code.push_str(&format!("{}}}\n", ident(tab))); + return code; + } + + code.push_str(&make(tab, newx, vars, def, ptr, &trg.show())); + return code; + } + + fn make( + tab : usize, + newx : &mut usize, + vars : &mut HashMap, + def : &run::Def, + ptr : run::Ptr, + trg : &String, + ) -> String { + //println!("make {:08x} {}", ptr.0, x); + let mut code = String::new(); + if ptr.is_nod() { + let lc = fresh(newx); + let p1 = def.node[ptr.loc() as usize].1; + let p2 = def.node[ptr.loc() as usize].2; + code.push_str(&format!("{}let {} = self.alloc();\n", ident(tab), lc)); + code.push_str(&make(tab, newx, vars, def, p2, &format!("Trg::Ptr(Ptr::new(VR2, 0, {}))", lc))); + code.push_str(&make(tab, newx, vars, def, p1, &format!("Trg::Ptr(Ptr::new(VR1, 0, {}))", lc))); + code.push_str(&format!("{}self.safe_link(Trg::Ptr(Ptr::new({}, {}, {})), {});\n", ident(tab), tag(ptr.tag()), ptr.lab(), lc, trg)); + } else if ptr.is_var() { + match got(vars, def, ptr) { + None => { + //println!("-var fst"); + vars.insert(ptr, trg.clone()); + }, + Some(got) => { + //println!("-var snd"); + code.push_str(&format!("{}self.safe_link({}, {});\n", ident(tab), trg, got)); + } + } + } else { + code.push_str(&format!("{}self.safe_link({}, Trg::Ptr({}));\n", ident(tab), trg, atom(ptr))); + } + return code; + } + + fn got( + vars : &HashMap, + def : &run::Def, + ptr : run::Ptr, + ) -> Option { + if ptr.is_var() { + let got = def.node[ptr.loc() as usize]; + let slf = if ptr.tag() == run::VR1 { got.1 } else { got.2 }; + return vars.get(&slf).cloned(); + } else { + return None; + } + } + + let fun = ast::val_to_name(fid); + let def = &book.get(fid).unwrap(); + + let mut code = String::new(); + // Given a label, returns true if the definition contains that dup label, directly or not + code.push_str(&format!("{}pub fn L_{}(&mut self, lab: Lab) -> bool {{\n", ident(tab), fun)); + for dup in &def.labs { + code.push_str(&format!("{}if lab == 0x{:x} {{ return true; }}\n", ident(tab+1), dup)); + } + code.push_str(&format!("{}return false;\n", ident(tab+1))); + code.push_str(&format!("{}}}\n", ident(tab))); + // Calls the definition, performing inline rewrites when possible, and expanding it when not + code.push_str(&format!("{}pub fn F_{}(&mut self, ptr: Ptr, trg: Trg) -> bool {{\n", ident(tab), fun)); + code.push_str(&format!("{}if self.get(trg).is_dup() && !self.L_{}(self.get(trg).lab()) {{\n", ident(tab+1), fun)); + code.push_str(&format!("{}self.copy(self.swap(trg, NULL), ptr);\n", ident(tab+2))); + code.push_str(&format!("{}return true;\n", ident(tab+2))); + code.push_str(&format!("{}}}\n", ident(tab+1))); + code.push_str(&call(book, tab+1, None, &mut 0, &mut HashMap::new(), fid, &Target { nam: "trg".to_string() })); + code.push_str(&format!("{}return true;\n", ident(tab+1))); + code.push_str(&format!("{}}}\n", ident(tab))); + + return code; +} + +// TODO: HVM-Lang must always output in this form. +fn adjust_redex(rf: run::Ptr, rx: run::Ptr) -> (run::Ptr, run::Ptr) { + if rf.is_skp() && !rx.is_skp() { + return (rf, rx); + } else if !rf.is_skp() && rx.is_skp() { + return (rx, rf); + } else { + println!("Invalid redex. Compiled HVM requires that ALL defs are in the form:"); + println!("@name = ROOT"); + println!(" & ATOM ~ TERM"); + println!(" & ATOM ~ TERM"); + println!(" & ATOM ~ TERM"); + println!(" ..."); + println!("Where ATOM must be either a ref (`@foo`), a num (`#123`), or an era (`*`)."); + println!("If you used HVM-Lang, please report on https://github.com/HigherOrderCO/hvm-lang."); + panic!("Invalid HVMC file."); + } +} diff --git a/book/.hvm/src/lib.rs b/book/.hvm/src/lib.rs new file mode 100644 index 000000000..6912fad47 --- /dev/null +++ b/book/.hvm/src/lib.rs @@ -0,0 +1,14 @@ +#![feature(generic_const_exprs)] +#![allow(incomplete_features)] + +#![allow(dead_code)] +#![allow(unused_variables)] +#![allow(unused_imports)] +#![allow(non_snake_case)] +#![allow(non_upper_case_globals)] + +pub mod ast; +pub mod fns; +pub mod jit; +pub mod run; +pub mod u60; diff --git a/book/.hvm/src/main.rs b/book/.hvm/src/main.rs new file mode 100644 index 000000000..58b8bf196 --- /dev/null +++ b/book/.hvm/src/main.rs @@ -0,0 +1,256 @@ +#![feature(generic_const_exprs)] +#![allow(incomplete_features)] + +#![allow(dead_code)] +#![allow(non_snake_case)] +#![allow(non_upper_case_globals)] +#![allow(unused_imports)] +#![allow(unused_variables)] + +use std::env; +use std::fs; + +use hvmc::ast; +use hvmc::fns; +use hvmc::jit; +use hvmc::run; +use hvmc::u60; + +use std::collections::HashSet; + +struct Args { + func: String, + argm: String, + opts: HashSet, +} + +fn get_args() -> Args { + let args: Vec = env::args().collect(); + let func = args.get(1).unwrap_or(&"help".to_string()).to_string(); + let argm = args.get(2).unwrap_or(&"".to_string()).to_string(); + let opts = args.iter().skip(3).map(|s| s.to_string()).collect::>(); + return Args { func, argm, opts }; +} + +// Runs 'main' without showing the CLI options +fn run_without_cli(args: Args) { + let lazy = args.opts.contains("-L"); + let seq = lazy || args.opts.contains("-1"); + let file = args.argm; + let book = run::Book::new(); + let mut net = run::Net::new(1 << 28, false); + let begin = std::time::Instant::now(); + if lazy { todo!() } + if seq { + net.normal(&book); + } else { + net.parallel_normal(&book); + } + println!("{}", net.show()); + print_stats(&net, begin); +} + +fn run_with_cli(args: Args) -> Result<(), Box> { + let lazy = args.opts.contains("-L"); + let seq = lazy || args.opts.contains("-1"); + match args.func.as_str() { + "run" => { + if args.argm.len() > 0 { + let file = args.argm; + let book = load_book(&file); + let mut net = run::Net::new(1 << 28, lazy); + let begin = std::time::Instant::now(); + if seq { + net.normal(&book); + } else { + net.parallel_normal(&book); + } + //println!("{}", net.show()); + println!("{}", net.show()); + if args.opts.contains("-s") { + print_stats(&net, begin); + } + } else { + println!("Usage: hvmc run [-s]"); + std::process::exit(1); + } + } + "compile" => { + if args.argm.len() > 0 { + let file = args.argm; + let book = load_book(&file); + let net = run::Net::new(1 << 28, lazy); + let begin = std::time::Instant::now(); + compile_book_to_rust_crate(&file, &book)?; + compile_rust_crate_to_executable(&file)?; + } else { + println!("Usage: hvmc compile "); + std::process::exit(1); + } + } + "gen-cuda-book" => { + if args.argm.len() > 0 { + let file = args.argm; + let book = load_book(&file); + let net = run::Net::new(1 << 28, lazy); + let begin = std::time::Instant::now(); + println!("{}", gen_cuda_book(&book)); + } else { + println!("Usage: hvmc gen-cuda-book "); + std::process::exit(1); + } + } + _ => { + println!("Usage: hvmc [-s]"); + println!("Commands:"); + println!(" run - Run the given file"); + println!(" compile - Compile the given file to an executable"); + println!(" gen-cuda-book - Generate a CUDA book from the given file"); + println!("Options:"); + println!(" [-s] Show stats, including rewrite count"); + println!(" [-1] Single-core mode (no parallelism)"); + } + } + Ok(()) +} + +#[cfg(not(feature = "hvm_cli_options"))] +fn main() { + run_without_cli(get_args()) +} + +#[cfg(feature = "hvm_cli_options")] +fn main() -> Result<(), Box> { + run_with_cli(get_args()) +} + +fn print_stats(net: &run::Net, begin: std::time::Instant) { + let rewrites = net.get_rewrites(); + println!("RWTS : {}", rewrites.total()); + println!("- ANNI : {}", rewrites.anni); + println!("- COMM : {}", rewrites.comm); + println!("- ERAS : {}", rewrites.eras); + println!("- DREF : {}", rewrites.dref); + println!("- OPER : {}", rewrites.oper); + println!("TIME : {:.3} s", (begin.elapsed().as_millis() as f64) / 1000.0); + println!("RPS : {:.3} m", (rewrites.total() as f64) / (begin.elapsed().as_millis() as f64) / 1000.0); +} + +// Load file +fn load_book(file: &str) -> run::Book { + let Ok(file) = fs::read_to_string(file) else { + eprintln!("Input file not found"); + std::process::exit(1); + }; + return ast::book_to_runtime(&ast::do_parse_book(&file)); +} + +pub fn compile_book_to_rust_crate(f_name: &str, book: &run::Book) -> Result<(), std::io::Error> { + let fns_rs = jit::compile_book(book); + let outdir = ".hvm"; + if std::path::Path::new(&outdir).exists() { + fs::remove_dir_all(&outdir)?; + } + let cargo_toml = include_str!("../Cargo.toml"); + let cargo_toml = cargo_toml.split("##--COMPILER-CUTOFF--##").next().unwrap(); + let cargo_toml = cargo_toml.replace("\"hvm_cli_options\"", ""); + fs::create_dir_all(&format!("{}/src", outdir))?; + fs::write(".hvm/Cargo.toml", cargo_toml)?; + fs::write(".hvm/src/ast.rs", include_str!("../src/ast.rs"))?; + fs::write(".hvm/src/jit.rs", include_str!("../src/jit.rs"))?; + fs::write(".hvm/src/lib.rs", include_str!("../src/lib.rs"))?; + fs::write(".hvm/src/main.rs", include_str!("../src/main.rs"))?; + fs::write(".hvm/src/run.rs", include_str!("../src/run.rs"))?; + fs::write(".hvm/src/u60.rs", include_str!("../src/u60.rs"))?; + fs::write(".hvm/src/fns.rs", fns_rs)?; + return Ok(()); +} + +pub fn compile_rust_crate_to_executable(f_name: &str) -> Result<(), std::io::Error> { + let output = std::process::Command::new("cargo").current_dir("./.hvm").arg("build").arg("--release").output()?; + let target = format!("./{}", f_name.replace(".hvmc", "")); + if std::path::Path::new(&target).exists() { + fs::remove_file(&target)?; + } + fs::copy("./.hvm/target/release/hvmc", target)?; + return Ok(()); +} + +// TODO: move to hvm-cuda repo +pub fn gen_cuda_book(book: &run::Book) -> String { + use std::collections::BTreeMap; + + // Sort the book.defs by key + let mut defs = BTreeMap::new(); + for (fid, def) in book.defs.iter() { + if def.node.len() > 0 { + defs.insert(fid, def.clone()); + } + } + + // Initializes code + let mut code = String::new(); + + // Generate function ids + for (i, id) in defs.keys().enumerate() { + code.push_str(&format!("const u32 F_{} = 0x{:x};\n", crate::ast::val_to_name(**id), id)); + } + code.push_str("\n"); + + // Create book + code.push_str("u32 BOOK_DATA[] = {\n"); + + // Generate book data + for (i, (id, net)) in defs.iter().enumerate() { + let node_len = net.node.len(); + let rdex_len = net.rdex.len(); + + code.push_str(&format!(" // @{}\n", crate::ast::val_to_name(**id))); + + // Collect all pointers from root, nodes and rdex into a single buffer + code.push_str(&format!(" // .nlen\n")); + code.push_str(&format!(" 0x{:08X},\n", node_len)); + code.push_str(&format!(" // .rlen\n")); + code.push_str(&format!(" 0x{:08X},\n", rdex_len)); + + // .node + code.push_str(" // .node\n"); + for (i, node) in net.node.iter().enumerate() { + code.push_str(&format!(" 0x{:08X},", node.1.0)); + code.push_str(&format!(" 0x{:08X},", node.2.0)); + if (i + 1) % 4 == 0 { + code.push_str("\n"); + } + } + if node_len % 4 != 0 { + code.push_str("\n"); + } + + // .rdex + code.push_str(" // .rdex\n"); + for (i, (a, b)) in net.rdex.iter().enumerate() { + code.push_str(&format!(" 0x{:08X},", a.0)); + code.push_str(&format!(" 0x{:08X},", b.0)); + if (i + 1) % 4 == 0 { + code.push_str("\n"); + } + } + if rdex_len % 4 != 0 { + code.push_str("\n"); + } + } + + code.push_str("};\n\n"); + + code.push_str("u32 JUMP_DATA[] = {\n"); + + let mut index = 0; + for (i, fid) in defs.keys().enumerate() { + code.push_str(&format!(" 0x{:08X}, 0x{:08X}, // @{}\n", fid, index, crate::ast::val_to_name(**fid))); + index += 2 + 2 * defs[fid].node.len() as u32 + 2 * defs[fid].rdex.len() as u32; + } + + code.push_str("};"); + + return code; +} diff --git a/book/.hvm/src/run.rs b/book/.hvm/src/run.rs new file mode 100644 index 000000000..d390cdcca --- /dev/null +++ b/book/.hvm/src/run.rs @@ -0,0 +1,1389 @@ +// An efficient Interaction Combinator runtime +// =========================================== +// This file implements an efficient interaction combinator runtime. Nodes are represented by 2 aux +// ports (P1, P2), with the main port (P1) omitted. A separate vector, 'rdex', holds main ports, +// and, thus, tracks active pairs that can be reduced in parallel. Pointers are unboxed, meaning +// that ERAs, NUMs and REFs don't use any additional space. REFs lazily expand to closed nets when +// they interact with nodes, and are cleared when they interact with ERAs, allowing for constant +// space evaluation of recursive functions on Scott encoded datatypes. + +use std::sync::atomic::{AtomicU64, AtomicUsize, Ordering}; +use std::sync::{Arc, Barrier}; +use std::collections::HashMap; +use std::collections::HashSet; +use crate::u60; + +pub type Tag = u8; +pub type Lab = u32; +pub type Loc = u32; +pub type Val = u64; +pub type AVal = AtomicU64; + +// Core terms. +pub const VR1: Tag = 0x0; // Variable to aux port 1 +pub const VR2: Tag = 0x1; // Variable to aux port 2 +pub const RD1: Tag = 0x2; // Redirect to aux port 1 +pub const RD2: Tag = 0x3; // Redirect to aux port 2 +pub const REF: Tag = 0x4; // Lazy closed net +pub const ERA: Tag = 0x5; // Unboxed eraser +pub const NUM: Tag = 0x6; // Unboxed number +pub const OP2: Tag = 0x7; // Binary numeric operation +pub const OP1: Tag = 0x8; // Unary numeric operation +pub const MAT: Tag = 0x9; // Numeric pattern-matching +pub const LAM: Tag = 0xA; // Main port of lam node +pub const TUP: Tag = 0xB; // Main port of tup node +pub const DUP: Tag = 0xC; // Main port of dup node +pub const END: Tag = 0xE; // Last pointer tag + +// Numeric operations. +pub const ADD: Lab = 0x00; // addition +pub const SUB: Lab = 0x01; // subtraction +pub const MUL: Lab = 0x02; // multiplication +pub const DIV: Lab = 0x03; // division +pub const MOD: Lab = 0x04; // modulus +pub const EQ : Lab = 0x05; // equal-to +pub const NE : Lab = 0x06; // not-equal-to +pub const LT : Lab = 0x07; // less-than +pub const GT : Lab = 0x08; // greater-than +pub const LTE: Lab = 0x09; // less-than-or-equal +pub const GTE: Lab = 0x0A; // greater-than-or-equal +pub const AND: Lab = 0x0B; // logical-and +pub const OR : Lab = 0x0C; // logical-or +pub const XOR: Lab = 0x0D; // logical-xor +pub const LSH: Lab = 0x0E; // left-shift +pub const RSH: Lab = 0x0F; // right-shift +pub const NOT: Lab = 0x10; // logical-not + +pub const ERAS: Ptr = Ptr::new(ERA, 0, 0); +pub const ROOT: Ptr = Ptr::new(VR2, 0, 0); +pub const NULL: Ptr = Ptr(0x0000_0000_0000_0000); +pub const GONE: Ptr = Ptr(0xFFFF_FFFF_FFFF_FFEF); +pub const LOCK: Ptr = Ptr(0xFFFF_FFFF_FFFF_FFFF); // if last digit is F it will be seen as a CTR + +// An auxiliary port. +pub type Port = Val; +pub const P1: Port = 0; +pub const P2: Port = 1; + +// A tagged pointer. +#[derive(Copy, Clone, Debug, Eq, PartialEq, PartialOrd, Hash)] +pub struct Ptr(pub Val); + +// An atomic tagged pointer. +pub struct APtr(pub AVal); + +// FIXME: the 'this' pointer of headers is wasteful, since it is only used once in the lazy +// reducer, and, there, only the tag/lab is needed, because the loc is already known. As such, we +// could actually store only the tag/lab, saving up 32 bits per node. + +// A principal port, used on lazy mode. +pub struct Head { + this: Ptr, // points to this node's port 0 + targ: Ptr, // points to the target port 0 +} + +// An atomic principal port, used on lazy mode. +pub struct AHead { + this: APtr, // points to this node's port 0 + targ: APtr, // points to the target port 0 +} + +// An interaction combinator node. +pub type Node = ([ Head; LAZY as usize], Ptr, Ptr); +pub type ANode = ([AHead; LAZY as usize], APtr, APtr); + +// A target pointer, with implied ownership. +#[derive(Copy, Clone, Debug, Eq, PartialEq, PartialOrd, Hash)] +pub enum Trg { + Dir(Ptr), // we don't own the pointer, so we point to its location + Ptr(Ptr), // we own the pointer, so we store it directly +} + +// The global node buffer. +pub type Nodes = [ANode]; + +// A handy wrapper around Nodes. +pub struct Heap<'a, const LAZY: bool> +where [(); LAZY as usize]: { + pub nodes: &'a Nodes, +} + +// Rewrite counter. +#[derive(Copy, Clone)] +pub struct Rewrites { + pub anni: usize, // anni rewrites + pub comm: usize, // comm rewrites + pub eras: usize, // eras rewrites + pub dref: usize, // dref rewrites + pub oper: usize, // oper rewrites +} + +// Rewrite counter, atomic. +pub struct AtomicRewrites { + pub anni: AtomicUsize, // anni rewrites + pub comm: AtomicUsize, // comm rewrites + pub eras: AtomicUsize, // eras rewrites + pub dref: AtomicUsize, // dref rewrites + pub oper: AtomicUsize, // oper rewrites +} + +// An allocation area delimiter +pub struct Area { + pub init: usize, // first allocation index + pub size: usize, // total nodes in area +} + +// A interaction combinator net. +pub struct NetFields<'a, const LAZY: bool> +where [(); LAZY as usize]: { + pub tid : usize, // thread id + pub tids: usize, // thread count + pub labs: Lab, // dup labels + pub heap: Heap<'a, LAZY>, // nodes + pub rdex: Vec<(Ptr,Ptr)>, // redexes + pub locs: Vec, + pub area: Area, // allocation area + pub next: usize, // next allocation index within area + pub rwts: Rewrites, // rewrite count +} + +// A compact closed net, used for dereferences. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct Def { + pub labs: HashSet>, + pub rdex: Vec<(Ptr, Ptr)>, + pub node: Vec<((), Ptr, Ptr)>, +} + +// A map of id to definitions (closed nets). +pub struct Book { + pub defs: HashMap>, +} + +impl Ptr { + #[inline(always)] + pub const fn new(tag: Tag, lab: Lab, loc: Loc) -> Self { + Ptr(((loc as Val) << 32) | ((lab as Val) << 4) | (tag as Val)) + } + + #[inline(always)] + pub const fn big(tag: Tag, val: Val) -> Self { + Ptr((val << 4) | (tag as Val)) + } + + #[inline(always)] + pub const fn tag(&self) -> Tag { + (self.0 & 0xF) as Tag + } + + #[inline(always)] + pub const fn lab(&self) -> Lab { + (self.0 as Lab) >> 4 + } + + #[inline(always)] + pub const fn loc(&self) -> Loc { + (self.0 >> 32) as Loc + } + + #[inline(always)] + pub const fn val(&self) -> Val { + self.0 >> 4 + } + + #[inline(always)] + pub fn is_nil(&self) -> bool { + return self.0 == 0; + } + + #[inline(always)] + pub fn is_var(&self) -> bool { + return matches!(self.tag(), VR1..=VR2) && !self.is_nil(); + } + + #[inline(always)] + pub fn is_red(&self) -> bool { + return matches!(self.tag(), RD1..=RD2) && !self.is_nil(); + } + + #[inline(always)] + pub fn is_era(&self) -> bool { + return matches!(self.tag(), ERA); + } + + #[inline(always)] + pub fn is_ctr(&self) -> bool { + return matches!(self.tag(), LAM..=END); + } + + #[inline(always)] + pub fn is_dup(&self) -> bool { + return matches!(self.tag(), DUP); + } + + #[inline(always)] + pub fn is_ref(&self) -> bool { + return matches!(self.tag(), REF); + } + + #[inline(always)] + pub fn is_pri(&self) -> bool { + return matches!(self.tag(), REF..=END); + } + + #[inline(always)] + pub fn is_num(&self) -> bool { + return matches!(self.tag(), NUM); + } + + #[inline(always)] + pub fn is_op1(&self) -> bool { + return matches!(self.tag(), OP1); + } + + #[inline(always)] + pub fn is_op2(&self) -> bool { + return matches!(self.tag(), OP2); + } + + #[inline(always)] + pub fn is_skp(&self) -> bool { + return matches!(self.tag(), ERA | NUM | REF); + } + + #[inline(always)] + pub fn is_mat(&self) -> bool { + return matches!(self.tag(), MAT); + } + + #[inline(always)] + pub fn is_nod(&self) -> bool { + return matches!(self.tag(), OP2..=END); + } + + #[inline(always)] + pub fn has_loc(&self) -> bool { + return matches!(self.tag(), VR1..=VR2 | OP2..=END); + } + + #[inline(always)] + pub fn redirect(&self) -> Ptr { + return Ptr::new(self.tag() + RD2 - VR2, 0, self.loc()); + } + + #[inline(always)] + pub fn unredirect(&self) -> Ptr { + return Ptr::new(self.tag() + RD2 - VR2, 0, self.loc()); + } + + #[inline(always)] + pub fn can_skip(a: Ptr, b: Ptr) -> bool { + return matches!(a.tag(), ERA | REF) && matches!(b.tag(), ERA | REF); + } + + #[inline(always)] + pub fn view(&self) -> String { + if *self == NULL { + return format!("(NUL)"); + } else { + return match self.tag() { + VR1 => format!("(VR1 {:07x} {:08x})", self.lab(), self.loc()), + VR2 => format!("(VR2 {:07x} {:08x})", self.lab(), self.loc()), + RD1 => format!("(RD1 {:07x} {:08x})", self.lab(), self.loc()), + RD2 => format!("(RD2 {:07x} {:08x})", self.lab(), self.loc()), + REF => format!("(REF \"{}\")", crate::ast::val_to_name(self.val())), + ERA => format!("(ERA)"), + NUM => format!("(NUM {:x})", self.val()), + OP2 => format!("(OP2 {:07x} {:08x})", self.lab(), self.loc()), + OP1 => format!("(OP1 {:07x} {:08x})", self.lab(), self.loc()), + MAT => format!("(MAT {:07x} {:08x})", self.lab(), self.loc()), + LAM => format!("(LAM {:07x} {:08x})", self.lab(), self.loc()), + TUP => format!("(TUP {:07x} {:08x})", self.lab(), self.loc()), + DUP => format!("(DUP {:07x} {:08x})", self.lab(), self.loc()), + END => format!("(END)"), + _ => format!("???"), + }; + }; + } +} + +impl APtr { + pub const fn new(ptr: Ptr) -> Self { + APtr(AtomicU64::new(ptr.0)) + } + + pub fn load(&self) -> Ptr { + Ptr(self.0.load(Ordering::Relaxed)) + } + + pub fn store(&self, ptr: Ptr) { + self.0.store(ptr.0, Ordering::Relaxed); + } +} + + +impl Book { + #[inline(always)] + pub fn new() -> Self { + Book { + defs: HashMap::with_hasher(std::hash::BuildHasherDefault::default()), + } + } + + #[inline(always)] + pub fn def(&mut self, name: Val, def: Def) { + self.defs.insert(name, def); + } + + #[inline(always)] + pub fn get(&self, name: Val) -> Option<&Def> { + self.defs.get(&name) + } +} + +impl Def { + pub fn new() -> Self { + Def { + labs: HashSet::with_hasher(std::hash::BuildHasherDefault::default()), + rdex: vec![], + node: vec![], + } + } +} + +impl<'a, const LAZY: bool> Heap<'a, LAZY> +where [(); LAZY as usize]: { + pub fn new(nodes: &'a Nodes) -> Self { + Heap { nodes } + } + + pub fn init(size: usize) -> Box<[ANode]> { + let mut data = vec![]; + const head : AHead = AHead { + this: APtr::new(NULL), + targ: APtr::new(NULL), + }; + for _ in 0..size { + let p0 = [head; LAZY as usize]; + let p1 = APtr::new(NULL); + let p2 = APtr::new(NULL); + data.push((p0, p1, p2)); + } + return data.into_boxed_slice(); + } + + #[inline(always)] + pub fn get(&self, index: Loc, port: Port) -> Ptr { + unsafe { + let node = self.nodes.get_unchecked(index as usize); + if port == P1 { + return node.1.load(); + } else { + return node.2.load(); + } + } + } + + #[inline(always)] + pub fn set(&self, index: Loc, port: Port, value: Ptr) { + unsafe { + let node = self.nodes.get_unchecked(index as usize); + if port == P1 { + node.1.store(value); + } else { + node.2.store(value); + } + } + } + + #[inline(always)] + pub fn get_pri(&self, index: Loc) -> Head { + unsafe { + //println!("main of: {:016x} = {:016x}", index, self.nodes.get_unchecked(index as usize).0[0].1.load().0); + let this = self.nodes.get_unchecked(index as usize).0[0].this.load(); + let targ = self.nodes.get_unchecked(index as usize).0[0].targ.load(); + return Head { this, targ }; + } + } + + #[inline(always)] + pub fn set_pri(&self, index: Loc, this: Ptr, targ: Ptr) { + //println!("set main {:x} = {:016x} ~ {:016x}", index, this.0, targ.0); + unsafe { + self.nodes.get_unchecked(index as usize).0[0].this.store(this); + self.nodes.get_unchecked(index as usize).0[0].targ.store(targ); + } + } + + #[inline(always)] + pub fn cas(&self, index: Loc, port: Port, expected: Ptr, value: Ptr) -> Result { + unsafe { + let node = self.nodes.get_unchecked(index as usize); + let data = if port == P1 { &node.1.0 } else { &node.2.0 }; + let done = data.compare_exchange_weak(expected.0, value.0, Ordering::Relaxed, Ordering::Relaxed); + return done.map(Ptr).map_err(Ptr); + } + } + + #[inline(always)] + pub fn swap(&self, index: Loc, port: Port, value: Ptr) -> Ptr { + unsafe { + let node = self.nodes.get_unchecked(index as usize); + let data = if port == P1 { &node.1.0 } else { &node.2.0 }; + return Ptr(data.swap(value.0, Ordering::Relaxed)); + } + } + + #[inline(always)] + pub fn get_root(&self) -> Ptr { + return self.get(ROOT.loc(), P2); + } + + #[inline(always)] + pub fn set_root(&self, value: Ptr) { + self.set(ROOT.loc(), P2, value); + } +} + +impl Rewrites { + pub fn new() -> Self { + Rewrites { + anni: 0, + comm: 0, + eras: 0, + dref: 0, + oper: 0, + } + } + + pub fn add_to(&self, target: &AtomicRewrites) { + target.anni.fetch_add(self.anni, Ordering::Relaxed); + target.comm.fetch_add(self.comm, Ordering::Relaxed); + target.eras.fetch_add(self.eras, Ordering::Relaxed); + target.dref.fetch_add(self.dref, Ordering::Relaxed); + target.oper.fetch_add(self.oper, Ordering::Relaxed); + } + + pub fn total(&self) -> usize { + self.anni + self.comm + self.eras + self.dref + self.oper + } + +} + +impl AtomicRewrites { + pub fn new() -> Self { + AtomicRewrites { + anni: AtomicUsize::new(0), + comm: AtomicUsize::new(0), + eras: AtomicUsize::new(0), + dref: AtomicUsize::new(0), + oper: AtomicUsize::new(0), + } + } + + pub fn add_to(&self, target: &mut Rewrites) { + target.anni += self.anni.load(Ordering::Relaxed); + target.comm += self.comm.load(Ordering::Relaxed); + target.eras += self.eras.load(Ordering::Relaxed); + target.dref += self.dref.load(Ordering::Relaxed); + target.oper += self.oper.load(Ordering::Relaxed); + } +} + +impl<'a, const LAZY: bool> NetFields<'a, LAZY> where [(); LAZY as usize]: { + // Creates an empty net with given size. + pub fn new(nodes: &'a Nodes) -> Self { + NetFields { + tid : 0, + tids: 1, + labs: 0x1, + heap: Heap { nodes }, + rdex: vec![], + locs: vec![0; 1 << 16], + area: Area { init: 0, size: nodes.len() }, + next: 0, + rwts: Rewrites::new(), + } + } + + // Creates a net and boots from a REF. + pub fn boot(&self, root_id: Val) { + self.heap.set_root(Ptr::big(REF, root_id)); + } + + // Total rewrite count. + pub fn rewrites(&self) -> usize { + return self.rwts.anni + self.rwts.comm + self.rwts.eras + self.rwts.dref + self.rwts.oper; + } + + #[inline(always)] + pub fn alloc(&mut self) -> Loc { + // On the first pass, just alloc without checking. + // Note: we add 1 to avoid overwritting root. + let index = if self.next < self.area.size - 1 { + self.next += 1; + self.area.init as Loc + self.next as Loc + // On later passes, search for an available slot. + } else { + loop { + self.next += 1; + let index = (self.area.init + self.next % self.area.size) as Loc; + if self.heap.get(index, P1).is_nil() && self.heap.get(index, P2).is_nil() { + break index; + } + } + }; + self.heap.set(index, P1, LOCK); + self.heap.set(index, P2, LOCK); + //println!("ALLOC {}", index); + index + } + + // Gets a pointer's target. + #[inline(always)] + pub fn get_target(&self, ptr: Ptr) -> Ptr { + self.heap.get(ptr.loc(), ptr.0 & 1) + } + + // Sets a pointer's target. + #[inline(always)] + pub fn set_target(&mut self, ptr: Ptr, val: Ptr) { + self.heap.set(ptr.loc(), ptr.0 & 1, val) + } + + // Takes a pointer's target. + #[inline(always)] + pub fn swap_target(&self, ptr: Ptr, value: Ptr) -> Ptr { + self.heap.swap(ptr.loc(), ptr.0 & 1, value) + } + + // Takes a pointer's target. + #[inline(always)] + pub fn take_target(&self, ptr: Ptr) -> Ptr { + loop { + let got = self.heap.swap(ptr.loc(), ptr.0 & 1, LOCK); + if got != LOCK && got != NULL { + return got; + } + } + } + + // Sets a pointer's target, using CAS. + #[inline(always)] + pub fn cas_target(&self, ptr: Ptr, expected: Ptr, value: Ptr) -> Result { + self.heap.cas(ptr.loc(), ptr.0 & 1, expected, value) + } + + // Like get_target, but also for main ports + #[inline(always)] + pub fn get_target_full(&self, ptr: Ptr) -> Ptr { + if ptr.is_var() || ptr.is_red() { + return self.get_target(ptr); + } + if ptr.is_nod() { + return self.heap.get_pri(ptr.loc()).targ; + } + panic!("Can't get target of: {}", ptr.view()); + } + + #[inline(always)] + pub fn redux(&mut self, a: Ptr, b: Ptr) { + if Ptr::can_skip(a, b) { + self.rwts.eras += 1; + } else if !LAZY { + self.rdex.push((a, b)); + } else { + if a.is_nod() { self.heap.set_pri(a.loc(), a, b); } + if b.is_nod() { self.heap.set_pri(b.loc(), b, a); } + } + } + + #[inline(always)] + pub fn get(&self, a: Trg) -> Ptr { + match a { + Trg::Dir(dir) => self.get_target(dir), + Trg::Ptr(ptr) => ptr, + } + } + + #[inline(always)] + pub fn swap(&self, a: Trg, val: Ptr) -> Ptr { + match a { + Trg::Dir(dir) => self.swap_target(dir, val), + Trg::Ptr(ptr) => ptr, + } + } + + // Links two pointers, forming a new wire. Assumes ownership. + #[inline(always)] + pub fn link(&mut self, a_ptr: Ptr, b_ptr: Ptr) { + if a_ptr.is_pri() && b_ptr.is_pri() { + return self.redux(a_ptr, b_ptr); + } else { + self.linker(a_ptr, b_ptr); + self.linker(b_ptr, a_ptr); + } + } + + // Given two locations, links both stored pointers, atomically. + #[inline(always)] + pub fn atomic_link(&mut self, a_dir: Ptr, b_dir: Ptr) { + //println!("link {:016x} {:016x}", a_dir.0, b_dir.0); + let a_ptr = self.take_target(a_dir); + let b_ptr = self.take_target(b_dir); + if a_ptr.is_pri() && b_ptr.is_pri() { + self.set_target(a_dir, NULL); + self.set_target(b_dir, NULL); + return self.redux(a_ptr, b_ptr); + } else { + self.atomic_linker(a_ptr, a_dir, b_ptr); + self.atomic_linker(b_ptr, b_dir, a_ptr); + } + } + + // Given a location, link the pointer stored to another pointer, atomically. + #[inline(always)] + pub fn half_atomic_link(&mut self, a_dir: Ptr, b_ptr: Ptr) { + let a_ptr = self.take_target(a_dir); + if a_ptr.is_pri() && b_ptr.is_pri() { + self.set_target(a_dir, NULL); + return self.redux(a_ptr, b_ptr); + } else { + self.atomic_linker(a_ptr, a_dir, b_ptr); + self.linker(b_ptr, a_ptr); + } + } + + // When two threads interfere, uses the lock-free link algorithm described on the 'paper/'. + #[inline(always)] + pub fn linker(&mut self, a_ptr: Ptr, b_ptr: Ptr) { + if a_ptr.is_var() { + self.set_target(a_ptr, b_ptr); + } else { + if LAZY && a_ptr.is_nod() { + self.heap.set_pri(a_ptr.loc(), a_ptr, b_ptr); + } + } + } + + // When two threads interfere, uses the lock-free link algorithm described on the 'paper/'. + #[inline(always)] + pub fn atomic_linker(&mut self, a_ptr: Ptr, a_dir: Ptr, b_ptr: Ptr) { + // If 'a_ptr' is a var... + if a_ptr.is_var() { + let got = self.cas_target(a_ptr, a_dir, b_ptr); + // Attempts to link using a compare-and-swap. + if got.is_ok() { + self.set_target(a_dir, NULL); + // If the CAS failed, resolve by using redirections. + } else { + //println!("[{:04x}] cas fail {:016x}", self.tid, got.unwrap_err().0); + if b_ptr.is_var() { + self.set_target(a_dir, b_ptr.redirect()); + //self.atomic_linker_var(a_ptr, a_dir, b_ptr); + } else if b_ptr.is_pri() { + self.set_target(a_dir, b_ptr); + self.atomic_linker_pri(a_ptr, a_dir, b_ptr); + } else { + todo!(); + } + } + } else { + self.set_target(a_dir, NULL); + if LAZY && a_ptr.is_nod() { + self.heap.set_pri(a_ptr.loc(), a_ptr, b_ptr); + } + } + } + + // Atomic linker for when 'b_ptr' is a principal port. + pub fn atomic_linker_pri(&mut self, mut a_ptr: Ptr, a_dir: Ptr, b_ptr: Ptr) { + loop { + // Peek the target, which may not be owned by us. + let mut t_dir = a_ptr; + let mut t_ptr = self.get_target(t_dir); + // If target is a redirection, we own it. Clear and move forward. + if t_ptr.is_red() { + self.set_target(t_dir, NULL); + a_ptr = t_ptr; + continue; + } + // If target is a variable, we don't own it. Try replacing it. + if t_ptr.is_var() { + if self.cas_target(t_dir, t_ptr, b_ptr).is_ok() { + //println!("[{:04x}] var", self.tid); + // Clear source location. + self.set_target(a_dir, NULL); + // Collect the orphaned backward path. + t_dir = t_ptr; + t_ptr = self.get_target(t_ptr); + while t_ptr.is_red() { + self.swap_target(t_dir, NULL); + t_dir = t_ptr; + t_ptr = self.get_target(t_dir); + } + return; + } + // If the CAS failed, the var changed, so we try again. + continue; + } + // If it is a node, two threads will reach this branch. + if t_ptr.is_pri() || t_ptr == GONE { + // Sort references, to avoid deadlocks. + let x_dir = if a_dir < t_dir { a_dir } else { t_dir }; + let y_dir = if a_dir < t_dir { t_dir } else { a_dir }; + // Swap first reference by GONE placeholder. + let x_ptr = self.swap_target(x_dir, GONE); + // First to arrive creates a redex. + if x_ptr != GONE { + //println!("[{:04x}] fst {:016x}", self.tid, x_ptr.0); + let y_ptr = self.swap_target(y_dir, GONE); + self.redux(x_ptr, y_ptr); + return; + // Second to arrive clears up the memory. + } else { + //println!("[{:04x}] snd", self.tid); + self.swap_target(x_dir, NULL); + while self.cas_target(y_dir, GONE, NULL).is_err() {}; + return; + } + } + // If it is taken, we wait. + if t_ptr == LOCK { + continue; + } + if t_ptr == NULL { + continue; + } + // Shouldn't be reached. + //println!("[{:04x}] {:016x} | {:016x} {:016x} {:016x}", self.tid, t_ptr.0, a_dir.0, a_ptr.0, b_ptr.0); + unreachable!() + } + } + + // Atomic linker for when 'b_ptr' is an aux port. + pub fn atomic_linker_var(&mut self, a_ptr: Ptr, a_dir: Ptr, b_ptr: Ptr) { + loop { + let ste_dir = b_ptr; + let ste_ptr = self.get_target(ste_dir); + if ste_ptr.is_var() { + let trg_dir = ste_ptr; + let trg_ptr = self.get_target(trg_dir); + if trg_ptr.is_red() { + let neo_ptr = trg_ptr.unredirect(); + if self.cas_target(ste_dir, ste_ptr, neo_ptr).is_ok() { + self.swap_target(trg_dir, NULL); + continue; + } + } + } + break; + } + } + + // Links two targets, using atomics when necessary, based on implied ownership. + #[inline(always)] + pub fn safe_link(&mut self, a: Trg, b: Trg) { + match (a, b) { + (Trg::Dir(a_dir), Trg::Dir(b_dir)) => self.atomic_link(a_dir, b_dir), + (Trg::Dir(a_dir), Trg::Ptr(b_ptr)) => self.half_atomic_link(a_dir, b_ptr), + (Trg::Ptr(a_ptr), Trg::Dir(b_dir)) => self.half_atomic_link(b_dir, a_ptr), + (Trg::Ptr(a_ptr), Trg::Ptr(b_ptr)) => self.link(a_ptr, b_ptr), + } + } + + // Performs an interaction over a redex. + #[inline(always)] + pub fn interact(&mut self, book: &Book, a: Ptr, b: Ptr) { + //println!("inter {} ~ {}", a.view(), b.view()); + match (a.tag(), b.tag()) { + (REF , OP2..) => self.call(book, a, b), + (OP2.. , REF ) => self.call(book, b, a), + (LAM.. , LAM..) if a.lab() == b.lab() => self.anni(a, b), + (LAM.. , LAM..) => self.comm(a, b), + (LAM.. , ERA ) => self.era2(a), + (ERA , LAM..) => self.era2(b), + (REF , ERA ) => self.rwts.eras += 1, + (ERA , REF ) => self.rwts.eras += 1, + (REF , NUM ) => self.rwts.eras += 1, + (NUM , REF ) => self.rwts.eras += 1, + (ERA , ERA ) => self.rwts.eras += 1, + (LAM.. , NUM ) => self.copy(a, b), + (NUM , LAM..) => self.copy(b, a), + (NUM , ERA ) => self.rwts.eras += 1, + (ERA , NUM ) => self.rwts.eras += 1, + (NUM , NUM ) => self.rwts.eras += 1, + (OP2 , NUM ) => self.op2n(a, b), + (NUM , OP2 ) => self.op2n(b, a), + (OP1 , NUM ) => self.op1n(a, b), + (NUM , OP1 ) => self.op1n(b, a), + (OP2 , LAM..) => self.comm(a, b), + (LAM.. , OP2 ) => self.comm(b, a), + (OP1 , LAM..) => self.pass(a, b), + (LAM.. , OP1 ) => self.pass(b, a), + (OP2 , ERA ) => self.era2(a), + (ERA , OP2 ) => self.era2(b), + (OP1 , ERA ) => self.era1(a), + (ERA , OP1 ) => self.era1(b), + (MAT , NUM ) => self.mtch(a, b), + (NUM , MAT ) => self.mtch(b, a), + (MAT , LAM..) => self.comm(a, b), + (LAM.. , MAT ) => self.comm(b, a), + (MAT , ERA ) => self.era2(a), + (ERA , MAT ) => self.era2(b), + _ => { + println!("Invalid interaction: {} ~ {}", a.view(), b.view()); + unreachable!(); + }, + }; + } + + pub fn anni(&mut self, a: Ptr, b: Ptr) { + self.rwts.anni += 1; + let a1 = Ptr::new(VR1, 0, a.loc()); + let b1 = Ptr::new(VR1, 0, b.loc()); + self.atomic_link(a1, b1); + let a2 = Ptr::new(VR2, 0, a.loc()); + let b2 = Ptr::new(VR2, 0, b.loc()); + self.atomic_link(a2, b2); + } + + pub fn comm(&mut self, a: Ptr, b: Ptr) { + self.rwts.comm += 1; + let loc0 = self.alloc(); + let loc1 = self.alloc(); + let loc2 = self.alloc(); + let loc3 = self.alloc(); + self.heap.set(loc0, P1, Ptr::new(VR1, 0, loc2)); + self.heap.set(loc0, P2, Ptr::new(VR1, 0, loc3)); + self.heap.set(loc1, P1, Ptr::new(VR2, 0, loc2)); + self.heap.set(loc1, P2, Ptr::new(VR2, 0, loc3)); + self.heap.set(loc2, P1, Ptr::new(VR1, 0, loc0)); + self.heap.set(loc2, P2, Ptr::new(VR1, 0, loc1)); + self.heap.set(loc3, P1, Ptr::new(VR2, 0, loc0)); + self.heap.set(loc3, P2, Ptr::new(VR2, 0, loc1)); + let a1 = Ptr::new(VR1, 0, a.loc()); + self.half_atomic_link(a1, Ptr::new(b.tag(), b.lab(), loc0)); + let b1 = Ptr::new(VR1, 0, b.loc()); + self.half_atomic_link(b1, Ptr::new(a.tag(), a.lab(), loc2)); + let a2 = Ptr::new(VR2, 0, a.loc()); + self.half_atomic_link(a2, Ptr::new(b.tag(), b.lab(), loc1)); + let b2 = Ptr::new(VR2, 0, b.loc()); + self.half_atomic_link(b2, Ptr::new(a.tag(), a.lab(), loc3)); + } + + pub fn era2(&mut self, a: Ptr) { + self.rwts.eras += 1; + let a1 = Ptr::new(VR1, 0, a.loc()); + self.half_atomic_link(a1, ERAS); + let a2 = Ptr::new(VR2, 0, a.loc()); + self.half_atomic_link(a2, ERAS); + } + + pub fn era1(&mut self, a: Ptr) { + self.rwts.eras += 1; + let a2 = Ptr::new(VR2, 0, a.loc()); + self.half_atomic_link(a2, ERAS); + } + + pub fn pass(&mut self, a: Ptr, b: Ptr) { + self.rwts.comm += 1; + let loc0 = self.alloc(); + let loc1 = self.alloc(); + let loc2 = self.alloc(); + self.heap.set(loc0, P1, Ptr::new(VR2, 0, loc1)); + self.heap.set(loc0, P2, Ptr::new(VR2, 0, loc2)); + self.heap.set(loc1, P1, self.heap.get(a.loc(), P1)); + self.heap.set(loc1, P2, Ptr::new(VR1, 0, loc0)); + self.heap.set(loc2, P1, self.heap.get(a.loc(), P1)); + self.heap.set(loc2, P2, Ptr::new(VR2, 0, loc0)); + let a2 = Ptr::new(VR2, 0, a.loc()); + self.half_atomic_link(a2, Ptr::new(b.tag(), b.lab(), loc0)); + let b1 = Ptr::new(VR1, 0, b.loc()); + self.half_atomic_link(b1, Ptr::new(a.tag(), a.lab(), loc1)); + let b2 = Ptr::new(VR2, 0, b.loc()); + self.half_atomic_link(b2, Ptr::new(a.tag(), a.lab(), loc2)); + } + + pub fn copy(&mut self, a: Ptr, b: Ptr) { + self.rwts.comm += 1; + let a1 = Ptr::new(VR1, 0, a.loc()); + self.half_atomic_link(a1, b); + let a2 = Ptr::new(VR2, 0, a.loc()); + self.half_atomic_link(a2, b); + } + + pub fn mtch(&mut self, a: Ptr, b: Ptr) { + self.rwts.oper += 1; + let a1 = Ptr::new(VR1, 0, a.loc()); // branch + let a2 = Ptr::new(VR2, 0, a.loc()); // return + if b.val() == 0 { + let loc0 = self.alloc(); + //self.heap.set(loc0, P2, ERAS); + self.link(Ptr::new(VR2, 0, loc0), ERAS); + self.half_atomic_link(a1, Ptr::new(LAM, 0, loc0)); + self.half_atomic_link(a2, Ptr::new(VR1, 0, loc0)); + } else { + let loc0 = self.alloc(); + let loc1 = self.alloc(); + self.link(Ptr::new(VR1, 0, loc0), ERAS); + self.link(Ptr::new(VR2, 0, loc0), Ptr::new(LAM, 0, loc1)); + self.link(Ptr::new(VR1, 0, loc1), Ptr::big(NUM, b.val() - 1)); + //self.heap.set(loc0, P1, ERAS); + //self.heap.set(loc0, P2, Ptr::new(LAM, 0, loc1)); + //self.heap.set(loc1, P1, Ptr::big(NUM, b.val() - 1)); + self.half_atomic_link(a1, Ptr::new(LAM, 0, loc0)); + self.half_atomic_link(a2, Ptr::new(VR2, 0, loc1)); + } + } + + pub fn op2n(&mut self, a: Ptr, b: Ptr) { + self.rwts.oper += 1; + let loc0 = self.alloc(); + let a1 = Ptr::new(VR1, 0, a.loc()); + let a2 = Ptr::new(VR2, 0, a.loc()); + self.heap.set(loc0, P1, b); + self.half_atomic_link(a2, Ptr::new(VR2, 0, loc0)); + self.half_atomic_link(a1, Ptr::new(OP1, a.lab(), loc0)); + } + + pub fn op1n(&mut self, a: Ptr, b: Ptr) { + self.rwts.oper += 1; + let op = a.lab(); + let v0 = self.heap.get(a.loc(), P1).val(); + let v1 = b.val(); + let v2 = self.op(op, v0, v1); + let a2 = Ptr::new(VR2, 0, a.loc()); + self.half_atomic_link(a2, Ptr::big(NUM, v2)); + } + + #[inline(always)] + pub fn op(&self, op: Lab, a: Val, b: Val) -> Val { + match op { + ADD => { u60::add(a, b) } + SUB => { u60::sub(a, b) } + MUL => { u60::mul(a, b) } + DIV => { u60::div(a, b) } + MOD => { u60::rem(a, b) } + EQ => { u60::eq(a, b) } + NE => { u60::ne(a, b) } + LT => { u60::lt(a, b) } + GT => { u60::gt(a, b) } + LTE => { u60::lte(a, b) } + GTE => { u60::gte(a, b) } + AND => { u60::and(a, b) } + OR => { u60::or(a, b) } + XOR => { u60::xor(a, b) } + NOT => { u60::not(a) } + LSH => { u60::lsh(a, b) } + RSH => { u60::rsh(a, b) } + _ => { unreachable!() } + } + } + + // Expands a closed net. + #[inline(always)] + pub fn call(&mut self, book: &Book, ptr: Ptr, trg: Ptr) { + //println!("call {} {}", ptr.view(), trg.view()); + self.rwts.dref += 1; + let mut ptr = ptr; + // FIXME: change "while" to "if" once lang prevents refs from returning refs + if ptr.is_ref() { + // Intercepts with a native function, if available. + if !LAZY && self.call_native(book, ptr, trg) { + return; + } + // Load the closed net. + let fid = ptr.val(); + let got = book.get(fid).unwrap(); + if !LAZY && trg.is_dup() && !got.labs.contains(&trg.lab()) { + return self.copy(trg, ptr); + } else if got.node.len() > 0 { + let len = got.node.len() - 1; + // Allocate space. + for i in 0 .. len { + *unsafe { self.locs.get_unchecked_mut(1 + i) } = self.alloc(); + } + // Load nodes, adjusted. + for i in 0 .. len { + let p1 = self.adjust(unsafe { got.node.get_unchecked(1 + i) }.1); + let p2 = self.adjust(unsafe { got.node.get_unchecked(1 + i) }.2); + let lc = *unsafe { self.locs.get_unchecked(1 + i) }; + //println!(":: link loc={} [{} {}]", lc, p1.view(), p2.view()); + if p1 != ROOT { self.link(Ptr::new(VR1, 0, lc), p1); } + if p2 != ROOT { self.link(Ptr::new(VR2, 0, lc), p2); } + } + // Load redexes, adjusted. + for r in &got.rdex { + let p1 = self.adjust(r.0); + let p2 = self.adjust(r.1); + self.redux(p1, p2); + //self.rdex.push((p1, p2)); + } + // Load root, adjusted. + ptr = self.adjust(got.node[0].2); + } + } + self.link(ptr, trg); + } + + // Adjusts dereferenced pointer locations. + #[inline(always)] + fn adjust(&mut self, ptr: Ptr) -> Ptr { + if ptr.has_loc() { + let tag = ptr.tag(); + // FIXME + let lab = if LAZY && ptr.is_dup() && ptr.lab() == 0 { + self.labs += 2; + self.labs + } else { + ptr.lab() + }; + //let lab = ptr.lab(); + let loc = *unsafe { self.locs.get_unchecked(ptr.loc() as usize) }; + return Ptr::new(tag, lab, loc) + } else { + return ptr; + } + } + + pub fn view(&self) -> String { + let mut txt = String::new(); + for i in 0 .. self.heap.nodes.len() as Loc { + let p0 = self.heap.get_pri(i).targ; + let p1 = self.heap.get(i, P1); + let p2 = self.heap.get(i, P2); + if p1 != NULL || p2 != NULL { + txt.push_str(&format!("{:04x} | {:22} {:22} {:22}\n", i, p0.view(), p1.view(), p2.view())); + } + } + return txt; + } + + // Reduces all redexes. + #[inline(always)] + pub fn reduce(&mut self, book: &Book, limit: usize) -> usize { + let mut count = 0; + while let Some((a, b)) = self.rdex.pop() { + //if !a.is_nil() && !b.is_nil() { + self.interact(book, a, b); + count += 1; + if count >= limit { + break; + } + //} + } + return count; + } + + // Expands heads. + #[inline(always)] + pub fn expand(&mut self, book: &Book) { + fn go(net: &mut NetFields, book: &Book, dir: Ptr, len: usize, key: usize) where [(); LAZY as usize]: { + //println!("[{:04x}] expand dir: {:016x}", net.tid, dir.0); + let ptr = net.get_target(dir); + if ptr.is_ctr() { + if len >= net.tids || key % 2 == 0 { + go(net, book, Ptr::new(VR1, 0, ptr.loc()), len * 2, key / 2); + } + if len >= net.tids || key % 2 == 1 { + go(net, book, Ptr::new(VR2, 0, ptr.loc()), len * 2, key / 2); + } + } else if ptr.is_ref() { + let got = net.swap_target(dir, LOCK); + if got != LOCK { + //println!("[{:08x}] expand {:08x}", net.tid, dir.0); + net.call(book, ptr, dir); + } + } + } + return go(self, book, ROOT, 1, self.tid); + } + + // Forks into child threads, returning a NetFields for the (tid/tids)'th thread. + pub fn fork(&self, tid: usize, tids: usize) -> Self { + let mut net = NetFields::new(self.heap.nodes); + net.tid = tid; + net.tids = tids; + net.area = Area { + init: self.heap.nodes.len() * tid / tids, + size: self.heap.nodes.len() / tids, + }; + let from = self.rdex.len() * (tid + 0) / tids; + let upto = self.rdex.len() * (tid + 1) / tids; + for i in from .. upto { + net.rdex.push((self.rdex[i].0, self.rdex[i].1)); + } + if tid == 0 { + net.next = self.next; + } + return net; + } + + // Evaluates a term to normal form in parallel + pub fn parallel_normal(&mut self, book: &Book) { + + const SHARE_LIMIT : usize = 1 << 12; // max share redexes per split + const LOCAL_LIMIT : usize = 1 << 18; // max local rewrites per epoch + + // Local thread context + struct ThreadContext<'a, const LAZY: bool> where [(); LAZY as usize]: { + tid: usize, // thread id + tids: usize, // thread count + tlog2: usize, // log2 of thread count + tick: usize, // current tick + net: NetFields<'a, LAZY>, // thread's own net object + book: &'a Book, // definition book + delta: &'a AtomicRewrites, // global delta rewrites + share: &'a Vec<(APtr, APtr)>, // global share buffer + rlens: &'a Vec, // global redex lengths + total: &'a AtomicUsize, // total redex length + barry: Arc, // synchronization barrier + } + + // Initialize global objects + let cores = std::thread::available_parallelism().unwrap().get() as usize; + let tlog2 = cores.ilog2() as usize; + let tids = 1 << tlog2; + let delta = AtomicRewrites::new(); // delta rewrite counter + let rlens = (0..tids).map(|_| AtomicUsize::new(0)).collect::>(); + let share = (0..SHARE_LIMIT*tids).map(|_| (APtr(AtomicU64::new(0)), APtr(AtomicU64::new(0)))).collect::>(); + let total = AtomicUsize::new(0); // sum of redex bag length + let barry = Arc::new(Barrier::new(tids)); // global barrier + + // Perform parallel reductions + std::thread::scope(|s| { + for tid in 0 .. tids { + let mut ctx = ThreadContext { + tid: tid, + tids: tids, + tick: 0, + net: self.fork(tid, tids), + book: &book, + tlog2: tlog2, + delta: &delta, + share: &share, + rlens: &rlens, + total: &total, + barry: Arc::clone(&barry), + }; + s.spawn(move || { + main(&mut ctx) + }); + } + }); + + // Clear redexes and sum stats + self.rdex.clear(); + delta.add_to(&mut self.rwts); + + // Main reduction loop + #[inline(always)] + fn main(ctx: &mut ThreadContext) where [(); LAZY as usize]: { + loop { + reduce(ctx); + expand(ctx); + if count(ctx) == 0 { break; } + } + ctx.net.rwts.add_to(ctx.delta); + } + + // Reduce redexes locally, then share with target + #[inline(always)] + fn reduce(ctx: &mut ThreadContext) where [(); LAZY as usize]: { + loop { + let reduced = ctx.net.reduce(ctx.book, LOCAL_LIMIT); + if count(ctx) == 0 { + break; + } + let tlog2 = ctx.tlog2; + split(ctx, tlog2); + ctx.tick += 1; + } + } + + // Expand head refs + #[inline(always)] + fn expand(ctx: &mut ThreadContext) where [(); LAZY as usize]: { + ctx.net.expand(ctx.book); + } + + // Count total redexes (and populate 'rlens') + #[inline(always)] + fn count(ctx: &mut ThreadContext) -> usize where [(); LAZY as usize]: { + ctx.barry.wait(); + ctx.total.store(0, Ordering::Relaxed); + ctx.barry.wait(); + ctx.rlens[ctx.tid].store(ctx.net.rdex.len(), Ordering::Relaxed); + ctx.total.fetch_add(ctx.net.rdex.len(), Ordering::Relaxed); + ctx.barry.wait(); + return ctx.total.load(Ordering::Relaxed); + } + + + // Share redexes with target thread + #[inline(always)] + fn split(ctx: &mut ThreadContext, plog2: usize) where [(); LAZY as usize]: { + unsafe { + let side = (ctx.tid >> (plog2 - 1 - (ctx.tick % plog2))) & 1; + let shift = (1 << (plog2 - 1)) >> (ctx.tick % plog2); + let a_tid = ctx.tid; + let b_tid = if side == 1 { a_tid - shift } else { a_tid + shift }; + let a_len = ctx.net.rdex.len(); + let b_len = ctx.rlens[b_tid].load(Ordering::Relaxed); + let send = if a_len > b_len { (a_len - b_len) / 2 } else { 0 }; + let recv = if b_len > a_len { (b_len - a_len) / 2 } else { 0 }; + let send = std::cmp::min(send, SHARE_LIMIT); + let recv = std::cmp::min(recv, SHARE_LIMIT); + for i in 0 .. send { + let init = a_len - send * 2; + let rdx0 = *ctx.net.rdex.get_unchecked(init + i * 2 + 0); + let rdx1 = *ctx.net.rdex.get_unchecked(init + i * 2 + 1); + let targ = ctx.share.get_unchecked(b_tid * SHARE_LIMIT + i); + *ctx.net.rdex.get_unchecked_mut(init + i) = rdx0; + targ.0.store(rdx1.0); + targ.1.store(rdx1.1); + } + ctx.net.rdex.truncate(a_len - send); + ctx.barry.wait(); + for i in 0 .. recv { + let got = ctx.share.get_unchecked(a_tid * SHARE_LIMIT + i); + ctx.net.rdex.push((got.0.load(), got.1.load())); + } + } + } + } + + // Lazy mode weak head normalizer + #[inline(always)] + pub fn weak_normal(&mut self, book: &Book, mut prev: Ptr) -> Ptr { + let mut path : Vec = vec![]; + + loop { + // Load ptrs + let next = self.get_target_full(prev); + + // If next is ref, dereferences + if next.is_ref() { + self.call(book, next, prev); + continue; + } + + // If next is root, stop. + if next == ROOT { + break ; + } + + // If next is a main port... + if next.is_pri() { + // If prev is a main port, reduce the active pair. + if prev.is_pri() { + self.interact(book, prev, next); + prev = path.pop().unwrap(); + continue; + // Otherwise, we're done. + } else { + break; + } + } + + // If next is an aux port, pass through. + let main = self.heap.get_pri(next.loc()); + path.push(prev); + prev = main.this; + } + + return self.get_target_full(prev); + } + + // Reduce a net to normal form. + pub fn normal(&mut self, book: &Book) { + if LAZY { + let mut visit = vec![ROOT]; + while let Some(prev) = visit.pop() { + //println!("normal {} | {}", prev.view(), self.rewrites()); + let next = self.weak_normal(book, prev); + if next.is_nod() { + visit.push(Ptr::new(VR1, 0, next.loc())); + if !next.is_op1() { visit.push(Ptr::new(VR2, 0, next.loc())); } // TODO: improve + } + } + } else { + self.expand(book); + while self.rdex.len() > 0 { + self.reduce(book, usize::MAX); + self.expand(book); + } + } + } + +} + +// A net holding a static nodes buffer. +pub struct StaticNet where [(); LAZY as usize]: { + pub mem: *mut [ANode], + pub net: NetFields<'static, LAZY>, +} + +// A simple Net API. Holds its own nodes buffer, and knows its mode (lazy/eager). +pub enum Net { + Lazy(StaticNet), + Eager(StaticNet), +} + +impl Drop for Net { + fn drop(&mut self) { + match self { + Net::Lazy(this) => { let _ = unsafe { Box::from_raw(this.mem) }; } + Net::Eager(this) => { let _ = unsafe { Box::from_raw(this.mem) }; } + } + } +} + +impl Net { + // Creates a new net with the given size. + pub fn new(size: usize, lazy: bool) -> Self { + if lazy { + let mem = Box::leak(Heap::::init(size)) as *mut _; + let net = NetFields::::new(unsafe { &*mem }); + net.boot(crate::ast::name_to_val("main")); + return Net::Lazy(StaticNet { mem, net }); + } else { + let mem = Box::leak(Heap::::init(size)) as *mut _; + let net = NetFields::::new(unsafe { &*mem }); + net.boot(crate::ast::name_to_val("main")); + return Net::Eager(StaticNet { mem, net }); + } + } + + // Pretty prints. + pub fn show(&self) -> String { + match self { + Net::Lazy(this) => crate::ast::show_runtime_net(&this.net), + Net::Eager(this) => crate::ast::show_runtime_net(&this.net), + } + } + + // Reduces to normal form. + pub fn normal(&mut self, book: &Book) { + match self { + Net::Lazy(this) => this.net.normal(book), + Net::Eager(this) => this.net.normal(book), + } + } + + // Reduces to normal form in parallel. + pub fn parallel_normal(&mut self, book: &Book) { + match self { + Net::Lazy(this) => this.net.parallel_normal(book), + Net::Eager(this) => this.net.parallel_normal(book), + } + } + + pub fn get_rewrites(&self) -> Rewrites { + match self { + Net::Lazy(this) => this.net.rwts, + Net::Eager(this) => this.net.rwts, + } + } +} diff --git a/book/.hvm/src/u60.rs b/book/.hvm/src/u60.rs new file mode 100644 index 000000000..c84f30976 --- /dev/null +++ b/book/.hvm/src/u60.rs @@ -0,0 +1,113 @@ +// Implements u48: 48-bit unsigned integers using u64 and u128 + +type U60 = u64; + +#[inline(always)] +pub fn new(a: u64) -> U60 { + return a & 0xFFF_FFFF_FFFF_FFFF; +} + +#[inline(always)] +pub fn val(a: u64) -> U60 { + return a; +} + +#[inline(always)] +pub fn add(a: U60, b: U60) -> U60 { + return new(a + b); +} + +#[inline(always)] +pub fn sub(a: U60, b: U60) -> U60 { + return if a >= b { a - b } else { 0x1000000000000000 - (b - a) }; +} + +#[inline(always)] +pub fn mul(a: U60, b: U60) -> U60 { + return new((a as u128 * b as u128) as u64); +} + +#[inline(always)] +pub fn div(a: U60, b: U60) -> U60 { + return a / b; +} + +#[inline(always)] +pub fn rem(a: U60, b: U60) -> U60 { + return a % b; +} + +#[inline(always)] +pub fn and(a: U60, b: U60) -> U60 { + return a & b; +} + +#[inline(always)] +pub fn or(a: U60, b: U60) -> U60 { + return a | b; +} + +#[inline(always)] +pub fn xor(a: U60, b: U60) -> U60 { + return a ^ b; +} + +#[inline(always)] +pub fn lsh(a: U60, b: U60) -> U60 { + return new(a << b); +} + +#[inline(always)] +pub fn rsh(a: U60, b: U60) -> U60 { + return a >> b; +} + +#[inline(always)] +pub fn lt(a: U60, b: U60) -> U60 { + return if a < b { 1 } else { 0 }; +} + +#[inline(always)] +pub fn gt(a: U60, b: U60) -> U60 { + return if a > b { 1 } else { 0 }; +} + +#[inline(always)] +pub fn lte(a: U60, b: U60) -> U60 { + return if a <= b { 1 } else { 0 }; +} + +#[inline(always)] +pub fn gte(a: U60, b: U60) -> U60 { + return if a >= b { 1 } else { 0 }; +} + +#[inline(always)] +pub fn eq(a: U60, b: U60) -> U60 { + return if a == b { 1 } else { 0 }; +} + +#[inline(always)] +pub fn ne(a: U60, b: U60) -> U60 { + return if a != b { 1 } else { 0 }; +} + +#[inline(always)] +pub fn min(a: U60, b: U60) -> U60 { + return if a < b { a } else { b }; +} + +#[inline(always)] +pub fn max(a: U60, b: U60) -> U60 { + return if a > b { a } else { b }; +} + +#[inline(always)] +pub fn not(a: U60) -> U60 { + return !a & 0xFFF_FFFF_FFFF_FFFF; +} + +#[inline(always)] +pub fn show(a: U60) -> String { + return format!("{}", a); +} diff --git a/book/.hvm/target/.rustc_info.json b/book/.hvm/target/.rustc_info.json new file mode 100644 index 000000000..fa4d4a065 --- /dev/null +++ b/book/.hvm/target/.rustc_info.json @@ -0,0 +1 @@ +{"rustc_fingerprint":4802413464031946296,"outputs":{"15729799797837862367":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.dylib\nlib___.dylib\nlib___.a\nlib___.dylib\n/Users/v/.rustup/toolchains/nightly-aarch64-apple-darwin\noff\npacked\nunpacked\n___\ndebug_assertions\noverflow_checks\npanic=\"unwind\"\nproc_macro\nrelocation_model=\"pic\"\ntarget_abi=\"\"\ntarget_arch=\"aarch64\"\ntarget_endian=\"little\"\ntarget_env=\"\"\ntarget_family=\"unix\"\ntarget_feature=\"aes\"\ntarget_feature=\"crc\"\ntarget_feature=\"dit\"\ntarget_feature=\"dotprod\"\ntarget_feature=\"dpb\"\ntarget_feature=\"dpb2\"\ntarget_feature=\"fcma\"\ntarget_feature=\"fhm\"\ntarget_feature=\"flagm\"\ntarget_feature=\"fp16\"\ntarget_feature=\"frintts\"\ntarget_feature=\"jsconv\"\ntarget_feature=\"lor\"\ntarget_feature=\"lse\"\ntarget_feature=\"neon\"\ntarget_feature=\"paca\"\ntarget_feature=\"pacg\"\ntarget_feature=\"pan\"\ntarget_feature=\"pmuv3\"\ntarget_feature=\"ras\"\ntarget_feature=\"rcpc\"\ntarget_feature=\"rcpc2\"\ntarget_feature=\"rdm\"\ntarget_feature=\"sb\"\ntarget_feature=\"sha2\"\ntarget_feature=\"sha3\"\ntarget_feature=\"ssbs\"\ntarget_feature=\"v8.1a\"\ntarget_feature=\"v8.2a\"\ntarget_feature=\"v8.3a\"\ntarget_feature=\"v8.4a\"\ntarget_feature=\"vh\"\ntarget_has_atomic\ntarget_has_atomic=\"128\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"ptr\"\ntarget_has_atomic_equal_alignment=\"128\"\ntarget_has_atomic_equal_alignment=\"16\"\ntarget_has_atomic_equal_alignment=\"32\"\ntarget_has_atomic_equal_alignment=\"64\"\ntarget_has_atomic_equal_alignment=\"8\"\ntarget_has_atomic_equal_alignment=\"ptr\"\ntarget_has_atomic_load_store\ntarget_has_atomic_load_store=\"128\"\ntarget_has_atomic_load_store=\"16\"\ntarget_has_atomic_load_store=\"32\"\ntarget_has_atomic_load_store=\"64\"\ntarget_has_atomic_load_store=\"8\"\ntarget_has_atomic_load_store=\"ptr\"\ntarget_os=\"macos\"\ntarget_pointer_width=\"64\"\ntarget_thread_local\ntarget_vendor=\"apple\"\nunix\n","stderr":""},"4614504638168534921":{"success":true,"status":"","code":0,"stdout":"rustc 1.76.0-nightly (9a66e4471 2023-11-19)\nbinary: rustc\ncommit-hash: 9a66e4471f71283fd54d80ef8147630d34756332\ncommit-date: 2023-11-19\nhost: aarch64-apple-darwin\nrelease: 1.76.0-nightly\nLLVM version: 17.0.5\n","stderr":""}},"successes":{}} \ No newline at end of file diff --git a/book/.hvm/target/CACHEDIR.TAG b/book/.hvm/target/CACHEDIR.TAG new file mode 100644 index 000000000..20d7c319c --- /dev/null +++ b/book/.hvm/target/CACHEDIR.TAG @@ -0,0 +1,3 @@ +Signature: 8a477f597d28d172789f06886806bc55 +# This file is a cache directory tag created by cargo. +# For information about cache directory tags see https://bford.info/cachedir/ diff --git a/book/.hvm/target/release/.cargo-lock b/book/.hvm/target/release/.cargo-lock new file mode 100644 index 000000000..e69de29bb diff --git a/book/.hvm/target/release/.fingerprint/hvm-core-5d3b356175a8b321/invoked.timestamp b/book/.hvm/target/release/.fingerprint/hvm-core-5d3b356175a8b321/invoked.timestamp new file mode 100644 index 000000000..e00328da5 --- /dev/null +++ b/book/.hvm/target/release/.fingerprint/hvm-core-5d3b356175a8b321/invoked.timestamp @@ -0,0 +1 @@ +This file has an mtime of when this was started. \ No newline at end of file diff --git a/book/.hvm/target/release/.fingerprint/hvm-core-5d3b356175a8b321/output-lib-hvmc b/book/.hvm/target/release/.fingerprint/hvm-core-5d3b356175a8b321/output-lib-hvmc new file mode 100644 index 000000000..f7d4eee42 --- /dev/null +++ b/book/.hvm/target/release/.fingerprint/hvm-core-5d3b356175a8b321/output-lib-hvmc @@ -0,0 +1,5 @@ +{"message":"expected one of `:`, `;`, `<`, `=`, or `where`, found `.`","code":null,"level":"error","spans":[{"file_name":"src/fns.rs","byte_start":186,"byte_end":187,"line_start":7,"line_end":7,"column_start":17,"column_end":18,"is_primary":true,"text":[{"text":"pub const F__U60.fib : Val = 0xf9e180fe9b25;","highlight_start":17,"highlight_end":18}],"label":"expected one of `:`, `;`, `<`, `=`, or `where`","suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[],"rendered":"\u001b[0m\u001b[1m\u001b[38;5;9merror\u001b[0m\u001b[0m\u001b[1m: expected one of `:`, `;`, `<`, `=`, or `where`, found `.`\u001b[0m\n\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m--> \u001b[0m\u001b[0msrc/fns.rs:7:17\u001b[0m\n\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m|\u001b[0m\n\u001b[0m\u001b[1m\u001b[38;5;12m7\u001b[0m\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m|\u001b[0m\u001b[0m \u001b[0m\u001b[0mpub const F__U60.fib : Val = 0xf9e180fe9b25;\u001b[0m\n\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m| \u001b[0m\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;9m^\u001b[0m\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;9mexpected one of `:`, `;`, `<`, `=`, or `where`\u001b[0m\n\n"} +{"message":"no method named `call_native` found for mutable reference `&mut NetFields<'a, LAZY>` in the current scope","code":{"code":"E0599","explanation":"This error occurs when a method is used on a type which doesn't implement it:\n\nErroneous code example:\n\n```compile_fail,E0599\nstruct Mouth;\n\nlet x = Mouth;\nx.chocolate(); // error: no method named `chocolate` found for type `Mouth`\n // in the current scope\n```\n\nIn this case, you need to implement the `chocolate` method to fix the error:\n\n```\nstruct Mouth;\n\nimpl Mouth {\n fn chocolate(&self) { // We implement the `chocolate` method here.\n println!(\"Hmmm! I love chocolate!\");\n }\n}\n\nlet x = Mouth;\nx.chocolate(); // ok!\n```\n"},"level":"error","spans":[{"file_name":"src/run.rs","byte_start":30344,"byte_end":30355,"line_start":993,"line_end":993,"column_start":24,"column_end":35,"is_primary":true,"text":[{"text":" if !LAZY && self.call_native(book, ptr, trg) {","highlight_start":24,"highlight_end":35}],"label":"method not found in `&mut NetFields<'a, LAZY>`","suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[],"rendered":"\u001b[0m\u001b[1m\u001b[38;5;9merror[E0599]\u001b[0m\u001b[0m\u001b[1m: no method named `call_native` found for mutable reference `&mut NetFields<'a, LAZY>` in the current scope\u001b[0m\n\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m--> \u001b[0m\u001b[0msrc/run.rs:993:24\u001b[0m\n\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m|\u001b[0m\n\u001b[0m\u001b[1m\u001b[38;5;12m993\u001b[0m\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m|\u001b[0m\u001b[0m \u001b[0m\u001b[0m if !LAZY && self.call_native(book, ptr, trg) {\u001b[0m\n\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m| \u001b[0m\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;9m^^^^^^^^^^^\u001b[0m\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;9mmethod not found in `&mut NetFields<'a, LAZY>`\u001b[0m\n\n"} +{"message":"missing type for `const` item","code":null,"level":"error","spans":[{"file_name":"src/fns.rs","byte_start":186,"byte_end":186,"line_start":7,"line_end":7,"column_start":17,"column_end":17,"is_primary":true,"text":[{"text":"pub const F__U60.fib : Val = 0xf9e180fe9b25;","highlight_start":17,"highlight_end":17}],"label":null,"suggested_replacement":null,"suggestion_applicability":null,"expansion":null}],"children":[{"message":"provide a type for the item","code":null,"level":"help","spans":[{"file_name":"src/fns.rs","byte_start":186,"byte_end":186,"line_start":7,"line_end":7,"column_start":17,"column_end":17,"is_primary":true,"text":[{"text":"pub const F__U60.fib : Val = 0xf9e180fe9b25;","highlight_start":17,"highlight_end":17}],"label":null,"suggested_replacement":": ","suggestion_applicability":"HasPlaceholders","expansion":null}],"children":[],"rendered":null}],"rendered":"\u001b[0m\u001b[1m\u001b[38;5;9merror\u001b[0m\u001b[0m\u001b[1m: missing type for `const` item\u001b[0m\n\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m--> \u001b[0m\u001b[0msrc/fns.rs:7:17\u001b[0m\n\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m|\u001b[0m\n\u001b[0m\u001b[1m\u001b[38;5;12m7\u001b[0m\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m|\u001b[0m\u001b[0m \u001b[0m\u001b[0mpub const F__U60.fib : Val = 0xf9e180fe9b25;\u001b[0m\n\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;12m| \u001b[0m\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;9m^\u001b[0m\u001b[0m \u001b[0m\u001b[0m\u001b[1m\u001b[38;5;9mhelp: provide a type for the item: `: `\u001b[0m\n\n"} +{"message":"aborting due to 3 previous errors","code":null,"level":"error","spans":[],"children":[],"rendered":"\u001b[0m\u001b[1m\u001b[38;5;9merror\u001b[0m\u001b[0m\u001b[1m: aborting due to 3 previous errors\u001b[0m\n\n"} +{"message":"For more information about this error, try `rustc --explain E0599`.","code":null,"level":"failure-note","spans":[],"children":[],"rendered":"\u001b[0m\u001b[1mFor more information about this error, try `rustc --explain E0599`.\u001b[0m\n"} diff --git a/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/dep-lib-nohash-hasher b/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/dep-lib-nohash-hasher new file mode 100644 index 0000000000000000000000000000000000000000..1b1cb4d44c57c2d7a5122870fa6ac3e62ff7e94e GIT binary patch literal 8 KcmZQzfB*mh2mk>9 literal 0 HcmV?d00001 diff --git a/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/invoked.timestamp b/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/invoked.timestamp new file mode 100644 index 000000000..e00328da5 --- /dev/null +++ b/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/invoked.timestamp @@ -0,0 +1 @@ +This file has an mtime of when this was started. \ No newline at end of file diff --git a/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/lib-nohash-hasher b/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/lib-nohash-hasher new file mode 100644 index 000000000..a2544425c --- /dev/null +++ b/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/lib-nohash-hasher @@ -0,0 +1 @@ +7cda99c4629b01d5 \ No newline at end of file diff --git a/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/lib-nohash-hasher.json b/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/lib-nohash-hasher.json new file mode 100644 index 000000000..26841172b --- /dev/null +++ b/book/.hvm/target/release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/lib-nohash-hasher.json @@ -0,0 +1 @@ +{"rustc":15865603277963313838,"features":"[\"default\", \"std\"]","target":2117364898282992337,"profile":15536308671813986309,"path":6587989396380489126,"deps":[],"local":[{"CheckDepInfo":{"dep_info":"release/.fingerprint/nohash-hasher-dc8a50f19f38f70e/dep-lib-nohash-hasher"}}],"rustflags":[],"metadata":8492774112348001440,"config":2202906307356721367,"compile_kind":0} \ No newline at end of file diff --git a/book/.hvm/target/release/deps/hvmc-5d3b356175a8b321.d b/book/.hvm/target/release/deps/hvmc-5d3b356175a8b321.d new file mode 100644 index 000000000..1eebd12de --- /dev/null +++ b/book/.hvm/target/release/deps/hvmc-5d3b356175a8b321.d @@ -0,0 +1,12 @@ +/Users/v/vic/dev/kind2/book/.hvm/target/release/deps/libhvmc-5d3b356175a8b321.rmeta: src/lib.rs src/ast.rs src/fns.rs src/jit.rs src/run.rs src/u60.rs + +/Users/v/vic/dev/kind2/book/.hvm/target/release/deps/libhvmc-5d3b356175a8b321.rlib: src/lib.rs src/ast.rs src/fns.rs src/jit.rs src/run.rs src/u60.rs + +/Users/v/vic/dev/kind2/book/.hvm/target/release/deps/hvmc-5d3b356175a8b321.d: src/lib.rs src/ast.rs src/fns.rs src/jit.rs src/run.rs src/u60.rs + +src/lib.rs: +src/ast.rs: +src/fns.rs: +src/jit.rs: +src/run.rs: +src/u60.rs: diff --git a/book/.hvm/target/release/deps/libnohash_hasher-dc8a50f19f38f70e.rlib b/book/.hvm/target/release/deps/libnohash_hasher-dc8a50f19f38f70e.rlib new file mode 100644 index 0000000000000000000000000000000000000000..b376a638789f83a835740d213e94c178be3f4f0c GIT binary patch literal 23504 zcmc(H31Cyj*6`e$tsCh=3oUJvn-)rvW^bA%l(hvc;8GC~rQe zny&83f}-vr$yT$~CNu|2b5an~fw3UioQxnZWav=SLyz9qyH8&t28r*9kAIb~!)~Vx zZPv7O2TkRLloaQiDoZ`pZs4=`#)Vs9gmB0cBb2cN0bj7eGZwy-fP_M#4b6#zcn(dq z9+eIh@n?P63|0V)Uy&anenotALx=Vr+-o4S*oTA%E6?~f=MX+1O##$*$U`C)pD3$x zL{&9Bf(UsqG!=mY!D`BIm@LM!;$cPAC1V7w%k6M@?Dh<+V6)iLj8?1B>eAKmO`(my zclhM1*YCNq{OandQD2`tM)*i$MnR#|S&-o=a5_EK3~NCh;pa)ekIRU8D((7_Yp*<@CA=JwSLuGRmf(-Y{w3TSf0S-s<4kaUKct9kv2bL7K&G zwR-F>m#q#eo+>)Ds=9FKsPf9Et18?Do}mThm7cn-mlGYtr@ z%4aTnt*Yy)_xV-BH}pOd_t62Wk~2S}(2?)9+TAvn!)XD+x7y4YSkPz~k^b3T$>~ewx<}y2}f^!-f`n>yEaOEZDel=YS&F{ZEwajXi}gh8e!4r&3KD{g z+*L*SmF1(#>T0jglfECm@BF(9u6+AXVc>DmgnXMf-RsOq0}0lAFYu3Rt@_<1CFKQm zHJ1;hnVy^U^8SO}LeH<9EJY6K&UBl%(3asTv^!lHUZ{T(f=yTGsrD39*Zpvj9N2hF zX?bVjzORI<+aJXu4yQBUmG5=iErpgsnF(&uo6$*$Co-aJ~(8;%|j8^ z`R2I$H)1hcep1|hZA<*?f94u{=q z@md{T=(9v#p8phDVca*TY{kjs%g655$1U16_#$QQuv-hPZm-4e@aB76*fjD|Pia9> zWgVZCzGCGCZC=oTU1N%}hxR~nyVqrP+8u?i0(*wTm5%-NLeQ%G$D}XLOWD+GwmIEa zld+0$(5o_BHg{o$+iSNLT5K*Bs>7W*nOqv2i;cshTT{CV}>W>;~*$-)sB;l ztlCpmU4>fwk}X4NXR>{KPBMB?iyyP4s9hNOo#6>2p}^^En0#@Df^tL#a}6e;j0Cij zNZ>1luMEC&$R_fBW!3k&E9wXr4B`g(o{zxOm-&#V8h|hvKM5_9k;tqO#U+KeRT<%w zESuY*AY4QUd__!zoIlY9AUS^$9{3j{X2i((gJ>Veaj_yMR?c@t1kc5bh6Fbizqz!nZ{;h+gPr~ob)z9H}pg>M*q+rU@JrHU+4rHz z7WhR2I8H_)IQ)=EXi(_Sq%AZffFv5)5udb+k&QE!Y+QM0!J8vFE`~q{;kQR~++ihu zIg&mu#o&Vo9JC;fc^XS-ETu8Q7&<1#G?%BjJk8|^KjA)P(UFr#bsR743`9wsgx7Ms zBn66TfU%zANirvqbmAl=9u<$lC>A3XMyVJPA*2^-rA6yxsHThu?PSPbCI#)tB~>CJ zQYqOLPNdMG$Ssu;%#`DJJ`_%P{}kfwlX{y#-AGilNAqY zanRQYba3Qn*lT0u5M z5}8!wk?!NMK#f*|9g{^Kpg&G063SqK8n!z~zmzhNVRD%o^1&$N+n#2wR*eM|tdCH` z8(-yl{_|HMliv)<-B5z#>mUX50^zsNjCuf{hl=9(t-cIk1>x&Mzi(c(cj*$atu2gm ze)$5ZR*X1)#R8tMMd`k-xbEX!pRM`&yIB_j1)oFM7*J=>{SaKQf_ec^#!nf*!I$ta zL0LIJbpXFd#_?-&_!kH8e-~5J2Jjm}4B(~@;CHp5sh0-u(}QVh#sDJ8AK|S-0F1`) z&7N0oO?+$VjdO%+|4Rp29*x~HTNW`E52Er*17N-L_z3@vk)LNUPk1TNlkVdbtjuQz-H{RA2rggqZg zxVK^mb}w#`_#_h|p&9_b2v6u)pbzvYnuI>h^YLVHTL3{}Xqj~~@>(=N(C=XD`+5{w zftgsrlQjtx2;*TKaoluZLYw+!4P*i}bOUeS!QkaD7<1iFxSp*f_7qUbxhl3Q8?I8&xjQifn zaT6kO{v)f+F#kZS^eY?bE-5Y)MpSu(a<34$&H`tcL*gey!gz!+xinU62O||X(JY=$ zq}&A`W{5}>jAL=j0=h53^Ovam)HtL;5UY2p z1tvR~BqO<+$Tm<@FrCPuonV53%n26gZmh;pEx^5Mfk=jX4l>6AxxPj<(V6G4xf|si z$sLHe7r8-IG;RUX(;%N|f1PUo4s-+90HNvx^oH~mRGZd0QuDBuv=Y zcAgrxjvDr>-!P;W4SPd{ieiJHVT%#+8y0TCa)S0ZOD(C0Hqn)@x!%fD&+s0OMxZ@2Cl+@YTedcC3j;s>Bj| zb4~oC6QKPyaS|a>iO)I(Dsk2h>oEfDfpR7#;9L(oz<`|zb`{Wx+)9Bu#{fGc1R&5woThQsK-^qduJH-G z7<{6ksF_IqU*#Gcri_Rb;4lt*B5D^z*t=jCNXQZ?8V(yuNW(`;qUaf0bV&5}c-D;9ip#1! z!#tHjVR@;$xXb`Msp7I>LSEobDo>~`7b-lJ-tx*)p{!ge0v<@@t`=a!V5&pr=cJFp zgEkh~Dx>?FP$609GumAWyZ9EPgK2sRk-Jk`8Rbq&$sINz{SOK_PQ&vm3PR7_>*jWV0L-uG z93rGP2qN$>@LTBd`#RFo65}z0sD17-GBF6JADVMTK@EH*2u2ysRR@9z>^^{+I}}XN z#e~xbU?7S4`27)1KF~pd5^(buX=G`|^D_d@rzaA6emS1;d|C0sPYYU@$^Se))aqo#D6N>pKgd+p_5M z6BpOa9Q^M%au!(0I~M#jhxHZ$AAbP-_k_|T;=O`z0D_Y+505Lpu~+qPkGexa4?z8h z-DPPob{Fn)D%RM_;O3#WNz8baws~D}^XR!EW{92PmtgeH+;!xD%3^oF72G^>7KG3q zs%{=R;xGZ?7Q=~nJ3{D*EFja`oOy(1iUwa2xx}?HJ_5$Z z)eySNZ=K3NE@p)ym2X_E3>C-4`cU7v_%J;MIxy7EXJQZj5_@m+xY&sFw3Bb8-P%7c zwuk!1#V4V3T>K-HjtdUm!{E>XHXJ_1(qgX%j{%^M0w)>Q6vDxm@NdvAKQWX$VBxq6 zA-?Xu@Y>a-bIu%kt(r%lz@O~ua6(_^z>hzG)Ws3>+#(6E**SyD!kJQyp3`CoBsdVpAOs3+S82!kYW$MVdjf=`sNGWI3({)Wr@9fxE0w1aZ8G>q1p| zsYmd*tBPU88d2pQ27qsc5rtj}>+2V~p$!!(cJEDXX!lNOZDDBPq8EGmwl=UR!z@RO zz%^2rE(PT!C2$2(TwYeyrHgMR6={EJ)7-mXR?<=7Y#tR|1RrsiE?q}B4MIVYyV4-E z5DR(TVWFY5_nI;jh35zu{H1Y899rOpTgYN?bV2?27B?*{Q!Us93_;(}I-nfjubnr; zsg_XzW6&UUc6auXz8y~Y3<24&P<75{+3RVx*tmN{PRYJ;IMg#-qkRb4Nt=S~3?N{b zr#fIn9tfv<$JXe9zn|VeHh-h^zOlJ5g0|!82;8{CWDes(Nc7XbtWS@B>c>K5IUs*0d*I^}vrm0O4vC9AV%&O9dSbcNf=s23$Ts-Wn`$d*IQF=HfFT?n2{CK0|_Y zGQ~orLR!rGZ@9L(>up>2Ys0k15fIJ2i%S_t@B~3kTQAxa18vnF+lq&NMK-A5xJzBi z0DP!UMw4JSFIIXS>JA@xLhx1k8n{h3tn5H`WZ}mjfbe@EnikkD_$vK}tdW3#oSg!# z^keV{sPtVxN3;JfW*^0D&fmlL2>wdnD$q(lC(yOdFOw!jcP~d`p)dqUfPo#Try5+5 z8Vw@-7J*BS%0Sl~Ch2fpr9q1l$-Lh9@dqG0l|+MVP#X-g6{=?r?NZx7(B;Ye3LgBSY_q@eH6G0DNL8PKBm3nJrq zur<-&m>0q24SCCx1?1>A8a!iE3-pj-k{Z1leCfb+Mqm8+1JKPf&@GTv7=*_jVN_9Z z0i4w;Jwlb+>%qeqy1VJ|sI`T6e=>NGph8gM^Bw6d-&Yt^R9q#Lx+|ZCg|oWSU0f{y z49CCn3S7?UYEI8s$lXJ4jD_kVPid8>WF%le*lvfs_ka8hk zR2U98MIQ0wnI{y(aZo7pcnYh4g7W*iBQDt_35=^QuJVqd)LvL=%SYiM6OKGpsBl?z z7fL?A6FN^s>*_jD>jntj1-<@(GI|BzmxV_@@xFN+thpns4g;R%MmX#SIO2}=7>b<+ zxMw!N-Le7hlMVC^`C0K4xvkUvs8X^3uV@vOgQ`$h#bqPQpY{~uexm?iRw^$m@R;;^ zs?+QgT+u|GK1-oG-2*l5ff}f)7Dl3%)aM9xn5~8uEGqp0L`G`*$Pt@XT z3nIx(Et2?_?b%woY{v=7k5d~w+FW;Kb+Nmo&v1j#XSnW3TKo+y-K)0~pv6ZNR13I^ zz#*V*J^*ac;$@2{;VUYEbQC)k-Jumh6^dIk+GiO9VI1ZE4{c{COfm%w-ZJXQ=$g|7 z#KGpSxu~bIyEX+Y%RnihBMB+!7s%21_%vy|BOeXrgAtbXRGNIRH>BCLSlVRKQK^5^ zQJLbef&@Z zpgH)iHE~!EU%~_0k?oZ~0YaL+LCoHT*-(qVz4E6f|FXNvgnQ-YwGrONprr7Gz>90+ zS6Cc^fGaEJe`5-U#nNapTdcM;d%7dTNtO-5k3Rs>M7S1)$7FNM6&$`}!$1eg>AmVTf5l5RvIQ$|``a~S<2qI?KX>-49Z@sy5{30L) zA{twWcoXmHL@VIL=sjAwUXt^7LX37(z)p zdo(l)fLB+10=@+SWI~oWeQd#@K_`;kDp-MF_1Mz~b@y^FFz5EG`XFQ4VC5(f)YawvacLMhvauUXE3kK*KzW2E;7@}+N z4l2BTCjbFJCoprHNE$ph=ZoE&>y`v9I=k`8%{gCOWANiEUfdYk12{guH(BZufWEXdo<;P2X3y!iB&hbkES^rN#T-b@d4s{5 zU;S;yn!am3WN@apS8slAmXpEp?(e?acy-=t1~=rqHvLd;&sYZYkCcr0@Q7?7gO%-i zuYaJ=Kld^Cp2opHKHl))Zw$UZ?S~svI&Auk!P=v1_nw_}_C5wXce)#9rk|@}@Gs6I z=EUt!WivRm_rL{BGrLy$;kpCMjiEtN4DPx9!w-9|xFl!r<&vzGZ(Xwn>`*FJsX z(bax=*;l8%G{qU=w@2Rj{oEOwv;FNkR*3zgewa6e@f(!;LYLHy>gxhpDa_up#TGkB{0 z?8)LsZal)^vdH75`dO!+X7Fo~i+`z@{K+8(kAA<+D~nS)Z)0$}(_D7)A9*DVZYb?h zzu^V*a0Yjokz)C9V+e#CVj{9({AnD^;`0q1_qCM_Mjs7 z*_mS*ta#+tZ+q0+HZgdn=BsIKdVIW*!S;>j+DEp&lh5F+J+J<7`t&&C0eSRJ0$#7y z!*fw|>r6;f6z+2uw}m&wNG*r2PeJ%AQO_glwFKQVS2?wwXdqF{X>QU)CYN-XBmu^p zoV=T8PZI47qKzavEz$KLx<`nvl;|cA-F%|^h|>XC5z!wa`fen3A%TO9!AlG~iNQdO zGl=mDF+NO8>xpT%{I043hyOfmBicX9q!TZCrF`X%a6a%s4r>EKGKZA_A(kXV3?hyY z?axFTLUbCUa}wPHMCT>CXNhh$(JdpoK4E$;Dl&=&MQEr3{&*p@ef#*(aQ2bMH;2&h zfDn6U__9TPUBp>8H54>;|8kuGOG2WyVl3E`k(XzQ`e@( z8paup8hRPuH7ZO`nf`97i|!HACuTs*!!eJ?xMPOJl*WvTX^1@=dp&km{G#}3)g+Zo zU8EkZenq`f{hj)PI$1MNldrj^>6m0s`XMPcS)05~dqn%QHbkeC22T5Sq5N0}4MDQ1J&X6|avGUu4@HxDvDX3jHv z%_Zha^Jp_6Sur^=17n87{3WI^=Bb$Km>=37j{Px~kDndiUo}c~QkAZLTK!k`JoP&D zarOOzLG!StUUN&+Iq9{epOfN~=V|w7Pit>#+v@bXUb-Q=a^3T~1-fwkAbpYkkiJ{$ z!c>XDYuITp7-tx-7#}vRH-($y%*ke**=%;1dzkx}2bdo;4>mt(E-)9H%grOq<3Oi7 zL)+NXvDac%@o&a^RTET1{iJ$?db)bCdXM@Cb+9H|GgR|~CML<6^i5Joa;N0A+6L`U zTDdM!XV(qT9J3 zpa*Un^xsP8zhP=O^xRqMMq`tC)I2Kw%yq;@#m$RX`zZIDi_bLj5V73#+6 zUe+zqW$Ov~n_ft*N&P;xpJBNn+*oNmXmpz9n{NJToqyz1Ic&`PZ7JjgG5sx@1(vf} zz)$nPC!XWHhBF-F3|XAPTwX?b(9oC{GkATlZ zba1cmO-W)-%lNPQ%lbj7>ry)yo;4gdWE-r*Su2n-=uEp7lN|WWgRb>Q;Td?f zj0N}?HV7x+ogP9awK$3)wmEbTI~lg6&3t8b_%Gq(B1q)q$dITRQPBb1nrUxOebbVL zV-%3^r~NoQ@{56??*2R&!2CEhWFj@BlX#bV*Mf~D)R)${<9}{saq9!sZYI;;u z+pz)M?p8E4U{!0R5^Jc$ls}MoBCM{>JY`k*weYbKO%anKgQH%GYTI^P>k`F!@x`n* z;MjU+-~j=rKK7w*C02LM#abzdj94km4j>Lpx0EPq0CL5T2>N39|0jRAE#uz>qIr#2 z^cwLc8vo=}wvE?!=2NHgsTcUvT;A|8Z)nFG$MD7@ys-ywdYd;%xK>ufKd0}yR#u8X z$Kk(64W3-`cBepoh`ERMQ-(#%l^_QF_n*kW2JX^eQlar=8b43tS{lDV00Rq=_YBNbdU5K=~3yA(ks#sS)?ph zmLN-(>19?~x~!`#TXv7^e%T<|5ZO?fSN4=_xNL%Kvg`%fblEJ~tFpPW1+qo5_hd_C zD`abAn`L`t$7Darnq-l3L2i-vl;_Ix<>m4b@^SJB@>=Ho%WO%RVm^GK#H-+K!@$n8=brC8@U@Ol z?*nXH$AU_CwWmv$3U^s?f$uTYX0fK%!P_M=veXO%6eizo(r7IQ|F;?qzbS&hbx<{? zYAC)}T3H6K)7A06OZfRxes&1>D_`iuakn}KNIP@0?~T#}riVnOc(~5skAP+%oH0Kk ziNZOZe-Z!V58g$@OERYG=mQR0?x6RzA7&lSLL1=S-E8=ONnaY_b-wfg`rMgyGE1KQ zcD5n=m#l>B9obW}SH(QgJ7*9VAr<-~IfU^vrV+pHXfyCfDW((ix#4=qaLg~s2jH0R z#u|WQ{-V?X9P<&uU0ADu$zZ-Xd`pMnm_ID3)soG0%#SMegqFmNAM=OY(~^W@7#;Jw zB?Fe>nC}wr;24hiQ?b`F9P=5XljQ$bV7f4WtnyDN!pbsV6m~p@WB%g6KFoZg_%0Ho zV}4E{0LOfd=;dK_%-=`rw5c}esFyGlF>0= zJg&VA$NbA_0XXIZ$K45|V}AF*nV>BsJA@chGY%vUeI63|jFM#p^C z-2=+9dlU2$GCJm~?iGMz{_P$CIOdb?1GxVrFuBZUo%5eCgR+btyE8(cHp8)dA@nLS z9J`y*1mKuI9v12UC@>l9z70|UbFU8FKP=Fji<2XyQn4^PUhEW7){ ze{f_tcAw(-1Agq@@eg;t0eqMYb|=y^KrXvC!V@8*V|O>s03QENlJR4AN%nt-$sd$q zGT41h@4L`5I(83=FXS^EyDP?`49D*CI{yJbb}xx92{kn(6g;W!*z{yrQ*P5=nw+M> zUQIM4H#NmQrYQ_=OCjR8H~pFX;LJg}ah9gR!>D74w~;RoE(Ef%ZSEWUwf z6yFy#T1+;Rg%+eg2nhcrDU2JF|NGz`mYDS7!5&%rins2ptQk)(lW^&hfs%XgeK0qb zOXd1=k4wX)R%wu0>X62^mufUYu@7*$43{j8j+Q1S2F3Q{vH^FGG)SK;?Ru}YT{~&# z&Ov>+K@S_H4?ghFz=t2|2-)}dk_L6^Asuj^FF!7WQ&~A(V&;8vE-AA+{6J1hV!Q#; z@tq*uF;QiNw2G#=bZP&4Qlt-bmJYbbC{;>>5<5t>JvxQRr8f8z1gX^;)Sip$(4j*D zjX0I1qe;$XWo2b_=elFyI`do{MRx43ZYSqbZi}MeG+N2>N6 z%WjOg`2LWEi{Ym&?kCZ1{B25y-RQ1>H+PMN?n-#qxlXb)xo_5%nuC|mYfle+@t%XE z&22Ai){#hKVS&?~4nGO!@}@bx85U0+8(nbTqz8z$2NsD33CVPvgt-}V`8OhBdTwA} ziohe+Lfi`n1~}qMToQ?987DCmaQ!E7ysJOozmo4i8+hQ?7kC%pU6s7167HoSErGOa z84y?U20#trjgb8qA63b@I`S^qL_#){ge=0rJH##nhe$*r2FpVl%4>++mBkyr;rYlR zd}I>eAI?s*IUfEe-32M6mtX{xs0vgr#xYBHUaIG%K|wtCYaGRiQHU7ecRDj1LUXV* zCvW@xPxd>VR#%!$B*_c8t^Qk7zUj7Xlhf@guohSf3JNmd=LcQJf?*>}7E>iY%0Z)} zo7+9Cz6e>K7rG)sG3vOy;<$XoKKYg0@Sl5z zmqsYcDik9Dxlev^rt-{q<<-r~--Oaw@iJl6yzhPK)UEGGDkOXmzxZ z-FJ$xld~mFiq&iNGp*08dSaHaWe4zmL4b=_cqVzJ5g%nud?8{WL^FqP$;}A~PRZIX z%SuWKnlxd&i-$u;+f@}aYe%kykabkOOGq71Rwrmis_)aSNX-}fA+0CbJpCY z>picZHa+3Ycxk%(rYp%xV+)w#C|0a+8eM1oGHUP!9Bc9H76)8^4^)#f>Z9< zF3nylOojhZf=$x~$V&?vpRlzt!5htWo09FER6i|iykg8~Mb(_)Vc(PR3lYkz_>V>s&dmakENW!n=Do@Q+p6nUkC@9Z^6@oVLNS$g+ zFVz7}!jTE8BgYd?H75SRsl2fdI#*?Pd7~zCcWy_YA$hf3S+Va|(d<)3$|xrM06#pCH9p zt)g+Jp3YVNY)P&=&`Wiyv3)~h;!#i_CoXeUO}8~Q@ssME)3RN=>$|S6 zbM2@H8@uk#Su;FH0a^`*3LH`!cX+$Cv2IJ*wEPiye9E`P2yHfBDCOHjoK?L$lRFSZN0=byT-M9$VO;= zFm^2HnNvHeqBic!Gs>SV;f=?Y=X!>pTL@C>IZ4%G1=uol4s;c);p%%WGH*DGSec#|IgDCRAj$KF2_6^2!#1a^f z=xYlNsnkM0SBxD}F$d}vtHrgie&Y8D+ZVMt+Y5&w*d_L#cJ`Bb$}_ppEyGV?=L|oS ztGv2u`~<}qEgdzZYoW!l&kU(}qu#lO%Y3({+w6M&X&8VBM;a532nna$7@wV>+Tu>w zwu1f0|u9*+rpZzFwkb!<8rk~5SOfXq&ssF9`1u}$_V;1X)lJ%GkKnCf8?uYzv%x# zuP1K&w(pAtna`FF$9=E|=6GD%q9n7|!vp^JTnu=YyBEI5Z-|I$@kAP^R`NJ}li~Xu zd@(S35o(T~1X)N2vTh;PngOd=x)FPU@s7sN$VhYATH^3 zj`{ZVN+h(DS}b-`zBSjFZ*%6CJAm*+&`7gp%E5`>yjAhe@!M^z+s`6lsnuNOD9bTg zOeTjVKi^zONCH)Ku*X|Icw~)xsArhH%rUsE#_g!v|LKa4+sC(SNpACBPVM|vC^E2H z9A#zJoE&4G-CSyRSU}R}{N>8qpUrwzIL^(qgwOutR2~xM=b3EQ@?1-PUT&GyYRdt_ z%Zh2sW_vn*_#Xe^GaI@bPW)&eRmoPGS8gq}n=E#7zSU*~!nY!)_ATo?dEGDS=?~g# zItAZ11PP7K{4$5tX)QBbY^6C)JLs+`a}F8oa@HM<465C@aYu25yw?+zdlF6{xy@|O z$;->nDYsb4%{IFe$iu5#)vhsvYeu=Cij><|1+Ta-`j+t1XG7n3bX_i%F`FGWo2ks1 zn`bfRJ1venj>zrhl@52^u+TB3@uf?@-pjvpd(7?;Mx@Tmb(oBf97~SLT$*doF@c28 z3cIJG)Lk>Oy6%N*^JMQueRKAm+DkwDOX&NfXhNyknd`LW<$wfJsT24oHdp=j%F3Fu zx(OHe<>>!D@wL4N?h8M=a*_-=;EH_(oL1+t6Xt|@xUOlAJQMdX+#_>Lb#@(uq zHqAFA_S%TW%%wS{jyz{hnWNkaJYWQ@PQck4lq>UNzmJ9q|WE4~Pv(5d>bZCj}9XUlT-*1V4AX zp&^P8jzj$Xq-elzlaVV7Pap{yvyu`B;emt);HpI`JwN1*(l;zp>D3HR$m$R%aM=Q- ziQMb(cs;1a)gn1cJ5?m{ImzfnEq*JKp>`4ECc_g*LV=%)B7hGRg>pm=a}6e;Ob}=l z6a+sR{N(UcKsHhIsP;Z&A67@WP!Lxvy&r+Ml-bYW1t3DsPejY)B&KkrTX2dJ_185(|aS0+OLBV%K1kWXjh$IF7HQK-h zamgYE#E16qbgj0RRyxY-Fbizqz!nZ{;h+gPr~ob$eqrznhhGHzBH`D9%NAK=D~Nog z+vSB0$U!=UrUwtViD0M%nyh!iIWTo1Im@>~4?{RyqW8GQ+{w^&Cqq{whOR~oU5yyJ z{0tRNn8iF5Ag^@@pC`r~P4iqkiqZLEj?>e$fyPD}n`msNaSn|wG|r{5mBx8AwqY#r z3yV2UPNF${NDMS6^k>o%nh`(}2knS&+QrDmsY^Dltgn4@1joe_=pg*IIF38ig1;C; zUl-!>MFb97kj6ZXgJ>+HF~Jx*CdM?Er@1`MQ{L zjO>geGU!m`c5(|aQ-R~TK8o=C9g_r%E~tQra0PUBED;PAkW0zoK+Q$)zZSz}#e-TL z^fdw<9Qj{LPC|A-Okie*Y&y7SDuV$ICZ9(WSqR3ko8T2N27vFTD2fOMUUDvkgezJA z8_*w>g48@EMDh?A*r2|l#mZbA>YfCaan3KV zg=)o!<5$%3{0k^u>Wb@D@BDPl{v*@R0}7scYz(L~=za*UPlkE{P|m+t%)yWFuR>V` zKe?FSE$8^P-T9Y``LD&)E5-aq5Cga=#r)1lntHXEpAt$_Q;SJZ>2PNq0$?&QA!V zscYQ{jCDt4In4f;bG-D=vp^r{Q8WpCn&*?q;+6n{!q777_~%9Bsukgav@i zNP`|L zsi?uCI82{Qg+9e$ouXXq)k)+Qq%aBDKf+L;Wf2VKzLd99aX3gZ*&32C!nj{-95*fo z=RdN_0P_#DN{{Lh_DWZ|Fx=x1YMesgIt!d(4oMmp1LG0K8ylSF=Mg9^|};HvA$1q8)@ zEcaBw*18T9uaB0aD8xg&n)1a`Xx=W#yvXLv+tQ4A-}}w04=~R_&8szv=0ygW_bZzB z1+*PAZzC2XqIpY=Xx=Jn-df~L%|mL@ye-&+sd?OMNn{T~)H-fq66|d5H0-suSV>5a zhP`SM+bym+!zP)Uw%c42loH$R4HIyY+6_)WfIlV~78hXHIW(*m7fz|y-3~D9EH!K$ zHSABHVMr|+_C_))iVcE>Ek?*^SX?8+euLo%`9P2D_oXQelR%A&B$fi?w*eZPC}yF_ zOv?mG%6*O$QmwBvVXZ@HD7gX61}-=!Zosw7r_@%2s8Xa>8K}W+6HKa112!0d%XE|| zRhyYAanO_xC;~fhaa`UEP~sF-VvE?b1C;ou00n$X>_kXZVv!K2#3pm|N_-QbL=IKr zb@QD{tf3Vn_P@8ySQ9&_5-ZLAn%I&OsKg$GL?vLJMk>${tNrF(lz24F<(J8R-2q>%c= zf*h=g15}A+IcTHUC%(pI!KcIz2#HFpN()rt&$}ow*#ZTmny^wO_BK-DLVyxSsS<~% z62As0u`fMPiK7UKN_?CisKi=J^EI(OKnXZRfN@hTjcNiZq?&lsf;DlRDzU`kuZiz7 z0PU-ZlL(1Qe3}uc#Ayqx$23S|6y;qA(7;AD*loe~1Qs~s0mTV8F|)<>panNTNH%2#%9+>}=X%%y2JB3*tAI}Ab|%z02G|)P0D&&zG>x+c;^x9~jc?e+;2RA^ z%|!D5D%a467SS;R9L8Z!MD2nIdl&2i30WdT!(l@SX?SELmY%UiheQ{L(>}b?TL&3y zWwBUn$wMNYg0IDj-62!p1_n+tv~)1{ek(}T%U}acH(?YT0$4InO`xJ-PbN}^!0S@b z{72DhpMGSm3JV~Gs2|w|2)}Mzy^5SyHPV7iR5#K9W!*zMN`mbo#A{(YL>9@qz;+=7 z#liEH2Gbx29$-FE4HWxiE#cUMsmUSnsNq1NvrvMy1P+W6VWi7jA=s-0SGCtM#Nigo zYpU$7YAx)fT-8H_lE9r*iQugfhB@5M8h4dYT_aQg4yY`cvd7>>8;g7) zr~8_4Ax-Ey%3cM#cn_u7F2`M=Nb|i&qZ9f$9Kz!zJ~u_llLCmL`#Gv%890h-ss!)o zVGfTd>5$y$R}G6PcKW zN{3gd8VY~UhPN>qmsyz<3 zS7p=+PJ5-tArW6u(0y)8KY>Xrc-_NU{*++cs*6?hPB1mDonZGMs}xn0zO1I&3$5fC zJk&8-m1$HS50(!?ltP)hEQ7U|Cf!*Lqkmr)RU?p`;v0t8_GMCTA8FJPYs z4+FoM9>1?4JuUGZW)P+1E+gYZaQdM+mx8H*GeTgL;as&Zl)&x-sJZ%3f-WYUJ^%wr z%*WqvaPol;3Y37GM>$JK4hsRY7LamoKOCR;%fZVJ8gkr0IgypxJ#fWi2nHjR;)8-T0KrLEg2xqU?0Np}QCA=GFw~FOU6zJoci}E( zV~wp0^$)d8V#X}m=5?X|(Q`@65Ie)wQ1s5+b>x7`Vt2nC>K{3^VYG)T{Ub*lCP3U| zm@EuS^{M)WST5Q>3XCw)q|UrOjGo8>GEM%>!!%Pg_=3nKv6=A^Fg7lS(OrJ?RK9UB zJshc|aj`O792e`urE&2=ZYFeKsGU#69{d&dUjMk*i1f6Re?hyoZ(M8(_l=8>!|AyA zKAesV4&B4x&;d3azQxjFuLq9-ppOD4IoA-z!H@87&@MkdoZDyQxN~7rcVBSj^3pk{ z>Sud-^a=dMt_~;kWmbHA0i-UDrYDC2p>s7%?Jm2APR1oo*VmFeXX!ha3w<40FejoA zUSd-niU{bN$0GcF^E}NUMRXZ}d9nuA0_tLig}`22E`m5-#C5?_Q{@mGc8?2Itl=K} z5CEhVMihD};sKw~4Utr+*u6JJ((awv+``brMKAXBt&y-O!z@ROz%^3)_GLAdm2d^) zs;Tz0Z!fK+BJJ;y{@(ps3py%n{!!6hkciv2?>OA170N2?ZmrNnEaY{9g@)GN>=qqR zcy|GVuQV=+gUjr23+Vz!7u1imxT#>7YQipH2uee1UyEX2?YtR9wTulIgIXcWo+Xhk zilTdlfNWT(vPxO@dYUaZ?rxD&nlugvJDy2V^@Da&Wg~i49alx;#vLYe7)PRuhQl|a$ih6RxGm8f`7w|D))60n5Vx(T*;Unx z_jQ00K>k}2jDB#>w1tR=1#e>rf@gt_X8$f`KZn^IWN!mMG3?RdW(xx(e@TLaIwq#J z1up_7Q8V0s;sb9)iJH9uOwi9t0`CJbmxIlB%QzCWDQa$O(SHWoo}~T}q!t5``6YcWr%8Y_WS=80{aa)-6=q6LN z2KNT|z#D>O&8O6w*5um)e0%{2S0%#{2Hw+?p`+pM;z~hpKmcYYIDFx?6#c&b%AN&u zG<%Miy#%xUl|47vSJ_kH@&WSJV1YXWk6yHVJ`dvdH15FX1>u}bu~4ay7W4iau5IpG z%jW&sFzs;!M04-pQpOQHK~U4yi#EkWTeZfv;-O!W4asoar7mRvK2WBiNwAw2D?Jf) zhX>veq)J}{w+V+@v?1FI@$m&9{6&bP1-1!NrJpGr0SL(1A<#-c2Cslh-wAXy`)e`# zC}wlM9===fRr(hKt@K|7y4Lw*(uC;lU3qbf&Ds>l=FH$9oHg=he<>B{bDmCc{yaG(x4umxOD>3^pX8TRr zmFhETb1F6I6ndub4B)HbNJl=87yAyRpzqKz$-%7|(4zQrBI6{mwVkgq&x6Yw@|LFw z$kAssc*dv}=pn--HF_2J(t+vJ2k`L)pqs9xTOgCrACEo4$O=~(oYmY8!DDwi@Gyq% zZhAawZsFaV1|B4+5R~|QI-TVo5c*fRJVKS-JrovBuiNhO3IN0LuVxr7XLL2EXDsCI zpf|>Xx5827aa4`~4WuJk9kQI9-UDAn%_;zgB%#J#jzVgLQc+m5Nd@D)E{}6GrFOzfTQd?5nQ-Lspu*MO_LO{n20Bkf>*_M7b;Uv_ zL8E!NnqC3;WZ{udyl);0YwmE9Rg0&&;Z}L|zkMj3vrR8w8%&}%eQr@ zL)F{v_PXqqU7yhkU7t}uNsGUsqI>mL0<`$>GOvKU2pj?`{{diw3NKqk3Exr)Bwg%O zbca>}RVZ%FXrE;agt3(W_o^%?Ogab{oYmBk(Xo4b5C@w(e^H0KlPVJ{OG_!BBMF)4 z7wE2*_%x_GA)ge=2O})&aO@ z(p*W9)U+hHN~DeLL0VGkmM>{>H3LTTwdlfyCATdRD1w7G;2{X&i((PAM2lBJbZW;p zgk^ZMw^>W~ML6S2VHKheH$ksM^wlP4x*MCO!;hK*d2d1L<+{cqcOZJJuCd5Hh(6W? zeE`wdo1hONdWOES$m59Kt=CbDKhi@J;qGm9zk`70;I~%KVLf~WFK9=$SN<3XY4!#& zdnaZ?ElPXkPxQWJ_d`AImHlfYe2qa#;SGTo*T!$LI0OM#R?PoS9}0`5PH!-p%sG}^ zYo3iP>yM8w0MU537KYa(L(>%Jt4qw;VbS50lTIRp|?&P$wuL5>&pg+ z0ERVQ=Ud~a8DPVP20-2+QQ}d9zuhH;=pLfLCks*_Ygtrd38(xL^gan^K>}XkTxbI# zYK?SgEua^KK5H>SMcnTb0Vxo%s)>lD^g59mVepCgz$l8?0~>g_t)wDO+(krZp9n~S zh;>awob`(U4~4X`y(o!TjJw{2CMx0`dWqN6ib9_VNP&n=O+>83D?hO*Og<5-O`;WB z@%x&CrZjB*Lni!~<&Hors>mk-QXpbW6A`EUBFsJ!XC)Ck1>pUu z))_fe#B6$b)>Om;J`s=t5eJ%xSb$e;q7}J55%1=RR{VgUi0lzA-;!V7(6Rm&~qtt2Nwun}o%z(_@ z7V5Rz>${=zRTfMq9O>aZAwUXt^7LX37(z)pdmQu&fKOK>0Y88MGOkdZJ~rdfpcBci zWLSY<_1N7N+`-l`y#IJAwNS1&QFch5~d2zx&)83egq#1{J=(6Mz7q6PUSGBn_S0{mWgS*DVQI zczWZdTXVj=!r;eOyu2~I;Ms)??(@vI)e{b$+s5E2o&IGsp|)ffgO9Wx_VUoL>W49S=%dremAZml4F0K0qCV!vPdgYqV95ec?aBjd7`*=M z%bSl6x>d~J%$hI87LOX`gFC#r_wiG4uW&41*6W=gv-&M248A#V44DR6U+=bs$Xk&1a{m7Ax zm*=fw@WJl0r_}epKY_vgBbB2+I4obl;1;dAtbe%czrJB`x8nnUd;DOZ>kPj3%9$H4 zw%PP4gH=b@?m0d2^g|4`?XVx5miy}j24A%uHniLJbPpc=Q8-szrDM1;@{u()&Gg-mTy&Ry;&@OQtzLh zD)@MAHiLh1_j~1X*$)F59NTq&Zl~)LS~GaE=JZL|BR3vlaCOX&RhsEP4`uM|n8jCz zP5QW=!K2=boUu4FYb%3uZHDTT-G>QI$z?eAKmL8uGlM2f0X41J?-6E{rdbG27fm7{Bylsiv}}zg*@Yvw*A-o z+ULZ!r(Zh!;lv{>Kj-$2o!8UW9AxmwXAcDTesi2F{GvKBC3-_b%Us4h+0L|1w{P_QCAW5 zM53Ng)E{wbAgdsndZM|HWG^6au+ch+b_daFiEb*%fa;>)Pk3-4MV&uV_x^vzzIouD17J*w@jdq)?ne_H>wzAmmHzH5AO z{DAn!Lop3E-deXuqZ}P-sv$8@tN;yNhQh7vqPMMa{H>EV?N=kaF zCG|{dLYgXVtLm`o4^@~tMQu|*tahrORnJr}Q}@x>HQ#Ei*>kgRWe?VF)@JBl)cvOG zrC+6wFvJ?#8Zr%9gW1s0P-y6G=w;|{c+5~@a2hHNZo?=8A%*eXGYOVv`XQFm4kQrD=TSJ$eeH2pOdntIKB*$c9Rv`*~~tyVWxcS$!uzg{0@NHnAw z)CPkg-%w!aYA81JF$^?3X(%(e3^j(~hOwYi$w_Y}Ig`gF6Xlc2;mRq> z#me2vGs@7EqLjfYXHw!*O{w3dhNWestyLXV{jO4|+o>(;Vs)u{w0fHQeRZbhDa|LE zw%Py4K9Sv3yI32ptJdw+S@f^#ujw1hgAa0AA5A!)5SH|MQs3k;$!C-ME31_gm2W9O zQJz#@7Yr$bQjVu^shZSnsaI2z(-x`rs!ppKRISuHbr<#HYPb3&^#XOQW}s%NCL+5g zdtY|0c8>O@_9j*{LhKMbD9gBrXQF6F_)dlY5&G) zk8#>UPWLXS3*q!bIsI<#o~mXkd(dGmN^%JJuBU^0g)}9JIZfk#XfA5{XRpg{qkUHU zqqa!*o-R~hso!%?iG#pmb(0}%S zA(3hS9sM>SmR_(V(pbD~$qLp5=LF{m7X)_=E)MP!JTUml;Id|}Vc_HMgg>EkEr6~y zfv#{PC0owYx1HLNL+!|-U5iN$e3wAix>xucd|Ji={0SR`6YxzBArqS%#SrTcSrI2A zHb>5H;f=Z)H8z^WOo|DMof;b#z|Bv4XX?AAG#sOVgfH#G;gMeq40ZSSfdJ+|QbWd5 zLo&p>+`AS$9`SkP+!pSr%Tc4FZ%0pv35lH&8{2YB0Jpmp%??=Aj#G&fsKm^BNIVfy z7dfwmC+bSnnCOP+i7}zEug11)IktI;V!cQ)s|`4|HV!->;MB(+>Q-WP=P%YwL1e^A zVRis<_yrojMB~XcewoIv(0B@sr_y+Q=8k}o)|{5drK14&wdo|O zp?%~QjW5DfIY+fiby9Uh6{A+E3)GLOtJD+K^VN}>=6D6-k^+{IK)gTQLOEadrfiXH ziEM>zm29nSgKU$mPPSY2o$RRWH`ygwm^?zJK1e=T z?vy_*e?~q|K1u$Pe2RR!e3pE!yjH$Y{;qt9e1&|C{B!vp`7!zL@&A9tWvB~Y*K7d>`?5XOORj3rm5t++4a9Pnzih# z*EG>o*=8|N@Se}#VLXFDgb(2-58+^627hiF1n*$@CY^r`F>x?S-Ecx82C_JKIG&CM zaJZq?fVUk9Gip27HCsk<6Jr>o;{2J!P{{LC=$SH6_N zaktY0q@B9;z>TVX`hKEPJX~k+he0zC&X}JFip4pde;NPc557gjOERYGsC`y*@BZ(p zJ}5j?h&I5tyG8K#l2RJsby9jCeeWndS*R#lRHQAsTG+N|d(q^g591&1(!Dl$;7T0^mkNFn!190Jze;C(GM#p@J_>m&RF~2`9 z-3-Tk+jw8iaLk{p3cxWRWk=LVEzesKKwlF>0=Jg&VA$NbAV0XXIZ$K45|V}AF*nVBsJA@chGY%vUdd63|pHM#p^CodU|TdlU2$GCJm~?i_$){_TPQ9P>$c z1>AoUm|W(w?*5-JgR+btyE8(cHp8)dA@nLS9J`xI3BWObJS@`xQD8FIeH)$%7>?c9 zp-X__*u6yiyGUhp%%9)m9(3#;4^PUhEW7){KX7C?cAsLs2S0Z2c+Z`003RlU-HF^E zAeY@6;favZvAY{v0FQqs$@sCmB+I|Ui ziN=P3LmCa@f!J4Vu_4L8y>ANXzv5a1iy&CWmdy0!(we{)j%?{8*B{? zd0Z8svf?Rkklm}ZEF_~q zR{W5ZpP0ubn>cm54i71~)DE5CKgh{!m!ySsQU;{c+a>EDolMhQuB>ObOxeR(vf^$! zSqoW6yEZaaK}MKDW`=))ATyalT62kQ+O%m)BQDvPu2*n{g@t*YxK0?jES^iG$n>7d zRthfjjyMi5nx07zr_(sINi60jM}cOM5wToE3rk`Km)pkw%WIp#HOAT6Whl6I5phX5 z2?;dO){>ZbmqfBPDe12f!!4;`!!S(edc>?+se882)REUL?+Lcb8RIEjs%! z_;OcQZg<1C&UHac(;g_?JmJ8_v#Ou_zTE8qiM->3%{mgJD=)LzbK$>)%XjA3oOwn^ z9UEP6-lPYJmircp2Z^95I0O zCvtp#Prj#{?>Q5A;7A-e2N?Hr63&y>HK9t?B=zA8pP`$`!PP&&E==_`LKzE zY$yp?goAI0^R*lz5rr5m4{0c$LKOLhy!Jbuj~T?rr1CxC>@<_(;cwFOA%*lo7y%`! Y0+ow#{1Tp*X?R&k2+#eQNO6SxACFOqlK=n! literal 0 HcmV?d00001 diff --git a/book/.hvm/target/release/deps/nohash_hasher-dc8a50f19f38f70e.d b/book/.hvm/target/release/deps/nohash_hasher-dc8a50f19f38f70e.d new file mode 100644 index 000000000..6503515cc --- /dev/null +++ b/book/.hvm/target/release/deps/nohash_hasher-dc8a50f19f38f70e.d @@ -0,0 +1,7 @@ +/Users/v/vic/dev/kind2/book/.hvm/target/release/deps/libnohash_hasher-dc8a50f19f38f70e.rmeta: /Users/v/.cargo/registry/src/index.crates.io-6f17d22bba15001f/nohash-hasher-0.2.0/src/lib.rs + +/Users/v/vic/dev/kind2/book/.hvm/target/release/deps/libnohash_hasher-dc8a50f19f38f70e.rlib: /Users/v/.cargo/registry/src/index.crates.io-6f17d22bba15001f/nohash-hasher-0.2.0/src/lib.rs + +/Users/v/vic/dev/kind2/book/.hvm/target/release/deps/nohash_hasher-dc8a50f19f38f70e.d: /Users/v/.cargo/registry/src/index.crates.io-6f17d22bba15001f/nohash-hasher-0.2.0/src/lib.rs + +/Users/v/.cargo/registry/src/index.crates.io-6f17d22bba15001f/nohash-hasher-0.2.0/src/lib.rs: diff --git a/book/Bool.and.kind2 b/book/Bool.and.kind2 index 362802af9..9f5135798 100644 --- a/book/Bool.and.kind2 +++ b/book/Bool.and.kind2 @@ -1,5 +1,7 @@ -Bool.and (a: Bool) (b: Bool) : Bool = +use Bool.{true,false,and} + +and (a: Bool) (b: Bool) : Bool = match b { - Bool.true: b - Bool.false: Bool.false + true: b + false: false } diff --git a/book/Bool.false.kind2 b/book/Bool.false.kind2 index 5e65f17ff..5a7366886 100644 --- a/book/Bool.false.kind2 +++ b/book/Bool.false.kind2 @@ -1,2 +1,2 @@ -Bool.false : Bool = +false : Bool = ~λP λt λf f diff --git a/book/Bool.lemma.notnot.kind2 b/book/Bool.lemma.notnot.kind2 index 78add0dd3..35effe2c8 100644 --- a/book/Bool.lemma.notnot.kind2 +++ b/book/Bool.lemma.notnot.kind2 @@ -1,6 +1,6 @@ use Bool.{true,false,not} -notnot (x: Bool) : {(not (not x)) = x} = +notnot (x: Bool) : (not (not x)) == x = match x { true: {=} false: {=} diff --git a/book/Equal.apply.kind2 b/book/Equal.apply.kind2 index 4a00c7666..6e3270c73 100644 --- a/book/Equal.apply.kind2 +++ b/book/Equal.apply.kind2 @@ -1,10 +1,11 @@ use Equal.{refl} -apply A B (f: ∀(x:A) B) (a: A) (b: A) (e: {a = b}) : {(f a) = (f b)} = +apply (f: A -> B) (e: a == b) : (f a) == (f b) = match e { refl: {=} } + //Equal.apply //: ∀(A: *) //∀(B: *) diff --git a/book/List.Church.cons.kind2 b/book/List.Church.cons.kind2 new file mode 100644 index 000000000..b04380238 --- /dev/null +++ b/book/List.Church.cons.kind2 @@ -0,0 +1,3 @@ +cons (head: T) (tail: (List.Church T)) : (List.Church T) += λP λcons λnil + (cons head (tail P cons nil)) diff --git a/book/List.Church.kind2 b/book/List.Church.kind2 new file mode 100644 index 000000000..d36f54423 --- /dev/null +++ b/book/List.Church.kind2 @@ -0,0 +1,5 @@ +List.Church (T) : * = + ∀(P: *) + ∀(cons: T -> P -> P) + ∀(nil: P) + P diff --git a/book/List.Church.nil.kind2 b/book/List.Church.nil.kind2 new file mode 100644 index 000000000..46cdc3474 --- /dev/null +++ b/book/List.Church.nil.kind2 @@ -0,0 +1,3 @@ +List.Church.nil (T) : (List.Church T) += λP λcons λnil + nil diff --git a/book/List.Folder.cons.kind2 b/book/List.Folder.cons.kind2 deleted file mode 100644 index 582c11edf..000000000 --- a/book/List.Folder.cons.kind2 +++ /dev/null @@ -1,5 +0,0 @@ -List.Folder.cons -: ∀(T: *) ∀(head: T) ∀(tail: (List.Folder T)) - (List.Folder T) -= λT λhead λtail λP λcons λnil - (cons head (tail P cons nil)) \ No newline at end of file diff --git a/book/List.Folder.kind2 b/book/List.Folder.kind2 deleted file mode 100644 index fae7e56d4..000000000 --- a/book/List.Folder.kind2 +++ /dev/null @@ -1,7 +0,0 @@ -List.Folder -: ∀(T: *) * -= λT - ∀(P: *) - ∀(cons: ∀(head: T) ∀(tail: P) P) - ∀(nil: P) - P \ No newline at end of file diff --git a/book/List.Folder.nil.kind2 b/book/List.Folder.nil.kind2 deleted file mode 100644 index dcdefc8f9..000000000 --- a/book/List.Folder.nil.kind2 +++ /dev/null @@ -1,3 +0,0 @@ -List.Folder.nil -: ∀(T: *) (List.Folder T) -= λT λP λcons λnil nil \ No newline at end of file diff --git a/book/List.cons.kind2 b/book/List.cons.kind2 index 7702507ef..7c1fee91d 100644 --- a/book/List.cons.kind2 +++ b/book/List.cons.kind2 @@ -1,3 +1,2 @@ -List.cons -: ∀(T: *) ∀(head: T) ∀(tail: (List T)) (List T) -= λT λhead λtail ~λP λcons λnil (cons head tail) \ No newline at end of file +List.cons (head: T) (tail: (List T)) : (List T) = + ~λP λcons λnil (cons head tail) diff --git a/book/List.fold.kind2 b/book/List.fold.kind2 index 4bbffccda..85b97072d 100644 --- a/book/List.fold.kind2 +++ b/book/List.fold.kind2 @@ -1,7 +1,7 @@ -List.fold -: ∀(T: *) ∀(list: (List T)) (List.Folder T) -= λT λlist λP λcons λnil - use fold_P = λxs P - use fold_cons = λhead λtail (cons head (List.fold T tail P cons nil)) - use fold_nil = nil - (~list fold_P fold_cons fold_nil) \ No newline at end of file +use List.{cons,nil} + +List.fold (xs: (List A)) (c: A -> B -> B) (n: B) : B = + match xs { + cons: (c xs.head (List.fold xs.tail c n)) + nil: n + } diff --git a/book/List.map.kind2 b/book/List.map.kind2 new file mode 100644 index 000000000..1a1ca819e --- /dev/null +++ b/book/List.map.kind2 @@ -0,0 +1,16 @@ +use List.{cons,nil} + +map (xs: (List A)) (f: A -> B) : (List B) = + fold xs { + cons: (cons (f xs.head) xs.tail) + nil: [] + } + + +//map A B (xs: (List A)) (f: ∀(x: A) B) : (List B) = + //(List.fold _ xs _ λhλt(cons _ (f h) t) []) + + //match xs { + //cons: (cons _ (f xs.head) (map _ _ xs.tail f)) + //nil: [] + //} diff --git a/book/List.nil.kind2 b/book/List.nil.kind2 index 03aac25bd..1231de8e3 100644 --- a/book/List.nil.kind2 +++ b/book/List.nil.kind2 @@ -1,3 +1,2 @@ -List.nil -: ∀(T: *) (List T) -= λT ~λP λcons λnil nil \ No newline at end of file +List.nil : (List T) = + ~λP λcons λnil nil diff --git a/book/Nat.lemma.bft.kind2 b/book/Nat.lemma.bft.kind2 index 1c0f67dc4..8e4b05ee4 100644 --- a/book/Nat.lemma.bft.kind2 +++ b/book/Nat.lemma.bft.kind2 @@ -2,6 +2,6 @@ use Nat.{succ,zero,half,double} bft (n: Nat) : {(half (double n)) = n} = match n { - succ: (Equal.apply _ _ succ _ _ (bft n.pred)) + succ: (Equal.apply _ _ _ _ succ (bft n.pred)) zero: {=} } diff --git a/book/_main.hvm2 b/book/_main.hvm2 new file mode 100644 index 000000000..382aeeb4b --- /dev/null +++ b/book/_main.hvm2 @@ -0,0 +1,21 @@ +_Char = 0 +_List = λ_T 0 +_List.Folder = λ_T 0 +_List.cons = λ_T λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail) +_List.fold = λ_list + let _list.P = 0 + let _list.cons = λ_list.head λ_list.tail λ_P λ_c λ_n ((_c _list.head) (((((_List.fold) _list.tail) _P) _c) _n)) + let _list.nil = λ_P λ_c λ_n _n + (((_list _list.P) _list.cons) _list.nil) +_List.map = λ_A λ_B λ_xs λ_f (((((_List.fold) _xs) 0) λ_h λ_t (((_List.cons 0) (_f _h)) _t)) (_List.nil 0)) +_List.nil = λ_T λ_P λ_cons λ_nil _nil +_Nat = 0 +_Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n) +_Nat.zero = λ_P λ_succ λ_zero _zero +_String = (_List _Char) +_String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail) +_String.nil = λ_P λ_cons λ_nil _nil +__main = ((((_List.map 0) 0) (((_List.cons 0) 1) (((_List.cons 0) 2) (((_List.cons 0) 3) (_List.nil 0))))) λ_x (+ _x 1)) + +main = __main + diff --git a/book/_main.hvmc b/book/_main.hvmc new file mode 100644 index 000000000..b317df7dd --- /dev/null +++ b/book/_main.hvmc @@ -0,0 +1,17 @@ +@cons = (a (b ((a (b c)) (* c)))) + +@foo = ({3 (a b) c} (a (d e))) + & @cons ~ (b (f e)) + & @map ~ (c (d f)) + +@main = a + & @map ~ ((<+ #1 b> b) (c a)) + & @cons ~ (#1 (d c)) + & @cons ~ (#2 (e d)) + & @cons ~ (#3 (@nil e)) + +@map = (a ((b (@nil c)) c)) + & @foo ~ (a b) + +@nil = (* (a a)) + diff --git a/book/_main.kind2 b/book/_main.kind2 index 6ee830915..e7191392c 100644 --- a/book/_main.kind2 +++ b/book/_main.kind2 @@ -4,8 +4,42 @@ //use Nat.{succ,zero} -_main : U60 = - (U60.fib 6) +_main: (List U60) = + (List.map _ _ (List.cons _ 1 (List.cons _ 2 (List.cons _ 3 (List.nil _)))) λx(+ x 1)) + +//_main : (Maybe U60) = + //(Maybe.bind _ _ (Maybe.some _ 1) λx + //(Maybe.bind _ _ (Maybe.some _ 2) λy + //(Maybe.some _ (+ x y)))) + + +//main : (Maybe U60) = { + //x = !bar + //y = 80 + //for i in [1,2,!(foo y)]: + //for j in [10,20,30]: + //x += i + //if x > j: + //return x + //return x + y +//} + + +//fold xs: + //cons: + //xs.head + xs.tail + //nil: + //0 + +//for x in xs: + + + + + + + + //_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) = //switch a { diff --git a/book/_tmp.hvm2 b/book/_tmp.hvm2 new file mode 100644 index 000000000..2e2409b7c --- /dev/null +++ b/book/_tmp.hvm2 @@ -0,0 +1,14 @@ +_Char = 0 +_List = λ_T 0 +_List.cons = λ_T λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail) +_List.map = λ_A λ_B λ_xs let _xs.P = 0 let _xs.cons = λ_xs.head λ_xs.tail λ_f (((_List.cons 0) (_f _xs.head)) ((((_List.map 0) 0) _xs.tail) _f)) let _xs.nil = λ_f (_List.nil 0) (((_xs _xs.P) _xs.cons) _xs.nil) +_List.nil = λ_T λ_P λ_cons λ_nil _nil +_Nat = 0 +_Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n) +_Nat.zero = λ_P λ_succ λ_zero _zero +_String = (_List _Char) +_String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail) +_String.nil = λ_P λ_cons λ_nil _nil + +main = (_List.map (_List.cons 0 1 (_List.cons 0 2 (_List.nil 0))) λx(+ x 10)) + diff --git a/book/_tmp.kind2 b/book/_tmp.kind2 new file mode 100644 index 000000000..3d2b2fe85 --- /dev/null +++ b/book/_tmp.kind2 @@ -0,0 +1,19 @@ +WARNING: unsolved metas. +WARNING: unsolved metas. +WARNING: unsolved metas. +WARNING: unsolved metas. +WARNING: unsolved metas. +_Char = 0 +_List = λ_T 0 +_List.cons = λ_T λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail) +_List.map = λ_A λ_B λ_xs let _xs.P = 0 let _xs.cons = λ_xs.head λ_xs.tail λ_f (((_List.cons 0) (_f _xs.head)) ((((_List.map 0) 0) _xs.tail) _f)) let _xs.nil = λ_f (_List.nil 0) (((_xs _xs.P) _xs.cons) _xs.nil) +_List.nil = λ_T λ_P λ_cons λ_nil _nil +_Nat = 0 +_Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n) +_Nat.zero = λ_P λ_succ λ_zero _zero +_String = (_List _Char) +_String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail) +_String.nil = λ_P λ_cons λ_nil _nil + +main = _List.map + diff --git a/kind2.ts b/kind2.ts deleted file mode 100755 index 65ae77c4a..000000000 --- a/kind2.ts +++ /dev/null @@ -1,436 +0,0 @@ -#!/usr/bin/env ts-node - -// TODO: move the parser to HVM - -// ICC: Parser, Stringifier and CLI -// ================================ - -// List -// ---- - -type List = - | { tag: "Cons"; head: A; tail: List } - | { tag: "Nil"; }; - -// Constructors -const Cons = (head: A, tail: List): List => ({ tag: "Cons", head, tail }); -const Nil = (): List => ({ tag: "Nil" }); - -// Term -// ---- - -type Term = - | { $: "All"; nam: string; inp: Term; bod: (x:Term)=> Term } // ∀(x: inp) bod - | { $: "Lam"; nam: string; bod: (x:Term)=> Term } // λx bod - | { $: "App"; fun: Term; arg: Term } // (fun arg) - | { $: "Ann"; val: Term; typ: Term } // {val:typ} - | { $: "Slf"; nam: string; bod: (x:Term)=> Term } // $x bod - | { $: "Ins"; val: Term } // ~val - | { $: "Set" } // * - | { $: "U60" } // #U60 - | { $: "Num"; val: BigInt } // #num - | { $: "Op2"; opr: string; fst: Term; snd: Term } // #( fst snd) - | { $: "Mat"; nam: string; x: Term; z: Term; s: (x:Term) => Term; p: (x: Term) => Term } // #match k = x { zero: z; succ: s }: p - | { $: "Txt"; txt: string } // "text" - | { $: "Ref"; nam: string; val?: Term } - | { $: "Let"; nam: string; val: Term; bod: (x:Term)=> Term } - | { $: "Hol"; nam: string } - | { $: "Var"; nam: string; idx: number }; - -// Constructors -export const All = (nam: string, inp: Term, bod: (x:Term)=> Term): Term => ({ $: "All", nam, inp, bod }); -export const Lam = (nam: string, bod: (x:Term)=> Term): Term => ({ $: "Lam", nam, bod }); -export const App = (fun: Term, arg: Term): Term => ({ $: "App", fun, arg }); -export const Ann = (val: Term, typ: Term): Term => ({ $: "Ann", val, typ }); -export const Slf = (nam: string, bod: (x:Term)=> Term): Term => ({ $: "Slf", nam, bod }); -export const Ins = (val: Term): Term => ({ $: "Ins", val }); -export const Set = (): Term => ({ $: "Set" }); -export const U60 = (): Term => ({ $: "U60" }); -export const Num = (val: BigInt): Term => ({ $: "Num", val }); -export const Op2 = (opr: string, fst: Term, snd: Term): Term => ({ $: "Op2", opr, fst, snd }); -export const Mat = (nam: string, x: Term, z: Term, s: (x:Term) => Term, p: (x:Term) => Term): Term => ({ $: "Mat", nam, x, z, s, p }); -export const Txt = (txt: string): Term => ({ $: "Txt", txt }); -export const Ref = (nam: string, val?: Term): Term => ({ $: "Ref", nam, val }); -export const Let = (nam: string, val: Term, bod: (x:Term)=> Term): Term => ({ $: "Let", nam, val, bod }); -export const Hol = (nam: string): Term => ({ $: "Hol", nam }); -export const Var = (nam: string, idx: number): Term => ({ $: "Var", nam, idx }); - -// Book -// ---- - -type Book = {[name: string]: Term}; - -// Stringifier -// ----------- - -export const name = (numb: number): string => { - let name = ''; - do { - name = String.fromCharCode(97 + (numb % 26)) + name; - numb = Math.floor(numb / 26) - 1; - } while (numb >= 0); - return name; -} - -export const context = (numb: number): string => { - var names = []; - for (var i = 0; i < numb; ++i) { - names.push(name(i)); - } - return "["+names.join(",")+"]"; -} - -const compile_oper = (opr: string): string => { - switch (opr) { - case "+" : return "ADD"; - case "-" : return "SUB"; - case "*" : return "MUL"; - case "/" : return "DIV"; - case "%" : return "MOD"; - case "==" : return "EQ"; - case "!=" : return "NE"; - case "<" : return "LT"; - case ">" : return "GT"; - case "<=" : return "LTE"; - case ">=" : return "GTE"; - case "&" : return "AND"; - case "|" : return "OR"; - case "^" : return "XOR"; - case "<<" : return "LSH"; - case ">>" : return "RSH"; - default: throw new Error("Unknown operator: " + opr); - } -}; - -export const compile = (term: Term, used_refs: any, dep: number = 0): string => { - switch (term.$) { - case "All": return `(All "${term.nam}" ${compile(term.inp, used_refs, dep)} λ${name(dep)} ${compile(term.bod(Var(term.nam,dep)), used_refs, dep + 1)})`; - case "Lam": return `(Lam "${term.nam}" λ${name(dep)} ${compile(term.bod(Var(term.nam,dep)), used_refs, dep + 1)})`; - case "App": return `(App ${compile(term.fun, used_refs, dep)} ${compile(term.arg, used_refs, dep)})`; - case "Ann": return `(Ann ${compile(term.val, used_refs, dep)} ${compile(term.typ, used_refs, dep)})`; - case "Slf": return `(Slf "${term.nam}" λ${name(dep)} ${compile(term.bod(Var(term.nam,dep)), used_refs, dep + 1)})`; - case "Ins": return `(Ins ${compile(term.val, used_refs, dep)})`; - case "Set": return `(Set)`; - case "U60": return `(U60)`; - case "Num": return `(Num ${term.val.toString()})`; - case "Op2": return `(Op2 ${compile_oper(term.opr)} ${compile(term.fst, used_refs, dep)} ${compile(term.snd, used_refs, dep)})`; - case "Mat": return `(Mat "${term.nam}" ${compile(term.x, used_refs, dep)} ${compile(term.z, used_refs, dep)} λ${name(dep)} ${compile(term.s(Var(term.nam,dep)), used_refs, dep + 1)} λ${name(dep)} ${compile(term.p(Var(term.nam,dep)), used_refs, dep + 1)})`; - case "Txt": return `(Txt \`${term.txt}\`)`; - case "Hol": return `(Hol "${term.nam}" ${context(dep)})`; - case "Var": return name(term.idx); - case "Ref": return (used_refs[term.nam] = 1), ("Book." + term.nam); - case "Let": return `(Let "${term.nam}" ${compile(term.val, used_refs, dep)} λ${name(dep)} ${compile(term.bod(Var(term.nam,dep)), used_refs, dep + 1)})`; - } -}; - -// Parser -// ------ - -export type Scope = List<[string, Term]>; - -export function find(list: Scope, nam: string): Term { - switch (list.tag) { - case "Cons": return list.head[0] === nam ? list.head[1] : find(list.tail, nam); - case "Nil" : return Ref(nam); - } -} - -export function skip(code: string): string { - while (true) { - if (code.slice(0, 2) === "//") { - do { code = code.slice(1); } while (code.length != 0 && code[0] != "\n"); - continue; - } - if (code[0] === "\n" || code[0] === " ") { - code = code.slice(1); - continue; - } - break; - } - return code; -} - -export function is_name_char(c: string): boolean { - return /[a-zA-Z0-9_.-]/.test(c); -} - -export function is_oper_char(c: string): boolean { - return /[+\-*/%<>=&|^!~]/.test(c); -} - -export function parse_word(is_letter: (c: string) => boolean, code: string): [string, string] { - code = skip(code); - var name = ""; - while (is_letter(code[0]||"")) { - name = name + code[0]; - code = code.slice(1); - } - return [code, name]; -} - -export function parse_name(code: string): [string, string] { - return parse_word(is_name_char, code); -} - -export function parse_oper(code: string): [string, string] { - return parse_word(is_oper_char, code); -} - -export function parse_text(code: string, text: string): [string, null] { - code = skip(code); - if (text === "") { - return [code, null]; - } else if (code[0] === text[0]) { - return parse_text(code.slice(1), text.slice(1)); - } else { - throw "parse error"; - } -} - -export function parse_term(code: string): [string, (ctx: Scope) => Term] { - code = skip(code); - // ALL: `∀(x: A) B[x]` -SUGAR - if (code[0] === "∀") { - var [code, nam] = parse_name(code.slice(2)); - var [code, _ ] = parse_text(code, ":"); - var [code, inp] = parse_term(code); - var [code, _ ] = parse_text(code, ")"); - var [code, bod] = parse_term(code); - return [code, ctx => All(nam, inp(ctx), x => bod(Cons([nam, x], ctx)))]; - } - // LAM: `λx f` - if (code[0] === "λ") { - var [code, nam] = parse_name(code.slice(1)); - var [code, bod] = parse_term(code); - return [code, ctx => Lam(nam, x => bod(Cons([nam, x], ctx)))]; - } - // APP: `(f x y z ...)` - if (code[0] === "(") { - var [code, fun] = parse_term(code.slice(1)); - var args: ((ctx: Scope) => Term)[] = []; - while (code[0] !== ")") { - var [code, arg] = parse_term(code); - args.push(arg); - code = skip(code); - } - var [code, _] = parse_text(code, ")"); - return [code, ctx => args.reduce((f, x) => App(f, x(ctx)), fun(ctx))]; - } - // ANN: `{x : T}` - if (code[0] === "{") { - var [code, val] = parse_term(code.slice(1)); - var [code, _ ] = parse_text(code, ":"); - var [code, typ] = parse_term(code); - var [code, _ ] = parse_text(code, "}"); - return [code, ctx => Ann(val(ctx), typ(ctx))]; - } - // SLF: `$x T` - if (code[0] === "$") { - var [code, nam] = parse_name(code.slice(1)); - var [code, bod] = parse_term(code); - return [code, ctx => Slf(nam, x => bod(Cons([nam, x], ctx)))]; - } - // INS: `~x` - if (code[0] === "~") { - var [code, val] = parse_term(code.slice(1)); - return [code, ctx => Ins(val(ctx))]; - } - // SET: `*` - if (code[0] === "*") { - return [code.slice(1), ctx => Set()]; - } - // LET: `let x = A in B` - if (code.slice(0,4) === "let ") { - var [code, nam] = parse_name(code.slice(4)); - var [code, _ ] = parse_text(code, "="); - var [code, val] = parse_term(code); - var [code, bod] = parse_term(code); - return [code, ctx => Let(nam, val(ctx), x => bod(Cons([nam, x], ctx)))]; - } - // U60: `#U60` - if (code.slice(0,4) === "#U60") { - return [code.slice(4), ctx => U60()]; - } - // OP2: `#( fst snd)` - if (code.slice(0,2) === "#(") { - var [code, opr] = parse_oper(code.slice(2)); - var [code, fst] = parse_term(code); - var [code, snd] = parse_term(code); - var [code, _] = parse_text(code, ")"); - return [code, ctx => Op2(opr, fst(ctx), snd(ctx))]; - } - // MAT: `#match x = val { #0: z; #+: s }: p` - if (code.slice(0,7) === "#match ") { - var [code, nam] = parse_name(code.slice(7)); - var [code, _ ] = parse_text(code, "="); - var [code, x] = parse_term(code); - var [code, _ ] = parse_text(code, "{"); - var [code, _ ] = parse_text(code, "#0:"); - var [code, z] = parse_term(code); - var [code, _ ] = parse_text(code, "#+:"); - var [code, s] = parse_term(code); - var [code, _ ] = parse_text(code, "}"); - var [code, _ ] = parse_text(code, ":"); - var [code, p] = parse_term(code); - return [code, ctx => Mat(nam, x(ctx), z(ctx), k => s(Cons([nam+"-1", k], ctx)), k => p(Cons([nam, k], ctx)))]; - } - // NUM: `#num` - if (code[0] === "#") { - var [code, num] = parse_name(code.slice(1)); - return [code, ctx => Num(BigInt(num))]; - } - // CHR: `'a'` -- char syntax sugar - if (code[0] === "'") { - var [code, chr] = [code.slice(2), code[1]]; - var [code, _] = parse_text(code, "'"); - return [code, ctx => Num(BigInt(chr.charCodeAt(0)))]; - } - // STR: `"text"` -- string syntax sugar - if (code[0] === "\"" || code[0] === "`") { - var str = ""; - var end = code[0]; - code = code.slice(1); - while (code[0] !== end) { - str += code[0]; - code = code.slice(1); - } - code = code.slice(1); - return [code, ctx => Txt(str)]; - } - // HOL: `?name` - if (code[0] === "?") { - var [code, nam] = parse_name(code.slice(1)); - return [code, ctx => Hol(nam)]; - } - // VAR: `name` - var [code, nam] = parse_name(code); - if (nam.length > 0) { - return [code, ctx => find(ctx, nam)]; - } - throw "parse error"; -} - -export function do_parse_term(code: string): Term { - return parse_term(code)[1](Nil()); -} - -export function parse_def(code: string): [string, {nam: string, val: Term}] { - var [code, nam] = parse_name(skip(code)); - if (skip(code)[0] === ":") { - var [code, _ ] = parse_text(code, ":"); - var [code, typ] = parse_term(code); - var [code, _ ] = parse_text(code, "="); - var [code, val] = parse_term(code); - return [code, {nam: nam, val: Ann(val(Nil()), typ(Nil()))}]; - } else { - var [code, _ ] = parse_text(code, "="); - var [code, val] = parse_term(code); - return [code, {nam: nam, val: val(Nil())}]; - } -} - -export function parse_book(code: string): Book { - var book : Book = {}; - while (code.length > 0) { - var [code, def] = parse_def(code); - book[def.nam] = def.val; - code = skip(code); - } - return book; -} - -export function do_parse_book(code: string): Book { - return parse_book(code); -} - -// CLI -// --- - -import * as fs from "fs"; -import { execSync } from "child_process"; - -export function main() { - // Loads Kind's HVM checker. - var kind2_hvm1 = fs.readFileSync(__dirname + "/kind2.hvm1", "utf8"); - - // Loads all local ".kind2" files. - const code = fs.readdirSync(".") - .filter(file => file.endsWith(".kind2")) - .map(file => fs.readFileSync("./"+file, "utf8")) - .join("\n"); - - // Parses into book. - const book = do_parse_book(code); - - // Compiles book to hvm1. - //var book_hvm1 = "Names = [" + Object.keys(book).map(x => '"'+x+'"').join(",") + "]\n"; - //var ref_count = 0; - var used_refs = {}; - var book_hvm1 = ""; - for (let name in book) { - book_hvm1 += "Book." + name + " = (Ref \"" + name + "\" " + compile(book[name], used_refs) + ")\n"; - } - - // Checks for unbound definitions - for (var ref_name in used_refs) { - if (!book[ref_name]) { - throw "Unbound definition: " + ref_name; - } - } - - // Gets arguments. - const args = process.argv.slice(2); - const func = args[0]; - const name = args[1]; - - // Creates main. - var main_hvm1 = ""; - switch (func) { - case "check": { - main_hvm1 = "Main = (Checker Book." + name + ")\n"; - break; - } - case "run": { - main_hvm1 = "Main = (Normalizer Book." + name + ")\n"; - break; - } - default: { - console.log("Usage: kind2 [check|run] "); - } - } - - // Generates the 'kind2.hvm1' file. - var checker_hvm1 = [kind2_hvm1, book_hvm1, main_hvm1].join("\n\n"); - - // Saves locally. - fs.writeFileSync("./.kind2.hvm1", checker_hvm1); - - // Runs 'hvm1 kind2.hvm1 -s -L -1' - - //const output = execSync("hvm1 run .kind2.hvm1 -s -L -1").toString(); - - //for (let name in book) { - //console.log("Checking: " + name); - - const output = execSync("hvm1 run -t 1 -c -f .kind2.hvm1 \"(Main)\"").toString(); - //const output = execSync(`hvm1 run -t 1 -c -f .kind2.hvm1 "(Checker Book.${name})"`).toString(); - try { - var check_text = output.slice(output.indexOf("[["), output.indexOf("RWTS")).trim(); - var stats_text = output.slice(output.indexOf("RWTS")); - var [logs, check] = JSON.parse(check_text); - logs.reverse(); - for (var log of logs) { - console.log(log); - } - console.log(check ? "Check!" : "Error."); - console.log(""); - console.log(stats_text); - } catch (e) { - console.log(output); - } - - //} - -}; - -main(); diff --git a/package.json b/package.json deleted file mode 100644 index 141ac955f..000000000 --- a/package.json +++ /dev/null @@ -1,22 +0,0 @@ -{ - "name": "kind2", - "version": "0.1.0", - "description": "", - "main": "kind2.ts", - "bin": { - "kind2": "./kind2.ts" - }, - "scripts": { - "test": "echo \"Error: no test specified\" && exit 1" - }, - "repository": { - "type": "git", - "url": "git+https://github.com/victortaelin/kind2.git" - }, - "author": "VictorTaelin", - "license": "MIT", - "bugs": { - "url": "https://github.com/victortaelin/kind2/issues" - }, - "homepage": "https://github.com/victortaelin/kind2#readme" -} diff --git a/src/book/compile.rs b/src/book/compile.rs index b7447e951..d112942bd 100644 --- a/src/book/compile.rs +++ b/src/book/compile.rs @@ -40,7 +40,7 @@ impl Book { pub fn to_hvm2(&self) -> String { let mut code = String::new(); for (name, term) in &self.defs { - code.push_str(&format!("{} = {}\n", name, term.to_hvm2())); + code.push_str(&format!("{} = {}\n", Term::to_hvm2_name(name), term.to_hvm2())); } code } diff --git a/src/book/mod.rs b/src/book/mod.rs index fcc929c36..7cc948ff5 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -49,6 +49,7 @@ impl Book { book.load(base, "Nat")?; book.load(base, "Nat.succ")?; book.load(base, "Nat.zero")?; + book.expand_implicits(); return Ok(book); } @@ -83,6 +84,19 @@ impl Book { return Ok(()); } + // Desugars all definitions + pub fn expand_implicits(&mut self) { + // Creates a map with the implicit count of each top-level definition + let mut implicit_count = BTreeMap::new(); + for (name, term) in self.defs.iter() { + implicit_count.insert(name.clone(), term.count_implicits()); + } + // Expands implicit calls of each top-level definition in the book + for def in self.defs.iter_mut() { + def.1.expand_implicits(im::Vector::new(), &implicit_count); + } + } + // Gets a file id from its name pub fn get_file_id(&mut self, name: &str) -> u64 { if let Some(id) = self.fids.get(name) { diff --git a/src/book/parse.rs b/src/book/parse.rs index d9bfb2084..cc279ae3a 100644 --- a/src/book/parse.rs +++ b/src/book/parse.rs @@ -49,12 +49,12 @@ impl<'i> KindParser<'i> { let mut typ = Term::Set; let mut val = Term::new_adt(&adt); for (idx_nam, idx_typ) in adt.idxs.iter().rev() { - typ = Term::All { nam: idx_nam.clone(), inp: Box::new(idx_typ.clone()), bod: Box::new(typ) }; - val = Term::Lam { nam: idx_nam.clone(), bod: Box::new(val) }; + typ = Term::All { era: false, nam: idx_nam.clone(), inp: Box::new(idx_typ.clone()), bod: Box::new(typ) }; + val = Term::Lam { era: false, nam: idx_nam.clone(), bod: Box::new(val) }; } for par_nam in adt.pars.iter().rev() { - typ = Term::All { nam: par_nam.clone(), inp: Box::new(Term::Set), bod: Box::new(typ) }; - val = Term::Lam { nam: par_nam.clone(), bod: Box::new(val) }; + typ = Term::All { era: false, nam: par_nam.clone(), inp: Box::new(Term::Set), bod: Box::new(typ) }; + val = Term::Lam { era: false, nam: par_nam.clone(), bod: Box::new(val) }; } //println!("NAM: {}", adt.name); //println!("TYP: {}", typ.show()); @@ -68,22 +68,23 @@ impl<'i> KindParser<'i> { let nam = uses.get(&nam).unwrap_or(&nam).to_string(); self.skip_trivia(); - // Untyped Arguments (optional) + // Arguments (optional) let mut args = im::Vector::new(); - while self.peek_one().map_or(false, |c| c.is_ascii_alphabetic()) { - let par = self.parse_name()?; - self.skip_trivia(); - args.push_back((par, Term::Met{})); - } - - // Typed Arguments (optional) - while self.peek_one() == Some('(') { - self.consume("(")?; + let mut uses = uses.clone(); + while self.peek_one() == Some('<') || self.peek_one() == Some('(') { + let implicit = self.peek_one() == Some('<'); + self.consume(if implicit { "<" } else { "(" })?; let arg_name = self.parse_name()?; - self.consume(":")?; - let arg_type = self.parse_term(fid, uses)?; - self.consume(")")?; - args.push_back((arg_name, arg_type)); + self.skip_trivia(); + let arg_type = if self.peek_one() == Some(':') { + self.consume(":")?; + self.parse_term(fid, &uses)? + } else { + Term::Met {} + }; + self.consume(if implicit { ">" } else { ")" })?; + uses = shadow(&arg_name, &uses); + args.push_back((implicit, arg_name, arg_type)); self.skip_trivia(); } @@ -92,7 +93,7 @@ impl<'i> KindParser<'i> { let ann; if self.peek_one() == Some(':') { self.consume(":")?; - typ = self.parse_term(fid, uses)?; + typ = self.parse_term(fid, &uses)?; ann = true; } else { typ = Term::Met {}; @@ -101,7 +102,9 @@ impl<'i> KindParser<'i> { // Value (mandatory) self.consume("=")?; - let mut val = self.parse_term(fid, uses)?; + let mut val = self.parse_term(fid, &uses)?; + + //println!("PARSING {}", nam); // Adds lambdas/foralls for each argument typ.add_alls(args.clone()); @@ -140,15 +143,16 @@ impl<'i> KindParser<'i> { impl Term { // Wraps a Lam around this term. - fn add_lam(&mut self, arg: &str) { + fn add_lam(&mut self, era: bool, arg: &str) { *self = Term::Lam { + era: era, nam: arg.to_string(), bod: Box::new(std::mem::replace(self, Term::Met {})), }; } // Wraps many lams around this term. Linearizes when possible. - fn add_lams(&mut self, args: im::Vector<(String,Term)>) { + fn add_lams(&mut self, args: im::Vector<(bool,String,Term)>) { // Passes through Src if let Term::Src { val, .. } = self { val.add_lams(args); @@ -161,35 +165,44 @@ impl Term { } // Linearizes a numeric pattern match if let Term::Swi { nam, z, s, .. } = self { - if args.len() >= 1 && args[0].0 == *nam { + if args.len() >= 1 && args[0].1 == *nam { let (head, tail) = args.split_at(1); z.add_lams(tail.clone()); s.add_lams(tail.clone()); - self.add_lam(&head[0].0); + self.add_lam(head[0].0, &head[0].1); return; } } // Linearizes a user-defined ADT match if let Term::Mch { mch } = self { - let Match { name, cses, .. } = &mut **mch; - if args.len() >= 1 && args[0].0 == *name { - let (head, tail) = args.split_at(1); - for (_, cse) in cses { - cse.add_lams(tail.clone()); + if !mch.fold { + let Match { name, cses, .. } = &mut **mch; + if args.len() >= 1 && args[0].1 == *name { + let (head, tail) = args.split_at(1); + for (_, cse) in cses { + cse.add_lams(tail.clone()); + } + self.add_lam(head[0].0, &head[0].1); + return; } - self.add_lam(&head[0].0); - return; } } // Prepend remaining lambdas - for (nam, _) in args.iter().rev() { - self.add_lam(&nam); + if args.len() > 0 { + let (head, tail) = args.split_at(1); + self.add_lam(head[0].0, &head[0].1); + if let Term::Lam { era: _, nam: _, bod } = self { + bod.add_lams(tail.clone()); + } else { + unreachable!(); + } } } // Wraps an All around this term. - fn add_all(&mut self, arg: &str, typ: &Term) { + fn add_all(&mut self, era: bool, arg: &str, typ: &Term) { *self = Term::All { + era: era, nam: arg.to_string(), inp: Box::new(typ.clone()), bod: Box::new(std::mem::replace(self, Term::Met {})), @@ -197,9 +210,9 @@ impl Term { } // Wraps many Lams around this term. - fn add_alls(&mut self, args: im::Vector<(String,Term)>) { - for (nam, typ) in args.iter().rev() { - self.add_all(&nam, typ); + fn add_alls(&mut self, args: im::Vector<(bool,String,Term)>) { + for (era, nam, typ) in args.iter().rev() { + self.add_all(*era, &nam, typ); } } diff --git a/src/main.rs b/src/main.rs index b3effcc5f..8595e9e5b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,3 +1,20 @@ +// PROJECT FILES: +//./term/mod.rs// +//./term/show.rs// +//./term/parse.rs// +//./term/compile.rs// +//./sugar/mod.rs// +//./show/mod.rs// +//./info/mod.rs// +//./info/parse.rs// +//./info/show.rs// +//./book/mod.rs// +//./book/compile.rs// +//./book/parse.rs// +//./book/show.rs// + +// PROJECT CLI (main.rs): + use clap::{Arg, ArgAction, Command}; use std::fs; use std::io::Write; @@ -49,7 +66,7 @@ fn generate_check_hs(book: &Book, command: &str, arg: &str) -> String { fn generate_hvm2(book: &Book, arg: &str) -> String { let book_hvm2 = book.to_hvm2(); - let main_hvm2 = format!("main = {}\n", arg); + let main_hvm2 = format!("main = {}\n", Term::to_hvm2_name(arg)); format!("{}\n{}", book_hvm2, main_hvm2) } @@ -102,13 +119,15 @@ fn normal(name: &str, _level: u32, runtime: &str) { eprintln!("{stderr}"); } -fn format_def(name: &str) { - let book = load_book(name); - let defn = book.defs.get(name).expect("definition exists"); - let form = book.format_def(name, defn).flatten(Some(40)); - - let path = PathBuf::from(format!("./{name}.kind2")); - fs::write(&path, form).expect(&format!("failed to write to '{:?}'", path)); +fn auto_format(file_name: &str) { + let base = std::env::current_dir().expect("failed to get current directory"); + let file = base.join(format!("{file_name}.kind2")); + let text = std::fs::read_to_string(&file).expect("failed to read file"); + let fid = Book::new().get_file_id(&file.to_str().unwrap().to_string()); + let book = KindParser::new(&text).parse_book(file_name, fid).expect("failed to parse book"); + let form = book.defs.iter().map(|(name, term)| book.format_def(name, term)).collect(); + let form = Show::pile("\n\n", form).flatten(Some(60)); + std::fs::write(&file, form).expect(&format!("failed to write to file '{}'", file_name)); } fn compile(name: &str) { @@ -185,7 +204,7 @@ fn main() { .value_parser(["hs", "hvm2"]) .default_value("hs"))) .subcommand(Command::new("format") - .about("Pretty-formats a definition") + .about("Auto-formats a file") .arg(Arg::new("name").required(true))) .subcommand(Command::new("compile") .about("Compiles to HVM2") @@ -207,7 +226,7 @@ fn main() { } Some(("format", sub_matches)) => { let name = sub_matches.get_one::("name").expect("required"); - format_def(name); + auto_format(name); } Some(("compile", sub_matches)) => { let name = sub_matches.get_one::("name").expect("required"); diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs index 9463797b6..8a1a48820 100644 --- a/src/sugar/mod.rs +++ b/src/sugar/mod.rs @@ -34,6 +34,7 @@ pub struct Constructor { #[derive(Debug, Clone)] pub struct Match { pub adt: String, // datatype + pub fold: bool, // is this a fold? pub name: String, // scrutinee name pub expr: Term, // structinee expression pub with: Vec<(String,Term)>, // terms to move in @@ -199,7 +200,7 @@ impl Term { let mut term = self; loop { match term { - Term::App { fun, arg } => { + Term::App { era: _, fun, arg } => { if let Term::Var { nam } = &**fun { if nam == "Nat.succ" { nat += 1; @@ -241,9 +242,9 @@ impl Term { let mut term = self; loop { match term { - Term::App { fun, arg } => { - if let Term::App { fun: cons, arg: head } = &**fun { - if let Term::App { fun: cons_fun, arg: _ } = &**cons { + Term::App { era: _, fun, arg } => { + if let Term::App { era: _, fun: cons, arg: head } = &**fun { + if let Term::App { era: _, fun: cons_fun, arg: _ } = &**cons { if let Term::Var { nam } = &**cons_fun { if nam == "List.cons" { vals.push(head.clone()); @@ -268,13 +269,17 @@ impl Term { // Builds a chain of applications of List.cons and List.nil from a Vec> pub fn new_list(list: &List) -> Term { let mut term = Term::App { + era: true, fun: Box::new(Term::Var { nam: "List.nil".to_string() }), arg: Box::new(Term::Met {}), }; for item in (&list.vals).into_iter().rev() { term = Term::App { + era: false, fun: Box::new(Term::App { + era: false, fun: Box::new(Term::App { + era: true, fun: Box::new(Term::Var { nam: "List.cons".to_string() }), arg: Box::new(Term::Met {}), }), @@ -333,9 +338,9 @@ impl Term { // - (EQUAL a b) ::= (App (App (App (Var "Equal") _) a) b) pub fn as_equal(&self) -> Option { match self { - Term::App { fun, arg: rhs } => { - if let Term::App { fun: eq_fun, arg: lhs } = &**fun { - if let Term::App { fun: eq_fun, arg: _ } = &**eq_fun { + Term::App { era: _, fun, arg: rhs } => { + if let Term::App { era: _, fun: eq_fun, arg: lhs } = &**fun { + if let Term::App { era: _, fun: eq_fun, arg: _ } = &**eq_fun { if let Term::Var { nam } = &**eq_fun { if nam == "Equal" { return Some(Equal { a: (**lhs).clone(), b: (**rhs).clone() }); @@ -352,8 +357,11 @@ impl Term { // Builds an equal chain pub fn new_equal(eq: &Equal) -> Term { Term::App { + era: false, fun: Box::new(Term::App { + era: false, fun: Box::new(Term::App { + era: true, fun: Box::new(Term::Var { nam: "Equal".to_string() }), arg: Box::new(Term::Met {}), }), @@ -419,7 +427,7 @@ impl Term { } // Reads the motive: `∀(P: ∀(I0: I0.TY) ∀(I1: I1.TY) ... ∀(x: (TY P0 P1 ... I0 I1 ...)) *).` - if let Term::All { nam, inp, bod } = term { + if let Term::All { era: _, nam, inp, bod } = term { // Gets the motive name pvar = nam.clone(); @@ -427,7 +435,7 @@ impl Term { let mut moti = &**inp; // Reads each motive index - while let Term::All { nam, inp: idx_inp, bod: idx_bod } = moti { + while let Term::All { era: _, nam, inp: idx_inp, bod: idx_bod } = moti { if let Term::All { .. } = &**idx_bod { idxs.push((nam.clone(), *idx_inp.clone())); moti = idx_bod; @@ -437,14 +445,14 @@ impl Term { } // Skips the witness - if let Term::All { nam: _, inp: wit_inp, bod: wit_bod } = moti { + if let Term::All { era: _, nam: _, inp: wit_inp, bod: wit_bod } = moti { // Here, the witness has form '(TY P0 P1 ... I0 I1 ...)' let mut wit_inp = wit_inp; // Skips the wit's indices (outermost Apps) for _ in 0 .. idxs.len() { - if let Term::App { fun: wit_inp_fun, arg: _ } = &**wit_inp { + if let Term::App { era: _, fun: wit_inp_fun, arg: _ } = &**wit_inp { wit_inp = wit_inp_fun; } else { return None; @@ -452,7 +460,7 @@ impl Term { } // Collects the wit's parameters (remaining Apps) - while let Term::App { fun: wit_inp_fun, arg: wit_inp_arg } = &**wit_inp { + while let Term::App { era: _, fun: wit_inp_fun, arg: wit_inp_arg } = &**wit_inp { if let Term::Var { nam: parameter } = &**wit_inp_arg { pars.push(parameter.to_string()); wit_inp = wit_inp_fun; @@ -485,12 +493,12 @@ impl Term { } // Reads each constructor: `∀(C0: ∀(C0_F0: C0_F0.TY) ∀(C0_F1: C0_F1.TY) ... (P I0 I1 ... (TY.C0 P0 P1 ... C0_F0 C0_F1 ...)))` - while let Term::All { nam, inp, bod } = term { + while let Term::All { era: _, nam, inp, bod } = term { let mut flds: Vec<(String,Term)> = Vec::new(); let mut ctyp: &Term = &**inp; // Reads each field - while let Term::All { nam, inp, bod } = ctyp { + while let Term::All { era: _, nam, inp, bod } = ctyp { flds.push((nam.clone(), *inp.clone())); ctyp = bod; } @@ -498,7 +506,7 @@ impl Term { // Now, the ctyp will be in the form (P I0 I1 ... (Ctr P0 P1 ... F0 F1 ...)) // Skips the outermost application - if let Term::App { fun: ctyp_fun, arg: _ } = ctyp { + if let Term::App { era: _, fun: ctyp_fun, arg: _ } = ctyp { ctyp = ctyp_fun; } else { return None; @@ -506,7 +514,7 @@ impl Term { // Collects constructor indices until we reach the pattern head P let mut ctr_idxs: Vec = Vec::new(); - while let Term::App { fun: fun_app, arg: arg_app } = ctyp { + while let Term::App { era: _, fun: fun_app, arg: arg_app } = ctyp { ctr_idxs.push(*arg_app.clone()); ctyp = fun_app; } @@ -538,18 +546,19 @@ impl Term { // Then appends each type parameter for par in adt.pars.iter() { - self_type = Term::App { fun: Box::new(self_type), arg: Box::new(Term::Var { nam: par.clone() }) }; + self_type = Term::App { era: false, fun: Box::new(self_type), arg: Box::new(Term::Var { nam: par.clone() }) }; } // And finally appends each index for (idx_name, _) in adt.idxs.iter() { - self_type = Term::App { fun: Box::new(self_type), arg: Box::new(Term::Var { nam: idx_name.clone() }) }; + self_type = Term::App { era: false, fun: Box::new(self_type), arg: Box::new(Term::Var { nam: idx_name.clone() }) }; } // 2. Builds the motive type: ∀(I0: I0.TY) ∀(I1: I1.TY) ... ∀(x: (Type P0 P1 ... I0 I1 ...)) * // Starts with the witness type: ∀(x: (Type P0 P1 ... I0 I1 ...)) * let mut motive_type = Term::All { + era: false, nam: "x".to_string(), inp: Box::new(self_type.clone()), bod: Box::new(Term::Set), @@ -558,6 +567,7 @@ impl Term { // Then prepends each index type for (idx_name, idx_type) in adt.idxs.iter().rev() { motive_type = Term::All { + era: false, nam: idx_name.clone(), inp: Box::new(idx_type.clone()), bod: Box::new(motive_type), @@ -570,6 +580,7 @@ impl Term { // Applies the motive to each index for (idx_name, _) in adt.idxs.iter() { term = Term::App { + era: false, fun: Box::new(term), arg: Box::new(Term::Var { nam: idx_name.clone() }), }; @@ -577,6 +588,7 @@ impl Term { // And applies it to the witness (self) term = Term::App { + era: false, fun: Box::new(term), arg: Box::new(Term::Var { nam: "self".to_string() }), }; @@ -589,6 +601,7 @@ impl Term { // Applies the motive to each constructor index for idx in ctr.idxs.iter().rev() { ctr_term = Term::App { + era: false, fun: Box::new(ctr_term), arg: Box::new(idx.clone()), }; @@ -598,16 +611,19 @@ impl Term { let mut ctr_type = Term::Var { nam: format!("{}.{}", adt.name, ctr.name) }; // For each type parameter - for par in adt.pars.iter() { - ctr_type = Term::App { - fun: Box::new(ctr_type), - arg: Box::new(Term::Var { nam: par.clone() }), - }; - } + // NOTE: Not necessary anymore due to auto implicit arguments + //for par in adt.pars.iter() { + //ctr_type = Term::App { + //era: true, + //fun: Box::new(ctr_type), + //arg: Box::new(Term::Var { nam: par.clone() }), + //}; + //} // And for each field for (fld_name, _fld_type) in ctr.flds.iter() { ctr_type = Term::App { + era: false, fun: Box::new(ctr_type), arg: Box::new(Term::Var { nam: fld_name.clone() }), }; @@ -615,6 +631,7 @@ impl Term { // Wraps the constructor type with the application ctr_term = Term::App { + era: false, fun: Box::new(ctr_term), arg: Box::new(ctr_type), }; @@ -622,6 +639,7 @@ impl Term { // Finally, quantifies each field for (fld_name, fld_type) in ctr.flds.iter().rev() { ctr_term = Term::All { + era: false, nam: fld_name.clone(), inp: Box::new(fld_type.clone()), bod: Box::new(ctr_term), @@ -630,6 +648,7 @@ impl Term { // And quantifies the constructor term = Term::All { + era: false, nam: ctr.name.clone(), inp: Box::new(ctr_term), bod: Box::new(term), @@ -638,6 +657,7 @@ impl Term { // 5 Quantifies the motive term = Term::All { + era: false, nam: "P".to_string(), inp: Box::new(motive_type), bod: Box::new(term), @@ -680,11 +700,8 @@ impl ADT { Err(format!("Cannot find definition for type '{}'.", name)) } } - -} - -impl ADT { + // Formats an ADT pub fn format(&self) -> Box { // ADT head: `data Name ` @@ -856,12 +873,14 @@ impl Term { if let Some(moti) = &mat.moti { // Creates the first lambda: 'λx ' motive = Term::Lam { + era: false, nam: mat.name.clone(), bod: Box::new(moti.clone()), }; // Creates a lambda for each index: 'λindices ... λx ' for (idx_name, _) in adt.idxs.iter().rev() { motive = Term::Lam { + era: false, nam: idx_name.clone(), bod: Box::new(motive), }; @@ -869,6 +888,7 @@ impl Term { // Creates a forall for each moved value: 'λindices ... λx ∀(a: A) ... ' for (nam, typ) in mat.with.iter().rev() { motive = Term::All { + era: false, nam: nam.clone(), inp: Box::new(typ.clone()), bod: Box::new(motive), @@ -892,6 +912,7 @@ impl Term { // Adds moved value lambdas for (nam, _) in mat.with.iter().rev() { ctr_term = Term::Lam { + era: false, nam: nam.clone(), bod: Box::new(ctr_term), }; @@ -899,6 +920,7 @@ impl Term { // Adds field lambdas for (fld_name, _) in ctr.flds.iter().rev() { ctr_term = Term::Lam { + era: false, nam: format!("{}.{}", mat.name, fld_name.clone()), bod: Box::new(ctr_term), }; @@ -911,13 +933,26 @@ impl Term { } } - // 3. Wrap Ins around term - term = Term::Ins { - val: Box::new(mat.expr.clone()) - }; + // 3. Wrap Ins or Type.fold around term + if mat.fold { + term = Term::App { + era: false, + fun: Box::new(Term::App { + era: true, + fun: Box::new(Term::Var { nam: format!("{}.fold", adt.name) }), + arg: Box::new(Term::Met {}), + }), + arg: Box::new(mat.expr.clone()), + }; + } else { + term = Term::Ins { + val: Box::new(mat.expr.clone()) + }; + } // 4. Apply the motive, making a Var for it term = Term::App { + era: true, fun: Box::new(term), arg: Box::new(Term::Var { nam: format!("{}.P", mat.name) }), }; @@ -925,6 +960,7 @@ impl Term { // 5. Apply each constructor (by name) for ctr in &adt.ctrs { term = Term::App { + era: false, fun: Box::new(term), arg: Box::new(Term::Var { nam: format!("{}.{}", mat.name, ctr.name) }), }; @@ -935,6 +971,7 @@ impl Term { let mut ann_type = Term::Met {}; for (nam, typ) in mat.with.iter().rev() { ann_type = Term::All { + era: false, nam: nam.clone(), inp: Box::new(typ.clone()), bod: Box::new(ann_type), @@ -950,6 +987,7 @@ impl Term { // 7. Applies each moved var for (nam, _) in mat.with.iter() { term = Term::App { + era: false, fun: Box::new(term), arg: Box::new(Term::Var { nam: nam.clone() }), }; @@ -971,8 +1009,6 @@ impl Term { bod: Box::new(term) }; - //println!("PARSED:\n{}", term.show()); - // 10. Return 'term' return term; } @@ -984,7 +1020,7 @@ impl Match { pub fn format(&self) -> Box { Show::pile(" ", vec![ Show::glue(" ", vec![ - Show::text("match"), + Show::text(if self.fold { "fold" } else { "match" }), Show::text(&self.name), Show::text("="), self.expr.format_go(), @@ -1015,9 +1051,9 @@ impl Match { impl<'i> KindParser<'i> { // MAT ::= match = { : <...> }: - pub fn parse_match(&mut self, fid: u64, uses: &Uses) -> Result { + pub fn parse_match(&mut self, fid: u64, uses: &Uses, fold: bool) -> Result { // Parses the header: 'match = ' - self.consume("match ")?; + self.consume(if fold { "fold " } else { "match " })?; let name = self.parse_name()?; self.skip_trivia(); let expr = if self.peek_one() == Some('=') { @@ -1090,7 +1126,7 @@ impl<'i> KindParser<'i> { } else { None }; - return Ok(Match { adt, name, expr, with, cses, moti }); + return Ok(Match { adt, fold, name, expr, with, cses, moti }); } } diff --git a/src/term/compile.rs b/src/term/compile.rs index 4aa5478f9..a2ce4d820 100644 --- a/src/term/compile.rs +++ b/src/term/compile.rs @@ -69,16 +69,16 @@ impl Term { format!("x{}", name.replace("-", "._.")) } match self { - Term::All { nam, inp, bod } => { + Term::All { era: _, nam, inp, bod } => { let inp = inp.to_hvm2_checker(env.clone(), met); let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met); format!("(All \"{}\" {} λ{} {})", nam, inp, binder(nam), bod) } - Term::Lam { nam, bod } => { + Term::Lam { era: _, nam, bod } => { let bod = bod.to_hvm2_checker(cons(&env, nam.clone()), met); format!("(Lam \"{}\" λ{} {})", nam, binder(nam), bod) } - Term::App { fun, arg } => { + Term::App { era: _, fun, arg } => { let fun = fun.to_hvm2_checker(env.clone(), met); let arg = arg.to_hvm2_checker(env.clone(), met); format!("(App {} {})", fun, arg) @@ -162,16 +162,16 @@ impl Term { pub fn to_hs_checker(&self, env: im::Vector, met: &mut usize) -> String { match self { - Term::All { nam, inp, bod } => { + Term::All { era: _, nam, inp, bod } => { let inp = inp.to_hs_checker(env.clone(), met); let bod = bod.to_hs_checker(cons(&env, nam.clone()), met); format!("(All \"{}\" {} $ \\{} -> {})", nam, inp, Term::to_hs_name(nam), bod) }, - Term::Lam { nam, bod } => { + Term::Lam { era: _, nam, bod } => { let bod = bod.to_hs_checker(cons(&env, nam.clone()), met); format!("(Lam \"{}\" $ \\{} -> {})", nam, Term::to_hs_name(nam), bod) }, - Term::App { fun, arg } => { + Term::App { era: _, fun, arg } => { let fun = fun.to_hs_checker(env.clone(), met); let arg = arg.to_hs_checker(env.clone(), met); format!("(App {} {})", fun, arg) @@ -252,17 +252,26 @@ impl Term { pub fn to_hvm2(&self) -> String { match self { - Term::All { nam: _, inp: _, bod: _ } => { + Term::All { era: _, nam: _, inp: _, bod: _ } => { format!("0") }, - Term::Lam { nam, bod } => { + Term::Lam { era, nam, bod } => { let bod = bod.to_hvm2(); - format!("λ{} {}", nam, bod) + if *era { + format!("{}", bod) + } else { + format!("λ{} {}", Term::to_hvm2_name(nam), bod) + } }, - Term::App { fun, arg } => { - let fun = fun.to_hvm2(); - let arg = arg.to_hvm2(); - format!("(App {} {})", fun, arg) + Term::App { era, fun, arg } => { + if *era { + let fun = fun.to_hvm2(); + format!("{}", fun) + } else { + let fun = fun.to_hvm2(); + let arg = arg.to_hvm2(); + format!("({} {})", fun, arg) + } }, Term::Ann { chk: _, val, typ: _ } => { val.to_hvm2() @@ -291,18 +300,18 @@ impl Term { let x = x.to_hvm2(); let z = z.to_hvm2(); let s = s.to_hvm2(); - format!("switch {} = {} {{ 0: {} _: {} }}", nam, x, z, s) + format!("match {} = {} {{ 0: {} +: {} }}", Term::to_hvm2_name(nam), x, z, s) }, Term::Let { nam, val, bod } => { let val = val.to_hvm2(); let bod = bod.to_hvm2(); - format!("let {} = {} {}", nam, val, bod) + format!("let {} = {} {}", Term::to_hvm2_name(nam), val, bod) }, // FIXME: change to "use" once hvm-lang supports it Term::Use { nam, val, bod } => { let val = val.to_hvm2(); let bod = bod.to_hvm2(); - format!("use {} = {} {}", nam, val, bod) + format!("let {} = {} {}", Term::to_hvm2_name(nam), val, bod) }, Term::Hol { nam: _ } => { format!("0") @@ -312,7 +321,7 @@ impl Term { format!("0") }, Term::Var { nam } => { - format!("{}", nam) + format!("{}", Term::to_hvm2_name(nam)) }, Term::Src { src: _, val } => { val.to_hvm2() @@ -329,4 +338,9 @@ impl Term { } } + pub fn to_hvm2_name(name: &str) -> String { + format!("_{}", name) + } + + } diff --git a/src/term/mod.rs b/src/term/mod.rs index 2d00fca0b..2bd3784b9 100644 --- a/src/term/mod.rs +++ b/src/term/mod.rs @@ -1,5 +1,10 @@ +//./../sugar/mod.rs// +//./parse.rs// +//./../book/parse.rs// + use crate::{*}; use std::collections::BTreeSet; +use std::collections::BTreeMap; pub mod compile; pub mod parse; @@ -40,9 +45,9 @@ pub struct Src { // VAR | #[derive(Clone, Debug)] pub enum Term { - All { nam: String, inp: Box, bod: Box }, - Lam { nam: String, bod: Box }, - App { fun: Box, arg: Box }, + All { era: bool, nam: String, inp: Box, bod: Box }, + Lam { era: bool, nam: String, bod: Box }, + App { era: bool, fun: Box, arg: Box }, Ann { chk: bool, val: Box, typ: Box }, Slf { nam: String, typ: Box, bod: Box }, Ins { val: Box }, @@ -102,14 +107,14 @@ impl Term { pub fn get_free_vars(&self, env: im::Vector, free_vars: &mut BTreeSet) { match self { - Term::All { nam, inp, bod } => { + Term::All { era: _, nam, inp, bod } => { inp.get_free_vars(env.clone(), free_vars); bod.get_free_vars(cons(&env, nam.clone()), free_vars); }, - Term::Lam { nam, bod } => { + Term::Lam { era: _, nam, bod } => { bod.get_free_vars(cons(&env, nam.clone()), free_vars); }, - Term::App { fun, arg } => { + Term::App { era: _, fun, arg } => { fun.get_free_vars(env.clone(), free_vars); arg.get_free_vars(env.clone(), free_vars); }, @@ -163,88 +168,27 @@ impl Term { } } - // Recurses through the term, desugaring Mch constructors - pub fn desugar(&mut self) { - match self { - // Desugars the Mch constructor using sugar::new_match - Term::Mch { mch } => { - *self = Term::new_match(&mch); - self.desugar(); - }, - // Recurses on subterms for all other constructors - Term::All { nam: _, inp, bod } => { - inp.desugar(); - bod.desugar(); - }, - Term::Lam { nam: _, bod } => { - bod.desugar(); - }, - Term::App { fun, arg } => { - fun.desugar(); - arg.desugar(); - }, - Term::Ann { chk: _, val, typ } => { - val.desugar(); - typ.desugar(); - }, - Term::Slf { nam: _, typ, bod } => { - typ.desugar(); - bod.desugar(); - }, - Term::Ins { val } => { - val.desugar(); - }, - Term::Op2 { opr: _, fst, snd } => { - fst.desugar(); - snd.desugar(); - }, - Term::Swi { nam: _, x, z, s, p } => { - x.desugar(); - z.desugar(); - s.desugar(); - p.desugar(); - }, - Term::Let { nam: _, val, bod } => { - val.desugar(); - bod.desugar(); - }, - Term::Use { nam: _, val, bod } => { - val.desugar(); - bod.desugar(); - }, - Term::Src { src: _, val } => { - val.desugar(); - }, - // Base cases, do nothing - Term::Set => {}, - Term::U60 => {}, - Term::Num { val: _ } => {}, - Term::Nat { nat: _ } => {}, - Term::Txt { txt: _ } => {}, - Term::Var { nam: _ } => {}, - Term::Hol { nam: _ } => {}, - Term::Met {} => {}, - } - } - // Removes Src's pub fn clean(&self) -> Term { match self { - Term::All { nam, inp, bod } => { + Term::All { era, nam, inp, bod } => { Term::All { + era: *era, nam: nam.clone(), inp: Box::new(inp.clean()), bod: Box::new(bod.clean()), } }, - Term::Lam { nam, bod } => { + Term::Lam { era, nam, bod } => { Term::Lam { + era: *era, nam: nam.clone(), bod: Box::new(bod.clean()), } }, - Term::App { fun, arg } => { + Term::App { era, fun, arg } => { Term::App { + era: *era, fun: Box::new(fun.clean()), arg: Box::new(arg.clean()), } @@ -330,5 +274,158 @@ impl Term { }, } } -} + // Expands syntax sugars like Mch to proper λ-encodings. + pub fn desugar(&mut self) { + match self { + // Desugars the Mch constructor using sugar::new_match + Term::Mch { mch } => { + *self = Term::new_match(&mch); + self.desugar(); + }, + // Recurses on subterms for all other constructors + Term::All { era: _, nam: _, inp, bod } => { + inp.desugar(); + bod.desugar(); + }, + Term::Lam { era: _, nam: _, bod } => { + bod.desugar(); + }, + Term::App { era: _, fun, arg } => { + fun.desugar(); + arg.desugar(); + }, + Term::Ann { chk: _, val, typ } => { + val.desugar(); + typ.desugar(); + }, + Term::Slf { nam: _, typ, bod } => { + typ.desugar(); + bod.desugar(); + }, + Term::Ins { val } => { + val.desugar(); + }, + Term::Op2 { opr: _, fst, snd } => { + fst.desugar(); + snd.desugar(); + }, + Term::Swi { nam: _, x, z, s, p } => { + x.desugar(); + z.desugar(); + s.desugar(); + p.desugar(); + }, + Term::Let { nam: _, val, bod } => { + val.desugar(); + bod.desugar(); + }, + Term::Use { nam: _, val, bod } => { + val.desugar(); + bod.desugar(); + }, + Term::Src { src: _, val } => { + val.desugar(); + }, + Term::Set => {}, + Term::U60 => {}, + Term::Num { .. } => {}, + Term::Nat { .. } => {}, + Term::Txt { .. } => {}, + Term::Var { .. } => {}, + Term::Hol { .. } => {}, + Term::Met {} => {}, + } + } + + // Expands implicit calls, applying them to the right number of metavars. + pub fn expand_implicits(&mut self, env: im::Vector, implicit_count: &BTreeMap) { + match self { + Term::All { era: _, nam, inp, bod } => { + inp.expand_implicits(env.clone(), implicit_count); + bod.expand_implicits(cons(&env, nam.clone()), implicit_count); + }, + Term::Lam { era: _, nam, bod } => { + bod.expand_implicits(cons(&env, nam.clone()), implicit_count); + }, + Term::App { era: _, fun, arg } => { + fun.expand_implicits(env.clone(), implicit_count); + arg.expand_implicits(env.clone(), implicit_count); + }, + Term::Ann { chk: _, val, typ } => { + val.expand_implicits(env.clone(), implicit_count); + typ.expand_implicits(env.clone(), implicit_count); + }, + Term::Slf { nam, typ, bod } => { + typ.expand_implicits(env.clone(), implicit_count); + bod.expand_implicits(cons(&env, nam.clone()), implicit_count); + }, + Term::Ins { val } => { + val.expand_implicits(env.clone(), implicit_count); + }, + Term::Set => {}, + Term::U60 => {}, + Term::Num { val: _ } => {}, + Term::Op2 { opr: _, fst, snd } => { + fst.expand_implicits(env.clone(), implicit_count); + snd.expand_implicits(env.clone(), implicit_count); + }, + Term::Swi { nam, x, z, s, p } => { + x.expand_implicits(env.clone(), implicit_count); + z.expand_implicits(env.clone(), implicit_count); + s.expand_implicits(cons(&env, format!("{}-1",nam)), implicit_count); + p.expand_implicits(cons(&env, nam.clone()), implicit_count); + }, + Term::Nat { nat: _ } => {}, + Term::Txt { txt: _ } => {}, + Term::Let { nam, val, bod } => { + val.expand_implicits(env.clone(), implicit_count); + bod.expand_implicits(cons(&env, nam.clone()), implicit_count); + }, + Term::Use { nam, val, bod } => { + val.expand_implicits(env.clone(), implicit_count); + bod.expand_implicits(cons(&env, nam.clone()), implicit_count); + }, + Term::Hol { nam: _ } => {}, + Term::Met {} => {}, + Term::Src { src: _, val } => { + val.expand_implicits(env, implicit_count); + }, + Term::Var { nam } => { + if !env.contains(nam) { + if let Some(implicits) = implicit_count.get(nam) { + for _ in 0..*implicits { + *self = Term::App { + era: true, + fun: Box::new(std::mem::replace(self, Term::Met {})), + arg: Box::new(Term::Met {}), + }; + } + } + } + }, + Term::Mch { .. } => { + unreachable!() + }, + } + } + + // Counts the number of implicit arguments of a term. + pub fn count_implicits(&self) -> u64 { + match self { + Term::All { era: true, nam: _, inp: _, bod } => { + return 1 + bod.count_implicits(); + } + Term::Src { src: _, val } => { + return val.count_implicits(); + } + Term::Ann { chk: _, val: _, typ } => { + return typ.count_implicits(); + } + _ => { + return 0; + } + } + } + +} diff --git a/src/term/parse.rs b/src/term/parse.rs index 30b6bf739..6e908636a 100644 --- a/src/term/parse.rs +++ b/src/term/parse.rs @@ -72,6 +72,12 @@ impl<'i> KindParser<'i> { } pub fn parse_term(&mut self, fid: u64, uses: &Uses) -> Result { + let init = self.parse_term_ini(fid, uses)?; + let term = self.parse_term_end(fid, uses, init)?; + return Ok(term); + } + + pub fn parse_term_ini(&mut self, fid: u64, uses: &Uses) -> Result { self.skip_trivia(); //println!("parsing ||{}", self.input[self.index..].replace("\n","")); @@ -87,7 +93,7 @@ impl<'i> KindParser<'i> { let bod = Box::new(self.parse_term(fid, &shadow(&nam, uses))?); let end = *self.index() as u64; let src = Src::new(fid, ini, end); - return Ok(Term::Src { src, val: Box::new(Term::All { nam, inp, bod }) }); + return Ok(Term::Src { src, val: Box::new(Term::All { era: false, nam, inp, bod }) }); } // LAM ::= λ @@ -104,20 +110,18 @@ impl<'i> KindParser<'i> { let bod = Box::new(self.parse_term(fid, &shadow(&nam, uses))?); let end = *self.index() as u64; let src = Src::new(fid, ini, end); - let typ = Box::new(Term::All { nam: nam.clone(), inp: typ, bod: Box::new(Term::Met {}) }); - let val = Box::new(Term::Lam { nam: nam.clone(), bod }); + let typ = Box::new(Term::All { era: false, nam: nam.clone(), inp: typ, bod: Box::new(Term::Met {}) }); + let val = Box::new(Term::Lam { era: false, nam: nam.clone(), bod }); let val = Box::new(Term::Ann { chk: true, typ, val }); return Ok(Term::Src { src, val }); } - //λ(x: A) B - //----------------- - //{λx B: ∀(x: A) _} // Untyped let nam = self.parse_name()?; + let era = false; let bod = Box::new(self.parse_term(fid, &shadow(&nam, uses))?); let end = *self.index() as u64; let src = Src::new(fid, ini, end); - return Ok(Term::Src { src, val: Box::new(Term::Lam { nam, bod }) }); + return Ok(Term::Src { src, val: Box::new(Term::Lam { era, nam, bod }) }); } // RFL ::= (=) @@ -129,7 +133,9 @@ impl<'i> KindParser<'i> { return Ok(Term::Src { src, val: Box::new(Term::App { + era: false, fun: Box::new(Term::App { + era: false, fun: Box::new(Term::Var { nam: "Equal.refl".to_string() }), arg: Box::new(Term::Met {}), }), @@ -167,7 +173,7 @@ impl<'i> KindParser<'i> { let src = Src::new(fid, ini, end); let mut app = fun; for arg in args { - app = Box::new(Term::App { fun: app, arg }); + app = Box::new(Term::App { era: false, fun: app, arg }); } return Ok(Term::Src { src, val: app }); } @@ -417,7 +423,16 @@ impl<'i> KindParser<'i> { // MCH ::= match = { : <...> }: if self.starts_with("match ") { let ini = *self.index() as u64; - let mch = self.parse_match(fid, uses)?; + let mch = self.parse_match(fid, uses, false)?; + let end = *self.index() as u64; + let src = Src::new(fid, ini, end); + return Ok(Term::Src { src, val: Box::new(Term::Mch { mch: Box::new(mch) }) }); + } + + // FLD ::= fold = { : <...> }: + if self.starts_with("fold ") { + let ini = *self.index() as u64; + let mch = self.parse_match(fid, uses, true)?; let end = *self.index() as u64; let src = Src::new(fid, ini, end); return Ok(Term::Src { src, val: Box::new(Term::Mch { mch: Box::new(mch) }) }); @@ -438,4 +453,73 @@ impl<'i> KindParser<'i> { } + pub fn parse_term_end(&mut self, fid: u64, uses: &Uses, term: Term) -> Result { + self.skip_trivia(); + + // Simple Function + if self.starts_with("->") { + self.consume("->")?; + let ini = *self.index() as u64; + let nam = "x".to_string(); + let inp = Box::new(term); + let bod = Box::new(self.parse_term(fid, &shadow(&nam, uses))?); + let end = *self.index() as u64; + let src = Src::new(fid, ini, end); + return Ok(Term::Src { src, val: Box::new(Term::All { era: false, nam, inp, bod }) }); + } + + // Equality + if self.starts_with("==") { + self.consume("==")?; + let ini = *self.index() as u64; + let v_0 = term; + let v_1 = self.parse_term(fid, uses)?; + let end = *self.index() as u64; + let src = Src::new(fid, ini, end); + let eql = Equal { a: v_0, b: v_1 }; + return Ok(Term::Src { src, val: Box::new(Term::new_equal(&eql)) }); + } + + // Annotation + if self.starts_with("::") { + self.consume("::")?; + let ini = *self.index() as u64; + let val = Box::new(term); + let typ = Box::new(self.parse_term(fid, uses)?); + let end = *self.index() as u64; + let src = Src::new(fid, ini, end); + return Ok(Term::Src { src, val: Box::new(Term::Ann { chk: true, typ, val }) }); + } + + // List.cons + if self.starts_with(",") { + self.consume(",")?; + let ini = *self.index() as u64; + let hd = Box::new(term); + let tl = Box::new(self.parse_term(fid, uses)?); + let end = *self.index() as u64; + let src = Src::new(fid, ini, end); + return Ok(Term::Src { + src, + val: Box::new(Term::App { + era: false, + fun: Box::new(Term::App { + era: false, + fun: Box::new(Term::App { + era: true, + fun: Box::new(Term::Var { nam: "cons".to_string() }), + arg: Box::new(Term::Met {}), + }), + arg: hd, + }), + arg: tl, + }), + }); + } + + return Ok(term); + } + + + } diff --git a/src/term/show.rs b/src/term/show.rs index a6038b370..23b669e9e 100644 --- a/src/term/show.rs +++ b/src/term/show.rs @@ -65,7 +65,7 @@ impl Term { Term::All { .. } => { let mut bnd = vec![]; let mut bod = self; - while let Term::All { nam, inp, bod: in_bod } = bod { + while let Term::All { era: _, nam, inp, bod: in_bod } = bod { bnd.push(Show::call("", vec![ Show::glue("", vec![ Show::text("∀("), @@ -85,7 +85,7 @@ impl Term { Term::Lam { .. } => { let mut bnd = vec![]; let mut bod = self; - while let Term::Lam { nam, bod: in_bod } = bod { + while let Term::Lam { era: _, nam, bod: in_bod } = bod { bnd.push(Show::text(&format!("λ{}",nam))); bod = in_bod; } @@ -97,7 +97,7 @@ impl Term { Term::App { .. } => { let mut fun = self; let mut spn = vec![]; - while let Term::App { fun: in_fun, arg } = fun { + while let Term::App { era: _, fun: in_fun, arg } = fun { spn.push(arg); fun = in_fun; }