Library Waterproof.Util.MessagesToUser
Require Export Ltac2.Ltac2.
Require Import Ltac2.Bool.
Require Import Ltac2.Init.
Require Import Ltac2.String.
Require Import Waterproof.Waterproof.
TODO: in later versions of Coq this can be replaced by a native function
Ltac2 fnl () := Message.of_string "
".
Ltac2 Type FeedbackLevel := [ Debug | Info | Notice | Warning | Error ].
Ltac2 @ external send_message_external: FeedbackLevel -> message -> unit := "rocq-runtime.plugins.coq-waterproof" "message_external".
Ltac2 @ external throw_external: message -> unit := "rocq-runtime.plugins.coq-waterproof" "throw_external".
Ltac2 @ external get_print_hypothesis_flag: unit -> bool := "rocq-runtime.plugins.coq-waterproof" "get_print_hypothesis_flag_external".
Ltac2 @ external get_redirect_errors_flag : unit -> bool := "rocq-runtime.plugins.coq-waterproof" "get_redirect_errors_flag_external".
Ltac2 @ external shortest_string_of_global_ffi : Std.reference -> string :=
"rocq-runtime.plugins.coq-waterproof" "shortest_string_of_global_external".
Ltac2 @ external get_last_warning : unit -> message option :=
"rocq-runtime.plugins.coq-waterproof" "get_last_warning_external".
Ltac2 @ external get_feedback_log_external : FeedbackLevel -> message list :=
"rocq-runtime.plugins.coq-waterproof" "get_feedback_log_external".
Ltac2 Type FeedbackLevel := [ Debug | Info | Notice | Warning | Error ].
Ltac2 @ external send_message_external: FeedbackLevel -> message -> unit := "rocq-runtime.plugins.coq-waterproof" "message_external".
Ltac2 @ external throw_external: message -> unit := "rocq-runtime.plugins.coq-waterproof" "throw_external".
Ltac2 @ external get_print_hypothesis_flag: unit -> bool := "rocq-runtime.plugins.coq-waterproof" "get_print_hypothesis_flag_external".
Ltac2 @ external get_redirect_errors_flag : unit -> bool := "rocq-runtime.plugins.coq-waterproof" "get_redirect_errors_flag_external".
Ltac2 @ external shortest_string_of_global_ffi : Std.reference -> string :=
"rocq-runtime.plugins.coq-waterproof" "shortest_string_of_global_external".
Ltac2 @ external get_last_warning : unit -> message option :=
"rocq-runtime.plugins.coq-waterproof" "get_last_warning_external".
Ltac2 @ external get_feedback_log_external : FeedbackLevel -> message list :=
"rocq-runtime.plugins.coq-waterproof" "get_feedback_log_external".
Can be removed in a later version of Rocq, probably 9.2,
because it has then been integrated in Ltac2.
Ltac2 @ external of_lconstr : constr -> message := "rocq-runtime.plugins.coq-waterproof" "message_of_lconstr".
Prints at level 200 (no surrounding parentheses).
Panics if there is more than one goal under focus.
Ltac2 Type exn ::= [RedirectedToUserError (message)].
Ltac2 send_message (lvl : FeedbackLevel) (msg : message) :=
send_message_external lvl msg.
Ltac2 inform (msg : message) :=
send_message Info msg.
Ltac2 notice (msg : message) :=
send_message Notice msg.
Ltac2 warn (msg : message) :=
send_message Warning msg.
Ltac2 get_feedback_log (lvl : FeedbackLevel) :=
get_feedback_log_external lvl.
Ltac2 info_notice (msg : message) := inform msg; notice msg.
Ltac2 replace_notice (template : string) :=
notice (Message.concat (Message.of_string "Hint, replace with: ") (Message.of_string template)).
Ltac2 insert_msg (msg : string) (template : string) :=
inform (Message.concat (Message.of_string "Hint, insert: ") (Message.of_string msg));
notice (Message.concat (Message.of_string "Hint, insert: ") (Message.of_string template)).
Ltac2 replace_msg (msg : string) (template : string) :=
inform (Message.concat (Message.of_string "Hint, replace with: ") (Message.of_string msg));
replace_notice template.
Ltac2 throw (msg : message) :=
if (get_redirect_errors_flag ()) then
Control.zero (RedirectedToUserError msg)
We use an OCaml error here, because it gets rendered much nicer in the editor
else throw_external msg.