In the current state, specification of a gospel value or a gospel type are in an attribute of an attribute. But this is written with two successive special coments. Thus, the source preprocessor has to manipulate two successive tokens to make one attribute.
I propose to let go of the successive special comments and write the logical declaration and its optional specifications in one. As specification clauses begin with a keyword, this should be possible to parse.
Then, instead of
(*@ type t *)
(*@ ephemeral *)
(*@ function f (x : integer) : bool *)
(*@ ensures true *)
(*@ function g (x : integer) : integer = x + 2 *)
(*@ requires true *)
we would write
(*@ type t
ephemeral *)
(*@ function f (x : integer) : bool
ensures true *)
(*@ function g (x : integer) : integer = x + 2
requires true *)
which will be turned by the source preprocessor in one floating attribute and then parsed by the gospel (attribute) parser into the corresponding items of the Uast.
In the current state, specification of a gospel value or a gospel type are in an attribute of an attribute. But this is written with two successive special coments. Thus, the source preprocessor has to manipulate two successive tokens to make one attribute.
I propose to let go of the successive special comments and write the logical declaration and its optional specifications in one. As specification clauses begin with a keyword, this should be possible to parse.
Then, instead of
we would write
which will be turned by the source preprocessor in one floating attribute and then parsed by the gospel (attribute) parser into the corresponding items of the Uast.