From 6538ebfd130c35bf15df5a2ca66504cbbd4d1812 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Thu, 21 Sep 2023 14:42:33 -0700 Subject: [PATCH] Support stopping on GTacExt (open_constr, etc.) --- plugins/ltac/tactic_debug.ml | 3 ++- plugins/ltac2/tac2core.ml | 4 +++- plugins/ltac2/tac2debug.ml | 2 +- plugins/ltac2/tac2expr.mli | 3 ++- plugins/ltac2/tac2intern.ml | 6 +++--- plugins/ltac2/tac2interp.ml | 34 ++++++++++++++++++++++++++++------ plugins/ltac2/tac2print.ml | 2 +- vernac/debugCommon.ml | 15 +++++++++++++-- vernac/debugCommon.mli | 3 +++ 9 files changed, 56 insertions(+), 16 deletions(-) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 5c7f77d1e7f0..5ebbbada68f4 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/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) *) diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index bdbb54cf97bc..84df175fa74f 100644 --- a/plugins/ltac2/tac2core.ml +++ b/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 diff --git a/plugins/ltac2/tac2debug.ml b/plugins/ltac2/tac2debug.ml index 25f32c25fadd..c96b2bbed5ce 100644 --- a/plugins/ltac2/tac2debug.ml +++ b/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" diff --git a/plugins/ltac2/tac2expr.mli b/plugins/ltac2/tac2expr.mli index e3032875e26f..4efd7158f457 100644 --- a/plugins/ltac2/tac2expr.mli +++ b/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 diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index b2f8a91bfcb9..1a12b6050cad 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/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 diff --git a/plugins/ltac2/tac2interp.ml b/plugins/ltac2/tac2interp.ml index 311e8c5a910b..232ac5b627b3 100644 --- a/plugins/ltac2/tac2interp.ml +++ b/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,7 +185,7 @@ 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 @@ -184,7 +193,7 @@ match e with 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 -> diff --git a/plugins/ltac2/tac2print.ml b/plugins/ltac2/tac2print.ml index 482cbb84d0c2..1ece86e73750 100644 --- a/plugins/ltac2/tac2print.ml +++ b/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 diff --git a/vernac/debugCommon.ml b/vernac/debugCommon.ml index 459f211a4598..cf50ab0a6a34 100644 --- a/vernac/debugCommon.ml +++ b/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 () = diff --git a/vernac/debugCommon.mli b/vernac/debugCommon.mli index d735ac83ad3c..eca391cd6f23 100644 --- a/vernac/debugCommon.mli +++ b/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