implement canonicalisation in case arms, work through first bit of app

1 files changed, 114 insertions, 56 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index e92d424..b979f54 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -19,8 +19,8 @@ impl CheckerState {
                     .into_iter()
                     .map(|p| {
                         let set = ctx.check_set(p.set.clone())?;
-                        ctx.make_element_binding(p.name.clone(), set.clone())?;
-                        Ok(Param { set, name: p.name })
+                        let canon = ctx.make_element_binding(p.name.clone(), set.clone())?;
+                        Ok(Param { set, name: canon })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
                 let codomain = Box::new(ctx.check_signature(*codomain)?);
@@ -28,26 +28,28 @@ impl CheckerState {
             }
             Signature::Theory(fields) => {
                 let mut ctx = self.clone();
-                let fields = fields
-                    .into_iter()
-                    .map(|SigField { signature, name }| {
-                        let signature = ctx.check_signature(signature)?;
-                        ctx.add_instance(
+                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)?;
+                    ctx.add_instance(name.clone(), InstanceValue::Hypothetical, signature.clone())?;
+                    // And lo, the special case, our chosen canonical form
+                    if signature == Signature::Set {
+                        ctx.add_set(
                             name.clone(),
-                            InstanceValue::Hypothetical,
-                            signature.clone(),
+                            Set::ClaimedSet(Instance::Var(name.clone())).into(),
                         )?;
-                        // And lo, the special case, our chosen canonical form
-                        if signature == Signature::Set {
-                            ctx.add_set(
-                                name.clone(),
-                                Set::ClaimedSet(Instance::Var(name.clone())).into(),
-                            )?;
-                        }
-                        Ok(SigField { name, signature })
-                    })
-                    .collect::<Result<Vec<_>, _>>()?;
-                Ok(Signature::Theory(fields))
+                    }
+                    new_fields.push(SigField { name, signature });
+                    // We must iteratively add the entire signature so that
+                    // field lookup does something, as we rely on that for type
+                    // checking. We could hack together a signature i suppose,
+                    // but the cleanest thing is to add the truncations of this
+                    // signature. In any event the context is discarded
+                    // afterward.
+                    ctx.add_signature(&temp_name, Signature::Theory(new_fields.clone()), true)?;
+                }
+                Ok(Signature::Theory(new_fields))
             }
         }
     }
