ABSTRACT SYNTAX

natural literal n = 0 | 1 | 2 | ...
integer literal i = ... | -2 | -1 | 0 | 1 | 2 | ...
kind k = Type(n) | Dependent(x)
integer bound B = i | -inf | inf
variable x
monotype t =
| x
| x(t, ..., t)
| int_range(B1, B2)
| tuple(t, ..., t)
| collection(t)
| fun(t, ..., t) -> t
| dependent(x)
| bool
| prop
| string
| state

For Vale/Dafny, collection = seq | set
For Vale/F*, collection = list

polytype T =
| forall a1:Type(0) ... an:Type(0). t
| forall a1:Type(0) ... an:Type(0). (x:t, ..., x:t) -> t (requires e) (ensures e)

bind = forall | exists | lambda
icmp = < | > | <= | >=
bop = && | ||
Bop = /\ | \/ | ==> | <== | <==>
trigger = {e, ..., e}
triggers = trigger ... trigger

expression e =
| #t(e)
| x
| x(e, ..., e)
| i | true | false | "...string-literal..."
| old(e)
| old[e](e)
| tuple(e, ..., e)
| collection(e, ..., e)
| (-e)
| e * e | e / e | e % e | e + e | e - e
| e icmp e | e = e | e <> e | e == e | e != e
| !e | e bop e | e Bop e
| if e then e else e
| let x:t = e1 in e2
| bind x:t, ..., x:t triggers :: e

destination dst =
| x
| let x:t

statement s =
| dst, ..., dst := x(e, ..., e)
| ...

Note: the following expressions are resolved into x(e1, ..., en) expressions for type checking:
| e[e] | e[e := e] | e.x | e.(x := e) | e is x
In the x(e1, ..., en) expression, the function x is an overloaded operator name,
written in Vale syntax as "operator([])", "operator([:=])", "operator(.x)", or "operator(.x:=)".
Inside the type checker, the overloaded operator name also contains the type name of the first
argument e1; this type name distinguishes different declarations of the same overloaded operator.
The type of e1 must be a named type x:k or x:(k, ..., k) -> k or a primitive type like "int",
not a type abbreviation x:k = t or x(...):k = t.

IO = in | out | inout
param = ghost | inline | IO operand
local = const ghost | mutable ghost | inline | IO operand
ret = ghost
opr_type = const | x | IO x
procedure types P = (param x:t, ..., param x:t) -> (ret x:t, ..., ret x:t) (reads x ... x) (modifies x ... x) (requires e) (ensures e)

environment members g =
| x:k | x:(k, ..., k) -> k | x:k = t | x(x:k, ..., x:k):k = t  (global type declarations)
| x:T | x:P | operand x:P  (global value declarations)
| operand x:t = opr_type, ..., opr_type   (global operand type declarations)
| operand x(param x:t, ..., param x:t):t  (global operand procedure type declarations)
| state x:t  (global state member)
| local x:t  (local value declarations)
| inline_only  (only allow inline expressions -- no ghost variables)
environment G = g ... g

Notes on variable scope:
- Global declarations have fully qualified names consisting of a module name plus a name within the module.
- No two modules can have the same name.
- Within a module, no two declarations can have the same name.
- In a scope that already has a local name x, it is illegal to declare another local with the same name x.
- In procedures, the environment contains a mutable ghost variable named "this" of type state
Local declarations (local x:t) are not qualified with a module name, and so do not conflict with global declarations.
However, references to global declarations can be unqualified (omitting the module name),
and in this case it's possible for a name x to match both a local name and a global name.
In this case, the local name takes precedence.


KINDING:  G |- t : k

G = ... x:k ... OR G = ... x:k = t ...
--------------------------------------
G |- x : k

G |- ... x:(k1, ..., kn) -> k0
G |- t1 : k1
...
G |- tn : kn
------------------------------
G |- x(t1, ..., tn) : k0

G |- int(-inf, inf) : Type(0)

G |- int(-inf, i) : Type(0)

G |- int(i, inf) : Type(0)

G |- int(i1, i2) : Type(0)

G |- t1 : Type(0)
...
G |- tn : Type(0)
---------------------------------
G |- tuple(t1, ..., tn) : Type(0)

G |- t0 : Type(0)
G |- t1 : Type(0)
...
G |- tn : Type(0)
-------------------------------------
G |- fun(t1, ..., tn) -> t0 : Type(0)

