diff options
Diffstat (limited to 'src/checker_signature.rs')
| -rw-r--r-- | src/checker_signature.rs | 56 |
1 files changed, 35 insertions, 21 deletions
diff --git a/src/checker_signature.rs b/src/checker_signature.rs index b979f54..8e99d3c 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -6,7 +6,7 @@ use tracing::instrument; impl CheckerState { #[instrument(skip(self), level = "debug", fields(%signature))] - pub fn check_signature(&self, signature: Signature) -> Result<Signature, CheckerError> { + pub fn check_signature(&self, signature: &Signature) -> Result<Signature, CheckerError> { match signature { Signature::Set => Ok(Signature::Set), Signature::Var(v) => { @@ -16,14 +16,14 @@ impl CheckerState { Signature::Ext { params, codomain } => { let mut ctx = self.clone(); let params = params - .into_iter() + .iter() .map(|p| { - let set = ctx.check_set(p.set.clone())?; + let set = ctx.check_set(&p.set)?; let canon = ctx.make_element_binding(p.name.clone(), set.clone())?; Ok(Param { set, name: canon }) }) .collect::<Result<Vec<_>, _>>()?; - let codomain = Box::new(ctx.check_signature(*codomain)?); + let codomain = Box::new(ctx.check_signature(codomain)?); Ok(Signature::Ext { params, codomain }) } Signature::Theory(fields) => { @@ -40,7 +40,10 @@ impl CheckerState { Set::ClaimedSet(Instance::Var(name.clone())).into(), )?; } - new_fields.push(SigField { name, signature }); + new_fields.push(SigField { + name: name.clone(), + signature, + }); // We must iteratively add the entire signature so that // field lookup does something, as we rely on that for type // checking. We could hack together a signature i suppose, @@ -57,11 +60,11 @@ impl CheckerState { #[instrument(skip(self), level = "debug", fields(%instance, ?signature))] pub fn check_instance( &self, - instance: Instance, + instance: &Instance, signature: Option<&Signature>, ) -> Result<Instance, CheckerError> { match instance { - Instance::SetCoerce(ref set) => { + Instance::SetCoerce(set) => { if let Some(signature) = signature && *signature != Signature::Set { @@ -71,14 +74,14 @@ impl CheckerState { claimed: signature.clone(), }); }; - let set = Box::new(self.check_set(*set.clone())?); + let set = Box::new(self.check_set(set)?); if let Set::ClaimedSet(inner) = *set { Ok(inner) } else { Ok(Instance::SetCoerce(set)) } } - Instance::Var(ref v) => { + Instance::Var(v) => { // Exactly the same discipline as for Element::Var, see there // for some sparse comments let lookup = self.lookup_instance(&v)?; @@ -97,7 +100,7 @@ impl CheckerState { Ok(Instance::Var(v.clone())) } } - Instance::Record(ref assignations) => { + Instance::Record(assignations) => { // once again, mutatis mutandis from elements let (instance_fnames, instance_finstances): (Vec<String>, Vec<&Instance>) = assignations @@ -146,17 +149,14 @@ impl CheckerState { } let sub_els = zip(instance_finstances, signature_fsigs) - .map(|(e_f, e_s)| self.check_instance(e_f.clone(), (&e_s).into())) + .map(|(e_f, e_s)| self.check_instance(e_f, (&e_s).into())) .collect::<Result<Vec<_>, _>>()?; let assignations = zip(instance_fnames, sub_els) .map(|(name, instance)| InstAssign { name, instance }) .collect(); Ok(Instance::Record(assignations)) } - Instance::Project { - ref instance, - ref field, - } => { + Instance::Project { instance, field } => { let Field { field: field_signature, owner: owner_signature, @@ -172,7 +172,7 @@ impl CheckerState { }); } - let inner = self.check_instance(*instance.clone(), owner_signature.into())?; + let inner = self.check_instance(instance, owner_signature.into())?; match inner { Instance::Var(_) | Instance::Project { .. } => Ok(Instance::Project { @@ -198,7 +198,7 @@ impl CheckerState { todo!("instance for") } Instance::App(inner, element) => { - let inner = self.check_instance(*inner, None)?; + let inner = self.check_instance(inner, None)?; match &inner { Instance::Var(v) => { let field = self.lookup_signature_field(&v)?; @@ -219,9 +219,23 @@ impl CheckerState { real: field.owner.clone(), }); }; - // TODO: we need to assert (somewhere else) that ext has >=1 params - // TODO: in the special case that params.len() == 1 we need to do something with codomain - let element = self.check_element(*element, ¶ms[0].set)?; + if params.is_empty() { + panic!( + "It should have been impossible to construct an Ext with no params, but here we are" + ); + } + if params.len() == 1 + && let Some(signature) = signature + { + if !self.equal(&**codomain, signature) { + return Err(CheckerError::WrongSignatureForInstance { + value: instance.clone().into(), + claimed: signature.clone(), + real: *codomain.clone(), + }); + } + } + let element = self.check_element(element, ¶ms[0].set)?; Ok(Instance::App( Box::new(Instance::Var(v.clone())), Box::new(element), @@ -233,7 +247,7 @@ impl CheckerState { Instance::Record(_) | Instance::SetCoerce(_) => { Err(CheckerError::NonFunctionalInstance { instance: inner, - element: *element, + element: *element.clone(), }) } Instance::Project { .. } | Instance::App(_, _) => panic!( |