diff options
| -rw-r--r-- | src/checker.rs | 198 | ||||
| -rw-r--r-- | src/main.rs | 6 |
2 files changed, 174 insertions, 30 deletions
diff --git a/src/checker.rs b/src/checker.rs index f3221d9..5f01a7d 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -2,8 +2,9 @@ use crate::ast::*; use tracing::{debug, instrument}; use derive_more::Display; -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; use std::fmt; +use std::iter::zip; impl Programme { pub fn check(&self) -> Result<(), CheckError> { @@ -20,23 +21,38 @@ pub enum CheckError { 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(Debug, Display)] -#[display("{set} @ {belongs_to}")] -struct SetRef { - set: Set, +#[derive(Display)] +#[display("{value} @ {belongs_to}")] +struct SetField { + value: Set, belongs_to: Set, } +#[derive(Display)] +#[display("{element} : {set}")] +struct CheckedElement { + element: Element, + set: Set, +} + #[derive(Default)] struct CheckState { - sets: HashMap<String, Set>, - elements: HashMap<String, Element>, - record_fields: HashMap<String, SetRef>, - variant_fields: HashMap<String, SetRef>, - signatures: HashMap<String, Signature>, - instances: HashMap<String, Instance>, + wf_sets: HashMap<String, Set>, + wf_elements: HashMap<String, CheckedElement>, + wf_signatures: HashMap<String, Signature>, + wf_instances: HashMap<String, Instance>, + record_fields: HashMap<String, SetField>, + variant_fields: HashMap<String, SetField>, } impl fmt::Display for CheckState { @@ -56,12 +72,12 @@ impl fmt::Display for CheckState { } write!(f, "CheckState {{")?; - section(f, "sets", &self.sets)?; - section(f, "elements", &self.elements)?; + 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.signatures)?; - section(f, "instances", &self.instances)?; + section(f, "signatures", &self.wf_signatures)?; + section(f, "instances", &self.wf_instances)?; write!(f, " }}")?; Ok(()) } @@ -70,7 +86,16 @@ impl fmt::Display for CheckState { impl CheckState { #[instrument(skip(self), level = "debug")] fn assert_unbound_set(&self, name: &String) -> Result<(), CheckError> { - if self.sets.contains_key(name) { + 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(()) @@ -81,11 +106,11 @@ impl CheckState { fn assert_correct_owner( &self, name: &String, - set_ref: &SetRef, + set_ref: &SetField, belongs_to: &Set, ) -> Result<(), CheckError> { - let SetRef { - set: _, + let SetField { + value: _, belongs_to: owner, } = set_ref; if !self.set_equal(owner, belongs_to) { @@ -107,8 +132,8 @@ impl CheckState { }; self.record_fields.insert( name.clone(), - SetRef { - set: set.clone(), + SetField { + value: set.clone(), belongs_to: belongs_to.clone(), }, ); @@ -127,8 +152,8 @@ impl CheckState { }; self.variant_fields.insert( name.clone(), - SetRef { - set: set.clone(), + SetField { + value: set.clone(), belongs_to: belongs_to.clone(), }, ); @@ -159,7 +184,14 @@ impl CheckState { } _ => (), }; - self.sets.insert(name.clone(), set); + self.wf_sets.insert(name.clone(), set); + Ok(()) + } + + 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(()) } } @@ -167,7 +199,8 @@ impl CheckState { // 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 this is fine + // 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))] fn set_equal(&self, set_a: &Set, set_b: &Set) -> bool { set_a == set_b @@ -186,8 +219,10 @@ impl CheckState { self.add_set(name, set) } - Decl::Element { .. } => { - return Err(CheckError::Unimplemented("elements".to_string())); + Decl::Element { name, element, set } => { + let set = self.check_set(set)?; + let element = self.check_element(element, &set)?; + self.add_element(name, element, set) } Decl::Signature { .. } => { return Err(CheckError::Unimplemented("signatures".to_string())); @@ -209,7 +244,7 @@ impl CheckState { Set::Variant(fields) => self.check_variant(fields), Set::ClaimedSet(_) => Err(CheckError::Unimplemented("instances as sets".to_string())), Set::Var(v) => { - if let Some(deref) = self.sets.get(v) { + if let Some(deref) = self.wf_sets.get(v) { Ok(deref.clone()) } else { Err(CheckError::Unbound(v.clone())) @@ -247,4 +282,111 @@ impl CheckState { .collect::<Result<Vec<_>, _>>()?; Ok(Set::Variant(fields)) } + + 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")] + fn check_element(&self, element: &Element, set: &Set) -> Result<Element, CheckError> { + 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) => { + if let Some(CheckedElement { + element: found_element, + set: found_set, + }) = self.wf_elements.get(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, found_set) { + return Err(CheckError::WrongSetForElement( + set.clone(), + found_set.clone(), + )); + } + Ok(found_element.clone()) + } else { + Err(CheckError::Unbound(v.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<String>, Vec<Set>) = 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<String>, 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::<Result<Vec<_>, _>>()?; + // rebuild + let assignations = zip(element_fnames, sub_els) + .map(|(name, element)| ElemAssign { name, element }) + .collect(); + // resign? + Ok(Element::Record(assignations)) + } + Element::Project(_, _) => Err(CheckError::Unimplemented("element project".to_string())), + 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 a76dde4..e389983 100644 --- a/src/main.rs +++ b/src/main.rs @@ -22,8 +22,10 @@ let set Y = X let set Z = record { .y : Y } -// let element x : X = { .b = true, .n = 41, .x = 3.14 } -// +let element x : X = { .b = true, .n = 41 } + +let element z : Z = { .y = x } + // let signature Graph = theory { // .Node :: Set, // .Edge :: (s : Node) (t : Node) -> Set |