summaryrefslogtreecommitdiff
path: root/proofs/decl_mode.ml
blob: 134a4d8b00e2678331913b11a9e3ee5a1cb21197 (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
(************************************************************************)
(*  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: decl_mode.ml 12422 2009-10-27 08:42:49Z corbinea $ 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 * 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"