Update ppx-elpi to work with current Elpi API and construct encoding of OCaml AST using it

[kiranandcode]

Hi @gares ! Following up from our discussion earlier, I've now managed to update your original implementation of ppx to the point where it now works with the current branch.

Certain tests fail, for reasons that I'm not fully sure about, but the produced code does compile at least.

This pull request is likely not in a stage to be merged, hence why I've left it as a draft, but I think it serves as a good point to discuss the implementation.

[kiranandcode]

A couple of implementation details that I was confused about while updating your ppx:

• Builtin.char --- the original ppx made reference to this, but the current version of Elpi no longer has any such built in data type. To make the implementation work, I constructed a value of type char Conversion.t by using Builtin.string but I'm not sure if this is the right strategy: https://github.com/Gopiandcode/elpi/blob/80389d558236a4fc4844dd6bc04da25079753c34/src/builtin.ml#L239

  let char : char Conversion.t =  {
  ty = TyName "char";
  pp_doc = (fun fmt () -> Format.fprintf fmt "Char values: single character strings");
  pp = (fun fmt b -> Format.fprintf fmt "%c" b);
  embed = (fun ~depth (st: State.t) (c: char) -> BuiltInData.string.embed ~depth st (String.make 1 c));
  readback = (fun ~depth st term  ->
      let st,name,goals = BuiltInData.string.readback ~depth st term in
      st,name.[0],goals
    );
  }
  

• Bindings of elpi_embed_<ty>, elpi_readback_<ty> and <ty>: <ty> Conversion.t --- in your original ppx, the generated code emits three let bindings for each of these types of functions. I have updated the ppx so it generates a single mutually recursive value binding for all three:

     [pstr_value Recursive (
      List.map (fun x -> x.ty_embed) non_opaque_extra @
      List.map (fun x -> x.ty_readback) non_opaque_extra @
      List.concat_map (fun x -> x.ty_conversion) non_opaque_extra
    )]
  

  The reason for this being that as the Elpi.API.PPX.embed_<list|option|...> combinators no longer exist, sometimes the embed function will need access to a Conversion.t value.

• Additional hypothesis and constraints parameters to embed and readback functions --- the original ppx would emit two additional parameters for embed and readback functions (typically named elpi__hyps and elpy_constraints):

         let elpi__state, [%p pvar px], [%p pvar y] =
       [%e t] ~depth: elpi__depth elpi__hyps elpi__constraints elpi__state [%e ex] in
     [%e embed_k (module B) c all_kargs all_tmp xs ys ts (n+1)]]
  

To make things typecheck, I removed these. I am not sure if this is because the API has changed, or whether I'm doing something wrong and changing the embedding.

Finally, I haven't updated the mapper and traversal code to do something smarter than generating string literals. I guess I can add this in once I've confirmed what I've done so far makes sense.

[gares]

Wow! Amazing!

I won't have time to look into this carefully before Tuesday, but I'm sincerely bluffed and looking forward to look at the code.

[gares]

Builtin.char

The way for creating this conversion with the current API would be https://github.com/LPCIC/elpi/blob/e8b50c786b99bfe7383ef126134babb014f3c5cc/src/API.mli#L386 but I then guess one should declare it in builtins (as for string, int, ...) and finally provide a couple APIs to link chars to strings. I frankly don't recall what I had to add chars, possibly just because ocaml has it.

[gares]

The reason for this being that as the Elpi.API.PPX.embed_<list|option|...> combinators no longer exist, sometimes the embed function will need access to a Conversion.t value.

I was hitting the value-restriction, I think this is why I added the separate combinators. If you are not, I'm all for any other solution based on full conversions.

[gares]

To make things typecheck, I removed these. I am not sure if this is because the API has changed, or whether I'm doing something wrong and changing the embedding.

These are still there in the ContextualConversion.t type. So I guess you did target Conversion.t after all, which is fine as a start, but won't allow some nice APIs depending on the context (the binders of the data crossed before calling the API).

I'll look into the code ASAP.

[gares]

Forgot to put @thierry-martinez in the loop, he might be interested as well.

[kiranandcode]

Okay, looking at the failing tests, I realise my updates are still missing a few details --- the generated code for the OCaml ast compiles, but ppx_elpi is still fairly incomplete and fails on the test-cases.

I'm currently working on gradually fixing the failing tests one by one. Will push my changes as I progress; hopefully once the tests compile again, ppx_elpi will be roughly complete.

[kiranandcode]

Also, there's some part of the prelude I think I provide that is ill-formed and causes elpi to reject the whole string-- maybe the root cause is the incorrect choice of constant for the mapper src:

https://github.com/LPCIC/elpi/pull/179/files#diff-997f924465628fc1a9429f582be50b7d172f7ffd5c856aff29659c19bf26057aR7

[gares]

I'm sorry I had no time to look into this last week. If we agree on a no-rebase rule, I may push comment or easy fixes on your branch directly. Would that be fine for you?

[kiranandcode]

Yes, sure, I'd be more than happy to await your changes.

[gares]

@Gopiandcode I have to suspend my activity on this branch. The status is the following:

• the old tests kind of pass, even if I had no time to dune promote the generated code and actually look at it
• I had to change the APIs, I tried to minimize the change, but I could not keep backward compatibility
• the PPX always generates ContextualConversion.t even if the data has no binders. I guess this is fine for now.

The first order part seems OK. The ppx for ocaml now works as before, see dune runtest ocaml-elpi/tests. Of course there are no declared binders in the AST. It is very rough, but it is a start.

The HO part (when one declares binders and context) needs more work, since:

• there was an odd choice of mine to hide the context inside the State.t, while I think it would make more sense to have operations like push to be part of the class which represents the context. To be understood
• I changed the datatype of query to hold contextual data, but the given context is not embedded (and there is no code for embedding it), so the API is very misleading.

[gares]

@manmatteo I just rebased this branch. Unfortunately it still does not suppord mutual datatypes, and looking at why3, terms, patterns and match_branches are mutual. So I need to fix that first. The I think we can have a chat and see how to apply this to why3

[manmatteo]

Generating via ppx would be great! In addition to the mutual recursion, there's also the fact that in Why3 patterns bind variables in the branch but no explicit binder is present, so I had to add one. I'm not sure if there's some extra care needed to make the ppx aware of this.

[gares]

Thanks for the heads up.

The ppx lets you override the code for each constructor, I guess we need to override the one for pattern matching branches, synthesize the binders, and call the generated code on the "fake" term. Similarly, on readback, we have to override the generated code, eat up the binders, and pass the ball to the generated code.