almost done

7 files changed, 186 insertions, 102 deletions

diff --git a/README.md b/README.md
index fafec00..a6cf033 100644
--- a/README.md
+++ b/README.md
@@ -2,7 +2,9 @@
 
 A simple type theory.
 
-## Judgements
+## Type Theory
+
+### Judgements
 - `C ctx` means `C` is a context.
 - `C ⊢ X set` means `X` is a set in context `C`.
 - `C ⊢ m : X` means `m` is a match of set `X`.
@@ -16,57 +18,71 @@ Contexts are built by extension with either kind of binding:
 
 Everywhere below, `...` ranges over a finite (possibly zero) index, and the labels `xi`, `si`, `vi` are assumed distinct within any single list.
 
-## The set layer
+### The set layer
 
-### Built-Ins
+#### Built-Ins
 For each `B ∈ { Nat, Int, Float, Str }`:
 - **Formation.** `C ⊢ B set`.
 - **Intro.** Literals of the appropriate form match the corresponding built-in (e.g. `C ⊢ 7 : Nat`).
 
-### Variables
+#### Variables
 - `C ⊢ x : X` when `x : X` is in `C`.
 
-### Records
-- **Formation.** `C ⊢ record { .x0 : X0, ..., .xn : Xn } set` when `C ⊢ X0 set`, `C, x0 : X0 ⊢ X1 set`, ..., `C, x0 : X0, ..., xn-1 : Xn-1 ⊢ Xn set`.
-- **Intro.** `C ⊢ { .x0 = m0, ..., .xn = mn } : record { .x0 : X0, ..., .xn : Xn }` when `C ⊢ m0 : X0`, `C ⊢ m1 : X1[m0/x0]`, ..., `C ⊢ mn : Xn[m0/x0, ..., mn-1/xn-1]`.
-- **Elim.** `C ⊢ m.xi : Xi[m.x0/x0, ..., m.xi-1/xi-1]` when `C ⊢ m : record { .x0 : X0, ..., .xn : Xn }`.
-- **β.** `{ ..., .xi = mi, ... }.xi=mi`.
-- **η.** `m=record { .x0=m.x0, ..., .xn=m.xn }` when `m : record { ... }`.
+#### Records
+- **Formation.** `C ⊢ record { x0 : X0, ..., xn : Xn } set` when `C ⊢ X0 set`, `C, x0 : X0 ⊢ X1 set`, ..., `C, x0 : X0, ..., xn-1 : Xn-1 ⊢ Xn set`.
+- **Intro.** `C ⊢ { x0 = m0, ..., xn = mn } : record { x0 : X0, ..., xn : Xn }` when `C ⊢ m0 : X0`, `C ⊢ m1 : X1[m0/x0]`, ..., `C ⊢ mn : Xn[m0/x0, ..., mn-1/xn-1]`.
+- **Elim.** `C ⊢ m.xi : Xi[(m .x0)/x0, ..., (m .xi-1)/xi-1]` when `C ⊢ m : record { x0 : X0, ..., xn : Xn }`.
+- **β.** `{ ..., xi = mi, ... } .xi=mi`.
+- **η.** `m=record { x0=m .x0, ..., xn=m .xn }` when `m : record { ... }`.
 
-### Variants
-- **Formation.** `C ⊢ variant { v0. : X0 | ... | vn. : Xn } set` when each `C ⊢ Xi set`.
-- **Intro.** `C ⊢ vi.(m) : variant { v0. : X0 | ... | vn. : Xn }` when `C ⊢ m : Xi`.
-- **Elim.** `C ⊢ case m of { v0.x0 => n0 | ... | vn.xn => nn } : X` when `C ⊢ m : variant { v0. : X0 | ... | vn. : Xn }` and, for each `i`, `C, xi : Xi ⊢ ni : X`.
-- **β.** `case vi.(m) of { ... | vi.xi => ni | ... }=ni[m/xi]`.
-- **η.** `m=case m of { v0.x0 => v0.(x0) | ... | vn.xn => vn.(xn) }` when `m : variant { ... }`.
+#### Variants
+- **Formation.** `C ⊢ variant { v0 : X0 | ... | vn : Xn } set` when each `C ⊢ Xi set`.
+- **Intro.** `C ⊢ vi. m : variant { v0 : X0 | ... | vn : Xn }` when `C ⊢ m : Xi`.
+- **Elim.** `C ⊢ case m of { v0. x0 => n0 | ... | vn. xn => nn } : X` when `C ⊢ m : variant { v0 : X0 | ... | vn : Xn }` and, for each `i`, `C, xi : Xi ⊢ ni : X`.
+- **β.** `case vi. m of { ... | vi. xi => ni | ... }=ni[m/xi]`.
+- **η.** `m=case m of { v0. x0 => v0. x0 | ... | vn. xn => vn. xn }` when `m : variant { ... }`.
 
