Stream: Coq devs & plugin devs

Topic: Constructing Notations in OCaml


view this post on Zulip Adrian Dapprich (Feb 24 2021 at 13:05):

Hi all, I am writing an OCaml program that uses Coq purely as a library to construct constr_exprs and print them to generate some Coq code.
At the moment I am trying to construct some CNotation nodes so that when I construct and print an equality expression I don't get (eq x y) but the familliar (x = y), and the same for function arrows.
The following works when I drop from coqtop.byte into the ocaml toplevel but in my ocaml program the print command at the end fails because because there is no special printing function defined for "_ = _" in Ppextend.specific_notation_printing_rules when I just use Coq as a library without running it.
My question is can I somehow load the Coq.Init.Logic file from OCaml so that the notation + their printing functions are defined? (I guess I could also rewrite my OCaml program to be a proper Coq plugin and call it from Coq so that the whole Prelude is available in the environment)

let ref_ s = Constrexpr_ops.mkRefC (Libnames.qualid_of_string s);;

let n = CAst.make (Constrexpr.CNotation (Some (Constrexpr.LastLonelyNotation), (Constrexpr.InConstrEntry, "_ = _"), ([ref_ "abc"; ref_ "def"], [], [], [])));;
let env = Global.env ();;
let sigma = Evd.from_env env;;
print_endline (Pp.string_of_ppcmds (Ppconstr.pr_lconstr_expr env sigma n));;

view this post on Zulip Adrian Dapprich (Feb 24 2021 at 13:11):

I also thought I could maybe define my own notation from ocaml like this

let eqc = Constrexpr_ops.mkAppC (ref_ "eq", [ ref_ "x"; ref_ "y" ]);;
Metasyntax.add_notation ~local:false None (Global.env()) eqc (CAst.make "x ~~ y", [Vernacexpr.SetLevel 70]) None;;

but add_notation apparently wants to globalize "eq" which fails because my environment is empty so this really leads me to the same question if I can interpret the whole Logic.v from ocaml I guess, since I don't want to define everything by hand.
Or is there a better way to go about this from the beginning (like using SerAPI?)

view this post on Zulip Pierre-Marie Pédrot (Feb 24 2021 at 13:17):

What are you ultimately doing with those terms? Just printing them? Or you want to provide them to Coq for further use?

view this post on Zulip Pierre-Marie Pédrot (Feb 24 2021 at 13:18):

As a general rule, using constr_expr for anything else than parsing is probably a bad idea.

view this post on Zulip Enrico Tassi (Feb 24 2021 at 13:25):

Using Coq as a pretty printer kind of works if you have actual Coq terms (in a meaningful environment). You then can call the code to print them and notations are applied for you.

Even if Coq is packaged as a set of libraries, I advise assuming they cannot work "standalone". Serapi won't change that.

view this post on Zulip Adrian Dapprich (Feb 24 2021 at 13:38):

Ultimately I'm just printing them, the whole thing was just about using the coq pretty printer to print previously constructed terms.

view this post on Zulip Pierre-Marie Pédrot (Feb 24 2021 at 13:41):

If your terms are simple, I'd tend to believe that implementing your own pretty-printer is likely the simplest solution.

view this post on Zulip Pierre-Marie Pédrot (Feb 24 2021 at 13:41):

Otherwise you'll have to plug into a Coq session and your problems will just start.

view this post on Zulip Adrian Dapprich (Feb 24 2021 at 13:45):

Yes, standalone seems harder than necessary so I might just switch to a Coq plugin because theoretically the program would make sense if I trigger it from Coq as a command. Why is it so hard to use a Coq session and is there documentation about that in doc/ somewhere?

view this post on Zulip Pierre-Marie Pédrot (Feb 24 2021 at 13:52):

There is no real doc, but the problem is that Coq maintains a big global state.

view this post on Zulip Pierre-Marie Pédrot (Feb 24 2021 at 13:52):

If you want a standalone program you have to emulate all the handling of that state normally done by the Coq program

view this post on Zulip Pierre-Marie Pédrot (Feb 24 2021 at 13:53):

if you want to have a command that lives in a Coq document, this will be transparently handled by the surrounding Coq instance

view this post on Zulip Adrian Dapprich (Feb 24 2021 at 13:57):

ok, thanks Pierre!

view this post on Zulip Enrico Tassi (Feb 24 2021 at 14:06):

You could give coq-elpi a try, I've recently added support for the coq.pp data type, and you have coq.term->pp to print terms and use them inside larger formatting expressions.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 24 2021 at 14:55):

You can also use SerAPI, it should be able to print the terms just fine given them as seralized inputs

view this post on Zulip Emilio Jesús Gallego Arias (Feb 24 2021 at 14:56):

Or you could start from SerAPI standalone code, it is fairly reasonable to use as a basis for your own standalone Coq

view this post on Zulip Emilio Jesús Gallego Arias (Feb 24 2021 at 14:56):

Handling the Coq state is fairly simple, once you know it, so I woudln't be too scared of that

view this post on Zulip Adrian Dapprich (Mar 01 2021 at 11:49):

Thanks for the pointers, but I wanted to do it purely using Coq as library, without further dependencies. In the end it was possible to hack around the restriction that eq was not defined by declaring a dummy notation like this Notation "x = y" := (x y) (probably also even simpler versions work) since during code generation I don't care what Coq thinks the notation means, just how it is printed.


Last updated: Oct 16 2021 at 02:03 UTC