summaryrefslogtreecommitdiff
path: root/proofs/pfedit.ml
blob: 5e3140690436eb591cbe7b50fa3f11a92e5656b3 (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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
(************************************************************************)
(*  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 Nameops
open Sign
open Term
open Declarations
open Entries
open Environ
open Evd
open Typing
open Refiner
open Tacexpr
open Proof_type
open Lib
open Safe_typing

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 undo n =
  let p = Proof_global.give_me_the_proof () in
  let d = Proof.V82.depth p in
  if n >= d then raise Proof.EmptyUndoStack;
  for i = 1 to n do
    Proof.undo p
  done

let current_proof_depth () =
  try
    let p = Proof_global.give_me_the_proof () in
    Proof.V82.depth p
  with Proof_global.NoCurrentProof -> -1

(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
   is the depth of the focus stack). *)
let undo_todepth n =
  try
    undo ((current_proof_depth ()) - n )
  with Proof_global.NoCurrentProof  when n=0 -> ()

let set_undo _ = ()
let get_undo _ = None


let start_proof id str hyps c ?init_tac ?compute_guard hook = 
  let goals = [ (Global.env_of_context hyps , c) ] in
  let init_tac = Option.map Proofview.V82.tactic init_tac in
  Proof_global.start_proof id str goals ?compute_guard hook;
  try Option.iter Proof_global.run_tactic init_tac
  with e -> Proof_global.discard_current (); raise e

let restart_proof () = undo_todepth 1

let cook_proof hook =
  let prf = Proof_global.give_me_the_proof () in
  hook prf;
  match Proof_global.close_proof () with
  | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
  | _ -> Util.anomaly "Pfedit.cook_proof: more than one proof term."

let xml_cook_proof = ref (fun _ -> ())
let set_xml_cook_proof f = xml_cook_proof := f

let get_pftreestate () =
  Proof_global.give_me_the_proof ()

let set_end_tac tac =
  let tac = Proofview.V82.tactic tac in
  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 -> Util.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 -> Util.error "No focused proof."

let get_goal_context i =
  try get_goal_context_gen i
  with NoSuchGoal -> Util.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,hook)) -> id,strength,concl,hook
    | _ -> Util.anomaly "Pfedit.current_proof_statement: more than one statement"

let solve_nth ?(with_end_tac=false) gi tac = 
  try 
    let tac = Proofview.V82.tactic tac in
    let tac = if with_end_tac then 
                Proof_global.with_end_tac tac
              else
		tac
    in
    Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac) 
  with 
    | Proof_global.NoCurrentProof  -> Util.error "No focused proof"
    | Proofview.IndexOutOfRange | Failure "list_chop" -> 
	let msg = str "No such goal: " ++ int gi ++ str "." in
	Util.errorlabstrm "" msg

let by = solve_nth 1

let instantiate_nth_evar_com n com = 
  let pf = Proof_global.give_me_the_proof () in
  Proof.V82.instantiate_evar n com pf


(**********************************************************************)
(* 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 typ tac =
  start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
  try
    by tac;
    let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
    delete_current_proof ();
    const
  with e ->
    delete_current_proof ();
    raise e

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
  (build_constant_by_tactic id sign typ tac).const_entry_body

(**********************************************************************)
(* 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 solve_by_implicit_tactic env sigma (evk,args) =
  let evi = Evd.find_undefined sigma evk in
  match (!implicit_tactic, snd (evar_source evk sigma)) with
  | Some tac, (ImplicitArg _ | QuestionMark _)
      when
	Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
	(Environ.named_context env) ->
      (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac)
       with e when Logic.catchable_exception e -> raise Exit)
  | _ -> raise Exit