mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-08-15 18:20:26 +03:00
Add clap cli
This commit is contained in:
parent
182814b528
commit
9981cfbabc
1
Cargo.lock
generated
1
Cargo.lock
generated
@ -135,6 +135,7 @@ dependencies = [
|
||||
name = "kind2"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"hvm",
|
||||
]
|
||||
|
||||
|
@ -7,3 +7,4 @@ edition = "2021"
|
||||
|
||||
[dependencies]
|
||||
hvm = "0.1.38"
|
||||
clap = { version = "3.1.8", features = ["derive"] }
|
||||
|
20
src/cli.rs
Normal file
20
src/cli.rs
Normal file
@ -0,0 +1,20 @@
|
||||
pub use clap::{Parser, Subcommand};
|
||||
|
||||
#[derive(Parser)]
|
||||
#[clap(author, version, about, long_about = None)]
|
||||
#[clap(propagate_version = true)]
|
||||
pub struct Cli {
|
||||
#[clap(subcommand)]
|
||||
pub command: Command,
|
||||
}
|
||||
|
||||
#[derive(Subcommand)]
|
||||
pub enum Command {
|
||||
/// Run a file interpreted
|
||||
#[clap(aliases = &["r"])]
|
||||
Run { file: String, params: Vec<String> },
|
||||
|
||||
/// Check a file
|
||||
#[clap(aliases = &["c"])]
|
||||
Check { file: String, params: Vec<String> },
|
||||
}
|
60
src/main.rs
60
src/main.rs
@ -3,23 +3,47 @@
|
||||
|
||||
// TODO: type{} syntax
|
||||
|
||||
mod cli;
|
||||
|
||||
use std::collections::HashMap;
|
||||
use cli::{Cli, Command, Parser};
|
||||
use hvm::parser as parser;
|
||||
|
||||
fn main() -> Result<(), String> {
|
||||
gen();
|
||||
fn main() {
|
||||
match run_cli() {
|
||||
Ok(..) => {}
|
||||
Err(err) => {
|
||||
eprintln!("{}", err);
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
let args: Vec<String> = std::env::args().collect();
|
||||
fn gen() {
|
||||
let file = read_file(&DEMO_CODE).unwrap();
|
||||
let code = compile_file(&file);
|
||||
let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string();
|
||||
checker.push_str(&code);
|
||||
std::fs::write("tmp.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file
|
||||
}
|
||||
|
||||
if args.len() <= 2 || args[1] != "check" && args[1] != "run" {
|
||||
println!("Usage:");
|
||||
println!("$ kind2 check file.kind");
|
||||
println!("$ kind2 run file.kind");
|
||||
return Ok(());
|
||||
const CHECKER_HVM: &str = include_str!("checker.hvm");
|
||||
|
||||
fn run_cli() -> Result<(), String> {
|
||||
let cli_matches = Cli::parse();
|
||||
|
||||
match cli_matches.command {
|
||||
Command::Run { file: path, params } => {
|
||||
kind2(&path, "Api.run_main")
|
||||
}
|
||||
|
||||
Command::Check { file: path, params } => {
|
||||
kind2(&path, "Api.check_all")
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
let path = &args[2];
|
||||
let file = match std::fs::read_to_string(path) {
|
||||
fn kind2(path: &str, main_function: &str) -> Result<(), String> {
|
||||
let file = match std::fs::read_to_string(&path) {
|
||||
Ok(code) => read_file(&code),
|
||||
Err(msg) => read_file(&DEMO_CODE),
|
||||
};
|
||||
@ -39,25 +63,15 @@ fn main() -> Result<(), String> {
|
||||
std::fs::write(format!("{}.hvm", path), checker.clone()).ok(); // writes checker to the checker.hvm file
|
||||
|
||||
let mut rt = hvm::Runtime::from_code(&checker)?;
|
||||
let main = rt.alloc_code(if args[1] == "check" { "Api.check_all" } else { "Api.run_main" })?;
|
||||
let main = rt.alloc_code(main_function)?;
|
||||
rt.normalize(main);
|
||||
println!("{}", readback_string(&rt, main)); // TODO: optimize by deserializing term into text directly
|
||||
|
||||
println!("Rewrites: {}", rt.get_rewrites());
|
||||
eprintln!("Rewrites: {}", rt.get_rewrites());
|
||||
|
||||
return Ok(());
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn gen() {
|
||||
let file = read_file(&DEMO_CODE).unwrap();
|
||||
let code = compile_file(&file);
|
||||
let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string();
|
||||
checker.push_str(&code);
|
||||
std::fs::write("tmp.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file
|
||||
}
|
||||
|
||||
const CHECKER_HVM: &str = include_str!("checker.hvm");
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum Term {
|
||||
Typ,
|
||||
|
Loading…
Reference in New Issue
Block a user