diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/checker.rs | 9 | ||||
| -rw-r--r-- | src/checker_set.rs | 193 |
2 files changed, 93 insertions, 109 deletions
diff --git a/src/checker.rs b/src/checker.rs index 05ebca2..976b9fb 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -1,5 +1,5 @@ use crate::ast::*; -use crate::checker_state::{CheckerError, CheckerState, ElementValue}; +use crate::checker_state::{CheckerError, CheckerState}; use tracing::{debug, instrument}; @@ -26,12 +26,7 @@ impl CheckerState { Decl::Element { name, element, set } => { let set = self.check_set(set.clone())?; let element = self.check_element(element.clone().into(), &set)?; - if matches!(element, ElementValue::Hypothetical(_)) { - panic!( - "invariant violation: from concrete values at the top level we returned a hypothetical value" - ); - } - self.add_element(name.clone(), element, set) + self.add_element(name.clone(), element.into(), set) } Decl::Signature { name, signature } => { let signature = self.check_signature(signature.clone())?; diff --git a/src/checker_set.rs b/src/checker_set.rs index 7ff6e4a..729ce08 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -48,13 +48,13 @@ impl CheckerState { fn _check_literal_set_helper( &self, - value: ElementValue, + value: Element, claimed: &Set, should_be: Set, ) -> Result<(), CheckerError> { if !self.equal(claimed, &should_be) { Err(CheckerError::WrongSetForElement { - value: value.clone(), + value: value.clone().into(), claimed: claimed.clone(), real: should_be, }) @@ -63,30 +63,11 @@ impl CheckerState { } } - #[instrument(skip(self), level = "debug", fields(%value, %set))] - pub fn check_element( - &self, - value: ElementValue, - set: &Set, - ) -> Result<ElementValue, CheckerError> { - 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 (*) - Value::Hypothetical(ref h_set) => { - if !self.equal(set, &h_set) { - Err(CheckerError::WrongSetForElement { - value: value.clone(), - claimed: set.clone(), - real: h_set.clone(), - }) - } else { - Ok(value) - } - } - Value::Concrete(ref element @ Element::Literal(ref lit)) => { - let value = value.clone(); + #[instrument(skip(self), level = "debug", fields(%element, %set))] + pub fn check_element(&self, element: Element, set: &Set) -> Result<Element, CheckerError> { + match element { + Element::Literal(ref lit) => { + let value = element.clone(); // we may infer the type from the element match lit { Literal::Int(_) => { @@ -107,22 +88,30 @@ impl CheckerState { } Ok(element.clone().into()) } - Value::Concrete(Element::Var(ref v)) => { + 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.equal(set, &lookup.container) { return Err(CheckerError::WrongSetForElement { - value: value.clone(), + value: element.clone().into(), claimed: set.clone(), real: lookup.container.clone(), }); } - Ok(lookup.value.clone()) + // If we found a formal binding, we have no value to report. + // This is the ONLY source of Var as a return value for + // check_element, so in other branches we condition our logic + // for formal bindings on finding Var after recursing. + if let ElementValue::Concrete(ref deref) = lookup.value { + Ok(deref.clone()) + } else { + Ok(Element::Var(v.clone())) + } } - Value::Concrete(ref concrete @ Element::Record(ref assignations)) => { + Element::Record(ref assignations) => { let rej = |reason| CheckerError::ElementDoesNotBelong { - element: concrete.clone(), + element: element.clone(), claimed: set.clone(), reason, }; @@ -162,24 +151,17 @@ impl CheckerState { let sub_els = zip(element_felements, set_fsets) .map(|(e_f, e_s)| self.check_element(e_f.clone().into(), &e_s)) .collect::<Result<Vec<_>, _>>()?; - // rebuild, hypotheticals are contagious + // rebuild let assignations = zip(element_fnames, sub_els) - .map(|(name, element)| match element { - Value::Concrete(element) => Some(ElemAssign { name, element }), - Value::Hypothetical(_) => None, - }) + .map(|(name, element)| ElemAssign { name, element }) .collect(); // resign? - Ok(if let Some(assignations) = assignations { - Element::Record(assignations).into() - } else { - Value::Hypothetical(set.clone()) - }) + Ok(Element::Record(assignations)) } - Value::Concrete(Element::Project { + Element::Project { element: ref inner, ref field, - }) => { + } => { // globally unique projections mean we know what the sets going // in and out must be let Field { @@ -190,41 +172,45 @@ impl CheckerState { // enforce the correct typing of the claimed result if !self.equal(set, field_set) { return Err(CheckerError::WrongSetForElement { - value, + value: element.clone().into(), claimed: set.clone(), real: field_set.clone(), }); } // enforce the correct typing of the element - let inner = self.check_element((*inner.clone()).into(), owner_set)?; + let inner = self.check_element(*inner.clone(), owner_set)?; + + // Unfortunately we still have to do something nasty here to + // obtain the data match inner { - Value::Concrete(inner) => { - // Unfortunately we still have to do something nasty here to obtain the data - let Element::Record(assignations) = inner else { - panic!( - "invariant violation: check_element returned non-record for record set" - ); - }; + // We're stuck on something that bottoms out in a binding + // blocking computation, nothing to be done here + Element::Var(_) | Element::Project { .. } | Element::Case { .. } => { + Ok(Element::Project { + element: Box::new(inner), + field: field.clone(), + }) + } + Element::Record(assignations) => { let sub_element = assignations .into_iter() .find(|a| a.name == *field) .expect( "invariant violation: record missing field that was type-checked", ) - .element - .clone(); - - Ok(sub_element.into()) + .element; + Ok(sub_element) } - // correct by (*) - Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())), + _ => panic!( + "invariant violation: check_element returned neither a record or stuck computation for record set" + ), } } - Value::Concrete(Element::Inject { + Element::Inject { 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 // roles are here interchanged @@ -236,31 +222,24 @@ impl CheckerState { // enforce the correct typing of the claimed result if !self.equal(set, owner_set) { return Err(CheckerError::WrongSetForElement { - value, + value: element.clone().into(), claimed: set.clone(), real: owner_set.clone(), }); } // enforce the correct typing of the element - let element = self.check_element((*inner.clone()).into(), field_set)?; - - match element { - Value::Concrete(element) => Ok(Element::Inject { - element: Box::new(element), - field: field.clone(), - } - .into()), - // correct by (*) - Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())), - } + let element = self.check_element(*inner.clone(), field_set)?; + Ok(Element::Inject { + element: Box::new(element), + field: field.clone(), + }) } - Value::Concrete( - ref element @ Element::Case { - ref arms, - ref scrutinee, - }, - ) => { + + Element::Case { + ref arms, + ref scrutinee, + } => { // TODO: do we allow mapping out of bottom? if arms.is_empty() { return Err(CheckerError::Unimplemented( @@ -276,7 +255,7 @@ impl CheckerState { .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.equal(owner, o)) { + if !arm_owners.into_iter().all(|o| self.equal(owner, o)) { return Err(CheckerError::IncosistentCaseScrutineeSet(element.clone())); } @@ -305,62 +284,72 @@ impl CheckerState { // scrutinee must be of the same set that all the arms are // implying, in particular this implies that the following holds // `inner : self.lookup_variant_field(field).field_set` - let scrutinee = self.check_element((*scrutinee.clone()).into(), owner)?; + let scrutinee = self.check_element(*scrutinee.clone(), owner)?; // which variant are we, if any + let matching: Option<(String, Element)> = match scrutinee { - Value::Hypothetical(_) => None, - Value::Concrete(Element::Inject { - field, - element: inner, - }) => Some((field, *inner)), - _ => { - panic!( - "invariant violation: we believe element is of a variant set but it's not an injection" - ); - } + Element::Inject { + ref field, + element: ref inner, + } => Some((field.clone(), *inner.clone())), + // These are all the cases which could become stuck on a + // formal binding + Element::Var(_) | Element::Project { .. } | Element::Case { .. } => None, + Element::Literal(_) | Element::Record(_) => panic!( + "invariant violation: scrutinee is a non-variant value at variant set" + ), }; // for each arm, recurse with a concrete value (if we have one) // otherwise fall back to hypothetical elements; in the former // case record the end result let mut computed_output = None; + let mut processed_arms = Vec::new(); for arm in arms { 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 - // we'd not have NNN instances of clone elsewhere in the - // codebase and we wouldn't be eagerly evaluating all - // expressions fully. - let mut new_context = self.clone(); let binding_name = arm.bound.clone(); let binding_set = field_set.clone(); - if let Some((tag, inner)) = &matching + let body = if let Some((tag, inner)) = &matching && *tag == arm.tag { - new_context.add_element(binding_name, inner.clone().into(), binding_set)?; + new_context.add_element( + binding_name.clone(), + inner.clone().into(), + binding_set, + )?; let output = new_context.check_element(arm.body.clone().into(), set)?; if matches!(computed_output, Some(_)) { panic!( "invariant violation: we somehow matched multiple arms in case analysis" ) } - computed_output = Some(output); + computed_output = Some(output.clone()); + output } else { new_context.add_element( - binding_name, + binding_name.clone(), Value::Hypothetical(field_set.clone()), binding_set, )?; - new_context.check_element(arm.body.clone().into(), set)?; + new_context.check_element(arm.body.clone().into(), set)? }; + + processed_arms.push(CaseArm { + tag: arm.tag.clone(), + bound: binding_name, + body, + }); } - Ok(computed_output.unwrap_or(Value::Hypothetical(set.clone()))) + Ok(computed_output.unwrap_or(Element::Case { + scrutinee: Box::new(scrutinee), + arms: processed_arms, + })) } } } |