G |- t : Type(0)
----------------------------
G |- collection(t) : Type(0)

G |- bool : Type(0)

G |- prop : Type(1)

G |- string : Type(0)

G |- state : Type(0)

T = forall. xk
G = ... x:T ...
---------------------------------
G |- dependent(x) : Dependent(xk)


TYPE EQUALITY:  G |- t = t'

G |- t = t

G = ... x:k = t' ...
--------------------
G |- x = t'

G = ... x(x1:k1, ..., xn:kn):k = t' ...
G |- t1 : k1
...
G |- tn : kn
-------------------------------------------------
G |- x(t1, ..., tn) = t'[x1 <- t1, ..., xn <- tn]

G |- x = x'
G |- t1 = t1'
...
G |- tn = tn'
---------------------------------------
G |- x(t1, ..., tn) = x'(t1', ..., tn')

G |- t1 = t1'
...
G |- tn = tn'
----------------------------------------------
G |- tuple(t1, ..., tn) = tuple(t1', ..., tn')

G |- t0 = t0'
G |- t1 = t1'
...
G |- tn = tn'
--------------------------------------------------------
G |- fun(t1, ..., tn) -> t0 = tuple(t1', ..., tn') -> t0

G |- t = t'
-----------------------------------
G |- collection(t) = collection(t')


SUBTYPING:  G |- t <: t'

G |- t <: t

G |- bool <: prop

B1' <= B1
B2 <= B2'
---------------------------------
G |- int(B1, B2) <: int(B1', B2')


EXPRESSION TYPING:  G |- e : t

G |- t = t'
G |- e : t
-----------
G |- e : t'

G |- t <: t'
G |- e : t
------------
G |- e : t'

G |- t':k'
G |- e:t
------------------------------ Note: downcasts incur an SMT check; downcasts from prop to bool always fail
G |- #t'(e) : t'

inline_only not in G
G = ... local x:t ...
local in {const ghost, mutable ghost}
----------------------------------------
G |- x : t

G = ... inline x:t ...
----------------------------------------
G |- x : t

inline_only not in G
G = ... IO operand x:xo ...
G |- operand xo : t includes ...
--------------------------------
G |- x : t

G = ... state x:t ...
---------------------
G |- x : t

T = forall a1:Type(0) ... an:Type(0). t
G = ... x:T ...
G |- t1 : Type(0)
...
G |- tn : Type(0)
---------------------------------------
G |- x : t[a1 <- t1, ..., an <- tn]

T = forall a1:Type(0) ... an:Type(0). (x1:t1', ..., xm:tm') -> t (requires e_req) (ensures e_ens)
G = ... x:T ...
G |- t1 : Type(0)
...
G |- tn : Type(0)
G |- e1 : t1'[a1 <- t1, ..., an <- tn]
...
G |- em : tm'[a1 <- t1, ..., an <- tn]
------------------------------------------------ Note: if e_req isn't True, then it is checked by the SMT solver
G |- x(e1, ..., en) : t[a1 <- t1, ..., an <- tn]

G |- e0 : fun(t1, ..., tn) -> t
G |- e1 : t1
...
G |- en : tn
-------------------------------
G |- e0(e1, ..., en) : t

//TODO: this is not yet implemented:
//G = ... x:Dependent(xk) ...
//---------------------------
//G |- x : xk

G |- i : int(i, i)

G |- true : bool

G |- false : bool

G |- "...string-literal..." : string

G |- e : t
---------------
G |- old(e) : t

G |- e : t
G |- e' : state
-------------------
G |- old[e'](e) : t

G |- t : Type(0)
G |- e1 : t
...
G |- en : t
--------------------------------------------
G |- collection(e1, ..., en) : collection(t)

G |- tuple(t1, ..., tn) : Type(0)
G |- e1 : t1
...
G |- en : tn
--------------------------------------------
G |- tuple(e1, ..., en) : tuple(t1, ..., tn)

G |- e : int(B1, B2)
-------------------------
G |- (-e) : int(-B2, -B1)

G |- e1 : int(B1, B1')
G |- e2 : int(B2, B2')
(op in {+, -, *}) OR (op in {/} AND ((B2 > 0) OR (B2' < 0)))
S = {B1 op B2, B1' op B2, B1 op B2', B1' op B2'}
------------------------------------------------------------ Note: (-inf + inf) is arbitrary and 0 * inf = 0 * -inf = 0
G |- e1 op e2 : int(min(S), max(S))

G |- e1 : int(B1, B1')
G |- e2 : int(B2, B2')
(B2 > 0) OR (B2' < 0)
S = {abs(B2), abs(B2')}
---------------------------------
G |- e1 % e2 : int(0, max(S) - 1)

G |- e1 : int(B1, B1')
G |- e2 : int(B2, B2')
----------------------
G |- e1 icmp e2 : bool

G |- e1 : t
G |- e2 : t
------------------ Note: this may require an SMT check that t supports decidable equality
G |- e = e : bool
G |- e <> e : bool

G |- e1 : t
G |- e2 : t
------------------
G |- e == e : prop
G |- e != e : prop

G |- e : bool
--------------
G |- !e : bool

t in {bool, prop}
G |- e : t
----------------- Note: ! is overloaded for bool and prop
G |- !e : t

t in {bool, prop}
G |- e1 : t
G |- e2 : t
------------------ Note: && and || are overloaded for bool and prop
G |- e1 bop e2 : t

G |- e1 : prop
G |- e2 : prop
---------------------
G |- e1 Bop e2 : prop

G |- e0 : bool
G |- e1 : t
G |- e2 : t
--------------------------------
G |- (if e0 then e1 else e2) : t

x is not a local variable in G
G |- e1 : t1
G, const ghost x:t1 |- e2 : t2
-------------------------------
G |- (let x:t1 = e1 in e2) : t2

bind in {forall, exists}
x1...xn are distinct and are not local variables in G
G' = G, const ghost x1:t1, ..., const ghost xn:tn
triggers = {e11, ..., e1j} ... {em1, ..., emk}
G' |- e11 : t11 ... G' |- e1j : t1j
...
G' |- em1 : tm1 ... G' |- emk : tmk
G' |- e : prop
-----------------------------------------------------
G |- (bind x1:t1, ..., xn:tn triggers :: e) : prop

G |- fun(t1, ..., tn) -> t : Type(0)
x1...xn are distinct and are not local variables in G
G' = G, const ghost x1:t1, ..., const ghost xn:tn
G' |- e : t
------------------------------------------------------------
G |- (lambda x1:t1, ..., xn:tn :: e) : fun(t1, ..., tn) -> t


OPERAND INCLUSION:  G |- operand x : t includes opr_type

G = ... (operand x:t = ...opr_type...) ...
------------------------------------------
G |- operand x : t includes opr_type

G = ... (operand x:t = ...) ...
-------------------------------
G |- operand x : t includes x

G |- operand x : t includes x'
G |- operand x' : t' includes opr_type
--------------------------------------
G |- operand x : t includes opr_type


OPERAND TYPING:  G |- param e : t

G |- e : t
----------------
G |- ghost e : t

G, inline_only |- e : t
-----------------------
G |- inline e : t

G |- operand xo : t includes const
G, inline_only |- e : t
---------------------------------- constants (immediates)
G |- in operand e : xo

G = ... IO operand x:xo ...
G |- operand xo' : to includes xo
If IO = in then IO' = in
---------------------------------
G |- IO' operand x : xo'

G = ... state xs:ts ...
G |- operand xo : to includes IO xs
If IO = in then IO' = in
-----------------------------------
G |- IO' operand xs : xo

G = ... operand xP(..., param xp:tp, ...):to ...
For each ea:
  G |- param ea : tp
G |- operand xo : to includes xP
------------------------------------------------
G |- IO operand xP(..., ea, ...) : xo


STATEMENT TYPING:  G |- s : G'

P = (..., param xp:tp, ...) ->
    (..., ghost xg:tg, ...)
    (reads ...xr...) (modifies ...xm...) (requires er) (ensures ee)
G = ... x:P ...
For each ea:
  G |- param ea : tp
All variables in ...dst... are distinct
For each dst:
  If dst = xd:
    G = ... mutable ghost xd:td ...
    G |- td <: tg
  If dst = let xd:td:
    xd is not a local variable in G
    G |- td <: tg
G' = G, const xd1:td1, ... const xdj:tdj for each let xdi:tdi in ...dst...
--------------------------------------------------------------------------
G |- ..., dst, ... := x(..., ea, ...) : G'

(There are more statements, but procedure call is the most important.)