commit grammar, format code (macro sigh), add pretty printing of AST

5 files changed, 255 insertions, 116 deletions

diff --git a/Cargo.lock b/Cargo.lock
index f16c8c3..91b9000 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -3,9 +3,42 @@
 version = 4
 
 [[package]]
+name = "convert_case"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "633458d4ef8c78b72454de2d54fd6ab2e60f9e02be22f3c6104cdc8a4e0fceb9"
+dependencies = [
+ "unicode-segmentation",
+]
+
+[[package]]
+name = "derive_more"
+version = "2.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d751e9e49156b02b44f9c1815bcb94b984cdcc4396ecc32521c739452808b134"
+dependencies = [
+ "derive_more-impl",
+]
+
+[[package]]
+name = "derive_more-impl"
+version = "2.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "799a97264921d8623a957f6c3b9011f3b5492f557bbb7a5a19b7fa6d06ba8dcb"
+dependencies = [
+ "convert_case",
+ "proc-macro2",
+ "quote",
+ "rustc_version",
+ "syn",
+ "unicode-xid",
+]
+
+[[package]]
 name = "makkai"
 version = "0.1.0"
 dependencies = [
+ "derive_more",
  "peg",
 ]
 
@@ -55,7 +88,45 @@ dependencies = [
 ]
 
 [[package]]
+name = "rustc_version"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92"
+dependencies = [
+ "semver",
+]
+
+[[package]]
+name = "semver"
+version = "1.0.28"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
 name = "unicode-ident"
 version = "1.0.24"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "unicode-segmentation"
+version = "1.13.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9629274872b2bfaf8d66f5f15725007f635594914870f65218920345aa11aa8c"
+
+[[package]]
+name = "unicode-xid"
+version = "0.2.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
diff --git a/Cargo.toml b/Cargo.toml
index af01f42..9b54426 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -4,4 +4,5 @@ version = "0.1.0"
 edition = "2024"
 
 [dependencies]
+derive_more = { version = "2.1", features = ["display"] }
 peg = "0.8.5"
diff --git a/grammar.txt b/grammar.txt
new file mode 100644
index 0000000..34d8e1b
--- /dev/null
+++ b/grammar.txt
@@ -0,0 +1,63 @@
+program           = { declaration } ;
+
+declaration       = set_decl | element_decl | theory_decl | instance_decl ;
+
+set_decl          = "let set" , set_var , "=" , set ;
+element_decl      = "let element" , elem_var , ":" , set , "=" , element ;
+theory_decl       = "let signature" , sig_var , "=" , signature ;
+instance_decl     = "let instance" , inst_var , "::" , signature , "=" , instance ;
+
+set               = record_set | variant_set | builtin_set | claimed_set | set_var | "(" , set , ")" ;
+record_set        = "record" , "{" , [ set_field { "," , set_field } ] , "}" ;
+set_field         = "." , lower_ident , ":" , set ;
+variant_set       = "variant" , "{" , [ variant_field { "|" , variant_field } ] , "}" ;
+variant_field     = lower_ident , "." , ":" , set ;
+builtin_set       = "Nat" | "Int" | "Float" | "Str" | "Bool" ;
+claimed_set       = "set" , "(" , instance , ")" ;
+
+signature         = "Set" | theory_sig | function_sig | sig_var | "(" , signature , ")" ;
+theory_sig        = "theory" , "{" , [ sig_field { "," , sig_field } ] , "}" ;
+sig_field         = "." , upper_ident , "::" , signature ;
+function_sig      = param_list , "->" , signature ;
+param_list        = param { param } ;
+param             = "(" , elem_var , ":" , set , ")" ;
+
+element           = case_elem | app_elem ;
+case_elem         = "case" , element , "of" , "{" , [ case_arm { "|" , case_arm } ] , "}" ;
+case_arm          = inject_elem , elem_var , "=>" , element ;
+app_elem          = dot_elem { dot_elem } ;
+dot_elem          = { inject_elem } , atom_elem , { project_elem } ;
+inject_elem       = ident , "." ;
+project_elem      = "." , ident ;
+atom_elem         = literal | elem_var | record_elem | "(" , element , ")" ;
+record_elem       = "{" , [ elem_assign { "," , elem_assign } ] , "}" ;
+elem_assign       = project_elem , "=" , element ;
+
+instance          = for_inst | app_inst ;
+for_inst          = "for" , param_list , "," , instance ;
+app_inst          = dot_inst { dot_elem } ;
+dot_inst          = atom_inst { project_elem } ;
+atom_inst         = set | inst_var | record_inst | "(" , instance , ")" ;
+record_inst       = "{" , [ inst_assign { "," , inst_assign } ] , "}" ;
+inst_assign       = project_elem , "=" , instance ;
+
+literal           = nat_lit | int_lit | float_lit | str_lit | bool_lit ;
+nat_lit           = digit , { digit } ;
+int_lit           = "-" , digit , { digit } ;
+float_lit         = [ "-" ] , digit , { digit } , "." , digit , { digit } ;
+str_lit           = '"' , { any_character_except_quote } , '"' ;
+bool_lit          = "true" | "false" ;
+
+set_var           = upper_ident ;
+sig_var           = upper_ident ;
+elem_var          = lower_ident ;
+inst_var          = lower_ident ;
+
+upper_ident       = upper_case_letter , { ident_char } ;
+lower_ident       = lower_case_letter , { ident_char } ;
+ident             = (upper_case_letter | lower_case_letter) , { ident_char } ;
+
+upper_case_letter = "A"..."Z" ;
+lower_case_letter = "a"..."z" ;
+digit             = "0"..."9" ;
+ident_char        = upper_case_letter | lower_case_letter | digit | "_" | "'" ;
diff --git a/makkai.md b/makkai.md
index d08b2db..e24730b 100644
--- a/makkai.md
+++ b/makkai.md
@@ -24,30 +24,25 @@ For each `B ∈ { Nat, Int, Float, Str }`:
 ### Variables
 - `C ⊢ x : X` when `x : X` is in `C`.
 
