Merge pull request #602 from LPCIC/ppgoal

API to print a goal

Author: gares

Changelog.md

@@ -1,5 +1,10 @@
 # Changelog
 
+## UNRELEASED
+
+### API
+- New `coq.goal->pp`
+
 ## [2.0.2] - 01/02/2024
 
 Requires Elpi 1.18.2 and Coq 8.19.

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} }.
 
 }}.