From 0886a16d73145270e953b8c2e0a4452b518ea16e Mon Sep 17 00:00:00 2001 From: tslil Date: Fri, 1 May 2026 12:36:24 +0100 Subject: working on fixing app, rework ast to have generics etc --- src/checker_signature.rs | 71 ++++++++++++++++++++++++++++-------------------- 1 file changed, 41 insertions(+), 30 deletions(-) (limited to 'src/checker_signature.rs') diff --git a/src/checker_signature.rs b/src/checker_signature.rs index bad38eb..2d5057f 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -31,8 +31,8 @@ impl CheckerState { let mut ctx = self.clone(); let temp_name = ctx.make_unique_name(); let mut new_fields = Vec::new(); - for SigField { signature, name } in fields { - let signature = ctx.check_signature(signature)?; + for Field { carries, name } in fields { + let signature = ctx.check_signature(carries)?; ctx.add_instance(name.clone(), InstanceValue::Hypothetical, signature.clone())?; // And lo, the special case, our chosen canonical form if signature == Signature::Set { @@ -41,9 +41,9 @@ impl CheckerState { Set::ClaimedSet(Instance::Var(name.clone())).into(), )?; } - new_fields.push(SigField { + new_fields.push(Field { name: name.clone(), - signature, + carries: signature, }); // We must iteratively add the entire signature so that // field lookup does something, as we rely on that for type @@ -140,9 +140,9 @@ impl CheckerState { let sub_instances = fields .iter() .map( - |SigField { + |Field { name: f_n, - signature: f_s, + carries: f_s, }| { let f_i = assignations .get(f_n) @@ -181,7 +181,7 @@ impl CheckerState { } } Instance::Project { instance, field } => { - let Field { + let OwnedField { field: field_signature, owner: owner_signature, } = self.lookup_signature_field(&field)?; @@ -268,7 +268,7 @@ impl CheckerState { let mut computed_output = None; let mut processed_arms = Vec::new(); for arm in arms { - let Field { + let OwnedField { field: field_set, .. } = self.lookup_variant_field(&arm.tag)?; @@ -288,7 +288,7 @@ impl CheckerState { ) } computed_output = Some(output.clone()); - InstCaseArm { + CaseArm { tag: arm.tag.clone(), bound: canonical, body: output, @@ -296,7 +296,7 @@ impl CheckerState { } else { let canonical = ctx.make_element_binding(binding_name, binding_set)?; let body = ctx.check_instance((&arm.body).into(), signature)?; - InstCaseArm { + CaseArm { tag: arm.tag.clone(), bound: canonical, body, @@ -386,14 +386,19 @@ impl CheckerState { }) } } - Instance::App(inner, element) => { + Instance::App { + instance: inner, + args, + } => { // this is the only time that we ever call check_instance with // 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, @@ -426,11 +431,12 @@ impl CheckerState { }); } } - let element = self.check_element(element, ¶ms[0].set)?; - Ok(Instance::App( - Box::new(Instance::Var(v.clone())), - Box::new(element), - )) + todo!("finish") + // let element = self.check_element(args, ¶ms[0].set)?; + // Ok(Instance::App( + // Box::new(Instance::Var(v.clone())), + // Box::new(element), + // )) } Instance::For { params, body } => { if params.is_empty() { @@ -440,28 +446,33 @@ impl CheckerState { } let mut ctx = self.clone(); let first_set = ctx.check_set(¶ms[0].set)?; - let element_checked = self.check_element(element, &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) - } + 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, - element: *element.clone(), + elements: args.clone(), }) } - Instance::Project { .. } | Instance::App(_, _) | Instance::Case { .. } => { + 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(Box::new(inner), element.clone())) + Ok(Instance::App { + instance: Box::new(inner), + args: args.clone(), + }) } } } -- cgit v1.3.1