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

6 files changed, 191 insertions, 103 deletions

diff --git a/src/checker.rs b/src/checker.rs
index dc3dc3c..f3c5205 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -33,7 +33,7 @@ impl CheckerState {
                 Decl::Signature { name, signature } => {
                     self.assert_unbound_signature(name)?;
                     let signature = self.check_signature(signature.clone())?;
-                    self.add_signature(name, signature)
+                    self.add_signature(name, signature, false)
                 }
                 Decl::Instance {
                     name,
@@ -42,7 +42,7 @@ impl CheckerState {
                 } => {
                     self.assert_unbound_instance(name)?;
                     let signature = self.check_signature(signature.clone())?;
-                    let instance = self.check_instance(instance.clone(), &signature)?;
+                    let instance = self.check_instance(instance.clone(), (&signature).into())?;
                     self.add_instance(name.clone(), instance.into(), signature)
                 }
             }?;
diff --git a/src/checker_set.rs b/src/checker_set.rs
index 86661c7..2bd011d 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -35,7 +35,7 @@ impl CheckerState {
                 Ok(Set::Variant(fields))
             }
             Set::ClaimedSet(instance) => {
-                let instance = self.check_instance(instance, &Signature::Set)?;
+                let instance = self.check_instance(instance, Some(&Signature::Set))?;
                 Ok(Set::ClaimedSet(instance))
             }
             Set::Var(v) => {
@@ -313,40 +313,38 @@ impl CheckerState {
                         field: field_set, ..
                     } = self.lookup_variant_field(&arm.tag)?;
 
-                    let mut new_context = self.clone();
+                    let mut ctx = self.clone();
                     let binding_name = arm.bound.clone();
                     let binding_set = field_set.clone();
 
-                    let body = if let Some((tag, inner)) = &matching
+                    let case_arm = if let Some((tag, inner)) = &matching
                         && *tag == arm.tag
                     {
-                        new_context.add_element(
-                            binding_name.clone(),
-                            inner.clone().into(),
-                            binding_set,
-                        )?;
-                        let output = new_context.check_element(arm.body.clone().into(), set)?;
+                        let canonical =
+                            ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
+                        let output = ctx.check_element(arm.body.clone().into(), set)?;
                         if matches!(computed_output, Some(_)) {
                             panic!(
                                 "invariant violation: we somehow matched multiple arms in case analysis"
                             )
                         }
                         computed_output = Some(output.clone());
-                        output
+                        CaseArm {
+                            tag: arm.tag.clone(),
+                            bound: canonical,
+                            body: output,
+                        }
                     } else {
-                        new_context.add_element(
-                            binding_name.clone(),
-                            Value::Hypothetical,
-                            binding_set,
-                        )?;
-                        new_context.check_element(arm.body.clone().into(), set)?
+                        let canonical = ctx.make_element_binding(binding_name, binding_set)?;
+                        let body = ctx.check_element(arm.body.clone().into(), set)?;
+                        CaseArm {
+                            tag: arm.tag.clone(),
+                            bound: canonical,
+                            body,
+                        }
                     };
 
-                    processed_arms.push(CaseArm {
-                        tag: arm.tag.clone(),
-                        bound: binding_name,
-                        body,
-                    });
+                    processed_arms.push(case_arm);
                 }
                 Ok(computed_output.unwrap_or(Element::Case {
                     scrutinee: Box::new(scrutinee),
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"
+                    ),
+                }
             }
         }
     }
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 1a6a0bd..6a458d5 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -47,6 +47,11 @@ pub enum CheckerError {
         claimed: Signature,
         reason: String,
     },
+    #[display("Non-functional instance {instance} found in application to element {element}")]
+    NonFunctionalInstance {
+        instance: Instance,
+        element: Element,
+    },
 }
 
 // -----------------------------------------------------------------------------
