aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proofview.ml4
-rw-r--r--proofs/proofview.mli31
-rw-r--r--proofs/proofview_gen.ml33
-rw-r--r--proofs/proofview_monad.mli4
-rw-r--r--proofs/tactic_debug.ml213
-rw-r--r--proofs/tactic_debug.mli24
6 files changed, 225 insertions, 84 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9496b51ea..3e05b60f0 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -575,3 +575,7 @@ module Goal = struct
let hyps = lift Goal.hyps
let env = lift Goal.env
end
+
+module NonLogical = Proofview_monad.NonLogical
+
+let tclLIFT = Proofview_monad.Logical.lift
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 136a44332..5caffa8bd 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -290,3 +290,34 @@ module Goal : sig
(* [lift Goal.env] *)
val env : Environ.env glist tactic
end
+
+
+module NonLogical : sig
+
+ type +'a t
+ type 'a ref
+
+ val ret : 'a -> 'a t
+ val bind : 'a t -> ('a -> 'b t) -> 'b t
+ val ignore : 'a t -> unit t
+ val seq : unit t -> 'a t -> 'a t
+
+ val new_ref : 'a -> 'a ref t
+ val set : 'a ref -> 'a -> unit t
+ val get : 'a ref -> 'a t
+
+ val read_line : string t
+ val print_char : char -> unit t
+ val print : Pp.std_ppcmds -> unit t
+
+ val raise : exn -> 'a t
+ val catch : 'a t -> (exn -> 'a t) -> 'a t
+ val timeout : int -> 'a t -> 'a t
+
+
+ (* [run] performs effects. *)
+ val run : 'a t -> 'a
+
+end
+
+val tclLIFT : 'a NonLogical.t -> 'a tactic
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 577aa2ddb..422095870 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -57,10 +57,21 @@ module IOBase =
let catch = fun s h () -> try s () with Proof_errors.Exception e -> h e ()
- type coq_Int = int
+ (** val read_line : string coq_T **)
+
+ let read_line = fun () -> try Pervasives.read_line () with e -> raise e ()
+
+ (** val print_char : char -> unit coq_T **)
+
+ let print_char = fun c () -> print_char c
+
+ (** val print :
+ Pp.std_ppcmds -> unit coq_T **)
+
+ let print = fun s () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()
(** val timeout :
- coq_Int -> 'a1 coq_T -> 'a1 coq_T **)
+ int -> 'a1 coq_T -> 'a1 coq_T **)
let timeout = fun n t () ->
let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
@@ -143,12 +154,26 @@ module NonLogical =
let catch s h =
IOBase.catch s h
- (** val timeout :
- IOBase.coq_Int -> 'a1 t -> 'a1 t **)
+ (** val timeout : int -> 'a1 t -> 'a1 t **)
let timeout n x =
IOBase.timeout n x
+ (** val read_line : string t **)
+
+ let read_line =
+ IOBase.read_line
+
+ (** val print_char : char -> unit t **)
+
+ let print_char c =
+ IOBase.print_char c
+
+ (** val print : Pp.std_ppcmds -> unit t **)
+
+ let print s =
+ IOBase.print s
+
(** val run : 'a1 t -> 'a1 **)
let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index 02550aebc..bdebe658c 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -27,6 +27,10 @@ module NonLogical : sig
val set : 'a ref -> 'a -> unit t
val get : 'a ref -> 'a t
+ val read_line : string t
+ val print_char : char -> unit t
+ val print : Pp.std_ppcmds -> unit t
+
val raise : exn -> 'a t
val catch : 'a t -> (exn -> 'a t) -> 'a t
val timeout : int -> 'a t -> 'a t
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 1b49f9ff8..dc48cfc3b 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -16,6 +16,14 @@ let (prtac, tactic_printer) = Hook.make ()
let (prmatchpatt, match_pattern_printer) = Hook.make ()
let (prmatchrl, match_rule_printer) = Hook.make ()
+(* Notations *)
+let return = Proofview.NonLogical.ret
+let (>>=) = Proofview.NonLogical.bind
+let (>>) = Proofview.NonLogical.seq
+let (:=) = Proofview.NonLogical.set
+let (!) = Proofview.NonLogical.get
+let raise = Proofview.NonLogical.raise
+
(* This module intends to be a beginning of debugger for tactic expressions.
Currently, it is quite simple and we can hope to have, in the future, a more
complete panel of commands dedicated to a proof assistant framework *)
@@ -30,20 +38,26 @@ let explain_logic_error = ref (fun e -> mt())
let explain_logic_error_no_anomaly = ref (fun e -> mt())
-let msg_tac_debug s = Pp.ppnl s; Pp.pp_flush ()
+let msg_tac_debug s = Proofview.NonLogical.print (s++fnl())
(* Prints the goal *)
-let db_pr_goal g =
- let env = Refiner.pf_env g in
+let db_pr_goal =
+ let (>>=) = Goal.bind in
+ Goal.env >>= fun env ->
+ Goal.concl >>= fun concl ->
let penv = print_named_context env in
- let pc = print_constr_env env (Goal.V82.concl (Refiner.project g) (Refiner.sig_it g)) in
- str" " ++ hv 0 (penv ++ fnl () ++
+ let pc = print_constr_env env concl in
+ Goal.return begin
+ str" " ++ hv 0 (penv ++ fnl () ++
str "============================" ++ fnl () ++
str" " ++ pc) ++ fnl ()
+ end
-let db_pr_goal g =
- msg_tac_debug (str "Goal:" ++ fnl () ++ db_pr_goal g)
+let db_pr_goal =
+ let (>>=) = Proofview.Notations.(>>=) in
+ Proofview.Goal.lift db_pr_goal >>= fun pg ->
+ Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg))
(* Prints the commands *)
@@ -56,15 +70,17 @@ let help () =
str " x = Exit")
(* Prints the goal and the command to be executed *)
-let goal_com g tac =
- begin
- db_pr_goal g;
- msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac)
- end
-
-let skipped = ref 0
-let skip = ref 0
-let breakpoint = ref None
+let goal_com tac =
+ Proofview.tclTHEN
+ db_pr_goal
+ (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac)))
+
+(* [run (new_ref _)] gives us a ref shared among [NonLogical.t]
+ expressions. It avoids parametrizing everything over a
+ reference. *)
+let skipped = Proofview.NonLogical.run (Proofview.NonLogical.new_ref 0)
+let skip = Proofview.NonLogical.run (Proofview.NonLogical.new_ref 0)
+let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.new_ref None)
let rec drop_spaces inst i =
if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
@@ -77,19 +93,28 @@ let possibly_unquote s =
s
(* (Re-)initialize debugger *)
-let db_initialize () =
- skip:=0;skipped:=0;breakpoint:=None
+let db_initialize =
+ (skip:=0) >> (skipped:=0) >> (breakpoint:=None)
+
+let int_of_string s =
+ try return (int_of_string s)
+ with e -> Proofview.NonLogical.raise e
+
+let string_get s i =
+ try return (String.get s i)
+ with e -> Proofview.NonLogical.raise e
(* Gives the number of steps or next breakpoint of a run command *)
let run_com inst =
- if (String.get inst 0) == 'r' then
+ string_get inst 0 >>= fun first_char ->
+ if first_char ='r' then
let i = drop_spaces inst 1 in
if String.length inst > i then
let s = String.sub inst i (String.length inst - i) in
if inst.[0] >= '0' && inst.[0] <= '9' then
- let num = int_of_string s in
- if num<0 then invalid_arg "run_com";
- skip:=num;skipped:=0
+ int_of_string s >>= fun num ->
+ (if num<0 then invalid_arg "run_com" else return ()) >>
+ (skip:=num) >> (skipped:=0)
else
breakpoint:=Some (possibly_unquote s)
else
@@ -100,69 +125,106 @@ let run_com inst =
(* Prints the run counter *)
let run ini =
if not ini then
- begin
- for _i = 1 to 2 do
- print_char (Char.chr 8);print_char (Char.chr 13)
- done;
- msg_tac_debug (str "Executed expressions: " ++ int !skipped ++ fnl())
- end;
- incr skipped
+ begin
+ Proofview.NonLogical.print (str"\b\r\b\r") >>
+ !skipped >>= fun skipped ->
+ msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl())
+ end >>
+ !skipped >>= fun x ->
+ skipped := x+1
+ else
+ return ()
(* Prints the prompt *)
let rec prompt level =
begin
- pp (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
- flush stdout;
- let exit () = skip:=0;skipped:=0;raise Sys.Break in
- let inst = try read_line () with End_of_file -> exit () in
+ Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+ let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
+ Proofview.NonLogical.catch Proofview.NonLogical.read_line
+ begin function
+ | End_of_file -> exit
+ | e -> raise e
+ end
+ >>= fun inst ->
match inst with
- | "" -> DebugOn (level+1)
- | "s" -> DebugOff
- | "x" -> print_char (Char.chr 8); exit ()
+ | "" -> return (DebugOn (level+1))
+ | "s" -> return (DebugOff)
+ | "x" -> Proofview.NonLogical.print_char '\b' >> exit
| "h"| "?" ->
begin
- help ();
+ help () >>
prompt level
end
| _ ->
- (try run_com inst;run true;DebugOn (level+1)
- with Failure _ | Invalid_argument _ -> prompt level)
+ Proofview.NonLogical.catch (run_com inst >> run true >> return (DebugOn (level+1)))
+ begin function
+ | Failure _ | Invalid_argument _ -> prompt level
+ | e -> raise e
+ end
end
(* Prints the state and waits for an instruction *)
-let debug_prompt lev g tac f =
+(* spiwack: the only reason why we need to take the continuation [f]
+ as an argument rather than returning the new level directly seems to
+ be that [f] is wrapped in with "explain_logic_error". I don't think
+ it serves any purpose in the current design, so we could just drop
+ that. *)
+let debug_prompt lev tac f =
+ let (>=) = Proofview.tclBIND in
(* What to print and to do next *)
let newlevel =
- if Int.equal !skip 0 then
- if Option.is_empty !breakpoint then (goal_com g tac; prompt lev)
- else (run false; DebugOn (lev+1))
- else (decr skip; run false; if Int.equal !skip 0 then skipped:=0; DebugOn (lev+1)) in
+ Proofview.tclLIFT !skip >= fun initial_skip ->
+ if Int.equal initial_skip 0 then
+ Proofview.tclLIFT !breakpoint >= fun breakpoint ->
+ if Option.is_empty breakpoint then Proofview.tclTHEN (goal_com tac) (Proofview.tclLIFT (prompt lev))
+ else Proofview.tclLIFT(run false >> return (DebugOn (lev+1)))
+ else Proofview.tclLIFT begin
+ (!skip >>= fun s -> skip:=s-1) >>
+ run false >>
+ !skip >>= fun new_skip ->
+ (if Int.equal new_skip 0 then skipped:=0 else return ()) >>
+ return (DebugOn (lev+1))
+ end in
+ newlevel >= fun newlevel ->
(* What to execute *)
- try f newlevel
- with reraise ->
- skip:=0; skipped:=0;
- if Logic.catchable_exception reraise then
- msg_tac_debug
- (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error reraise);
- raise reraise
-
-let is_debug db = match db, !breakpoint with
-| DebugOff, _ -> false
-| _, Some _ -> false
-| _ -> Int.equal !skip 0
+ Proofview.tclOR
+ (f newlevel)
+ begin fun reraise ->
+ Proofview.tclTHEN
+ (Proofview.tclLIFT begin
+ (skip:=0) >> (skipped:=0) >>
+ if Logic.catchable_exception reraise then
+ msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise)
+ else return ()
+ end)
+ (Proofview.tclZERO reraise)
+ end
+
+let is_debug db =
+ !breakpoint >>= fun breakpoint ->
+ match db, breakpoint with
+ | DebugOff, _ -> return false
+ | _, Some _ -> return false
+ | _ ->
+ !skip >>= fun skip ->
+ return (Int.equal skip 0)
(* Prints a constr *)
let db_constr debug env c =
- if is_debug debug then
+ is_debug debug >>= fun db ->
+ if db then
msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c)
+ else return ()
(* Prints the pattern rule *)
let db_pattern_rule debug num r =
- if is_debug debug then
+ is_debug debug >>= fun db ->
+ if db then
begin
msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
str "|" ++ spc () ++ Hook.get prmatchrl r)
end
+ else return ()
(* Prints the hypothesis pattern identifier if it exists *)
let hyp_bound = function
@@ -171,59 +233,74 @@ let hyp_bound = function
(* Prints a matched hypothesis *)
let db_matched_hyp debug env (id,_,c) ido =
- if is_debug debug then
+ is_debug debug >>= fun db ->
+ if db then
msg_tac_debug (str "Hypothesis " ++
str ((Names.Id.to_string id)^(hyp_bound ido)^
" has been matched: ") ++ print_constr_env env c)
+ else return ()
(* Prints the matched conclusion *)
let db_matched_concl debug env c =
- if is_debug debug then
+ is_debug debug >>= fun db ->
+ if db then
msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c)
+ else return ()
(* Prints a success message when the goal has been matched *)
let db_mc_pattern_success debug =
- if is_debug debug then
+ is_debug debug >>= fun db ->
+ if db then
msg_tac_debug (str "The goal has been successfully matched!" ++ fnl() ++
str "Let us execute the right-hand side part..." ++ fnl())
+ else return ()
(* Prints a failure message for an hypothesis pattern *)
let db_hyp_pattern_failure debug env (na,hyp) =
- if is_debug debug then
+ is_debug debug >>= fun db ->
+ if db then
msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
" cannot match: ") ++
Hook.get prmatchpatt env hyp)
+ else return ()
(* Prints a matching failure message for a rule *)
let db_matching_failure debug =
- if is_debug debug then
+ is_debug debug >>= fun db ->
+ if db then
msg_tac_debug (str "This rule has failed due to matching errors!" ++ fnl() ++
str "Let us try the next one...")
+ else return ()
(* Prints an evaluation failure message for a rule *)
let db_eval_failure debug s =
- if is_debug debug then
+ is_debug debug >>= fun db ->
+ if db then
let s = str "message \"" ++ s ++ str "\"" in
msg_tac_debug
(str "This rule has failed due to \"Fail\" tactic (" ++
s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
+ else return ()
(* Prints a logic failure message for a rule *)
let db_logic_failure debug err =
- if is_debug debug then
+ is_debug debug >>= fun db ->
+ if db then
begin
- msg_tac_debug (!explain_logic_error err);
+ msg_tac_debug (Pervasives.(!) explain_logic_error err) >>
msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++
str "Let us try the next one...")
end
+ else return ()
let is_breakpoint brkname s = match brkname, s with
| Some s, MsgString s'::_ -> String.equal s s'
| _ -> false
let db_breakpoint debug s =
+ !breakpoint >>= fun opt_breakpoint ->
match debug with
- | DebugOn lev when not (List.is_empty s) && is_breakpoint !breakpoint s ->
+ | DebugOn lev when not (List.is_empty s) && is_breakpoint opt_breakpoint s ->
breakpoint:=None
| _ ->
- ()
+ return ()
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 3b9858f16..1ae1a3905 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -31,37 +31,37 @@ type debug_info =
(** Prints the state and waits *)
val debug_prompt :
- int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a
+ int -> glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic
(** Initializes debugger *)
-val db_initialize : unit -> unit
+val db_initialize : unit Proofview.NonLogical.t
(** Prints a constr *)
-val db_constr : debug_info -> env -> constr -> unit
+val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t
(** Prints the pattern rule *)
val db_pattern_rule :
- debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
+ debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t
(** Prints a matched hypothesis *)
val db_matched_hyp :
- debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit
+ debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t
(** Prints the matched conclusion *)
-val db_matched_concl : debug_info -> env -> constr -> unit
+val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t
(** Prints a success message when the goal has been matched *)
-val db_mc_pattern_success : debug_info -> unit
+val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t
(** Prints a failure message for an hypothesis pattern *)
val db_hyp_pattern_failure :
- debug_info -> env -> Name.t * constr_pattern match_pattern -> unit
+ debug_info -> env -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t
(** Prints a matching failure message for a rule *)
-val db_matching_failure : debug_info -> unit
+val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
(** Prints an evaluation failure message for a rule *)
-val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit
+val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t
(** An exception handler *)
val explain_logic_error: (exn -> Pp.std_ppcmds) ref
@@ -73,8 +73,8 @@ val explain_logic_error: (exn -> Pp.std_ppcmds) ref
val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
(** Prints a logic failure message for a rule *)
-val db_logic_failure : debug_info -> exn -> unit
+val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
(** Prints a logic failure message for a rule *)
val db_breakpoint : debug_info ->
- Id.t Loc.located message_token list -> unit
+ Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 07:29:41 +0000