← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to proofs/tactic_debug.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
proofs/tactic_debug.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: tactic_debug.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
10
 
 
11
open Names
 
12
open Constrextern
 
13
open Pp
 
14
open Tacexpr
 
15
open Termops
 
16
 
 
17
let prtac = ref (fun _ -> assert false)
 
18
let set_tactic_printer f = prtac := f
 
19
let prmatchpatt = ref (fun _ _ -> assert false)
 
20
let set_match_pattern_printer f = prmatchpatt := f
 
21
let prmatchrl = ref (fun _ -> assert false)
 
22
let set_match_rule_printer f = prmatchrl := f
 
23
 
 
24
(* This module intends to be a beginning of debugger for tactic expressions.
 
25
   Currently, it is quite simple and we can hope to have, in the future, a more
 
26
   complete panel of commands dedicated to a proof assistant framework *)
 
27
 
 
28
(* Debug information *)
 
29
type debug_info =
 
30
  | DebugOn of int
 
31
  | DebugOff
 
32
 
 
33
(* An exception handler *)
 
34
let explain_logic_error = ref (fun e -> mt())
 
35
 
 
36
let explain_logic_error_no_anomaly = ref (fun e -> mt())
 
37
 
 
38
(* Prints the goal *)
 
39
let db_pr_goal g =
 
40
  msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g))
 
41
 
 
42
(* Prints the commands *)
 
43
let help () =
 
44
  msgnl (str "Commands: <Enter>=Continue" ++ fnl() ++
 
45
         str "          h/?=Help" ++ fnl() ++
 
46
         str "          r<num>=Run <num> times" ++ fnl() ++
 
47
         str "          s=Skip" ++ fnl() ++
 
48
         str "          x=Exit")
 
49
 
 
50
(* Prints the goal and the command to be executed *)
 
51
let goal_com g tac =
 
52
  begin
 
53
    db_pr_goal g;
 
54
    msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ())
 
55
  end
 
56
 
 
57
(* Gives the number of a run command *)
 
58
let run_com inst =
 
59
  if (String.get inst 0)='r' then
 
60
    let num = int_of_string (String.sub inst 1 ((String.length inst)-1)) in
 
61
    if num>0 then num
 
62
    else raise (Invalid_argument "run_com")
 
63
  else
 
64
    raise (Invalid_argument "run_com")
 
65
 
 
66
let allskip = ref 0
 
67
let skip = ref 0
 
68
 
 
69
(* Prints the run counter *)
 
70
let run ini =
 
71
  if not ini then 
 
72
    for i=1 to 2 do
 
73
      print_char (Char.chr 8);print_char (Char.chr 13)
 
74
    done;
 
75
  msg (str "Executed expressions: " ++ int (!allskip - !skip) ++ 
 
76
       fnl() ++ fnl())
 
77
 
 
78
(* Prints the prompt *)
 
79
let rec prompt level =
 
80
  begin
 
81
    msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
 
82
    flush stdout;
 
83
    let exit () = skip:=0;allskip:=0;raise Sys.Break in
 
84
    let inst = try read_line () with End_of_file -> exit () in
 
85
    match inst with
 
86
    | ""  -> true
 
87
    | "s" -> false
 
88
    | "x" -> print_char (Char.chr 8); exit ()
 
89
    | "h"| "?" ->
 
90
      begin
 
91
        help ();
 
92
        prompt level
 
93
      end
 
94
    | _ ->
 
95
      (try let ctr=run_com inst in skip:=ctr;allskip:=ctr;run true;true
 
96
       with Failure _ | Invalid_argument _ -> prompt level)
 
97
  end
 
98
 
 
99
(* Prints the state and waits for an instruction *)
 
100
let debug_prompt lev g tac f =
 
101
  (* What to print and to do next *)
 
102
  let continue =
 
103
    if !skip = 0 then (goal_com g tac; prompt lev)
 
104
    else (decr skip; run false; if !skip=0 then allskip:=0; true) in
 
105
  (* What to execute *)
 
106
  try f (if continue then DebugOn (lev+1) else DebugOff)
 
107
  with e ->
 
108
    skip:=0; allskip:=0;
 
109
    if Logic.catchable_exception e then
 
110
      ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
 
111
    raise e
 
112
 
 
113
(* Prints a constr *)
 
114
let db_constr debug env c =
 
115
  if debug <> DebugOff & !skip = 0 then
 
116
    msgnl (str "Evaluated term: " ++ print_constr_env env c)
 
117
 
 
118
(* Prints the pattern rule *)
 
119
let db_pattern_rule debug num r =
 
120
  if debug <> DebugOff & !skip = 0 then
 
121
  begin
 
122
    msgnl (str "Pattern rule " ++ int num ++ str ":");
 
123
    msgnl (str "|" ++ spc () ++ !prmatchrl r)
 
124
  end
 
125
 
 
126
(* Prints the hypothesis pattern identifier if it exists *)
 
127
let hyp_bound = function
 
128
  | Anonymous -> " (unbound)"
 
129
  | Name id -> " (bound to "^(Names.string_of_id id)^")"
 
130
 
 
131
(* Prints a matched hypothesis *)
 
132
let db_matched_hyp debug env (id,_,c) ido =
 
133
  if debug <> DebugOff & !skip = 0 then
 
134
    msgnl (str "Hypothesis " ++
 
135
           str ((Names.string_of_id id)^(hyp_bound ido)^
 
136
                " has been matched: ") ++ print_constr_env env c)
 
137
 
 
138
(* Prints the matched conclusion *)
 
139
let db_matched_concl debug env c =
 
140
  if debug <> DebugOff & !skip = 0 then
 
141
    msgnl (str "Conclusion has been matched: " ++ print_constr_env env c)
 
142
 
 
143
(* Prints a success message when the goal has been matched *)
 
144
let db_mc_pattern_success debug =
 
145
  if debug <> DebugOff & !skip = 0 then
 
146
    msgnl (str "The goal has been successfully matched!" ++ fnl() ++
 
147
           str "Let us execute the right-hand side part..." ++ fnl())
 
148
 
 
149
let pp_match_pattern env = function
 
150
  | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c)
 
151
  | Subterm (b,o,c) ->
 
152
    Subterm (b,o,(extern_constr_pattern (names_of_rel_context env) c))
 
153
 
 
154
(* Prints a failure message for an hypothesis pattern *)
 
155
let db_hyp_pattern_failure debug env (na,hyp) =
 
156
  if debug <> DebugOff & !skip = 0 then
 
157
    msgnl (str ("The pattern hypothesis"^(hyp_bound na)^
 
158
                " cannot match: ") ++
 
159
           !prmatchpatt env hyp)
 
160
 
 
161
(* Prints a matching failure message for a rule *)
 
162
let db_matching_failure debug =
 
163
  if debug <> DebugOff & !skip = 0 then
 
164
    msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++
 
165
           str "Let us try the next one...")
 
166
 
 
167
(* Prints an evaluation failure message for a rule *)
 
168
let db_eval_failure debug s =
 
169
  if debug <> DebugOff & !skip = 0 then
 
170
    let s = str "message \"" ++ s ++ str "\"" in
 
171
    msgnl 
 
172
      (str "This rule has failed due to \"Fail\" tactic (" ++
 
173
       s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
 
174
 
 
175
(* Prints a logic failure message for a rule *)
 
176
let db_logic_failure debug err =
 
177
  if debug <> DebugOff & !skip = 0 then
 
178
  begin
 
179
    msgnl (!explain_logic_error err);
 
180
    msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++
 
181
           str "Let us try the next one...")
 
182
  end