fix ext nesting, don't register junky intermediate signatures

2 files changed, 72 insertions, 28 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 2888568..0145e82 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -15,36 +15,67 @@ impl CheckerState {
                 Ok(deref.clone())
             }
             Signature::Ext { params, codomain } => {
+                if params.is_empty() {
+                    return Err(CheckerError::Unimplemented(
+                        "extension signature with empty params".to_string(),
+                    ));
+                }
                 let mut ctx = self.clone();
+
+                // a little juggling here to ensure that we merge names without
+                // collision, the pattern is: bind to something unique, recurse,
+                // fix the names which involves in particular messing about with
+                // counters
                 let params = params
                     .iter()
                     .map(|p| {
                         let set = ctx.check_set(&p.set)?;
-                        let canon = ctx.make_element_binding(p.name.clone(), set.clone())?;
+                        let canon = ctx.make_unique_name();
+                        ctx.add_element(
+                            p.name.clone(),
+                            Element::Var(canon.clone()).into(),
+                            set.clone(),
+                        )?;
+                        ctx.add_element(canon.clone(), ElementValue::Hypothetical, set.clone())?;
                         Ok(Param { set, name: canon })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
+
+                // use tactic "trust_me"
+                let snapshot = ctx.get_binder_counter();
                 let codomain = ctx.check_signature(codomain)?;
+                ctx.set_binder_counter(snapshot);
 
-                let result = if let Signature::Ext {
+                let (params, codomain) = if let Signature::Ext {
                     params: inner,
                     codomain: deep,
                 } = codomain
                 {
                     let mut merged = params.clone();
                     merged.extend(inner.iter().cloned());
-                    Signature::Ext {
-                        params: merged,
-                        codomain: deep,
-                    }
+                    (merged, *deep)
                 } else {
-                    Signature::Ext {
-                        params,
-                        codomain: Box::new(codomain),
-                    }
+                    (params, codomain)
                 };
 
-                Ok(result)
+                // normalise
+                let mut ctx = self.clone();
+                let params = params
+                    .into_iter()
+                    .map(|Param { name, set }| {
+                        let canonical = ctx.make_element_binding(name, set.clone())?;
+                        Ok(Param {
+                            name: canonical,
+                            set,
+                        })
+                    })
+                    .collect::<Result<Vec<_>, _>>()?;
+                let codomain = ctx.check_signature(&codomain)?;
+
+                Ok(Signature::Ext {
+                    params,
+                    codomain: Box::new(codomain),
+                })
             }
             Signature::Theory(fields) => {
                 let mut ctx = self.clone();
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);
+    }
 }