From 89304b27ea81270684810c18d3315c9d399beaf9 Mon Sep 17 00:00:00 2001 From: tslil Date: Tue, 5 May 2026 11:15:07 +0100 Subject: address remaining TODO, fix issues with left-nesting for for and ext, add motivation blurb to the readme --- src/parser.rs | 32 ++++++++++++++++++++++++++++---- 1 file changed, 28 insertions(+), 4 deletions(-) (limited to 'src/parser.rs') 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() -- cgit v1.3.1