blob: 92d4089015c5f8989733f6f03a1993c7bb362df3 (
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
127
128
129
130
131
132
133
134
135
136
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Term
open Evd
open CErrors
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 split_tree=
Skip_patt of Id.Set.t * split_tree
| Split_patt of Id.Set.t * inductive *
(bool array * (Id.Set.t * split_tree) option) array
| Close_patt of split_tree
| End_patt of (Id.t * (int * 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 * Id.t list
| Suppose_case
| Claim
| Focus_claim
type pm_info =
{ pm_stack : stack_info list}
let info = Store.field ()
(* Current proof mode *)
type command_mode =
Mode_tactic
| Mode_proof
| Mode_none
let mode_of_pftreestate pts =
(* spiwack: it used to be "top_goal_..." but this should be fine *)
let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
let goal = List.hd goals in
match Store.get (Goal.V82.extra sigma goal) info with
| None -> Mode_tactic
| Some _ -> Mode_proof
let get_current_mode () =
try
mode_of_pftreestate (Pfedit.get_pftreestate ())
with Proof_global.NoCurrentProof -> Mode_none
let check_not_proof_mode str =
match get_current_mode () with
| Mode_proof -> error str
| _ -> ()
let get_info sigma gl=
match Store.get (Goal.V82.extra sigma gl) info with
| None -> invalid_arg "get_info"
| Some pm -> pm
let try_get_info sigma gl =
Store.get (Goal.V82.extra sigma gl) info
let get_goal_stack pts =
let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
let info = get_info sigma (List.hd goals) in
info.pm_stack
let proof_focus = Proof.new_focus_kind ()
let proof_cond = Proof.done_cond proof_focus
let focus p =
let inf = get_goal_stack p in
Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
let unfocus () =
Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
let get_top_stack pts =
try
Proof.get_at_focus proof_focus pts
with Proof.NoSuchFocus ->
let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in
let info = get_info sigma gl in
info.pm_stack
let get_stack pts = Proof.get_at_focus proof_focus pts
let get_last env = match Environ.named_context env with
| decl :: _ -> Context.Named.Declaration.get_id decl
| [] -> error "no previous statement to use"
let get_end_command pts =
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 (Pp.str"lonely suppose")
|
