diff options
| -rw-r--r-- | Cargo.lock | 71 | ||||
| -rw-r--r-- | Cargo.toml | 1 | ||||
| -rw-r--r-- | grammar.txt | 63 | ||||
| -rw-r--r-- | makkai.md | 19 | ||||
| -rw-r--r-- | src/parser.rs | 217 |
5 files changed, 255 insertions, 116 deletions
@@ -3,9 +3,42 @@ version = 4 [[package]] +name = "convert_case" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "633458d4ef8c78b72454de2d54fd6ab2e60f9e02be22f3c6104cdc8a4e0fceb9" +dependencies = [ + "unicode-segmentation", +] + +[[package]] +name = "derive_more" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d751e9e49156b02b44f9c1815bcb94b984cdcc4396ecc32521c739452808b134" +dependencies = [ + "derive_more-impl", +] + +[[package]] +name = "derive_more-impl" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "799a97264921d8623a957f6c3b9011f3b5492f557bbb7a5a19b7fa6d06ba8dcb" +dependencies = [ + "convert_case", + "proc-macro2", + "quote", + "rustc_version", + "syn", + "unicode-xid", +] + +[[package]] name = "makkai" version = "0.1.0" dependencies = [ + "derive_more", "peg", ] @@ -55,7 +88,45 @@ dependencies = [ ] [[package]] +name = "rustc_version" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92" +dependencies = [ + "semver", +] + +[[package]] +name = "semver" +version = "1.0.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" + +[[package]] +name = "syn" +version = "2.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] name = "unicode-ident" version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "unicode-segmentation" +version = "1.13.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9629274872b2bfaf8d66f5f15725007f635594914870f65218920345aa11aa8c" + +[[package]] +name = "unicode-xid" +version = "0.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853" @@ -4,4 +4,5 @@ version = "0.1.0" edition = "2024" [dependencies] +derive_more = { version = "2.1", features = ["display"] } peg = "0.8.5" diff --git a/grammar.txt b/grammar.txt new file mode 100644 index 0000000..34d8e1b --- /dev/null +++ b/grammar.txt @@ -0,0 +1,63 @@ +program = { declaration } ; + +declaration = set_decl | element_decl | theory_decl | instance_decl ; + +set_decl = "let set" , set_var , "=" , set ; +element_decl = "let element" , elem_var , ":" , set , "=" , element ; +theory_decl = "let signature" , sig_var , "=" , signature ; +instance_decl = "let instance" , inst_var , "::" , signature , "=" , instance ; + +set = record_set | variant_set | builtin_set | claimed_set | set_var | "(" , set , ")" ; +record_set = "record" , "{" , [ set_field { "," , set_field } ] , "}" ; +set_field = "." , lower_ident , ":" , set ; +variant_set = "variant" , "{" , [ variant_field { "|" , variant_field } ] , "}" ; +variant_field = lower_ident , "." , ":" , set ; +builtin_set = "Nat" | "Int" | "Float" | "Str" | "Bool" ; +claimed_set = "set" , "(" , instance , ")" ; + +signature = "Set" | theory_sig | function_sig | sig_var | "(" , signature , ")" ; +theory_sig = "theory" , "{" , [ sig_field { "," , sig_field } ] , "}" ; +sig_field = "." , upper_ident , "::" , signature ; +function_sig = param_list , "->" , signature ; +param_list = param { param } ; +param = "(" , elem_var , ":" , set , ")" ; + +element = case_elem | app_elem ; +case_elem = "case" , element , "of" , "{" , [ case_arm { "|" , case_arm } ] , "}" ; +case_arm = inject_elem , elem_var , "=>" , element ; +app_elem = dot_elem { dot_elem } ; +dot_elem = { inject_elem } , atom_elem , { project_elem } ; +inject_elem = ident , "." ; +project_elem = "." , ident ; +atom_elem = literal | elem_var | record_elem | "(" , element , ")" ; +record_elem = "{" , [ elem_assign { "," , elem_assign } ] , "}" ; +elem_assign = project_elem , "=" , element ; + +instance = for_inst | app_inst ; +for_inst = "for" , param_list , "," , instance ; +app_inst = dot_inst { dot_elem } ; +dot_inst = atom_inst { project_elem } ; +atom_inst = set | inst_var | record_inst | "(" , instance , ")" ; +record_inst = "{" , [ inst_assign { "," , inst_assign } ] , "}" ; +inst_assign = project_elem , "=" , instance ; + +literal = nat_lit | int_lit | float_lit | str_lit | bool_lit ; +nat_lit = digit , { digit } ; +int_lit = "-" , digit , { digit } ; +float_lit = [ "-" ] , digit , { digit } , "." , digit , { digit } ; +str_lit = '"' , { any_character_except_quote } , '"' ; +bool_lit = "true" | "false" ; + +set_var = upper_ident ; +sig_var = upper_ident ; +elem_var = lower_ident ; +inst_var = lower_ident ; + +upper_ident = upper_case_letter , { ident_char } ; +lower_ident = lower_case_letter , { ident_char } ; +ident = (upper_case_letter | lower_case_letter) , { ident_char } ; + +upper_case_letter = "A"..."Z" ; +lower_case_letter = "a"..."z" ; +digit = "0"..."9" ; +ident_char = upper_case_letter | lower_case_letter | digit | "_" | "'" ; @@ -24,30 +24,25 @@ For each `B ∈ { Nat, Int, Float, Str }`: ### Variables - `C ⊢ x : X` when `x : X` is in `C`. -### Conjunction (records) -- **Formation.** `C ⊢ record { .x0 : X0, ..., .xn : Xn } set` when - `C ⊢ X0 set`, `C, x0 : X0 ⊢ X1 set`, ..., `C, x0 : X0, ..., xn-1 : Xn-1 ⊢ Xn set`. -- **Intro.** `C ⊢ { .x0 = m0, ..., .xn = mn } : record { .x0 : X0, ..., .xn : Xn }` when - `C ⊢ m0 : X0`, `C ⊢ m1 : X1[m0/x0]`, ..., `C ⊢ mn : Xn[m0/x0, ..., mn-1/xn-1]`. +### Records +- **Formation.** `C ⊢ record { .x0 : X0, ..., .xn : Xn } set` when `C ⊢ X0 set`, `C, x0 : X0 ⊢ X1 set`, ..., `C, x0 : X0, ..., xn-1 : Xn-1 ⊢ Xn set`. +- **Intro.** `C ⊢ { .x0 = m0, ..., .xn = mn } : record { .x0 : X0, ..., .xn : Xn }` when `C ⊢ m0 : X0`, `C ⊢ m1 : X1[m0/x0]`, ..., `C ⊢ mn : Xn[m0/x0, ..., mn-1/xn-1]`. - **Elim.** `C ⊢ m.xi : Xi[m.x0/x0, ..., m.xi-1/xi-1]` when `C ⊢ m : record { .x0 : X0, ..., .xn : Xn }`. - **β.** `{ ..., .xi = mi, ... }.xi=mi`. - **η.** `m=record { .x0=m.x0, ..., .xn=m.xn }` when `m : record { ... }`. -### Disjunction (variants) +### Variants - **Formation.** `C ⊢ variant { v0. : X0 | ... | vn. : Xn } set` when each `C ⊢ Xi set`. - **Intro.** `C ⊢ vi.(m) : variant { v0. : X0 | ... | vn. : Xn }` when `C ⊢ m : Xi`. -- **Elim.** `C ⊢ case m of { v0.x0 => n0 | ... | vn.xn => nn } : X` when - `C ⊢ m : variant { v0. : X0 | ... | vn. : Xn }` and, for each `i`, `C, xi : Xi ⊢ ni : X`. +- **Elim.** `C ⊢ case m of { v0.x0 => n0 | ... | vn.xn => nn } : X` when `C ⊢ m : variant { v0. : X0 | ... | vn. : Xn }` and, for each `i`, `C, xi : Xi ⊢ ni : X`. - **β.** `case vi.(m) of { ... | vi.xi => ni | ... }=ni[m/xi]`. - **η.** `m=case m of { v0.x0 => v0.(x0) | ... | vn.xn => vn.(xn) }` when `m : variant { ... }`. ## The signature layer ### Theory -- **Formation.** `C ⊢ theory { .s0 :: S0, ..., .sn :: Sn } signature` when - `C ⊢ S0 signature`, `C, s0 :: S0 ⊢ S1 signature`, ..., `C, s0 :: S0, ..., sn-1 :: Sn-1 ⊢ Sn signature`. -- **Intro.** `C ⊢ { .s0 = I0, ..., .sn = In } :: theory { .s0 :: S0, ..., .sn :: Sn }` when - `C ⊢ I0 :: S0`, `C ⊢ I1 :: S1[I0/s0]`, ..., `C ⊢ In :: Sn[I0/s0, ..., In-1/sn-1]`. +- **Formation.** `C ⊢ theory { .s0 :: S0, ..., .sn :: Sn } signature` when `C ⊢ S0 signature`, `C, s0 :: S0 ⊢ S1 signature`, ..., `C, s0 :: S0, ..., sn-1 :: Sn-1 ⊢ Sn signature`. +- **Intro.** `C ⊢ { .s0 = I0, ..., .sn = In } :: theory { .s0 :: S0, ..., .sn :: Sn }` when `C ⊢ I0 :: S0`, `C ⊢ I1 :: S1[I0/s0]`, ..., `C ⊢ In :: Sn[I0/s0, ..., In-1/sn-1]`. - **Elim.** `C ⊢ I.si :: Si[I.s0/s0, ..., I.si-1/si-1]` when `C ⊢ I :: theory { .s0 :: S0, ..., .sn :: Sn }`. - **β.** `{ ..., .si=Ii, ... }.si=Ii`. - **η.** `I={ .s0=I.s0, ..., .sn=I.sn }` when `I :: theory { ... }`. diff --git a/src/parser.rs b/src/parser.rs index 1af9d49..a0da79c 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -1,8 +1,9 @@ +use derive_more::Display; use peg::parser; // Set layer -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Display)] pub enum BuiltIn { Nat, Int, @@ -11,55 +12,68 @@ pub enum BuiltIn { Bool, } -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{name} : {set}")] pub struct SetField { pub name: String, pub set: Set, -} // .x : X +} -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Display)] +#[display("{name}. : {set}")] pub struct VariantField { pub name: String, pub set: Set, -} // x. : X +} -#[derive(Clone, Debug, PartialEq)] +#[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)] +#[derive(Clone, Debug, PartialEq, Display)] +#[display("({name} : {set})")] pub struct Param { pub name: String, pub set: Set, -} // (x : X) +} -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{name} :: {signature}")] pub struct SigField { pub name: String, pub signature: Signature, -} // .s :: S +} -#[derive(Clone, Debug, PartialEq)] +#[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>, - }, // (x:X)(y:Y) -> S + }, + #[display("{_0}")] Var(String), } // Element layer -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Display)] pub enum Literal { Nat(u64), Int(i64), @@ -68,27 +82,36 @@ pub enum Literal { Bool(bool), } -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{name} = {element}")] pub struct ElemAssign { pub name: String, pub element: Element, -} // .x = m +} -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{tag} {bound} => {body}")] pub struct CaseArm { pub tag: String, pub bound: String, pub body: Element, -} // v. x => n +} -#[derive(Clone, Debug, PartialEq)] +#[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>), - Project(Box<Element>, String), // m .x - Inject(String, Box<Element>), // v. m - App(Box<Element>, Box<Element>), // f x + #[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>, @@ -97,41 +120,47 @@ pub enum Element { // Instance layer -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Display)] +#[display(".{name} = {instance}")] pub struct InstAssign { pub name: String, pub instance: Instance, -} // .s = I +} -#[derive(Clone, Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq, Display)] pub enum Instance { - SetCoerce(Box<Set>), // X :: Set + #[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>, - }, // for (x:X), I - App(Box<Instance>, Box<Element>), // I m - Project(Box<Instance>, String), // I .s + }, + #[display("{_0} {_1}")] + App(Box<Instance>, Box<Element>), + #[display("{_0} .{_1}")] + Project(Box<Instance>, String), } // Declarations -#[derive(Clone, Debug, PartialEq)] + +#[derive(Clone, Debug, PartialEq, Display)] pub enum Decl { - Set { - name: String, - set: Set, - }, + #[display("let set {name} = {set}")] + Set { name: String, set: Set }, + #[display("let element {name} : {set} = {element}")] Element { name: String, set: Set, element: Element, }, - Signature { - name: String, - signature: Signature, - }, + #[display("let signature {name} = {signature}")] + Signature { name: String, signature: Signature }, + #[display("let instance {name} :: {signature} = {instance}")] Instance { name: String, signature: Signature, @@ -139,7 +168,9 @@ pub enum Decl { }, } -pub type Program = Vec<Decl>; +#[derive(Display)] +#[display("{}", _0.iter().map(|d| d.to_string()).collect::<Vec<_>>().join("\n"))] +pub struct Programme(Vec<Decl>); parser! { pub grammar parser() for str { @@ -153,26 +184,26 @@ parser! { // 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 kw_let_set() = "let set" wb() + rule kw_let_element() = "let element" wb() + rule kw_let_signature() = "let signature" 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_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() @@ -242,63 +273,52 @@ parser! { // set layer rule set_field() -> SetField - = n:project_lower() _ ":" _ s:set() - { SetField { name: n, set: s } } + = n:project_lower() _ ":" _ s:set() { SetField { name: n, set: s } } rule variant_field() -> VariantField - = n:inject_lower() _ ":" _ s:set() _ - { VariantField { name: n, set: s } } + = n:inject_lower() _ ":" _ s:set() _ { VariantField { name: n, set: s } } rule claimed_set() -> Instance - = kw_set() "(" _ i:instance() _ ")" {i} + = 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) } + = 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 } } + = "(" _ 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 } } + = 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) } } + / 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 } } + = 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) } + / "{" fs:(elem_assign() ** ",") _ "}" { Element::Record(fs) } / "(" _ e:element() _ ")" { e } rule dot_elem() -> Element - = tags:(t:inject() _ { t })* - head:atom_elem() - projs:(p:project() { p })* + = 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) @@ -317,15 +337,10 @@ parser! { } 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 } } pub rule element() -> Element - = kw_case() __ scrut:element() _ kw_of() _ "{" - arms:(_ a:case_arm() _ { a }) ** "|" - _ "|"? - _ "}" - { Element::Case { scrutinee: Box::new(scrut), arms } } + = kw_case() __ scrut:element() _ kw_of() _ "{" arms:(_ a:case_arm() _ { a }) ** "|" _ "}" { Element::Case { scrutinee: Box::new(scrut), arms } } / app_elem() // instance layer @@ -337,8 +352,7 @@ parser! { rule atom_inst() -> Instance = s:set() { Instance::SetCoerce(Box::new(s)) } / v:inst_var() { Instance::Var(v) } - / "{" fs:(inst_assign() ** ",") _ ","? _ "}" - { Instance::Record(fs) } + / "{" fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) } / "(" _ i:instance() _ ")" { i } rule dot_inst() -> Instance @@ -358,24 +372,19 @@ parser! { } pub rule instance() -> Instance - = kw_for() __ ps:param_list() _ "," _ body:instance() - { Instance::For { params: ps, body: Box::new(body) } } + = 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 } } + = 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() -> Program - = _ ds:(decl() ** _) _ { ds } + pub rule program() -> Programme + = _ ds:(decl() ** _) _ { Programme(ds) } } } @@ -385,7 +394,7 @@ mod tests { fn debug_parse(src: &str) { match parser::program(src) { - Ok(p) => println!("```{}\n```\n=> {:?}\n", src, p), + Ok(p) => println!("```{}\n```\n=>\n{}\n", src, p), Err(e) => { let line = e.location.line; let col = e.location.column; @@ -437,9 +446,9 @@ let set Maybe = variant { #[test] fn test_theories_and_instances() { let src = r#" - let theory Graph = theory { + let signature Graph = theory { .Node :: Set, - .Edge :: (s : Node) (t : Node) -> Set, + .Edge :: (s : Node) (t : Node) -> Set } let instance loop :: Graph = { |