diff options
Diffstat (limited to 'src/checker_signature.rs')
| -rw-r--r-- | src/checker_signature.rs | 83 |
1 files changed, 73 insertions, 10 deletions
diff --git a/src/checker_signature.rs b/src/checker_signature.rs index cc6cadc..ab54fd1 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -10,6 +10,7 @@ impl CheckerState { pub fn check_signature(&self, signature: &Signature) -> Result<Signature, CheckerError> { match signature { Signature::Set => Ok(Signature::Set), + Signature::FromSet(set) => Ok(Signature::FromSet(self.check_set(set)?)), Signature::Var(v) => { let deref = self.lookup_signature(&v)?; Ok(deref.clone()) @@ -64,6 +65,7 @@ impl CheckerState { .into_iter() .map(|Param { name, set }| { let canonical = ctx.make_element_binding(name, set.clone())?; + let set = ctx.check_set(&set)?; Ok(Param { name: canonical, set, @@ -129,6 +131,22 @@ impl CheckerState { Ok(Instance::SetCoerce(set)) } } + Instance::ElementCoerce(element) => { + if let Some(signature) = signature { + let Signature::FromSet(set) = signature else { + return Err(CheckerError::WrongSignatureForInstance { + value: instance.clone().into(), + real: Signature::FromSet(Set::Var("_".to_string())), + claimed: signature.clone(), + }); + }; + let element = self.check_element(element, set)?; + Ok(Instance::ElementCoerce(element)) + } else { + // todo!("how do we handle check_element without a set?"); + Ok(Instance::ElementCoerce(element.clone())) + } + } Instance::Var(v) => { // Exactly the same discipline as for Element::Var, see there // for some sparse comments @@ -260,7 +278,11 @@ impl CheckerState { .instance; Ok(sub_element) } - _ => panic!( + Instance::For { .. } + | Instance::ElementCoerce(_) + | Instance::SetCoerce(_) + | Instance::App { .. } + | Instance::Case { .. } => panic!( "invariant violation: check_instance returned neither a record or stuck computation for record set" ), } @@ -314,11 +336,21 @@ impl CheckerState { ), }; + let posit_equality_with = match &scrutinee { + Element::Var(v) => Some(v.clone()), + Element::Inject { .. } + | Element::Project { .. } + | Element::Case { .. } + | Element::Literal(_) + | Element::Record(_) => None, + }; + let mut computed_output = None; let mut processed_arms = Vec::new(); for arm in arms { let OwnedField { - field: field_set, .. + field: field_set, + owner, } = self.lookup_variant_field(&arm.tag)?; let mut ctx = self.clone(); @@ -330,7 +362,15 @@ impl CheckerState { { let canonical = ctx.make_element_definition(binding_name, inner.clone(), binding_set)?; - let output = ctx.check_instance((&arm.body).into(), signature)?; + let this_signature = if let Some(signature) = signature { + let signature = ctx.check_signature(signature)?; + Some(signature) + } else { + None + }; + + let output = + ctx.check_instance((&arm.body).into(), this_signature.as_ref())?; if matches!(computed_output, Some(_)) { panic!( "invariant violation: we somehow matched multiple arms in case analysis" @@ -344,7 +384,26 @@ impl CheckerState { } } else { let canonical = ctx.make_element_binding(binding_name, binding_set)?; - let body = ctx.check_instance((&arm.body).into(), signature)?; + if let Some(ref scrutinee_var) = posit_equality_with { + ctx.add_element( + scrutinee_var.clone(), + Element::Inject { + field: arm.tag.clone(), + element: Box::new(Element::Var(canonical.clone())), + } + .into(), + owner.clone(), + )?; + }; + let this_signature = if let Some(signature) = signature { + let signature = ctx.check_signature(signature)?; + Some(signature) + } else { + None + }; + + let body = + ctx.check_instance((&arm.body).into(), this_signature.as_ref())?; CaseArm { tag: arm.tag.clone(), bound: canonical, @@ -508,7 +567,7 @@ impl CheckerState { // nevertheless we need the tiniest amount of bidirectionality // here to deal with case, project, and var recursively - let subject_sig: Option<Signature> = self.stuck_subject_signature(&subject)?; + let subject_sig: Option<Signature> = self._stuck_subject_signature(&subject)?; if let Some(subject_sig) = subject_sig { let Signature::Ext { params, codomain } = subject_sig else { @@ -567,7 +626,7 @@ impl CheckerState { ctx.check_instance(&residual, signature) } } - Instance::Record(_) | Instance::SetCoerce(_) => { + Instance::Record(_) | Instance::SetCoerce(_) | Instance::ElementCoerce(_) => { Err(CheckerError::NonFunctionalInstance { instance: subject, elements: args, @@ -611,7 +670,7 @@ impl CheckerState { Ok((ctx, checked)) } - fn stuck_subject_signature(&self, inst: &Instance) -> Result<Option<Signature>, CheckerError> { + fn _stuck_subject_signature(&self, inst: &Instance) -> Result<Option<Signature>, CheckerError> { match inst { Instance::Var(v) => Ok(Some(self.lookup_instance(v)?.container.clone())), Instance::Project { field, .. } => { @@ -620,10 +679,14 @@ impl CheckerState { // All arms of a stuck Case share a signature by the case // elimination typing rule, and we've already expanded the body, so // we can pick any arm. - Instance::Case { arms, .. } => self - .stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body), - Instance::For { .. } | Instance::Record(_) | Instance::SetCoerce(_) => Ok(None), + // TODO! this is wrong! + Instance::Case { arms, .. } => self + ._stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body), + Instance::ElementCoerce(_) + | Instance::For { .. } + | Instance::Record(_) + | Instance::SetCoerce(_) => Ok(None), Instance::App { .. } => unreachable!( "invariant violation: _stuck_head_signature called on a left-nested App" |