diff options
Diffstat (limited to 'src/parser.rs')
| -rw-r--r-- | src/parser.rs | 66 |
1 files changed, 32 insertions, 34 deletions
diff --git a/src/parser.rs b/src/parser.rs index f205407..73e8dd3 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -45,12 +45,12 @@ 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 @@ -134,19 +134,20 @@ parser! { = 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() ++ _ @@ -168,11 +169,12 @@ parser! { } rule signature() -> Signature - = kw_Set() { Signature::Set } - / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } - / s:sig_ext() { s } - / v:sig_var() { Signature::Var(v) } - / "(" _ s:signature() _ ")" { s } + = kw_Set() { Signature::Set } + / "<" _ s:set() _ ">" { Signature::FromSet(s) } + / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } + / s:sig_ext() { s } + / v:sig_var() { Signature::Var(v) } + / "(" _ s:signature() _ ")" { s } // ==================================================================== // Elements @@ -204,9 +206,8 @@ parser! { { 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 @@ -221,10 +222,12 @@ parser! { { 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)) } + / "<" _ e:element() _ ">" { Instance::ElementCoerce(e) } / v:inst_var() { Instance::Var(v) } / f:sig_var() { Instance::Var(f) } / "{" _ fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) } @@ -269,24 +272,19 @@ parser! { } rule instance() -> Instance - = i:inst_for() { i } - / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" - { Instance::Case { scrutinee: Box::new(scrut), arms } } - / app_inst() + = i:inst_for() { i } + / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" { Instance::Case { scrutinee: Box::new(scrut), arms } } + / a:app_inst() { a } // ==================================================================== // 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) } |