[funind] Move duplicated `observe_tac` function to indfun_common.

We also attempt a version that may work with `Proofview.tactic` , may
need more work.

5 files changed, 87 insertions, 145 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 08298bf02c..d49dd74eee 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -18,77 +18,6 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
-(* let msgnl = Pp.msgnl *)
-
-(*
-let observe strm =
-  if do_observe ()
-  then Pp.msg_debug strm
-  else ()
-
-let do_observe_tac s tac g =
- try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
- with e ->
-   let e = ExplainErr.process_vernac_interp_error e in
-   let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
-   msg_debug (str "observation "++ s++str " raised exception " ++
-            Errors.print e ++ str " on goal " ++ goal );
-   raise e;;
-
-let observe_tac_stream s tac g =
-  if do_observe ()
-  then do_observe_tac  s tac g
-  else tac g
-
-let observe_tac s tac g = observe_tac_stream (str s) tac g
-  *)
-
-
-let debug_queue = Stack.create ()
-
-let rec print_debug_queue e =
-  if  not (Stack.is_empty debug_queue)
-  then
-    begin
-      let lmsg,goal = Stack.pop debug_queue in
-      let _ =
-        match e with
-        | Some e ->
-           Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
-        | None ->
-           begin
-             Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
-           end in
-      print_debug_queue None ;
-    end
-
-let observe strm =
-  if do_observe ()
-  then Feedback.msg_debug strm
-  else ()
-
-let do_observe_tac s tac g =
-  let goal = Printer.pr_goal g in
-  let lmsg = (str "observation : ") ++ s in
-  Stack.push (lmsg,goal) debug_queue;
-  try
-    let v = tac g in
-    ignore(Stack.pop debug_queue);
-    v
-  with reraise ->
-    let reraise = CErrors.push reraise in
-    if not (Stack.is_empty debug_queue)
-    then print_debug_queue (Some (fst reraise));
-    iraise reraise
-
-let observe_tac_stream s tac g =
-  if do_observe ()
-  then do_observe_tac s tac g
-  else tac g
-
-let observe_tac s = observe_tac_stream (str s)
-
-
 let list_chop ?(msg="") n l =
   try
     List.chop n l
@@ -120,6 +49,7 @@ type 'a dynamic_info =
 
 type body_info = constr dynamic_info
 
+let observe_tac s = observe_tac (fun _ _ -> Pp.str s)
 
 let finish_proof dynamic_infos g =
   observe_tac "finish"
@@ -171,7 +101,7 @@ let is_incompatible_eq env sigma t =
         | _ -> false
     with e when CErrors.noncritical e -> false
   in
-  if res then   observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t);
+  if res then observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t);
   res
 
 let change_hyp_with_using msg hyp_id t tac : tactic =
@@ -843,7 +773,8 @@ let build_proof
           | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
-    observe_tac_stream (str "build_proof with " ++ pr_leconstr_env (pf_env g) (project g) dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+    Indfun_common.observe_tac (fun env sigma ->
+        str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args env sigma do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
       let (f_args',args) = dyn_infos.info in
@@ -1232,7 +1163,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
               if this_fix_info.idx + 1 = 0
               then tclIDTAC (* Someone  tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
               else
-                observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1)))
+                Indfun_common.observe_tac (fun _ _ -> str "h_fix " ++ int (this_fix_info.idx +1))
+                  (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1)))
             else
               Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
                 other_fix_infos 0)
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 72975d6871..e16825aa3f 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -15,30 +15,7 @@ open Indfun_common
 
 module RelDecl = Context.Rel.Declaration
 
-(* Move to common *)
-let observe strm =
-  if do_observe ()
-  then Feedback.msg_debug strm
-  else ()
-
-let do_observe_tac s tac g =
-  let goal =
-    try Printer.pr_goal g
-    with e when CErrors.noncritical e -> assert false
-  in
-  try
-    let v = tac g in
-    msgnl Pp.(goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
-  with reraise ->
-    let reraise = CErrors.push reraise in
-    observe Pp.(hov 0 (str "observation "++ s++str " raised exception " ++
-                       CErrors.iprint reraise ++ str " on goal" ++ fnl() ++ goal ));
-    iraise reraise;;
-
-let observe_tac s tac g =
-  if do_observe ()
-  then do_observe_tac (Pp.str s) tac g
-  else tac g
+let observe_tac s = observe_tac (fun _ _ -> Pp.str s)
 
 (*
    Construct a fixpoint as a Glob_term
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5cc3c96983..52a29fb559 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -377,7 +377,73 @@ let () = declare_bool_option function_debug_sig
 
 let do_observe () = !function_debug
 
+let observe strm =
+  if do_observe ()
+  then Feedback.msg_debug strm
+  else ()
+
+let debug_queue = Stack.create ()
+
+let print_debug_queue b e =
+  if not (Stack.is_empty debug_queue)
+  then
+    let lmsg,goal = Stack.pop debug_queue in
+    (if b then
+       Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
+     else
+       Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal))
+       (* print_debug_queue false e; *)
+    )
 
