diff options
Diffstat (limited to 'src/checker.rs')
| -rw-r--r-- | src/checker.rs | 225 |
1 files changed, 128 insertions, 97 deletions
diff --git a/src/checker.rs b/src/checker.rs index a53a48a..f3221d9 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -1,34 +1,35 @@ use crate::ast::*; -use tracing::{debug, instrument, trace}; +use tracing::{debug, instrument}; use derive_more::Display; use std::collections::HashMap; +use std::fmt; + +impl Programme { + pub fn check(&self) -> Result<(), CheckError> { + let mut state = CheckState::default(); + state.check(self) + } +} #[derive(Display)] pub enum CheckError { #[display("Unbound: {_0}")] Unbound(String), - #[display("Duplicate field: {_0}")] - DuplicateField(String), #[display("Rebinding: {_0}")] Rebinding(String), #[display("The following functionality is unimplemented: {_0}")] Unimplemented(String), } -#[derive(Debug)] +#[derive(Debug, Display)] +#[display("{set} @ {belongs_to}")] struct SetRef { set: Set, - belongs_to: String, + belongs_to: Set, } -#[derive(Debug)] -struct ElRef { - set: Set, - belongs_to: String, -} - -#[derive(Debug, Default)] +#[derive(Default)] struct CheckState { sets: HashMap<String, Set>, elements: HashMap<String, Element>, @@ -38,51 +39,72 @@ struct CheckState { instances: HashMap<String, Instance>, } -impl CheckState { - #[instrument(skip(self), level = "debug")] - fn assert_unbound_set(&self, name: &String) -> Result<(), CheckError> { - if self.sets.contains_key(name) { - Err(CheckError::Rebinding(name.clone())) - } else { - Ok(()) +impl fmt::Display for CheckState { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + fn section<K, V>(f: &mut fmt::Formatter<'_>, name: &str, map: &HashMap<K, V>) -> 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, "}},") } - } - #[instrument(skip(self), level = "debug")] - fn assert_unbound_record_field(&self, name: &String) -> Result<(), CheckError> { - if self.record_fields.contains_key(name) { - Err(CheckError::Rebinding(name.clone())) - } else { - Ok(()) - } + write!(f, "CheckState {{")?; + section(f, "sets", &self.sets)?; + section(f, "elements", &self.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)?; + write!(f, " }}")?; + Ok(()) } +} +impl CheckState { #[instrument(skip(self), level = "debug")] - fn assert_unbound_variant_field(&self, name: &String) -> Result<(), CheckError> { - if self.variant_fields.contains_key(name) { + fn assert_unbound_set(&self, name: &String) -> Result<(), CheckError> { + if self.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.elements.contains_key(name) { + #[instrument(skip(self), level = "debug", fields(%name, %set_ref, %belongs_to))] + fn assert_correct_owner( + &self, + name: &String, + set_ref: &SetRef, + belongs_to: &Set, + ) -> Result<(), CheckError> { + let SetRef { + set: _, + belongs_to: owner, + } = set_ref; + if !self.set_equal(owner, belongs_to) { Err(CheckError::Rebinding(name.clone())) } else { Ok(()) } } - #[instrument(skip(self), level = "debug")] + #[instrument(skip(self), level = "debug", fields(%name, %set, %belongs_to))] fn add_record_field( &mut self, name: &String, set: &Set, - belongs_to: &String, + belongs_to: &Set, ) -> Result<(), CheckError> { - self.assert_unbound_record_field(name)?; + if let Some(set_ref) = self.record_fields.get(name) { + self.assert_correct_owner(name, set_ref, belongs_to)?; + }; self.record_fields.insert( name.clone(), SetRef { @@ -93,14 +115,16 @@ impl CheckState { Ok(()) } - #[instrument(skip(self), level = "debug")] + #[instrument(skip(self), level = "debug", fields(%name, %set, %belongs_to))] fn add_variant_field( &mut self, name: &String, set: &Set, - belongs_to: &String, + belongs_to: &Set, ) -> Result<(), CheckError> { - self.assert_unbound_variant_field(name)?; + if let Some(set_ref) = self.variant_fields.get(name) { + self.assert_correct_owner(name, set_ref, belongs_to)?; + }; self.variant_fields.insert( name.clone(), SetRef { @@ -111,82 +135,82 @@ impl CheckState { Ok(()) } - #[instrument(skip(self), level = "debug")] - fn add_set(&mut self, name: &String, set: &Set) -> Result<(), CheckError> { + #[instrument(skip(self), level = "debug", fields(%name, %set))] + fn add_set(&mut self, name: &String, set: Set) -> Result<(), CheckError> { self.assert_unbound_set(name)?; - match set { + match &set { Set::Record(fields) => { - for RecordField { name: rfn, set } in fields { - self.add_record_field(rfn, set, name)?; + for RecordField { + name: rfn, + set: rset, + } in fields + { + self.add_record_field(rfn, rset, &set)?; } } Set::Variant(fields) => { - for VariantField { name: vfn, set } in fields { - self.add_variant_field(vfn, set, name)?; + for VariantField { + name: vfn, + set: vset, + } in fields + { + self.add_variant_field(vfn, vset, &set)?; } } _ => (), }; - self.sets.insert(name.clone(), set.clone()); - Ok(()) - } - - #[instrument(skip(self), level = "debug")] - fn add_element(&mut self, name: &String, element: &Element) -> Result<(), CheckError> { - self.assert_unbound_element(name)?; - self.elements.insert(name.clone(), element.clone()); + self.sets.insert(name.clone(), set); 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 this is fine + #[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 + } + #[instrument(skip(self, prog), level = "debug")] pub fn check(&mut self, prog: &Programme) -> Result<(), CheckError> { let Programme(decls) = prog; for decl in decls { - debug!(%decl, "checking declaration"); + debug!(%self); + debug!(%decl); match decl { Decl::Set { name, set } => { - self.assert_unbound_set(name)?; - self.check_set(set)?; - // One catch, prohibit "let .. X = X" - if let Set::Var(v) = set - && v == name - { - return Err(CheckError::Rebinding(v.clone())); - }; + let set = self.check_set(set)?; self.add_set(name, set) } - Decl::Element { name, set, element } => { - self.check_element(name, set, element)?; - // TODO: don't drop the set? - self.add_element(name, element) + Decl::Element { .. } => { + return Err(CheckError::Unimplemented("elements".to_string())); + } + Decl::Signature { .. } => { + return Err(CheckError::Unimplemented("signatures".to_string())); + } + Decl::Instance { .. } => { + return Err(CheckError::Unimplemented("instances".to_string())); } - Decl::Signature { name, signature } => Ok(()), - Decl::Instance { - name, - signature, - instance, - } => Ok(()), }?; } + debug!(%self, "END"); Ok(()) } #[instrument(skip(self), level = "debug")] - fn check_set(&self, set: &Set) -> Result<(), CheckError> { + fn check_set(&self, set: &Set) -> Result<Set, CheckError> { match set { - Set::BuiltIn(_) => Ok(()), + Set::BuiltIn(_) => Ok(set.clone()), Set::Record(fields) => self.check_record(fields), - Set::Variant(fields) => Err(CheckError::Unimplemented("variants".to_string())), - Set::ClaimedSet(instance) => { - Err(CheckError::Unimplemented("instances as sets".to_string())) - } + Set::Variant(fields) => self.check_variant(fields), + Set::ClaimedSet(_) => Err(CheckError::Unimplemented("instances as sets".to_string())), Set::Var(v) => { - if self.sets.contains_key(v) { - Ok(()) + if let Some(deref) = self.sets.get(v) { + Ok(deref.clone()) } else { Err(CheckError::Unbound(v.clone())) } @@ -195,25 +219,32 @@ impl CheckState { } #[instrument(skip(self), level = "debug")] - fn check_record(&self, fields: &Vec<RecordField>) -> Result<(), CheckError> { - for RecordField { name, set } in fields { - self.assert_unbound_record_field(name)?; - self.check_set(set)?; - } - Ok(()) + fn check_record(&self, fields: &Vec<RecordField>) -> Result<Set, CheckError> { + let fields = fields + .iter() + .map(|RecordField { name, set }| { + let set = self.check_set(set)?; + Ok(RecordField { + name: name.clone(), + set, + }) + }) + .collect::<Result<Vec<_>, _>>()?; + Ok(Set::Record(fields)) } #[instrument(skip(self), level = "debug")] - fn check_element(&self, name: &String, set: &Set, element: &Element) -> Result<(), CheckError> { - self.assert_unbound_element(name)?; - self.check_set(set)?; - Ok(()) - } -} - -impl Programme { - pub fn check(&self) -> Result<(), CheckError> { - let mut state = CheckState::default(); - state.check(self) + fn check_variant(&self, fields: &Vec<VariantField>) -> Result<Set, CheckError> { + let fields = fields + .iter() + .map(|VariantField { name, set }| { + let set = self.check_set(set)?; + Ok(VariantField { + name: name.clone(), + set, + }) + }) + .collect::<Result<Vec<_>, _>>()?; + Ok(Set::Variant(fields)) } } |