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.