fill in some more todos

4 files changed, 52 insertions, 130 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index c3d1b3a..e12cfb2 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -2,7 +2,6 @@ use crate::ast::*;
 use crate::checker_state::*;
 
 use std::collections::HashMap;
-use std::iter::zip;
 use tracing::instrument;
 
 impl CheckerState {
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 6633dd1..89f4441 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -276,7 +276,23 @@ impl CheckerState {
                         params: inst_params,
                     })
                 } else {
-                    todo!("expand only mode???")
+                    let mut ctx = self.clone();
+                    let inst_params = inst_params
+                        .iter()
+                        .map(|Param { name, set }| {
+                            let set = ctx.check_set(set)?;
+                            let canon = ctx.make_element_binding(name.clone(), set.clone())?;
+                            Ok(Param {
+                                name: canon,
+                                set: set,
+                            })
+                        })
+                        .collect::<Result<Vec<_>, _>>()?;
+                    let body = ctx.check_instance(body, None)?;
+                    Ok(Instance::For {
+                        params: inst_params,
+                        body: Box::new(body),
+                    })
                 }
             }
             Instance::App(inner, element) => {
@@ -326,86 +342,29 @@ impl CheckerState {
                         ))
                     }
                     Instance::For { params, body } => {
-                        // if params.is_empty() {
-                        //     panic!(
-                        //         "It should have been impossible to construct a For with no params, but here we are"
-                        //     );
-                        // }
-                        // 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");
+                        if params.is_empty() {
+                            panic!(
+                                "it should have been impossible to construct a for with no parameters, but here we are"
+                            );
+                        }
+                        let mut ctx = self.clone();
+                        let first_set = ctx.check_set(&params[0].set)?;
+                        let element_checked = self.check_element(element, &first_set)?;
+                        ctx.make_element_definition(
+                            params[0].name.clone(),
+                            element_checked,
+                            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 {
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 7587a5e..c9be445 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -373,6 +373,7 @@ impl CheckerState {
                     signature: field_sig,
                 } in fields
                 {
+                    // TODO: are we supposed to recurse?
                     // let name = self.make_unique_name();
                     // self.add_signature(&name, field_sig.clone(), rebind)?;
                     self.add_signature_field(field_name, field_sig, &signature, rebind)?;
diff --git a/src/main.rs b/src/main.rs
index 692379f..34d6360 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -18,57 +18,20 @@ fn main() {
         .init();
 
     let src = r#"
+let signature Graph = theory {
+    Node :: Set,
+    Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
+}
 
-// let X be the set Y, call it Z
-// let set X = record { b : Bool, n : Nat }
-// let set Y = X
-// let set Z = record { y : Y }
-// make some elements
-// let element x : X = { .b = true, .n = 41 }
-// let element z : Z = { .y = x }
-// exercise case matching
-// let set Z_or_Float = variant [ z : Z | f : Float ]
-// let element injected : Z_or_Float = z. z
-// let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ]
-
-// 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 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 instance natPoset :: Graph = {
-//     .Node = Nat :: Set,
-//     .Edge = for (s : Nat) (t : Nat), Bool :: Set
-// }
-
-// 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 signature S = theory {
-  A :: Set,
-  B :: (x : set-of(A)) -> Set
+let instance natGraph :: Graph = {
+    .Node = Nat :: Set,
+    .Edge = for (s : Nat) (t : Nat), Bool :: Set
 }
 
-let instance i :: S = {
-  .A = Nat :: Set,
-  .B = for (x : set-of(A)), Bool :: Set
+let set NatEdges = record {
+  source: set-of(natGraph .Node),
+  target: set-of(natGraph .Node),
+  connected: set-of(natGraph .Edge source target)
 }
 "#;
     let programme = parser::debug_parse(src);