87 lines
2.4 KiB
EBNF
87 lines
2.4 KiB
EBNF
input = {top level}.
|
||
|
||
top level = load | decl.
|
||
|
||
decl = namespace | def.
|
||
|
||
(* top level semicolons are optional because all decls start with a
|
||
special word. like in ocaml *)
|
||
|
||
load = "load", STRING, [";"].
|
||
|
||
namespace = "namespace", "{", {decl}, "}", [";"].
|
||
|
||
def = def intro, NAME, [":", term], "=", term, [";"].
|
||
def intro = "def0" | "defω" | "def", [qty, "."].
|
||
(* "def" with no qty defaults to ω *)
|
||
|
||
qty = "0" | "1" | "ω".
|
||
|
||
dim = dim const | name.
|
||
dim const = "0" | "1".
|
||
dim arg = "@", dim.
|
||
|
||
|
||
pat var = NAME | "_".
|
||
|
||
term = lambda | pi | sigma | ann | let.
|
||
|
||
lambda = ("λ" | "δ"), {pat var}+, "⇒", term.
|
||
|
||
case = case intro, term, "return", case return, "of", case body.
|
||
(* default qty is 1 *)
|
||
case intro = "case0" | "case1" | "caseω" | "case", [qty, "."].
|
||
case return = [pat var, "⇒"], term.
|
||
case body = "{", {pattern, "⇒", term / ";"}, [";"], "}".
|
||
|
||
pattern = "zero" | "0"
|
||
| "succ", pat var, [",", [qty, "."], pat var]
|
||
(* default qty for IH is 1 *)
|
||
| TAG
|
||
| "[", pat var, "]"
|
||
| "(", pat var, ",", pat var, ")".
|
||
|
||
(* default qty is 1 *)
|
||
pi = [qty, "."], (binder | term arg), "→", term.
|
||
binder = "(", {NAME}+, ":", term, ")".
|
||
|
||
sigma = (binder | ann), "×", (sigma | ann).
|
||
|
||
ann = infix eq, ["∷", term].
|
||
|
||
bare let binder = pat var, "=", term.
|
||
qty let binder = [qty, "."], bare let binder.
|
||
|
||
let = ("let0" | "let1" | "letω"), {bare let binder / ";"}+, "in", term
|
||
| "let", {qty let binder / ";"}+, "in", term.
|
||
|
||
infix eq = app term, ["≡", term, ":", app term]. (* dependent is below *)
|
||
|
||
app term = coe | comp | split universe | dep eq | special app | normal app.
|
||
split universe = "★", NAT.
|
||
dep eq = "Eq", type line, term arg, term arg.
|
||
special app = ("fst" | "snd" | "succ"), {term arg}+.
|
||
normal app = term arg, {term arg | dim arg}.
|
||
|
||
(* direction defaults to @0 @1 *)
|
||
coe = "coe", type line, [dim arg, dim arg], term arg.
|
||
type line = "[", [pat var, "⇒"], term, "]".
|
||
|
||
comp = "comp", type line, [dim arg, dim arg],
|
||
term arg, dim arg, comp body.
|
||
comp body = "{", comp branch, ";", comp branch, [";"], "}".
|
||
comp branch = dim const, name, "⇒", term.
|
||
|
||
displacement = SUPER.
|
||
|
||
term arg = UNIVERSE | "★", SUPER
|
||
| "{", {BARE TAG / ","}, [","], "}"
|
||
| TAG
|
||
| "[", [qty, "."], term, "]"
|
||
| "ℕ"
|
||
| "zero"
|
||
| NAT
|
||
| QNAME, displacement
|
||
| "(", {term / ","}+, [","], ")"
|
||
| case.
|