lost track of what's going on

1 files changed, 196 insertions, 114 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index e86ff9e..6633dd1 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -1,5 +1,6 @@
 use crate::ast::*;
 use crate::checker_state::*;
+use std::collections::HashMap;
 use std::iter::zip;
 
 use tracing::instrument;
@@ -100,23 +101,13 @@ impl CheckerState {
                     Ok(Instance::Var(v.clone()))
                 }
             }
-            Instance::Record(assignations) => {
-                // once again, mutatis mutandis from elements
-                let (instance_fnames, instance_finstances): (Vec<String>, Vec<&Instance>) =
-                    assignations
-                        .iter()
-                        .map(|InstAssign { name, instance }| (name.clone(), instance))
-                        .unzip();
-
-                let mut instance_fnames_sorted = instance_fnames.clone();
-                instance_fnames_sorted.sort();
 
-                let signature_fsigs: Vec<Option<Signature>>;
+            Instance::Record(assignations) => {
                 if let Some(signature) = signature {
                     let rej = |reason| CheckerError::InstanceDoesNotBelong {
                         instance: instance.clone(),
                         claimed: signature.clone(),
-                        reason: reason,
+                        reason,
                     };
 
                     let fields = if let Signature::Theory(fields) = signature {
@@ -125,36 +116,70 @@ impl CheckerState {
                         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();
+                    let mut signature_fnames_sorted: Vec<String> =
+                        fields.iter().map(|x| x.name.clone()).collect();
                     signature_fnames_sorted.sort();
 
+                    let mut instance_fnames_sorted: Vec<String> =
+                        assignations.iter().map(|x| x.name.clone()).collect();
+                    instance_fnames_sorted.sort();
+
                     if signature_fnames_sorted != instance_fnames_sorted {
                         return Err(rej(format!(
                             "expected [{}] but found [{}]",
-                            signature_fnames.join(", "),
-                            instance_fnames.join(", "),
+                            signature_fnames_sorted.join(", "),
+                            instance_fnames_sorted.join(", "),
                         )));
                     }
+
+                    let assignations = assignations
+                        .iter()
+                        .map(|x| (&x.name, &x.instance))
+                        .collect::<HashMap<_, _>>();
+
+                    let mut ctx = self.clone();
+                    let sub_instances = fields
+                        .iter()
+                        .map(
+                            |SigField {
+                                 name: f_n,
+                                 signature: f_s,
+                             }| {
+                                let f_i = assignations
+                                    .get(f_n)
+                                    .expect("we have already checked that all fields are present");
+                                let f_s = ctx.check_signature(f_s)?;
+                                let f_i = ctx.check_instance(f_i, Some(&f_s))?;
+
+                                if f_s == Signature::Set {
+                                    ctx.add_set(
+                                        f_n.clone(),
+                                        Set::ClaimedSet(Instance::Var(f_n.clone())).into(),
+                                    )?;
+                                }
+
+                                ctx.add_instance(f_n.clone(), f_i.clone().into(), f_s.clone())?;
+                                Ok(InstAssign {
+                                    name: f_n.clone(),
+                                    instance: f_i,
+                                })
+                            },
+                        )
+                        .collect::<Result<Vec<_>, _>>()?;
+
+                    Ok(Instance::Record(sub_instances))
                 } else {
-                    signature_fsigs = std::iter::repeat(None)
-                        .take(instance_finstances.len())
-                        .collect();
+                    let sub_insts = assignations
+                        .iter()
+                        .map(|InstAssign { name, instance }| {
+                            Ok(InstAssign {
+                                name: name.clone(),
+                                instance: self.check_instance(instance, None)?,
+                            })
+                        })
+                        .collect::<Result<Vec<_>, _>>()?;
+                    Ok(Instance::Record(sub_insts))
                 }
-
-                let sub_els = zip(instance_finstances, signature_fsigs)
-                    .map(|(e_f, e_s)| self.check_instance(e_f, (&e_s).into()))
-                    .collect::<Result<Vec<_>, _>>()?;
-                let assignations = zip(instance_fnames, sub_els)
-                    .map(|(name, instance)| InstAssign { name, instance })
-                    .collect();
-                Ok(Instance::Record(assignations))
             }
             Instance::Project { instance, field } => {
                 let Field {
@@ -194,8 +219,65 @@ impl CheckerState {
                     ),
                 }
             }
-            Instance::For { .. } => {
-                todo!("instance for")
+            Instance::For {
+                params: inst_params,
+                body,
+            } => {
+                if let Some(signature) = signature {
+                    if inst_params.is_empty() {
+                        todo!("should be impossible");
+                    };
+                    let Signature::Ext {
+                        params: sig_params,
+                        codomain,
+                    } = signature
+                    else {
+                        todo!("need to raise error");
+                    };
+                    if sig_params.is_empty() {
+                        todo!("should be impossible")
+                    }
+                    if sig_params.len() != inst_params.len() {
+                        todo!("this is a type error")
+                    }
+                    let mut ctx = self.clone();
+                    let inst_params = zip(inst_params, sig_params)
+                        .map(
+                            |(
+                                Param {
+                                    name: inst_n,
+                                    set: inst_s,
+                                },
+                                Param {
+                                    name: set_n,
+                                    set: set_s,
+                                },
+                            )| {
+                                let inst_s = ctx.check_set(inst_s)?;
+                                let set_s = ctx.check_set(set_s)?;
+                                if !ctx.equal(&inst_s, &set_s) {
+                                    todo!("type error")
+                                }
+                                ctx.add_element(
+                                    inst_n.clone(),
+                                    Element::Var(set_n.clone()).into(),
+                                    set_s.clone(),
+                                )?;
+                                Ok(Param {
+                                    name: set_n.clone(),
+                                    set: set_s,
+                                })
+                            },
+                        )
+                        .collect::<Result<Vec<_>, _>>()?;
+                    let body = ctx.check_instance(body, Some(&*codomain))?;
+                    Ok(Instance::For {
+                        body: Box::new(body),
+                        params: inst_params,
+                    })
+                } else {
+                    todo!("expand only mode???")
+                }
             }
             Instance::App(inner, element) => {
                 // this is the only time that we ever call check_instance with
@@ -244,85 +326,85 @@ 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.
-                        }
+                        // 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");
                     }
                     Instance::Record(_) | Instance::SetCoerce(_) => {