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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \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 hyps c ?init_tac terminator =
let goals = [ (Global.env_of_context hyps , c) ] in
Proof_global.start_proof 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 } ->
(id,(constr,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 (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 tac pr =
try
let tac = match with_end_tac with
| None -> tac
| Some etac -> Proofview.tclTHEN tac etac in
let tac = match gi with
| Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
| Vernacexpr.SelectAll -> tac
in
Proof.run_tactic (Global.env ()) tac pr
with
| Proof_global.NoCurrentProof -> Errors.error "No focused proof"
| Proofview.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) 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 sign ?(goal_kind = Global,Proof Theorem) typ tac =
start_proof id goal_kind sign typ (fun _ -> ());
try
let status = by tac in
let _,(const,_) = cook_proof () in
delete_current_proof ();
const, status
with reraise ->
delete_current_proof ();
raise reraise
let build_by_tactic env 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 ce,status = build_constant_by_tactic id sign typ tac in
let ce = Term_typing.handle_side_effects env ce in
let cb, se = Future.force ce.const_entry_body in
assert(Declareops.side_effects_is_empty (Declareops.no_seff));
cb,status
(**********************************************************************)
(* 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) ->
(try fst (build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) [])))
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
|
