use std::io::Read;
use std::process::ExitCode;
use clap::{CommandFactory, Parser, ValueEnum};
use elenchus_compiler::FileResolver;
use elenchus_solver::{Report, verify, verify_source};
#[derive(Parser)]
#[command(
name = "elenchus",
version,
about = "Check an elenchus .vrf program for logical consistency.",
long_about = "Reads a .vrf program (a file, inline --text, or explicit stdin \
with '-'), runs the engine, and prints the verdict. With a file, \
IMPORTs are resolved relative to it. Exit code: 0 consistent, 1 \
underdetermined/warnings, 2 conflicts."
)]
struct Cli {
file: Option<String>,
#[arg(long, conflicts_with = "file")]
text: Option<String>,
#[arg(long, value_enum, default_value_t = Format::Human)]
format: Format,
}
#[derive(Clone, Copy, ValueEnum)]
enum Format {
Human,
Json,
}
fn main() -> ExitCode {
let cli = Cli::parse();
if cli.text.is_none() && cli.file.is_none() {
eprintln!("elenchus: no input provided; pass a file, --text, or - for stdin\n");
let mut cmd = Cli::command();
let _ = cmd.print_help();
eprintln!();
return ExitCode::from(2);
}
let report = match build_report(&cli) {
Ok(r) => r,
Err(e) => {
eprintln!("elenchus: {e}");
return ExitCode::from(2);
}
};
match cli.format {
Format::Human => println!("{report}"),
Format::Json => println!("{}", report.to_json()),
}
ExitCode::from(report.exit_code() as u8)
}
fn build_report(cli: &Cli) -> Result<Report, String> {
if let Some(text) = &cli.text {
return verify_source("<text>", text).map_err(|e| e.to_string());
}
match cli.file.as_deref() {
Some(path) => {
if path == "-" {
let mut buf = String::new();
std::io::stdin()
.read_to_string(&mut buf)
.map_err(|e| format!("reading stdin: {e}"))?;
verify_source("<stdin>", &buf).map_err(|e| e.to_string())
} else {
verify(path, &FileResolver).map_err(|e| e.to_string())
}
}
None => Err("no input provided; pass a file, --text, or - for stdin".to_string()),
}
}