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
|
