diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | Cargo.lock | 61 | ||||
| -rw-r--r-- | Cargo.toml | 7 | ||||
| -rw-r--r-- | makkai.md | 71 | ||||
| -rw-r--r-- | src/checker.rs | 7 | ||||
| -rw-r--r-- | src/main.rs | 6 | ||||
| -rw-r--r-- | src/parser.rs | 455 |
7 files changed, 608 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ea8c4bf --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/target diff --git a/Cargo.lock b/Cargo.lock new file mode 100644 index 0000000..f16c8c3 --- /dev/null +++ b/Cargo.lock @@ -0,0 +1,61 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "makkai" +version = "0.1.0" +dependencies = [ + "peg", +] + +[[package]] +name = "peg" +version = "0.8.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9928cfca101b36ec5163e70049ee5368a8a1c3c6efc9ca9c5f9cc2f816152477" +dependencies = [ + "peg-macros", + "peg-runtime", +] + +[[package]] +name = "peg-macros" +version = "0.8.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6298ab04c202fa5b5d52ba03269fb7b74550b150323038878fe6c372d8280f71" +dependencies = [ + "peg-runtime", + "proc-macro2", + "quote", +] + +[[package]] +name = "peg-runtime" +version = "0.8.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "132dca9b868d927b35b5dd728167b2dee150eb1ad686008fc71ccb298b776fca" + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..af01f42 --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "makkai" +version = "0.1.0" +edition = "2024" + +[dependencies] +peg = "0.8.5" diff --git a/makkai.md b/makkai.md new file mode 100644 index 0000000..d08b2db --- /dev/null +++ b/makkai.md @@ -0,0 +1,71 @@ +# Makkai + +## Judgements +- `C ctx` means `C` is a context. +- `C ⊢ X set` means `X` is a set in context `C`. +- `C ⊢ m : X` means `m` is a match of set `X`. +- `C ⊢ S signature` means `S` is a signature in context `C`. +- `C ⊢ I :: S` means `I` is an instance of signature `S`. + +Contexts are built by extension with either kind of binding: +- `· ctx`. +- `C, x : X` ctx, when `C ⊢ X set`. +- `C, i :: S` ctx, when `C ⊢ S signature`. + +Everywhere below, `...` ranges over a finite (possibly zero) index, and the labels `xi`, `si`, `vi` are assumed distinct within any single list. + +## The set layer + +### Built-Ins +For each `B ∈ { Nat, Int, Float, Str }`: +- **Formation.** `C ⊢ B set`. +- **Intro.** Literals of the appropriate form match the corresponding built-in (e.g. `C ⊢ 7 : Nat`). + +### 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]`. +- **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) +- **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`. +- **β.** `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]`. +- **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 { ... }`. + +### Variables +- `C ⊢ i :: S` when `i :: S` is in `C`. + +## The interface + +### The signature `Set` +- **Formation.** `C ⊢ Set signature`. +- **Intro.** `C ⊢ X :: Set` when `C ⊢ X set`. +- **Elim.** `C ⊢ set-of(I) set` when `C ⊢ I :: Set`. +- **β.** `set-of(X)=X` when `X :: Set` arises from `C ⊢ X set`. +- **η.** `I=set-of(I)` viewed as an instance, when `I :: Set`. + +### Extension signatures +- **Formation.** `C ⊢ (x: X) -> S signature` when `C ⊢ X set` and `C, x : X ⊢ S signature`. +- **Intro.** `C ⊢ for (y: X). I :: (x: X) -> S` when `C, y : X ⊢ I :: S[y/x]`. +- **β.** `(for (x: X). I)(y)=I[y/x]`. +- **η.** `I=for (x: X). I(x)` when x is not free in I. 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); + } +} |