Expressions

Every expression has a type that can be uniquely determined from the expression itself, provided the expression is well-formed and well-typed.

Expression ::=
  | Literal
  | Id
  | OperatorExpr
  | FunctionCall
  | LabeledExpr
  | LetExpr
  | QuantifierExpr
  | "(" Expression ")"

Literal expressions

Literal ::=
  | false | true
  | 0 | 1 | 2 | ...
  | "|" LiteralIdentifier ":" Type "|"

The literals false and true have the built-in type bool.

Natural numbers have the built-in type int. They are unbounded integers.

A custom literal is an identifier-like token with a given type. TODO: description

Identifier expressions

Id ::=
  Identifier

The given identifier denotes a variable in scope, specifically

• in-, inout-, or out-parameter

• mutable or immutable local variable

• bound variable

Operator expressions

OperatorExpr ::=
  | if Expression Expression else Expression
  | Expression BinaryOp Expression
  | UnaryOp Expression
BinaryOp ::=
  | "<==>"
  | "==>" | "<=="
  | "&&" | "||"
  | "==" | "!=" | "<" | "<=" | ">=" | ">"
  | "+" | "-"
  | "*" | "div" | "mod"
UnaryOp ::=
  | "!" | "-"

Function calls

FunctionCall ::=
  Identifier "(" Expression*, ")"

TODO: description

Labeled expressions

LabeledExpr ::=
  Identifier ":" Expression

The Expression parses as far as possible.

TODO: description

Let expressions

LetExpr ::=
  val Identifier ":=" Expression Expression

Note that there is no punctuation between the two expressions.

TODO: description

Quantifier expressions

QuantifierExpr ::=
  ( forall | exists ) Identifier ":" Type
  Pattern*
  Expression
Pattern ::=
  pattern Expression+,

TODO: description