fix parser bug, fix beta reduction for setcoerce, disambiguate set coerce in parser

1 files changed, 9 insertions, 5 deletions

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)
             }
         "#;