OcamlP4 is unsupported on newer versions of ocaml

[jpdoyle]

I updated my system, which installed ocaml v4.10.0, which no longer supports ocamlp4. It looks like the alternative recommendation is PPX, but automatic translation with https://github.com/janestreet/camlp4-to-ppx throws up some parsing errors. I'm not familiar enough with camp4 or ppx to confidently do the translation by hand.

[jpdoyle]

I think the actual issue is an ocaml packaging problem on my OS, but leaving this issue open since camlp4 may fully lose support at any moment

[btj]

VeriFast currently uses Camlp4 to translate the streams notation used in parser.ml.

Note that ppx is a very different approach to "preprocessing". In particular, ppx plugins transform the OCaml AST, so the input is first parsed by the regular OCaml parser. Therefore, ppx cannot be used to support the streams notation.

My understanding is that we will get in trouble only if we ever want to use post-OCaml 4.08 syntax. At that point, the obvious next thing to try would be to switch to Camlp5.

If we ever want to stop depending on OCaml's -pp support, I guess we'll have to update parser.ml to use a different notation. It's not immediately clear to me that there is a straightforward ppx-based alternative.

[btj]

https://discuss.ocaml.org/t/the-end-of-camlp4

[btj]

Stream parser syntax: https://caml.inria.fr/pub/docs/tutorial-camlp4/tutorial002.html

ppx:

• https://caml.inria.fr/pub/docs/manual-ocaml/attributes.html
• https://caml.inria.fr/pub/docs/manual-ocaml/extensionnodes.html
• https://caml.inria.fr/pub/docs/manual-ocaml/compilerlibref/Ast_mapper.html
• https://ppxlib.readthedocs.io/en/latest/

Some background info on ppx:

• Proposal: parsetree rewriters ocaml/ocaml#5634
• https://web.archive.org/web/20210104212805/https://www.lexifi.com/ocaml/syntax-extensions-without-camlp4/
• https://web.archive.org/web/20210104213515/https://www.lexifi.com/ocaml/syntax-extensions-without-camlp4-lets-do-it/

[btj]

Consider the following code using stream parser syntax:

type tok = If | Then | Else | Let | In | Equal | Ident of int
let rec expr =
  parser
    [< 'If; x = expr; 'Then; y = expr; 'Else; z = expr >] -> "if"
  | [< 'Let; 'Ident x; 'Equal; x = expr; 'In; y = expr >] -> "let"

Camlp4 translates it into something like

let expect s f = try let x = f (Stream.peek s) in Stream.junk s; x with Match_failure _ -> raise (Stream.Error "Parse error")
type tok = If | Then | Else | Let | In | Equal | Ident of int
let rec expr =
  fun s ->
  match Stream.peek s with
    If -> Stream.junk s;
    let x = expr s in
    let () = expect s (fun Then -> ()) in
    let y = expr s in
    let () = expect s (fun Else -> ()) in
    let z = expr s in
    "if"
  | Let -> Stream.junk s;
    let x = expect (fun (Ident x) -> x) in
    let () = expect (fun Equal -> ()) in
    let x = expr s in
    let () = expect (fun In -> ()) in
    let y = expr s in
    "let"
  | _ -> raise Stream.Failure

The stream parser syntax can be approximated using OCaml's extension nodes syntax as follows:

let rec expr =
  function%parser
    [ If; [%let x = expr]; Then; [%let y = expr]; Else; [%let z = expr] ] -> "if"
  | [ Let; Ident x; Equal; [%let x = expr]; In; [%let y = expr] ] -> "let"

[btj]

@jeremiedimino pointed out to me that the following also works:

let rec expr =
  function%parser
    [ If; expr as x; Then; expr as y; Else; expr as z ] -> "if"
  | [ Let; Ident x; Equal; expr as x; In; expr as y ] -> "let"

Very tolerable indeed!

Note: the E as x syntax does not work if E is not just a simple function name. In those cases, we still need to use the clunkier [%let x = E] syntax.