-## The signature layer
+### The signature layer
 
-### Theory
-- **Formation.** `C ⊢ theory { .s0 :: S0, ..., .sn :: Sn } signature` when `C ⊢ S0 signature`, `C, s0 :: S0 ⊢ S1 signature`, ..., `C, s0 :: S0, ..., sn-1 :: Sn-1 ⊢ Sn signature`.
-- **Intro.** `C ⊢ { .s0 = I0, ..., .sn = In } :: theory { .s0 :: S0, ..., .sn :: Sn }` when `C ⊢ I0 :: S0`, `C ⊢ I1 :: S1[I0/s0]`, ..., `C ⊢ In :: Sn[I0/s0, ..., In-1/sn-1]`.
-- **Elim.** `C ⊢ I.si :: Si[I.s0/s0, ..., I.si-1/si-1]` when `C ⊢ I :: theory { .s0 :: S0, ..., .sn :: Sn }`.
-- **β.** `{ ..., .si=Ii, ... }.si=Ii`.
-- **η.** `I={ .s0=I.s0, ..., .sn=I.sn }` when `I :: theory { ... }`.
+#### Theory
+- **Formation.** `C ⊢ theory { s0 :: S0, ..., sn :: Sn } signature` when `C ⊢ S0 signature`, `C, s0 :: S0 ⊢ S1 signature`, ..., `C, s0 :: S0, ..., sn-1 :: Sn-1 ⊢ Sn signature`.
+- **Intro.** `C ⊢ { s0 = I0, ..., sn = In } :: theory { s0 :: S0, ..., sn :: Sn }` when `C ⊢ I0 :: S0`, `C ⊢ I1 :: S1[I0/s0]`, ..., `C ⊢ In :: Sn[I0/s0, ..., In-1/sn-1]`.
+- **Elim.** `C ⊢ I .si :: Si[(I .s0)/s0, ..., (I .si-1)/si-1]` when `C ⊢ I :: theory { s0 :: S0, ..., sn :: Sn }`.
+- **β.** `{ ..., si=Ii, ... } .si=Ii`.
+- **η.** `I={ s0=I .s0, ..., sn=I .sn }` when `I :: theory { ... }`.
 
-### Variables
+#### Variables
 - `C ⊢ i :: S` when `i :: S` is in `C`.
 
-## The interface between signatures and sets
+### The interface between signatures and sets
 
-### The signature `Set`
+#### The signature `Set`
 - **Formation.** `C ⊢ Set signature`.
 - **Intro.** `C ⊢ X :: Set` when `C ⊢ X set`.
 - **Elim.** `C ⊢ set-of(I) set` when `C ⊢ I :: Set`.
 - **β.** `set-of(X)=X` when `X :: Set` arises from `C ⊢ X set`.
 - **η.** `I=set-of(I)` viewed as an instance, when `I :: Set`.
 
-### Extension signatures
+#### Extension signatures
 - **Formation.** `C ⊢ (x: X) -> S signature` when `C ⊢ X set` and `C, x : X ⊢ S signature`.
 - **Intro.** `C ⊢ for (y: X). I :: (x: X) -> S` when `C, y : X ⊢ I :: S[y/x]`.
 - **β.** `(for (x: X). I)(y)=I[y/x]`.
 - **η.** `I=for (x: X). I(x)` when x is not free in I.
 
+#### Instances via case analysis
+A construction admitting an instance of any signature, given an element of a variant set and a branch for every tag.
+- **Intro.** `C ⊢ case m of { v0. x0 => I0 | ... | vn. xn => In } :: S` when `C ⊢ S signature`, `C ⊢ m : variant { v0. : X0 | ... | vn. : Xn }`, and, for each `i`, `C, xi : Xi ⊢ Ii :: S`.
+- **β.** `case vi. m of { ... | vi. xi => Ii | ... }=Ii[m/xi]`.
+
+
+## Rust implementation
+
+Usage `makkai [--debug] file1.makkai ... fileN.makkai`
+
+See the [grammar](grammar.txt) for details, and the examples in `examples/`.
+
+Note: the checker does not presently support η-equivalence in all cases.
+
 # License
 
 Copyright tslil clingman 2026, this programme is free software and is made available under the terms of the GPL v3 or later. See LICENSE for details.
