synthesize with elpi

[gares]

I test it using 8.14+rc1 and Elpi 1.11.2, it should work the same on 8.13 and Elpi 1.11.1, but I've no clue if it works on 8.12 + Elpi very old version...

[eponier]

No std.fold-map nor coq.reduction.lazy.norm in coq 8.12.

[eponier]

But it compiles fine with coq 8.13.

[gares]

Tomorrow I'll do fields_t/fields/construct, since there is a missing feature.
In particular deep pattern matching is not "automatic" because the compiler used by Coq is impossible to use (at the OCaml level).
So I'll write a build-match for positives < k, and then use it (it would call the continuation of the branch passing the positive number of the branch, and nest match behind the scenes...). Unless one of you wants to give it a try before... Not sure it will be fun.

[gares]

Also, questions are welcome if the code is unclear.

[eponier]

These pattern-matchings exist because we manipulate positives, if we used native ints, we would have a cascade of if instead, and thus no problem of deep pattern-matching. We could use a cascade of if in the the positive case too, not sure of the performance impact.

[gares]

I tried with natives but construct does not type check well since you dont get the substitution for free anymore

[eponier]

Indeed, it is probably better to begin with the positive case then.

[gares]

I wrote some code for fields_t and fields. It should also generate construct, since it is entangled, but I have no time for it. It should not be too hard... We can either do it together the next week I'm at the lab, or someone can try this on his own. I don't think I'll have time tomorrow or Friday.

[gares]

it looks ok, the only bug I can see is the first one mentioned here: https://lpcic.github.io/coq-elpi/tutorial_elpi_lang.html#pitfalls

[gares]

Hint: you can directly construct (global (const C)) instead of just C (or P IIRC) in the first map2, so that you don't need to map again.

Hint: std.map L (x\ coq.mk-app x [t]) L1 is slightly better, another option is to just [t|L] and in the base case std.rev.

[eponier]

A small bug that I've just discovered: as we use the name of the type in the name of the generated functions, there is an error if we give an absolute path, e.g. Elpi tag List.list..

[gares]

The "clean" fix: https://github.com/LPCIC/coq-elpi/blob/master/elpi-builtin.elpi#L290

[gares]

hurray!

[gares]

👑