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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: subtac.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
open Global
open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Classops
open List
open Recordops
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern
open Dyn
open Vernacexpr
open Subtac_coercion
open Subtac_utils
open Coqlib
open Printer
open Subtac_errors
open Context
open Eterm
let require_library dirpath =
let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
Library.require_library [qualid] None
(*
let subtac_one_fixpoint env isevars (f, decl) =
let ((id, n, bl, typ, body), decl) =
Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl)
in
let _ =
try trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
Ppconstr.pr_constr_expr body)
with _ -> ()
in ((id, n, bl, typ, body), decl)
*)
let subtac_fixpoint isevars l =
(* TODO: Copy command.build_recursive *)
()
(*
let save id const (locality,kind) hook =
let {const_entry_body = pft;
const_entry_type = tpo;
const_entry_opaque = opacity } = const in
let l,r = match locality with
| Local when Lib.sections_are_opened () ->
let k = logical_kind_of_goal_kind kind in
let c = SectionLocalDef (pft, tpo, opacity) in
let _ = declare_variable id (Lib.cwd(), c, k) in
(Local, VarRef id)
| Local ->
let k = logical_kind_of_goal_kind kind in
let kn = declare_constant id (DefinitionEntry const, k) in
(Global, ConstRef kn)
| Global ->
let k = logical_kind_of_goal_kind kind in
let kn = declare_constant id (DefinitionEntry const, k) in
(Global, ConstRef kn) in
Pfedit.delete_current_proof ();
hook l r;
definition_message id
let save_named opacity =
let id,(const,persistence,hook) = Pfedit.cook_proof () in
let const = { const with const_entry_opaque = opacity } in
save id const persistence hook
let check_anonymity id save_ident =
if atompart_of_id id <> "Unnamed_thm" then
error "This command can only be used for unnamed theorem"
(*
message("Overriding name "^(string_of_id id)^" and using "^save_ident)
*)
let save_anonymous opacity save_ident =
let id,(const,persistence,hook) = Pfedit.cook_proof () in
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
save save_ident const persistence hook
let save_anonymous_with_strength kind opacity save_ident =
let id,(const,_,hook) = Pfedit.cook_proof () in
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
(* we consider that non opaque behaves as local for discharge *)
save save_ident const (Global, Proof kind) hook
let subtac_end_proof = function
| Admitted -> admit ()
| Proved (is_opaque,idopt) ->
if_verbose show_script ();
match idopt with
| None -> save_named is_opaque
| Some ((_,id),None) -> save_anonymous is_opaque id
| Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
*)
open Pp
open Ppconstr
open Decl_kinds
open Tacinterp
open Tacexpr
let start_proof_com env isevars sopt kind (bl,t) hook =
let id = match sopt with
| Some id ->
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
errorlabstrm "start_proof" (pr_id id ++ str " already exists");
id
| None ->
next_global_ident_away false (id_of_string "Unnamed_thm")
(Pfedit.get_all_proof_names ())
in
let evm, c, typ =
Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
in
let _ = Typeops.infer_type env c in
Command.start_proof id kind c hook
let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
let subtac_utils_path =
make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"])
let utils_tac s =
lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s))
let utils_call tac args =
TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
let start_proof_and_print env isevars idopt k t hook =
start_proof_com env isevars idopt k t hook;
print_subgoals ()
(*if !pcoq <> None then (out_some !pcoq).start_proof ()*)
let _ = Subtac_obligations.set_default_tactic
(Tacinterp.eval_tactic (utils_call "subtac_simpl" []))
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
(* check_required_library ["Coq";"Logic";"JMeq"]; *)
require_library "Coq.subtac.FixSub";
require_library "Coq.subtac.Utils";
let env = Global.env () in
let isevars = ref (create_evar_defs Evd.empty) in
try
match command with
VernacDefinition (defkind, (locid, id), expr, hook) ->
(match expr with
ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None
(* let evm, c, ctyp = in *)
(* trace (str "Starting proof"); *)
(* Command.start_proof id goal_kind c hook; *)
(* trace (str "Started proof"); *)
| DefineBody (bl, _, c, tycon) ->
Subtac_pretyping.subtac_proof env isevars id bl c tycon
(* let tac = Eterm.etermtac (evm, c) in *)
(* trace (str "Starting proof"); *)
(* Command.start_proof id goal_kind ctyp hook; *)
(* trace (str "Started proof"); *)
(* Pfedit.by tac) *))
| VernacFixpoint (l, b) ->
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l b)
| VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) ->
if not(Pfedit.refining ()) then
if lettop then
errorlabstrm "Subtac_command.StartProof"
(str "Let declarations can only be used in proof editing mode");
if Lib.is_modtype () then
errorlabstrm "Subtac_command.StartProof"
(str "Proof editing mode not supported in module types");
start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
(*| VernacEndProof e ->
subtac_end_proof e*)
| _ -> user_err_loc (loc,"", str ("Invalid Program command"))
with
| Typing_error e ->
msg_warning (str "Type error in Program tactic:");
let cmds =
(match e with
| NonFunctionalApp (loc, x, mux, e) ->
str "non functional application of term " ++
e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux
| NonSigma (loc, t) ->
str "Term is not of Sigma type: " ++ t
| NonConvertible (loc, x, y) ->
str "Unconvertible terms:" ++ spc () ++
x ++ spc () ++ str "and" ++ spc () ++ y
| IllSorted (loc, t) ->
str "Term is ill-sorted:" ++ spc () ++ t
)
in msg_warning cmds
| Subtyping_error e ->
msg_warning (str "(Program tactic) Subtyping error:");
let cmds =
match e with
| UncoercibleInferType (loc, x, y) ->
str "Uncoercible terms:" ++ spc ()
++ x ++ spc () ++ str "and" ++ spc () ++ y
| UncoercibleInferTerm (loc, x, y, tx, ty) ->
str "Uncoercible terms:" ++ spc ()
++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x
++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y
| UncoercibleRewrite (x, y) ->
str "Uncoercible terms:" ++ spc ()
++ x ++ spc () ++ str "and" ++ spc () ++ y
in msg_warning cmds
| Type_errors.TypeError (env, exn) as e ->
debug 2 (Himsg.explain_type_error env exn);
raise e
| Pretype_errors.PretypeError (env, exn) as e ->
debug 2 (Himsg.explain_pretype_error env exn);
raise e
| (Stdpp.Exc_located (loc, e')) as e ->
debug 2 (str "Parsing exception: ");
(match e' with
| Type_errors.TypeError (env, exn) ->
debug 2 (Himsg.explain_type_error env exn);
raise e
| Pretype_errors.PretypeError (env, exn) ->
debug 2 (Himsg.explain_pretype_error env exn);
raise e
| e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e'');
raise e)
| e ->
msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e);
raise e
|
