Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 427 insertions, 0 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
new file mode 100644
index 00000000..2745270a
--- /dev/null
+++ b/proofs/proof_global.ml
@@ -0,0 +1,427 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(***********************************************************************)
+(*                                                                     *)
+(*      This module defines proof facilities relevant to the           *)
+(*      toplevel. In particular it defines the global proof            *)
+(*      environment.                                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+open Pp
+open Names
+
+(*** Proof Modes ***)
+
+(* Type of proof modes :
+    - A function [set] to set it *from standard mode*
+    - A function [reset] to reset the *standard mode* from it *)
+type proof_mode = {
+  name : string ;
+  set : unit -> unit ;
+  reset : unit -> unit
+}
+
+let proof_modes = Hashtbl.create 6
+let find_proof_mode n =
+  try Hashtbl.find proof_modes n
+  with Not_found ->
+    Util.error (Format.sprintf "No proof mode named \"%s\"." n)
+
+let register_proof_mode ({ name = n } as m) = Hashtbl.add proof_modes n m
+(* initial mode: standard mode *)
+let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
+let _ = register_proof_mode standard
+
+(* Default proof mode, to be set at the beginning of proofs. *)
+let default_proof_mode = ref standard
+
+let _ =
+  Goptions.declare_string_option {Goptions.
+    optsync = true ;
+    optdepr = false;
+    optname = "default proof mode" ;
+    optkey = ["Default";"Proof";"Mode"] ;
+    optread = begin fun () -> 
+                               let { name = name } = !default_proof_mode in name 
+                     end;
+    optwrite = begin fun n -> 
+                                default_proof_mode := find_proof_mode n
+                      end
+  }
+
+(*** Proof Global Environment ***)
+
+(* local shorthand *)
+type nproof = identifier*Proof.proof
+
+(* Extra info on proofs. *)
+type lemma_possible_guards = int list list
+type proof_info = { 
+  strength : Decl_kinds.goal_kind ;
+  compute_guard :  lemma_possible_guards; 
+  hook :Tacexpr.declaration_hook ;
+  mode : proof_mode
+}
+
+(* Invariant: a proof is at most in one of current_proof and suspended. And the 
+   domain of proof_info is the union of that of current_proof and suspended.*)
+(* The head of [!current_proof] is the actual current proof, the other ones are to
+    be resumed when the current proof is closed, aborted or suspended. *)
+let current_proof = ref ([]:nproof list)
+let suspended = ref ([] : nproof list)
+let proof_info = ref (Idmap.empty : proof_info Idmap.t)
+
+(* Current proof_mode, for bookkeeping *)
+let current_proof_mode = ref !default_proof_mode
+
+(* combinators for proof modes *)
+let update_proof_mode () = 
+  match !current_proof with
+  | (id,_)::_ ->  
+      let { mode = m } = Idmap.find id !proof_info in
+      !current_proof_mode.reset ();
+      current_proof_mode := m;
+      !current_proof_mode.set ()
+  | _ -> 
+      !current_proof_mode.reset (); 
+      current_proof_mode := standard
+
+(* combinators for the current_proof and suspended lists *)
+let push a l = l := a::!l;
+  update_proof_mode ()
+
+exception NoSuchProof
+let _ = Errors.register_handler begin function
+  | NoSuchProof -> Util.error "No such proof."
+  | _ -> raise Errors.Unhandled
+end
+let rec extract id l = 
+  let rec aux = function
+    | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l)
+    | np::l -> let (np', l) = aux l in (np' , np::l)
+    | [] -> raise NoSuchProof
+  in
+  let (np,l') = aux !l in
+  l := l';
+  update_proof_mode ();
+  np
+
+exception NoCurrentProof
+let _ = Errors.register_handler begin function
+  | NoCurrentProof -> Util.error "No focused proof (No proof-editing in progress)."
+  | _ -> raise Errors.Unhandled
+end
+let extract_top l =
+  match !l with
+  | np::l' -> l := l' ; update_proof_mode (); np
+  | [] -> raise NoCurrentProof	
+let find_top l =
+  match !l with
+  | np::_ -> np
+  | [] -> raise NoCurrentProof
+
+let rotate_top l1 l2 =
+  let np = extract_top l1 in
+  push np l2
+
+let rotate_find id l1 l2 =
+  let np = extract id l1 in
+  push np l2
+  
+
+(* combinators for the proof_info map *)
+let add id info m =
+  m := Idmap.add id info !m
+let remove id m =
+  m := Idmap.remove id !m
+
+(*** Proof Global manipulation ***)
+
+let get_all_proof_names () =
+    List.map fst !current_proof @
+    List.map fst !suspended
+
+let give_me_the_proof () = 
+  snd (find_top current_proof)
+
+let get_current_proof_name () =
+  fst (find_top current_proof)
+
+(* spiwack: it might be considered to move error messages away.
+    Or else to remove special exceptions from Proof_global.
+    Arguments for the former: there is no reason Proof_global is only
+    accessed directly through vernacular commands. Error message should be 
+   pushed to external layers, and so we should be able to have a finer
+   control on error message on complex actions. *)
+let msg_proofs use_resume =
+  match get_all_proof_names () with
+    | [] -> (spc () ++ str"(No proof-editing in progress).")
+    | l ->  (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
+               (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l) ++
+	       str"." ++
+               (if use_resume then (fnl () ++ str"Use \"Resume\" first.")
+              	else (mt ()))
+	    )
+
+
+let there_is_a_proof () = !current_proof <> []
+let there_are_suspended_proofs () = !suspended <> []
+let there_are_pending_proofs () = 
+  there_is_a_proof () || 
+  there_are_suspended_proofs ()
+let check_no_pending_proof () = 
+  if not (there_are_pending_proofs ()) then
+    ()
+  else begin
+    Util.error (Pp.string_of_ppcmds
+      (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++
+       str"Use \"Abort All\" first or complete proof(s)."))
+  end
+
+
+let suspend () =
+  rotate_top current_proof suspended
+
+let resume_last () =
+  rotate_top suspended current_proof
+
+let resume id =
+  rotate_find id suspended current_proof
+
+let discard_gen id =
+  try 
+    ignore (extract id current_proof);
+    remove id proof_info
+  with NoSuchProof -> ignore (extract id suspended)
+
+let discard (loc,id) = 
+  try
+    discard_gen id
+  with NoSuchProof ->
+    Util.user_err_loc
+      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
+
+let discard_current () =
+  let (id,_) = extract_top current_proof in
+  remove id proof_info
+ 
+let discard_all () =
+  current_proof := []; 
+  suspended := [];
+  proof_info := Idmap.empty
+
+(* [set_proof_mode] sets the proof mode to be used after it's called. It is
+    typically called by the Proof Mode command. *)
+(* Core component.
+    No undo handling.
+    Applies to proof [id], and proof mode [m]. *)
+let set_proof_mode m id = 
+  let info = Idmap.find id !proof_info in
+  let info = { info with mode = m } in
+  proof_info := Idmap.add id info !proof_info;
+  update_proof_mode ()
+(* Complete function.
+    Handles undo.
+    Applies to current proof, and proof mode name [mn]. *)
+let set_proof_mode mn =
+  let m = find_proof_mode mn in
+  let id = get_current_proof_name () in
+  let pr = give_me_the_proof () in
+  Proof.add_undo begin let curr = !current_proof_mode in fun () ->
+    set_proof_mode curr id ; update_proof_mode ()
+  end pr ;
+  set_proof_mode m id
+
+(* [start_proof s str env t hook tac] starts a proof of name [s] and
+    conclusion [t]; [hook] is optionally a function to be applied at
+    proof end (e.g. to declare the built constructions as a coercion
+    or a setoid morphism); init_tac is possibly a tactic to
+    systematically apply at initialization time (e.g. to start the
+    proof of mutually dependent theorems).
+    It raises exception [ProofInProgress] if there is a proof being
+    currently edited. *)
+let start_proof  id str goals ?(compute_guard=[]) hook =
+  (* arnaud: ajouter une vérification pour la présence de id dans le proof_global *)
+  let p = Proof.start goals in
+  add id { strength=str ; 
+	        compute_guard=compute_guard ; 
+		hook=hook ;
+	        mode = ! default_proof_mode } proof_info ;
+  push (id,p) current_proof
+
+(* arnaud: à enlever *)
+let run_tactic tac = 
+  let p = give_me_the_proof () in
+  let env = Global.env () in
+  Proof.run_tactic env tac p
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac =
+  let p = give_me_the_proof () in
+  Proof.set_endline_tactic tac p
+
+let set_used_variables l =
+  let p = give_me_the_proof () in
+  let env = Global.env () in
+  let ids = List.fold_right Idset.add l Idset.empty in
+  let ctx = Environ.keep_hyps env ids in
+  Proof.set_used_variables ctx p
+
+let get_used_variables () =
+  Proof.get_used_variables (give_me_the_proof ())
+
+let with_end_tac tac =
+  let p = give_me_the_proof () in
+  Proof.with_end_tac p tac
+
+let close_proof () =
+  (* spiwack: for now close_proof doesn't actually discard the proof, it is done
+      by [Command.save]. *)
+  try 
+    let id = get_current_proof_name () in
+    let p = give_me_the_proof () in
+    let proofs_and_types = Proof.return p in
+    let section_vars = Proof.get_used_variables p in
+    let entries = List.map
+      (fun (c,t) -> { Entries.const_entry_body = c;
+                      const_entry_secctx = section_vars;
+                      const_entry_type = Some t;
+		      const_entry_opaque = true })
+      proofs_and_types
+    in
+    let { compute_guard=cg ; strength=str ; hook=hook } =
+      Idmap.find id !proof_info
+    in
+    (id, (entries,cg,str,hook))
+  with 
+    |  Proof.UnfinishedProof ->
+	 Util.error "Attempt to save an incomplete proof"
+    | Proof.HasUnresolvedEvar ->
+	Util.error "Attempt to save a proof with existential variables still non-instantiated"
+
+
+(**********************************************************)
+(*                                                                                                  *)
+(*                              Utility functions                                          *)
+(*                                                                                                  *)
+(**********************************************************)
+
+let maximal_unfocus k p =
+  begin try while Proof.no_focused_goal p do
+    Proof.unfocus k p
+  done
+  with Proof.FullyUnfocused | Proof.CannotUnfocusThisWay -> ()
+  end
+
+
+(**********************************************************)
+(*                                                        *)
+(*                                 Bullets                *)
+(*                                                        *)
+(**********************************************************)
+
+module Bullet = struct
+
+  open Store.Field
+
+
+  type t = Vernacexpr.bullet
+
+  type behavior = {
+    name : string;
+    put : Proof.proof -> t -> unit
+  }
+
+  let behaviors = Hashtbl.create 4
+  let register_behavior b = Hashtbl.add behaviors b.name b
+
+  (*** initial modes ***)
+  let none = {
+    name = "None";
+    put = fun _ _ -> ()
+  }
+  let _ = register_behavior none
+
+  module Strict = struct
+    (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
+    let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind)
+    let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
+
+    let get_bullets pr =
+      try Proof.get_at_focus bullet_kind pr
+      with Proof.NoSuchFocus -> []
+
+    let has_bullet bul pr =
+      let rec has_bullet = function
+	| b'::_ when bul=b' -> true
+	| _::l -> has_bullet l
+	| [] -> false
+      in
+      has_bullet (get_bullets pr)
+
+    (* precondition: the stack is not empty *)
+    let pop pr =
+      match get_bullets pr with
+      | b::_ ->
+	Proof.unfocus bullet_kind pr;
+	(*returns*) b
+      | _ -> assert false
+
+    let push b pr =
+      Proof.focus bullet_cond (b::get_bullets pr) 1 pr
+
+    let put p bul =
+      if has_bullet bul p then
+	Proof.transaction p begin fun () ->
+	  while bul <> pop p do () done;
+	  push bul p
+	end
+      else 
+	push bul p
+
+    let strict = {
+      name = "Strict Subproofs";
+      put = put
+    }
+    let _ = register_behavior strict
+  end
+
+  (* Current bullet behavior, controled by the option *)
+  let current_behavior = ref Strict.strict
+    
+  let _ =
+    Goptions.declare_string_option {Goptions.
+      optsync = true;
+      optdepr = false;
+      optname = "bullet behavior";
+      optkey = ["Bullet";"Behavior"];
+      optread = begin fun () ->
+	(!current_behavior).name
+      end;
+      optwrite = begin fun n ->
+	current_behavior := Hashtbl.find behaviors n
+      end
+    }
+
+  let put p b =
+    (!current_behavior).put p b
+end
+
+
+module V82 = struct
+  let get_current_initial_conclusions () =
+    let p = give_me_the_proof () in
+    let id = get_current_proof_name () in
+    let { strength=str ; hook=hook } = 
+      Idmap.find id !proof_info
+    in
+    (id,(Proof.V82.get_initial_conclusions p, str, hook))
+end
+