diff options
| -rw-r--r-- | src/checker.rs | 9 | ||||
| -rw-r--r-- | src/checker_set.rs | 38 | ||||
| -rw-r--r-- | src/checker_signature.rs | 13 | ||||
| -rw-r--r-- | src/checker_state.rs | 154 | ||||
| -rw-r--r-- | src/main.rs | 1 |
5 files changed, 162 insertions, 53 deletions
diff --git a/src/checker.rs b/src/checker.rs index 1760c0e..05ebca2 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -19,12 +19,12 @@ impl CheckerState { debug!(%self, %decl); match decl { Decl::Set { name, set } => { - let set = self.check_set(set)?; + let set = self.check_set(set.clone())?; self.add_set(name, set) } Decl::Element { name, element, set } => { - let set = self.check_set(set)?; + let set = self.check_set(set.clone())?; let element = self.check_element(element.clone().into(), &set)?; if matches!(element, ElementValue::Hypothetical(_)) { panic!( @@ -33,8 +33,9 @@ impl CheckerState { } self.add_element(name.clone(), element, set) } - Decl::Signature { .. } => { - return Err(CheckerError::Unimplemented("signatures".to_string())); + Decl::Signature { name, signature } => { + let signature = self.check_signature(signature.clone())?; + self.add_signature(name, signature) } Decl::Instance { .. } => { return Err(CheckerError::Unimplemented("instances".to_string())); diff --git a/src/checker_set.rs b/src/checker_set.rs index 93ba4b3..2ea0c3d 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -6,12 +6,12 @@ use tracing::instrument; impl CheckerState { #[instrument(skip(self), level = "debug", fields(%set))] - pub fn check_set(&self, set: &Set) -> Result<Set, CheckerError> { + pub fn check_set(&self, set: Set) -> Result<Set, CheckerError> { match set { Set::BuiltIn(_) => Ok(set.clone()), Set::Record(fields) => { let fields = fields - .iter() + .into_iter() .map(|RecordField { name, set }| { let set = self.check_set(set)?; Ok(RecordField { @@ -24,7 +24,7 @@ impl CheckerState { } Set::Variant(fields) => { let fields = fields - .iter() + .into_iter() .map(|VariantField { name, set }| { let set = self.check_set(set)?; Ok(VariantField { @@ -37,7 +37,7 @@ impl CheckerState { } Set::ClaimedSet(_) => Err(CheckerError::Unimplemented("instances as sets".to_string())), Set::Var(v) => { - let deref = self.lookup_set(v)?; + let deref = self.lookup_set(&v)?; Ok(deref.clone()) } } @@ -49,7 +49,7 @@ impl CheckerState { claimed: &Set, should_be: Set, ) -> Result<(), CheckerError> { - if !self.set_equal(claimed, &should_be) { + if !self.equal(claimed, &should_be) { Err(CheckerError::WrongSetForElement { value: value.clone(), claimed: claimed.clone(), @@ -72,7 +72,7 @@ impl CheckerState { // check_element, we can safely ignore its payload. I'll point this // out later as (*) ElementValue::Hypothetical(ref h_set) => { - if !self.set_equal(set, &h_set) { + if !self.equal(set, &h_set) { Err(CheckerError::WrongSetForElement { value: value.clone(), claimed: set.clone(), @@ -108,7 +108,7 @@ impl CheckerState { let lookup = self.lookup_element(&v)?; // we have previously done the work to discover the type of // this element, so what we're claiming now must match! - if !self.set_equal(set, &lookup.set) { + if !self.equal(set, &lookup.set) { return Err(CheckerError::WrongSetForElement { value: value.clone(), claimed: set.clone(), @@ -179,13 +179,13 @@ impl CheckerState { }) => { // globally unique projections mean we know what the sets going // in and out must be - let SetField { - field_set, - owner_set, + let Field { + field: field_set, + owner: owner_set, } = self.lookup_record_field(&field)?; // enforce the correct typing of the claimed result - if !self.set_equal(set, field_set) { + if !self.equal(set, field_set) { return Err(CheckerError::WrongSetForElement { value, claimed: set.clone(), @@ -225,13 +225,13 @@ impl CheckerState { // globally unique injections mean that we know what the sets // going in and out must be, but compared to projections their // roles are here interchanged - let SetField { - field_set, - owner_set, + let Field { + field: field_set, + owner: owner_set, } = self.lookup_variant_field(&field)?; // enforce the correct typing of the claimed result - if !self.set_equal(set, owner_set) { + if !self.equal(set, owner_set) { return Err(CheckerError::WrongSetForElement { value, claimed: set.clone(), @@ -270,10 +270,10 @@ impl CheckerState { // arms agree on the set to which the scrutinee should belong let arm_owners = arms .iter() - .map(|ca| self.lookup_variant_field(&ca.tag).map(|sf| &sf.owner_set)) + .map(|ca| self.lookup_variant_field(&ca.tag).map(|sf| &sf.owner)) .collect::<Result<Vec<_>, _>>()?; let owner = arm_owners[0]; // safe because of the above decision about bottom - if !arm_owners.iter().all(|o| self.set_equal(owner, o)) { + if !arm_owners.iter().all(|o| self.equal(owner, o)) { return Err(CheckerError::IncosistentCaseScrutineeSet(element.clone())); } @@ -323,7 +323,9 @@ impl CheckerState { // case record the end result let mut computed_output = None; for arm in arms { - let SetField { field_set, .. } = self.lookup_variant_field(&arm.tag)?; + let Field { + field: field_set, .. + } = self.lookup_variant_field(&arm.tag)?; // TODO: if we were worried about overhead we'd have a separate // locals stack, though truly if we were worried about overhead diff --git a/src/checker_signature.rs b/src/checker_signature.rs new file mode 100644 index 0000000..8fc982a --- /dev/null +++ b/src/checker_signature.rs @@ -0,0 +1,13 @@ +use crate::ast::*; +use crate::checker_state::*; + +use tracing::instrument; + +impl CheckerState { + #[instrument(skip(self), level = "debug", fields(%signature))] + pub fn check_signature(&self, signature: Signature) -> Result<Signature, CheckerError> { + Err(CheckerError::Unimplemented( + "signature checking".to_string(), + )) + } +} 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(()) + } +} diff --git a/src/main.rs b/src/main.rs index b0bc33c..2b798e1 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,6 +1,7 @@ mod ast; mod checker; mod checker_set; +mod checker_signature; mod checker_state; mod parser; |