move assert unbound to only top-level decls to allow shadowing

2 files changed, 20 insertions, 20 deletions

diff --git a/src/checker.rs b/src/checker.rs
index 976b9fb..da4463c 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -19,20 +19,25 @@ impl CheckerState {
             debug!(%self, %decl);
             match decl {
                 Decl::Set { name, set } => {
+                    self.assert_unbound_set(name)?;
                     let set = self.check_set(set.clone())?;
                     self.add_set(name, set)
                 }
 
                 Decl::Element { name, element, set } => {
+                    self.assert_unbound_element(name)?;
                     let set = self.check_set(set.clone())?;
                     let element = self.check_element(element.clone().into(), &set)?;
                     self.add_element(name.clone(), element.into(), set)
                 }
                 Decl::Signature { name, signature } => {
+                    self.assert_unbound_signature(name)?;
                     let signature = self.check_signature(signature.clone())?;
                     self.add_signature(name, signature)
                 }
-                Decl::Instance { .. } => {
+                Decl::Instance { name, .. } => {
+                    self.assert_unbound_instance(name)?;
+
                     return Err(CheckerError::Unimplemented("instances".to_string()));
                 }
             }?;
diff --git a/src/checker_state.rs b/src/checker_state.rs
index a14a6e4..73edd10 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -48,8 +48,10 @@ pub struct Field<T: std::fmt::Display> {
 
 #[derive(Display, Clone)]
 pub enum Value<Term: std::fmt::Display, Type: std::fmt::Display> {
+    /// The storage format for concrete terms.
     Concrete(Term),
     #[display("_ : {_0}")]
+    /// The storage format for formal bindings.
     Hypothetical(Type),
 }
 
@@ -122,10 +124,8 @@ impl fmt::Display for CheckerState {
 // -----------------------------------------------------------------------------
 // Equality
 
-// The invariant we're maintaining is that everything is fully evaluated before
-// we commit it to be stored in the state. Because of our invariant we don't
-// actually need to do anything non-trivial here.
-
+// we work very hard to store canonical forms so that equality is purely
+// structural. This approach may or may not survive contact with reality.
 pub trait DecideEquality<T> {
     fn equal(&self, thing_a: &T, thing_b: &T) -> bool;
 }
@@ -167,7 +167,7 @@ impl CheckerState {
 // -----------------------------------------------------------------------------
 // Sets
 impl CheckerState {
-    fn assert_unbound_set(&self, name: &String) -> Result<(), CheckerError> {
+    pub fn assert_unbound_set(&self, name: &String) -> Result<(), CheckerError> {
         if self.wf_sets.contains_key(name) {
             Err(CheckerError::Rebinding(name.clone()))
         } else {
@@ -175,7 +175,7 @@ impl CheckerState {
         }
     }
 
-    fn assert_unbound_element(&self, name: &String) -> Result<(), CheckerError> {
+    pub fn assert_unbound_element(&self, name: &String) -> Result<(), CheckerError> {
         if self.wf_elements.contains_key(name) {
             Err(CheckerError::Rebinding(name.clone()))
         } else {
@@ -225,7 +225,6 @@ impl CheckerState {
 
     #[instrument(skip(self), level = "debug", fields(%name, %set))]
     pub fn add_set(&mut self, name: &String, set: Set) -> Result<(), CheckerError> {
-        self.assert_unbound_set(name)?;
         match &set {
             Set::Record(fields) => {
                 for RecordField {
@@ -258,7 +257,6 @@ impl CheckerState {
         element: Value<Element, Set>,
         set: Set,
     ) -> Result<(), CheckerError> {
-        self.assert_unbound_element(&name)?;
         self.wf_elements.insert(
             name,
             Checked {
@@ -297,7 +295,7 @@ impl CheckerState {
 // -----------------------------------------------------------------------------
 // Signatures
 impl CheckerState {
-    fn assert_unbound_signature(&self, name: &String) -> Result<(), CheckerError> {
+    pub fn assert_unbound_signature(&self, name: &String) -> Result<(), CheckerError> {
         if self.wf_signatures.contains_key(name) {
             Err(CheckerError::Rebinding(name.clone()))
         } else {
@@ -305,13 +303,13 @@ impl CheckerState {
         }
     }
 
-    // fn assert_unbound_instance(&self, name: &String) -> Result<(), CheckerError> {
-    //     if self.wf_instances.contains_key(name) {
-    //         Err(CheckerError::Rebinding(name.clone()))
-    //     } else {
-    //         Ok(())
-    //     }
-    // }
+    pub fn assert_unbound_instance(&self, name: &String) -> Result<(), CheckerError> {
+        if self.wf_instances.contains_key(name) {
+            Err(CheckerError::Rebinding(name.clone()))
+        } else {
+            Ok(())
+        }
+    }
 
     #[instrument(skip(self), level = "debug", fields(%name, %field_signature, %owner_signature))]
     fn add_signature_field(
@@ -339,8 +337,6 @@ impl CheckerState {
         name: &String,
         signature: Signature,
     ) -> Result<(), CheckerError> {
-        self.assert_unbound_signature(name)?;
-
         match &signature {
             Signature::Theory(fields) => {
                 for SigField {
@@ -367,7 +363,6 @@ impl CheckerState {
         instance: InstanceValue,
         signature: Signature,
     ) -> Result<(), CheckerError> {
-        self.assert_unbound_element(&name)?;
         self.wf_instances.insert(
             name,
             Checked {