From d682ad6bbb5547ffbcc19da90275ff43e4e03e20 Mon Sep 17 00:00:00 2001 From: tslil Date: Wed, 6 May 2026 14:27:43 +0100 Subject: WiP --- src/ast.rs | 10 ++++-- src/checker.rs | 3 +- src/checker_set.rs | 37 ++++++++++++++++++--- src/checker_signature.rs | 83 ++++++++++++++++++++++++++++++++++++++++++------ src/checker_state.rs | 2 +- src/parser.rs | 66 +++++++++++++++++++------------------- 6 files changed, 148 insertions(+), 53 deletions(-) (limited to 'src') diff --git a/src/ast.rs b/src/ast.rs index e254c65..24c7125 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -68,6 +68,9 @@ pub enum Signature { #[display("Set")] Set, + #[display("⟨{_0}⟩")] + FromSet(Set), + #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::>().join(" , "))] Theory(Vec>), @@ -126,7 +129,7 @@ pub enum Element { element: Box, }, - #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] + #[display("case {scrutinee} of [ {} ]", arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] Case { scrutinee: Box, arms: Vec>, @@ -147,6 +150,9 @@ pub enum Instance { #[display("({_0} :: Set)")] SetCoerce(Box), + #[display("⟨{_0}⟩")] + ElementCoerce(Element), + #[display("{_0}")] Var(String), @@ -171,7 +177,7 @@ pub enum Instance { field: String, }, - #[display("case {} of [ {} ]", scrutinee, arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] + #[display("case {scrutinee} of [ {} ]", arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] Case { scrutinee: Box, arms: Vec>, diff --git a/src/checker.rs b/src/checker.rs index 2474bab..f94fccc 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -16,7 +16,7 @@ impl CheckerState { let Programme(decls) = prog; for decl in decls { - debug!(%decl); + print!("{decl} ... "); self.reset_binders(); match decl { Decl::Set { name, set } => { @@ -47,6 +47,7 @@ impl CheckerState { self.add_instance(name.clone(), instance.into(), signature) } }?; + println!("Ok"); } debug!(%self); Ok(()) diff --git a/src/checker_set.rs b/src/checker_set.rs index a00ea81..1a89631 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -230,7 +230,7 @@ impl CheckerState { .element; Ok(sub_element) } - _ => panic!( + Element::Inject { .. } | Element::Literal(_) => panic!( "invariant violation: check_element returned neither a record or stuck computation for record set" ), } @@ -312,7 +312,6 @@ impl CheckerState { let scrutinee = self.check_element(scrutinee, owner)?; // which variant are we, if any - let matching: Option<(String, Element)> = match scrutinee { Element::Inject { ref field, @@ -326,6 +325,18 @@ impl CheckerState { ), }; + // are we allowed to posit the equality of elements scrutinee = + // (arm.tag). (arm.bound) when looking at necessarily + // non-matching arms? + let posit_equality_with = match &scrutinee { + Element::Var(v) => Some(v.clone()), + Element::Inject { .. } + | Element::Project { .. } + | Element::Case { .. } + | Element::Literal(_) + | Element::Record(_) => None, + }; + // for each arm, recurse with a concrete value (if we have one) // otherwise fall back to hypothetical elements; in the former // case record the end result @@ -333,7 +344,8 @@ impl CheckerState { let mut processed_arms = Vec::new(); for arm in arms { let OwnedField { - field: field_set, .. + field: field_set, + owner, } = self.lookup_variant_field(&arm.tag)?; let mut ctx = self.clone(); @@ -345,7 +357,9 @@ impl CheckerState { { let canonical = ctx.make_element_definition(binding_name, inner.clone(), binding_set)?; - let output = ctx.check_element((&arm.body).into(), set)?; + let this_set = ctx.check_set(set)?; + + let output = ctx.check_element((&arm.body).into(), &this_set)?; if matches!(computed_output, Some(_)) { panic!( "invariant violation: we somehow matched multiple arms in case analysis" @@ -359,7 +373,20 @@ impl CheckerState { } } else { let canonical = ctx.make_element_binding(binding_name, binding_set)?; - let body = ctx.check_element((&arm.body).into(), set)?; + + if let Some(ref scrutinee_var) = posit_equality_with { + ctx.make_element_definition( + scrutinee_var.clone(), + Element::Inject { + field: arm.tag.clone(), + element: Box::new(Element::Var(canonical.clone())), + }, + owner.clone(), + )?; + }; + let this_set = ctx.check_set(set)?; + let body = ctx.check_element((&arm.body).into(), &this_set)?; + CaseArm { tag: arm.tag.clone(), bound: canonical, diff --git a/src/checker_signature.rs b/src/checker_signature.rs index cc6cadc..ab54fd1 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -10,6 +10,7 @@ impl CheckerState { pub fn check_signature(&self, signature: &Signature) -> Result { match signature { Signature::Set => Ok(Signature::Set), + Signature::FromSet(set) => Ok(Signature::FromSet(self.check_set(set)?)), Signature::Var(v) => { let deref = self.lookup_signature(&v)?; Ok(deref.clone()) @@ -64,6 +65,7 @@ impl CheckerState { .into_iter() .map(|Param { name, set }| { let canonical = ctx.make_element_binding(name, set.clone())?; + let set = ctx.check_set(&set)?; Ok(Param { name: canonical, set, @@ -129,6 +131,22 @@ impl CheckerState { Ok(Instance::SetCoerce(set)) } } + Instance::ElementCoerce(element) => { + if let Some(signature) = signature { + let Signature::FromSet(set) = signature else { + return Err(CheckerError::WrongSignatureForInstance { + value: instance.clone().into(), + real: Signature::FromSet(Set::Var("_".to_string())), + claimed: signature.clone(), + }); + }; + let element = self.check_element(element, set)?; + Ok(Instance::ElementCoerce(element)) + } else { + // todo!("how do we handle check_element without a set?"); + Ok(Instance::ElementCoerce(element.clone())) + } + } Instance::Var(v) => { // Exactly the same discipline as for Element::Var, see there // for some sparse comments @@ -260,7 +278,11 @@ impl CheckerState { .instance; Ok(sub_element) } - _ => panic!( + Instance::For { .. } + | Instance::ElementCoerce(_) + | Instance::SetCoerce(_) + | Instance::App { .. } + | Instance::Case { .. } => panic!( "invariant violation: check_instance returned neither a record or stuck computation for record set" ), } @@ -314,11 +336,21 @@ impl CheckerState { ), }; + let posit_equality_with = match &scrutinee { + Element::Var(v) => Some(v.clone()), + Element::Inject { .. } + | Element::Project { .. } + | Element::Case { .. } + | Element::Literal(_) + | Element::Record(_) => None, + }; + let mut computed_output = None; let mut processed_arms = Vec::new(); for arm in arms { let OwnedField { - field: field_set, .. + field: field_set, + owner, } = self.lookup_variant_field(&arm.tag)?; let mut ctx = self.clone(); @@ -330,7 +362,15 @@ impl CheckerState { { let canonical = ctx.make_element_definition(binding_name, inner.clone(), binding_set)?; - let output = ctx.check_instance((&arm.body).into(), signature)?; + let this_signature = if let Some(signature) = signature { + let signature = ctx.check_signature(signature)?; + Some(signature) + } else { + None + }; + + let output = + ctx.check_instance((&arm.body).into(), this_signature.as_ref())?; if matches!(computed_output, Some(_)) { panic!( "invariant violation: we somehow matched multiple arms in case analysis" @@ -344,7 +384,26 @@ impl CheckerState { } } else { let canonical = ctx.make_element_binding(binding_name, binding_set)?; - let body = ctx.check_instance((&arm.body).into(), signature)?; + if let Some(ref scrutinee_var) = posit_equality_with { + ctx.add_element( + scrutinee_var.clone(), + Element::Inject { + field: arm.tag.clone(), + element: Box::new(Element::Var(canonical.clone())), + } + .into(), + owner.clone(), + )?; + }; + let this_signature = if let Some(signature) = signature { + let signature = ctx.check_signature(signature)?; + Some(signature) + } else { + None + }; + + let body = + ctx.check_instance((&arm.body).into(), this_signature.as_ref())?; CaseArm { tag: arm.tag.clone(), bound: canonical, @@ -508,7 +567,7 @@ impl CheckerState { // nevertheless we need the tiniest amount of bidirectionality // here to deal with case, project, and var recursively - let subject_sig: Option = self.stuck_subject_signature(&subject)?; + let subject_sig: Option = self._stuck_subject_signature(&subject)?; if let Some(subject_sig) = subject_sig { let Signature::Ext { params, codomain } = subject_sig else { @@ -567,7 +626,7 @@ impl CheckerState { ctx.check_instance(&residual, signature) } } - Instance::Record(_) | Instance::SetCoerce(_) => { + Instance::Record(_) | Instance::SetCoerce(_) | Instance::ElementCoerce(_) => { Err(CheckerError::NonFunctionalInstance { instance: subject, elements: args, @@ -611,7 +670,7 @@ impl CheckerState { Ok((ctx, checked)) } - fn stuck_subject_signature(&self, inst: &Instance) -> Result, CheckerError> { + fn _stuck_subject_signature(&self, inst: &Instance) -> Result, CheckerError> { match inst { Instance::Var(v) => Ok(Some(self.lookup_instance(v)?.container.clone())), Instance::Project { field, .. } => { @@ -620,10 +679,14 @@ impl CheckerState { // All arms of a stuck Case share a signature by the case // elimination typing rule, and we've already expanded the body, so // we can pick any arm. - Instance::Case { arms, .. } => self - .stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body), - Instance::For { .. } | Instance::Record(_) | Instance::SetCoerce(_) => Ok(None), + // TODO! this is wrong! + Instance::Case { arms, .. } => self + ._stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body), + Instance::ElementCoerce(_) + | Instance::For { .. } + | Instance::Record(_) + | Instance::SetCoerce(_) => Ok(None), Instance::App { .. } => unreachable!( "invariant violation: _stuck_head_signature called on a left-nested App" diff --git a/src/checker_state.rs b/src/checker_state.rs index ad01d50..a88c6b0 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -399,7 +399,7 @@ impl CheckerState { Signature::Ext { codomain, .. } => { self._register_signature_fields(codomain, rebind)?; } - _ => (), + Signature::Var(_) | Signature::Set | Signature::FromSet(_) => (), } Ok(()) } diff --git a/src/parser.rs b/src/parser.rs index f205407..73e8dd3 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -45,12 +45,12 @@ parser! { rule kw_false() = "false" wb() rule keyword() = - kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance() - / kw_record() / kw_variant() / kw_theory() - / kw_case() / kw_of() / kw_for() - / kw_Set() / kw_set_of() / kw_set() - / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() - / kw_true() / kw_false() + kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance() + / kw_record() / kw_variant() / kw_theory() + / kw_case() / kw_of() / kw_for() + / kw_Set() / kw_set_of() / kw_set() + / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() + / kw_true() / kw_false() // ==================================================================== // Identifiers @@ -134,19 +134,20 @@ parser! { = kw_set_of() _ "(" _ i:instance() _ ")" { i } rule set() -> Set - = kw_record() _ "{" _ fs:(set_field() ** ",") _ "}" { Set::Record(fs) } - / kw_variant() _ "[" _ vs:(variant_field() ** "|") _ "]" { Set::Variant(vs) } - / b:builtin() { Set::BuiltIn(b) } - / i:claimed_set() { Set::ClaimedSet(i) } - / v:set_var() { Set::Var(v) } - / "(" _ s:set() _ ")" { s } + = kw_record() _ "{" _ fs:(set_field() ** ",") _ "}" { Set::Record(fs) } + / kw_variant() _ "[" _ vs:(variant_field() ** "|") _ "]" { Set::Variant(vs) } + / b:builtin() { Set::BuiltIn(b) } + / i:claimed_set() { Set::ClaimedSet(i) } + / v:set_var() { Set::Var(v) } + / "(" _ s:set() _ ")" { s } // ==================================================================== // Signatures // ==================================================================== rule param() -> Param - = "(" _ n:elem_var() _ ":" _ s:set() _ ")" { Param { name: n, set: s } } + = "(" _ n:elem_var() _ ":" _ s:set() _ ")" + { Param { name: n, set: s } } rule param_list() -> Vec = param() ++ _ @@ -168,11 +169,12 @@ parser! { } rule signature() -> Signature - = kw_Set() { Signature::Set } - / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } - / s:sig_ext() { s } - / v:sig_var() { Signature::Var(v) } - / "(" _ s:signature() _ ")" { s } + = kw_Set() { Signature::Set } + / "<" _ s:set() _ ">" { Signature::FromSet(s) } + / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } + / s:sig_ext() { s } + / v:sig_var() { Signature::Var(v) } + / "(" _ s:signature() _ ")" { s } // ==================================================================== // Elements @@ -204,9 +206,8 @@ parser! { { CaseArm { tag: t, bound: x, body } } rule element() -> Element - = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" - { Element::Case { scrutinee: Box::new(scrut), arms } } - / d:dot_elem() { d } + = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } + / d:dot_elem() { d } // ==================================================================== // Instances @@ -221,10 +222,12 @@ parser! { { InstAssign { name: n, instance: i } } rule explicit_set_coerce() -> Set - = s:set() _ "::" _ kw_Set() { s } + = s:set() _ "::" _ kw_Set() + { s } rule atom_inst() -> Instance = s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) } + / "<" _ e:element() _ ">" { Instance::ElementCoerce(e) } / v:inst_var() { Instance::Var(v) } / f:sig_var() { Instance::Var(f) } / "{" _ fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) } @@ -269,24 +272,19 @@ parser! { } rule instance() -> Instance - = i:inst_for() { i } - / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" - { Instance::Case { scrutinee: Box::new(scrut), arms } } - / app_inst() + = i:inst_for() { i } + / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" { Instance::Case { scrutinee: Box::new(scrut), arms } } + / a:app_inst() { a } // ==================================================================== // Top-level declarations // ==================================================================== rule decl() -> Decl - = kw_let_set() _ n:set_var() _ "=" _ s:set() - { Decl::Set { name: n, set: s } } - / kw_let_element() _ n:elem_var() _ ":" _ s:set() _ "=" _ e:element() - { Decl::Element { name: n, set: s, element: e } } - / kw_let_signature() _ n:sig_var() _ "=" _ sg:signature() - { Decl::Signature { name: n, signature: sg } } - / kw_let_instance() _ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance() - { Decl::Instance { name: n, signature: sg, instance: i } } + = kw_let_set() _ n:set_var() _ "=" _ s:set() { Decl::Set { name: n, set: s } } + / kw_let_element() _ n:elem_var() _ ":" _ s:set() _ "=" _ e:element() { Decl::Element { name: n, set: s, element: e } } + / kw_let_signature() _ n:sig_var() _ "=" _ sg:signature() { Decl::Signature { name: n, signature: sg } } + / kw_let_instance() _ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance() { Decl::Instance { name: n, signature: sg, instance: i } } pub rule program() -> Programme = _ ds:(decl() ** _) _ { Programme(ds) } -- cgit v1.3.1