diff options
Diffstat (limited to 'src/main.rs')
| -rw-r--r-- | src/main.rs | 96 |
1 files changed, 53 insertions, 43 deletions
diff --git a/src/main.rs b/src/main.rs index 1925b41..2a8b274 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,59 +5,69 @@ mod checker_signature; mod checker_state; mod parser; +use std::env; +use std::fs; +use std::process; use tracing_subscriber::{layer::SubscriberExt, util::SubscriberInitExt}; use tracing_tree::HierarchicalLayer; fn main() { - tracing_subscriber::registry() - .with( - HierarchicalLayer::new(2) - .with_targets(false) - .with_bracketed_fields(true), - ) - .init(); + let args: Vec<String> = env::args().skip(1).collect(); - let src = r#" -// let signature Graph = theory { -// Vertex :: Set, -// Edge :: (s : set-of(Vertex)) (t : set-of(Vertex)) -> Set -// } + if args.is_empty() { + eprintln!("Usage: makkai [--debug] <file.makkai> [file.makkai ...]"); + process::exit(1); + } -// let set Empty = variant[] -// let set Unit = record{} -// let element pt : Unit = {} -// let set F1 = variant [ one0 : Unit ] -// let set F2 = variant [ two0 : Unit | two1 : Unit ] -// let set F3 = variant [ three0 : Unit | three1 : Unit | three2: Unit ] + let debug_mode = args.first().map_or(false, |arg| arg == "--debug"); -// let instance oneSimplex :: Graph = { -// .Vertex = F3 :: Set, -// .Edge = for (s : set-of(Vertex)) (t : set-of(Vertex)), -// case s of [ -// three0. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Unit :: Set | three2. pt => Unit :: Set ] -// | three1. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Unit :: Set ] -// | three2. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Empty :: Set ] -// ] -// } + if debug_mode { + tracing_subscriber::registry() + .with( + HierarchicalLayer::new(2) + .with_targets(false) + .with_bracketed_fields(true), + ) + .init(); + } -// let set OneSimplexEdges = record { -// source: set-of(oneSimplex .Vertex), -// target: set-of(oneSimplex .Vertex), -// connected: set-of(oneSimplex .Edge source target) -// } + let files: Vec<String> = if debug_mode { + args.into_iter().skip(1).collect() + } else { + args + }; -// let element vertex0 : F3 = three0. {} -// let element vertex1 : F3 = three1. {} -// let element edge01 : set-of(oneSimplex .Edge vertex0 vertex1) = pt + if files.is_empty() { + eprintln!("Usage: makkai [--debug] <file.makkai> [file.makkai ...]"); + process::exit(1); + } -let signature S = theory { - F :: (x : Nat) (y : Bool) -> Set, - G :: (z : set-of(F 3 5)) -> Set -} -"#; - let programme = parser::parse(src); + for file in files { + let src = match fs::read_to_string(&file) { + Ok(content) => content, + Err(e) => { + let msg = match e.kind() { + std::io::ErrorKind::NotFound => "file not found".to_string(), + _ => format!("io error: {}", e), + }; + eprintln!("{}: {}", file, msg); + process::exit(1); + } + }; + + let programme = match parser::parse_result(&src) { + Ok(p) => p, + Err(parse_err) => { + eprintln!("{}: Error\n\t{}", file, parse_err); + process::exit(1); + } + }; - if let Err(e) = programme.check() { - println!("{}", e); + if let Err(check_err) = programme.check() { + eprintln!("{} Error\n\t{}", file, check_err); + process::exit(1); + } else { + println!("{} Ok", file); + } } } |
