blob: cdb7b0675e59338a5ac200fd0b50a13072512179 (
plain)
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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id:$ i*)
open Names
open Term
open Evd
open Util
let daimon_flag = ref false
let set_daimon_flag () = daimon_flag:=true
let clear_daimon_flag () = daimon_flag:=false
let get_daimon_flag () = !daimon_flag
type command_mode =
Mode_tactic
| Mode_proof
| Mode_none
let mode_of_pftreestate pts =
let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in
if goal.evar_extra = None then
Mode_tactic
else
Mode_proof
let get_current_mode () =
try
mode_of_pftreestate (Pfedit.get_pftreestate ())
with _ -> Mode_none
let check_not_proof_mode str =
if get_current_mode () = Mode_proof then
error str
type split_tree=
Skip_patt of Idset.t * split_tree
| Split_patt of Idset.t * inductive *
(bool array * (Idset.t * split_tree) option) array
| Close_patt of split_tree
| End_patt of (identifier * int)
type elim_kind =
EK_dep of split_tree
| EK_nodep
| EK_unknown
type recpath = int option*Declarations.wf_paths
type per_info =
{per_casee:constr;
per_ctype:types;
per_ind:inductive;
per_pred:constr;
per_args:constr list;
per_params:constr list;
per_nparams:int;
per_wf:recpath}
type stack_info =
Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
| Suppose_case
| Claim
| Focus_claim
type pm_info =
{ pm_stack : stack_info list}
let pm_in,pm_out = Dyn.create "pm_info"
let get_info gl=
match gl.evar_extra with
None -> invalid_arg "get_info"
| Some extra ->
try pm_out extra with _ -> invalid_arg "get_info"
let get_stack pts =
let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in
info.pm_stack
let get_top_stack pts =
let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in
info.pm_stack
let get_end_command pts =
match mode_of_pftreestate pts with
Mode_proof ->
Some
begin
match get_top_stack pts with
[] -> "\"end proof\""
| Claim::_ -> "\"end claim\""
| Focus_claim::_-> "\"end focus\""
| (Suppose_case :: Per (et,_,_,_) :: _
| Per (et,_,_,_) :: _ ) ->
begin
match et with
Decl_expr.ET_Case_analysis ->
"\"end cases\" or start a new case"
| Decl_expr.ET_Induction ->
"\"end induction\" or start a new case"
end
| _ -> anomaly "lonely suppose"
end
| Mode_tactic ->
begin
try
ignore
(Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts);
Some "\"return\""
with Not_found -> None
end
| Mode_none ->
error "no proof in progress"
let get_last env =
try
let (id,_,_) = List.hd (Environ.named_context env) in id
with Invalid_argument _ -> error "no previous statement to use"
|
