address remaining TODO, fix issues with left-nesting for for and ext, add motivation blurb to the readme

1 files changed, 17 insertions, 11 deletions

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);
+    }
 }