pps: support for spec comments preceding specified items

[fpottier]

The following .mli file gives rise to Error: OCaml syntax error:

(*@ model content: int *)
type 'a t

The error message seems incorrect: this is a valid OCaml file.

More generally, OCaml allows documentation comments to appear either before or after the object that they document. It would be good if the same was true of Gospel comments. Thus, I would expect the following to be accepted:

(**A type. *)
(*@ model content: int *)
type 'a t

Or, if we insist that Gospel comments must come after the object that they document, then perhaps this should be documented.

[pascutto]

The error message seems incorrect: this is a valid OCaml file.

To give a bit of insight, actually the result of the preprocessor is not a valid OCaml file:

[@@gospel {| a = make n x
      requires n > 0
      ensures  forall i. a(i) = x |}]
val make : int -> 'a -> 'a t

You can experiment with it using the gospel pps command.

We tried to make the preprocessor as simple as possible (because attachment is a tricky thing to do properly), but I agree it would be nice to support more layout cases. In the meantime, I've clarified that we only support comments after in #149.

[fpottier]

Thanks!

[pascutto]

@n-osborne and I just had a look at this and the reason why it's not implemented now is it would mess with the locations (which we think is not worth doing), since you would want to preprocess

(*@ a = make n x
       requires n > 0
       ensures  forall i. a(i) = x *)
val make : int -> 'a -> 'a t

into

val make : int -> 'a -> 'a t
[@@gospel {| a = make n x
      requires n > 0
      ensures  forall i. a(i) = x |}]

We could add location annotations to fix this though.

[fpottier]

I note that in Cameleer, it is really painful to have to write the specification of a function after the whole function (whose code can be long). In the end I think we will want to write the spec in front of the code in an .ml file, and consequently there will also be a desire to be allowed to write the spec in front of the declaration in an .mli file.

[pascutto]

It makes sense indeed. I'm not so sure about how Cameleer works about this (/cc @mariojppereira) but I suspect it translates them into attributes in the same location which might explain why you have to write them afterwards.

[mariojppereira]

It makes sense indeed. I'm not so sure about how Cameleer works about this (/cc @mariojppereira) but I suspect it translates them into attributes in the same location which might explain why you have to write them afterwards.

This is exactly the case.

@fpottier , are you suggesting something like the following?

  (*@ r = foo x
           ensures r = x *)
  let foo x = x

This is still possible, as I can attach the Gospel attribute (generated by the preprocessor) to the let symbol that comes afterwards.

[mariojppereira]

@n-osborne and I just had a look at this and the reason why it's not implemented now is it would mess with the locations (which we think is not worth doing), since you would want to preprocess

(*@ a = make n x
       requires n > 0
       ensures  forall i. a(i) = x *)
val make : int -> 'a -> 'a t

into

val make : int -> 'a -> 'a t
[@@gospel {| a = make n x
      requires n > 0
      ensures  forall i. a(i) = x |}]

We could add location annotations to fix this though.

I think using ## would help sorting out this issue.

[mariojppereira]

It makes sense indeed. I'm not so sure about how Cameleer works about this (/cc @mariojppereira) but I suspect it translates them into attributes in the same location which might explain why you have to write them afterwards.

This is exactly the case.

@fpottier , are you suggesting something like the following?

  (*@ r = foo x
           ensures r = x *)
  let foo x = x

This is still possible, as I can attach the Gospel attribute (generated by the preprocessor) to the let symbol that comes afterwards.

If we forget about (*@ comments, the following would be accepted by Cameleer:

  let [@gospel {| a = make n x
       requires n > 0
       ensures  forall i. a(i) = x |}]
  make n x = ...

I can make an effort inside the preprocessor to move the attribute to the next let (or and, in case of mutually-recursive functions) and use some location annotations to keep the good location values.

[fpottier]

@fpottier , are you suggesting something like the following?

Yes! Allowing the spec to appear in front of the code.

[pascutto]

We should document this in the short term, before we fix this.

[shym]

As this is now documented, I remove it from the milestone.