rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

update syntax.ebnf

Browse source
This commit is contained in:
rhiannon morris 2023-12-04 23:35:54 +01:00
parent e48f03a61c
commit 8b8129027d
1 changed files with 11 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
syntax.ebnf
View file

@ -24,7 +24,7 @@ dim arg = "@", dim.
pat var = NAME | "_". pat var = NAME | "_".
term = lambda | case | pi | sigma | ann. term = lambda | pi | sigma | ann | let.
lambda = ("λ" | "δ"), {pat var}+, "⇒", term. lambda = ("λ" | "δ"), {pat var}+, "⇒", term.
@ -49,12 +49,18 @@ sigma = (binder | ann), "×", (sigma | ann).
ann = infix eq, ["∷", term]. 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 *) infix eq = app term, ["≡", term, ":", app term]. (* dependent is below *)
app term = coe | comp | split universe | dep eq | succ | normal app. app term = coe | comp | split universe | dep eq | special app | normal app.
split universe = "★", NAT. split universe = "★", NAT.
dep eq = "Eq", type line, term arg, term arg. dep eq = "Eq", type line, term arg, term arg.
succ = "succ", term arg. special app = ("fst" | "snd" | "succ"), {term arg}+.
normal app = term arg, {term arg | dim arg}. normal app = term arg, {term arg | dim arg}.
(* direction defaults to @0 @1 *) (* direction defaults to @0 @1 *)
@ -76,4 +82,5 @@ term arg = UNIVERSE | "★", SUPER
| "zero" | "zero"
| NAT | NAT
| QNAME, displacement | QNAME, displacement
| "(", {term / ","}+, [","], ")". | "(", {term / ","}+, [","], ")"
| case.