Support stopping on GTacExt (open_constr, etc.)

plugins/ltac/tactic_debug.ml

@@ -202,7 +202,7 @@ let db_initialize is_tac =
   let open Proofview.NonLogical in
   let x = (skip:=0) >> (skipped:=0) >> (idtac_breakpt:=None) in
   if is_tac then begin
-          idtac_bpt_stop.contents <- false;
+    idtac_bpt_stop.contents <- false;
     make DebugCommon.init >> x
   end else x
 
@@ -367,6 +367,7 @@ let debug_prompt lev tac f varmap trace =
     end
 
 (* for ltac1:(tac) *)
+(* todo: apparently not needed *)
 let entry_stop_check tac =
 (*  Printf.eprintf "entry_stop_check\n%!"; *)
   let can_stop = match CAst.(tac.v) with (* avoid double stop for ltac1:(xx) *)

plugins/ltac2/tac2core.ml

@@ -1517,8 +1517,10 @@ let () =
       let wrap (e, info) = set_bt info >>= fun info ->
           DebugCommon.pop_chunk ();
           Proofview.tclZERO ~info e in
+(*
       Proofview.tclTHEN
         (Ltac_plugin.Tactic_debug.entry_stop_check tac)
+*)
         (Proofview.tclOR tac2 wrap >>= fun () -> DebugCommon.pop_chunk (); return v_unit)
     in
     let len = List.length ids in
@@ -1642,7 +1644,7 @@ let () =
   let subs globs (ids, tac) =
     (* Let-bind the notation terms inside the tactic *)
     let fold id (c, _) (rem, accu) =
-      let c = GTacExt (Tac2quote.wit_preterm, c) in
+      let c = GTacExt (Tac2quote.wit_preterm, None, c) in
       let rem = Id.Set.remove id rem in
       rem, (Name id, c) :: accu
     in

plugins/ltac2/tac2debug.ml

@@ -184,7 +184,7 @@ let rec dump_expr2 ?(indent=0) ?(p="D") e =
   | GTacOpn _ -> print "GTacOpn"
   | GTacWth _ -> print "GTacWth"
   | GTacFullMatch _ -> print "GTacFullMatch"
-  | GTacExt (tag,_) -> print (Printf.sprintf "GTacExt %s" (Tac2dyn.Arg.repr tag))
+  | GTacExt (tag,_, _) -> print (Printf.sprintf "GTacExt %s" (Tac2dyn.Arg.repr tag))
   | GTacPrm (ml, _) -> print (Printf.sprintf "GTacPrm %s. %s\n%!" ml.mltac_plugin ml.mltac_tactic)
   | GTacAls  _ -> print "GTacAls"
 

plugins/ltac2/tac2expr.mli

@@ -175,7 +175,8 @@ type glb_tacexpr =
 | GTacOpn of ltac_constructor * glb_tacexpr list
 | GTacWth of glb_tacexpr open_match
 | GTacFullMatch of glb_tacexpr * (glb_pat * glb_tacexpr) list
-| GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
+(* todo: * Loc.t option at the end gives a syntax error :-( *)
+| GTacExt : (_, 'a) Tac2dyn.Arg.tag * Loc.t option * 'a -> glb_tacexpr
 | GTacPrm of ml_tactic_name * glb_tacexpr list
 | GTacAls of glb_tacexpr * Loc.t option
 

plugins/ltac2/tac2intern.ml

@@ -1356,7 +1356,7 @@ let rec intern_rec env {loc;v=e} = match e with
       obj.ml_intern self ist arg
   in
   let e = match arg with
-  | GlbVal arg -> GTacExt (tag, arg)
+  | GlbVal arg -> GTacExt (tag, loc, arg)
   | GlbTacexpr e -> e
   in
   (e, tpe)
@@ -1764,10 +1764,10 @@ let rec subst_expr subst e = match e with
   let e' = subst_expr subst e in
   let r' = subst_expr subst r in
   if kn' == kn && e' == e && r' == r then e0 else GTacSet (kn', e', p, r')
-| GTacExt (tag, arg) ->
+| GTacExt (tag, loc, arg) ->
   let tpe = interp_ml_object tag in
   let arg' = tpe.ml_subst subst arg in
-  if arg' == arg then e else GTacExt (tag, arg')
+  if arg' == arg then e else GTacExt (tag, loc, arg')
 | GTacOpn (kn, el) as e0 ->
   let kn' = subst_kn subst kn in
   let el' = List.Smart.map (fun e -> subst_expr subst e) el in

plugins/ltac2/tac2interp.ml

@@ -134,6 +134,15 @@ and match_pattern_against_or ist pats v =
 let rec interp (ist : environment) e =
 (*  let p = "I" in *)
 (*  dump_expr2 ~p e; *)
+(*
+(match ist.stack with
+| Some ((rtn, loc) :: tl) -> Printf.eprintf "TOS is %s\n%!" rtn;
+  if rtn = "Rewriter.Language.IdentifiersBasicGenerate.Compilers.Basic.Tactic.reify_package_of_package" then
+    let p = "XX" in
+    dump_expr2 ~p e
+| _ -> ()
+);
+*)
 match e with
 | GTacAtm (AtmInt n) -> return (Tac2ffi.of_int n)
 | GTacAtm (AtmStr s) -> return (Tac2ffi.of_string s)
