Syntax for Return Types

[DavePearce]

Currently, there is a distinction between the syntax for parameter and return types which is inconsistent. Specifically, function parameters are represented as instances WhileyFile.Parameter, whilst function returns are represented as a single instance of TypePattern.

This inconsistency does cause some surprising issues:

• During verification condition generation, we have to carefully switch between the environment for a body and that of the postcondition.
• A single instance of RegisterDeclarations is not sufficient for all declared variables in a function, as it cannot include the return value.
• On the other hand, there are some neat things you can do with the type pattern in terms of post-conditions.

Two examples related to the latter:

function f() -> { int x, int y }
ensures x > y:
    ...

(this is fine)

function f({int x, int y}) -> int
requires x > y:
    ...

(this is not fine).

Furthermore, I think it would be nice to be able to write this:

function f{int x, int y} -> int
requires x > y:
    ...

Which describes a function with named parameter values.

[DavePearce]

There is some connection with #480 here.

[DavePearce]

Resolved as part of #537