Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

file 177 lines (144 sloc) 5.919 kb
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
(************************************************************************)
(* 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 Entries
open Environ
open Evd
open Refiner

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 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))
  | _ -> Errors.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 -> Errors.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 -> Errors.error "No focused proof."

let get_goal_context i =
  try get_goal_context_gen i
  with NoSuchGoal -> Errors.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
    | _ -> Errors.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 -> Errors.error "No focused proof"
    | Proofview.IndexOutOfRange | Failure "List.chop" ->
let msg = str "No such goal: " ++ int gi ++ str "." in
Errors.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, (Evar_kinds.ImplicitArg _ | Evar_kinds.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
Something went wrong with that request. Please try again.