Source file `tac2bt.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Tac2expr
open Proofview.Notations

let backtrace_evd : backtrace Evd.Store.field = Evd.Store.field "ltac2_trace"

let backtrace : backtrace Exninfo.t = Exninfo.make "ltac2_trace"

let print_ltac2_backtrace = ref false

let () = Goptions.declare_bool_option {
  Goptions.optstage = Summary.Stage.Interp;
  Goptions.optdepr = None;
  Goptions.optkey = ["Ltac2"; "Backtrace"];
  Goptions.optread = (fun () -> !print_ltac2_backtrace);
  Goptions.optwrite = (fun b -> print_ltac2_backtrace := b);
}

let ltac2_in_ltac1_profiling = ref false

let () = Goptions.declare_bool_option {
  Goptions.optstage = Summary.Stage.Interp;
  Goptions.optdepr = None;
  Goptions.optkey = ["Ltac2"; "In"; "Ltac1"; "Profiling"];
  Goptions.optread = (fun () -> !ltac2_in_ltac1_profiling);
  Goptions.optwrite = (fun b -> ltac2_in_ltac1_profiling := b);
}

let get_backtrace =
  Proofview.tclEVARMAP >>= fun sigma ->
  match Evd.Store.get (Evd.get_extra_data sigma) backtrace_evd with
  | None -> Proofview.tclUNIT []
  | Some bt -> Proofview.tclUNIT bt

let set_backtrace bt =
  Proofview.tclEVARMAP >>= fun sigma ->
  let store = Evd.get_extra_data sigma in
  let store = Evd.Store.set store backtrace_evd bt in
  let sigma = Evd.set_extra_data store sigma in
  Proofview.Unsafe.tclEVARS sigma

let pr_frame, pr_frame_hook = Hook.make ()

let with_frame frame tac =
  let tac =
    if !print_ltac2_backtrace then
      get_backtrace >>= fun bt ->
      set_backtrace (frame :: bt) >>= fun () ->
      Proofview.tclOR tac (fun (e,info) ->
          (* If it's already present assume it's more precise *)
          let info = if Option.has_some (Exninfo.get info backtrace) then info
            else Exninfo.add info backtrace (frame::bt)
          in
          Proofview.tclZERO ~info e)
          >>= fun ans ->
      set_backtrace bt >>= fun () ->
      Proofview.tclUNIT ans
    else tac
  in
  if !ltac2_in_ltac1_profiling then
    let pr_frame f = Some (Hook.get pr_frame f) in
    Profile_tactic.do_profile_gen pr_frame frame ~count_call:true tac
  else tac