diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/checker.rs | 225 | ||||
| -rw-r--r-- | src/main.rs | 28 | ||||
| -rw-r--r-- | src/parser.rs | 11 |
3 files changed, 153 insertions, 111 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)) } } diff --git a/src/main.rs b/src/main.rs index 11357a9..a76dde4 100644 --- a/src/main.rs +++ b/src/main.rs @@ -16,21 +16,25 @@ fn main() { let src = r#" -let set X = record { .b : Bool, .n : Nat } +let set X = record { .b : Bool, .n : Nat } // basic -let element x : X = { .b = true, .n = 41, .x = 3.14 } +let set Y = X -let signature Graph = theory { - .Node :: Set, - .Edge :: (s : Node) (t : Node) -> Set -} - -let instance natPoset :: Graph = { - .Node = Nat, - .Edge = for (s : Nat) (t : Nat), Bool -} +let set Z = record { .y : Y } -let element node : set(natPoset .Node) = 7 +// let element x : X = { .b = true, .n = 41, .x = 3.14 } +// +// let signature Graph = theory { +// .Node :: Set, +// .Edge :: (s : Node) (t : Node) -> Set +// } +// +// let instance natPoset :: Graph = { +// .Node = Nat, +// .Edge = for (s : Nat) (t : Nat), Bool +// } +// +// let element node : set(natPoset .Node) = 7 "#; let programme = parser::parser::program(src); diff --git a/src/parser.rs b/src/parser.rs index f98673e..7fa4241 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -4,10 +4,17 @@ use crate::ast::*; parser! { pub grammar parser() for str { + + // comment + + rule comment() = quiet!{ "//" [^'\n' |'\r']* ['\n' | '\r'] } + // whitespace - rule _() = quiet!{ [' ' | '\t' | '\n' | '\r']* } - rule __() = quiet!{ [' ' | '\t' | '\n' | '\r']+ } + rule ws_char() = [' ' | '\t' | '\n' | '\r'] + rule skip() = ws_char() / comment() + rule _() = quiet!{ skip()* } + rule __() = quiet!{ skip()+ } rule ident_tail() = ['a'..='z' | 'A'..='Z' | '0'..='9' | '_' | '\''] rule wb() = !ident_tail() |