From 651a67cb568d80e72f8c6a650b985991f4b129d8 Mon Sep 17 00:00:00 2001 From: tslil Date: Wed, 29 Apr 2026 10:56:16 +0100 Subject: fix parser bug, fix beta reduction for setcoerce, disambiguate set coerce in parser --- src/parser.rs | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'src/parser.rs') diff --git a/src/parser.rs b/src/parser.rs index 65aa7f4..e917aac 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -179,9 +179,13 @@ parser! { = n:project_upper() _ "=" _ i:instance() { InstAssign { name: n, instance: i } } + rule explicit_set_coerce() -> Set + = _ s:set() _ "::" _ kw_Set() _ { s } + rule atom_inst() -> Instance - = s:set() { Instance::SetCoerce(Box::new(s)) } - / v:inst_var() { Instance::Var(v) } + = v:inst_var() { Instance::Var(v) } + / f:sig_var() { Instance::Var(f) } + / s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) } / "{" fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) } / "(" _ i:instance() _ ")" { i } @@ -291,8 +295,8 @@ let set Maybe = variant [ } let instance natPoset :: Graph = { - .Node = Nat, - .Edge = for (s : Nat) (t : Nat), Bool + .Node = (Nat :: Set), + .Edge = for (s : Nat) (t : Nat), Bool::Set } let element node : set-of(natPoset .Node) = 7 @@ -300,7 +304,7 @@ let set Maybe = variant [ let set NatEdges = record { source: set-of(natPoset .Node), target: set-of(natPoset .Node), - connected: set-of(natPoset .Edge source target) + connected: set-of(set-of(natPoset .Edge source target) :: Set) } "#; -- cgit v1.3.1