1 files changed, 52 insertions, 22 deletions

diff --git a/src/ast.rs b/src/ast.rs
index 0590556..1b34fc3 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -2,7 +2,7 @@ use derive_more::Display;
 
 // Set layer
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 pub enum BuiltIn {
     Nat,
     Int,
@@ -11,68 +11,75 @@ pub enum BuiltIn {
     Bool,
 }
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 #[display(".{name} : {set}")]
 pub struct RecordField {
     pub name: String,
     pub set: Set,
 }
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 #[display("{name}. : {set}")]
 pub struct VariantField {
     pub name: String,
     pub set: Set,
 }
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 pub enum Set {
     #[display("{_0}")]
     BuiltIn(BuiltIn),
+
     #[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
     Record(Vec<RecordField>),
+
     #[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, Display)]
+#[derive(Clone, PartialEq, Display)]
 #[display("({name} : {set})")]
 pub struct Param {
     pub name: String,
     pub set: Set,
 }
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 #[display(".{name} :: {signature}")]
 pub struct SigField {
     pub name: String,
     pub signature: Signature,
 }
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, 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>,
     },
+
     #[display("{_0}")]
     Var(String),
 }
 
 // Element layer
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 pub enum Literal {
     Nat(u64),
     Int(i64),
@@ -81,14 +88,14 @@ pub enum Literal {
     Bool(bool),
 }
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 #[display(".{name} = {element}")]
 pub struct ElemAssign {
     pub name: String,
     pub element: Element,
 }
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 #[display(".{tag} {bound} => {body}")]
 pub struct CaseArm {
     pub tag: String,
@@ -96,21 +103,33 @@ pub struct CaseArm {
     pub body: Element,
 }
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, 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>),
-    #[display("{_0} .{_1}")]
-    Project(Box<Element>, String),
-    #[display("{_0}. {_1}")]
-    Inject(String, Box<Element>),
+
+    #[display("{element} .{field}")]
+    Project {
+        element: Box<Element>,
+        field: String,
+    },
+
+    #[display("{field}. {element}")]
+    Inject {
+        field: String,
+        element: Box<Element>,
+    },
+
     #[display("{_0} {_1}")]
     App(Box<Element>, Box<Element>),
-    #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
+
+    #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
     Case {
         scrutinee: Box<Element>,
         arms: Vec<CaseArm>,
@@ -119,46 +138,57 @@ pub enum Element {
 
 // Instance layer
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 #[display(".{name} = {instance}")]
 pub struct InstAssign {
     pub name: String,
     pub instance: Instance,
 }
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 pub enum Instance {
     #[display("({_0} :: Set)")]
     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(""))]
+
+    #[display("for {}, {body}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(""))]
     For {
         params: Vec<Param>,
         body: Box<Instance>,
     },
+
     #[display("{_0} {_1}")]
     App(Box<Instance>, Box<Element>),
-    #[display("{_0} .{_1}")]
-    Project(Box<Instance>, String),
+
+    #[display("{instance} .{field}")]
+    Project {
+        instance: Box<Instance>,
+        field: String,
+    },
 }
 
 // Declarations
 
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
 pub enum Decl {
     #[display("let set {name} = {set}")]
     Set { name: String, set: Set },
+
     #[display("let element {name} : {set} = {element}")]
     Element {
         name: String,
         set: Set,
         element: Element,
     },
+
     #[display("let signature {name} = {signature}")]
     Signature { name: String, signature: Signature },
+
     #[display("let instance {name} :: {signature} = {instance}")]
     Instance {
         name: String,