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

1 files changed, 113 insertions, 104 deletions

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 = {