diff options
| -rw-r--r-- | src/checker_signature.rs | 191 | ||||
| -rw-r--r-- | src/parser.rs | 18 |
2 files changed, 138 insertions, 71 deletions
diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 2d5057f..42a581f 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -394,88 +394,143 @@ impl CheckerState { // signature = None, and in this mode all we want is to put // inner into a canonical form pushing stuck terms to the leaves // and simplifying everything else. - let inner = self.check_instance(inner, None)?; - println!("HERE {:?}, {:?}", inner, args); - match &inner { - Instance::Var(v) => { - println!("VAR {}", v); - let field = self.lookup_signature_field(&v)?; - let Signature::Ext { - ref params, - ref codomain, - } = field.field - else { + let subject = self.check_instance(inner, None)?; + + // the whole game here is to make sure that we have no left + // nesting, and that we're fully evaluated. If that's true then + // we don't need to come up with signatures for partial + // application. The parser already enforces this, but the + // cunning user may supply ASTs directly so we do this here as + // well. + let (subject, args) = match subject { + Instance::App { + instance: inner_inner, + args: inner_args, + } => { + let mut merged = inner_args; + merged.extend(args.iter().cloned()); + return self.check_instance( + &Instance::App { + instance: inner_inner, + args: merged, + }, + signature, + ); + } + other => (other, args.clone()), + }; + + let subject_sig: Option<Signature> = match &subject { + Instance::Var(v) => Some(self.lookup_instance(v)?.container.clone()), + Instance::Project { field, .. } => { + Some(self.lookup_signature_field(field)?.field.clone()) + } + // TODO: i think we need to handle case here + Instance::App { .. } + | Instance::Record(_) + | Instance::SetCoerce(_) + | Instance::For { .. } + | Instance::Case { .. } => None, + }; + + if let Some(subject_sig) = subject_sig { + let Signature::Ext { params, codomain } = subject_sig else { + return Err(CheckerError::NonFunctionalInstance { + instance: subject, + elements: args, + }); + }; + let (ctx, checked_args) = self._bind_args(¶ms, &args)?; + + if let Some(expected) = signature { + let result_sig = if args.len() == params.len() { + ctx.check_signature(&codomain)? + } else { + let remaining: Vec<Param> = params[args.len()..] + .iter() + .map(|p| { + let s = ctx.check_set(&p.set)?; + Ok(Param { + name: p.name.clone(), + set: s, + }) + }) + .collect::<Result<_, CheckerError>>()?; + let cod = ctx.check_signature(&codomain)?; + Signature::Ext { + params: remaining, + codomain: Box::new(cod), + } + }; + if !self.equal(expected, &result_sig) { return Err(CheckerError::WrongSignatureForInstance { - value: inner.clone().into(), - claimed: Signature::Ext { - params: vec![Param { - name: "...".to_string(), - set: Set::Var("...".to_string()), - }], - codomain: Box::new(Signature::Var("...".to_string())), - }, - real: field.owner.clone(), + value: subject.clone().into(), + claimed: expected.clone(), + real: result_sig, }); - }; - if params.is_empty() { - panic!( - "It should have been impossible to construct an Ext with no params, but here we are" - ); - } - if let Some(signature) = signature { - if !self.equal(&**codomain, signature) { - return Err(CheckerError::WrongSignatureForInstance { - value: instance.clone().into(), - claimed: signature.clone(), - real: *codomain.clone(), - }); - } } - todo!("finish") - // let element = self.check_element(args, ¶ms[0].set)?; - // Ok(Instance::App( - // Box::new(Instance::Var(v.clone())), - // Box::new(element), - // )) } + + return Ok(Instance::App { + instance: Box::new(subject), + args: checked_args, + }); + } + + match subject { Instance::For { params, body } => { - if params.is_empty() { - panic!( - "it should have been impossible to construct a for with no parameters, but here we are" - ); + let (ctx, _checked) = self._bind_args(¶ms, &args)?; + if args.len() == params.len() { + ctx.check_instance(&body, signature) + } else { + let residual = Instance::For { + params: params[args.len()..].to_vec(), + body, + }; + ctx.check_instance(&residual, signature) } - let mut ctx = self.clone(); - let first_set = ctx.check_set(¶ms[0].set)?; - todo!("finish this") - // let element_checked = self.check_element(args, &first_set)?; - // ctx.add_element(params[0].name.clone(), element_checked.into(), first_set)?; - // if params.len() == 1 { - // ctx.check_instance(body, signature) - // } else { - // let residual = Instance::For { - // params: params[1..].to_vec(), - // body: body.clone(), - // }; - // ctx.check_instance(&residual, signature) - // } } Instance::Record(_) | Instance::SetCoerce(_) => { Err(CheckerError::NonFunctionalInstance { - instance: inner, - elements: args.clone(), + instance: subject, + elements: args, }) } - Instance::Project { .. } | Instance::App { .. } | Instance::Case { .. } => { - println!("Stuck"); - // it would appear that we are stuck here, so our only - // choice is to continue to be so - Ok(Instance::App { - instance: Box::new(inner), - args: args.clone(), - }) + Instance::Case { .. } => { + todo!("App applied to a Case instance?"); + } + Instance::Var(_) | Instance::Project { .. } => { + unreachable!("handled in the stuck-head branch above") + } + Instance::App { .. } => { + unreachable!("handled by the merge-and-recurse branch above") } } } } } + + fn _bind_args( + &self, + 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() + ); + } + let mut ctx = self.clone(); + let checked = zip(params.iter(), args.iter()) + .map(|(p, a)| { + let p_set = ctx.check_set(&p.set)?; + let a = ctx.check_element(a, &p_set)?; + ctx.add_element(p.name.clone(), a.clone().into(), p_set)?; + Ok(a) + }) + .collect::<Result<Vec<_>, _>>()?; + Ok((ctx, checked)) + } } diff --git a/src/parser.rs b/src/parser.rs index ecf6ab3..285bb84 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -227,9 +227,21 @@ parser! { } rule app_inst() -> Instance - = head:dot_inst() args:(__ a:dot_elem() { a })* - { if args.is_empty() { head } else { Instance::App{instance: Box::new(head), args } }} - + = subject:dot_inst() args:(__ a:dot_elem() { a })* + { + if args.is_empty() { + subject + } else { + match subject { + Instance::App { instance: inner_head, args: inner_args } => { + let mut all_args = inner_args; + all_args.extend(args); + Instance::App { instance: inner_head, args: all_args } + } + other => Instance::App { instance: Box::new(other), args }, + } + } + } rule instance() -> Instance = kw_for() _ ps:param_list() _ "," _ body:instance() |