wip on App For

2 files changed, 92 insertions, 35 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 7b07105..e86ff9e 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -198,6 +198,10 @@ impl CheckerState {
                 todo!("instance for")
             }
             Instance::App(inner, element) => {
+                // 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)?;
                 match &inner {
                     Instance::Var(v) => {
@@ -245,28 +249,81 @@ impl CheckerState {
                                 "It should have been impossible to construct a For with no params, but here we are"
                             );
                         }
-                        let mut ctx = self.clone();
-                        for (idx, param) in params.iter().enumerate() {
-                            let Param {
-                                name: param_name,
-                                set: param_set,
-                            } = param.clone();
-                            if idx == 0 {
-                                let element = self.check_element(&*element, &param_set)?;
-                                ctx.make_element_definition(param_name, element, param_set)?;
-                            } else {
-                                ctx.make_element_binding(param_name, param_set)?;
-                            }
-                        }
-                        let instance = ctx.check_instance(body, signature)?;
-                        if params.len() == 1 {
-                            Ok(instance)
-                        } else {
-                            Ok(Instance::For {
-                                params: params[1..].iter().map(|p| p.clone()).collect(),
-                                body: Box::new(instance),
-                            })
+                        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(_) => {
                         Err(CheckerError::NonFunctionalInstance {
diff --git a/src/main.rs b/src/main.rs
index b8987a2..57e7f52 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -36,22 +36,22 @@ fn main() {
 // let element e : set-of(natPoset .Edge 3 5) = true
 
 // this should be difficult unless we correctly handle various forms of alpha/beta
-let signature OneSet = theory { F :: Set }
-let signature T = theory {
-    A :: Set,
-    B :: (x : set-of({ .F = A } .F)) -> Set,
-    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 OneSet = theory { F :: Set }
+// let signature T = theory {
+//     A :: Set,
+//     B :: (x : set-of({ .F = A } .F)) -> Set,
+//     C :: (x : set-of(set-of(set-of(A) :: Set) :: Set)) (b : set-of(B x)) -> Set
 // }
 
-// let instance natPoset :: Graph = {
-//     .Node = Nat :: Set,
-//     .Edge = for (s : Nat) (t : Nat), Bool :: 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 element node : set-of(natPoset .Node) = 7