Merge branch 'master' into attlabel

Author: gares

Changelog.md

@@ -5,6 +5,7 @@
 ### API
 - New `coq.parse-attributes` support for the `attlabel` specification,
   see `coq-lib-common.elpi` for its documentation.
+- New `coq.goal->pp`
 
 ## [2.0.2] - 01/02/2024
 

README.md

@@ -181,14 +181,13 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
 - `Elpi Program <qname> <code>` lower level primitive letting one crate a
   command/tactic with a custom preamble `<code>`.
-
-- `Elpi Accumulate [<qname>] [<code>|File <filename> From <loadpath>|Db <dbname>]`
+- `From some.load.path Extra Dependency "filename" as <fname>`.
+- `Elpi Accumulate [<qname>] [<code>|File <fname>|Db <dbname>]`
   adds code to the current program (or `<qname>` if specified).
   The code can be verbatim, from a file or a Db.
   It understands the `#[skip="rex"]` and `#[only="rex"]` which make the command
   a no op if the Coq version is matched (or not) by the given regular expression.
-  File names are relative to the directory mapped to `<loadpath>`; if more than
-  one such directory exists, the `<filename>` must exists only once.
+  File names `<fname>` must have been previously declared with the above command.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
 - `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
   specified).

coq-builtin.elpi

@@ -1691,6 +1691,16 @@ external pred coq.term->string i:term, o:string.
 % - @holes! (default: false, prints evars as _)
 external pred coq.term->pp i:term, o:coq.pp.
 
+% [coq.goal->pp G B] prints a goal G to a pp.t B using Coq's pretty
+% printer"
+% Supported attributes:
+% - @ppall! (default: false, prints all details)
+% - @ppmost! (default: false, prints most details)
+% - @pplevel! (default: _, prints parentheses to reach that level, 200 =
+% off)
+% - @holes! (default: false, prints evars as _)
+external pred coq.goal->pp i:goal, o:coq.pp.
+
 % -- Extra Dependencies -----------------------------------------------
 
 % [coq.extra-dep Identifier FileName] Resolve the file name of an extra

src/coq_elpi_builtins.ml

@@ -3830,6 +3830,30 @@ Supported attributes:
      state, !: s, [])),
   DocAbove);
 
+  MLCode(Pred("coq.goal->pp",
+    CIn(goal,"G",
+    Out(ppboxes, "B",
+    Full(raw_ctx, {|prints a goal G to a pp.t B using Coq's pretty printer"
+Supported attributes:
+- @ppall! (default: false, prints all details)
+- @ppmost! (default: false, prints most details)
+- @pplevel! (default: _, prints parentheses to reach that level, 200 = off)
+- @holes! (default: false, prints evars as _)|}))),
+  (fun (proof_context,evar,args) _ ~depth _ _ state ->
+     let sigma = get_sigma state in
+     let pr_named_context_of env sigma =
+      let make_decl_list env d pps = Printer.pr_named_decl env sigma d :: pps in
+      let psl = List.rev (Environ.fold_named_context make_decl_list env ~init:[]) in
+      Pp.(v 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)) in
+     let s = Pp.(repr @@ with_pp_options proof_context.options.pp (fun () ->
+        v 0 @@ 
+        pr_named_context_of proof_context.env sigma ++ cut () ++
+        str "======================" ++ cut () ++
+        Printer.pr_econstr_env proof_context.env sigma
+          Evd.(evar_concl @@ find_undefined sigma evar))) in
+     state, !: s, [])),
+  DocAbove);
+
   LPDoc "-- Extra Dependencies -----------------------------------------------";
 
   MLCode(Pred("coq.extra-dep",

tests/test_tactic.v

@@ -26,12 +26,10 @@ Elpi Print foobar.
 Elpi Tactic print_goal.
 Elpi Accumulate lp:{{
 
-  solve (goal L _ T _ As as G) [seal G] :-
+  solve (goal _ _ _ _ _ as G) [seal G] :-
     print_constraints,
-    coq.say "Goal: ", coq.say As, coq.say "\n",
-    coq.say L,
-    coq.say "------------",
-    coq.say T {coq.term->string T}.
+    coq.say "Goal: \n",
+    coq.say {coq.pp->string {coq.goal->pp G} }.
 
 }}.