almost done

3 files changed, 84 insertions, 65 deletions

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<Signature> = 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<Signature> = 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::<Result<Vec<_>, _>>()?;
         Ok((ctx, checked))
     }
+
+    fn stuck_subject_signature(&self, inst: &Instance) -> Result<Option<Signature>, 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 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);
+        }
     }
 }
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<Programme, String> {
     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
+            ))
         }
     }
 }