Merge PR #8688: Generalizing the various evar_map printers in Termops over an environment

9 files changed, 64 insertions, 62 deletions

diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
new file mode 100644
index 0000000000..81ed91f52b
--- /dev/null
+++ b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then
+
+    Elpi_CI_REF=master+generalized-evar-printers-pr8688
+    Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 44d44ccc4b..fd08f9ffe8 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -168,8 +168,8 @@ let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(Termops.pr_metaset metas)
-let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd)
-let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd)
+let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) (Global.env ()) evd)
+let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None (Global.env ()) evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
 let ppexistentialset evars =
@@ -180,14 +180,14 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 let ppgoal g = pp(Printer.pr_goal g)
-let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g))
+let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Refiner.project g))
 let pphintdb db = pp(envpp Hints.pr_hint_db_env db)
 let ppproofview p =
   let gls,sigma = Proofview.proofview p in
-  pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma)
+  pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) (Global.env ()) sigma)
 
 let ppopenconstr (x : Evd.open_constr) =
-  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c)
+  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) (Global.env ()) evd ++ envpp pr_econstr_env c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 5e220fd8f1..f720e5195d 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -104,12 +104,7 @@ let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c)
 let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c)
 let term_printer = ref debug_print_constr_env
 
-let print_constr_env env sigma t = !term_printer env sigma t
-let print_constr t =
-  let env = Global.env () in
-  let evd = Evd.from_env env in
-  !term_printer env evd t
-
+let print_constr_env env sigma t = !term_printer (env:env) sigma (t:Evd.econstr)
 let set_print_constr f = term_printer := f
 
 module EvMap = Evar.Map
@@ -164,10 +159,10 @@ let protect f x =
   try f x
   with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
 
-let print_kconstr a =
-  protect (fun c -> print_constr c) a
+let print_kconstr env sigma a =
+  protect (fun c -> print_constr_env env sigma c) a
 
-let pr_meta_map evd =
+let pr_meta_map env sigma =
   let open Evd in
   let print_constr = print_kconstr in
   let pr_name = function
@@ -177,25 +172,25 @@ let pr_meta_map evd =
     | (mv,Cltyp (na,b)) ->
       	hov 0
 	  (pr_meta mv ++ pr_name na ++ str " : " ++
-           print_constr b.rebus ++ fnl ())
+           print_constr env sigma b.rebus ++ fnl ())
     | (mv,Clval(na,(b,s),t)) ->
       	hov 0
 	  (pr_meta mv ++ pr_name na ++ str " := " ++
-           print_constr b.rebus ++
-	   str " : " ++ print_constr t.rebus ++
+           print_constr env sigma b.rebus ++
+           str " : " ++ print_constr env sigma t.rebus ++
 	   spc () ++ pr_instance_status s ++ fnl ())
   in
-  prlist pr_meta_binding (meta_list evd)
+  prlist pr_meta_binding (meta_list sigma)
 
-let pr_decl (decl,ok) =
+let pr_decl env sigma (decl,ok) =
   let open NamedDecl in
   let print_constr = print_kconstr in
   match decl with
   | LocalAssum (id,_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}")
   | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++
-                           print_constr c ++ str (if ok then ")" else "}")
+                           print_constr env sigma c ++ str (if ok then ")" else "}")
 
-let pr_evar_source = function
+let pr_evar_source env sigma = function
   | Evar_kinds.NamedHole id -> Id.print id
   | Evar_kinds.QuestionMark _ -> str "underscore"
   | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
@@ -208,11 +203,11 @@ let pr_evar_source = function
       let print_constr = print_kconstr in
       let id = Option.get ido in
       str "parameter " ++ Id.print id ++ spc () ++ str "of" ++
-      spc () ++ print_constr (EConstr.of_constr @@ printable_constr_of_global c)
+      spc () ++ print_constr env sigma (EConstr.of_constr @@ printable_constr_of_global c)
   | Evar_kinds.InternalHole -> str "internal placeholder"
   | Evar_kinds.TomatchTypeParameter (ind,n) ->
       let print_constr = print_kconstr in
-      pr_nth n ++ str " argument of type " ++ print_constr (EConstr.mkInd ind)
+      pr_nth n ++ str " argument of type " ++ print_constr env sigma (EConstr.mkInd ind)
   | Evar_kinds.GoalEvar -> str "goal evar"
   | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ -> str "matching variable"
@@ -224,7 +219,7 @@ let pr_evar_source = function
      | Some Evar_kinds.Domain -> str "domain of "
      | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk
 
-let pr_evar_info evi =
+let pr_evar_info env sigma evi =
   let open Evd in
   let print_constr = print_kconstr in
   let phyps =
@@ -233,23 +228,23 @@ let pr_evar_info evi =
       | None -> List.map (fun c -> (c, true)) (evar_context evi)
       | Some filter -> List.combine (evar_context evi) filter
       in
