fix ext nesting, don't register junky intermediate signatures

1 files changed, 30 insertions, 17 deletions

diff --git a/src/checker_state.rs b/src/checker_state.rs
index 45d2dab..ad01d50 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -380,34 +380,39 @@ impl CheckerState {
         Ok(())
     }
 
-    #[instrument(skip(self), level = "debug", fields(%name, %signature))]
-    pub fn add_signature(
+    fn _register_signature_fields(
         &mut self,
-        name: &String,
-        signature: Signature,
+        signature: &Signature,
         rebind: bool,
     ) -> Result<(), CheckerError> {
-        match &signature {
+        match signature {
             Signature::Theory(fields) => {
                 for Field {
                     name: field_name,
                     carries: field_sig,
                 } in fields
                 {
-                    let inner_name = self.make_unique_name();
-                    self.add_signature(&inner_name, field_sig.clone(), rebind)?;
-                    self.add_signature_field(field_name, field_sig, &signature, rebind)?;
+                    self._register_signature_fields(field_sig, rebind)?;
+                    self.add_signature_field(field_name, field_sig, signature, rebind)?;
                 }
             }
             Signature::Ext { codomain, .. } => {
-                let inner_name = self.make_unique_name();
-                self.add_signature(&inner_name, (**codomain).clone(), rebind)?;
+                self._register_signature_fields(codomain, rebind)?;
             }
-            Signature::Set | Signature::Var(_) => (),
-        };
+            _ => (),
+        }
+        Ok(())
+    }
 
+    #[instrument(skip(self), level = "debug", fields(%name, %signature))]
+    pub fn add_signature(
+        &mut self,
+        name: &String,
+        signature: Signature,
+        rebind: bool,
+    ) -> Result<(), CheckerError> {
+        self._register_signature_fields(&signature, rebind)?;
         self.wf_signatures.insert(name.clone(), signature);
-
         Ok(())
     }
 
@@ -453,14 +458,14 @@ impl CheckerState {
 // -----------------------------------------------------------------------------
 // Bindings
 
-fn _reserved_name(n: usize) -> String {
-    format!("#{}", n)
+fn _reserved_name(n: usize, alter: bool) -> String {
+    format!("{}#{}", if alter { "@" } else { "" }, n)
 }
 
 impl CheckerState {
     fn _make_canonical_element(&mut self, name: String, set: Set) -> Result<String, CheckerError> {
         let n = self.binder_element.fetch_add(1, Ordering::Relaxed);
-        let canonical = _reserved_name(n);
+        let canonical = _reserved_name(n, false);
         self.add_element(name, Element::Var(canonical.clone()).into(), set)?;
         Ok(canonical)
     }
@@ -487,10 +492,18 @@ impl CheckerState {
     #[instrument(skip(self))]
     pub fn make_unique_name(&mut self) -> String {
         let n = self.unique_name.fetch_add(1, Ordering::Relaxed);
-        _reserved_name(n)
+        _reserved_name(n, true)
     }
 
     pub fn reset_binders(&mut self) {
         self.binder_element.store(0, Ordering::Relaxed);
     }
+
+    pub fn get_binder_counter(&self) -> usize {
+        self.binder_element.load(Ordering::Relaxed)
+    }
+
+    pub fn set_binder_counter(&mut self, counter: usize) {
+        self.binder_element.store(counter, Ordering::Relaxed);
+    }
 }