diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/checker_set.rs | 51 | ||||
| -rw-r--r-- | src/checker_state.rs | 8 |
2 files changed, 37 insertions, 22 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs index db47c14..93ba4b3 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -43,9 +43,15 @@ impl CheckerState { } } - fn _check_literal_set_helper(&self, claimed: &Set, should_be: Set) -> Result<(), CheckerError> { + fn _check_literal_set_helper( + &self, + value: ElementValue, + claimed: &Set, + should_be: Set, + ) -> Result<(), CheckerError> { if !self.set_equal(claimed, &should_be) { Err(CheckerError::WrongSetForElement { + value: value.clone(), claimed: claimed.clone(), real: should_be, }) @@ -54,54 +60,57 @@ impl CheckerState { } } - #[instrument(skip(self), level = "debug", fields(%element, %set))] + #[instrument(skip(self), level = "debug", fields(%value, %set))] pub fn check_element( &self, - element: ElementValue, + value: ElementValue, set: &Set, ) -> Result<ElementValue, CheckerError> { - match element { + match value { // This arm ensures that if we ever in the position of obtaining a // hypothetical from a call to check_element, in the context of // check_element, we can safely ignore its payload. I'll point this // out later as (*) - ElementValue::Hypothetical(h_set) => { + ElementValue::Hypothetical(ref h_set) => { if !self.set_equal(set, &h_set) { Err(CheckerError::WrongSetForElement { + value: value.clone(), claimed: set.clone(), - real: h_set, + real: h_set.clone(), }) } else { - Ok(ElementValue::Hypothetical(h_set)) + Ok(value) } } ElementValue::Concrete(ref element @ Element::Literal(ref lit)) => { + let value = value.clone(); // we may infer the type from the element match lit { Literal::Int(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Int))?; + self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Int))?; } Literal::Nat(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Nat))?; + self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Nat))?; } Literal::Str(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Str))?; + self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Str))?; } Literal::Bool(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Bool))?; + self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Bool))?; } Literal::Float(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Float))?; + self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Float))?; } } Ok(element.clone().into()) } - ElementValue::Concrete(Element::Var(v)) => { + ElementValue::Concrete(Element::Var(ref v)) => { 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) { return Err(CheckerError::WrongSetForElement { + value: value.clone(), claimed: set.clone(), real: lookup.set.clone(), }); @@ -165,8 +174,8 @@ impl CheckerState { }) } ElementValue::Concrete(Element::Project { - element: inner, - field, + element: ref inner, + ref field, }) => { // globally unique projections mean we know what the sets going // in and out must be @@ -178,13 +187,14 @@ impl CheckerState { // enforce the correct typing of the claimed result if !self.set_equal(set, field_set) { return Err(CheckerError::WrongSetForElement { + value, claimed: set.clone(), real: field_set.clone(), }); } // enforce the correct typing of the element - let inner = self.check_element((*inner).into(), owner_set)?; + let inner = self.check_element((*inner.clone()).into(), owner_set)?; match inner { ElementValue::Concrete(inner) => { // Unfortunately we still have to do something nasty here to obtain the data @@ -195,7 +205,7 @@ impl CheckerState { }; let sub_element = assignations .into_iter() - .find(|a| a.name == field) + .find(|a| a.name == *field) .expect( "invariant violation: record missing field that was type-checked", ) @@ -209,8 +219,8 @@ impl CheckerState { } } ElementValue::Concrete(Element::Inject { - element: inner, - field, + element: ref inner, + ref field, }) => { // globally unique injections mean that we know what the sets // going in and out must be, but compared to projections their @@ -223,13 +233,14 @@ impl CheckerState { // enforce the correct typing of the claimed result if !self.set_equal(set, owner_set) { return Err(CheckerError::WrongSetForElement { + value, claimed: set.clone(), real: owner_set.clone(), }); } // enforce the correct typing of the element - let element = self.check_element((*inner).into(), field_set)?; + let element = self.check_element((*inner.clone()).into(), field_set)?; match element { ElementValue::Concrete(element) => Ok(Element::Inject { diff --git a/src/checker_state.rs b/src/checker_state.rs index 19a7c51..86f229e 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -13,8 +13,12 @@ pub enum CheckerError { Rebinding(String), #[display("The following functionality is unimplemented: {_0}")] Unimplemented(String), - #[display("Element claimed to belong to {claimed} but actually belongs to {real}")] - WrongSetForElement { claimed: Set, real: Set }, + #[display("Element {value} claimed to belong to {claimed} but actually belongs to {real}")] + WrongSetForElement { + value: ElementValue, + claimed: Set, + real: Set, + }, #[display("Element {element} does belong to set {claimed}: {reason}")] ElementDoesNotBelong { element: Element, |