-      prlist_with_sep spc pr_decl (List.rev decls)
+      prlist_with_sep spc (pr_decl env sigma) (List.rev decls)
     with Invalid_argument _ -> str "Ill-formed filtered context" in
-  let pty = print_constr evi.evar_concl in
+  let pty = print_constr env sigma evi.evar_concl in
   let pb =
     match evi.evar_body with
       | Evar_empty -> mt ()
-      | Evar_defined c -> spc() ++ str"=> "  ++ print_constr c
+      | Evar_defined c -> spc() ++ str"=> "  ++ print_constr env sigma c
   in
   let candidates =
     match evi.evar_body, evi.evar_candidates with
       | Evar_empty, Some l ->
            spc () ++ str "{" ++
-           prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
+           prlist_with_sep (fun () -> str "|") (print_constr env sigma) l ++ str "}"
       | _ ->
           mt ()
   in
-  let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
+  let src = str "(" ++ pr_evar_source env sigma (snd evi.evar_source) ++ str ")" in
   hov 2
     (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]" ++
        candidates ++ spc() ++ src)
@@ -304,8 +299,8 @@ let has_no_evar sigma =
   try let () = Evd.fold (fun _ _ () -> raise Exit) sigma () in true
   with Exit -> false
 
-let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
-let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l
+let pr_evd_level sigma = UState.pr_uctx_level (Evd.evar_universe_context sigma)
+let reference_of_level sigma l = UState.qualid_of_level (Evd.evar_universe_context sigma) l
 
 let pr_evar_universe_context ctx =
   let open UState in
@@ -321,12 +316,12 @@ let pr_evar_universe_context ctx =
      str "WEAK CONSTRAINTS:"++brk(0,1)++
      h 0 (UState.pr_weak prl ctx) ++ fnl ())
 
-let print_env_short env =
+let print_env_short env sigma =
   let print_constr = print_kconstr in
   let pr_rel_decl = function
     | RelDecl.LocalAssum (n,_) -> Name.print n
     | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := "
-                                  ++ print_constr (EConstr.of_constr b) ++ str ")"
+                                  ++ print_constr env sigma (EConstr.of_constr b) ++ str ")"
   in
   let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
   let nc = List.rev (named_context env) in
@@ -346,7 +341,7 @@ let pr_evar_constraints sigma pbs =
           naming/renaming. *)
       Namegen.make_all_name_different env sigma
     in
-    print_env_short env ++ spc () ++ str "|-" ++ spc () ++
+    print_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++
       protect (print_constr_env env sigma) t1 ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
@@ -355,7 +350,7 @@ let pr_evar_constraints sigma pbs =
   in
   prlist_with_sep fnl pr_evconstr pbs
 
-let pr_evar_map_gen with_univs pr_evars sigma =
+let pr_evar_map_gen with_univs pr_evars env sigma =
   let uvs = Evd.evar_universe_context sigma in
   let (_, conv_pbs) = Evd.extract_all_conv_pbs sigma in
   let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl ()
@@ -374,15 +369,15 @@ let pr_evar_map_gen with_univs pr_evars sigma =
   and metas =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
-      str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
+      str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma
   in
   evs ++ svs ++ cstrs ++ typeclasses ++ metas
 
-let pr_evar_list sigma l =
+let pr_evar_list env sigma l =
   let open Evd in
   let pr (ev, evi) =
     h 0 (Evar.print ev ++
-      str "==" ++ pr_evar_info evi ++
+      str "==" ++ pr_evar_info env sigma evi ++
       (if evi.evar_body == Evar_empty
        then str " {" ++ pr_existential_key sigma ev ++ str "}"
        else mt ()))
@@ -405,18 +400,18 @@ let to_list d =
   Evd.fold fold_undef d ();
   !l
 
-let pr_evar_by_depth depth sigma = match depth with
+let pr_evar_by_depth depth env sigma = match depth with
 | None ->
   (* Print all evars *)
-  str"EVARS:" ++ brk(0,1) ++ pr_evar_list sigma (to_list sigma) ++ fnl()
+  str"EVARS:" ++ brk(0,1) ++ pr_evar_list env sigma (to_list sigma) ++ fnl()
 | Some n ->
   (* Print closure of undefined evars *)
   str"UNDEFINED EVARS:"++
   (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
   brk(0,1)++
-  pr_evar_list sigma (evar_dependency_closure n sigma) ++ fnl()
+  pr_evar_list env sigma (evar_dependency_closure n sigma) ++ fnl()
 
-let pr_evar_by_filter filter sigma =
+let pr_evar_by_filter filter env sigma =
   let open Evd in
   let elts = Evd.fold (fun evk evi accu -> (evk, evi) :: accu) sigma [] in
   let elts = List.rev elts in
@@ -431,49 +426,49 @@ let pr_evar_by_filter filter sigma =
   let prdef =
     if List.is_empty defined then mt ()
     else str "DEFINED EVARS:" ++ brk (0, 1) ++
-      pr_evar_list sigma defined
+      pr_evar_list env sigma defined
   in
   let prundef =
     if List.is_empty undefined then mt ()
     else str "UNDEFINED EVARS:" ++ brk (0, 1) ++
-      pr_evar_list sigma undefined
+      pr_evar_list env sigma undefined
   in
   prdef ++ prundef
 
-let pr_evar_map ?(with_univs=true) depth sigma =
-  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma
+let pr_evar_map ?(with_univs=true) depth env sigma =
+  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth env sigma) env sigma
 
