aboutsummaryrefslogtreecommitdiff
path: root/src/checker_state.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/checker_state.rs')
-rw-r--r--src/checker_state.rs29
1 files changed, 1 insertions, 28 deletions
diff --git a/src/checker_state.rs b/src/checker_state.rs
index b710ac3..1a6a0bd 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -41,7 +41,7 @@ pub enum CheckerError {
claimed: Signature,
real: Signature,
},
- #[display("Instance {instance} does belong to set {claimed}: {reason}")]
+ #[display("Instance {instance} is not of signature {claimed}: {reason}")]
InstanceDoesNotBelong {
instance: Instance,
claimed: Signature,
@@ -111,7 +111,6 @@ pub struct CheckerState {
variant_fields: HashMap<String, Field<Set>>,
signature_fields: HashMap<String, Field<Signature>>,
binder_element: usize,
- binder_instance: usize,
}
impl fmt::Display for CheckerState {
@@ -424,30 +423,4 @@ impl CheckerState {
self.binder_element += 1;
Ok(())
}
-
- #[instrument(skip(self), level = "debug", fields(%name, %signature))]
- pub fn make_instance_binding(
- &mut self,
- name: String,
- signature: Signature,
- ) -> Result<(), CheckerError> {
- let canonical = format!("db_i_{}", self.binder_instance);
- self.add_instance(
- canonical.clone(),
- InstanceValue::Hypothetical,
- signature.clone(),
- )?;
- self.add_instance(
- name.clone(),
- Instance::Var(canonical.clone()).into(),
- signature.clone(),
- )?;
- // And lo, the special case, our chosen canonical form
- if signature == Signature::Set {
- self.add_set(name, Set::ClaimedSet(Instance::Var(canonical)).into())?;
- }
-
- self.binder_instance += 1;
- Ok(())
- }
}