2. Language Reference

This section gives a systematic overview of the Statix language.

2.1. Lexical matters

2.1.1. Identifiers

lc-id = [a-z][a-zA-Z0-9\_]*
uc-id = [A-Z][a-zA-Z0-9\_]*

Most identifiers in Statix fall into one of two categories, which we will refer to as:

  • Lowercase identifiers, that start with a lowercase character, and must match the regular expression [a-z][a-zA-Z0-9\_]*.
  • Uppercase identifiers, that start with an uppercase character, and must match the regular expression [A-Z][a-zA-Z0-9\_]*.

2.1.2. Comments

Comments in Statix follow the C-style:

  • // ... single line ... for single-line comments
  • /* ... multiple lines ... */ for multi-line comments

Multi-line comments can be nested, and run until the end of the file when the closing */ is omitted.

2.2. Terms and patterns

term = uc-id "(" {term ","}* ")"
     | "(" {term ","}* ")"
     | "[" {term ","}* "]"
     | "[" {term ","}* "|" term "]"
     | int
     | str
     | namespace-id? "{" {term ", "}* ("@" var-id)? "}"
     | var-id

pattern = uc-id "(" {pattern ","}* ")"
        | "(" {pattern ","}* ")"
        | "[" {pattern ","}* "]"
        | "[" {pattern ","}* "|" pattern "]"
        | int
        | str
        | var-id
        | "_"

 int = [1-9][0-9]*
 str = "\"" ([^\"\\]|"\\"[nrt\\])* "\""

 position = "-"
          | var-id
          | "_"

2.3. Modules

module module-id

  section*

NaBL2 specifications are organized in modules. A module is identified by a module identifier. Module identifiers consist of one or more names seperated by slashes, as in {name /}+. The names must match the regular expression [a-zA-Z0-9\_][a-zA-Z0-9\_\.\-]*.

Every module is defined in its own file, with the extensions .stx. The module name and the file paths must coincide.

Example. An empty module analysis/main, defined in a file .../analysis/main.nabl2.

module analysis/main

// work on this

Modules consist of sections for imports, signatures, and rule definitions. The rest of this section describes imports, and subsequents sections deal with signatures and rules.

2.3.1. Imports

imports

  module-ref*

A module can import definitions from other modules be importing the other module. Imports are specified in an imports section, which lists the modules being imported. A module reference can be:

  • A module identifier, which imports a single module with that name.
  • A wildcard, which imports all modules with a given prefix. A wildcard is like a module identifier, but with a dash as the last part, as in {name /}+ /-.

A wildcard import does not work recursively. For example, analysis/- would imports analysis/functions, and analysis/classes, but not analysis/lets/recursive.

Example. A main module importing several submodules.

module main

imports

   builtins
   functions/-
   classes/-
   types

2.4. Signatures

signatures

  signature*

2.4.1. Terms

Sorts

Constructors

2.4.2. Name binding

Relations

Namespaces

Name resolution

2.4.3. Rules

constraint generator

  rule-def*

2.4.4. Predicat rules

2.4.5. Functional rules

2.4.6. Mapping rules

2.5. Constraints

2.5.1. Base constraints

2.5.2. Term equality

2.5.3. Name binding

Scope graph

Queries

Occurrences

2.5.4. Arithmetic

2.6. Misc notes

2.6.1. Error messages