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 = "+" | "-" | "*" | "/"
| "<=" | ">=" | "<" | ">"
| "=" | "&&" | "||"