From 89304b27ea81270684810c18d3315c9d399beaf9 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Tue, 5 May 2026 11:15:07 +0100
Subject: address remaining TODO, fix issues with left-nesting for for and ext,
 add motivation blurb to the readme

---
 src/checker_state.rs | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

(limited to 'src/checker_state.rs')

diff --git a/src/checker_state.rs b/src/checker_state.rs
index 3404a35..45d2dab 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -272,27 +272,27 @@ impl CheckerState {
     }
 
     #[instrument(skip(self), level = "debug", fields(%name, %set))]
-    pub fn add_set(&mut self, name: String, set: SetValue) -> Result<(), CheckerError> {
+    pub fn add_set(&mut self, name: String, set: Set) -> Result<(), CheckerError> {
         match &set {
-            SetValue::Concrete(set @ Set::Record(fields)) => {
+            Set::Record(fields) => {
                 for Field {
                     name: rfn,
                     carries: field_set,
                 } in fields
                 {
-                    self.add_record_field(rfn, field_set, set)?;
+                    self.add_record_field(rfn, field_set, &set)?;
                 }
             }
-            SetValue::Concrete(set @ Set::Variant(fields)) => {
+            Set::Variant(fields) => {
                 for Field {
                     name: vfn,
                     carries: field_set,
                 } in fields
                 {
-                    self.add_variant_field(vfn, field_set, set)?;
+                    self.add_variant_field(vfn, field_set, &set)?;
                 }
             }
-            _ => (),
+            Set::Var(_) | Set::BuiltIn(_) | Set::ClaimedSet(_) => (),
         };
         self.wf_sets.insert(name, set.into());
         Ok(())
@@ -394,14 +394,16 @@ impl CheckerState {
                     carries: field_sig,
                 } in fields
                 {
-                    // TODO: are we supposed to recurse?
-                    // let name = self.make_unique_name();
-                    // self.add_signature(&name, field_sig.clone(), rebind)?;
+                    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)?;
                 }
             }
-            // TODO: is there more?
-            _ => (),
+            Signature::Ext { codomain, .. } => {
+                let inner_name = self.make_unique_name();
+                self.add_signature(&inner_name, (**codomain).clone(), rebind)?;
+            }
+            Signature::Set | Signature::Var(_) => (),
         };
 
         self.wf_signatures.insert(name.clone(), signature);
@@ -487,4 +489,8 @@ impl CheckerState {
         let n = self.unique_name.fetch_add(1, Ordering::Relaxed);
         _reserved_name(n)
     }
+
+    pub fn reset_binders(&mut self) {
+        self.binder_element.store(0, Ordering::Relaxed);
+    }
 }
-- 
cgit v1.3.1