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
|
(************************************************************************)
(* 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$ *)
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 Scoq
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) =
Interp_fixpoint.rewrite_fixpoint env [] (f, decl)
in
let _ = trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
Ppconstr.pr_constr_expr body)
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
*)
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
require_library "Coq.subtac.FixSub";
try
match command with
VernacDefinition (defkind, (locid, id), expr, hook) ->
let env = Global.env () in
let isevars = ref (create_evar_defs Evd.empty) in
(match expr with
ProveBody (bl, c) ->
let evm, c, ctyp = Interp.subtac_process env isevars id bl c None in
trace (str "Starting proof");
Command.start_proof id goal_kind c hook;
trace (str "Started proof");
| DefineBody (bl, _, c, tycon) ->
let evm, c, ctyp = Interp.subtac_process env isevars id bl c tycon in
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)
(*| 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, e) ->
debug 2 (Himsg.explain_type_error env e)
| Pretype_errors.PretypeError (env, e) ->
debug 2 (Himsg.explain_pretype_error env e)
| Stdpp.Exc_located (loc, e) ->
debug 2 (str "Parsing exception: ");
(match e with
| Type_errors.TypeError (env, e) ->
debug 2 (Himsg.explain_type_error env e)
| Pretype_errors.PretypeError (env, e) ->
debug 2 (Himsg.explain_pretype_error env e)
| e -> msg_warning (str "Unexplained exception: " ++ Cerrors.explain_exn e))
| e ->
msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e)
|
