CSL Grammar

The following grammar describes the CSL language. CSL source files must be encoded using UTF-8.

CSL is whitespace insensitive. This means that the syntax allows an arbitrary amount of whitespace and comment lines around tokens (written as "token"). Anything on a line between // and the newline character is treated as a comment and ignored.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The top-level entry point to the grammar

csl-unit = declaration*

declaration = type-declaration
            | value-declaration
            | contract-declaration
            | template-declaration
            | module-declaration
            | external-declaration
            | observable-declaration


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; modules

module-declaration = "module" upper-case-identifier "{" declaration*  "}"

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; types

type-declaration = "type" (sum-type-declaration | record-type-declaration)

sum-type-declaration = upper-case-identifier
                       lower-case-identifier*
                       ("|" upper-case-identifier type-atom*)+

record-type-declaration = upper-case-identifier [ ":" type ]
                          "{" [ record-field-declaration ( "," record-field-declaration)* ] "}"
record-field-declaration = lower-case-identifier ":" type

type = type-atom
     | type-application
     | type "->" type ; function type

type-application = type-name
                 | type-application type

type-name = qualifier upper-case-identifier ; type name

type-atom = lower-case-identifier ; type variable

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; external declarations

external-declaration =
  "external"
  [ "<" [ (type-variable-binding ",")* type-variable-binding ] ">" ]
  external-declaration-name
  ":"
  type

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; observables declarations

observable-declaration = "observable" upper-case-identifier ":" type

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; expressions

value-declaration = "val" val-bindings

val-bindings =
  (val-binding "with")* val-binding

val-modifier = "report" | "property" | "test"

val-binding =
  [ val-modifier ]
  [ "<" [ (type-variable-binding ",")* type-variable-binding ] ">" ]
  ; Note: patterns other than 'x : T' are only allowed
  ; if the binding occurs within an expression.
  pattern
  "="
  expression

type-variable-binding = lower-case-identifier [":" "Ord"]

expression = expression expression
           | expression BINARY_OPERATOR expression
           | "(" (expression ",")* [ expression ] ")" ; tuples and parentheses
           | if-expression
           | type-case-expression
           | function-expression
           | match-expression
           | let-expression
           | record-expression
           | qualifier lower-case-identifier ; variable
           | literal
           | qualifier upper-case-identifier ; constructor
           | "[" [ (expression ",")* expression ] "]" ; list
           | expression ":>" type ; upcast operator
           | scenario-expression

if-expression =
  "if" "(" expression ")" expression "else" expression

type-case-expression =
  "type" lower-case-identifier "=" expression "of"
  "{"
  (type-atom "->" expression ";")*
  "_" "->" expression
  "}"

match-expression =
  "match" expression "with" "{" ("|" pattern "->" expression)+ "}"

function-expression =
  "\" pattern "->" expression
  [ "|" pattern "->" expression
    ("|" pattern "->" expression)* ]

let-expression =
  "let" ("val" pattern "=" expression)+
  "in" expression

record-expression =
  type "{" [ "use" expression "with" ] (lower-case-identifier "=" expression ",")* "}"

scenario-expression =
  "scenario" "(" contract ")" expression


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; patterns

pattern =
  (pattern-atom | pattern-apply) ("as" lower-case-identifier)* (":" type)*

pattern-apply = qualifier upper-case-identifier pattern-atom*

pattern-atom = "_"
             | "(" (pattern ",")* [ pattern ] ")" ; tuples and parentheses
             | record-pattern
             | qualifier upper-case-identifier ; constructor
             | lower-case-identifier ; variable
             | literal

record-pattern =
  "?" type
  "{"
  [ (lower-case-identifier "=" pattern ",")*
    lower-case-identifier "=" pattern ]
  "}"


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; contracts

template-declaration = rec-template-declaration
                     | meta-template-declaration

rec-template-declaration = "template" ["rec"] rec-template-bindings
rec-template-bindings =
  (rec-template-binding "with")* rec-template-binding
rec-template-binding =
  [ "entrypoint" ]
  [ "[" "]" ] ; Optional empty list of contract parameters
  upper-case-identifier
  pattern* "=" contract

contract-parameter = "_"
                   | "(" contract-parameter ")"
                   | lower-case-identifier ; variable
                   | contract-parameter ":" type

meta-template-declaration = "template" meta-template-bindings
meta-template-bindings =
  (meta-template-binding "with")* meta-template-binding
meta-template-binding =
  "[" (contract-parameter ",")* contract-parameter "]" ; List of contract parameters
  upper-case-identifier
  "("
  [ (pattern ",")* pattern ]
  ")" "=" contract

contract-declaration = "contract" ["rec"] contract-bindings
contract-bindings =
  (contract-binding "with")* contract-binding
contract-binding =
  [ "entrypoint" ]
  lower-case-identifier
  "="
  contract

local-declaration = template-declaration
                  | contract-declaration
                  | value-declaration

contract = "success"
         | "failure"
         | contract "and" contract
         | contract "or" contract
         | contract "then" contract
         | "(" contract ")"
         | application-contract
         | variable-contract
         | prefix-contract
         | let-contract
         | contract-function
         | obs-contract

contract-function =
  "\" pattern "->" contract
  [ "|" pattern "->" contract
    ("|" pattern "->" contract)* ]

application-contract = qualifier upper-case-identifier
                       "[" (contract ",")* [ contract ] "]"
                       expression*
                     | contract expression

variable-contract = lower-case-identifier

prefix-qualifier = pattern "<-" expression

prefix-contract =
  "<" ( "*" | expression) ">"
  [ lower-case-identifier ":" ] type
  [ "matching" "{" (prefix-qualifier ",")* [ prefix-qualifier ] "}" ]
  [ "where" expression ]

let-contract =
  "let" (local-declaration)+
  "in" contract

obs-contract = "observe" lower-case-identifier "<-"
               qualifier upper-case-identifier expression* "then" contract
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Basic grammar components

external-declaration-name = /prim__[a-zA-Z0-9_]+/
lower-case-identifier = /[a-z][a-zA-Z0-9_]*/
upper-case-identifier = /[A-Z][a-zA-Z0-9_]*/

literal = float-literal
        | integer-literal
        | duration-literal
        | date-time-literal
        | string-literal

float-literal = /[0-9]+\.[0-9]+([eE][+-]?[0-9]+)?/
integer-literal = /[0-9]+/

fixed3 = /[0-9]+(\.[0-9]{1,3})?/
duration-literal =
  "#"
  /[+-]?P/ (duration-time | duration-date duration-time?)
  "#"

duration-date = fixed3 "D"
duration-time = "T" (duration-hours | duration-minutes | duration-seconds)
duration-hours = fixed3 "H" (duration-minutes | duration-seconds)?
duration-minutes = fixed3 "M" duration-seconds?
duration-seconds = fixed3 "S"

; These two are defined elsewhere.
date-time-literal =
  "#"
  ( ( /[0-9]{4}/
    | /[0-9]{4}-[0-9]{2}/
    | /[0-9]{4}-[0-9]{2}-[0-9]{2}/
    | /[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}/
    | /[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}/
    | /[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}/
    | /[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}\.[0-9]{0,3}/
    )
    [ /[+-][0-9]{4}|[+-][0-9]{2}:[0-9]{2}|Z/ ]
  ) "#"
string-literal = haskell-style-string ; see Haskell 98 report

; A sequence of zero or more qualifer names interspersed with '::'.
qualifier = (upper-case-identifier "::")*

BINARY_OPERATOR = "+" | "-" | "*" | "/"
                | "<=" | ">=" | "<" | ">"
                | "=" | "&&" | "||"