-let pr_evar_map_filter ?(with_univs=true) filter sigma =
-  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma
+let pr_evar_map_filter ?(with_univs=true) filter env sigma =
+  pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter env sigma) env sigma
 
 let pr_metaset metas =
   str "[" ++ pr_sequence pr_meta (Evd.Metaset.elements metas) ++ str "]"
 
 let pr_var_decl env decl =
   let open NamedDecl in
-  let evd = Evd.from_env env in
+  let sigma = Evd.from_env env in
   let pbody = match decl with
     | LocalAssum _ ->  mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let c = EConstr.of_constr c in
-        let pb = print_constr_env env evd c in
+        let pb = print_constr_env env sigma c in
 	  (str" := " ++ pb ++ cut () ) in
-  let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
+  let pt = print_constr_env env sigma (EConstr.of_constr (get_type decl)) in
   let ptyp = (str" : " ++ pt) in
     (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp))
 
 let pr_rel_decl env decl =
   let open RelDecl in
-  let evd = Evd.from_env env in
+  let sigma = Evd.from_env env in
   let pbody = match decl with
     | LocalAssum _ -> mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let c = EConstr.of_constr c in
-        let pb = print_constr_env env evd c in
+        let pb = print_constr_env env sigma c in
 	  (str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
+  let ptyp = print_constr_env env sigma (EConstr.of_constr (get_type decl)) in
     match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
       | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
diff --git a/engine/termops.mli b/engine/termops.mli
index f7b9469ae8..1054fbbc5e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -304,11 +304,11 @@ val pr_existential_key : evar_map -> Evar.t -> Pp.t
 
 val pr_evar_suggested_name : Evar.t -> evar_map -> Id.t
 
-val pr_evar_info : evar_info -> Pp.t
+val pr_evar_info : env -> evar_map -> evar_info -> Pp.t
 val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t
-val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t
+val pr_evar_map : ?with_univs:bool -> int option -> env -> evar_map -> Pp.t
 val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
-  evar_map -> Pp.t
+  env -> evar_map -> Pp.t
 val pr_metaset : Metaset.t -> Pp.t
 val pr_evar_universe_context : UState.t -> Pp.t
 val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9f7669f1d5..8b2721ae4e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1492,7 +1492,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 	   if not (Evd.is_defined acc ev) then 
 	     user_err ~hdr:"rewrite"
 			  (str "Unsolved constraint remaining: " ++ spc () ++
-			   Termops.pr_evar_info (Evd.find acc ev))
+                           Termops.pr_evar_info env acc (Evd.find acc ev))
 	   else Evd.remove acc ev) 
 	  cstrs evars'
       in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index d25ae38c53..d01338fa95 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -577,7 +577,7 @@ let pr_clenv clenv =
   h 0
     (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++
      str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++
-     pr_evar_map (Some 2) clenv.evd)
+     pr_evar_map (Some 2) clenv.env clenv.evd)
 
 (****************************************************************)
 (** Evar version of mk_clenv *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 388bf8efb5..231a8fe266 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -130,10 +130,10 @@ let db_pr_goal sigma g =
                    str" "  ++ pc) ++ fnl ()
 
 let pr_gls gls =
-  hov 0 (pr_evar_map (Some 2) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
+  hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
 
 let pr_glls glls =
-  hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++
+  hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++
          prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls))
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f302960870..14c83a6802 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -83,6 +83,7 @@ val refine           : constr -> tactic
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.t
 val pr_glls   : goal list sigma -> Pp.t
+[@@ocaml.deprecated "Please move to \"new\" proof engine"]
 
 (** Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ca77e03707..844caf5a3e 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -769,7 +769,7 @@ let pr_constraints printenv env sigma evars cstrs =
       h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs)
     else
       let filter evk _ = Evar.Map.mem evk evars in
-      pr_evar_map_filter ~with_univs:false filter sigma
+      pr_evar_map_filter ~with_univs:false filter env sigma
 
 let explain_unsatisfiable_constraints env sigma constr comp =
   let (_, constraints) = Evd.extract_all_conv_pbs sigma in