diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/checker.rs | 7 | ||||
| -rw-r--r-- | src/checker_state.rs | 33 |
2 files changed, 20 insertions, 20 deletions
diff --git a/src/checker.rs b/src/checker.rs index 976b9fb..da4463c 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -19,20 +19,25 @@ impl CheckerState { debug!(%self, %decl); match decl { Decl::Set { name, set } => { + self.assert_unbound_set(name)?; let set = self.check_set(set.clone())?; self.add_set(name, set) } Decl::Element { name, element, set } => { + self.assert_unbound_element(name)?; let set = self.check_set(set.clone())?; let element = self.check_element(element.clone().into(), &set)?; self.add_element(name.clone(), element.into(), set) } Decl::Signature { name, signature } => { + self.assert_unbound_signature(name)?; let signature = self.check_signature(signature.clone())?; self.add_signature(name, signature) } - Decl::Instance { .. } => { + Decl::Instance { name, .. } => { + self.assert_unbound_instance(name)?; + return Err(CheckerError::Unimplemented("instances".to_string())); } }?; diff --git a/src/checker_state.rs b/src/checker_state.rs index a14a6e4..73edd10 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -48,8 +48,10 @@ pub struct Field<T: std::fmt::Display> { #[derive(Display, Clone)] pub enum Value<Term: std::fmt::Display, Type: std::fmt::Display> { + /// The storage format for concrete terms. Concrete(Term), #[display("_ : {_0}")] + /// The storage format for formal bindings. Hypothetical(Type), } @@ -122,10 +124,8 @@ 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. Because of our invariant we don't -// actually need to do anything non-trivial here. - +// we work very hard to store canonical forms so that equality is purely +// structural. This approach may or may not survive contact with reality. pub trait DecideEquality<T> { fn equal(&self, thing_a: &T, thing_b: &T) -> bool; } @@ -167,7 +167,7 @@ impl CheckerState { // ----------------------------------------------------------------------------- // Sets impl CheckerState { - fn assert_unbound_set(&self, name: &String) -> Result<(), CheckerError> { + pub fn assert_unbound_set(&self, name: &String) -> Result<(), CheckerError> { if self.wf_sets.contains_key(name) { Err(CheckerError::Rebinding(name.clone())) } else { @@ -175,7 +175,7 @@ impl CheckerState { } } - fn assert_unbound_element(&self, name: &String) -> Result<(), CheckerError> { + pub fn assert_unbound_element(&self, name: &String) -> Result<(), CheckerError> { if self.wf_elements.contains_key(name) { Err(CheckerError::Rebinding(name.clone())) } else { @@ -225,7 +225,6 @@ impl CheckerState { #[instrument(skip(self), level = "debug", fields(%name, %set))] pub fn add_set(&mut self, name: &String, set: Set) -> Result<(), CheckerError> { - self.assert_unbound_set(name)?; match &set { Set::Record(fields) => { for RecordField { @@ -258,7 +257,6 @@ impl CheckerState { element: Value<Element, Set>, set: Set, ) -> Result<(), CheckerError> { - self.assert_unbound_element(&name)?; self.wf_elements.insert( name, Checked { @@ -297,7 +295,7 @@ impl CheckerState { // ----------------------------------------------------------------------------- // Signatures impl CheckerState { - fn assert_unbound_signature(&self, name: &String) -> Result<(), CheckerError> { + pub fn assert_unbound_signature(&self, name: &String) -> Result<(), CheckerError> { if self.wf_signatures.contains_key(name) { Err(CheckerError::Rebinding(name.clone())) } else { @@ -305,13 +303,13 @@ impl CheckerState { } } - // fn assert_unbound_instance(&self, name: &String) -> Result<(), CheckerError> { - // if self.wf_instances.contains_key(name) { - // Err(CheckerError::Rebinding(name.clone())) - // } else { - // Ok(()) - // } - // } + pub 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( @@ -339,8 +337,6 @@ impl CheckerState { name: &String, signature: Signature, ) -> Result<(), CheckerError> { - self.assert_unbound_signature(name)?; - match &signature { Signature::Theory(fields) => { for SigField { @@ -367,7 +363,6 @@ impl CheckerState { instance: InstanceValue, signature: Signature, ) -> Result<(), CheckerError> { - self.assert_unbound_element(&name)?; self.wf_instances.insert( name, Checked { |