From 90e451893671ceebaa37fcb634b5d7a3f153ba70 Mon Sep 17 00:00:00 2001 From: tslil Date: Mon, 4 May 2026 17:52:04 +0100 Subject: almost done --- src/checker_signature.rs | 37 ++++++++++------ src/main.rs | 108 ++++++++++++++++++++++++++--------------------- src/parser.rs | 16 +++---- 3 files changed, 90 insertions(+), 71 deletions(-) (limited to 'src') diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 42a581f..30598d3 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -420,18 +420,9 @@ impl CheckerState { other => (other, args.clone()), }; - let subject_sig: Option = match &subject { - Instance::Var(v) => Some(self.lookup_instance(v)?.container.clone()), - Instance::Project { field, .. } => { - Some(self.lookup_signature_field(field)?.field.clone()) - } - // TODO: i think we need to handle case here - Instance::App { .. } - | Instance::Record(_) - | Instance::SetCoerce(_) - | Instance::For { .. } - | Instance::Case { .. } => None, - }; + // nevertheless we need the tiniest amount of bidirectionality + // here to deal with case, project, and var recursively + let subject_sig: Option = self.stuck_subject_signature(&subject)?; if let Some(subject_sig) = subject_sig { let Signature::Ext { params, codomain } = subject_sig else { @@ -497,7 +488,7 @@ impl CheckerState { }) } Instance::Case { .. } => { - todo!("App applied to a Case instance?"); + unreachable!("_stuck_subject_signature should have dealt with this") } Instance::Var(_) | Instance::Project { .. } => { unreachable!("handled in the stuck-head branch above") @@ -533,4 +524,24 @@ impl CheckerState { .collect::, _>>()?; Ok((ctx, checked)) } + + fn stuck_subject_signature(&self, inst: &Instance) -> Result, CheckerError> { + match inst { + Instance::Var(v) => Ok(Some(self.lookup_instance(v)?.container.clone())), + Instance::Project { field, .. } => { + Ok(Some(self.lookup_signature_field(field)?.field.clone())) + } + // All arms of a stuck Case share a signature by the case + // elimination typing rule, and we've already expanded the body, so + // we can pick any arm. + Instance::Case { arms, .. } => self + .stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body), + + Instance::For { .. } | Instance::Record(_) | Instance::SetCoerce(_) => Ok(None), + + Instance::App { .. } => unreachable!( + "invariant violation: _stuck_head_signature called on a left-nested App" + ), + } + } } 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 src = r#" -// let signature Graph = theory { -// Vertex :: Set, -// Edge :: (s : set-of(Vertex)) (t : set-of(Vertex)) -> Set -// } - -// 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 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 ] -// ] -// } - -// let set OneSimplexEdges = record { -// source: set-of(oneSimplex .Vertex), -// target: set-of(oneSimplex .Vertex), -// connected: set-of(oneSimplex .Edge source target) -// } - -// let element vertex0 : F3 = three0. {} -// let element vertex1 : F3 = three1. {} -// let element edge01 : set-of(oneSimplex .Edge vertex0 vertex1) = pt - -let signature S = theory { - F :: (x : Nat) (y : Bool) -> Set, - G :: (z : set-of(F 3 5)) -> Set -} -"#; - let programme = parser::parse(src); + let args: Vec = env::args().skip(1).collect(); + + if args.is_empty() { + eprintln!("Usage: makkai [--debug] [file.makkai ...]"); + process::exit(1); + } + + let debug_mode = args.first().map_or(false, |arg| arg == "--debug"); + + if debug_mode { + tracing_subscriber::registry() + .with( + HierarchicalLayer::new(2) + .with_targets(false) + .with_bracketed_fields(true), + ) + .init(); + } + + let files: Vec = if debug_mode { + args.into_iter().skip(1).collect() + } else { + args + }; + + if files.is_empty() { + eprintln!("Usage: makkai [--debug] [file.makkai ...]"); + process::exit(1); + } + + 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); + } } } diff --git a/src/parser.rs b/src/parser.rs index 285bb84..4e41644 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -269,23 +269,21 @@ parser! { } } -pub fn parse(src: &str) -> Programme { +pub fn parse_result(src: &str) -> Result { match parser::program(src) { - Ok(p) => { - println!("{}", p); - p - } + Ok(p) => Ok(p), Err(e) => { let line = e.location.line; let col = e.location.column; let off = e.location.offset; - println!("FAIL at {}:{} (offset {})", line, col, off); - println!("expected: {:#}", e.expected); let before = &src[off.saturating_sub(40)..off]; let after = &src[off..(off + 40).min(src.len())]; - println!("...{}⟨HERE⟩{}...", before, after); - panic!("Parse failed!"); + + Err(format!( + "FAIL at {}:{} (offset {})\nexpected: {:#?}\n...{}⟨HERE⟩{}...", + line, col, off, e.expected, before, after + )) } } } -- cgit v1.3.1