@@ -56,11 +58,13 @@ impl CheckerState {
     pub fn check_instance(
         &self,
         instance: Instance,
-        signature: &Signature,
+        signature: Option<&Signature>,
     ) -> Result<Instance, CheckerError> {
         match instance {
             Instance::SetCoerce(ref set) => {
-                if *signature != Signature::Set {
+                if let Some(signature) = signature
+                    && *signature != Signature::Set
+                {
                     return Err(CheckerError::WrongSignatureForInstance {
                         value: instance.clone().into(),
                         real: Signature::Set,
@@ -78,7 +82,9 @@ impl CheckerState {
                 // Exactly the same discipline as for Element::Var, see there
                 // for some sparse comments
                 let lookup = self.lookup_instance(&v)?;
-                if !self.equal(signature, &lookup.container) {
+                if let Some(signature) = signature
+                    && !self.equal(signature, &lookup.container)
+                {
                     return Err(CheckerError::WrongSignatureForInstance {
                         value: instance.clone().into(),
                         claimed: signature.clone(),
@@ -93,25 +99,6 @@ impl CheckerState {
             }
             Instance::Record(ref assignations) => {
                 // once again, mutatis mutandis from elements
-                let rej = |reason| CheckerError::InstanceDoesNotBelong {
-                    instance: instance.clone(),
-                    claimed: signature.clone(),
-                    reason,
-                };
-
-                let fields = if let Signature::Theory(fields) = signature {
-                    Ok(fields)
-                } else {
-                    Err(rej("instance is not a record instance".to_string()))
-                }?;
-
-                let (signature_fnames, signature_fsigs): (Vec<String>, Vec<Signature>) = fields
-                    .iter()
-                    .map(|SigField { name, signature }| (name.clone(), signature.clone()))
-                    .unzip();
-                let mut signature_fnames_sorted = signature_fnames.clone();
-                signature_fnames_sorted.sort();
-
                 let (instance_fnames, instance_finstances): (Vec<String>, Vec<&Instance>) =
                     assignations
                         .iter()
@@ -121,16 +108,45 @@ impl CheckerState {
                 let mut instance_fnames_sorted = instance_fnames.clone();
                 instance_fnames_sorted.sort();
 
-                if signature_fnames_sorted != instance_fnames_sorted {
-                    return Err(rej(format!(
-                        "expected [{}] but found [{}]",
-                        signature_fnames.join(", "),
-                        instance_fnames.join(", "),
-                    )));
+                let signature_fsigs: Vec<Option<Signature>>;
+                if let Some(signature) = signature {
+                    let rej = |reason| CheckerError::InstanceDoesNotBelong {
+                        instance: instance.clone(),
+                        claimed: signature.clone(),
+                        reason: reason,
+                    };
+
+                    let fields = if let Signature::Theory(fields) = signature {
+                        Ok(fields)
+                    } else {
+                        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();
+                    signature_fnames_sorted.sort();
+
+                    if signature_fnames_sorted != instance_fnames_sorted {
+                        return Err(rej(format!(
+                            "expected [{}] but found [{}]",
+                            signature_fnames.join(", "),
+                            instance_fnames.join(", "),
+                        )));
+                    }
+                } else {
+                    signature_fsigs = std::iter::repeat(None)
+                        .take(instance_finstances.len())
+                        .collect();
                 }
 
                 let sub_els = zip(instance_finstances, signature_fsigs)
-                    .map(|(e_f, e_s)| self.check_instance(e_f.clone(), &e_s))
+                    .map(|(e_f, e_s)| self.check_instance(e_f.clone(), (&e_s).into()))
                     .collect::<Result<Vec<_>, _>>()?;
                 let assignations = zip(instance_fnames, sub_els)
                     .map(|(name, instance)| InstAssign { name, instance })
@@ -146,7 +162,9 @@ impl CheckerState {
                     owner: owner_signature,
                 } = self.lookup_signature_field(&field)?;
 
-                if !self.equal(signature, field_signature) {
+                if let Some(signature) = signature
+                    && !self.equal(signature, field_signature)
+                {
                     return Err(CheckerError::WrongSignatureForInstance {
                         value: (*instance.clone()).into(),
                         claimed: signature.clone(),
@@ -154,7 +172,7 @@ impl CheckerState {
                     });
                 }
 
-                let inner = self.check_instance(*instance.clone(), owner_signature)?;
+                let inner = self.check_instance(*instance.clone(), owner_signature.into())?;
 
                 match inner {
                     Instance::Var(_) | Instance::Project { .. } => Ok(Instance::Project {
@@ -176,12 +194,52 @@ impl CheckerState {
                     ),
                 }
             }
-            Instance::For { params, body } => {
-                Err(CheckerError::Unimplemented("instance for".to_string()))
+            Instance::For { .. } => {
+                todo!("instance for")
             }
-            Instance::App(inst, elem) => {
-                println!("{}", self);
-                Err(CheckerError::Unimplemented("instance app".to_string()))
+            Instance::App(inner, element) => {
+                let inner = self.check_instance(*inner, None)?;
+                match &inner {
+                    Instance::Var(v) => {
+                        let field = self.lookup_signature_field(&v)?;
+                        let Signature::Ext {
+                            ref params,
+                            ref codomain,
+                        } = field.field
+                        else {
+                            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(),
+                            });
+                        };
+                        // TODO: we need to assert (somewhere else) that ext has >=1 params
+                        // TODO: in the special case that params.len() == 1 we need to do something with codomain
+                        let element = self.check_element(*element, &params[0].set)?;
+                        Ok(Instance::App(
+                            Box::new(Instance::Var(v.clone())),
+                            Box::new(element),
+                        ))
+                    }
+                    Instance::For { .. } => {
+                        todo!("app for")
+                    }
+                    Instance::Record(_) | Instance::SetCoerce(_) => {
+                        Err(CheckerError::NonFunctionalInstance {
+                            instance: inner,
+                            element: *element,
+                        })
+                    }
+                    Instance::Project { .. } | Instance::App(_, _) => panic!(
+                        "invariant violation: we did not completely expand the inner instance in our app"
+                    ),
+                }
             }
         }
     }