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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Util
open Names
open Entries
open Environ
open Evd
let refining = Proof_global.there_are_pending_proofs
let check_no_pending_proofs = Proof_global.check_no_pending_proof
let get_current_proof_name = Proof_global.get_current_proof_name
let get_all_proof_names = Proof_global.get_all_proof_names
type lemma_possible_guards = Proof_global.lemma_possible_guards
let delete_proof = Proof_global.discard
let delete_current_proof = Proof_global.discard_current
let delete_all_proofs = Proof_global.discard_all
let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator =
let goals = [ (Global.env_of_context hyps , c) ] in
Proof_global.start_proof sigma id str goals terminator;
let env = Global.env () in
ignore (Proof_global.with_current_proof (fun _ p ->
match init_tac with
| None -> p,(true,[])
| Some tac -> Proof.run_tactic env tac p))
let cook_this_proof p =
match p with
| { Proof_global.id;entries=[constr];persistence;universes } ->
(id,(constr,universes,persistence))
| _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
let cook_proof () =
cook_this_proof (fst
(Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)))
let get_pftreestate () =
Proof_global.give_me_the_proof ()
let set_end_tac tac =
Proof_global.set_endline_tactic tac
let set_used_variables l =
Proof_global.set_used_variables l
let get_used_variables () =
Proof_global.get_used_variables ()
exception NoSuchGoal
let _ = Errors.register_handler begin function
| NoSuchGoal -> Errors.error "No such goal."
| _ -> raise Errors.Unhandled
end
let get_nth_V82_goal i =
let p = Proof_global.give_me_the_proof () in
let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
try
{ it=(List.nth goals (i-1)) ; sigma=sigma; }
with Failure _ -> raise NoSuchGoal
let get_goal_context_gen i =
try
let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in
(sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
let get_goal_context i =
try get_goal_context_gen i
with NoSuchGoal -> Errors.error "No such goal."
let get_current_goal_context () =
try get_goal_context_gen 1
with NoSuchGoal ->
(* spiwack: returning empty evar_map, since if there is no goal, under focus,
there is no accessible evar either *)
(Evd.empty, Global.env ())
let current_proof_statement () =
match Proof_global.V82.get_current_initial_conclusions () with
| (id,([concl],strength)) -> id,strength,concl
| _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
let solve ?with_end_tac gi info_lvl tac pr =
try
let tac = match with_end_tac with
| None -> tac
| Some etac -> Proofview.tclTHEN tac etac in
let tac = match info_lvl with
| None -> tac
| Some _ -> Proofview.Trace.record_info_trace tac
in
let tac = match gi with
| Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
| Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
| Vernacexpr.SelectAll -> tac
| Vernacexpr.SelectAllParallel ->
Errors.anomaly(str"SelectAllParallel not handled by Stm")
in
let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
let () =
match info_lvl with
| None -> ()
| Some i -> Pp.ppnl (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
in
(p,status)
with
| Proof_global.NoCurrentProof -> Errors.error "No focused proof"
| CList.IndexOutOfRange ->
match gi with
| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
Errors.errorlabstrm "" msg
| _ -> assert false
let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
let instantiate_nth_evar_com n com =
Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
(**********************************************************************)
(* Shortcut to build a term using tactics *)
open Decl_kinds
let next = let n = ref 0 in fun () -> incr n; !n
let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
let evd = Evd.from_env ~ctx Environ.empty_env in
start_proof id goal_kind evd sign typ (fun _ -> ());
try
let status = by tac in
let _,(const,univs,_) = cook_proof () in
delete_current_proof ();
const, status, univs
with reraise ->
let reraise = Errors.push reraise in
delete_current_proof ();
iraise reraise
let build_by_tactic env ctx ?(poly=false) typ tac =
let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = val_of_named_context (named_context env) in
let gk = Global, poly, Proof Theorem in
let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
let ce = Term_typing.handle_entry_side_effects env ce in
let (cb, ctx), se = Future.force ce.const_entry_body in
assert(Declareops.side_effects_is_empty se);
assert(Univ.ContextSet.is_empty ctx);
cb, status, univs
(**********************************************************************)
(* Support for resolution of evars in tactic interpretation, including
resolution by application of tactics *)
let implicit_tactic = ref None
let declare_implicit_tactic tac = implicit_tactic := Some tac
let clear_implicit_tactic () = implicit_tactic := None
let solve_by_implicit_tactic env sigma evk =
let evi = Evd.find_undefined sigma evk in
match (!implicit_tactic, snd (evar_source evk sigma)) with
| Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
when
Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
(try
let (ans, _, _) =
build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in
ans
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
|
