mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Implement HVM.log
This commit is contained in:
Victor Maia
parent
dde08af0cb
commit
a7c3b0ab7b
115
Cargo.lock
generated
115
Cargo.lock
generated
@ -34,6 +34,18 @@ version = "1.3.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
|
||||
|
||||
[[package]]
|
||||
name = "bumpalo"
|
||||
version = "3.11.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c1ad822118d20d2c234f427000d5acc36eabe1e29a348c89b63dd60b13f28e5d"
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
version = "1.0.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "3.2.10"
|
||||
@ -108,15 +120,18 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
|
||||
|
||||
[[package]]
|
||||
name = "hvm"
|
||||
version = "0.1.73"
|
||||
version = "0.1.75"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3a227613b46d330d50ee2fd4a4e1dbdd574dd4fcec7b2465694b84f49aba1592"
|
||||
checksum = "4e70b6dd8ff4dc0ff1b29634547d8e4714455f93e4539e9b993c780bfd83e914"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"highlight_error",
|
||||
"instant",
|
||||
"itertools",
|
||||
"num_cpus",
|
||||
"regex",
|
||||
"wasm-bindgen",
|
||||
"web-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
@ -129,6 +144,18 @@ dependencies = [
|
||||
"hashbrown",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "instant"
|
||||
version = "0.1.12"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"js-sys",
|
||||
"wasm-bindgen",
|
||||
"web-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "itertools"
|
||||
version = "0.10.3"
|
||||
@ -138,9 +165,18 @@ dependencies = [
|
||||
"either",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "js-sys"
|
||||
version = "0.3.59"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "258451ab10b34f8af53416d1fdab72c22e805f0c92a1136d59470ec0b11138b2"
|
||||
dependencies = [
|
||||
"wasm-bindgen",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind2"
|
||||
version = "0.2.57"
|
||||
version = "0.2.59"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"highlight_error",
|
||||
@ -153,6 +189,15 @@ version = "0.2.126"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "349d5a591cd28b49e1d1037471617a32ddcda5731b99419008085f72d5a53836"
|
||||
|
||||
[[package]]
|
||||
name = "log"
|
||||
version = "0.4.17"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "abb12e687cfb44aa40f41fc3978ef76448f9b6038cad6aef4259d3c095a2382e"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "memchr"
|
||||
version = "2.5.0"
|
||||
@ -284,6 +329,70 @@ version = "0.9.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen"
|
||||
version = "0.2.82"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "fc7652e3f6c4706c8d9cd54832c4a4ccb9b5336e2c3bd154d5cccfbf1c1f5f7d"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"wasm-bindgen-macro",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen-backend"
|
||||
version = "0.2.82"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "662cd44805586bd52971b9586b1df85cdbbd9112e4ef4d8f41559c334dc6ac3f"
|
||||
dependencies = [
|
||||
"bumpalo",
|
||||
"log",
|
||||
"once_cell",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
"wasm-bindgen-shared",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen-macro"
|
||||
version = "0.2.82"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b260f13d3012071dfb1512849c033b1925038373aea48ced3012c09df952c602"
|
||||
dependencies = [
|
||||
"quote",
|
||||
"wasm-bindgen-macro-support",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen-macro-support"
|
||||
version = "0.2.82"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5be8e654bdd9b79216c2929ab90721aa82faf65c48cdf08bdc4e7f51357b80da"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
"wasm-bindgen-backend",
|
||||
"wasm-bindgen-shared",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "wasm-bindgen-shared"
|
||||
version = "0.2.82"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6598dd0bd3c7d51095ff6531a5b23e02acdc81804e30d8f07afb77b7215a140a"
|
||||
|
||||
[[package]]
|
||||
name = "web-sys"
|
||||
version = "0.3.59"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ed055ab27f941423197eb86b2035720b1a3ce40504df082cac2ecc6ed73335a1"
|
||||
dependencies = [
|
||||
"js-sys",
|
||||
"wasm-bindgen",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "winapi"
|
||||
version = "0.3.9"
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
[package]
|
||||
name = "kind2"
|
||||
version = "0.2.59"
|
||||
version = "0.2.60"
|
||||
edition = "2021"
|
||||
description = "A pure functional functional language that uses the HVM."
|
||||
repository = "https://github.com/Kindelia/Kind2"
|
||||
@ -10,7 +10,7 @@ keywords = ["functional", "language", "type-theory", "proof-assistant"]
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
hvm = "0.1.73"
|
||||
hvm = "0.1.75"
|
||||
#hvm = { path = "../hvm" }
|
||||
highlight_error = "0.1.1"
|
||||
clap = { version = "3.1.8", features = ["derive"] }
|
||||
|
||||
@ -1763,7 +1763,11 @@ pub fn compile_entry(entry: &Entry) -> String {
|
||||
let rule_rhs = compile_term(&rule.body, false, false);
|
||||
let mut text = String::new();
|
||||
text.push_str(&format!("(Q${} orig{}) = {}\n", rule.name, pats.join(""), body_rhs));
|
||||
text.push_str(&format!("(F${} orig{}) = {}\n", rule.name, pats.join(""), rule_rhs));
|
||||
if rule.name == "HVM.log" {
|
||||
text.push_str(&format!("(F$HVM.log orig a r log ret) = (HVM.put (Show log) ret)"));
|
||||
} else {
|
||||
text.push_str(&format!("(F${} orig{}) = {}\n", rule.name, pats.join(""), rule_rhs));
|
||||
}
|
||||
|
||||
//for size in 0 .. 9 {
|
||||
//let mut vars = vec![];
|
||||
|
||||
@ -259,14 +259,14 @@ fn run_with_hvm(code: &str, main: &str, read_string: bool) -> Result<RunResult,
|
||||
pub fn readback_string(rt: &hvm::Runtime, host: u64) -> String {
|
||||
let str_cons = rt.get_id("String.cons");
|
||||
let str_nil = rt.get_id("String.nil");
|
||||
let mut term = rt.ptr(host);
|
||||
let mut term = rt.at(host);
|
||||
let mut text = String::new();
|
||||
loop {
|
||||
if hvm::get_tag(term) == hvm::CTR {
|
||||
let fid = hvm::get_ext(term);
|
||||
if fid == str_cons {
|
||||
let head = rt.ptr(hvm::get_loc(term, 0));
|
||||
let tail = rt.ptr(hvm::get_loc(term, 1));
|
||||
let head = rt.at(hvm::get_loc(term, 0));
|
||||
let tail = rt.at(hvm::get_loc(term, 1));
|
||||
if hvm::get_tag(head) == hvm::NUM {
|
||||
text.push(std::char::from_u32(hvm::get_num(head) as u32).unwrap_or('?'));
|
||||
term = tail;
|
||||
|
||||
@ -103,6 +103,9 @@ pub fn to_hvm_rule(book: &Book, rule: &Rule) -> String {
|
||||
|
||||
pub fn to_hvm_entry(book: &Book, entry: &Entry) -> String {
|
||||
let name = &entry.name;
|
||||
if name == "HVM.log" {
|
||||
return "".to_string();
|
||||
}
|
||||
let mut args = vec![];
|
||||
for arg in &entry.args {
|
||||
args.push(format!(" {}({}: {})", if arg.eras { "-" } else { "" }, arg.name, show_term(&arg.tipo)));
|
||||
|
||||
Loading…
Reference in New Issue
Block a user