1 files changed, 41 insertions, 30 deletions

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, &params[0].set)?;
-                        Ok(Instance::App(
-                            Box::new(Instance::Var(v.clone())),
-                            Box::new(element),
-                        ))
+                        todo!("finish")
+                        // let element = self.check_element(args, &params[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(&params[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(),
+                        })
                     }
                 }
             }