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?)
What are you ultimately doing with those terms? Just printing them? Or you want to provide them to Coq for further use?
As a general rule, using constr_expr for anything else than parsing is probably a bad idea.
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.
Ultimately I'm just printing them, the whole thing was just about using the coq pretty printer to print previously constructed terms.
If your terms are simple, I'd tend to believe that implementing your own pretty-printer is likely the simplest solution.
Otherwise you'll have to plug into a Coq session and your problems will just start.
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?
There is no real doc, but the problem is that Coq maintains a big global state.
If you want a standalone program you have to emulate all the handling of that state normally done by the Coq program
if you want to have a command that lives in a Coq document, this will be transparently handled by the surrounding Coq instance
ok, thanks Pierre!
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.
You can also use SerAPI, it should be able to print the terms just fine given them as seralized inputs
Or you could start from SerAPI standalone code, it is fairly reasonable to use as a basis for your own standalone Coq
Handling the Coq state is fairly simple, once you know it, so I woudln't be too scared of that
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