Imported Upstream version 8.5~beta1+dfsg

1 files changed, 84 insertions, 95 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 77e7b324..fdc93bcb 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,19 +9,9 @@
 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
@@ -35,58 +25,28 @@ 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 start_proof (id : Id.t) str sigma hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof id str goals ?compute_guard hook;
-  let tac = match init_tac with
-   | Some tac -> Proofview.V82.tactic tac
-   | None -> Proofview.tclUNIT ()
-  in
-  try Proof_global.run_tactic tac
-  with reraise -> Proof_global.discard_current (); raise reraise
-
-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
-
+  Proof_global.start_proof sigma id str goals terminator;
+  let env = Global.env () in
+  ignore (Proof_global.with_current_proof (fun _ p ->
+    match init_tac with
+    | None -> p,(true,[])
+    | Some tac -> Proof.run_tactic env tac p))
+
+let cook_this_proof p =
+  match p with
+  | { Proof_global.id;entries=[constr];persistence;universes } ->
+      (id,(constr,universes,persistence))
+  | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
+
+let cook_proof () =
+  cook_this_proof (fst
+    (Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)))
 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 =
@@ -96,25 +56,25 @@ let get_used_variables () =
 
 exception NoSuchGoal
 let _ = Errors.register_handler begin function
-  | NoSuchGoal -> Util.error "No such goal."
+  | 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
+  let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
   try
-    { it=(List.nth goals (i-1)) ; sigma=sigma }
+          { 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 { 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 -> Util.error "No such goal."
+  with NoSuchGoal -> Errors.error "No such goal."
 
 let get_current_goal_context () =
   try get_goal_context_gen 1
@@ -125,29 +85,44 @@ let get_current_goal_context () =
 
 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"
+    | (id,([concl],strength)) -> id,strength,concl
+    | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
 
-let solve_nth ?(with_end_tac=false) gi tac = 
+let solve ?with_end_tac gi info_lvl tac pr =
   try 
-    let tac = Proofview.V82.tactic tac in
-    let tac = if with_end_tac then 
-                Proof_global.with_end_tac tac
-              else
-		tac
+    let tac = match with_end_tac with
+      | None -> tac
+      | Some etac -> Proofview.tclTHEN tac etac in
+    let tac = match info_lvl with
+      | None -> tac
+      | Some _ -> Proofview.Trace.record_info_trace 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 tac = match gi with
+      | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
+      | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
+      | Vernacexpr.SelectAll -> tac
+      | Vernacexpr.SelectAllParallel ->
+          Errors.anomaly(str"SelectAllParallel not handled by Stm")
+    in
+    let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
+    let () =
+      match info_lvl with
+      | None -> ()
+      | Some i -> Pp.ppnl (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+    in
+    (p,status)
+  with
+    | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
+    | CList.IndexOutOfRange ->
+        match gi with
+	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
+	                            Errors.errorlabstrm "" msg
+        | _ -> assert false
 
-let by = solve_nth 1
+let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
 
 let instantiate_nth_evar_com n com = 
-  let pf = Proof_global.give_me_the_proof () in
-  Proof.V82.instantiate_evar n com pf
+  Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
 
 
 (**********************************************************************)
@@ -157,21 +132,29 @@ 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 _ _ -> ());
+let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
+  let evd = Evd.from_env ~ctx Environ.empty_env in
+  start_proof id goal_kind evd sign typ (fun _ -> ());
   try
-    by tac;
-    let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
+    let status = by tac in
+    let _,(const,univs,_) = cook_proof () in
     delete_current_proof ();
-    const
+    const, status, univs
   with reraise ->
+    let reraise = Errors.push reraise in
     delete_current_proof ();
-    raise reraise
+    iraise reraise
 
-let build_by_tactic env typ tac =
-  let id = id_of_string ("temporary_proof"^string_of_int (next())) in
+let build_by_tactic env ctx ?(poly=false) 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
+  let gk = Global, poly, Proof Theorem in
+  let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
+  let ce = Term_typing.handle_entry_side_effects env ce in
+  let (cb, ctx), se = Future.force ce.const_entry_body in
+  assert(Declareops.side_effects_is_empty se);
+  assert(Univ.ContextSet.is_empty ctx);
+  cb, status, univs
 
 (**********************************************************************)
 (* Support for resolution of evars in tactic interpretation, including
@@ -181,13 +164,19 @@ let implicit_tactic = ref None
 
 let declare_implicit_tactic tac = implicit_tactic := Some tac
 
-let solve_by_implicit_tactic env sigma (evk,args) =
+let clear_implicit_tactic () = implicit_tactic := None
+
+let solve_by_implicit_tactic env sigma evk =
   let evi = Evd.find_undefined sigma evk in
   match (!implicit_tactic, snd (evar_source evk sigma)) with
-  | Some tac, (ImplicitArg _ | QuestionMark _)
+  | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
       when
-	Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
+	Context.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)
+      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
+      (try
+        let (ans, _, _) = 
+	  build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in
+        ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit