quox/syntax.ebnf

86 lines
2.4 KiB
EBNF
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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.