From d57f1d3c845220c741db73c1fada017a75b11992 Mon Sep 17 00:00:00 2001 From: tslil Date: Thu, 30 Apr 2026 15:55:11 +0100 Subject: fill in some more todos --- src/checker_signature.rs | 121 ++++++++++++++++------------------------------- 1 file changed, 40 insertions(+), 81 deletions(-) (limited to 'src/checker_signature.rs') diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 6633dd1..89f4441 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -276,7 +276,23 @@ impl CheckerState { params: inst_params, }) } else { - todo!("expand only mode???") + let mut ctx = self.clone(); + let inst_params = inst_params + .iter() + .map(|Param { name, set }| { + let set = ctx.check_set(set)?; + let canon = ctx.make_element_binding(name.clone(), set.clone())?; + Ok(Param { + name: canon, + set: set, + }) + }) + .collect::, _>>()?; + let body = ctx.check_instance(body, None)?; + Ok(Instance::For { + params: inst_params, + body: Box::new(body), + }) } } Instance::App(inner, element) => { @@ -326,86 +342,29 @@ impl CheckerState { )) } Instance::For { params, body } => { - // if params.is_empty() { - // panic!( - // "It should have been impossible to construct a For with no params, but here we are" - // ); - // } - // if let Some(signature) = signature { - // let Signature::Ext { - // params: sig_params, - // codomain, - // } = signature - // else { - // return Err(CheckerError::WrongSignatureForInstance { - // value: inner.clone().into(), - // claimed: signature.clone(), - // real: Signature::Ext { - // params: vec![Param { - // name: "...".to_string(), - // set: Set::Var("...".to_string()), - // }], - // codomain: Box::new(Signature::Var("...".to_string())), - // }, - // }); - // }; - // if params.len() != sig_params.len() { - // todo!("raise an error about incorrect signature") - // }; - // let mut ctx = self.clone(); - // let (params, sig_params): (Vec, Vec) = - // zip(params, sig_params) - // .enumerate() - // .map(|(idx, (a_p, s_p))| { - // let a_set = ctx.check_set(&a_p.set)?; - // let p_set = ctx.check_set(&s_p.set)?; - // if !ctx.equal(&a_set, &p_set) { - // todo!( - // "raise an error about the for/Ext being incorrect" - // ); - // } - // if idx == 0 { - // let element = ctx.check_element(&*element, &p_set)?; - // ctx.make_element_definition( - // a_p.name.clone(), - // element.clone(), - // a_set.clone(), - // )?; - // ctx.make_element_definition( - // s_p.name.clone(), - // element, - // p_set.clone(), - // )?; - // } else { - // let canon_a = ctx.make_element_binding( - // a_p.name.clone(), - // a_set.clone(), - // )?; - // ctx.add_element( - // s_p.name.clone(), - // Element::Var(canon_a).into(), - // p_set.clone(), - // )?; - // } - // Ok(( - // Param { - // name: a_p.name.clone(), - // set: a_set, - // }, - // Param { - // name: s_p.name.clone(), - // set: p_set, - // }, - // )) - // }) - // .collect::>()?; - // // TODO: now we need to build a new For and a new - // // Ext, and check the latter then check that the - // // former fits the latter. The base case would be - // // checking that body's expected signature is - // // codomain. - // } - todo!("finish this"); + if params.is_empty() { + panic!( + "it should have been impossible to construct a for with no parameters, but here we are" + ); + } + let mut ctx = self.clone(); + let first_set = ctx.check_set(¶ms[0].set)?; + let element_checked = self.check_element(element, &first_set)?; + ctx.make_element_definition( + params[0].name.clone(), + element_checked, + 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 { -- cgit v1.3.1