mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-17 11:30:30 +03:00
refactored CLI - by Claude3
This commit is contained in:
parent
6726b552b3
commit
dd6706a7d5
160
Cargo.lock
generated
160
Cargo.lock
generated
@ -11,6 +11,54 @@ dependencies = [
|
|||||||
"highlight_error",
|
"highlight_error",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "anstream"
|
||||||
|
version = "0.6.13"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "d96bd03f33fe50a863e394ee9718a706f988b9079b20c3784fb726e7678b62fb"
|
||||||
|
dependencies = [
|
||||||
|
"anstyle",
|
||||||
|
"anstyle-parse",
|
||||||
|
"anstyle-query",
|
||||||
|
"anstyle-wincon",
|
||||||
|
"colorchoice",
|
||||||
|
"utf8parse",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "anstyle"
|
||||||
|
version = "1.0.6"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "8901269c6307e8d93993578286ac0edf7f195079ffff5ebdeea6a59ffb7e36bc"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "anstyle-parse"
|
||||||
|
version = "0.2.3"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "c75ac65da39e5fe5ab759307499ddad880d724eed2f6ce5b5e8a26f4f387928c"
|
||||||
|
dependencies = [
|
||||||
|
"utf8parse",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "anstyle-query"
|
||||||
|
version = "1.0.2"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "e28923312444cdd728e4738b3f9c9cac739500909bb3d3c94b43551b16517648"
|
||||||
|
dependencies = [
|
||||||
|
"windows-sys",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "anstyle-wincon"
|
||||||
|
version = "3.0.2"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "1cd54b81ec8d6180e24654d0b371ad22fc3dd083b6ff8ba325b72e00c87660a7"
|
||||||
|
dependencies = [
|
||||||
|
"anstyle",
|
||||||
|
"windows-sys",
|
||||||
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "bitmaps"
|
name = "bitmaps"
|
||||||
version = "2.1.0"
|
version = "2.1.0"
|
||||||
@ -20,6 +68,39 @@ dependencies = [
|
|||||||
"typenum",
|
"typenum",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "clap"
|
||||||
|
version = "4.5.2"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "b230ab84b0ffdf890d5a10abdbc8b83ae1c4918275daea1ab8801f71536b2651"
|
||||||
|
dependencies = [
|
||||||
|
"clap_builder",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "clap_builder"
|
||||||
|
version = "4.5.2"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "ae129e2e766ae0ec03484e609954119f123cc1fe650337e155d03b022f24f7b4"
|
||||||
|
dependencies = [
|
||||||
|
"anstream",
|
||||||
|
"anstyle",
|
||||||
|
"clap_lex",
|
||||||
|
"strsim",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "clap_lex"
|
||||||
|
version = "0.7.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "colorchoice"
|
||||||
|
version = "1.0.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "highlight_error"
|
name = "highlight_error"
|
||||||
version = "0.1.1"
|
version = "0.1.1"
|
||||||
@ -45,6 +126,7 @@ name = "kind2"
|
|||||||
version = "0.1.0"
|
version = "0.1.0"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"TSPL",
|
"TSPL",
|
||||||
|
"clap",
|
||||||
"highlight_error",
|
"highlight_error",
|
||||||
"im",
|
"im",
|
||||||
]
|
]
|
||||||
@ -74,14 +156,92 @@ dependencies = [
|
|||||||
"typenum",
|
"typenum",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "strsim"
|
||||||
|
version = "0.11.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "5ee073c9e4cd00e28217186dbe12796d692868f432bf2e97ee73bed0c56dfa01"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "typenum"
|
name = "typenum"
|
||||||
version = "1.17.0"
|
version = "1.17.0"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
|
checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "utf8parse"
|
||||||
|
version = "0.2.1"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "version_check"
|
name = "version_check"
|
||||||
version = "0.9.4"
|
version = "0.9.4"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
|
checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "windows-sys"
|
||||||
|
version = "0.52.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
|
||||||
|
dependencies = [
|
||||||
|
"windows-targets",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "windows-targets"
|
||||||
|
version = "0.52.4"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "7dd37b7e5ab9018759f893a1952c9420d060016fc19a472b4bb20d1bdd694d1b"
|
||||||
|
dependencies = [
|
||||||
|
"windows_aarch64_gnullvm",
|
||||||
|
"windows_aarch64_msvc",
|
||||||
|
"windows_i686_gnu",
|
||||||
|
"windows_i686_msvc",
|
||||||
|
"windows_x86_64_gnu",
|
||||||
|
"windows_x86_64_gnullvm",
|
||||||
|
"windows_x86_64_msvc",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "windows_aarch64_gnullvm"
|
||||||
|
version = "0.52.4"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "bcf46cf4c365c6f2d1cc93ce535f2c8b244591df96ceee75d8e83deb70a9cac9"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "windows_aarch64_msvc"
|
||||||
|
version = "0.52.4"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "da9f259dd3bcf6990b55bffd094c4f7235817ba4ceebde8e6d11cd0c5633b675"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "windows_i686_gnu"
|
||||||
|
version = "0.52.4"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "b474d8268f99e0995f25b9f095bc7434632601028cf86590aea5c8a5cb7801d3"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "windows_i686_msvc"
|
||||||
|
version = "0.52.4"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "1515e9a29e5bed743cb4415a9ecf5dfca648ce85ee42e15873c3cd8610ff8e02"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "windows_x86_64_gnu"
|
||||||
|
version = "0.52.4"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "5eee091590e89cc02ad514ffe3ead9eb6b660aedca2183455434b93546371a03"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "windows_x86_64_gnullvm"
|
||||||
|
version = "0.52.4"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "77ca79f2451b49fa9e2af39f0747fe999fcda4f5e241b2898624dca97a1f2177"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "windows_x86_64_msvc"
|
||||||
|
version = "0.52.4"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8"
|
||||||
|
@ -11,3 +11,4 @@ path = "src/main.rs"
|
|||||||
TSPL = "0.0.8"
|
TSPL = "0.0.8"
|
||||||
highlight_error = "0.1.1"
|
highlight_error = "0.1.1"
|
||||||
im = "15.1.0"
|
im = "15.1.0"
|
||||||
|
clap = "4.5.2"
|
||||||
|
@ -1,8 +1,5 @@
|
|||||||
use crate::{*};
|
use crate::{*};
|
||||||
|
|
||||||
use std::collections::BTreeMap;
|
|
||||||
use std::collections::BTreeSet;
|
|
||||||
|
|
||||||
impl Book {
|
impl Book {
|
||||||
|
|
||||||
pub fn to_hvm1_checker(&self) -> String {
|
pub fn to_hvm1_checker(&self) -> String {
|
||||||
|
@ -1,8 +1,5 @@
|
|||||||
use crate::{*};
|
use crate::{*};
|
||||||
|
|
||||||
use std::collections::BTreeMap;
|
|
||||||
use std::collections::BTreeSet;
|
|
||||||
|
|
||||||
impl<'i> KindParser<'i> {
|
impl<'i> KindParser<'i> {
|
||||||
|
|
||||||
// Parses a top-level use-declaration
|
// Parses a top-level use-declaration
|
||||||
|
268
src/main.rs
268
src/main.rs
@ -1,5 +1,8 @@
|
|||||||
#![allow(dead_code)]
|
use clap::{Arg, ArgAction, Command};
|
||||||
#![allow(unused_imports)]
|
use std::fs;
|
||||||
|
use std::io::Write;
|
||||||
|
use std::path::PathBuf;
|
||||||
|
use std::process::Command as SysCommand;
|
||||||
|
|
||||||
mod book;
|
mod book;
|
||||||
mod info;
|
mod info;
|
||||||
@ -7,33 +10,17 @@ mod show;
|
|||||||
mod sugar;
|
mod sugar;
|
||||||
mod term;
|
mod term;
|
||||||
|
|
||||||
use book::{*};
|
use book::*;
|
||||||
use info::{*};
|
use info::*;
|
||||||
use show::{*};
|
use show::*;
|
||||||
use sugar::{*};
|
use sugar::*;
|
||||||
use term::{*};
|
use term::*;
|
||||||
|
|
||||||
use TSPL::Parser;
|
|
||||||
use highlight_error::highlight_error;
|
use highlight_error::highlight_error;
|
||||||
use std::env;
|
use TSPL::Parser;
|
||||||
use std::fs::File;
|
|
||||||
use std::io::Write;
|
|
||||||
use std::process::Command;
|
|
||||||
|
|
||||||
TSPL::new_parser!(KindParser);
|
TSPL::new_parser!(KindParser);
|
||||||
|
|
||||||
fn generate_check_hvm1(book: &Book, command: &str, arg: &str) -> String {
|
|
||||||
let kind_hvm1 = include_str!("./kind2.hvm1");
|
|
||||||
let book_hvm1 = book.to_hvm1_checker();
|
|
||||||
let main_hvm1 = match command {
|
|
||||||
"check" => format!("Main = (API.check Book.{})\n", arg),
|
|
||||||
"run" => format!("Main = (API.normal Book.{})\n", arg),
|
|
||||||
_ => panic!("invalid command"),
|
|
||||||
};
|
|
||||||
let hvm1_code = format!("{}\n{}\n{}", kind_hvm1, book_hvm1, main_hvm1);
|
|
||||||
return hvm1_code;
|
|
||||||
}
|
|
||||||
|
|
||||||
fn generate_check_hvm2(book: &Book, command: &str, arg: &str) -> String {
|
fn generate_check_hvm2(book: &Book, command: &str, arg: &str) -> String {
|
||||||
let kind_hvm2 = include_str!("./kind2.hvm2");
|
let kind_hvm2 = include_str!("./kind2.hvm2");
|
||||||
let book_hvm2 = book.to_hvm2_checker();
|
let book_hvm2 = book.to_hvm2_checker();
|
||||||
@ -42,69 +29,45 @@ fn generate_check_hvm2(book: &Book, command: &str, arg: &str) -> String {
|
|||||||
"run" => format!("main = (apiNormal Book.{})\n", arg),
|
"run" => format!("main = (apiNormal Book.{})\n", arg),
|
||||||
_ => panic!("invalid command"),
|
_ => panic!("invalid command"),
|
||||||
};
|
};
|
||||||
let hvm2_code = format!("{}\n{}\n{}", kind_hvm2, book_hvm2, main_hvm2);
|
format!("{}\n{}\n{}", kind_hvm2, book_hvm2, main_hvm2)
|
||||||
return hvm2_code;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn generate_check_hs(book: &Book, command: &str, arg: &str) -> String {
|
fn generate_check_hs(book: &Book, command: &str, arg: &str) -> String {
|
||||||
let kind_hs = include_str!("./kind2.hs");
|
let kind_hs = include_str!("./kind2.hs")
|
||||||
let kind_hs = kind_hs.lines().filter(|line| !line.starts_with("xString")).collect::<Vec<_>>().join("\n");
|
.lines()
|
||||||
|
.filter(|line| !line.starts_with("xString"))
|
||||||
|
.collect::<Vec<_>>()
|
||||||
|
.join("\n");
|
||||||
let book_hs = book.to_hs_checker();
|
let book_hs = book.to_hs_checker();
|
||||||
let main_hs = match command {
|
let main_hs = match command {
|
||||||
"check" => format!("main = (apiCheck {})\n", Term::to_hs_name(arg)),
|
"check" => format!("main = (apiCheck {})\n", Term::to_hs_name(arg)),
|
||||||
"run" => format!("main = (apiNormal {})\n", Term::to_hs_name(arg)),
|
"run" => format!("main = (apiNormal {})\n", Term::to_hs_name(arg)),
|
||||||
_ => panic!("invalid command"),
|
_ => panic!("invalid command"),
|
||||||
};
|
};
|
||||||
let hs_code = format!("{}\n{}\n{}", kind_hs, book_hs, main_hs);
|
format!("{}\n{}\n{}", kind_hs, book_hs, main_hs)
|
||||||
return hs_code;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn generate_hvm2(book: &Book, _command: &str, arg: &str) -> String {
|
fn generate_hvm2(book: &Book, arg: &str) -> String {
|
||||||
let book_hvm2 = book.to_hvm2();
|
let book_hvm2 = book.to_hvm2();
|
||||||
let main_hvm2 = format!("main = {}\n", arg);
|
let main_hvm2 = format!("main = {}\n", arg);
|
||||||
let code_hvm2 = format!("{}\n{}", book_hvm2, main_hvm2);
|
format!("{}\n{}", book_hvm2, main_hvm2)
|
||||||
return code_hvm2;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn get_infos(book: &Book, cmd: &str, file: &str, runtime: &str) -> (Vec<Info>, String) {
|
fn run_kore(book: &Book, cmd: &str, file: &str, runtime: &str) -> (Vec<Info>, String) {
|
||||||
// Auto-formats the definition.
|
|
||||||
// let defn = book.defs.get(file).unwrap();
|
|
||||||
// let form = book.format_def(file, defn).flatten(60);
|
|
||||||
|
|
||||||
// Overwrites the original file with the formatted version.
|
|
||||||
// File::create(&format!("./{}.kind2", file))
|
|
||||||
// .and_then(|mut file| file.write_all(form.as_bytes()))
|
|
||||||
// .unwrap_or_else(|_| panic!("Failed to auto-format '{}.kind2'.", file));
|
|
||||||
|
|
||||||
let command = match runtime {
|
let command = match runtime {
|
||||||
"--ghc" => {
|
"hs" => {
|
||||||
// Generates the Haskell checker.
|
|
||||||
let check_hs = generate_check_hs(&book, cmd, file);
|
let check_hs = generate_check_hs(&book, cmd, file);
|
||||||
let mut file = File::create(".check.hs").expect("Failed to create '.check.hs'.");
|
let mut file = fs::File::create(".check.hs").expect("Failed to create '.check.hs'.");
|
||||||
file.write_all(check_hs.as_bytes()).expect("Failed to write '.check.hs'.");
|
file.write_all(check_hs.as_bytes()).expect("Failed to write '.check.hs'.");
|
||||||
|
SysCommand::new("runghc").arg(".check.hs").output().expect("Failed to execute command")
|
||||||
// Calls GHC and get outputs.
|
|
||||||
Command::new("runghc").arg(".check.hs").output().expect("Failed to execute command")
|
|
||||||
}
|
}
|
||||||
"--hvm1" => {
|
"hvm2" => {
|
||||||
// Generates the HVM1 checker.
|
let check_hvm2 = generate_check_hvm2(&book, cmd, file);
|
||||||
let check_hvm1 = generate_check_hvm1(&book, cmd, file);
|
let mut file = fs::File::create(".check.hvm2").expect("Failed to create '.check.hvm2'.");
|
||||||
let mut file = File::create(".check.hvm1").expect("Failed to create '.check.hvm1'.");
|
file.write_all(check_hvm2.as_bytes()).expect("Failed to write '.check.hvm2'.");
|
||||||
file.write_all(check_hvm1.as_bytes()).expect("Failed to write '.check.hvm1'.");
|
SysCommand::new("hvml").arg("run").arg("-L").arg(".check.hvm2").output().expect("Failed to execute command")
|
||||||
|
|
||||||
// Calls HVM1 and get outputs.
|
|
||||||
Command::new("hvm1").arg("run").arg("-t").arg("1").arg("-c").arg("-f").arg(".check.hvm1").arg("(Main)").output().expect("Failed to execute command")
|
|
||||||
}
|
}
|
||||||
"--hvm2" => {
|
_ => panic!("invalid runtime"),
|
||||||
// Generates the hvm2 checker.
|
|
||||||
let check_hs = generate_check_hvm2(&book, cmd, file);
|
|
||||||
let mut file = File::create(".check.hvm2").expect("Failed to create '.check.hs'.");
|
|
||||||
file.write_all(check_hs.as_bytes()).expect("Failed to write '.check.hs'.");
|
|
||||||
|
|
||||||
// Calls HVMl and get outputs.
|
|
||||||
Command::new("hvml").arg("run").arg("-L").arg(".check.hvm2").output().expect("Failed to execute command")
|
|
||||||
}
|
|
||||||
_ => panic!("invalid command"),
|
|
||||||
};
|
};
|
||||||
|
|
||||||
let stdout = String::from_utf8_lossy(&command.stdout);
|
let stdout = String::from_utf8_lossy(&command.stdout);
|
||||||
@ -113,83 +76,69 @@ pub fn get_infos(book: &Book, cmd: &str, file: &str, runtime: &str) -> (Vec<Info
|
|||||||
(Info::parse_infos(&stdout), stderr.to_string())
|
(Info::parse_infos(&stdout), stderr.to_string())
|
||||||
}
|
}
|
||||||
|
|
||||||
fn main() {
|
fn check(name: &str, runtime: &str) {
|
||||||
let args: Vec<String> = env::args().collect();
|
let book = load_book(name);
|
||||||
|
let (infos, stderr) = run_kore(&book, "check", name, runtime);
|
||||||
if args.len() < 2 {
|
|
||||||
show_help();
|
|
||||||
}
|
|
||||||
|
|
||||||
let cmd = &args[1];
|
|
||||||
|
|
||||||
//println!("loading");
|
|
||||||
match cmd.as_str() {
|
|
||||||
"check" | "run" => {
|
|
||||||
if args.len() < 3 {
|
|
||||||
show_help();
|
|
||||||
}
|
|
||||||
let arg = &args[2];
|
|
||||||
let opt = &args.get(3).map(|x| x.as_str()).unwrap_or("--ghc");
|
|
||||||
match Book::boot(".", arg) {
|
|
||||||
Ok(book) => {
|
|
||||||
let (infos, stderr) = get_infos(&book, cmd, arg, opt);
|
|
||||||
|
|
||||||
for info in &infos {
|
for info in &infos {
|
||||||
println!("{}", info.pretty(&book))
|
println!("{}", info.pretty(&book));
|
||||||
}
|
}
|
||||||
|
|
||||||
if stderr.is_empty() && infos.len() == 0 {
|
if stderr.is_empty() && infos.is_empty() {
|
||||||
println!("check!");
|
println!("check!");
|
||||||
}
|
}
|
||||||
|
|
||||||
// Prints stdout errors and stats.
|
eprintln!("{stderr}");
|
||||||
eprintln!("{}", stderr);
|
|
||||||
},
|
|
||||||
Err(e) => {
|
|
||||||
eprintln!("{}", e);
|
|
||||||
std::process::exit(1);
|
|
||||||
},
|
|
||||||
}
|
|
||||||
},
|
|
||||||
"compare" => {
|
|
||||||
test_runtime_compatibility();
|
|
||||||
}
|
|
||||||
_ => {
|
|
||||||
show_help();
|
|
||||||
},
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
//fn main() {
|
fn normal(name: &str, _level: u32, runtime: &str) {
|
||||||
//env::set_current_dir("./book").expect("Failed to change directory to ./book");
|
let book = load_book(name);
|
||||||
//let adt = term::sugar::adt::ADT::load("Vector");
|
let (infos, stderr) = run_kore(&book, "run", name, runtime);
|
||||||
//println!("{:?}", adt);
|
|
||||||
//}
|
|
||||||
|
|
||||||
fn show_help() {
|
for info in &infos {
|
||||||
eprintln!("Usage: kind2 [check|run] <name>");
|
println!("{}", info.pretty(&book));
|
||||||
eprintln!(" kind2 compare");
|
|
||||||
std::process::exit(1);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn test_runtime_compatibility() {
|
eprintln!("{stderr}");
|
||||||
use std::fs;
|
}
|
||||||
|
|
||||||
let q = env!("CARGO_MANIFEST_DIR").to_owned() + "/book/";
|
fn format_def(name: &str) {
|
||||||
let paths = fs::read_dir(&q).unwrap();
|
let book = load_book(name);
|
||||||
let mut paths: Vec<_> = paths.into_iter().map(|path| path.unwrap().path()).collect();
|
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 compile(name: &str) {
|
||||||
|
let book = load_book(name);
|
||||||
|
let code = generate_hvm2(&book, name);
|
||||||
|
println!("{code}");
|
||||||
|
}
|
||||||
|
|
||||||
|
fn compare_runtimes() {
|
||||||
|
let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book");
|
||||||
|
let mut paths: Vec<_> = fs::read_dir(&book_dir)
|
||||||
|
.expect("failed to read book directory")
|
||||||
|
.map(|r| r.expect("failed to read entry").path())
|
||||||
|
.collect();
|
||||||
paths.sort();
|
paths.sort();
|
||||||
|
|
||||||
for path in paths {
|
for path in paths {
|
||||||
let base = path.file_stem().unwrap().to_str().unwrap();
|
let name = path.file_stem().unwrap().to_str().unwrap();
|
||||||
let Ok(book) = Book::boot(&q, base) else {
|
|
||||||
|
let Some(book) = Book::boot(book_dir.to_str().unwrap(), name).ok() else {
|
||||||
continue;
|
continue;
|
||||||
};
|
};
|
||||||
print!("{:<30}: ", base);
|
|
||||||
for rt in ["--ghc", "--hvm2"] {
|
print!("{name:<30}: ");
|
||||||
let _ = std::io::stdout().flush();
|
|
||||||
let (infos, stderr) = get_infos(&book, "check", base, rt);
|
for rt in ["hs", "hvm2"] {
|
||||||
|
std::io::stdout().flush().expect("failed to flush stdout");
|
||||||
|
let (infos, stderr) = run_kore(&book, "check", name, rt);
|
||||||
if stderr.is_empty() {
|
if stderr.is_empty() {
|
||||||
if infos.len() == 0 {
|
if infos.is_empty() {
|
||||||
print!("\x1b[32;1m+\x1b[0m ");
|
print!("\x1b[32;1m+\x1b[0m ");
|
||||||
} else {
|
} else {
|
||||||
print!("\x1b[31;1m-\x1b[0m ");
|
print!("\x1b[31;1m-\x1b[0m ");
|
||||||
@ -198,6 +147,73 @@ fn test_runtime_compatibility() {
|
|||||||
print!("\x1b[33;1m*\x1b[0m ");
|
print!("\x1b[33;1m*\x1b[0m ");
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
println!();
|
println!();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn load_book(name: &str) -> Book {
|
||||||
|
let cwd = std::env::current_dir().expect("failed to get current directory");
|
||||||
|
Book::boot(cwd.to_str().unwrap(), name).unwrap_or_else(|e| {
|
||||||
|
eprintln!("{e}");
|
||||||
|
std::process::exit(1);
|
||||||
|
})
|
||||||
|
}
|
||||||
|
|
||||||
|
fn main() {
|
||||||
|
let matches = Command::new("kind2")
|
||||||
|
.about("The Kind2 Programming Language")
|
||||||
|
.subcommand_required(true)
|
||||||
|
.arg_required_else_help(true)
|
||||||
|
.subcommand(Command::new("check")
|
||||||
|
.about("Type-checks a term")
|
||||||
|
.arg(Arg::new("name").required(true))
|
||||||
|
.arg(Arg::new("runtime")
|
||||||
|
.long("use")
|
||||||
|
.value_parser(["hs", "hvm2"])
|
||||||
|
.default_value("hs")))
|
||||||
|
.subcommand(Command::new("normal")
|
||||||
|
.about("Normalizes a term")
|
||||||
|
.arg(Arg::new("name").required(true))
|
||||||
|
.arg(Arg::new("level")
|
||||||
|
.long("level")
|
||||||
|
.short('l')
|
||||||
|
.action(ArgAction::Set)
|
||||||
|
.value_parser(clap::value_parser!(u32)))
|
||||||
|
.arg(Arg::new("runtime")
|
||||||
|
.long("use")
|
||||||
|
.value_parser(["hs", "hvm2"])
|
||||||
|
.default_value("hs")))
|
||||||
|
.subcommand(Command::new("format")
|
||||||
|
.about("Pretty-formats a definition")
|
||||||
|
.arg(Arg::new("name").required(true)))
|
||||||
|
.subcommand(Command::new("compile")
|
||||||
|
.about("Compiles to HVM2")
|
||||||
|
.arg(Arg::new("name").required(true)))
|
||||||
|
.subcommand(Command::new("compare").about("Runs internal comparison tests"))
|
||||||
|
.get_matches();
|
||||||
|
|
||||||
|
match matches.subcommand() {
|
||||||
|
Some(("check", sub_matches)) => {
|
||||||
|
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||||
|
let runtime = sub_matches.get_one::<String>("runtime").expect("defaulted");
|
||||||
|
check(name, runtime);
|
||||||
|
}
|
||||||
|
Some(("normal", sub_matches)) => {
|
||||||
|
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||||
|
let level = sub_matches.get_one::<u32>("level").copied().unwrap_or(0);
|
||||||
|
let runtime = sub_matches.get_one::<String>("runtime").expect("defaulted");
|
||||||
|
normal(name, level, runtime);
|
||||||
|
}
|
||||||
|
Some(("format", sub_matches)) => {
|
||||||
|
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||||
|
format_def(name);
|
||||||
|
}
|
||||||
|
Some(("compile", sub_matches)) => {
|
||||||
|
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||||
|
compile(name);
|
||||||
|
}
|
||||||
|
Some(("compare", _)) => compare_runtimes(),
|
||||||
|
_ => unreachable!(),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
@ -1,5 +1,3 @@
|
|||||||
use crate::Term;
|
|
||||||
|
|
||||||
// Example:
|
// Example:
|
||||||
// ["(" "foo" "arg0" "arg1" "arg2" ")"]
|
// ["(" "foo" "arg0" "arg1" "arg2" ")"]
|
||||||
// Call:
|
// Call:
|
||||||
|
@ -81,7 +81,7 @@ impl Src {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn name(numb: usize) -> String {
|
fn _name(numb: usize) -> String {
|
||||||
let mut name = String::new();
|
let mut name = String::new();
|
||||||
let mut numb = numb as i64;
|
let mut numb = numb as i64;
|
||||||
loop {
|
loop {
|
||||||
|
Loading…
Reference in New Issue
Block a user