From 617f3931de77bd795a97331e7146eb10266af7e9 Mon Sep 17 00:00:00 2001 From: tslil Date: Thu, 30 Apr 2026 10:52:07 +0100 Subject: lost track of what's going on --- src/checker_set.rs | 68 +++++++---- src/checker_signature.rs | 310 ++++++++++++++++++++++++++++++----------------- src/checker_state.rs | 2 + src/main.rs | 26 ++-- 4 files changed, 260 insertions(+), 146 deletions(-) diff --git a/src/checker_set.rs b/src/checker_set.rs index 10f9b28..c3d1b3a 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -1,6 +1,7 @@ use crate::ast::*; use crate::checker_state::*; +use std::collections::HashMap; use std::iter::zip; use tracing::instrument; @@ -39,7 +40,11 @@ impl CheckerState { } Set::ClaimedSet(instance) => { let instance = self.check_instance(instance, Some(&Signature::Set))?; - Ok(Set::ClaimedSet(instance)) + if let Instance::SetCoerce(set) = instance { + Ok(*set) + } else { + Ok(Set::ClaimedSet(instance)) + } } Set::Var(v) => { let deref = self.lookup_set(&v)?; @@ -128,40 +133,55 @@ impl CheckerState { Err(rej("element is a record instance".to_string())) }?; - let (set_fnames, set_fsets): (Vec, Vec) = fields - .iter() - .map(|RecordField { name, set }| (name.clone(), set.clone())) - .unzip(); - let mut set_fnames_sorted = set_fnames.clone(); + let mut set_fnames_sorted: Vec = + fields.iter().map(|x| x.name.clone()).collect(); set_fnames_sorted.sort(); - let (element_fnames, element_felements): (Vec, Vec<&Element>) = - assignations - .iter() - .map(|ElemAssign { name, element }| (name.clone(), element)) - .unzip(); - - let mut element_fnames_sorted = element_fnames.clone(); + let mut element_fnames_sorted: Vec = + assignations.iter().map(|x| x.name.clone()).collect(); element_fnames_sorted.sort(); + // make sure that we are correctly filling the record if set_fnames_sorted != element_fnames_sorted { return Err(rej(format!( "expected [{}] but found [{}]", - set_fnames.join(", "), - element_fnames.join(", "), + set_fnames_sorted.join(", "), + element_fnames_sorted.join(", "), ))); } - // recurse, sets have already been completely expanded - let sub_els = zip(element_felements, set_fsets) - .map(|(e_f, e_s)| self.check_element(e_f.into(), &e_s)) + let assignations = assignations + .into_iter() + .map(|x| (&x.name, &x.element)) + .collect::>(); + + let mut ctx = self.clone(); + // the basic pattern here is that we use ctx.check_* to perform + // substitutions for us, as we steadily march through the users + // definitions + let sub_elements = fields + .iter() + .map( + |RecordField { + name: f_n, + set: f_s, + }| { + let f_e = assignations + .get(f_n) + .expect("we have already checked that all fields are present"); + + let f_s = ctx.check_set(f_s)?; + let f_e = ctx.check_element(f_e, &f_s)?; + ctx.add_element(f_n.clone(), f_e.clone().into(), f_s)?; + + Ok(ElemAssign { + name: f_n.clone(), + element: f_e, + }) + }, + ) .collect::, _>>()?; - // rebuild - let assignations = zip(element_fnames, sub_els) - .map(|(name, element)| ElemAssign { name, element }) - .collect(); - // resign? - Ok(Element::Record(assignations)) + Ok(Element::Record(sub_elements)) } Element::Project { element: inner, 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, 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>; + 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; - (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 = + fields.iter().map(|x| x.name.clone()).collect(); signature_fnames_sorted.sort(); + let mut instance_fnames_sorted: Vec = + 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::>(); + + 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::, _>>()?; + + 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::, _>>()?; + 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::, _>>()?; - 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::, _>>()?; + 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, Vec) = - 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::>()?; - // 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, Vec) = + // 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::>()?; + // // 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(_) => { diff --git a/src/checker_state.rs b/src/checker_state.rs index 6a458d5..7587a5e 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -373,6 +373,8 @@ impl CheckerState { signature: field_sig, } in fields { + // 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 57e7f52..692379f 100644 --- a/src/main.rs +++ b/src/main.rs @@ -43,15 +43,15 @@ fn main() { // 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 @@ -60,6 +60,16 @@ let instance natPoset :: Graph = { // 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 i :: S = { + .A = Nat :: Set, + .B = for (x : set-of(A)), Bool :: Set +} "#; let programme = parser::debug_parse(src); -- cgit v1.3.1