diff --git a/examples/one_simplex.makkai b/examples/one_simplex.makkai
new file mode 100644
index 0000000..590cf04
--- /dev/null
+++ b/examples/one_simplex.makkai
@@ -0,0 +1,31 @@
+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
diff --git a/examples/signature_param.makkai b/examples/signature_param.makkai
new file mode 100644
index 0000000..9dae31b
--- /dev/null
+++ b/examples/signature_param.makkai
@@ -0,0 +1,4 @@
+let signature S = theory {
+  F :: (x : Nat) (y : Bool) -> Set,
+  G :: (z : set-of(F 3 4)) -> Set // this sould fail
+}
diff --git a/grammar.txt b/grammar.txt
index 9772501..e180bb0 100644
--- a/grammar.txt
+++ b/grammar.txt
@@ -7,6 +7,7 @@ element_decl      = "let element" , elem_var , ":" , set , "=" , element ;
 theory_decl       = "let signature" , sig_var , "=" , signature ;
 instance_decl     = "let instance" , inst_var , "::" , signature , "=" , instance ;
 
+(* Sets *)
 set               = record_set | variant_set | builtin_set | claimed_set | set_var | "(" , set , ")" ;
 record_set        = "record" , "{" , [ set_field { "," , set_field } ] , "}" ;
 set_field         = lower_ident , ":" , set ;
@@ -15,31 +16,40 @@ variant_field     = lower_ident , ":" , set ;
 builtin_set       = "Nat" | "Int" | "Float" | "Str" | "Bool" ;
 claimed_set       = "set-of" , "(" , instance , ")" ;
 
+(* Signatures *)
 signature         = "Set" | theory_sig | function_sig | sig_var | "(" , signature , ")" ;
 theory_sig        = "theory" , "{" , [ sig_field { "," , sig_field } ] , "}" ;
-sig_field         = "." , upper_ident , "::" , signature ;
+sig_field         = upper_ident , "::" , signature ;
 function_sig      = param_list , "->" , signature ;
 param_list        = param { param } ;
 param             = "(" , elem_var , ":" , set , ")" ;
 
+(* Elements *)
 element           = case_elem | dot_elem ;
-case_elem         = "case" , element , "of" , "{" , [ case_arm { "|" , case_arm } ] , "}" ;
-case_arm          = inject_elem , elem_var , "=>" , element ;
+case_elem         = "case" , element , "of" , "[" , [ elem_case_arm { "|" , elem_case_arm } ] , "]" ;
+elem_case_arm     = inject_elem , elem_var , "=>" , element ;
 dot_elem          = { inject_elem } , atom_elem , { project_elem } ;
 inject_elem       = ident , "." ;
 project_elem      = "." , ident ;
-atom_elem         = literal | elem_var | record_elem | "(" , element , ")" ;
+atom_elem         = literal | record_elem | "(" , element , ")" | elem_var ;
 record_elem       = "{" , [ elem_assign { "," , elem_assign } ] , "}" ;
-elem_assign       = project_elem , "=" , element ;
+elem_assign       = elem_field_label , "=" , element ;
+elem_field_label  = "." , lower_ident ;
 
-instance          = for_inst | app_inst ;
+(* Instances *)
+instance          = for_inst | case_inst | app_inst ;
 for_inst          = "for" , param_list , "," , instance ;
-app_inst          = dot_inst { dot_elem } ;
-dot_inst          = atom_inst { project_elem } ;
-atom_inst         = set ":: Set" | inst_var | record_inst | "(" , instance , ")" ;
+case_inst         = "case" , element , "of" , "[" , [ inst_case_arm { "|" , inst_case_arm } ] , "]" ;
+inst_case_arm     = inject_elem , elem_var , "=>" , instance ;
+app_inst          = dot_inst , { dot_elem } ;
+dot_inst          = atom_inst , { project_elem } ;
+atom_inst         = set_coerce | inst_var | sig_var | record_inst | "(" , instance , ")" ;
+set_coerce        = set , "::" , "Set" ;
 record_inst       = "{" , [ inst_assign { "," , inst_assign } ] , "}" ;
-inst_assign       = project_elem , "=" , instance ;
+inst_assign       = inst_field_label , "=" , instance ;
+inst_field_label  = "." , upper_ident ;
 
+(* Literals *)
 literal           = nat_lit | int_lit | float_lit | str_lit | bool_lit ;
 nat_lit           = digit , { digit } ;
 int_lit           = "-" , digit , { digit } ;
@@ -47,6 +57,7 @@ float_lit         = [ "-" ] , digit , { digit } , "." , digit , { digit } ;
 str_lit           = '"' , { any_character_except_quote } , '"' ;
 bool_lit          = "true" | "false" ;
 
+(* Identifiers *)
 set_var           = upper_ident ;
 sig_var           = upper_ident ;
 elem_var          = lower_ident ;
@@ -60,3 +71,6 @@ upper_case_letter = "A"..."Z" ;
 lower_case_letter = "a"..."z" ;
 digit             = "0"..."9" ;
 ident_char        = upper_case_letter | lower_case_letter | digit | "_" | "'" ;
+
+(* Lexical *)
+comment           = "//" , { any_character_except_newline } , ( newline | end_of_input ) ;
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
+            ))
         }
     }
 }