working on fixing app, rework ast to have generics etc

6 files changed, 249 insertions, 236 deletions

diff --git a/src/ast.rs b/src/ast.rs
index fab1236..76b6c9f 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -1,28 +1,35 @@
 use derive_more::Display;
 
-// Set layer
+// Generic
+
+pub trait TypingSignifier {
+    const SIGNIFIER: &'static str;
+}
 
 #[derive(Clone, PartialEq, Display, Debug)]
-pub enum BuiltIn {
-    Nat,
-    Int,
-    Float,
-    Str,
-    Bool,
+#[display(".{tag} {bound} => {body}")]
+pub struct CaseArm<T: std::fmt::Display> {
+    pub tag: String,
+    pub bound: String,
+    pub body: T,
 }
 
 #[derive(Clone, PartialEq, Display, Debug)]
-#[display("{name} : {set}")]
-pub struct RecordField {
+#[display("{name} {} {carries}", T::SIGNIFIER)]
+pub struct Field<T: std::fmt::Display + TypingSignifier> {
     pub name: String,
-    pub set: Set,
+    pub carries: T,
 }
 
+// Set layer
+
 #[derive(Clone, PartialEq, Display, Debug)]
-#[display("{name} : {set}")]
-pub struct VariantField {
-    pub name: String,
-    pub set: Set,
+pub enum BuiltIn {
+    Nat,
+    Int,
+    Float,
+    Str,
+    Bool,
 }
 
 #[derive(Clone, PartialEq, Display, Debug)]
@@ -31,10 +38,10 @@ pub enum Set {
     BuiltIn(BuiltIn),
 
     #[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
-    Record(Vec<RecordField>),
+    Record(Vec<Field<Set>>),
 
     #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
-    Variant(Vec<VariantField>),
+    Variant(Vec<Field<Set>>),
 
     #[display("set-of({_0})")]
     ClaimedSet(Instance),
@@ -43,6 +50,10 @@ pub enum Set {
     Var(String),
 }
 
+impl TypingSignifier for Set {
+    const SIGNIFIER: &'static str = ":";
+}
+
 // Signature layer
 
 #[derive(Clone, PartialEq, Display, Debug)]
@@ -53,19 +64,12 @@ pub struct Param {
 }
 
 #[derive(Clone, PartialEq, Display, Debug)]
-#[display("{name} :: {signature}")]
-pub struct SigField {
-    pub name: String,
-    pub signature: Signature,
-}
-
-#[derive(Clone, PartialEq, Display, Debug)]
 pub enum Signature {
     #[display("Set")]
     Set,
 
     #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
-    Theory(Vec<SigField>),
+    Theory(Vec<Field<Signature>>),
 
     #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(", "), codomain)]
     Ext {
@@ -77,6 +81,10 @@ pub enum Signature {
     Var(String),
 }
 
+impl TypingSignifier for Signature {
+    const SIGNIFIER: &'static str = "::";
+}
+
 // Element layer
 
 #[derive(Clone, PartialEq, Display, Debug)]
@@ -96,14 +104,6 @@ pub struct ElemAssign {
 }
 
 #[derive(Clone, PartialEq, Display, Debug)]
-#[display(".{tag} {bound} => {body}")]
-pub struct CaseArm {
-    pub tag: String,
-    pub bound: String,
-    pub body: Element,
-}
-
-#[derive(Clone, PartialEq, Display, Debug)]
 pub enum Element {
     #[display("{_0}")]
     Literal(Literal),
@@ -129,7 +129,7 @@ pub enum Element {
     #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
     Case {
         scrutinee: Box<Element>,
-        arms: Vec<CaseArm>,
+        arms: Vec<CaseArm<Element>>,
     },
 }
 
@@ -143,14 +143,6 @@ pub struct InstAssign {
 }
 
 #[derive(Clone, PartialEq, Display, Debug)]
-#[display(".{tag} {bound} => {body}")]
-pub struct InstCaseArm {
-    pub tag: String,
-    pub bound: String,
-    pub body: Instance,
-}
-
-#[derive(Clone, PartialEq, Display, Debug)]
 pub enum Instance {
     #[display("({_0} :: Set)")]
     SetCoerce(Box<Set>),
@@ -167,8 +159,11 @@ pub enum Instance {
         body: Box<Instance>,
     },
 
-    #[display("{_0} {_1}")]
-    App(Box<Instance>, Box<Element>),
+    #[display("{instance} {}", args.iter().map(|e| e.to_string()).collect::<Vec<_>>().join(" "))]
+    App {
+        instance: Box<Instance>,
+        args: Vec<Element>,
+    },
 
     #[display("{instance} .{field}")]
     Project {
@@ -179,7 +174,7 @@ pub enum Instance {
     #[display("case {} of [ {} ]", scrutinee, arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
     Case {
         scrutinee: Box<Element>,
-        arms: Vec<InstCaseArm>,
+        arms: Vec<CaseArm<Instance>>,
     },
 }
 
diff --git a/src/checker_set.rs b/src/checker_set.rs
index 6ef8182..626f74d 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -13,12 +13,12 @@ impl CheckerState {
                 let mut ctx = self.clone();
                 let fields = fields
                     .into_iter()
-                    .map(|RecordField { name, set }| {
-                        let set = ctx.check_set(set)?;
+                    .map(|Field { name, carries }| {
+                        let set = ctx.check_set(carries)?;
                         ctx.add_element(name.clone(), ElementValue::Hypothetical, set.clone())?;
-                        Ok(RecordField {
+                        Ok(Field {
                             name: name.clone(),
-                            set,
+                            carries: set,
                         })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
@@ -27,11 +27,11 @@ impl CheckerState {
             Set::Variant(fields) => {
                 let fields = fields
                     .into_iter()
-                    .map(|VariantField { name, set }| {
-                        let set = self.check_set(set)?;
-                        Ok(VariantField {
+                    .map(|Field { name, carries }| {
+                        let set = self.check_set(carries)?;
+                        Ok(Field {
                             name: name.clone(),
-                            set,
+                            carries: set,
                         })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
@@ -161,9 +161,9 @@ impl CheckerState {
                 let sub_elements = fields
                     .iter()
                     .map(
-                        |RecordField {
+                        |Field {
                              name: f_n,
-                             set: f_s,
+                             carries: f_s,
                          }| {
                             let f_e = assignations
                                 .get(f_n)
@@ -188,7 +188,7 @@ impl CheckerState {
             } => {
                 // globally unique projections mean we know what the sets going
                 // in and out must be
-                let Field {
+                let OwnedField {
                     field: field_set,
                     owner: owner_set,
                 } = self.lookup_record_field(&field)?;
@@ -238,7 +238,7 @@ impl CheckerState {
                 // globally unique injections mean that we know what the sets
                 // going in and out must be, but compared to projections their
                 // roles are here interchanged
-                let Field {
+                let OwnedField {
                     field: field_set,
                     owner: owner_set,
                 } = self.lookup_variant_field(&field)?;
@@ -327,7 +327,7 @@ impl CheckerState {
                 let mut computed_output = None;
                 let mut processed_arms = Vec::new();
                 for arm in arms {
-                    let Field {
+                    let OwnedField {
                         field: field_set, ..
                     } = self.lookup_variant_field(&arm.tag)?;
 
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index bad38eb..2d5057f 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -31,8 +31,8 @@ impl CheckerState {
                 let mut ctx = self.clone();
                 let temp_name = ctx.make_unique_name();
                 let mut new_fields = Vec::new();
-                for SigField { signature, name } in fields {
-                    let signature = ctx.check_signature(signature)?;
+                for Field { carries, name } in fields {
+                    let signature = ctx.check_signature(carries)?;
                     ctx.add_instance(name.clone(), InstanceValue::Hypothetical, signature.clone())?;
                     // And lo, the special case, our chosen canonical form
                     if signature == Signature::Set {
@@ -41,9 +41,9 @@ impl CheckerState {
                             Set::ClaimedSet(Instance::Var(name.clone())).into(),
                         )?;
                     }
-                    new_fields.push(SigField {
+                    new_fields.push(Field {
                         name: name.clone(),
-                        signature,
+                        carries: signature,
                     });
                     // We must iteratively add the entire signature so that
                     // field lookup does something, as we rely on that for type
@@ -140,9 +140,9 @@ impl CheckerState {
                     let sub_instances = fields
                         .iter()
                         .map(
-                            |SigField {
+                            |Field {
                                  name: f_n,
-                                 signature: f_s,
+                                 carries: f_s,
                              }| {
                                 let f_i = assignations
                                     .get(f_n)
@@ -181,7 +181,7 @@ impl CheckerState {
                 }
             }
             Instance::Project { instance, field } => {
-                let Field {
+                let OwnedField {
                     field: field_signature,
                     owner: owner_signature,
                 } = self.lookup_signature_field(&field)?;
@@ -268,7 +268,7 @@ impl CheckerState {
                 let mut computed_output = None;
                 let mut processed_arms = Vec::new();
                 for arm in arms {
-                    let Field {
+                    let OwnedField {
                         field: field_set, ..
                     } = self.lookup_variant_field(&arm.tag)?;
 
@@ -288,7 +288,7 @@ impl CheckerState {
                             )
                         }
                         computed_output = Some(output.clone());
-                        InstCaseArm {
+                        CaseArm {
                             tag: arm.tag.clone(),
                             bound: canonical,
                             body: output,
@@ -296,7 +296,7 @@ impl CheckerState {
                     } else {
                         let canonical = ctx.make_element_binding(binding_name, binding_set)?;
                         let body = ctx.check_instance((&arm.body).into(), signature)?;
-                        InstCaseArm {
+                        CaseArm {
                             tag: arm.tag.clone(),
                             bound: canonical,
                             body,
@@ -386,14 +386,19 @@ impl CheckerState {
                     })
                 }
             }
-            Instance::App(inner, element) => {
+            Instance::App {
+                instance: inner,
+                args,
+            } => {
                 // this is the only time that we ever call check_instance with
                 // signature = None, and in this mode all we want is to put
                 // inner into a canonical form pushing stuck terms to the leaves
                 // and simplifying everything else.
                 let inner = self.check_instance(inner, None)?;
+                println!("HERE {:?}, {:?}", inner, args);
                 match &inner {
                     Instance::Var(v) => {
+                        println!("VAR {}", v);
                         let field = self.lookup_signature_field(&v)?;
                         let Signature::Ext {
                             ref params,
@@ -426,11 +431,12 @@ impl CheckerState {
                                 });
                             }
                         }
-                        let element = self.check_element(element, &params[0].set)?;
-                        Ok(Instance::App(
-                            Box::new(Instance::Var(v.clone())),
-                            Box::new(element),
-                        ))
+                        todo!("finish")
+                        // let element = self.check_element(args, &params[0].set)?;
+                        // Ok(Instance::App(
+                        //     Box::new(Instance::Var(v.clone())),
+                        //     Box::new(element),
+                        // ))
                     }
                     Instance::For { params, body } => {
                         if params.is_empty() {
@@ -440,28 +446,33 @@ impl CheckerState {
                         }
                         let mut ctx = self.clone();
                         let first_set = ctx.check_set(&params[0].set)?;
-                        let element_checked = self.check_element(element, &first_set)?;
-                        ctx.add_element(params[0].name.clone(), element_checked.into(), first_set)?;
-                        if params.len() == 1 {
-                            ctx.check_instance(body, signature)
-                        } else {
-                            let residual = Instance::For {
-                                params: params[1..].to_vec(),
-                                body: body.clone(),
-                            };
-                            ctx.check_instance(&residual, signature)
-                        }
+                        todo!("finish this")
+                        // let element_checked = self.check_element(args, &first_set)?;
+                        // ctx.add_element(params[0].name.clone(), element_checked.into(), first_set)?;
+                        // if params.len() == 1 {
+                        //     ctx.check_instance(body, signature)
+                        // } else {
+                        //     let residual = Instance::For {
+                        //         params: params[1..].to_vec(),
+                        //         body: body.clone(),
+                        //     };
+                        //     ctx.check_instance(&residual, signature)
+                        // }
                     }
                     Instance::Record(_) | Instance::SetCoerce(_) => {
                         Err(CheckerError::NonFunctionalInstance {
                             instance: inner,
-                            element: *element.clone(),
+                            elements: args.clone(),
                         })
                     }
-                    Instance::Project { .. } | Instance::App(_, _) | Instance::Case { .. } => {
+                    Instance::Project { .. } | Instance::App { .. } | Instance::Case { .. } => {
+                        println!("Stuck");
                         // it would appear that we are stuck here, so our only
                         // choice is to continue to be so
-                        Ok(Instance::App(Box::new(inner), element.clone()))
+                        Ok(Instance::App {
+                            instance: Box::new(inner),
+                            args: args.clone(),
+                        })
                     }
                 }
             }
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 3d933f2..a8473ff 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -50,10 +50,10 @@ pub enum CheckerError {
         claimed: Signature,
         reason: String,
     },
-    #[display("Non-functional instance {instance} found in application to element {element}")]
+    #[display("Non-functional instance {instance} found in application to elements {}", elements.iter().map(|e| e.to_string()).collect::<Vec<_>>().join(" "))]
     NonFunctionalInstance {
         instance: Instance,
-        element: Element,
+        elements: Vec<Element>,
     },
 }
 
@@ -61,7 +61,7 @@ pub enum CheckerError {
 // Generics for wrapping fields, values, and coercing them
 #[derive(Display, Clone)]
 #[display("{field} @ {owner}")]
-pub struct Field<T: std::fmt::Display> {
+pub struct OwnedField<T: std::fmt::Display> {
     pub field: T,
     pub owner: T,
 }
@@ -115,9 +115,9 @@ pub struct CheckerState {
     wf_elements: HashMap<String, CheckedElement>,
     wf_signatures: HashMap<String, Signature>,
     wf_instances: HashMap<String, CheckedInstance>,
-    record_fields: HashMap<String, Field<Set>>,
-    variant_fields: HashMap<String, Field<Set>>,
-    signature_fields: HashMap<String, Field<Signature>>,
+    record_fields: HashMap<String, OwnedField<Set>>,
+    variant_fields: HashMap<String, OwnedField<Set>>,
+    signature_fields: HashMap<String, OwnedField<Signature>>,
     binder_element: Arc<AtomicUsize>,
     unique_name: Arc<AtomicUsize>,
 }
@@ -179,7 +179,7 @@ impl CheckerState {
     fn assert_correct_owner<T>(
         &self,
         name: &String,
-        field: &Field<T>,
+        field: &OwnedField<T>,
         belongs_to: &T,
     ) -> Result<(), CheckerError>
     where
@@ -225,7 +225,7 @@ impl CheckerState {
         };
         self.record_fields.insert(
             name.clone(),
-            Field {
+            OwnedField {
                 field: field_set.clone(),
                 owner: owner_set.clone(),
             },
@@ -245,7 +245,7 @@ impl CheckerState {
         };
         self.variant_fields.insert(
             name.clone(),
-            Field {
+            OwnedField {
                 field: field_set.clone(),
                 owner: owner_set.clone(),
             },
@@ -257,18 +257,18 @@ impl CheckerState {
     pub fn add_set(&mut self, name: String, set: SetValue) -> Result<(), CheckerError> {
         match &set {
             SetValue::Concrete(set @ Set::Record(fields)) => {
-                for RecordField {
+                for Field {
                     name: rfn,
-                    set: field_set,
+                    carries: field_set,
                 } in fields
                 {
                     self.add_record_field(rfn, field_set, set)?;
                 }
             }
             SetValue::Concrete(set @ Set::Variant(fields)) => {
-                for VariantField {
+                for Field {
                     name: vfn,
-                    set: field_set,
+                    carries: field_set,
                 } in fields
                 {
                     self.add_variant_field(vfn, field_set, set)?;
@@ -309,13 +309,13 @@ impl CheckerState {
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_record_field(&self, name: &String) -> Result<&Field<Set>, CheckerError> {
+    pub fn lookup_record_field(&self, name: &String) -> Result<&OwnedField<Set>, CheckerError> {
         self.record_fields
             .get(name)
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_variant_field(&self, name: &String) -> Result<&Field<Set>, CheckerError> {
+    pub fn lookup_variant_field(&self, name: &String) -> Result<&OwnedField<Set>, CheckerError> {
         self.variant_fields
             .get(name)
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
@@ -354,7 +354,7 @@ impl CheckerState {
         };
         self.signature_fields.insert(
             name.clone(),
-            Field {
+            OwnedField {
                 field: field_signature.clone(),
                 owner: owner_signature.clone(),
             },
@@ -371,9 +371,9 @@ impl CheckerState {
     ) -> Result<(), CheckerError> {
         match &signature {
             Signature::Theory(fields) => {
-                for SigField {
+                for Field {
                     name: field_name,
-                    signature: field_sig,
+                    carries: field_sig,
                 } in fields
                 {
                     // TODO: are we supposed to recurse?
@@ -420,7 +420,10 @@ impl CheckerState {
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_signature_field(&self, name: &String) -> Result<&Field<Signature>, CheckerError> {
+    pub fn lookup_signature_field(
+        &self,
+        name: &String,
+    ) -> Result<&OwnedField<Signature>, CheckerError> {
         self.signature_fields
             .get(name)
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
diff --git a/src/main.rs b/src/main.rs
index 834792e..1925b41 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -18,35 +18,42 @@ fn main() {
         .init();
 
     let src = r#"
-let signature Graph = theory {
-    Node :: Set,
-    Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
-}
+// 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 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 = {
-    .Node = F3 :: Set,
-    .Edge = for (s : set-of(Node)) (t : set-of(Node)),
-              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 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 .Node),
-  target: set-of(oneSimplex .Node),
-  connected: set-of(oneSimplex .Edge source target)
-}
+// let set OneSimplexEdges = record {
+//   source: set-of(oneSimplex .Vertex),
+//   target: set-of(oneSimplex .Vertex),
+//   connected: set-of(oneSimplex .Edge source target)
+// }
 
-let element edge : set-of(oneSimplex .Edge (three0. pt) (three1. pt)) = pt
+// 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);
 
diff --git a/src/parser.rs b/src/parser.rs
index 6e4a09d..ecf6ab3 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -45,25 +45,25 @@ parser! {
         rule kw_false()         = "false"         wb()
 
         rule keyword() =
-              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_of()      / kw_set()
-            / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool()
-            / kw_true() / kw_false()
+        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_of()      / kw_set()
+        / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool()
+        / kw_true() / kw_false()
 
         // ====================================================================
         // Identifiers
         // ====================================================================
 
         rule lower_ident() -> String
-            = !keyword() s:$(['a'..='z'] ident_tail()*) { s.to_string() }
+        = !keyword() s:$(['a'..='z'] ident_tail()*) { s.to_string() }
 
         rule upper_ident() -> String
-            = !keyword() s:$(['A'..='Z'] ident_tail()*) { s.to_string() }
+        = !keyword() s:$(['A'..='Z'] ident_tail()*) { s.to_string() }
 
         rule any_ident() -> String
-            = !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) { s.to_string() }
+        = !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) { s.to_string() }
 
         rule elem_var() -> String = lower_ident()
         rule inst_var() -> String = lower_ident()
@@ -75,11 +75,11 @@ parser! {
         // ====================================================================
 
         rule project() -> String
-            = __ "." n:any_ident() { n }
+        = __ "." n:any_ident() { n }
 
         rule inject() -> String
-            = _ !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) "." __
-              { s.to_string() }
+        = _ !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) "." __
+        { s.to_string() }
 
         // ====================================================================
         // Record-field labels
@@ -93,170 +93,167 @@ parser! {
         // ====================================================================
 
         rule nat_lit() -> Literal
-            = n:$(['0'..='9']+) !"." { Literal::Nat(n.parse().unwrap()) }
+        = n:$(['0'..='9']+) !"." { Literal::Nat(n.parse().unwrap()) }
 
         rule int_lit() -> Literal
-            = "-" n:$(['0'..='9']+) !"." { Literal::Int(-(n.parse::<i64>().unwrap())) }
+        = "-" n:$(['0'..='9']+) !"." { Literal::Int(-(n.parse::<i64>().unwrap())) }
 
         rule float_lit() -> Literal
-            = s:$("-"? ['0'..='9']+ "." ['0'..='9']+) { Literal::Float(s.parse().unwrap()) }
+        = s:$("-"? ['0'..='9']+ "." ['0'..='9']+) { Literal::Float(s.parse().unwrap()) }
 
         rule str_lit() -> Literal
-            = "\"" s:$((!"\"" [_])*) "\"" { Literal::Str(s.to_string()) }
+        = "\"" s:$((!"\"" [_])*) "\"" { Literal::Str(s.to_string()) }
 
         rule bool_lit() -> Literal
-            = kw_true()  { Literal::Bool(true) }
-            / kw_false() { Literal::Bool(false) }
+        = kw_true()  { Literal::Bool(true) }
+        / kw_false() { Literal::Bool(false) }
 
         rule literal() -> Literal
-            = float_lit() / int_lit() / nat_lit() / str_lit() / bool_lit()
+        = float_lit() / int_lit() / nat_lit() / str_lit() / bool_lit()
 
         rule builtin() -> BuiltIn
-            = kw_Nat()   { BuiltIn::Nat }
-            / kw_Int()   { BuiltIn::Int }
-            / kw_Float() { BuiltIn::Float }
-            / kw_Str()   { BuiltIn::Str }
-            / kw_Bool()  { BuiltIn::Bool }
+        = kw_Nat()   { BuiltIn::Nat }
+        / kw_Int()   { BuiltIn::Int }
+        / kw_Float() { BuiltIn::Float }
+        / kw_Str()   { BuiltIn::Str }
+        / kw_Bool()  { BuiltIn::Bool }
 
         // ====================================================================
         // Sets
         // ====================================================================
 
-        rule set_field() -> RecordField
-            = _ n:lower_ident() _ ":" _ s:set() _
-              { RecordField { name: n, set: s } }
+        rule set_field() -> Field<Set>
+        = _ n:lower_ident() _ ":" _ s:set() _
+        { Field { name: n, carries: s } }
 
-        rule variant_field() -> VariantField
-            = _ n:lower_ident() _ ":" _ s:set() _
-              { VariantField { name: n, set: s } }
+        rule variant_field() -> Field<Set>
+        = _ n:lower_ident() _ ":" _ s:set() _
+        { Field { name: n, carries: s } }
 
         rule claimed_set() -> Instance
-            = kw_set_of() _ "(" _ i:instance() _ ")" { i }
+        = kw_set_of() _ "(" _ i:instance() _ ")" { i }
 
         rule set() -> Set
-            = 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 }
+        = 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 }
 
         // ====================================================================
         // Signatures
         // ====================================================================
 
         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:upper_ident() _ "::" _ s:signature() _
-              { SigField { name: n, signature: s } }
+        rule sig_field() -> Field<Signature>
+        = _ n:upper_ident() _ "::" _ s:signature() _
+        { Field { name: n, carries: s } }
 
         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) } }
-            / v:sig_var()                 { Signature::Var(v) }
-            / "(" _ s:signature() _ ")"   { s }
+        = 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) } }
+        / v:sig_var()                 { Signature::Var(v) }
+        / "(" _ s:signature() _ ")"   { s }
 
         // ====================================================================
         // Elements
         // ====================================================================
 
         rule elem_assign() -> ElemAssign
-            = _ n:field_lower() _ "=" _ e:element() _
-              { ElemAssign { name: n, element: e } }
+        = _ n:field_lower() _ "=" _ e:element() _
+        { ElemAssign { name: n, element: e } }
 
         rule atom_elem() -> Element
-            = l:literal()                              { Element::Literal(l) }
-            / "{" _ fs:(elem_assign() ** ",") _ "}"    { Element::Record(fs) }
-            / "(" _ e:element() _ ")"                  { e }
-            / v:elem_var()                             { Element::Var(v) }
+        = l:literal()                              { Element::Literal(l) }
+        / "{" _ fs:(elem_assign() ** ",") _ "}"    { Element::Record(fs) }
+        / "(" _ e:element() _ ")"                  { e }
+        / v:elem_var()                             { Element::Var(v) }
 
         rule dot_elem() -> Element
-            = tags:(t:inject() _ { t })* head:atom_elem() projs:(p:project() { p })*
-            {
-                let base = projs.into_iter().fold(head, |acc, p| {
-                    Element::Project { element: Box::new(acc), field: p }
-                });
-                tags.into_iter().rev().fold(base, |acc, t| {
-                    Element::Inject { field: t, element: Box::new(acc) }
-                })
-            }
+        = tags:(t:inject() _ { t })* head:atom_elem() projs:(p:project() { p })*
+        {
+            let base = projs.into_iter().fold(head, |acc, p| {
+                Element::Project { element: Box::new(acc), field: p }
+            });
+            tags.into_iter().rev().fold(base, |acc, t| {
+                Element::Inject { field: t, element: Box::new(acc) }
+            })
+        }
 
-        rule case_arm() -> CaseArm
-            = _ t:inject() _ x:elem_var() _ "=>" _ body:element() _
-              { CaseArm { tag: t, bound: x, body } }
+        rule case_arm() -> CaseArm<Element>
+        = _ t:inject() _ x:elem_var() _ "=>" _ body:element() _
+        { CaseArm { tag: t, bound: x, body } }
 
         rule element() -> Element
-            = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]"
-              { Element::Case { scrutinee: Box::new(scrut), arms } }
-            / d:dot_elem() { d }
+        = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]"
+        { Element::Case { scrutinee: Box::new(scrut), arms } }
+        / d:dot_elem() { d }
 
         // ====================================================================
         // Instances
         // ====================================================================
 
-        rule inst_case_arm() -> InstCaseArm
-            = _ t:inject() _ x:elem_var() _ "=>" _ body:instance() _
-              { InstCaseArm { tag: t, bound: x, body } }
+        rule inst_case_arm() -> CaseArm<Instance>
+        = _ t:inject() _ x:elem_var() _ "=>" _ body:instance() _
+        { CaseArm { tag: t, bound: x, body } }
 
         rule inst_assign() -> InstAssign
-            = _ n:field_upper() _ "=" _ i:instance() _
-              { InstAssign { name: n, instance: i } }
+        = _ n:field_upper() _ "=" _ i:instance() _
+        { InstAssign { name: n, instance: i } }
 
         rule explicit_set_coerce() -> Set
-            = s:set() _ "::" _ kw_Set() { s }
+        = s:set() _ "::" _ kw_Set() { s }
 
         rule atom_inst() -> Instance
-            = s:explicit_set_coerce()                    { Instance::SetCoerce(Box::new(s)) }
-            / v:inst_var()                               { Instance::Var(v) }
-            / f:sig_var()                                { Instance::Var(f) }
-            / "{" _ fs:(inst_assign() ** ",") _ "}"      { Instance::Record(fs) }
-            / "(" _ i:instance() _ ")"                   { i }
+        = s:explicit_set_coerce()                    { Instance::SetCoerce(Box::new(s)) }
+        / v:inst_var()                               { Instance::Var(v) }
+        / f:sig_var()                                { Instance::Var(f) }
+        / "{" _ fs:(inst_assign() ** ",") _ "}"      { Instance::Record(fs) }
+        / "(" _ i:instance() _ ")"                   { i }
 
         rule dot_inst() -> Instance
-            = head:atom_inst() projs:(p:project() { p })*
-            {
-                projs.into_iter().fold(head, |acc, p| {
-                    Instance::Project { instance: Box::new(acc), field: p }
-                })
-            }
+        = head:atom_inst() projs:(p:project() { p })*
+        {
+            projs.into_iter().fold(head, |acc, p| {
+                Instance::Project { instance: Box::new(acc), field: p }
+            })
+        }
 
         rule app_inst() -> Instance
-            = head:dot_inst() tail:(__ a:dot_elem() { a })*
-            {
-                tail.into_iter().fold(head, |acc, a| {
-                    Instance::App(Box::new(acc), Box::new(a))
-                })
-            }
+        = head:dot_inst() args:(__ a:dot_elem() { a })*
+        { if args.is_empty() { head } else { Instance::App{instance: Box::new(head), args } }}
+
 
         rule instance() -> Instance
-            = kw_for() _ ps:param_list() _ "," _ body:instance()
-              { Instance::For { params: ps, body: Box::new(body) } }
-            / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]"
-              { Instance::Case { scrutinee: Box::new(scrut), arms } }
-            / app_inst()
+        = kw_for() _ ps:param_list() _ "," _ body:instance()
+        { Instance::For { params: ps, body: Box::new(body) } }
+        / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]"
+        { Instance::Case { scrutinee: Box::new(scrut), arms } }
+        / app_inst()
 
         // ====================================================================
         // Top-level 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_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 } }
+        = 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() -> Programme
-            = _ ds:(decl() ** _) _ { Programme(ds) }
+        = _ ds:(decl() ** _) _ { Programme(ds) }
     }
 }