diff options
Diffstat (limited to 'src/checker_signature.rs')
| -rw-r--r-- | src/checker_signature.rs | 18 |
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 |