1 files changed, 39 insertions, 44 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>>,
     },
 }