working on fixing app, rework ast to have generics etc

1 files changed, 102 insertions, 105 deletions

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) }
     }
 }