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
|
(************************************************************************)
(* 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 11309 2008-08-06 10:30:35Z herbelin $ *)
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 Eterm
let require_library dirpath =
let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
Library.require_library [qualid] None
open Pp
open Ppconstr
open Decl_kinds
open Tacinterp
open Tacexpr
let solve_tccs_in_type env id isevars evm c typ =
if not (evm = Evd.empty) then
let stmt_id = Nameops.add_suffix id "_stmt" in
let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in
(** Make all obligations transparent so that real dependencies can be sorted out by the user *)
let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in
match Subtac_obligations.add_definition stmt_id c' typ obls with
Subtac_obligations.Defined cst -> constant_value (Global.env())
(match cst with ConstRef kn -> kn | _ -> assert false)
| _ ->
errorlabstrm "start_proof"
(str "The statement obligations could not be resolved automatically, " ++ spc () ++
str "write a statement definition first.")
else
let _ = Typeops.infer_type env c in c
let start_proof_com env isevars sopt kind (bl,t) hook =
let id = match sopt with
| Some (loc,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
user_err_loc (loc,"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, _imps =
Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
in
let c = solve_tccs_in_type env id isevars evm c typ in
Command.start_proof id kind c hook
let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
let start_proof_and_print env isevars idopt k t hook =
start_proof_com env isevars idopt k t hook;
print_subgoals ()
let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
let assumption_message id =
Flags.if_verbose message ((string_of_id id) ^ " is assumed")
let declare_assumption env isevars idl is_coe k bl c nl =
if not (Pfedit.refining ()) then
let id = snd (List.hd idl) in
let evm, c, typ, imps =
Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None
in
let c = solve_tccs_in_type env id isevars evm c typ in
List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl
else
errorlabstrm "Command.Assumption"
(str "Cannot declare an assumption while in proof editing mode.")
let dump_definition (loc, id) s =
Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id))
let dump_constraint ty ((loc, n), _, _) =
match n with
| Name id -> dump_definition (loc, id) ty
| Anonymous -> ()
let dump_variable lid = ()
let vernac_assumption env isevars kind l nl =
let global = fst kind = Global in
List.iter (fun (is_coe,(idl,c)) ->
if !Flags.dump then
List.iter (fun lid ->
if global then dump_definition lid "ax"
else dump_variable lid) idl;
declare_assumption env isevars idl is_coe kind [] c nl) l
let check_fresh (loc,id) =
if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
user_err_loc (loc,"",pr_id id ++ str " already exists")
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
check_required_library ["Coq";"Program";"Tactics"];
let env = Global.env () in
let isevars = ref (create_evar_defs Evd.empty) in
try
match command with
| VernacDefinition (defkind, (_, id as lid), expr, hook) ->
check_fresh lid;
dump_definition lid "def";
(match expr with
| ProveBody (bl, t) ->
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 lid) (Global, DefinitionBody Definition) (bl,t)
(fun _ _ -> ())
| DefineBody (bl, _, c, tycon) ->
ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon))
| VernacFixpoint (l, b) ->
List.iter (fun ((lid, _, _, _, _), _) ->
check_fresh lid;
dump_definition lid "fix") l;
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l b)
| VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
if !Flags.dump then dump_definition id "prf";
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");
check_fresh id;
start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
| VernacAssumption (stre,nl,l) ->
vernac_assumption env isevars stre l nl
| VernacInstance (glob, sup, is, props, pri) ->
if !Flags.dump then dump_constraint "inst" is;
ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
| VernacCoFixpoint (l, b) ->
List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l;
ignore(Subtac_command.build_corecursive l b)
(*| 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
| Cases.PatternMatchingError (env, exn) as e ->
debug 2 (Himsg.explain_pattern_matching_error env exn);
raise e
| 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, Proof_type.LtacLocated (_,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
|
