Adrian Dapprich (Feb 24 2021 at 13:05): 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));;
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?)
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?
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.
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.
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.
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.
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.
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?
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.
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
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
Adrian Dapprich (Feb 24 2021 at 13:57):ok, thanks Pierre!
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.
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
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
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
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: Jun 09 2023 at 07:01 UTC