From 89304b27ea81270684810c18d3315c9d399beaf9 Mon Sep 17 00:00:00 2001 From: tslil Date: Tue, 5 May 2026 11:15:07 +0100 Subject: address remaining TODO, fix issues with left-nesting for for and ext, add motivation blurb to the readme --- src/ast.rs | 2 +- src/checker.rs | 3 +- src/checker_set.rs | 7 +++-- src/checker_signature.rs | 74 +++++++++++++++++++++++++++++++++++------------- src/checker_state.rs | 28 +++++++++++------- src/parser.rs | 32 ++++++++++++++++++--- 6 files changed, 108 insertions(+), 38 deletions(-) (limited to 'src') diff --git a/src/ast.rs b/src/ast.rs index 76b6c9f..e254c65 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -71,7 +71,7 @@ pub enum Signature { #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::>().join(" , "))] Theory(Vec>), - #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::>().join(", "), codomain)] + #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::>().join(""), codomain)] Ext { params: Vec, codomain: Box, diff --git a/src/checker.rs b/src/checker.rs index fdba181..c381ba4 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -16,11 +16,12 @@ impl CheckerState { let Programme(decls) = prog; for decl in decls { + self.reset_binders(); match decl { Decl::Set { name, set } => { self.assert_unbound_set(name)?; let set = self.check_set(set)?; - self.add_set(name.clone(), set.into()) + self.add_set(name.clone(), set) } Decl::Element { name, element, set } => { diff --git a/src/checker_set.rs b/src/checker_set.rs index 98e10ec..a00ea81 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -1,7 +1,7 @@ use crate::ast::*; use crate::checker_state::*; -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; use tracing::instrument; impl CheckerState { @@ -11,6 +11,10 @@ impl CheckerState { Set::BuiltIn(_) => Ok(set.clone()), Set::Record(fields) => { let mut ctx = self.clone(); + let field_set = fields.iter().map(|f| &f.name).collect::>(); + if field_set.len() != fields.len() { + todo!("duplicate fields"); + } let fields = fields .into_iter() .map(|Field { name, carries }| { @@ -260,7 +264,6 @@ impl CheckerState { }) } Element::Case { arms, scrutinee } => { - // TODO: do we allow mapping out of bottom? if arms.is_empty() { return Err(CheckerError::Unimplemented( "mapping out of bottom types".to_string(), diff --git a/src/checker_signature.rs b/src/checker_signature.rs index beb0af6..2888568 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -24,8 +24,27 @@ impl CheckerState { Ok(Param { set, name: canon }) }) .collect::, _>>()?; - let codomain = Box::new(ctx.check_signature(codomain)?); - Ok(Signature::Ext { params, codomain }) + let codomain = ctx.check_signature(codomain)?; + + let result = if let Signature::Ext { + params: inner, + codomain: deep, + } = codomain + { + let mut merged = params.clone(); + merged.extend(inner.iter().cloned()); + Signature::Ext { + params: merged, + codomain: deep, + } + } else { + Signature::Ext { + params, + codomain: Box::new(codomain), + } + }; + + Ok(result) } Signature::Theory(fields) => { let mut ctx = self.clone(); @@ -36,10 +55,7 @@ impl CheckerState { ctx.add_instance(name.clone(), InstanceValue::Hypothetical, signature.clone())?; // And lo, the special case, our chosen canonical form if signature == Signature::Set { - ctx.add_set( - name.clone(), - Set::ClaimedSet(Instance::Var(name.clone())).into(), - )?; + ctx.add_set(name.clone(), Set::ClaimedSet(Instance::Var(name.clone())))?; } new_fields.push(Field { name: name.clone(), @@ -153,7 +169,7 @@ impl CheckerState { if f_s == Signature::Set { ctx.add_set( f_n.clone(), - Set::ClaimedSet(Instance::Var(f_n.clone())).into(), + Set::ClaimedSet(Instance::Var(f_n.clone())), )?; } @@ -316,12 +332,37 @@ impl CheckerState { params: inst_params, body, } => { + if inst_params.is_empty() { + return Err(CheckerError::Unimplemented( + "for instance with empty params".to_string(), + )); + } + + // deal with left-nesting + let mut ctx = self.clone(); + for Param { name, set } in inst_params { + ctx.make_element_binding(name.clone(), set.clone())?; + } + let body = ctx.check_instance(body, None)?; + let (inst_params, body) = if let Instance::For { + params: inner_params, + body: inner_body, + } = body + { + let mut merged = inst_params.clone(); + merged.extend(inner_params.clone()); + (merged, *inner_body) + } else { + (inst_params.clone(), body) + }; + if let Some(signature) = signature { if inst_params.is_empty() { return Err(CheckerError::Unimplemented( "instance for with empty params".to_string(), )); }; + let Signature::Ext { params: sig_params, codomain, @@ -339,11 +380,13 @@ impl CheckerState { claimed: signature.clone(), }); }; + if sig_params.is_empty() { return Err(CheckerError::Unimplemented( "extension signature with empty params".to_string(), )); } + if sig_params.len() != inst_params.len() { return Err(CheckerError::InstanceDoesNotBelong { instance: instance.clone(), @@ -365,7 +408,7 @@ impl CheckerState { set: set_s, }, )| { - let inst_s = ctx.check_set(inst_s)?; + let inst_s = ctx.check_set(&inst_s)?; let set_s = ctx.check_set(set_s)?; if !ctx.equal(&inst_s, &set_s) { return Err(CheckerError::InstanceDoesNotBelong{ @@ -387,7 +430,7 @@ impl CheckerState { }, ) .collect::, _>>()?; - let body = ctx.check_instance(body, Some(&*codomain))?; + let body = ctx.check_instance(&body, Some(&*codomain))?; Ok(Instance::For { body: Box::new(body), params: inst_params, @@ -405,7 +448,7 @@ impl CheckerState { }) }) .collect::, _>>()?; - let body = ctx.check_instance(body, None)?; + let body = ctx.check_instance(&body, None)?; Ok(Instance::For { params: inst_params, body: Box::new(body), @@ -416,18 +459,11 @@ impl CheckerState { instance: inner, args, } => { - // 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 subject = self.check_instance(inner, None)?; - // the whole game here is to make sure that we have no left // nesting, and that we're fully evaluated. If that's true then - // we don't need to come up with signatures for partial - // application. The parser already enforces this, but the - // cunning user may supply ASTs directly so we do this here as - // well. + // structural equality is much more powerful, and partial + // application is simpler. let (subject, args) = match subject { Instance::App { instance: inner_inner, diff --git a/src/checker_state.rs b/src/checker_state.rs index 3404a35..45d2dab 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -272,27 +272,27 @@ impl CheckerState { } #[instrument(skip(self), level = "debug", fields(%name, %set))] - pub fn add_set(&mut self, name: String, set: SetValue) -> Result<(), CheckerError> { + pub fn add_set(&mut self, name: String, set: Set) -> Result<(), CheckerError> { match &set { - SetValue::Concrete(set @ Set::Record(fields)) => { + Set::Record(fields) => { for Field { name: rfn, carries: field_set, } in fields { - self.add_record_field(rfn, field_set, set)?; + self.add_record_field(rfn, field_set, &set)?; } } - SetValue::Concrete(set @ Set::Variant(fields)) => { + Set::Variant(fields) => { for Field { name: vfn, carries: field_set, } in fields { - self.add_variant_field(vfn, field_set, set)?; + self.add_variant_field(vfn, field_set, &set)?; } } - _ => (), + Set::Var(_) | Set::BuiltIn(_) | Set::ClaimedSet(_) => (), }; self.wf_sets.insert(name, set.into()); Ok(()) @@ -394,14 +394,16 @@ impl CheckerState { carries: field_sig, } in fields { - // TODO: are we supposed to recurse? - // let name = self.make_unique_name(); - // self.add_signature(&name, field_sig.clone(), rebind)?; + let inner_name = self.make_unique_name(); + self.add_signature(&inner_name, field_sig.clone(), rebind)?; self.add_signature_field(field_name, field_sig, &signature, rebind)?; } } - // TODO: is there more? - _ => (), + Signature::Ext { codomain, .. } => { + let inner_name = self.make_unique_name(); + self.add_signature(&inner_name, (**codomain).clone(), rebind)?; + } + Signature::Set | Signature::Var(_) => (), }; self.wf_signatures.insert(name.clone(), signature); @@ -487,4 +489,8 @@ impl CheckerState { let n = self.unique_name.fetch_add(1, Ordering::Relaxed); _reserved_name(n) } + + pub fn reset_binders(&mut self) { + self.binder_element.store(0, Ordering::Relaxed); + } } diff --git a/src/parser.rs b/src/parser.rs index 4e41644..31956bd 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -154,11 +154,23 @@ parser! { = _ n:upper_ident() _ "::" _ s:signature() _ { Field { name: n, carries: s } } + rule sig_ext() -> Signature + = ps:param_list() _ "->" _ cod:signature() + { + match cod { + Signature::Ext { params: inner, codomain } => { + let mut all = ps; + all.extend(inner); + Signature::Ext { params: all, codomain } + } + other => Signature::Ext { params: ps, codomain: Box::new(other) }, + } + } + rule signature() -> Signature = kw_Set() { Signature::Set } / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } - / ps:param_list() _ "->" _ cod:signature() - { Signature::Ext { params: ps, codomain: Box::new(cod) } } + / s:sig_ext() { s } / v:sig_var() { Signature::Var(v) } / "(" _ s:signature() _ ")" { s } @@ -243,9 +255,21 @@ parser! { } } - rule instance() -> Instance + rule inst_for() -> Instance = kw_for() _ ps:param_list() _ "," _ body:instance() - { Instance::For { params: ps, body: Box::new(body) } } + { + match body { + Instance::For { params: inner, body } => { + let mut all = ps; + all.extend(inner); + Instance::For { params: all, body } + } + other => Instance::For { params: ps, body: Box::new(other) }, + } + } + + 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() -- cgit v1.3.1