-### Conjunction (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]`.
+### 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 { ... }`.
 
-### Disjunction (variants)
+### 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`.
+- **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
 
 ### 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]`.
+- **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 { ... }`.
diff --git a/src/parser.rs b/src/parser.rs
index 1af9d49..a0da79c 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -1,8 +1,9 @@
+use derive_more::Display;
 use peg::parser;
 
 // Set layer
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
 pub enum BuiltIn {
     Nat,
     Int,
@@ -11,55 +12,68 @@ pub enum BuiltIn {
     Bool,
 }
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} : {set}")]
 pub struct SetField {
     pub name: String,
     pub set: Set,
-} // .x : X
+}
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display("{name}. : {set}")]
 pub struct VariantField {
     pub name: String,
     pub set: Set,
-} // x. : X
+}
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
 pub enum Set {
+    #[display("{_0}")]
     BuiltIn(BuiltIn),
+    #[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
     Record(Vec<SetField>),
+    #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
     Variant(Vec<VariantField>),
+    #[display("set({_0})")]
     ClaimedSet(Instance),
+    #[display("{_0}")]
     Var(String),
 }
 
 // Signature layer
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display("({name} : {set})")]
 pub struct Param {
     pub name: String,
     pub set: Set,
-} // (x : X)
+}
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} :: {signature}")]
 pub struct SigField {
     pub name: String,
     pub signature: Signature,
-} // .s :: S
+}
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
 pub enum Signature {
+    #[display("Set")]
     Set,
+    #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
     Theory(Vec<SigField>),
+    #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(", "), codomain)]
     Ext {
         params: Vec<Param>,
         codomain: Box<Signature>,
-    }, // (x:X)(y:Y) -> S
+    },
+    #[display("{_0}")]
     Var(String),
 }
 
 // Element layer
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
 pub enum Literal {
     Nat(u64),
     Int(i64),
@@ -68,27 +82,36 @@ pub enum Literal {
     Bool(bool),
 }
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} = {element}")]
 pub struct ElemAssign {
     pub name: String,
     pub element: Element,
-} // .x = m
+}
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{tag} {bound} => {body}")]
 pub struct CaseArm {
     pub tag: String,
     pub bound: String,
     pub body: Element,
-} // v. x => n
+}
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
 pub enum Element {
+    #[display("{_0}")]
     Literal(Literal),
+    #[display("{_0}")]
     Var(String),
+    #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
     Record(Vec<ElemAssign>),
-    Project(Box<Element>, String),   // m .x
-    Inject(String, Box<Element>),    // v. m
-    App(Box<Element>, Box<Element>), // f x
+    #[display("{_0} .{_1}")]
+    Project(Box<Element>, String),
+    #[display("{_0}. {_1}")]
+    Inject(String, Box<Element>),
+    #[display("{_0} {_1}")]
+    App(Box<Element>, Box<Element>),
+    #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
     Case {
         scrutinee: Box<Element>,
         arms: Vec<CaseArm>,
@@ -97,41 +120,47 @@ pub enum Element {
 
 // Instance layer
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} = {instance}")]
 pub struct InstAssign {
     pub name: String,
     pub instance: Instance,
-} // .s = I
+}
 
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, PartialEq, Display)]
 pub enum Instance {
-    SetCoerce(Box<Set>), // X :: Set
+    #[display("{_0}")]
+    SetCoerce(Box<Set>),
+    #[display("{_0}")]
     Var(String),
+    #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(", "))]
     Record(Vec<InstAssign>),
+    #[display("for {}, {body}", params.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(""))]
     For {
         params: Vec<Param>,
         body: Box<Instance>,
-    }, // for (x:X), I
-    App(Box<Instance>, Box<Element>), // I m
-    Project(Box<Instance>, String),   // I .s
+    },
+    #[display("{_0} {_1}")]
+    App(Box<Instance>, Box<Element>),
+    #[display("{_0} .{_1}")]
+    Project(Box<Instance>, String),
 }
 
 // Declarations
-#[derive(Clone, Debug, PartialEq)]
+
+#[derive(Clone, Debug, PartialEq, Display)]
 pub enum Decl {
-    Set {
-        name: String,
-        set: Set,
-    },
+    #[display("let set {name} = {set}")]
+    Set { name: String, set: Set },
+    #[display("let element {name} : {set} = {element}")]
     Element {
         name: String,
         set: Set,
         element: Element,
     },
-    Signature {
-        name: String,
-        signature: Signature,
-    },
+    #[display("let signature {name} = {signature}")]
+    Signature { name: String, signature: Signature },
+    #[display("let instance {name} :: {signature} = {instance}")]
     Instance {
         name: String,
         signature: Signature,
@@ -139,7 +168,9 @@ pub enum Decl {
     },
 }
 
-pub type Program = Vec<Decl>;
+#[derive(Display)]
+#[display("{}", _0.iter().map(|d| d.to_string()).collect::<Vec<_>>().join("\n"))]
+pub struct Programme(Vec<Decl>);
 
 parser! {
     pub grammar parser() for str {
@@ -153,26 +184,26 @@ parser! {
 
         // keywords
 
-        rule kw_let_set()      = "let set"      wb()
-        rule kw_let_element()  = "let element"  wb()
-        rule kw_let_theory()   = "let theory"   wb()
-        rule kw_let_instance() = "let instance" wb()
-        rule kw_record()   = "record"   wb()
-        rule kw_variant()  = "variant"  wb()
-        rule kw_theory()   = "theory"   wb()
-        rule kw_case()     = "case"     wb()
-        rule kw_of()       = "of"       wb()
-        rule kw_for()      = "for"      wb()
-        rule kw_set()      = "set"      wb()
-        rule kw_Set()      = "Set"      wb()
-        rule kw_Nat()      = "Nat"      wb()
-        rule kw_Int()      = "Int"      wb()
-        rule kw_Float()    = "Float"    wb()
-        rule kw_Str()      = "Str"      wb()
-        rule kw_Bool()     = "Bool"     wb()
+        rule kw_let_set()       = "let set"       wb()
+        rule kw_let_element()   = "let element"   wb()
+        rule kw_let_signature() = "let signature" wb()
+        rule kw_let_instance()  = "let instance"  wb()
+        rule kw_record()        = "record"        wb()
+        rule kw_variant()       = "variant"       wb()
+        rule kw_theory()        = "theory"        wb()
+        rule kw_case()          = "case"          wb()
+        rule kw_of()            = "of"            wb()
+        rule kw_for()           = "for"           wb()
+        rule kw_set()           = "set"           wb()
+        rule kw_Set()           = "Set"           wb()
+        rule kw_Nat()           = "Nat"           wb()
+        rule kw_Int()           = "Int"           wb()
+        rule kw_Float()         = "Float"         wb()
+        rule kw_Str()           = "Str"           wb()
+        rule kw_Bool()          = "Bool"          wb()
 
         rule keyword() =
-        kw_let_set() / kw_let_element() / kw_let_theory() / kw_let_instance()
+        kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance()
         / kw_record()  / kw_variant()     / kw_theory()
         / kw_case()    / kw_of()          / kw_for()
         / kw_Set() / kw_set()
@@ -242,63 +273,52 @@ parser! {
         // set layer
 
         rule set_field() -> SetField
-        = n:project_lower() _ ":" _ s:set()
-        { SetField { name: n, set: s } }
+        = n:project_lower() _ ":" _ s:set() { SetField { name: n, set: s } }
 
         rule variant_field() -> VariantField
-        = n:inject_lower() _ ":" _ s:set() _
-        { VariantField { name: n, set: s } }
+        = n:inject_lower() _ ":" _ s:set() _ { VariantField { name: n, set: s } }
 
         rule claimed_set() -> Instance
-        = kw_set() "(" _ i:instance() _ ")" {i}
+        = kw_set() "(" _ i:instance() _ ")" { i }
 
         pub rule set() -> Set
-        = kw_record()  _ "{" fs:(set_field() ** ",") _ "}"
-        { Set::Record(fs) }
-        / kw_variant() _ "{" _ vs:(variant_field() ** "|") "}"
-        { Set::Variant(vs) }
+        = kw_record()  _ "{" fs:(set_field() ** ",") _ "}" { Set::Record(fs) }
+        / kw_variant() _ "{" _ vs:(variant_field() ** "|") "}" { Set::Variant(vs) }
         / b:builtin() { Set::BuiltIn(b) }
         / i:claimed_set() { Set::ClaimedSet(i) }
         / v:set_var() { Set::Var(v) }
         / "(" _ s:set() _ ")" { s }
+
         // signature layer
 
         rule param() -> Param
-        = "(" _ n:elem_var() _ ":" _ s:set() _ ")"
-        { Param { name: n, set: s } }
+        = "(" _ n:elem_var() _ ":" _ s:set() _ ")" { Param { name: n, set: s } }
 
         rule param_list() -> Vec<Param> = param() ++ _
 
         rule sig_field() -> SigField
-        = n:project_upper() _ "::" _ s:signature()
-        { SigField { name: n, signature: s } }
+        = n:project_upper() _ "::" _ s:signature() { SigField { name: n, signature: s } }
 
         pub rule signature() -> Signature
         = kw_Set()    { Signature::Set }
-        / kw_theory() _ "{" fs:(sig_field() ** ",") _ ","? _ "}"
-        { Signature::Theory(fs) }
-        / ps:param_list() _ "->" _ cod:signature()
-        { Signature::Ext { params: ps, codomain: Box::new(cod) } }
+        / kw_theory() _ "{" fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) }
+        / ps:param_list() _ "->" _ cod:signature() { Signature::Ext { params: ps, codomain: Box::new(cod) } }
         / v:sig_var() { Signature::Var(v) }
         / "(" _ s:signature() _ ")" { s }
 
         // element layer
 
         rule elem_assign() -> ElemAssign
-        = n:project() _ "=" _ e:element()
-        { ElemAssign { name: n, element: e } }
+        = n:project() _ "=" _ e:element() { ElemAssign { name: n, element: e } }
 
         rule atom_elem() -> Element
         = l:literal() { Element::Literal(l) }
         / v:elem_var() { Element::Var(v) }
-        / "{" fs:(elem_assign() ** ",") _ ","? _ "}"
-        { Element::Record(fs) }
+        / "{" fs:(elem_assign() ** ",") _ "}" { Element::Record(fs) }
         / "(" _ e:element() _ ")" { e }
 
         rule dot_elem() -> Element
-        = tags:(t:inject() _ { t })*
-        head:atom_elem()
-        projs:(p:project() { p })*
+        = tags:(t:inject() _ { t })* head:atom_elem() projs:(p:project() { p })*
         {
             let base = projs.into_iter().fold(head, |acc, p| {
                 Element::Project(Box::new(acc), p)
@@ -317,15 +337,10 @@ parser! {
         }
 
         rule case_arm() -> CaseArm
-        = t:inject() _ x:elem_var() _ "=>" _ body:element()
-        { CaseArm { tag: t, bound: x, body } }
+        = t:inject() _ x:elem_var() _ "=>" _ body:element() { CaseArm { tag: t, bound: x, body } }
 
         pub rule element() -> Element
-        = kw_case() __ scrut:element() _ kw_of() _ "{"
-        arms:(_ a:case_arm() _ { a }) ** "|"
-        _ "|"?
-        _ "}"
-        { Element::Case { scrutinee: Box::new(scrut), arms } }
+        = kw_case() __ scrut:element() _ kw_of() _ "{" arms:(_ a:case_arm() _ { a }) ** "|"  _ "}" { Element::Case { scrutinee: Box::new(scrut), arms } }
         / app_elem()
 
         // instance layer
@@ -337,8 +352,7 @@ parser! {
         rule atom_inst() -> Instance
         = s:set() { Instance::SetCoerce(Box::new(s)) }
         / v:inst_var() { Instance::Var(v) }
-        / "{" fs:(inst_assign() ** ",") _ ","? _ "}"
-        { Instance::Record(fs) }
+        / "{" fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) }
         / "(" _ i:instance() _ ")" { i }
 
         rule dot_inst() -> Instance
@@ -358,24 +372,19 @@ parser! {
         }
 
         pub rule instance() -> Instance
-        = kw_for() __ ps:param_list() _ "," _ body:instance()
-        { Instance::For { params: ps, body: Box::new(body) } }
+        = kw_for() __ ps:param_list() _ "," _ body:instance() { Instance::For { params: ps, body: Box::new(body) } }
         / app_inst()
 
         // declarations
 
         rule decl() -> Decl
-        = kw_let_set() __ n:set_var() _ "=" _ s:set()
-        { Decl::Set { name: n, set: s } }
-        / kw_let_element() __ n:elem_var() _ ":" _ s:set() _ "=" _ e:element()
-        { Decl::Element { name: n, set: s, element: e } }
-        / kw_let_theory() __ n:sig_var() _ "=" _ sg:signature()
-        { Decl::Signature { name: n, signature: sg } }
-        / kw_let_instance() __ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance()
-        { Decl::Instance { name: n, signature: sg, instance: i } }
+        = kw_let_set() __ n:set_var() _ "=" _ s:set() { Decl::Set { name: n, set: s } }
+        / kw_let_element() __ n:elem_var() _ ":" _ s:set() _ "=" _ e:element() { Decl::Element { name: n, set: s, element: e } }
+        / kw_let_signature() __ n:sig_var() _ "=" _ sg:signature() { Decl::Signature { name: n, signature: sg } }
+        / kw_let_instance() __ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance() { Decl::Instance { name: n, signature: sg, instance: i } }
 
-        pub rule program() -> Program
-        = _ ds:(decl() ** _) _ { ds }
+        pub rule program() -> Programme
+        = _ ds:(decl() ** _) _ { Programme(ds) }
     }
 }
 
@@ -385,7 +394,7 @@ mod tests {
 
     fn debug_parse(src: &str) {
         match parser::program(src) {
-            Ok(p) => println!("```{}\n```\n=> {:?}\n", src, p),
+            Ok(p) => println!("```{}\n```\n=>\n{}\n", src, p),
             Err(e) => {
                 let line = e.location.line;
                 let col = e.location.column;
@@ -437,9 +446,9 @@ let set Maybe = variant {
     #[test]
     fn test_theories_and_instances() {
         let src = r#"
-            let theory Graph = theory {
+            let signature Graph = theory {
                 .Node :: Set,
-                .Edge :: (s : Node) (t : Node) -> Set,
+                .Edge :: (s : Node) (t : Node) -> Set
             }
 
             let instance loop :: Graph = {