mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-10-03 18:27:13 +03:00
implicits args and stuff
This commit is contained in:
Victor Taelin
parent
dd6706a7d5
commit
0647ea9bc7
1
.gitignore
vendored
1
.gitignore
vendored
@ -8,3 +8,4 @@ demo/
|
||||
.fill.tmp
|
||||
.check.hs
|
||||
guide.txt
|
||||
.hvm
|
||||
|
||||
16
book/.hvm/Cargo.lock
generated
Normal file
16
book/.hvm/Cargo.lock
generated
Normal file
@ -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"
|
||||
31
book/.hvm/Cargo.toml
Normal file
31
book/.hvm/Cargo.toml
Normal file
@ -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"
|
||||
|
||||
799
book/.hvm/src/ast.rs
Normal file
799
book/.hvm/src/ast.rs
Normal file
@ -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<Tree>, rgt: Box<Tree> },
|
||||
Tup { lft: Box<Tree>, rgt: Box<Tree> },
|
||||
Dup { lab: run::Lab, lft: Box<Tree>, rgt: Box<Tree> },
|
||||
Var { nam: String },
|
||||
Ref { nam: run::Val },
|
||||
Num { val: run::Val },
|
||||
Op1 { opr: run::Lab, lft: run::Val, rgt: Box<Tree> },
|
||||
Op2 { opr: run::Lab, lft: Box<Tree>, rgt: Box<Tree> },
|
||||
Mat { sel: Box<Tree>, ret: Box<Tree> },
|
||||
}
|
||||
|
||||
type Redex = Vec<(Tree, Tree)>;
|
||||
|
||||
#[derive(Clone, Hash, PartialEq, Eq, Debug)]
|
||||
pub struct Net {
|
||||
pub root: Tree,
|
||||
pub rdex: Redex,
|
||||
}
|
||||
|
||||
pub type Book = BTreeMap<String, Net>;
|
||||
|
||||
// Parser
|
||||
// ------
|
||||
|
||||
// FIXME: remove after skip is fixed
|
||||
fn skip_spaces(chars: &mut Peekable<Chars>) {
|
||||
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<Chars>) {
|
||||
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<Chars>, 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<Chars>) -> Result<u64, String> {
|
||||
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<Chars>) -> Result<String, String> {
|
||||
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<Chars>) -> Result<String, String> {
|
||||
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<Chars>) -> Result<run::Lab, String> {
|
||||
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<Chars>) -> Result<Tree, String> {
|
||||
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<Chars>) -> Result<Net, String> {
|
||||
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<Chars>) -> Result<Book, String> {
|
||||
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<T>(code: &str, parse_fn: impl Fn(&mut Peekable<Chars>) -> Result<T, String>) -> 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<const LAZY: bool>(rt_net: &run::NetFields<LAZY>, 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<const LAZY: bool>(rt_net: &run::NetFields<LAZY>) -> 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<u8> {
|
||||
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<u8>) -> 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<u8> {
|
||||
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<u8>) -> 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<const LAZY: bool>(rt_net: &mut run::NetFields<LAZY>, tree: &Tree, vars: &mut HashMap<String, Parent>, 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<const LAZY: bool>(rt_net: &mut run::NetFields<LAZY>, 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<const LAZY: bool>(rt_net: &mut run::NetFields<LAZY>, 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<run::Lab, nohash_hasher::BuildNoHashHasher<run::Lab>>;
|
||||
type InsideRefs = HashSet<run::Val>;
|
||||
#[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<run::Val, Inside>, fid: run::Val, seen: &mut HashSet<run::Val>) {
|
||||
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::<false>::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<const LAZY: bool>(net: &run::NetFields<LAZY>) -> 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<LAZY>, 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<const LAZY: bool>(rt_net: &run::NetFields<LAZY>, ptr: run::Ptr, parent: Parent, vars: &mut HashMap<Parent, String>, 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<const LAZY: bool>(rt_net: &run::NetFields<LAZY>, 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<const LAZY: bool>(rt_net: &run::NetFields<LAZY>) -> 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::<false>::init(def.node.len());
|
||||
let net = net_from_runtime(&runtime_def_to_runtime_net(&nodes, &def));
|
||||
book.insert(name, net);
|
||||
}
|
||||
}
|
||||
book
|
||||
}
|
||||
355
book/.hvm/src/fns.rs
Normal file
355
book/.hvm/src/fns.rs
Normal file
@ -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;
|
||||
}
|
||||
|
||||
}
|
||||
452
book/.hvm/src/jit.rs
Normal file
452
book/.hvm/src/jit.rs
Normal file
@ -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<NUM>'
|
||||
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<run::Ptr, String>,
|
||||
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<run::Val>,
|
||||
newx : &mut usize,
|
||||
vars : &mut HashMap<run::Ptr, String>,
|
||||
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<run::Val>,
|
||||
newx : &mut usize,
|
||||
vars : &mut HashMap<run::Ptr, String>,
|
||||
def : &run::Def,
|
||||
ptr : run::Ptr,
|
||||
trg : &Target,
|
||||
) -> String {
|
||||
//println!("burn {:08x} {}", ptr.0, x);
|
||||
let mut code = String::new();
|
||||
|
||||
// (<?(ifz ifs) ret> 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<run::Ptr, String>,
|
||||
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<run::Ptr, String>,
|
||||
def : &run::Def,
|
||||
ptr : run::Ptr,
|
||||
) -> Option<String> {
|
||||
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.");
|
||||
}
|
||||
}
|
||||
14
book/.hvm/src/lib.rs
Normal file
14
book/.hvm/src/lib.rs
Normal file
@ -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;
|
||||
256
book/.hvm/src/main.rs
Normal file
256
book/.hvm/src/main.rs
Normal file
@ -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<String>,
|
||||
}
|
||||
|
||||
fn get_args() -> Args {
|
||||
let args: Vec<String> = 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::<HashSet<_>>();
|
||||
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<dyn std::error::Error>> {
|
||||
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 <file.hvmc> [-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 <file.hvmc>");
|
||||
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 <file.hvmc>");
|
||||
std::process::exit(1);
|
||||
}
|
||||
}
|
||||
_ => {
|
||||
println!("Usage: hvmc <cmd> <file.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<dyn std::error::Error>> {
|
||||
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;
|
||||
}
|
||||
1389
book/.hvm/src/run.rs
Normal file
1389
book/.hvm/src/run.rs
Normal file
File diff suppressed because it is too large
Load Diff
113
book/.hvm/src/u60.rs
Normal file
113
book/.hvm/src/u60.rs
Normal file
@ -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);
|
||||
}
|
||||
1
book/.hvm/target/.rustc_info.json
Normal file
1
book/.hvm/target/.rustc_info.json
Normal file
@ -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":{}}
|
||||
3
book/.hvm/target/CACHEDIR.TAG
Normal file
3
book/.hvm/target/CACHEDIR.TAG
Normal file
@ -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/
|
||||
0
book/.hvm/target/release/.cargo-lock
Normal file
0
book/.hvm/target/release/.cargo-lock
Normal file
@ -0,0 +1 @@
|
||||
This file has an mtime of when this was started.
|
||||
@ -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":": <type>","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: `: <type>`\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"}
|
||||
Binary file not shown.
@ -0,0 +1 @@
|
||||
This file has an mtime of when this was started.
|
||||
@ -0,0 +1 @@
|
||||
7cda99c4629b01d5
|
||||
@ -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}
|
||||
12
book/.hvm/target/release/deps/hvmc-5d3b356175a8b321.d
Normal file
12
book/.hvm/target/release/deps/hvmc-5d3b356175a8b321.d
Normal file
@ -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:
|
||||
Binary file not shown.
Binary file not shown.
@ -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:
|
||||
@ -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
|
||||
}
|
||||
|
||||
@ -1,2 +1,2 @@
|
||||
Bool.false : Bool =
|
||||
false : Bool =
|
||||
~λP λt λf f
|
||||
|
||||
@ -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: {=}
|
||||
|
||||
@ -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 <A> <B> <a> <b> (f: A -> B) (e: a == b) : (f a) == (f b) =
|
||||
match e {
|
||||
refl: {=}
|
||||
}
|
||||
|
||||
|
||||
//Equal.apply
|
||||
//: ∀(A: *)
|
||||
//∀(B: *)
|
||||
|
||||
3
book/List.Church.cons.kind2
Normal file
3
book/List.Church.cons.kind2
Normal file
@ -0,0 +1,3 @@
|
||||
cons <T> (head: T) (tail: (List.Church T)) : (List.Church T)
|
||||
= λP λcons λnil
|
||||
(cons head (tail P cons nil))
|
||||
5
book/List.Church.kind2
Normal file
5
book/List.Church.kind2
Normal file
@ -0,0 +1,5 @@
|
||||
List.Church (T) : * =
|
||||
∀(P: *)
|
||||
∀(cons: T -> P -> P)
|
||||
∀(nil: P)
|
||||
P
|
||||
3
book/List.Church.nil.kind2
Normal file
3
book/List.Church.nil.kind2
Normal file
@ -0,0 +1,3 @@
|
||||
List.Church.nil (T) : (List.Church T)
|
||||
= λP λcons λnil
|
||||
nil
|
||||
@ -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))
|
||||
@ -1,7 +0,0 @@
|
||||
List.Folder
|
||||
: ∀(T: *) *
|
||||
= λT
|
||||
∀(P: *)
|
||||
∀(cons: ∀(head: T) ∀(tail: P) P)
|
||||
∀(nil: P)
|
||||
P
|
||||
@ -1,3 +0,0 @@
|
||||
List.Folder.nil
|
||||
: ∀(T: *) (List.Folder T)
|
||||
= λT λP λcons λnil nil
|
||||
@ -1,3 +1,2 @@
|
||||
List.cons
|
||||
: ∀(T: *) ∀(head: T) ∀(tail: (List T)) (List T)
|
||||
= λT λhead λtail ~λP λcons λnil (cons head tail)
|
||||
List.cons <T> (head: T) (tail: (List T)) : (List T) =
|
||||
~λP λcons λnil (cons head tail)
|
||||
|
||||
@ -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)
|
||||
use List.{cons,nil}
|
||||
|
||||
List.fold <A> <B> (xs: (List A)) (c: A -> B -> B) (n: B) : B =
|
||||
match xs {
|
||||
cons: (c xs.head (List.fold xs.tail c n))
|
||||
nil: n
|
||||
}
|
||||
|
||||
16
book/List.map.kind2
Normal file
16
book/List.map.kind2
Normal file
@ -0,0 +1,16 @@
|
||||
use List.{cons,nil}
|
||||
|
||||
map <A> <B> (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: []
|
||||
//}
|
||||
@ -1,3 +1,2 @@
|
||||
List.nil
|
||||
: ∀(T: *) (List T)
|
||||
= λT ~λP λcons λnil nil
|
||||
List.nil <T> : (List T) =
|
||||
~λP λcons λnil nil
|
||||
|
||||
@ -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: {=}
|
||||
}
|
||||
|
||||
21
book/_main.hvm2
Normal file
21
book/_main.hvm2
Normal file
@ -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
|
||||
|
||||
17
book/_main.hvmc
Normal file
17
book/_main.hvmc
Normal file
@ -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))
|
||||
|
||||
@ -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 {
|
||||
|
||||
14
book/_tmp.hvm2
Normal file
14
book/_tmp.hvm2
Normal file
@ -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))
|
||||
|
||||
19
book/_tmp.kind2
Normal file
19
book/_tmp.kind2
Normal file
@ -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
|
||||
|
||||
436
kind2.ts
436
kind2.ts
@ -1,436 +0,0 @@
|
||||
#!/usr/bin/env ts-node
|
||||
|
||||
// TODO: move the parser to HVM
|
||||
|
||||
// ICC: Parser, Stringifier and CLI
|
||||
// ================================
|
||||
|
||||
// List
|
||||
// ----
|
||||
|
||||
type List<A> =
|
||||
| { tag: "Cons"; head: A; tail: List<A> }
|
||||
| { tag: "Nil"; };
|
||||
|
||||
// Constructors
|
||||
const Cons = <A>(head: A, tail: List<A>): List<A> => ({ tag: "Cons", head, tail });
|
||||
const Nil = <A>(): List<A> => ({ 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 } // #(<opr> 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<A>(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: `#(<opr> 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] <name>");
|
||||
}
|
||||
}
|
||||
|
||||
// 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();
|
||||
22
package.json
22
package.json
@ -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"
|
||||
}
|
||||
@ -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
|
||||
}
|
||||
|
||||
@ -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) {
|
||||
|
||||
@ -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);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
39
src/main.rs
39
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::<String>("name").expect("required");
|
||||
format_def(name);
|
||||
auto_format(name);
|
||||
}
|
||||
Some(("compile", sub_matches)) => {
|
||||
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||
|
||||
112
src/sugar/mod.rs
112
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<Box<Term>>
|
||||
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<Equal> {
|
||||
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<Term> = 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<Show> {
|
||||
|
||||
// ADT head: `data Name <params> <indices>`
|
||||
@ -856,12 +873,14 @@ impl Term {
|
||||
if let Some(moti) = &mat.moti {
|
||||
// Creates the first lambda: 'λx <motive>'
|
||||
motive = Term::Lam {
|
||||
era: false,
|
||||
nam: mat.name.clone(),
|
||||
bod: Box::new(moti.clone()),
|
||||
};
|
||||
// Creates a lambda for each index: 'λindices ... λx <motive>'
|
||||
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) ... <motive>'
|
||||
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> {
|
||||
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 <name> = <term> { <name> : <term> <...> }: <term>
|
||||
pub fn parse_match(&mut self, fid: u64, uses: &Uses) -> Result<Match, String> {
|
||||
pub fn parse_match(&mut self, fid: u64, uses: &Uses, fold: bool) -> Result<Match, String> {
|
||||
// Parses the header: 'match <name> = <expr>'
|
||||
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 });
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
@ -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<String>, 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)
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
245
src/term/mod.rs
245
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 | <name>
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum Term {
|
||||
All { nam: String, inp: Box<Term>, bod: Box<Term> },
|
||||
Lam { nam: String, bod: Box<Term> },
|
||||
App { fun: Box<Term>, arg: Box<Term> },
|
||||
All { era: bool, nam: String, inp: Box<Term>, bod: Box<Term> },
|
||||
Lam { era: bool, nam: String, bod: Box<Term> },
|
||||
App { era: bool, fun: Box<Term>, arg: Box<Term> },
|
||||
Ann { chk: bool, val: Box<Term>, typ: Box<Term> },
|
||||
Slf { nam: String, typ: Box<Term>, bod: Box<Term> },
|
||||
Ins { val: Box<Term> },
|
||||
@ -102,14 +107,14 @@ impl Term {
|
||||
|
||||
pub fn get_free_vars(&self, env: im::Vector<String>, free_vars: &mut BTreeSet<String>) {
|
||||
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<String>, implicit_count: &BTreeMap<String, u64>) {
|
||||
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;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
@ -72,6 +72,12 @@ impl<'i> KindParser<'i> {
|
||||
}
|
||||
|
||||
pub fn parse_term(&mut self, fid: u64, uses: &Uses) -> Result<Term, String> {
|
||||
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<Term, String> {
|
||||
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 ::= λ<name> <term>
|
||||
@ -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 <name> = <term> { <name> : <term> <...> }: <term>
|
||||
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 <name> = <term> { <name> : <term> <...> }: <term>
|
||||
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<Term, String> {
|
||||
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);
|
||||
}
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
||||
@ -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;
|
||||
}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user