Stream: Elpi users & devs

Topic: Coq-ELPI API

Philip (Aug 30 2023 at 10:54):

Do I understand correctly, that there is no OCaml API for Coq-ELPI? Context: I am looking for a way to add a built-in predicate to a Coq-ELPI session, that will in part have to execute OCaml code and query ELPI (which includes a coq.env.add-indt invocation).

Enzo Crance (Aug 30 2023 at 11:28):

Hello Philip. IIUC if you want to add a built-in predicate to Coq-Elpi, the only solution available for now is to edit the coq_elpi_builtins.ml file to add your predicates, then recompile the package.

Enrico Tassi (Aug 30 2023 at 11:31):

There are two things:

• to add a builtin to coq-elpi you have, for now, to clone the repo and add your code here: https://github.com/LPCIC/coq-elpi/blob/87c64ec400b5833ab1e5c07b9a8ea41d60cab31d/src/coq_elpi_builtins.ml#L1253 (there are plenty of examples). You need to recompile coq-elpi for that to work.
• there is no streamlined API to run coq-elpi, but you can do it, see: https://github.com/LPCIC/coq-elpi/tree/master/apps/coercion (a coq plugin using coq-elpi )

Enrico Tassi (Aug 30 2023 at 11:36):

Just to be sure, your main driver is a program written in what? ;-)

Philip (Aug 30 2023 at 11:55):

It is written in OCaml, and involves Disk-IO and some parsing, which seems to be something I'd rather not do in ELPI.

Philip (Aug 30 2023 at 11:55):

The coercion example seems to me something like what I am looking for, I'll have to study it in more detail. Thanks!

Philip (Aug 30 2023 at 11:57):

Enzo Crance said:

Hello Philip. IIUC if you want to add a built-in predicate to Coq-Elpi, the only solution available for now is to edit the coq_elpi_builtins.ml file to add your predicates, then recompile the package.

That would be regrettable, since we would like to publish the tool (FWIW, the context is that we trying to automatically translate the specification logic of Abella into something that can be used with Coq), in a way that wouldn't be too cumbersome to setup and use.

Enrico Tassi (Aug 30 2023 at 11:58):

Note that initializing Coq (as a library) is not super trivial either. So maybe it is easier to have your main written in Coq-Elpi, and then coqc yourfile.v as a way to set up Coq and run your elpi code.

Enrico Tassi (Aug 30 2023 at 12:00):

@Philip maybe you want to explain your intended workflow so that I can suggest what is easier to do.

Philip (Aug 30 2023 at 12:08):

The intended workflow will sort of depend on what is feasible and practicable. My current ideal would be to just have to write

FromAbella "stlc".

Behind the scenes, it will be necessary for some Ocaml code to parse and process a few files, then (somehow) pass this data into an Elpi query, which generates the proper types. My idea was to write a Coq Plugin, that could access the Coq-ELPI handler (elpi from API.ml), and dispatch a constructed query to trigger the indented side-effect. Another approach, but that might change the way the tool is used, would be to extend ELPI with a built-in predicate that does the parsing and processing, and "outputs" the necessary information.

Hope this doesn't sound too vague.

Enrico Tassi (Aug 30 2023 at 12:30):

I believe the latter would be much simpler, even if initially you would need to fork coq-elpi to add a builtin.
Note that for a quick prototype you can even use the system API.

From elpi Require Import elpi.

Elpi Command FromAbella.
Elpi Accumulate lp:{{

main [str X] :- % here you could call you existing ocaml code to generate X.elpi
  Cmd is "echo 'p \"" ^ X ^ "\".' > tests/" ^ X ^ ".elpi",
  system Cmd _.

}}.
Elpi Export FromAbella.

FromAbella "stlc".

From elpi.tests Extra Dependency "stlc.elpi" as stlc.

Elpi Command test.
Elpi Accumulate File stlc.
Elpi Accumulate lp:{{
  main _ :- p X, coq.say X.
}}.
Elpi Typecheck.
Elpi Export test.

test. (* prints stlc *)

Enrico Tassi (Aug 30 2023 at 12:31):

This snippets make FromAbella "stlc". generate a file stlc.elpi containing p "stlc"., then the test command loads and queries it.

Enrico Tassi (Aug 30 2023 at 12:33):

This "hack" does not require to patch coq-elpi, but I'm happy to get a PR for any new builtin which makes sense in general.
Otherwise, at some point, I'll let builtins to be extensible, but is not a priority of mine, so you will have to wait.

Enrico Tassi (Aug 30 2023 at 12:35):

If you want to test the code above, you need to pass Coq options like -R tests/ elpi.tests so that tests/X.elpi is found by the extra dependency directive.

Enrico Tassi (Aug 30 2023 at 12:37):

In any case feel free to ask for help, I'd love to have a bridge to Abella in Coq.

Philip (Aug 30 2023 at 13:00):

This looks like a great starting point (the system simplifies the problem significantly), thank you very much!

Last updated: Oct 13 2024 at 01:02 UTC