From 85f0f5bd9ba573ad288ed582399b37e126f598c9 Mon Sep 17 00:00:00 2001 From: tslil Date: Fri, 24 Apr 2026 08:37:02 +0100 Subject: checking for injections, projections, rm vesitigial App --- src/ast.rs | 3 -- src/checker.rs | 116 +++++++++++++++++++++++++++++++++++++++++++-------------- src/main.rs | 6 +++ src/parser.rs | 16 ++------ 4 files changed, 98 insertions(+), 43 deletions(-) (limited to 'src') diff --git a/src/ast.rs b/src/ast.rs index 1b34fc3..f517b37 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -126,9 +126,6 @@ pub enum Element { element: Box, }, - #[display("{_0} {_1}")] - App(Box, Box), - #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] Case { scrutinee: Box, diff --git a/src/checker.rs b/src/checker.rs index d45a5a4..2c6c5d0 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -32,10 +32,10 @@ pub enum CheckError { } #[derive(Display)] -#[display("{value} @ {belongs_to}")] +#[display("{field_set} @ {owner_set}")] struct SetField { - value: Set, - belongs_to: Set, + field_set: Set, + owner_set: Set, } #[derive(Display)] @@ -109,52 +109,48 @@ impl CheckState { set_ref: &SetField, belongs_to: &Set, ) -> Result<(), CheckError> { - let SetField { - value: _, - belongs_to: owner, - } = set_ref; - if !self.set_equal(owner, belongs_to) { + if !self.set_equal(&set_ref.owner_set, belongs_to) { Err(CheckError::Rebinding(name.clone())) } else { Ok(()) } } - #[instrument(skip(self), level = "debug", fields(%name, %set, %belongs_to))] + #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))] fn add_record_field( &mut self, name: &String, - set: &Set, - belongs_to: &Set, + field_set: &Set, + owner_set: &Set, ) -> Result<(), CheckError> { if let Some(set_ref) = self.record_fields.get(name) { - self.assert_correct_owner(name, set_ref, belongs_to)?; + self.assert_correct_owner(name, set_ref, owner_set)?; }; self.record_fields.insert( name.clone(), SetField { - value: set.clone(), - belongs_to: belongs_to.clone(), + field_set: field_set.clone(), + owner_set: owner_set.clone(), }, ); Ok(()) } - #[instrument(skip(self), level = "debug", fields(%name, %set, %belongs_to))] + #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))] fn add_variant_field( &mut self, name: &String, - set: &Set, - belongs_to: &Set, + field_set: &Set, + owner_set: &Set, ) -> Result<(), CheckError> { if let Some(set_ref) = self.variant_fields.get(name) { - self.assert_correct_owner(name, set_ref, belongs_to)?; + self.assert_correct_owner(name, set_ref, owner_set)?; }; self.variant_fields.insert( name.clone(), SetField { - value: set.clone(), - belongs_to: belongs_to.clone(), + field_set: field_set.clone(), + owner_set: owner_set.clone(), }, ); Ok(()) @@ -167,19 +163,19 @@ impl CheckState { Set::Record(fields) => { for RecordField { name: rfn, - set: rset, + set: field_set, } in fields { - self.add_record_field(rfn, rset, &set)?; + self.add_record_field(rfn, field_set, &set)?; } } Set::Variant(fields) => { for VariantField { name: vfn, - set: vset, + set: field_set, } in fields { - self.add_variant_field(vfn, vset, &set)?; + self.add_variant_field(vfn, field_set, &set)?; } } _ => (), @@ -377,11 +373,75 @@ impl CheckState { // resign? Ok(Element::Record(assignations)) } - Element::Project { .. } => { - Err(CheckError::Unimplemented("element project".to_string())) + Element::Project { + element: inner, + field, + } => { + // globally unique projections mean we know what the sets going + // in and out must be + let Some(SetField { + field_set, + owner_set, + }) = self.record_fields.get(field) + else { + return Err(CheckError::Unbound(field.clone())); + }; + + // enforce the correct typing of the claimed result + if !self.set_equal(set, field_set) { + return Err(CheckError::WrongSetForElement( + set.clone(), + field_set.clone(), + )); + } + + // enforce the correct typing of the element + let inner = self.check_element(inner, owner_set)?; + + // Unfortunately we still have to do something nasty here to obtain the data + let Element::Record(assignations) = inner else { + panic!("invariant violation: check_element returned non-record for record set"); + }; + let sub_element = assignations + .into_iter() + .find(|a| a.name == *field) + .expect("invariant violation: record missing field that was type-checked") + .element + .clone(); + + Ok(sub_element) + } + Element::Inject { + element: inner, + field, + } => { + // globally unique injections mean that we know what the sets + // going in and out must be, but compared to projections their + // roles are here interchanged + let Some(SetField { + field_set, + owner_set, + }) = self.variant_fields.get(field) + else { + return Err(CheckError::Unbound(field.clone())); + }; + + // enforce the correct typing of the claimed result + if !self.set_equal(set, owner_set) { + return Err(CheckError::WrongSetForElement( + set.clone(), + owner_set.clone(), + )); + } + + // enforce the correct typing of the element + let element = self.check_element(inner, field_set)?; + + Ok(Element::Inject { + element: Box::new(element), + field: field.clone(), + }) } - Element::Inject { .. } => Err(CheckError::Unimplemented("element inject".to_string())), - Element::App(_, _) => Err(CheckError::Unimplemented("element app".to_string())), Element::Case { .. } => Err(CheckError::Unimplemented("element case".to_string())), } } diff --git a/src/main.rs b/src/main.rs index e389983..f7ad1c1 100644 --- a/src/main.rs +++ b/src/main.rs @@ -22,10 +22,16 @@ let set Y = X let set Z = record { .y : Y } +let set W = variant [ z. : Z | f. : Float ] + let element x : X = { .b = true, .n = 41 } let element z : Z = { .y = x } +let element the_nat : Nat = z .y .n + +let element w : W = f. 1.44 + // let signature Graph = theory { // .Node :: Set, // .Edge :: (s : Node) (t : Node) -> Set diff --git a/src/parser.rs b/src/parser.rs index 8b75c2c..5dd777b 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -120,7 +120,7 @@ parser! { rule set() -> Set = kw_record() _ "{" fs:(set_field() ** ",") _ "}" { Set::Record(fs) } - / kw_variant() _ "{" _ vs:(variant_field() ** "|") "}" { Set::Variant(vs) } + / 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) } @@ -165,20 +165,12 @@ parser! { }) } - rule app_elem() -> Element - = head:dot_elem() tail:(__ d:dot_elem() { d })* - { - tail.into_iter().fold(head, |acc, a| { - Element::App(Box::new(acc), Box::new(a)) - }) - } - rule case_arm() -> CaseArm = t:inject() _ x:elem_var() _ "=>" _ body:element() { CaseArm { tag: t, bound: x, body } } rule element() -> Element = kw_case() __ scrut:element() _ kw_of() _ "{" arms:(_ a:case_arm() _ { a }) ** "|" _ "}" { Element::Case { scrutinee: Box::new(scrut), arms } } - / app_elem() + / d:dot_elem() { d } // instance layer @@ -258,10 +250,10 @@ let set Config = record { .label : Str } -let set Maybe = variant { +let set Maybe = variant [ none. : record {} | some. : Config -} +] "#; debug_parse(src); -- cgit v1.3.1