diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/checker_set.rs | 4 | ||||
| -rw-r--r-- | src/checker_signature.rs | 52 | ||||
| -rw-r--r-- | src/checker_state.rs | 20 |
3 files changed, 61 insertions, 15 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs index 626f74d..98e10ec 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -276,7 +276,9 @@ impl CheckerState { .collect::<Result<Vec<_>, _>>()?; let owner = arm_owners[0]; // safe because of the above decision about bottom if !arm_owners.into_iter().all(|o| self.equal(owner, o)) { - return Err(CheckerError::IncosistentCaseScrutineeSet(element.clone())); + return Err(CheckerError::ElementInconsistentCaseScrutineeSet( + element.clone(), + )); } // all cases are handled diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 30598d3..beb0af6 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -232,7 +232,9 @@ impl CheckerState { let owner = arm_owners[0]; if !arm_owners.into_iter().all(|o| self.equal(owner, o)) { - todo!("inconsistent case scrutinee set"); + return Err(CheckerError::InstanceInconsistentCaseScrutineeSet( + instance.clone(), + )); } let Set::Variant(fields) = owner else { @@ -316,20 +318,39 @@ impl CheckerState { } => { if let Some(signature) = signature { if inst_params.is_empty() { - todo!("should be impossible"); + return Err(CheckerError::Unimplemented( + "instance for with empty params".to_string(), + )); }; let Signature::Ext { params: sig_params, codomain, } = signature else { - todo!("need to raise error"); + return Err(CheckerError::WrongSignatureForInstance { + real: Signature::Ext { + params: vec![Param { + name: "_".to_string(), + set: Set::Var("_".to_string()), + }], + codomain: Box::new(Signature::Var("_".to_string())), + }, + value: instance.clone().into(), + claimed: signature.clone(), + }); }; if sig_params.is_empty() { - todo!("should be impossible") + return Err(CheckerError::Unimplemented( + "extension signature with empty params".to_string(), + )); } if sig_params.len() != inst_params.len() { - todo!("this is a type error") + return Err(CheckerError::InstanceDoesNotBelong { + instance: instance.clone(), + reason: "instance and signature have differing number of parameters" + .to_string(), + claimed: signature.clone(), + }); } let mut ctx = self.clone(); let inst_params = zip(inst_params, sig_params) @@ -347,7 +368,12 @@ impl CheckerState { let inst_s = ctx.check_set(inst_s)?; let set_s = ctx.check_set(set_s)?; if !ctx.equal(&inst_s, &set_s) { - todo!("type error") + return Err(CheckerError::InstanceDoesNotBelong{ + instance: instance.clone(), + claimed: signature.clone(), + reason: format!("the signature specifies set {} but in this position the instance has set {}", + set_s, inst_s), + }); } ctx.add_element( inst_n.clone(), @@ -431,7 +457,7 @@ impl CheckerState { elements: args, }); }; - let (ctx, checked_args) = self._bind_args(¶ms, &args)?; + let (ctx, checked_args) = self._bind_args(instance, ¶ms, &args)?; if let Some(expected) = signature { let result_sig = if args.len() == params.len() { @@ -470,7 +496,7 @@ impl CheckerState { match subject { Instance::For { params, body } => { - let (ctx, _checked) = self._bind_args(¶ms, &args)?; + let (ctx, _checked) = self._bind_args(instance, ¶ms, &args)?; if args.len() == params.len() { ctx.check_instance(&body, signature) } else { @@ -503,15 +529,15 @@ impl CheckerState { fn _bind_args( &self, + instance: &Instance, params: &[Param], args: &[Element], ) -> Result<(CheckerState, Vec<Element>), CheckerError> { if args.len() > params.len() { - todo!( - "over-application: {} args to a function of arity {}", - args.len(), - params.len() - ); + return Err(CheckerError::OverApplication { + instance: instance.clone(), + applied_to: args.len(), + }); } let mut ctx = self.clone(); let checked = zip(params.iter(), args.iter()) diff --git a/src/checker_state.rs b/src/checker_state.rs index a8473ff..3404a35 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -12,24 +12,33 @@ use std::sync::atomic::{AtomicUsize, Ordering}; pub enum CheckerError { #[display("Unbound: {_0}")] Unbound(String), + #[display("Rebinding: {_0}")] Rebinding(String), + #[display("The following functionality is unimplemented: {_0}")] Unimplemented(String), + #[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, claimed: Set, reason: String, }, + + #[display("Case analysis {_0} does not have consistent set for scrutinee")] + ElementInconsistentCaseScrutineeSet(Element), + #[display("Case analysis {_0} does not have consistent set for scrutinee")] - IncosistentCaseScrutineeSet(Element), + InstanceInconsistentCaseScrutineeSet(Instance), + #[display("Incomplete case analysis: covered [{}] but required [{}]", found.join(", "), required.join(", ") @@ -38,23 +47,32 @@ pub enum CheckerError { found: Vec<String>, required: Vec<String>, }, + #[display("Instance {value} claimed to belong to {claimed} but actually belongs to {real}")] WrongSignatureForInstance { value: InstanceValue, claimed: Signature, real: Signature, }, + #[display("Instance {instance} is not of signature {claimed}: {reason}")] InstanceDoesNotBelong { instance: Instance, claimed: Signature, reason: String, }, + #[display("Non-functional instance {instance} found in application to elements {}", elements.iter().map(|e| e.to_string()).collect::<Vec<_>>().join(" "))] NonFunctionalInstance { instance: Instance, elements: Vec<Element>, }, + + #[display("Instance {instance} applied to too many arguments: {applied_to}")] + OverApplication { + instance: Instance, + applied_to: usize, + }, } // ----------------------------------------------------------------------------- |