@@ -111,6 +116,7 @@ pub struct CheckerState {
     variant_fields: HashMap<String, Field<Set>>,
     signature_fields: HashMap<String, Field<Signature>>,
     binder_element: usize,
+    unique_name: usize,
 }
 
 impl fmt::Display for CheckerState {
@@ -136,6 +142,7 @@ impl fmt::Display for CheckerState {
         section(f, "variant_fields", &self.variant_fields)?;
         section(f, "signatures", &self.wf_signatures)?;
         section(f, "instances", &self.wf_instances)?;
+        section(f, "signature_fields", &self.signature_fields)?;
         writeln!(f, " }}")?;
         Ok(())
     }
@@ -332,13 +339,14 @@ impl CheckerState {
     }
 
     #[instrument(skip(self), level = "debug", fields(%name, %field_signature, %owner_signature))]
-    fn add_signature_field(
+    pub fn add_signature_field(
         &mut self,
         name: &String,
         field_signature: &Signature,
         owner_signature: &Signature,
+        rebind: bool,
     ) -> Result<(), CheckerError> {
-        if let Some(signature_ref) = self.signature_fields.get(name) {
+        if !rebind && let Some(signature_ref) = self.signature_fields.get(name) {
             self.assert_correct_owner(name, signature_ref, owner_signature)?;
         };
         self.signature_fields.insert(
@@ -356,6 +364,7 @@ impl CheckerState {
         &mut self,
         name: &String,
         signature: Signature,
+        rebind: bool,
     ) -> Result<(), CheckerError> {
         match &signature {
             Signature::Theory(fields) => {
@@ -364,7 +373,7 @@ impl CheckerState {
                     signature: field_sig,
                 } in fields
                 {
-                    self.add_signature_field(field_name, field_sig, &signature)?;
+                    self.add_signature_field(field_name, field_sig, &signature, rebind)?;
                 }
             }
             // TODO: is there more?
@@ -415,12 +424,35 @@ impl CheckerState {
 // -----------------------------------------------------------------------------
 // Bindings
 impl CheckerState {
-    #[instrument(skip(self), level = "debug", fields(%name, %set))]
-    pub fn make_element_binding(&mut self, name: String, set: Set) -> Result<(), CheckerError> {
-        let canonical = format!("db_e_{}", self.binder_element);
-        self.add_element(canonical.clone(), ElementValue::Hypothetical, set.clone())?;
-        self.add_element(name, Element::Var(canonical).into(), set)?;
+    fn _make_canonical_element(&mut self, name: String, set: Set) -> Result<String, CheckerError> {
+        let canonical = format!("_#{}", self.binder_element);
+        self.add_element(name, Element::Var(canonical.clone()).into(), set)?;
         self.binder_element += 1;
-        Ok(())
+        Ok(canonical)
+    }
+
+    #[instrument(skip(self), level = "debug", fields(%name, %set))]
+    pub fn make_element_binding(&mut self, name: String, set: Set) -> Result<String, CheckerError> {
+        let canonical = self._make_canonical_element(name, set.clone())?;
+        self.add_element(canonical.clone(), ElementValue::Hypothetical, set)?;
+        Ok(canonical)
+    }
+
+    #[instrument(skip(self), level = "debug", fields(%name, %set))]
+    pub fn make_element_definition(
+        &mut self,
+        name: String,
+        value: Element,
+        set: Set,
+    ) -> Result<String, CheckerError> {
+        let canonical = self._make_canonical_element(name, set.clone())?;
+        self.add_element(canonical.clone(), Value::Concrete(value), set)?;
+        Ok(canonical)
+    }
+
+    #[instrument(skip(self))]
+    pub fn make_unique_name(&mut self) -> String {
+        self.unique_name += 1;
+        format!("_#{}", self.unique_name)
     }
 }
diff --git a/src/main.rs b/src/main.rs
index f721ef4..b8987a2 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -43,23 +43,23 @@ let signature T = theory {
     C :: (x : set-of(set-of(set-of(A) :: Set) :: Set)) (b : set-of(B x)) -> Set
 }
 
-let signature Graph = theory {
-    Node :: Set,
-    Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
-}
+// let signature Graph = theory {
+//     Node :: Set,
+//     Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
+// }
 
-let instance natPoset :: Graph = {
-    .Node = Nat :: Set,
-    .Edge = for (s : Nat) (t : Nat), Bool :: Set
-}
+// let instance natPoset :: Graph = {
+//     .Node = Nat :: Set,
+//     .Edge = for (s : Nat) (t : Nat), Bool :: Set
+// }
 
-let element node : set-of(natPoset .Node) = 7
+// let element node : set-of(natPoset .Node) = 7
 
-let set NatEdges = record {
-  source: set-of(natPoset .Node),
-  target: set-of(natPoset .Node),
-  connected: set-of(natPoset .Edge source target)
-}
+// let set NatEdges = record {
+//   source: set-of(natPoset .Node),
+//   target: set-of(natPoset .Node),
+//   connected: set-of(natPoset .Edge source target)
+// }
 "#;
     let programme = parser::debug_parse(src);
 
diff --git a/src/parser.rs b/src/parser.rs
index 418a17e..1aed3f8 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -225,7 +225,7 @@ parser! {
 pub fn debug_parse(src: &str) -> Programme {
     match parser::program(src) {
         Ok(p) => {
-            println!("```{}\n```\n=>\n{}\n", src, p);
+            println!("{}", p);
             p
         }
         Err(e) => {