wire in instance checking to the main checker

1 files changed, 14 insertions, 4 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 15203b2..e92d424 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -32,8 +32,18 @@ impl CheckerState {
                     .into_iter()
                     .map(|SigField { signature, name }| {
                         let signature = ctx.check_signature(signature)?;
-                        // This call handles the special case in the event that signature is Set
-                        ctx.make_instance_binding(name.clone(), signature.clone())?;
+                        ctx.add_instance(
+                            name.clone(),
+                            InstanceValue::Hypothetical,
+                            signature.clone(),
+                        )?;
+                        // And lo, the special case, our chosen canonical form
+                        if signature == Signature::Set {
+                            ctx.add_set(
+                                name.clone(),
+                                Set::ClaimedSet(Instance::Var(name.clone())).into(),
+                            )?;
+                        }
                         Ok(SigField { name, signature })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
@@ -42,7 +52,7 @@ impl CheckerState {
         }
     }
 
-    #[instrument(skip(self), level = "debug", fields(%instance, %signature))]
+    #[instrument(skip(self), level = "debug", fields(%instance, ?signature))]
     pub fn check_instance(
         &self,
         instance: Instance,
@@ -92,7 +102,7 @@ impl CheckerState {
                 let fields = if let Signature::Theory(fields) = signature {
                     Ok(fields)
                 } else {
-                    Err(rej("instance is a record instance".to_string()))
+                    Err(rej("instance is not a record instance".to_string()))
                 }?;
 
                 let (signature_fnames, signature_fsigs): (Vec<String>, Vec<Signature>) = fields