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

5 files changed, 21 insertions, 15 deletions

diff --git a/grammar.txt b/grammar.txt
index 32585bb..9772501 100644
--- a/grammar.txt
+++ b/grammar.txt
@@ -36,7 +36,7 @@ instance          = for_inst | app_inst ;
 for_inst          = "for" , param_list , "," , instance ;
 app_inst          = dot_inst { dot_elem } ;
 dot_inst          = atom_inst { project_elem } ;
-atom_inst         = set | inst_var | record_inst | "(" , instance , ")" ;
+atom_inst         = set ":: Set" | inst_var | record_inst | "(" , instance , ")" ;
 record_inst       = "{" , [ inst_assign { "," , inst_assign } ] , "}" ;
 inst_assign       = project_elem , "=" , instance ;
 
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 36b11ca..15203b2 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -58,7 +58,11 @@ impl CheckerState {
                     });
                 };
                 let set = Box::new(self.check_set(*set.clone())?);
-                Ok(Instance::SetCoerce(set))
+                if let Set::ClaimedSet(inner) = *set {
+                    Ok(inner)
+                } else {
+                    Ok(Instance::SetCoerce(set))
+                }
             }
             Instance::Var(ref v) => {
                 // Exactly the same discipline as for Element::Var, see there
@@ -158,7 +162,7 @@ impl CheckerState {
                         Ok(sub_element)
                     }
                     _ => panic!(
-                        "invariant violation: check_element returned neither a record or stuck computation for record set"
+                        "invariant violation: check_instance returned neither a record or stuck computation for record set"
                     ),
                 }
             }
diff --git a/src/checker_state.rs b/src/checker_state.rs
index dc76a10..b710ac3 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -442,11 +442,9 @@ impl CheckerState {
             Instance::Var(canonical.clone()).into(),
             signature.clone(),
         )?;
-        // And lo, the special case:
-        // TODO: is this correct in the presence of de bruijn?
+        // And lo, the special case, our chosen canonical form
         if signature == Signature::Set {
-            self.add_set(canonical.clone(), SetValue::Hypothetical)?;
-            self.add_set(name, Set::Var(canonical).into())?;
+            self.add_set(name, Set::ClaimedSet(Instance::Var(canonical)).into())?;
         }
 
         self.binder_instance += 1;
diff --git a/src/main.rs b/src/main.rs
index a40eb87..94a9428 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -36,7 +36,7 @@ let signature OneSet = theory { F :: Set }
 let signature T = theory {
     A :: Set,
     B :: (x : set-of({ .F = A } .F)) -> Set,
-    C :: (x : set-of(A)) (b : set-of(B x)) -> Set
+    C :: (x : set-of(set-of(set-of(A) :: Set) :: Set)) (b : set-of(B x)) -> Set
 }
 
 let signature Graph = theory {
@@ -45,8 +45,8 @@ let signature Graph = theory {
 }
 
 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
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)
             }
         "#;