diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/checker.rs | 7 | ||||
| -rw-r--r-- | src/main.rs | 6 | ||||
| -rw-r--r-- | src/parser.rs | 455 |
3 files changed, 468 insertions, 0 deletions
diff --git a/src/checker.rs b/src/checker.rs new file mode 100644 index 0000000..ea099ab --- /dev/null +++ b/src/checker.rs @@ -0,0 +1,7 @@ +use crate::parser::*; + +pub enum CheckError { + Unbound(String), + DuplicateField(String), + ExpectedTypeFoundTerm(String), +} diff --git a/src/main.rs b/src/main.rs new file mode 100644 index 0000000..56e14c5 --- /dev/null +++ b/src/main.rs @@ -0,0 +1,6 @@ +mod checker; +mod parser; + +fn main() { + println!("Hello, world!"); +} diff --git a/src/parser.rs b/src/parser.rs new file mode 100644 index 0000000..1af9d49 --- /dev/null +++ b/src/parser.rs @@ -0,0 +1,455 @@ +use peg::parser; + +// Set layer + +#[derive(Clone, Debug, PartialEq)] +pub enum BuiltIn { + Nat, + Int, + Float, + Str, + Bool, +} + +#[derive(Clone, Debug, PartialEq)] +pub struct SetField { + pub name: String, + pub set: Set, +} // .x : X + +#[derive(Clone, Debug, PartialEq)] +pub struct VariantField { + pub name: String, + pub set: Set, +} // x. : X + +#[derive(Clone, Debug, PartialEq)] +pub enum Set { + BuiltIn(BuiltIn), + Record(Vec<SetField>), + Variant(Vec<VariantField>), + ClaimedSet(Instance), + Var(String), +} + +// Signature layer + +#[derive(Clone, Debug, PartialEq)] +pub struct Param { + pub name: String, + pub set: Set, +} // (x : X) + +#[derive(Clone, Debug, PartialEq)] +pub struct SigField { + pub name: String, + pub signature: Signature, +} // .s :: S + +#[derive(Clone, Debug, PartialEq)] +pub enum Signature { + Set, + Theory(Vec<SigField>), + Ext { + params: Vec<Param>, + codomain: Box<Signature>, + }, // (x:X)(y:Y) -> S + Var(String), +} + +// Element layer + +#[derive(Clone, Debug, PartialEq)] +pub enum Literal { + Nat(u64), + Int(i64), + Float(f64), + Str(String), + Bool(bool), +} + +#[derive(Clone, Debug, PartialEq)] +pub struct ElemAssign { + pub name: String, + pub element: Element, +} // .x = m + +#[derive(Clone, Debug, PartialEq)] +pub struct CaseArm { + pub tag: String, + pub bound: String, + pub body: Element, +} // v. x => n + +#[derive(Clone, Debug, PartialEq)] +pub enum Element { + Literal(Literal), + Var(String), + Record(Vec<ElemAssign>), + Project(Box<Element>, String), // m .x + Inject(String, Box<Element>), // v. m + App(Box<Element>, Box<Element>), // f x + Case { + scrutinee: Box<Element>, + arms: Vec<CaseArm>, + }, +} + +// Instance layer + +#[derive(Clone, Debug, PartialEq)] +pub struct InstAssign { + pub name: String, + pub instance: Instance, +} // .s = I + +#[derive(Clone, Debug, PartialEq)] +pub enum Instance { + SetCoerce(Box<Set>), // X :: Set + Var(String), + Record(Vec<InstAssign>), + For { + params: Vec<Param>, + body: Box<Instance>, + }, // for (x:X), I + App(Box<Instance>, Box<Element>), // I m + Project(Box<Instance>, String), // I .s +} + +// Declarations +#[derive(Clone, Debug, PartialEq)] +pub enum Decl { + Set { + name: String, + set: Set, + }, + Element { + name: String, + set: Set, + element: Element, + }, + Signature { + name: String, + signature: Signature, + }, + Instance { + name: String, + signature: Signature, + instance: Instance, + }, +} + +pub type Program = Vec<Decl>; + +parser! { + pub grammar parser() for str { + // whitespace + + rule _() = quiet!{ [' ' | '\t' | '\n' | '\r']* } + rule __() = quiet!{ [' ' | '\t' | '\n' | '\r']+ } + + rule ident_tail() = ['a'..='z' | 'A'..='Z' | '0'..='9' | '_' | '\''] + rule wb() = !ident_tail() + + // keywords + + rule kw_let_set() = "let set" wb() + rule kw_let_element() = "let element" wb() + rule kw_let_theory() = "let theory" wb() + rule kw_let_instance() = "let instance" wb() + rule kw_record() = "record" wb() + rule kw_variant() = "variant" wb() + rule kw_theory() = "theory" wb() + rule kw_case() = "case" wb() + rule kw_of() = "of" wb() + rule kw_for() = "for" wb() + rule kw_set() = "set" wb() + rule kw_Set() = "Set" wb() + rule kw_Nat() = "Nat" wb() + rule kw_Int() = "Int" wb() + rule kw_Float() = "Float" wb() + rule kw_Str() = "Str" wb() + rule kw_Bool() = "Bool" wb() + + rule keyword() = + kw_let_set() / kw_let_element() / kw_let_theory() / kw_let_instance() + / kw_record() / kw_variant() / kw_theory() + / kw_case() / kw_of() / kw_for() + / kw_Set() / kw_set() + / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() + + // identifiers + + rule lower_ident() -> String + = !keyword() s:$(['a'..='z'] ident_tail()*) { s.to_string() } + + rule upper_ident() -> String + = !keyword() s:$(['A'..='Z'] ident_tail()*) { s.to_string() } + + rule elem_var() -> String = lower_ident() + rule inst_var() -> String = lower_ident() + rule set_var() -> String = upper_ident() + rule sig_var() -> String = upper_ident() + + // projections, injections + // Note: we don't capture the dot + + rule project() -> String + = __ "." n:$(['a'..='z' | 'A'..='Z'] ident_tail()*) { n.to_string() } + + rule inject() -> String + = _ n:$(['a'..='z' | 'A'..='Z'] ident_tail()*) "." __ { n.to_string() } + + rule project_lower() -> String + = __ "." n:$(['a'..='z'] ident_tail()*) { n.to_string() } + + rule inject_lower() -> String + = _ n:$(['a'..='z'] ident_tail()*) "." __ { n.to_string() } + + rule project_upper() -> String + = __ "." n:$(['A'..='Z'] ident_tail()*) { n.to_string() } + + + // literals + + rule nat_lit() -> Literal + = n:$(['0'..='9']+) !"." { Literal::Nat(n.parse().unwrap()) } + + rule int_lit() -> Literal + = "-" n:$(['0'..='9']+) !"." { Literal::Int(-(n.parse::<i64>().unwrap())) } + + rule float_lit() -> Literal + = s:$("-"? ['0'..='9']+ "." ['0'..='9']+) { Literal::Float(s.parse().unwrap()) } + + rule str_lit() -> Literal + = "\"" s:$((!"\"" [_])*) "\"" { Literal::Str(s.to_string()) } + + rule bool_lit() -> Literal + = "true" { Literal::Bool(true) } / "false" { Literal::Bool(false) } + + rule literal() -> Literal + = float_lit() / int_lit() / nat_lit() / str_lit() / bool_lit() + + // built-in + + rule builtin() -> BuiltIn + = kw_Nat() { BuiltIn::Nat } + / kw_Int() { BuiltIn::Int } + / kw_Float() { BuiltIn::Float } + / kw_Str() { BuiltIn::Str } + / kw_Bool() { BuiltIn::Bool } + + // set layer + + rule set_field() -> SetField + = n:project_lower() _ ":" _ s:set() + { SetField { name: n, set: s } } + + rule variant_field() -> VariantField + = n:inject_lower() _ ":" _ s:set() _ + { VariantField { name: n, set: s } } + + rule claimed_set() -> Instance + = kw_set() "(" _ i:instance() _ ")" {i} + + pub rule set() -> Set + = kw_record() _ "{" fs:(set_field() ** ",") _ "}" + { Set::Record(fs) } + / kw_variant() _ "{" _ vs:(variant_field() ** "|") "}" + { Set::Variant(vs) } + / b:builtin() { Set::BuiltIn(b) } + / i:claimed_set() { Set::ClaimedSet(i) } + / v:set_var() { Set::Var(v) } + / "(" _ s:set() _ ")" { s } + // signature layer + + rule param() -> Param + = "(" _ n:elem_var() _ ":" _ s:set() _ ")" + { Param { name: n, set: s } } + + rule param_list() -> Vec<Param> = param() ++ _ + + rule sig_field() -> SigField + = n:project_upper() _ "::" _ s:signature() + { SigField { name: n, signature: s } } + + pub 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) } } + / v:sig_var() { Signature::Var(v) } + / "(" _ s:signature() _ ")" { s } + + // element layer + + rule elem_assign() -> ElemAssign + = n:project() _ "=" _ e:element() + { ElemAssign { name: n, element: e } } + + rule atom_elem() -> Element + = l:literal() { Element::Literal(l) } + / v:elem_var() { Element::Var(v) } + / "{" fs:(elem_assign() ** ",") _ ","? _ "}" + { Element::Record(fs) } + / "(" _ e:element() _ ")" { e } + + rule dot_elem() -> Element + = tags:(t:inject() _ { t })* + head:atom_elem() + projs:(p:project() { p })* + { + let base = projs.into_iter().fold(head, |acc, p| { + Element::Project(Box::new(acc), p) + }); + tags.into_iter().rev().fold(base, |acc, t| { + Element::Inject(t, Box::new(acc)) + }) + } + + rule app_elem() -> Element + = head:dot_elem() tail:(__ d:dot_elem() { d })* + { + tail.into_iter().fold(head, |acc, a| { + Element::App(Box::new(acc), Box::new(a)) + }) + } + + rule case_arm() -> CaseArm + = t:inject() _ x:elem_var() _ "=>" _ body:element() + { CaseArm { tag: t, bound: x, body } } + + pub rule element() -> Element + = kw_case() __ scrut:element() _ kw_of() _ "{" + arms:(_ a:case_arm() _ { a }) ** "|" + _ "|"? + _ "}" + { Element::Case { scrutinee: Box::new(scrut), arms } } + / app_elem() + + // instance layer + + rule inst_assign() -> InstAssign + = n:project() _ "=" _ i:instance() + { InstAssign { name: n, instance: i } } + + rule atom_inst() -> Instance + = s:set() { Instance::SetCoerce(Box::new(s)) } + / v:inst_var() { Instance::Var(v) } + / "{" fs:(inst_assign() ** ",") _ ","? _ "}" + { Instance::Record(fs) } + / "(" _ i:instance() _ ")" { i } + + rule dot_inst() -> Instance + = head:atom_inst() projs:(p:project() { p })* + { + projs.into_iter().fold(head, |acc, p| { + Instance::Project(Box::new(acc), p) + }) + } + + rule app_inst() -> Instance + = head:dot_inst() tail:(__ a:dot_elem() { a })* + { + tail.into_iter().fold(head, |acc, a| { + Instance::App(Box::new(acc), Box::new(a)) + }) + } + + pub rule instance() -> Instance + = kw_for() __ ps:param_list() _ "," _ body:instance() + { Instance::For { params: ps, body: Box::new(body) } } + / app_inst() + + // declarations + + rule decl() -> Decl + = kw_let_set() __ n:set_var() _ "=" _ s:set() + { Decl::Set { name: n, set: s } } + / kw_let_element() __ n:elem_var() _ ":" _ s:set() _ "=" _ e:element() + { Decl::Element { name: n, set: s, element: e } } + / kw_let_theory() __ n:sig_var() _ "=" _ sg:signature() + { Decl::Signature { name: n, signature: sg } } + / kw_let_instance() __ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance() + { Decl::Instance { name: n, signature: sg, instance: i } } + + pub rule program() -> Program + = _ ds:(decl() ** _) _ { ds } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn debug_parse(src: &str) { + match parser::program(src) { + Ok(p) => println!("```{}\n```\n=> {:?}\n", src, p), + Err(e) => { + let line = e.location.line; + let col = e.location.column; + let off = e.location.offset; + println!("FAIL at {}:{} (offset {})", line, col, off); + println!("expected: {:#}", e.expected); + + let before = &src[off.saturating_sub(40)..off]; + let after = &src[off..(off + 40).min(src.len())]; + println!("...{}⟨HERE⟩{}...", before, after); + panic!("Parse failed!"); + } + } + } + + #[test] + fn test_sets() { + let src = r#" +let set Config = record { + .enabled : Bool, + .count : Nat, + .offset : Int, + .scale : Float, + .label : Str +} + +let set Maybe = variant { + none. : record {} + | some. : Config +} + "#; + + debug_parse(src); + } + + #[test] + fn test_elements() { + let src = r#" + let element foo : Nat = + case some. config .count of { + none. ignore => 0 + | some. n => n + } + "#; + + debug_parse(src); + } + + #[test] + fn test_theories_and_instances() { + let src = r#" + let theory Graph = theory { + .Node :: Set, + .Edge :: (s : Node) (t : Node) -> Set, + } + + let instance loop :: Graph = { + .Node = Nat, + .Edge = for (s : Nat) (t : Nat), Nat + } + + let element node : set(loop .Node) = 7 + "#; + + debug_parse(src); + } +} |