diff options
Diffstat (limited to 'src/checker_signature.rs')
| -rw-r--r-- | src/checker_signature.rs | 310 |
1 files changed, 196 insertions, 114 deletions
diff --git a/src/checker_signature.rs b/src/checker_signature.rs index e86ff9e..6633dd1 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -1,5 +1,6 @@ use crate::ast::*; use crate::checker_state::*; +use std::collections::HashMap; use std::iter::zip; use tracing::instrument; @@ -100,23 +101,13 @@ impl CheckerState { Ok(Instance::Var(v.clone())) } } - Instance::Record(assignations) => { - // once again, mutatis mutandis from elements - let (instance_fnames, instance_finstances): (Vec<String>, Vec<&Instance>) = - assignations - .iter() - .map(|InstAssign { name, instance }| (name.clone(), instance)) - .unzip(); - - let mut instance_fnames_sorted = instance_fnames.clone(); - instance_fnames_sorted.sort(); - let signature_fsigs: Vec<Option<Signature>>; + Instance::Record(assignations) => { if let Some(signature) = signature { let rej = |reason| CheckerError::InstanceDoesNotBelong { instance: instance.clone(), claimed: signature.clone(), - reason: reason, + reason, }; let fields = if let Signature::Theory(fields) = signature { @@ -125,36 +116,70 @@ impl CheckerState { Err(rej("signature has no fields".to_string())) }?; - let signature_fnames: Vec<String>; - (signature_fnames, signature_fsigs) = fields - .iter() - .map(|SigField { name, signature }| { - (name.clone(), signature.clone().into()) - }) - .unzip(); - let mut signature_fnames_sorted = signature_fnames.clone(); + let mut signature_fnames_sorted: Vec<String> = + fields.iter().map(|x| x.name.clone()).collect(); signature_fnames_sorted.sort(); + let mut instance_fnames_sorted: Vec<String> = + assignations.iter().map(|x| x.name.clone()).collect(); + instance_fnames_sorted.sort(); + if signature_fnames_sorted != instance_fnames_sorted { return Err(rej(format!( "expected [{}] but found [{}]", - signature_fnames.join(", "), - instance_fnames.join(", "), + signature_fnames_sorted.join(", "), + instance_fnames_sorted.join(", "), ))); } + + let assignations = assignations + .iter() + .map(|x| (&x.name, &x.instance)) + .collect::<HashMap<_, _>>(); + + let mut ctx = self.clone(); + let sub_instances = fields + .iter() + .map( + |SigField { + name: f_n, + signature: f_s, + }| { + let f_i = assignations + .get(f_n) + .expect("we have already checked that all fields are present"); + let f_s = ctx.check_signature(f_s)?; + let f_i = ctx.check_instance(f_i, Some(&f_s))?; + + if f_s == Signature::Set { + ctx.add_set( + f_n.clone(), + Set::ClaimedSet(Instance::Var(f_n.clone())).into(), + )?; + } + + ctx.add_instance(f_n.clone(), f_i.clone().into(), f_s.clone())?; + Ok(InstAssign { + name: f_n.clone(), + instance: f_i, + }) + }, + ) + .collect::<Result<Vec<_>, _>>()?; + + Ok(Instance::Record(sub_instances)) } else { - signature_fsigs = std::iter::repeat(None) - .take(instance_finstances.len()) - .collect(); + let sub_insts = assignations + .iter() + .map(|InstAssign { name, instance }| { + Ok(InstAssign { + name: name.clone(), + instance: self.check_instance(instance, None)?, + }) + }) + .collect::<Result<Vec<_>, _>>()?; + Ok(Instance::Record(sub_insts)) } - - let sub_els = zip(instance_finstances, signature_fsigs) - .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 { instance, field } => { let Field { @@ -194,8 +219,65 @@ impl CheckerState { ), } } - Instance::For { .. } => { - todo!("instance for") + Instance::For { + params: inst_params, + body, + } => { + if let Some(signature) = signature { + if inst_params.is_empty() { + todo!("should be impossible"); + }; + let Signature::Ext { + params: sig_params, + codomain, + } = signature + else { + todo!("need to raise error"); + }; + if sig_params.is_empty() { + todo!("should be impossible") + } + if sig_params.len() != inst_params.len() { + todo!("this is a type error") + } + let mut ctx = self.clone(); + let inst_params = zip(inst_params, sig_params) + .map( + |( + Param { + name: inst_n, + set: inst_s, + }, + Param { + name: set_n, + set: set_s, + }, + )| { + 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") + } + ctx.add_element( + inst_n.clone(), + Element::Var(set_n.clone()).into(), + set_s.clone(), + )?; + Ok(Param { + name: set_n.clone(), + set: set_s, + }) + }, + ) + .collect::<Result<Vec<_>, _>>()?; + let body = ctx.check_instance(body, Some(&*codomain))?; + Ok(Instance::For { + body: Box::new(body), + params: inst_params, + }) + } else { + todo!("expand only mode???") + } } Instance::App(inner, element) => { // this is the only time that we ever call check_instance with @@ -244,85 +326,85 @@ 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<Param>, Vec<Param>) = - 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::<Result<_, _>>()?; - // 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. - } + // 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<Param>, Vec<Param>) = + // 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::<Result<_, _>>()?; + // // 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"); } Instance::Record(_) | Instance::SetCoerce(_) => { |