diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.rs | 172 | ||||
| -rw-r--r-- | src/checker.rs | 216 | ||||
| -rw-r--r-- | src/main.rs | 40 | ||||
| -rw-r--r-- | src/parser.rs | 190 |
4 files changed, 435 insertions, 183 deletions
diff --git a/src/ast.rs b/src/ast.rs new file mode 100644 index 0000000..0590556 --- /dev/null +++ b/src/ast.rs @@ -0,0 +1,172 @@ +use derive_more::Display; + +// Set layer + +#[derive(Clone, Debug, PartialEq, Display)] +pub enum BuiltIn { + Nat, + Int, + Float, + Str, + Bool, +} + +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{name} : {set}")] +pub struct RecordField { + pub name: String, + pub set: Set, +} + +#[derive(Clone, Debug, PartialEq, Display)] +#[display("{name}. : {set}")] +pub struct VariantField { + pub name: String, + pub set: Set, +} + +#[derive(Clone, Debug, PartialEq, Display)] +pub enum Set { + #[display("{_0}")] + BuiltIn(BuiltIn), + #[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))] + Record(Vec<RecordField>), + #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))] + Variant(Vec<VariantField>), + #[display("set({_0})")] + ClaimedSet(Instance), + #[display("{_0}")] + Var(String), +} + +// Signature layer + +#[derive(Clone, Debug, PartialEq, Display)] +#[display("({name} : {set})")] +pub struct Param { + pub name: String, + pub set: Set, +} + +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{name} :: {signature}")] +pub struct SigField { + pub name: String, + pub signature: Signature, +} + +#[derive(Clone, Debug, PartialEq, Display)] +pub enum Signature { + #[display("Set")] + Set, + #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))] + Theory(Vec<SigField>), + #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(", "), codomain)] + Ext { + params: Vec<Param>, + codomain: Box<Signature>, + }, + #[display("{_0}")] + Var(String), +} + +// Element layer + +#[derive(Clone, Debug, PartialEq, Display)] +pub enum Literal { + Nat(u64), + Int(i64), + Float(f64), + Str(String), + Bool(bool), +} + +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{name} = {element}")] +pub struct ElemAssign { + pub name: String, + pub element: Element, +} + +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{tag} {bound} => {body}")] +pub struct CaseArm { + pub tag: String, + pub bound: String, + pub body: Element, +} + +#[derive(Clone, Debug, PartialEq, Display)] +pub enum Element { + #[display("{_0}")] + Literal(Literal), + #[display("{_0}")] + Var(String), + #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))] + Record(Vec<ElemAssign>), + #[display("{_0} .{_1}")] + Project(Box<Element>, String), + #[display("{_0}. {_1}")] + Inject(String, Box<Element>), + #[display("{_0} {_1}")] + App(Box<Element>, Box<Element>), + #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))] + Case { + scrutinee: Box<Element>, + arms: Vec<CaseArm>, + }, +} + +// Instance layer + +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{name} = {instance}")] +pub struct InstAssign { + pub name: String, + pub instance: Instance, +} + +#[derive(Clone, Debug, PartialEq, Display)] +pub enum Instance { + #[display("({_0} :: Set)")] + SetCoerce(Box<Set>), + #[display("{_0}")] + Var(String), + #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(", "))] + Record(Vec<InstAssign>), + #[display("for {}, {body}", params.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(""))] + For { + params: Vec<Param>, + body: Box<Instance>, + }, + #[display("{_0} {_1}")] + App(Box<Instance>, Box<Element>), + #[display("{_0} .{_1}")] + Project(Box<Instance>, String), +} + +// Declarations + +#[derive(Clone, Debug, PartialEq, Display)] +pub enum Decl { + #[display("let set {name} = {set}")] + Set { name: String, set: Set }, + #[display("let element {name} : {set} = {element}")] + Element { + name: String, + set: Set, + element: Element, + }, + #[display("let signature {name} = {signature}")] + Signature { name: String, signature: Signature }, + #[display("let instance {name} :: {signature} = {instance}")] + Instance { + name: String, + signature: Signature, + instance: Instance, + }, +} + +#[derive(Display)] +#[display("{}", _0.iter().map(|d| d.to_string()).collect::<Vec<_>>().join("\n"))] +pub struct Programme(pub Vec<Decl>); diff --git a/src/checker.rs b/src/checker.rs index ea099ab..a53a48a 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -1,7 +1,219 @@ -use crate::parser::*; +use crate::ast::*; +use tracing::{debug, instrument, trace}; +use derive_more::Display; +use std::collections::HashMap; + +#[derive(Display)] pub enum CheckError { + #[display("Unbound: {_0}")] Unbound(String), + #[display("Duplicate field: {_0}")] DuplicateField(String), - ExpectedTypeFoundTerm(String), + #[display("Rebinding: {_0}")] + Rebinding(String), + #[display("The following functionality is unimplemented: {_0}")] + Unimplemented(String), +} + +#[derive(Debug)] +struct SetRef { + set: Set, + belongs_to: String, +} + +#[derive(Debug)] +struct ElRef { + set: Set, + belongs_to: String, +} + +#[derive(Debug, 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>, +} + +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(()) + } + } + + #[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(()) + } + } + + #[instrument(skip(self), level = "debug")] + fn assert_unbound_variant_field(&self, name: &String) -> Result<(), CheckError> { + if self.variant_fields.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) { + Err(CheckError::Rebinding(name.clone())) + } else { + Ok(()) + } + } + + #[instrument(skip(self), level = "debug")] + fn add_record_field( + &mut self, + name: &String, + set: &Set, + belongs_to: &String, + ) -> Result<(), CheckError> { + self.assert_unbound_record_field(name)?; + self.record_fields.insert( + name.clone(), + SetRef { + set: set.clone(), + belongs_to: belongs_to.clone(), + }, + ); + Ok(()) + } + + #[instrument(skip(self), level = "debug")] + fn add_variant_field( + &mut self, + name: &String, + set: &Set, + belongs_to: &String, + ) -> Result<(), CheckError> { + self.assert_unbound_variant_field(name)?; + self.variant_fields.insert( + name.clone(), + SetRef { + set: set.clone(), + belongs_to: belongs_to.clone(), + }, + ); + Ok(()) + } + + #[instrument(skip(self), level = "debug")] + 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 } in fields { + self.add_record_field(rfn, set, name)?; + } + } + Set::Variant(fields) => { + for VariantField { name: vfn, set } in fields { + self.add_variant_field(vfn, set, name)?; + } + } + _ => (), + }; + 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()); + Ok(()) + } +} + +impl CheckState { + #[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"); + 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())); + }; + 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::Signature { name, signature } => Ok(()), + Decl::Instance { + name, + signature, + instance, + } => Ok(()), + }?; + } + Ok(()) + } + + #[instrument(skip(self), level = "debug")] + fn check_set(&self, set: &Set) -> Result<(), CheckError> { + match set { + Set::BuiltIn(_) => Ok(()), + 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::Var(v) => { + if self.sets.contains_key(v) { + Ok(()) + } else { + Err(CheckError::Unbound(v.clone())) + } + } + } + } + + #[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(()) + } + + #[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) + } } diff --git a/src/main.rs b/src/main.rs index 56e14c5..11357a9 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,6 +1,44 @@ +mod ast; mod checker; mod parser; +use tracing_subscriber::{layer::SubscriberExt, util::SubscriberInitExt}; +use tracing_tree::HierarchicalLayer; + fn main() { - println!("Hello, world!"); + tracing_subscriber::registry() + .with( + HierarchicalLayer::new(2) + .with_targets(false) + .with_bracketed_fields(true), + ) + .init(); + + let src = r#" + +let set X = record { .b : Bool, .n : Nat } + +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); + + assert!(programme.is_ok()); + let programme = programme.unwrap(); + println!("Parsed:\n```\n{}\n```\n", programme); + + if let Err(e) = programme.check() { + println!("{}", e); + } } diff --git a/src/parser.rs b/src/parser.rs index a0da79c..f98673e 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -1,176 +1,6 @@ -use derive_more::Display; use peg::parser; -// Set layer - -#[derive(Clone, Debug, PartialEq, Display)] -pub enum BuiltIn { - Nat, - Int, - Float, - Str, - Bool, -} - -#[derive(Clone, Debug, PartialEq, Display)] -#[display(".{name} : {set}")] -pub struct SetField { - pub name: String, - pub set: Set, -} - -#[derive(Clone, Debug, PartialEq, Display)] -#[display("{name}. : {set}")] -pub struct VariantField { - pub name: String, - pub set: Set, -} - -#[derive(Clone, Debug, PartialEq, Display)] -pub enum Set { - #[display("{_0}")] - BuiltIn(BuiltIn), - #[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))] - Record(Vec<SetField>), - #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))] - Variant(Vec<VariantField>), - #[display("set({_0})")] - ClaimedSet(Instance), - #[display("{_0}")] - Var(String), -} - -// Signature layer - -#[derive(Clone, Debug, PartialEq, Display)] -#[display("({name} : {set})")] -pub struct Param { - pub name: String, - pub set: Set, -} - -#[derive(Clone, Debug, PartialEq, Display)] -#[display(".{name} :: {signature}")] -pub struct SigField { - pub name: String, - pub signature: Signature, -} - -#[derive(Clone, Debug, PartialEq, Display)] -pub enum Signature { - #[display("Set")] - Set, - #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))] - Theory(Vec<SigField>), - #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(", "), codomain)] - Ext { - params: Vec<Param>, - codomain: Box<Signature>, - }, - #[display("{_0}")] - Var(String), -} - -// Element layer - -#[derive(Clone, Debug, PartialEq, Display)] -pub enum Literal { - Nat(u64), - Int(i64), - Float(f64), - Str(String), - Bool(bool), -} - -#[derive(Clone, Debug, PartialEq, Display)] -#[display(".{name} = {element}")] -pub struct ElemAssign { - pub name: String, - pub element: Element, -} - -#[derive(Clone, Debug, PartialEq, Display)] -#[display(".{tag} {bound} => {body}")] -pub struct CaseArm { - pub tag: String, - pub bound: String, - pub body: Element, -} - -#[derive(Clone, Debug, PartialEq, Display)] -pub enum Element { - #[display("{_0}")] - Literal(Literal), - #[display("{_0}")] - Var(String), - #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))] - Record(Vec<ElemAssign>), - #[display("{_0} .{_1}")] - Project(Box<Element>, String), - #[display("{_0}. {_1}")] - Inject(String, Box<Element>), - #[display("{_0} {_1}")] - App(Box<Element>, Box<Element>), - #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))] - Case { - scrutinee: Box<Element>, - arms: Vec<CaseArm>, - }, -} - -// Instance layer - -#[derive(Clone, Debug, PartialEq, Display)] -#[display(".{name} = {instance}")] -pub struct InstAssign { - pub name: String, - pub instance: Instance, -} - -#[derive(Clone, Debug, PartialEq, Display)] -pub enum Instance { - #[display("{_0}")] - SetCoerce(Box<Set>), - #[display("{_0}")] - Var(String), - #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(", "))] - Record(Vec<InstAssign>), - #[display("for {}, {body}", params.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(""))] - For { - params: Vec<Param>, - body: Box<Instance>, - }, - #[display("{_0} {_1}")] - App(Box<Instance>, Box<Element>), - #[display("{_0} .{_1}")] - Project(Box<Instance>, String), -} - -// Declarations - -#[derive(Clone, Debug, PartialEq, Display)] -pub enum Decl { - #[display("let set {name} = {set}")] - Set { name: String, set: Set }, - #[display("let element {name} : {set} = {element}")] - Element { - name: String, - set: Set, - element: Element, - }, - #[display("let signature {name} = {signature}")] - Signature { name: String, signature: Signature }, - #[display("let instance {name} :: {signature} = {instance}")] - Instance { - name: String, - signature: Signature, - instance: Instance, - }, -} - -#[derive(Display)] -#[display("{}", _0.iter().map(|d| d.to_string()).collect::<Vec<_>>().join("\n"))] -pub struct Programme(Vec<Decl>); +use crate::ast::*; parser! { pub grammar parser() for str { @@ -272,8 +102,8 @@ parser! { // set layer - rule set_field() -> SetField - = n:project_lower() _ ":" _ s:set() { SetField { name: n, set: s } } + rule set_field() -> RecordField + = n:project_lower() _ ":" _ s:set() { RecordField { name: n, set: s } } rule variant_field() -> VariantField = n:inject_lower() _ ":" _ s:set() _ { VariantField { name: n, set: s } } @@ -281,7 +111,7 @@ parser! { rule claimed_set() -> Instance = kw_set() "(" _ i:instance() _ ")" { i } - pub rule set() -> Set + rule set() -> Set = kw_record() _ "{" fs:(set_field() ** ",") _ "}" { Set::Record(fs) } / kw_variant() _ "{" _ vs:(variant_field() ** "|") "}" { Set::Variant(vs) } / b:builtin() { Set::BuiltIn(b) } @@ -299,7 +129,7 @@ parser! { rule sig_field() -> SigField = n:project_upper() _ "::" _ s:signature() { SigField { name: n, signature: s } } - pub rule signature() -> Signature + rule signature() -> Signature = kw_Set() { Signature::Set } / kw_theory() _ "{" fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } / ps:param_list() _ "->" _ cod:signature() { Signature::Ext { params: ps, codomain: Box::new(cod) } } @@ -339,7 +169,7 @@ parser! { rule case_arm() -> CaseArm = t:inject() _ x:elem_var() _ "=>" _ body:element() { CaseArm { tag: t, bound: x, body } } - pub rule element() -> Element + rule element() -> Element = kw_case() __ scrut:element() _ kw_of() _ "{" arms:(_ a:case_arm() _ { a }) ** "|" _ "}" { Element::Case { scrutinee: Box::new(scrut), arms } } / app_elem() @@ -371,7 +201,7 @@ parser! { }) } - pub rule instance() -> Instance + rule instance() -> Instance = kw_for() __ ps:param_list() _ "," _ body:instance() { Instance::For { params: ps, body: Box::new(body) } } / app_inst() @@ -451,12 +281,12 @@ let set Maybe = variant { .Edge :: (s : Node) (t : Node) -> Set } - let instance loop :: Graph = { + let instance natPoset :: Graph = { .Node = Nat, - .Edge = for (s : Nat) (t : Nat), Nat + .Edge = for (s : Nat) (t : Nat), Bool } - let element node : set(loop .Node) = 7 + let element node : set(natPoset .Node) = 7 "#; debug_parse(src); |