+let do_observe_tac s tac g =
+  let goal = Printer.pr_goal g in
+  let s = s (pf_env g) (project g) in
+  let lmsg = (str "observation : ") ++ s in
+  Stack.push (lmsg,goal) debug_queue;
+  try
+    let v = tac g in
+    ignore(Stack.pop debug_queue);
+    v
+  with reraise ->
+    let reraise = CErrors.push reraise in
+    if not (Stack.is_empty debug_queue)
+    then print_debug_queue true (fst reraise);
+    Util.iraise reraise
+
+let observe_tac s tac g =
+  if do_observe ()
+  then do_observe_tac s tac g
+  else tac g
+
+module New = struct
+
+let do_observe_tac ~header s tac =
+  let open Proofview.Notations in
+  let open Proofview in
+  Goal.enter begin fun gl ->
+    let goal = Printer.pr_goal (Goal.print gl) in
+    let env, sigma = Goal.env gl, Goal.sigma gl in
+    let s = s env sigma in
+    let lmsg = seq [header; str " : " ++ s] in
+    tclLIFT (NonLogical.make (fun () ->
+        Feedback.msg_debug (s++fnl()))) >>= fun () ->
+    tclOR (
+      Stack.push (lmsg, goal) debug_queue;
+      tac >>= fun v ->
+      ignore(Stack.pop debug_queue);
+      Proofview.tclUNIT v)
+      (fun (exn, info) ->
+         if not (Stack.is_empty debug_queue)
+         then print_debug_queue true exn;
+         tclZERO ~info exn)
+  end
+
+let observe_tac ~header s tac =
+  if do_observe ()
+  then do_observe_tac ~header s tac
+  else tac
+
+end
 
 let strict_tcc = ref false
 let is_strict_tcc () = !strict_tcc
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 0b8cbf6dc5..fff4711044 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -85,7 +85,21 @@ val update_Function : function_info -> unit
 val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t
 val pr_table : Environ.env -> Evd.evar_map -> Pp.t
 
+val observe_tac
+  : (Environ.env -> Evd.evar_map -> Pp.t)
+  -> Tacmach.tactic -> Tacmach.tactic
+
+module New : sig
+
+  val observe_tac
+    : header:Pp.t
+    -> (Environ.env -> Evd.evar_map -> Pp.t)
+    -> unit Proofview.tactic -> unit Proofview.tactic
+
+end
+
 (* val function_debug : bool ref  *)
+val observe : Pp.t -> unit
 val do_observe : unit -> bool
 val do_rewrite_dependent : unit -> bool
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 937118bf57..8e9abfc789 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -199,53 +199,6 @@ let (declare_f : Id.t -> Decls.logical_kind -> Constr.t list -> GlobRef.t -> Glo
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
-
-
-(* Debugging mechanism *)
-let debug_queue = Stack.create ()
-
-let print_debug_queue b e =
-  if  not (Stack.is_empty debug_queue)
-  then
-    begin
-      let lmsg,goal = Stack.pop debug_queue in
-      if b then
-        Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.iprint e) ++ str " on goal" ++ fnl() ++ goal))
-      else
-        begin
-          Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
-        end;
-      (* print_debug_queue false e; *)
-    end
-
-let observe strm =
-  if do_observe ()
-  then Feedback.msg_debug strm
-  else ()
-
-
-let do_observe_tac s tac g =
-  let goal = Printer.pr_goal g in
-  let s = s (pf_env g) (project g) in
-  let lmsg = (str "recdef : ") ++ s in
-  observe (s++fnl());
-  Stack.push (lmsg,goal) debug_queue;
-  try
-    let v = tac g in
-    ignore(Stack.pop debug_queue);
-    v
-  with reraise ->
-    let reraise = CErrors.push reraise in
-    if not (Stack.is_empty debug_queue)
-    then print_debug_queue true reraise;
-    iraise reraise
-
-let observe_tac s tac g =
-  if do_observe ()
-  then do_observe_tac s tac g
-  else tac g
-
-
 let observe_tclTHENLIST s tacl =
   if do_observe ()
   then