Alpha grammar

Generated by debug/docs-set.py. Do not edit by hand: this document is derived from the live compiler, so editing it here would only make it disagree with the language.

Lexical structure

an identifier begins with a letter and continues with letters, digits, -, /, . or '
a comment runs from -- to the end of the line
the only delimiters are ( and ); :, . and = are their own lexemes
a natural literal is a run of decimal digits

Module grammar

A module is a sequence of line-oriented declarations:

module <qualified-name>
import <qualified-name>        -- must name an earlier module
family <Name> : Type <level>  -- parameters, indices, constructors, fields, then end-family
def <name> [: <type>] = <term>

Families precede definitions. An import must name a module that appears earlier in the closure, so the module graph is acyclic by construction.

Term forms (78)

Every form the edition defines, in the syntax the parser accepts:

form	shape
`app`	`(app FUNCTION ARGUMENT)`
`bind`	`(bind EFFECTS RESULT COMPUTATION CONTINUATION)`
`byte`	`(byte 0..255)`
`byte-and`	`see docs/language/SPECIFICATION.md`
`byte-equal`	`(byte-equal A B)`
`byte-less-than`	`(byte-less-than A B)`
`byte-or`	`see docs/language/SPECIFICATION.md`
`byte-shift-left`	`see docs/language/SPECIFICATION.md`
`byte-shift-right`	`see docs/language/SPECIFICATION.md`
`byte-string-literal`	`see docs/language/SPECIFICATION.md`
`byte-to-nat`	`(byte-to-nat BYTE)`
`byte-xor`	`see docs/language/SPECIFICATION.md`
`bytes`	`(bytes B0 B1 ...)`
`bytes-append`	`(bytes-append A B)`
`bytes-builder-append`	`(bytes-builder-append A B)`
`bytes-builder-build`	`(bytes-builder-build BUILDER)`
`bytes-builder-chunk`	`(bytes-builder-chunk BYTES)`
`bytes-builder-empty`	`(bytes-builder-empty)`
`bytes-checksum`	`(bytes-checksum BYTES)`
`bytes-cons`	`(bytes-cons BYTE BYTES)`
`bytes-eliminate`	`(bytes-eliminate MOTIVE BASE STEP SCRUTINEE)`
`bytes-equal`	`(bytes-equal A B)`
`bytes-head`	`(bytes-head BYTES)`
`bytes-index-nonzero`	`(bytes-index-nonzero BYTES INDEX)`
`bytes-length`	`(bytes-length BYTES)`
`bytes-set-free-index`	`(bytes-set-free-index BYTES INDEX DEPTH OFFSET)`
`bytes-set-index`	`(bytes-set-index BYTES INDEX)`
`bytes-tail`	`(bytes-tail BYTES)`
`case`	`see docs/language/SPECIFICATION.md`
`computation`	`(computation EFFECTS RESULT)`
`constructor`	`(constructor FAMILY CONSTRUCTOR ARGUMENT ...)`
`do`	`see docs/language/SPECIFICATION.md`
`effect-row`	`(effect-row)`
`effects`	`(effects E ...)`
`eliminate`	`(eliminate FAMILY MOTIVE SCRUTINEE (branch C BINDER ... . BODY) ...)`
`equal`	`(equal TYPE LEFT RIGHT)`
`f32-add`	`see docs/language/SPECIFICATION.md`
`f32-divide`	`see docs/language/SPECIFICATION.md`
`f32-equal`	`see docs/language/SPECIFICATION.md`
`f32-less-than`	`see docs/language/SPECIFICATION.md`
`f32-multiply`	`see docs/language/SPECIFICATION.md`
`f32-subtract`	`see docs/language/SPECIFICATION.md`
`family`	`(family NAME ARGUMENT ...)`
`first`	`(first PAIR)`
`fsucc`	`(fsucc BOUND INDEX)`
`fzero`	`(fzero BOUND)`
`ih`	`see docs/language/SPECIFICATION.md`
`lambda`	`(lambda QUANTITY NAME : TYPE . BODY)`
`let`	`(let QUANTITY NAME = VALUE in BODY)`
`let*`	`see docs/language/SPECIFICATION.md`
`match`	`see docs/language/SPECIFICATION.md`
`match-with`	`see docs/language/SPECIFICATION.md`
`nat-add`	`see docs/language/SPECIFICATION.md`
`nat-divide`	`see docs/language/SPECIFICATION.md`
`nat-eliminate`	`(nat-eliminate MOTIVE BASE STEP SCRUTINEE)`
`nat-less-than`	`(nat-less-than A B)`
`nat-literal`	`see docs/language/SPECIFICATION.md`
`nat-modulo`	`see docs/language/SPECIFICATION.md`
`nat-multiply`	`see docs/language/SPECIFICATION.md`
`nat-subtract`	`see docs/language/SPECIFICATION.md`
`nat-to-byte`	`(nat-to-byte NAT)`
`pair`	`(pair SIGMA-TYPE FIRST SECOND)`
`partial`	`(partial COMPUTATION-TYPE)`
`pi`	`(pi QUANTITY NAME : TYPE . RESULT)`
`project`	`see docs/language/SPECIFICATION.md`
`read-file`	`(read-file PATH)`
`record`	`see docs/language/SPECIFICATION.md`
`refl`	`(refl TYPE VALUE)`
`return`	`(return EFFECTS VALUE)`
`runtime-image-v4-build`	`(runtime-image-v4-build BUILDER)`
`second`	`(second PAIR)`
`sigma`	`(sigma QUANTITY NAME : TYPE . RESULT)`
`succ`	`(succ NAT)`
`text-literal`	`see docs/language/SPECIFICATION.md`
`transport`	`(transport MOTIVE PROOF VALUE)`
`update`	`see docs/language/SPECIFICATION.md`
`write-file`	`(write-file PATH CONTENTS)`
`zero`	`zero`

Quantities

erased, affine, linear, unrestricted. A binder's quantity is part of its type and is enforced by the kernel: a linear binder used twice is a ALPHA-QUANTITY-VIOLATION.

The live inventory behind this document: {}.