From 36a9377163ecd3300f7b9ad3c4d8e93d97ce41ff Mon Sep 17 00:00:00 2001 From: tslil Date: Fri, 24 Apr 2026 10:44:41 +0100 Subject: computing cases --- src/check_state.rs | 223 ---------------------------------------- src/checker.rs | 21 ++-- src/checker_set.rs | 283 +++++++++++++++++++++++++++++++++++++++++++++++++++ src/checker_state.rs | 233 ++++++++++++++++++++++++++++++++++++++++++ src/main.rs | 8 +- src/parser.rs | 6 +- src/set_checker.rs | 205 ------------------------------------- 7 files changed, 534 insertions(+), 445 deletions(-) delete mode 100644 src/check_state.rs create mode 100644 src/checker_set.rs create mode 100644 src/checker_state.rs delete mode 100644 src/set_checker.rs (limited to 'src') diff --git a/src/check_state.rs b/src/check_state.rs deleted file mode 100644 index d775993..0000000 --- a/src/check_state.rs +++ /dev/null @@ -1,223 +0,0 @@ -use crate::ast::*; -use tracing::instrument; - -use derive_more::Display; -use std::collections::HashMap; -use std::fmt; - -#[derive(Display)] -pub enum CheckError { - #[display("Unbound: {_0}")] - Unbound(String), - #[display("Rebinding: {_0}")] - Rebinding(String), - #[display("The following functionality is unimplemented: {_0}")] - Unimplemented(String), - #[display("Element claimed to belong to {_0} but actually belongs to {_1}")] - WrongSetForElement(Set, Set), - #[display("Element {element} does belong to set {claimed}: {reason}")] - ElementDoesNotBelong { - element: Element, - claimed: Set, - reason: String, - }, -} - -#[derive(Display)] -#[display("{field_set} @ {owner_set}")] -pub struct SetField { - pub field_set: Set, - pub owner_set: Set, -} - -#[derive(Display)] -#[display("{element} : {set}")] -pub struct CheckedElement { - pub element: Element, - pub set: Set, -} - -#[derive(Default)] -pub struct CheckState { - wf_sets: HashMap, - wf_elements: HashMap, - wf_signatures: HashMap, - wf_instances: HashMap, - record_fields: HashMap, - variant_fields: HashMap, -} - -impl fmt::Display for CheckState { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - fn section(f: &mut fmt::Formatter<'_>, name: &str, map: &HashMap) -> fmt::Result - where - K: fmt::Display + Ord, - V: fmt::Display, - { - write!(f, " {name} = {{")?; - let mut entries: Vec<_> = map.iter().collect(); - entries.sort_by(|a, b| a.0.cmp(b.0)); - for (k, v) in entries { - write!(f, "{k} ~> {v}, ")?; - } - write!(f, "}},") - } - - write!(f, "CheckState {{")?; - section(f, "sets", &self.wf_sets)?; - section(f, "elements", &self.wf_elements)?; - section(f, "record_fields", &self.record_fields)?; - section(f, "variant_fields", &self.variant_fields)?; - section(f, "signatures", &self.wf_signatures)?; - section(f, "instances", &self.wf_instances)?; - write!(f, " }}")?; - Ok(()) - } -} - -// The invariant we're maintaining is that everything is fully evaluated before -// we commit it to be stored in the state. -impl CheckState { - // Because of our invariant we don't actually need to do anything - // non-trivial here. - #[instrument(skip(self), level = "debug", fields(%set_a, %set_b))] - pub fn set_equal(&self, set_a: &Set, set_b: &Set) -> bool { - set_a == set_b - } - - #[instrument(skip(self), level = "debug")] - fn assert_unbound_set(&self, name: &String) -> Result<(), CheckError> { - if self.wf_sets.contains_key(name) { - Err(CheckError::Rebinding(name.clone())) - } else { - Ok(()) - } - } - - #[instrument(skip(self), level = "debug")] - fn assert_unbound_element(&self, name: &String) -> Result<(), CheckError> { - if self.wf_elements.contains_key(name) { - Err(CheckError::Rebinding(name.clone())) - } else { - Ok(()) - } - } - - #[instrument(skip(self), level = "debug", fields(%name, %set_ref, %belongs_to))] - fn assert_correct_owner( - &self, - name: &String, - set_ref: &SetField, - belongs_to: &Set, - ) -> Result<(), CheckError> { - if !self.set_equal(&set_ref.owner_set, belongs_to) { - Err(CheckError::Rebinding(name.clone())) - } else { - Ok(()) - } - } - - #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))] - fn add_record_field( - &mut self, - name: &String, - 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, owner_set)?; - }; - self.record_fields.insert( - name.clone(), - SetField { - field_set: field_set.clone(), - owner_set: owner_set.clone(), - }, - ); - Ok(()) - } - - #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))] - fn add_variant_field( - &mut self, - name: &String, - 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, owner_set)?; - }; - self.variant_fields.insert( - name.clone(), - SetField { - field_set: field_set.clone(), - owner_set: owner_set.clone(), - }, - ); - Ok(()) - } - - #[instrument(skip(self), level = "debug", fields(%name, %set))] - pub fn add_set(&mut self, name: &String, set: Set) -> Result<(), CheckError> { - self.assert_unbound_set(name)?; - match &set { - Set::Record(fields) => { - for RecordField { - name: rfn, - set: field_set, - } in fields - { - self.add_record_field(rfn, field_set, &set)?; - } - } - Set::Variant(fields) => { - for VariantField { - name: vfn, - set: field_set, - } in fields - { - self.add_variant_field(vfn, field_set, &set)?; - } - } - _ => (), - }; - self.wf_sets.insert(name.clone(), set); - Ok(()) - } - - pub fn add_element( - &mut self, - name: &String, - element: Element, - set: Set, - ) -> Result<(), CheckError> { - self.assert_unbound_element(name)?; - self.wf_elements - .insert(name.clone(), CheckedElement { element, set }); - Ok(()) - } - - pub fn lookup_set(&self, name: &String) -> Result<&Set, CheckError> { - self.wf_sets - .get(name) - .map_or(Err(CheckError::Unbound(name.clone())), Ok) - } - - pub fn lookup_element(&self, name: &String) -> Result<&CheckedElement, CheckError> { - self.wf_elements - .get(name) - .map_or(Err(CheckError::Unbound(name.clone())), Ok) - } - - pub fn lookup_record_field(&self, name: &String) -> Result<&SetField, CheckError> { - self.record_fields - .get(name) - .map_or(Err(CheckError::Unbound(name.clone())), Ok) - } - - pub fn lookup_variant_field(&self, name: &String) -> Result<&SetField, CheckError> { - self.variant_fields - .get(name) - .map_or(Err(CheckError::Unbound(name.clone())), Ok) - } -} diff --git a/src/checker.rs b/src/checker.rs index 7a7f4d4..3ebcb4d 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -1,23 +1,22 @@ use crate::ast::*; -use crate::check_state::{CheckError, CheckState}; +use crate::checker_state::{CheckerError, CheckerState}; use tracing::{debug, instrument}; impl Programme { - pub fn check(&self) -> Result<(), CheckError> { - let mut state = CheckState::default(); + pub fn check(&self) -> Result<(), CheckerError> { + let mut state = CheckerState::default(); state.check(self) } } -impl CheckState { +impl CheckerState { #[instrument(skip(self, prog), level = "debug")] - pub fn check(&mut self, prog: &Programme) -> Result<(), CheckError> { + pub fn check(&mut self, prog: &Programme) -> Result<(), CheckerError> { let Programme(decls) = prog; for decl in decls { - debug!(%self); - debug!(%decl); + debug!(%self, %decl); match decl { Decl::Set { name, set } => { let set = self.check_set(set)?; @@ -27,17 +26,17 @@ impl CheckState { Decl::Element { name, element, set } => { let set = self.check_set(set)?; let element = self.check_element(element, &set)?; - self.add_element(name, element, set) + self.add_element(name.clone(), element, set) } Decl::Signature { .. } => { - return Err(CheckError::Unimplemented("signatures".to_string())); + return Err(CheckerError::Unimplemented("signatures".to_string())); } Decl::Instance { .. } => { - return Err(CheckError::Unimplemented("instances".to_string())); + return Err(CheckerError::Unimplemented("instances".to_string())); } }?; } - debug!(%self, "END"); + debug!(%self); Ok(()) } } diff --git a/src/checker_set.rs b/src/checker_set.rs new file mode 100644 index 0000000..a14ac9a --- /dev/null +++ b/src/checker_set.rs @@ -0,0 +1,283 @@ +use crate::ast::*; +use crate::checker_state::*; + +use std::iter::zip; +use tracing::instrument; + +impl CheckerState { + #[instrument(skip(self), level = "debug", fields(%set))] + pub fn check_set(&self, set: &Set) -> Result { + match set { + Set::BuiltIn(_) => Ok(set.clone()), + Set::Record(fields) => { + let fields = fields + .iter() + .map(|RecordField { name, set }| { + let set = self.check_set(set)?; + Ok(RecordField { + name: name.clone(), + set, + }) + }) + .collect::, _>>()?; + Ok(Set::Record(fields)) + } + Set::Variant(fields) => { + let fields = fields + .iter() + .map(|VariantField { name, set }| { + let set = self.check_set(set)?; + Ok(VariantField { + name: name.clone(), + set, + }) + }) + .collect::, _>>()?; + Ok(Set::Variant(fields)) + } + Set::ClaimedSet(_) => Err(CheckerError::Unimplemented("instances as sets".to_string())), + Set::Var(v) => { + let deref = self.lookup_set(v)?; + Ok(deref.clone()) + } + } + } + + fn _check_literal_set_helper(&self, claimed: &Set, should_be: Set) -> Result<(), CheckerError> { + if !self.set_equal(claimed, &should_be) { + Err(CheckerError::WrongSetForElement(claimed.clone(), should_be)) + } else { + Ok(()) + } + } + + #[instrument(skip(self), level = "debug", fields(%element, %set))] + pub fn check_element(&self, element: &Element, set: &Set) -> Result { + match element { + Element::Literal(lit) => { + // we may infer the type from the element + match lit { + Literal::Int(_) => { + self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Int))?; + } + Literal::Nat(_) => { + self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Nat))?; + } + Literal::Str(_) => { + self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Str))?; + } + Literal::Bool(_) => { + self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Bool))?; + } + Literal::Float(_) => { + self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Float))?; + } + } + Ok(element.clone()) + } + Element::Var(v) => { + let lookup = self.lookup_element(v)?; + // we have previously done the work to discover the type of + // this element, so what we're claiming now must match! + if !self.set_equal(set, &lookup.set) { + return Err(CheckerError::WrongSetForElement( + set.clone(), + lookup.set.clone(), + )); + } + Ok(lookup.element.clone()) + } + Element::Record(assignations) => { + let rej = |reason| CheckerError::ElementDoesNotBelong { + element: element.clone(), + claimed: set.clone(), + reason, + }; + + // make sure we are filling a record + let fields = if let Set::Record(fields) = set { + Ok(fields) + } else { + 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(); + 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(); + element_fnames_sorted.sort(); + + if set_fnames_sorted != element_fnames_sorted { + return Err(rej(format!( + "expected [{}] but found [{}]", + set_fnames.join(", "), + element_fnames.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, &e_s)) + .collect::, _>>()?; + // rebuild + let assignations = zip(element_fnames, sub_els) + .map(|(name, element)| ElemAssign { name, element }) + .collect(); + // resign? + Ok(Element::Record(assignations)) + } + Element::Project { + element: inner, + field, + } => { + // globally unique projections mean we know what the sets going + // in and out must be + let SetField { + field_set, + owner_set, + } = self.lookup_record_field(field)?; + + // enforce the correct typing of the claimed result + if !self.set_equal(set, field_set) { + return Err(CheckerError::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 SetField { + field_set, + owner_set, + } = self.lookup_variant_field(field)?; + + // enforce the correct typing of the claimed result + if !self.set_equal(set, owner_set) { + return Err(CheckerError::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::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(), + )); + } + + // 1. Syntactic checks + // ------------------- + // arms agree on the set to which the scrutinee should belong + let arm_owners = arms + .iter() + .map(|ca| self.lookup_variant_field(&ca.tag).map(|sf| &sf.owner_set)) + .collect::, _>>()?; + let owner = arm_owners[0]; // safe because of the above decision about bottom + if !arm_owners.iter().all(|o| self.set_equal(owner, o)) { + return Err(CheckerError::IncosistentCaseScrutineeSet(element.clone())); + } + + // all cases are handled + let Set::Variant(fields) = owner else { + panic!( + "invariant violation: looking up the owner of a variant field resulted in a non-variant set", + ) + }; + let mut required_field_names_sorted: Vec = + fields.iter().map(|vf| vf.name.clone()).collect(); + required_field_names_sorted.sort(); + let mut covered_field_names_sorted: Vec = + arms.iter().map(|ca| ca.tag.clone()).collect(); + covered_field_names_sorted.sort(); + if required_field_names_sorted != covered_field_names_sorted { + return Err(CheckerError::IncompleteCaseAnalysis { + found: covered_field_names_sorted, + required: required_field_names_sorted, + }); + } + + // 2. semantic checks + // ------------------ + + // scrutinee must be of the same set that all the arms are + // implying, in particular this implies that the following holds + // `inner : self.lookup_variant_field(field).field_set` + let scrutinee = self.check_element(scrutinee, owner)?; + + // which variant are we? + let Element::Inject { + field, + element: inner, + } = scrutinee + else { + panic!( + "invariant violation: we believe element is of a variant set but it's not an injection" + ); + }; + + // TODO: we would like to check that each arm is correct, but + // there's no easy way to do this? we can insert hypothetical + // elements of the correct type into the checkerstate, but if + // the body exacts non-trivial computation we won't be to pass + // further checks. In the future would could build first class + // support for hypothetical elements and do proper bi-di + // checking, but for now we only check the branch that matters. + + let CaseArm { tag, bound, body } = arms.iter().find(|ca| ca.tag == field).expect("invariant violation: we know that all cases are covered and that the element is of the valid type"); + let SetField { field_set, .. } = self.lookup_variant_field(tag)?; + // TODO: if we were worried about overhead we'd have a separate + // locals stack, though truly if we were worried about overhead + // we'd not have NNN instances of clone elsewhere in the + // codebase and we wouldn't be eagerly evaluating all + // expressions fully. + let mut new_context = self.clone(); + new_context.add_element(bound.clone(), *inner.clone(), field_set.clone())?; + let computed = new_context.check_element(body, set)?; + + Ok(computed) + } + } + } +} diff --git a/src/checker_state.rs b/src/checker_state.rs new file mode 100644 index 0000000..c4b4a3a --- /dev/null +++ b/src/checker_state.rs @@ -0,0 +1,233 @@ +use crate::ast::*; +use tracing::instrument; + +use derive_more::Display; +use std::collections::HashMap; +use std::fmt; + +#[derive(Display)] +pub enum CheckerError { + #[display("Unbound: {_0}")] + Unbound(String), + #[display("Rebinding: {_0}")] + Rebinding(String), + #[display("The following functionality is unimplemented: {_0}")] + Unimplemented(String), + #[display("Element claimed to belong to {_0} but actually belongs to {_1}")] + WrongSetForElement(Set, Set), + #[display("Element {element} does belong to set {claimed}: {reason}")] + ElementDoesNotBelong { + element: Element, + claimed: Set, + reason: String, + }, + #[display("Case analysis {_0} does not have consistent set for scrutinee")] + IncosistentCaseScrutineeSet(Element), + #[display("Incomplete case analysis: covered [{}] but required [{}]", + found.join(", "), + required.join(", ") + )] + IncompleteCaseAnalysis { + found: Vec, + required: Vec, + }, +} + +#[derive(Display, Clone)] +#[display("{field_set} @ {owner_set}")] +pub struct SetField { + pub field_set: Set, + pub owner_set: Set, +} + +#[derive(Display, Clone)] +#[display("{element} : {set}")] +pub struct CheckedElement { + pub element: Element, + pub set: Set, +} + +#[derive(Default, Clone)] +pub struct CheckerState { + wf_sets: HashMap, + wf_elements: HashMap, + wf_signatures: HashMap, + wf_instances: HashMap, + record_fields: HashMap, + variant_fields: HashMap, +} + +impl fmt::Display for CheckerState { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + fn section(f: &mut fmt::Formatter<'_>, name: &str, map: &HashMap) -> fmt::Result + where + K: fmt::Display + Ord, + V: fmt::Display, + { + writeln!(f, " {name} = {{")?; + let mut entries: Vec<_> = map.iter().collect(); + entries.sort_by(|a, b| a.0.cmp(b.0)); + for (k, v) in entries { + writeln!(f, " {k} ~> {v},")?; + } + writeln!(f, " }},") + } + + writeln!(f, "CheckState {{")?; + section(f, "sets", &self.wf_sets)?; + section(f, "elements", &self.wf_elements)?; + section(f, "record_fields", &self.record_fields)?; + section(f, "variant_fields", &self.variant_fields)?; + section(f, "signatures", &self.wf_signatures)?; + section(f, "instances", &self.wf_instances)?; + writeln!(f, " }}")?; + Ok(()) + } +} + +// The invariant we're maintaining is that everything is fully evaluated before +// we commit it to be stored in the state. +impl CheckerState { + // Because of our invariant we don't actually need to do anything + // non-trivial here. + #[instrument(skip(self), level = "debug", fields(%set_a, %set_b))] + pub fn set_equal(&self, set_a: &Set, set_b: &Set) -> bool { + set_a == set_b + } + + #[instrument(skip(self), level = "debug")] + fn assert_unbound_set(&self, name: &String) -> Result<(), CheckerError> { + if self.wf_sets.contains_key(name) { + Err(CheckerError::Rebinding(name.clone())) + } else { + Ok(()) + } + } + + #[instrument(skip(self), level = "debug")] + fn assert_unbound_element(&self, name: &String) -> Result<(), CheckerError> { + if self.wf_elements.contains_key(name) { + Err(CheckerError::Rebinding(name.clone())) + } else { + Ok(()) + } + } + + #[instrument(skip(self), level = "debug", fields(%name, %set_ref, %belongs_to))] + fn assert_correct_owner( + &self, + name: &String, + set_ref: &SetField, + belongs_to: &Set, + ) -> Result<(), CheckerError> { + if !self.set_equal(&set_ref.owner_set, belongs_to) { + Err(CheckerError::Rebinding(name.clone())) + } else { + Ok(()) + } + } + + #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))] + fn add_record_field( + &mut self, + name: &String, + field_set: &Set, + owner_set: &Set, + ) -> Result<(), CheckerError> { + if let Some(set_ref) = self.record_fields.get(name) { + self.assert_correct_owner(name, set_ref, owner_set)?; + }; + self.record_fields.insert( + name.clone(), + SetField { + field_set: field_set.clone(), + owner_set: owner_set.clone(), + }, + ); + Ok(()) + } + + #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))] + fn add_variant_field( + &mut self, + name: &String, + field_set: &Set, + owner_set: &Set, + ) -> Result<(), CheckerError> { + if let Some(set_ref) = self.variant_fields.get(name) { + self.assert_correct_owner(name, set_ref, owner_set)?; + }; + self.variant_fields.insert( + name.clone(), + SetField { + field_set: field_set.clone(), + owner_set: owner_set.clone(), + }, + ); + Ok(()) + } + + #[instrument(skip(self), level = "debug", fields(%name, %set))] + pub fn add_set(&mut self, name: &String, set: Set) -> Result<(), CheckerError> { + self.assert_unbound_set(name)?; + match &set { + Set::Record(fields) => { + for RecordField { + name: rfn, + set: field_set, + } in fields + { + self.add_record_field(rfn, field_set, &set)?; + } + } + Set::Variant(fields) => { + for VariantField { + name: vfn, + set: field_set, + } in fields + { + self.add_variant_field(vfn, field_set, &set)?; + } + } + _ => (), + }; + self.wf_sets.insert(name.clone(), set); + Ok(()) + } + + pub fn add_element( + &mut self, + name: String, + element: Element, + set: Set, + ) -> Result<(), CheckerError> { + self.assert_unbound_element(&name)?; + self.wf_elements + .insert(name, CheckedElement { element, set }); + Ok(()) + } + + pub fn lookup_set(&self, name: &String) -> Result<&Set, CheckerError> { + self.wf_sets + .get(name) + .map_or(Err(CheckerError::Unbound(name.clone())), Ok) + } + + pub fn lookup_element(&self, name: &String) -> Result<&CheckedElement, CheckerError> { + self.wf_elements + .get(name) + .map_or(Err(CheckerError::Unbound(name.clone())), Ok) + } + + pub fn lookup_record_field(&self, name: &String) -> Result<&SetField, CheckerError> { + self.record_fields + .get(name) + .map_or(Err(CheckerError::Unbound(name.clone())), Ok) + } + + pub fn lookup_variant_field(&self, name: &String) -> Result<&SetField, CheckerError> { + self.variant_fields + .get(name) + .map_or(Err(CheckerError::Unbound(name.clone())), Ok) + } +} diff --git a/src/main.rs b/src/main.rs index df36027..c57eef6 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,8 +1,8 @@ mod ast; -mod check_state; mod checker; +mod checker_set; +mod checker_state; mod parser; -mod set_checker; use tracing_subscriber::{layer::SubscriberExt, util::SubscriberInitExt}; use tracing_tree::HierarchicalLayer; @@ -32,7 +32,9 @@ let element z : Z = { .y = x } let element the_nat : Nat = z .y .n -let element w : W = f. 1.44 +let element injected : W = z. z + +let element compute : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ] // let signature Graph = theory { // .Node :: Set, diff --git a/src/parser.rs b/src/parser.rs index 5dd777b..958f09d 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -169,7 +169,7 @@ parser! { = 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 } } + = kw_case() __ scrut:element() _ kw_of() _ "[" arms:(_ a:case_arm() _ { a }) ** "|" _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } / d:dot_elem() { d } // instance layer @@ -263,10 +263,10 @@ let set Maybe = variant [ fn test_elements() { let src = r#" let element foo : Nat = - case some. config .count of { + case some. config .count of [ none. ignore => 0 | some. n => n - } + ] "#; debug_parse(src); diff --git a/src/set_checker.rs b/src/set_checker.rs deleted file mode 100644 index 5762d9c..0000000 --- a/src/set_checker.rs +++ /dev/null @@ -1,205 +0,0 @@ -use crate::ast::*; -use crate::check_state::*; - -use std::iter::zip; -use tracing::instrument; - -impl CheckState { - #[instrument(skip(self), level = "debug", fields(%set))] - pub fn check_set(&self, set: &Set) -> Result { - match set { - Set::BuiltIn(_) => Ok(set.clone()), - Set::Record(fields) => { - let fields = fields - .iter() - .map(|RecordField { name, set }| { - let set = self.check_set(set)?; - Ok(RecordField { - name: name.clone(), - set, - }) - }) - .collect::, _>>()?; - Ok(Set::Record(fields)) - } - Set::Variant(fields) => { - let fields = fields - .iter() - .map(|VariantField { name, set }| { - let set = self.check_set(set)?; - Ok(VariantField { - name: name.clone(), - set, - }) - }) - .collect::, _>>()?; - Ok(Set::Variant(fields)) - } - Set::ClaimedSet(_) => Err(CheckError::Unimplemented("instances as sets".to_string())), - Set::Var(v) => { - let deref = self.lookup_set(v)?; - Ok(deref.clone()) - } - } - } - - fn _check_literal_set_helper(&self, claimed: &Set, should_be: Set) -> Result<(), CheckError> { - if !self.set_equal(claimed, &should_be) { - Err(CheckError::WrongSetForElement(claimed.clone(), should_be)) - } else { - Ok(()) - } - } - - #[instrument(skip(self), level = "debug", fields(%element, %set))] - pub fn check_element(&self, element: &Element, set: &Set) -> Result { - match element { - Element::Literal(lit) => { - // we may infer the type from the element - match lit { - Literal::Int(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Int))?; - } - Literal::Nat(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Nat))?; - } - Literal::Str(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Str))?; - } - Literal::Bool(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Bool))?; - } - Literal::Float(_) => { - self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Float))?; - } - } - Ok(element.clone()) - } - Element::Var(v) => { - let lookup = self.lookup_element(v)?; - // we have previously done the work to discover the type of - // this element, so what we're claiming now must match! - if !self.set_equal(set, &lookup.set) { - return Err(CheckError::WrongSetForElement( - set.clone(), - lookup.set.clone(), - )); - } - Ok(lookup.element.clone()) - } - Element::Record(assignations) => { - let rej = |reason| CheckError::ElementDoesNotBelong { - element: element.clone(), - claimed: set.clone(), - reason, - }; - - // make sure we are filling a record - let fields = if let Set::Record(fields) = set { - Ok(fields) - } else { - 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(); - 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(); - element_fnames_sorted.sort(); - - if set_fnames_sorted != element_fnames_sorted { - return Err(rej(format!( - "expected [{}] but found [{}]", - set_fnames.join(", "), - element_fnames.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, &e_s)) - .collect::, _>>()?; - // rebuild - let assignations = zip(element_fnames, sub_els) - .map(|(name, element)| ElemAssign { name, element }) - .collect(); - // resign? - Ok(Element::Record(assignations)) - } - Element::Project { - element: inner, - field, - } => { - // globally unique projections mean we know what the sets going - // in and out must be - let SetField { - field_set, - owner_set, - } = self.lookup_record_field(field)?; - - // 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 SetField { - field_set, - owner_set, - } = self.lookup_variant_field(field)?; - - // 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::Case { .. } => Err(CheckError::Unimplemented("element case".to_string())), - } - } -} -- cgit v1.3.1