@@ -153,7 +162,7 @@ match e with
 | GTacApp (f, args, loc) ->  (* todo: move much of following to tac2debug.ml *)
   let fname = match f with
   | GTacRef kn -> let s = KerName.to_string kn in if false then Printf.eprintf "kn = %s\n%!" s; s
-  | GTacExt (tag,_) -> (Tac2dyn.Arg.repr tag)   (* for ltac1val: *)
+  | GTacExt (tag,_,_) -> (Tac2dyn.Arg.repr tag)   (* for ltac1val: *)
   | _ -> "???"
   in
 (*  Printf.eprintf "fname = %s not starts_with = %b\n%!" fname (Bool.not (starts_with "Ltac2." fname)); *)
@@ -176,15 +185,15 @@ match e with
         varmaps = ist.env_ist :: ist.varmaps }
     else ist
   in
-  let (>=) = Proofview.tclBIND in
+  let (>=) = Proofview.tclBIND in  (* todo?: simplify fun () -> () below *)
   let step = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> ())) >= fun () ->
     if DebugCommon.get_debug () && stop_stuff ist0 loc then
       (DebugCommon.db_pr_goals ()) >>= fun () -> read_loop (); interp ist f
     else
       interp ist f
   in
   Proofview.tclTHEN
-    (DebugCommon.save_goals ())  (* TODO: shouldn't execute if not in debug; restructure code *)
+    (DebugCommon.save_goals ())
     (step >>= fun f ->
       Proofview.Monad.List.map (fun e -> interp ist0 e) args >>= fun args ->
       Tac2ffi.apply (Tac2ffi.to_closure f) args)
@@ -245,11 +254,24 @@ match e with
 (*    end else ist in*)
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
   with_frame (FrPrim ml) (Tac2ffi.apply (Tac2env.interp_primitive ml) el)
-| GTacExt (tag, e) ->
+| GTacExt (tag, loc, e) ->
   let chunk = (ist.locs, fmt_stack2 ist.stack, fmt_vars2 (ist.env_ist :: ist.varmaps)) in
   DebugCommon.set_top_chunk chunk;
-  let tpe = Tac2env.interp_ml_object tag in
-  with_frame (FrExtn (tag, e)) (tpe.Tac2env.ml_interp ist e)
+(*  Printf.eprintf "interp GTacExt\n%!"; *)
+  let step =
+    Proofview.NonLogical.make (fun () ->
+      if (DebugCommon.get_debug () && stop_stuff ist loc) then begin
+        DebugCommon.db_pr_goals2 ();
+        read_loop ()
+      end)
+  in
+  Proofview.tclTHEN
+    (DebugCommon.save_goals ())
+    (Proofview.tclLIFT step >>=
+      (fun _ ->
+(*        Printf.eprintf "interp2 GTacExt\n%!"; *)
+        let tpe = Tac2env.interp_ml_object tag in
+        with_frame (FrExtn (tag, e)) (tpe.Tac2env.ml_interp ist e)))
 
 and interp_closure ist0 f =
   let ans = fun args ->

plugins/ltac2/tac2print.ml

@@ -400,7 +400,7 @@ let pr_glbexpr_gen lvl c =
     in
     let c = pr_constructor kn in
     paren (hov 0 (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl)))
-  | GTacExt (tag, arg) ->
+  | GTacExt (tag, _, arg) ->
     let tpe = interp_ml_object tag in
     let env = Global.env() in
     let sigma = Evd.from_env env in

vernac/debugCommon.ml

@@ -472,9 +472,20 @@ let db_fmt_goals () =
   str (CString.plural (List.length gls) "Goal") ++ str ":" ++ fnl () ++
       Pp.seq (List.map db_fmt_goal gls)
 
-let db_pr_goals () =
+
+ let db_pr_goals3 () =
+  let open Proofview.NonLogical in
+  let gs = make (fun () -> (* Printf.eprintf "db_pr_goals3\n%!"; *) db_fmt_goals ()) in
+  gs >>= fun gs -> goals gs
+
+let db_pr_goals2 () =
+(*  Printf.eprintf "db_pr_goals2\n%!"; *)
   let gs = db_fmt_goals () in
-  Proofview.tclLIFT (goals gs)   (* TODO: MAYBE DROP THIS LINE? *)
+  ignore @@ goals gs;
+  ()
+
+let db_pr_goals () =
+  Proofview.tclLIFT (db_pr_goals3 ())
 
 let isTerminal () = (hook ()).isTerminal
 let read () =

vernac/debugCommon.mli

@@ -49,6 +49,9 @@ val format_stack : string option list -> Loc.t option list -> DebugHook.Answer.s
 
 val db_pr_goals : unit -> unit Proofview.tactic
 
+val db_pr_goals2 : unit -> unit
+(* val db_pr_goals2 : unit -> unit Proofview.NonLogical.t *)
+
 val pop_chunk : unit -> unit
 
 val new_stop_point : unit -> unit