diff options
Diffstat (limited to 'src/parser.rs')
| -rw-r--r-- | src/parser.rs | 328 |
1 files changed, 145 insertions, 183 deletions
diff --git a/src/parser.rs b/src/parser.rs index d95c190..6e4a09d 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -3,23 +3,25 @@ use peg::parser; use crate::ast::*; parser! { - pub grammar parser() for str { + grammar parser() for str { - // comment + // ==================================================================== + // Whitespace and comments + // ==================================================================== - rule comment() = quiet!{ "//" [^'\n' |'\r']* ['\n' | '\r'] } - - // whitespace + rule comment() = quiet!{ "//" [^'\n' | '\r']* (['\n' | '\r'] / ![_]) } rule ws_char() = [' ' | '\t' | '\n' | '\r'] - rule skip() = ws_char() / comment() - rule _() = quiet!{ skip()* } - rule __() = quiet!{ skip()+ } + rule skip() = ws_char() / comment() + rule _() = quiet!{ skip()* } + rule __() = quiet!{ skip()+ } rule ident_tail() = ['a'..='z' | 'A'..='Z' | '0'..='9' | '_' | '\''] rule wb() = !ident_tail() - // keywords + // ==================================================================== + // Keywords + // ==================================================================== rule kw_let_set() = "let set" wb() rule kw_let_element() = "let element" wb() @@ -39,194 +41,226 @@ parser! { rule kw_Float() = "Float" wb() rule kw_Str() = "Str" wb() rule kw_Bool() = "Bool" wb() + rule kw_true() = "true" wb() + rule kw_false() = "false" wb() rule keyword() = - kw_let_set() / kw_let_element() / kw_let_signature() / 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() + kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance() + / kw_record() / kw_variant() / kw_theory() + / kw_case() / kw_of() / kw_for() + / kw_Set() / kw_set_of() / kw_set() + / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() + / kw_true() / kw_false() - // identifiers + // ==================================================================== + // Identifiers + // ==================================================================== rule lower_ident() -> String - = !keyword() s:$(['a'..='z'] ident_tail()*) { s.to_string() } + = !keyword() s:$(['a'..='z'] ident_tail()*) { s.to_string() } rule upper_ident() -> String - = !keyword() s:$(['A'..='Z'] ident_tail()*) { s.to_string() } + = !keyword() s:$(['A'..='Z'] ident_tail()*) { s.to_string() } + + rule any_ident() -> String + = !keyword() s:$(['a'..='z' | '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 + // ==================================================================== + // Projections (.field) and injections (tag.) -- chain forms + // ==================================================================== rule project() -> String - = __ "." n:$(['a'..='z' | 'A'..='Z'] ident_tail()*) { n.to_string() } + = __ "." n:any_ident() { n } 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() } + = _ !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) "." __ + { s.to_string() } - rule inject_lower() -> String - = _ n:$(['a'..='z'] ident_tail()*) "." __ { n.to_string() } + // ==================================================================== + // Record-field labels + // ==================================================================== - rule project_upper() -> String - = __ "." n:$(['A'..='Z'] ident_tail()*) { n.to_string() } + rule field_lower() -> String = "." n:lower_ident() { n } + rule field_upper() -> String = "." n:upper_ident() { n } - - // literals + // ==================================================================== + // Literals and built-in sets + // ==================================================================== rule nat_lit() -> Literal - = n:$(['0'..='9']+) !"." { Literal::Nat(n.parse().unwrap()) } + = n:$(['0'..='9']+) !"." { Literal::Nat(n.parse().unwrap()) } rule int_lit() -> Literal - = "-" n:$(['0'..='9']+) !"." { Literal::Int(-(n.parse::<i64>().unwrap())) } + = "-" n:$(['0'..='9']+) !"." { Literal::Int(-(n.parse::<i64>().unwrap())) } rule float_lit() -> Literal - = s:$("-"? ['0'..='9']+ "." ['0'..='9']+) { Literal::Float(s.parse().unwrap()) } + = s:$("-"? ['0'..='9']+ "." ['0'..='9']+) { Literal::Float(s.parse().unwrap()) } rule str_lit() -> Literal - = "\"" s:$((!"\"" [_])*) "\"" { Literal::Str(s.to_string()) } + = "\"" s:$((!"\"" [_])*) "\"" { Literal::Str(s.to_string()) } rule bool_lit() -> Literal - = "true" { Literal::Bool(true) } / "false" { Literal::Bool(false) } + = kw_true() { Literal::Bool(true) } + / kw_false() { Literal::Bool(false) } rule literal() -> Literal - = float_lit() / int_lit() / nat_lit() / str_lit() / bool_lit() - - // built-in + = float_lit() / int_lit() / nat_lit() / str_lit() / bool_lit() rule builtin() -> BuiltIn - = kw_Nat() { BuiltIn::Nat } - / kw_Int() { BuiltIn::Int } - / kw_Float() { BuiltIn::Float } - / kw_Str() { BuiltIn::Str } - / kw_Bool() { BuiltIn::Bool } + = kw_Nat() { BuiltIn::Nat } + / kw_Int() { BuiltIn::Int } + / kw_Float() { BuiltIn::Float } + / kw_Str() { BuiltIn::Str } + / kw_Bool() { BuiltIn::Bool } - // set layer + // ==================================================================== + // Sets + // ==================================================================== rule set_field() -> RecordField - = _ n:lower_ident() _ ":" _ s:set() { RecordField { name: n, set: s } } + = _ n:lower_ident() _ ":" _ s:set() _ + { RecordField { name: n, set: s } } rule variant_field() -> VariantField - = _ n:lower_ident() _ ":" _ s:set() _ { VariantField { name: n, set: s } } + = _ n:lower_ident() _ ":" _ s:set() _ + { VariantField { name: n, set: s } } rule claimed_set() -> Instance - = kw_set_of() "(" _ i:instance() _ ")" { i } + = kw_set_of() _ "(" _ i:instance() _ ")" { i } 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 } + = 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 + // ==================================================================== + // Signatures + // ==================================================================== rule param() -> Param - = "(" _ n:elem_var() _ ":" _ s:set() _ ")" { Param { name: n, set: s } } + = "(" _ n:elem_var() _ ":" _ s:set() _ ")" { Param { name: n, set: s } } rule param_list() -> Vec<Param> = param() ++ _ rule sig_field() -> SigField - = _ n:upper_ident() _ "::" _ s:signature() { SigField { name: n, signature: s } } + = _ n:upper_ident() _ "::" _ s:signature() _ + { SigField { name: n, signature: s } } 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 } + = 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 + // ==================================================================== + // Elements + // ==================================================================== rule elem_assign() -> ElemAssign - = n:project() _ "=" _ e:element() { ElemAssign { name: n, element: e } } + = _ n:field_lower() _ "=" _ 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 } + = l:literal() { Element::Literal(l) } + / "{" _ fs:(elem_assign() ** ",") _ "}" { Element::Record(fs) } + / "(" _ e:element() _ ")" { e } + / v:elem_var() { Element::Var(v) } 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{element: Box::new(acc), field: p}} - ); - tags.into_iter().rev().fold(base, |acc, t| { - Element::Inject{field: t, element: Box::new(acc)} - }) - } + = tags:(t:inject() _ { t })* head:atom_elem() projs:(p:project() { p })* + { + let base = projs.into_iter().fold(head, |acc, p| { + Element::Project { element: Box::new(acc), field: p } + }); + tags.into_iter().rev().fold(base, |acc, t| { + Element::Inject { field: t, element: Box::new(acc) } + }) + } rule case_arm() -> CaseArm - = t:inject() _ x:elem_var() _ "=>" _ body:element() { CaseArm { tag: t, bound: x, body } } + = _ t:inject() _ x:elem_var() _ "=>" _ body:element() _ + { CaseArm { tag: t, bound: x, body } } rule element() -> Element - = kw_case() __ scrut:element() _ kw_of() _ "[" arms:(_ a:case_arm() _ { a }) ** "|" _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } - / d:dot_elem() { d } + = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" + { Element::Case { scrutinee: Box::new(scrut), arms } } + / d:dot_elem() { d } - // instance layer + // ==================================================================== + // Instances + // ==================================================================== rule inst_case_arm() -> InstCaseArm - = t:inject() _ x:elem_var() _ "=>" _ body:instance() { InstCaseArm { tag: t, bound: x, body } } + = _ t:inject() _ x:elem_var() _ "=>" _ body:instance() _ + { InstCaseArm { tag: t, bound: x, body } } rule inst_assign() -> InstAssign - = n:project_upper() _ "=" _ i:instance() - { InstAssign { name: n, instance: i } } + = _ n:field_upper() _ "=" _ i:instance() _ + { InstAssign { name: n, instance: i } } rule explicit_set_coerce() -> Set - = _ s:set() _ "::" _ kw_Set() _ { s } + = s:set() _ "::" _ kw_Set() { s } rule atom_inst() -> Instance - = s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) } - / v:inst_var() { Instance::Var(v) } - / f:sig_var() { Instance::Var(f) } - / "{" fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) } - / "(" _ i:instance() _ ")" { i } + = s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) } + / v:inst_var() { Instance::Var(v) } + / f:sig_var() { Instance::Var(f) } + / "{" _ 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{instance: Box::new(acc), field: p} - }) - } + = head:atom_inst() projs:(p:project() { p })* + { + projs.into_iter().fold(head, |acc, p| { + Instance::Project { instance: Box::new(acc), field: 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)) - }) - } + = head:dot_inst() tail:(__ a:dot_elem() { a })* + { + tail.into_iter().fold(head, |acc, a| { + Instance::App(Box::new(acc), Box::new(a)) + }) + } rule instance() -> Instance - = kw_for() __ ps:param_list() _ "," _ body:instance() { Instance::For { params: ps, body: Box::new(body) } } - / kw_case() __ scrut:element() _ kw_of() _ "[" arms:(_ a:inst_case_arm() _ { a }) ** "|" _ "]" { Instance::Case { scrutinee: Box::new(scrut), arms } } - / app_inst() + = kw_for() _ ps:param_list() _ "," _ body:instance() + { Instance::For { params: ps, body: Box::new(body) } } + / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" + { Instance::Case { scrutinee: Box::new(scrut), arms } } + / app_inst() - // declarations + // ==================================================================== + // Top-level 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_signature() __ 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 } } + = 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_signature() _ 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() -> Programme - = _ ds:(decl() ** _) _ { Programme(ds) } + = _ ds:(decl() ** _) _ { Programme(ds) } } } -pub fn debug_parse(src: &str) -> Programme { +pub fn parse(src: &str) -> Programme { match parser::program(src) { Ok(p) => { println!("{}", p); @@ -246,75 +280,3 @@ pub fn debug_parse(src: &str) -> Programme { } } } - -#[cfg(test)] -mod tests { - use super::*; - - #[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 signature OneSet = theory { F :: Set } - - let signature T = theory { - A :: Set, - B :: (x : set-of({ .F = A } .F)) -> Set, - C :: (x : set-of(A)) (b : set-of(B x)) -> Set - } - - - let signature Graph = theory { - Node :: Set, - Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set - } - - let instance natPoset :: Graph = { - .Node = (Nat :: Set), - .Edge = for (s : Nat) (t : Nat), Bool::Set - } - - let element node : set-of(natPoset .Node) = 7 - - let set NatEdges = record { - source: set-of(natPoset .Node), - target: set-of(natPoset .Node), - connected: set-of(set-of(natPoset .Edge source target) :: Set) - } - "#; - - debug_parse(src); - } -} |