From ecc2c04edbcfdd097377683c28b92cd10e437d35 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Tue, 28 Apr 2026 14:24:06 +0100
Subject: move assert unbound to only top-level decls to allow shadowing

---
 src/checker_state.rs | 33 ++++++++++++++-------------------
 1 file changed, 14 insertions(+), 19 deletions(-)

(limited to 'src/checker_state.rs')

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 {
-- 
cgit v1.3.1