Source file exceptions.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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
(******************************************************************************)
(*                  This file is part of Waterproof-lib.                      *)
(*                                                                            *)
(*   Waterproof-lib is free software: you can redistribute it and/or modify   *)
(*    it under the terms of the GNU General Public License as published by    *)
(*     the Free Software Foundation, either version 3 of the License, or      *)
(*                    (at your option) any later version.                     *)
(*                                                                            *)
(*     Waterproof-lib is distributed in the hope that it will be useful,      *)
(*      but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*       MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the         *)
(*               GNU General Public License for more details.                 *)
(*                                                                            *)
(*     You should have received a copy of the GNU General Public License      *)
(*   along with Waterproof-lib. If not, see <https://www.gnu.org/licenses/>.  *)
(*                                                                            *)
(******************************************************************************)

open Pp
open Feedback

let wp_debug_log = Summary.ref ~name:"wp_debug_log" []
let wp_info_log = Summary.ref ~name:"wp_info_log" []
let wp_notice_log = Summary.ref ~name:"wp_notice_log" []
let wp_warning_log = Summary.ref ~name:"wp_warning_log" []
let wp_error_log = Summary.ref ~name:"wp_error_log" []

(**
  A rudimentary feedback log
*)
let feedback_log (lvl : level) : Pp.t list ref =
  match lvl with
  | Debug -> wp_debug_log
  | Info -> wp_info_log
  | Notice -> wp_notice_log
  | Warning -> wp_warning_log
  | Error -> wp_error_log

(**
  The id that we obtained when registering wp_feedback_logger as a feeder in Feedback.mli
*)
let wp_feedback_logger_id = Summary.ref ~name: "wp_feedback_logger_id" None

let info_counter = Summary.ref ~name:"info_counter" 0

(**
  A custom feedback logger for waterproof
*)
let wp_feedback_logger (fb : feedback) : unit =
  match fb.contents with
  | Message (lvl, _, msg) ->
    (feedback_log lvl :=
      (msg) :: !(feedback_log lvl);
    info_counter := !info_counter + 1)
  | _ -> ()

(**
  Adds wp_feedback_logger to Coq's feedback mechanism
*)
let add_wp_feedback_logger () : unit =
  match !wp_feedback_logger_id with
  | Some _ -> msg_warning (str "The waterproof feedback logger was already added")
  | None -> let id = Feedback.add_feeder wp_feedback_logger in
            wp_feedback_logger_id := Some id

(**
  Basic exception info
*)
let fatal_flag: 'a Exninfo.t = Exninfo.make ()

(**
  The last thrown warning
*)
let last_thrown_warning : Pp.t option ref = Summary.ref ~name:"last_thrown_warning" None

(**
  Redirect warnings: this is useful when testing the plugin
*)
let redirect_feedback : bool ref = Summary.ref ~name:"redirect_feedback" false

(**
  Redirect errors: this is useful when testing the plugin
*)
let redirect_errors : bool ref = Summary.ref ~name:"redirect_errors" false

(**
  Print hypotheses help
*)
let print_hypothesis_help : bool ref = Summary.ref ~name:"print_hypothesis_help" false

(**
  Type of exceptions used in Wateproof
*)
type wexn =
  | CastError of string (** Indicates that a cast made by the FFI has failed  *)
  | FailedAutomation of string (** Indicates that the automatic solver called has failed  *)
  | FailedTest of string (** Indicates that the running test has failed *)
  | NonExistingDataset of Hints.hint_db_name (** Indicates that the user tried to import a non-existing hint dataset *)
  | UnusedLemmas (** Indicates that no proof using all the given lemmas has been found *)
  | ToUserError of Pp.t (** An error that should go directly to the user *)

(**
  Converts errors to displayable messages
*)
let pr_wexn (exn: wexn): t =
  match exn with
    | CastError message -> str "Cast error: " ++ str message
    | FailedAutomation message -> str "Automatic solving failed: " ++ str message
    | FailedTest test -> str "Failed test: " ++ str test
    | NonExistingDataset dataset -> str "Non existing dataset: the dataset " ++ str dataset ++ str " is not defined"
    | UnusedLemmas -> str "No proof using all given lemmas has been found"
    | ToUserError message -> message

(**
  Throws an error with given info and message
*)
let throw ?(info: Exninfo.info = Exninfo.null) (exn: wexn): 'a =
  let fatal = Exninfo.add info fatal_flag () in
  CErrors.user_err ?info:(Some fatal) (pr_wexn exn)

(**
  Send a message
*)
let message (lvl : Feedback.level) (input : Pp.t) : unit Proofview.tactic =
  if !redirect_feedback then
    Proofview.tclUNIT @@ (feedback_log lvl := input :: !(feedback_log lvl))
  else
    Proofview.tclUNIT @@ feedback (Message (lvl, None, input))

(**
  Send a warning
*)
let warn (input : Pp.t) : unit Proofview.tactic =
  message Warning input

(**
  Send a notice
*)
let notice (input : Pp.t) : unit Proofview.tactic =
  message Notice input

(**
  Send an info message
*)
let inform (input : Pp.t) : unit Proofview.tactic =
  message Info input

(**
  Throw an error
*)
let err (input : Pp.t) : unit Proofview.tactic =
  throw (ToUserError input)

(**
  Return the last warning
*)
let get_last_warning () : Pp.t option Proofview.tactic =
  Proofview.tclUNIT @@
    match !(feedback_log Warning) with
    | [] -> None
    | hd :: tl -> Some hd