diff options
Diffstat (limited to 'src/parser.rs')
| -rw-r--r-- | src/parser.rs | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/parser.rs b/src/parser.rs index 8dbc31e..6ab5900 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -32,6 +32,7 @@ parser! { rule kw_theory() = "theory" wb() rule kw_case() = "case" wb() rule kw_of() = "of" wb() + rule kw_element_of() = "element-of" wb() rule kw_for() = "for" wb() rule kw_set() = "set" wb() rule kw_set_of() = "set-of" wb() @@ -48,8 +49,8 @@ parser! { 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_Set() / kw_set_of() / kw_set() / kw_element_of() + / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() / kw_true() / kw_false() // ==================================================================== @@ -205,8 +206,13 @@ parser! { = _ t:inject() _ x:elem_var() _ "=>" _ body:element() _ { CaseArm { tag: t, bound: x, body } } + rule claimed_element() -> Instance + = kw_element_of() _ "(" _ i:instance() _ ")" { i } + + rule element() -> Element - = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } + = i:claimed_element() { Element::ClaimedElement(Box::new(i)) } + / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } / d:dot_elem() { d } // ==================================================================== |