implement canonicalisation in case arms, work through first bit of app

1 files changed, 41 insertions, 9 deletions

diff --git a/src/checker_state.rs b/src/checker_state.rs
index 1a6a0bd..6a458d5 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -47,6 +47,11 @@ pub enum CheckerError {
         claimed: Signature,
         reason: String,
     },
+    #[display("Non-functional instance {instance} found in application to element {element}")]
+    NonFunctionalInstance {
+        instance: Instance,
+        element: Element,
+    },
 }
 
 // -----------------------------------------------------------------------------
@@ -111,6 +116,7 @@ pub struct CheckerState {
     variant_fields: HashMap<String, Field<Set>>,
     signature_fields: HashMap<String, Field<Signature>>,
     binder_element: usize,
+    unique_name: usize,
 }
 
 impl fmt::Display for CheckerState {
@@ -136,6 +142,7 @@ impl fmt::Display for CheckerState {
         section(f, "variant_fields", &self.variant_fields)?;
         section(f, "signatures", &self.wf_signatures)?;
         section(f, "instances", &self.wf_instances)?;
+        section(f, "signature_fields", &self.signature_fields)?;
         writeln!(f, " }}")?;
         Ok(())
     }
@@ -332,13 +339,14 @@ impl CheckerState {
     }
 
     #[instrument(skip(self), level = "debug", fields(%name, %field_signature, %owner_signature))]
-    fn add_signature_field(
+    pub fn add_signature_field(
         &mut self,
         name: &String,
         field_signature: &Signature,
         owner_signature: &Signature,
+        rebind: bool,
     ) -> Result<(), CheckerError> {
-        if let Some(signature_ref) = self.signature_fields.get(name) {
+        if !rebind && let Some(signature_ref) = self.signature_fields.get(name) {
             self.assert_correct_owner(name, signature_ref, owner_signature)?;
         };
         self.signature_fields.insert(
@@ -356,6 +364,7 @@ impl CheckerState {
         &mut self,
         name: &String,
         signature: Signature,
+        rebind: bool,
     ) -> Result<(), CheckerError> {
         match &signature {
             Signature::Theory(fields) => {
@@ -364,7 +373,7 @@ impl CheckerState {
                     signature: field_sig,
                 } in fields
                 {
-                    self.add_signature_field(field_name, field_sig, &signature)?;
+                    self.add_signature_field(field_name, field_sig, &signature, rebind)?;
                 }
             }
             // TODO: is there more?
@@ -415,12 +424,35 @@ impl CheckerState {
 // -----------------------------------------------------------------------------
 // Bindings
 impl CheckerState {
-    #[instrument(skip(self), level = "debug", fields(%name, %set))]
-    pub fn make_element_binding(&mut self, name: String, set: Set) -> Result<(), CheckerError> {
-        let canonical = format!("db_e_{}", self.binder_element);
-        self.add_element(canonical.clone(), ElementValue::Hypothetical, set.clone())?;
-        self.add_element(name, Element::Var(canonical).into(), set)?;
+    fn _make_canonical_element(&mut self, name: String, set: Set) -> Result<String, CheckerError> {
+        let canonical = format!("_#{}", self.binder_element);
+        self.add_element(name, Element::Var(canonical.clone()).into(), set)?;
         self.binder_element += 1;
-        Ok(())
+        Ok(canonical)
+    }
+
+    #[instrument(skip(self), level = "debug", fields(%name, %set))]
+    pub fn make_element_binding(&mut self, name: String, set: Set) -> Result<String, CheckerError> {
+        let canonical = self._make_canonical_element(name, set.clone())?;
+        self.add_element(canonical.clone(), ElementValue::Hypothetical, set)?;
+        Ok(canonical)
+    }
+
+    #[instrument(skip(self), level = "debug", fields(%name, %set))]
+    pub fn make_element_definition(
+        &mut self,
+        name: String,
+        value: Element,
+        set: Set,
+    ) -> Result<String, CheckerError> {
+        let canonical = self._make_canonical_element(name, set.clone())?;
+        self.add_element(canonical.clone(), Value::Concrete(value), set)?;
+        Ok(canonical)
+    }
+
+    #[instrument(skip(self))]
+    pub fn make_unique_name(&mut self) -> String {
+        self.unique_name += 1;
+        format!("_#{}", self.unique_name)
     }
 }