aboutsummaryrefslogtreecommitdiff
path: root/src/parser.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser.rs')
-rw-r--r--src/parser.rs32
1 files changed, 28 insertions, 4 deletions
diff --git a/src/parser.rs b/src/parser.rs
index 4e41644..31956bd 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -154,11 +154,23 @@ parser! {
= _ n:upper_ident() _ "::" _ s:signature() _
{ Field { name: n, carries: s } }
+ rule sig_ext() -> Signature
+ = ps:param_list() _ "->" _ cod:signature()
+ {
+ match cod {
+ Signature::Ext { params: inner, codomain } => {
+ let mut all = ps;
+ all.extend(inner);
+ Signature::Ext { params: all, codomain }
+ }
+ other => Signature::Ext { params: ps, codomain: Box::new(other) },
+ }
+ }
+
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) } }
+ / s:sig_ext() { s }
/ v:sig_var() { Signature::Var(v) }
/ "(" _ s:signature() _ ")" { s }
@@ -243,9 +255,21 @@ parser! {
}
}
- rule instance() -> Instance
+ rule inst_for() -> Instance
= kw_for() _ ps:param_list() _ "," _ body:instance()
- { Instance::For { params: ps, body: Box::new(body) } }
+ {
+ match body {
+ Instance::For { params: inner, body } => {
+ let mut all = ps;
+ all.extend(inner);
+ Instance::For { params: all, body }
+ }
+ other => Instance::For { params: ps, body: Box::new(other) },
+ }
+ }
+
+ 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()