package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct