diff options
| author | tslil <tslil@posteo.de> | 2026-05-07 11:50:06 +0100 |
|---|---|---|
| committer | tslil <tslil@posteo.de> | 2026-05-07 13:34:30 +0100 |
| commit | 8d9c0e5868b2a7fa22080f814357dcda69a10057 (patch) | |
| tree | 5a49bfd66ea2e8d6ffeb425a7198bdb58fb3ec02 /src/parser.rs | |
| parent | d14c744a1cff323f8a837ef620a93ee518c392a2 (diff) | |
add complete lifted sets
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 } // ==================================================================== |