Grammar

The full grammar, in EBNF. The normative specification of the language — lexis, static semantics, the refinement relation and the diagnostic codes — lives in the repository beside the parser that implements it; this page is the shape of the text.

declaration    = kernel-decl | spec-decl ;

kernel-decl    = "kernel" ident [ parameters ]
                 "(" [ arguments ] ")"
                 "->" results ;

spec-decl      = "spec" ident version [ string ]
                 "{" kernel-decl "}" ;

version        = digits "." digits "." digits ;

parameters     = "<" parameter { "," parameter } [ "," ] ">" ;
parameter      = type-param | value-param ;
type-param     = "type" ident [ ":" constraint | "=" scalar-type ] ;
value-param    = ident ":" scalar-type ;
constraint     = "Numeric" | "Integer" | "Real" ;

arguments      = argument { "," argument } [ "," ] ;
argument       = "%" ident ":" type [ "=" ident ] ;
results        = result | "(" result { "," result } [ "," ] ")" ;
result         = "%" ident ":" type ;

type           = scalar-type | ident | tensor | secret ;
scalar-type    = int-type | float-type ;
int-type       = "i8" | "i16" | "i32" | "i64"
               | "u8" | "u16" | "u32" | "u64" ;
float-type     = "f32" | "f64" ;
tensor         = "tensor" "<" dimension { "x" dimension } "x" element ">" ;
element        = scalar-type | ident ;
dimension      = "?" | digits | ident ;
secret         = "secret" "<" type ">" ;

ident          = letter { letter | digit | "_" } ;
letter         = "A"…"Z" | "a"…"z" | "_" ;
digits         = digit { digit } ;
digit          = "0"…"9" ;
string         = '"' { character except '"' and line feed } '"' ;
comment        = "//" { character except line feed } ;

Notes a tool needs beyond the productions:

• One production for both. A kernel and a specification differ in static semantics, not syntax: a kernel may leave things open, a specification may not.
• Dimension-list mode. Inside tensor<…> the letter x is a separator when surrounded by whitespace or preceded by a digit or ?; otherwise it is part of an identifier. See Types.
• Reserved words — kernel, spec, type, secret, tensor, the value types, the classes and the scalar types — may not be used as identifiers.
• = ident on an argument is meaningful only for arguments a specification adds beyond its kernel's; see Declarations.
• Comments are equivalent to whitespace and are not in the tree; the source text is canonical and rendered in full.