aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/decl_mode/decl_mode.ml
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")