refactor equality checking and fields as we start to build towards signatures

1 files changed, 123 insertions, 31 deletions

diff --git a/src/checker_state.rs b/src/checker_state.rs
index 86f229e..8ec153d 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -38,10 +38,10 @@ pub enum CheckerError {
 }
 
 #[derive(Display, Clone)]
-#[display("{field_set} @ {owner_set}")]
-pub struct SetField {
-    pub field_set: Set,
-    pub owner_set: Set,
+#[display("{field} @ {owner}")]
+pub struct Field<T: std::fmt::Display> {
+    pub field: T,
+    pub owner: T,
 }
 
 #[derive(Display, Clone)]
@@ -70,8 +70,9 @@ pub struct CheckerState {
     wf_elements: HashMap<String, CheckedElement>,
     wf_signatures: HashMap<String, Signature>,
     wf_instances: HashMap<String, Instance>,
-    record_fields: HashMap<String, SetField>,
-    variant_fields: HashMap<String, SetField>,
+    record_fields: HashMap<String, Field<Set>>,
+    variant_fields: HashMap<String, Field<Set>>,
+    signature_fields: HashMap<String, Field<Signature>>,
 }
 
 impl fmt::Display for CheckerState {
@@ -102,40 +103,64 @@ impl fmt::Display for CheckerState {
     }
 }
 
+// -----------------------------------------------------------------------------
+// Equality
+
 // The invariant we're maintaining is that everything is fully evaluated before
-// we commit it to be stored in the state.
-impl CheckerState {
-    // Because of our invariant we don't actually need to do anything
-    // non-trivial here.
+// we commit it to be stored in the state. Because of our invariant we don't
+// actually need to do anything non-trivial here.
+
+pub trait DecideEquality<T> {
+    fn equal(&self, thing_a: &T, thing_b: &T) -> bool;
+}
+
+impl DecideEquality<Set> for CheckerState {
     #[instrument(skip(self), level = "debug", fields(%set_a, %set_b))]
-    pub fn set_equal(&self, set_a: &Set, set_b: &Set) -> bool {
+    fn equal(&self, set_a: &Set, set_b: &Set) -> bool {
         set_a == set_b
     }
+}
 
-    fn assert_unbound_set(&self, name: &String) -> Result<(), CheckerError> {
-        if self.wf_sets.contains_key(name) {
+impl DecideEquality<Signature> for CheckerState {
+    #[instrument(skip(self), level = "debug", fields(%signature_a, %signature_b))]
+    fn equal(&self, signature_a: &Signature, signature_b: &Signature) -> bool {
+        signature_a == signature_b
+    }
+}
+
+impl CheckerState {
+    #[instrument(skip(self), level = "debug", fields(%name, %field, %belongs_to))]
+    fn assert_correct_owner<T>(
+        &self,
+        name: &String,
+        field: &Field<T>,
+        belongs_to: &T,
+    ) -> Result<(), CheckerError>
+    where
+        Self: DecideEquality<T>,
+        T: std::fmt::Display,
+    {
+        if !self.equal(&field.owner, belongs_to) {
             Err(CheckerError::Rebinding(name.clone()))
         } else {
             Ok(())
         }
     }
+}
 
-    fn assert_unbound_element(&self, name: &String) -> Result<(), CheckerError> {
-        if self.wf_elements.contains_key(name) {
+// -----------------------------------------------------------------------------
+// Sets
+impl CheckerState {
+    fn assert_unbound_set(&self, name: &String) -> Result<(), CheckerError> {
+        if self.wf_sets.contains_key(name) {
             Err(CheckerError::Rebinding(name.clone()))
         } else {
             Ok(())
         }
     }
 
-    #[instrument(skip(self), level = "debug", fields(%name, %set_ref, %belongs_to))]
-    fn assert_correct_owner(
-        &self,
-        name: &String,
-        set_ref: &SetField,
-        belongs_to: &Set,
-    ) -> Result<(), CheckerError> {
-        if !self.set_equal(&set_ref.owner_set, belongs_to) {
+    fn assert_unbound_element(&self, name: &String) -> Result<(), CheckerError> {
+        if self.wf_elements.contains_key(name) {
             Err(CheckerError::Rebinding(name.clone()))
         } else {
             Ok(())
@@ -154,9 +179,9 @@ impl CheckerState {
         };
         self.record_fields.insert(
             name.clone(),
-            SetField {
-                field_set: field_set.clone(),
-                owner_set: owner_set.clone(),
+            Field {
+                field: field_set.clone(),
+                owner: owner_set.clone(),
             },
         );
         Ok(())
@@ -174,9 +199,9 @@ impl CheckerState {
         };
         self.variant_fields.insert(
             name.clone(),
-            SetField {
-                field_set: field_set.clone(),
-                owner_set: owner_set.clone(),
+            Field {
+                field: field_set.clone(),
+                owner: owner_set.clone(),
             },
         );
         Ok(())
@@ -240,15 +265,82 @@ impl CheckerState {
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_record_field(&self, name: &String) -> Result<&SetField, CheckerError> {
+    pub fn lookup_record_field(&self, name: &String) -> Result<&Field<Set>, CheckerError> {
         self.record_fields
             .get(name)
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 
-    pub fn lookup_variant_field(&self, name: &String) -> Result<&SetField, CheckerError> {
+    pub fn lookup_variant_field(&self, name: &String) -> Result<&Field<Set>, CheckerError> {
         self.variant_fields
             .get(name)
             .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
     }
 }
+
+// -----------------------------------------------------------------------------
+// Signatures
+impl CheckerState {
+    fn assert_unbound_signature(&self, name: &String) -> Result<(), CheckerError> {
+        if self.wf_signatures.contains_key(name) {
+            Err(CheckerError::Rebinding(name.clone()))
+        } else {
+            Ok(())
+        }
+    }
+
+    // fn assert_unbound_instance(&self, name: &String) -> Result<(), CheckerError> {
+    //     if self.wf_instances.contains_key(name) {
+    //         Err(CheckerError::Rebinding(name.clone()))
+    //     } else {
+    //         Ok(())
+    //     }
+    // }
+
+    #[instrument(skip(self), level = "debug", fields(%name, %field_signature, %owner_signature))]
+    fn add_signature_field(
+        &mut self,
+        name: &String,
+        field_signature: &Signature,
+        owner_signature: &Signature,
+    ) -> Result<(), CheckerError> {
+        if let Some(signature_ref) = self.signature_fields.get(name) {
+            self.assert_correct_owner(name, signature_ref, owner_signature)?;
+        };
+        self.signature_fields.insert(
+            name.clone(),
+            Field {
+                field: field_signature.clone(),
+                owner: owner_signature.clone(),
+            },
+        );
+        Ok(())
+    }
+
+    #[instrument(skip(self), level = "debug", fields(%name, %signature))]
+    pub fn add_signature(
+        &mut self,
+        name: &String,
+        signature: Signature,
+    ) -> Result<(), CheckerError> {
+        self.assert_unbound_signature(name)?;
+
+        match &signature {
+            Signature::Theory(fields) => {
+                for SigField {
+                    name: field_name,
+                    signature: field_sig,
+                } in fields
+                {
+                    self.add_signature_field(field_name, field_sig, &signature)?;
+                }
+            }
+            // TODO: is there more?
+            _ => (),
+        };
+
+        self.wf_signatures.insert(name.clone(), signature);
+
+        Ok(())
+    }
+}