(************************************************************************)
(*  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 Util
open Names
open Vernacexpr

(** Command history stack

    We maintain a stack of the past states of the system. Each
    successfully interpreted command adds an [info] element
    to this stack, storing what were the (label / current proof / ...)
    just _after_ the interpretation of this command.

    - A label is just an integer, starting from Lib.first_command_label
      initially, and incremented at each new successful command.
    - If some proofs are opened, we have their number in [nproofs],
      the name of the current proof in [prfname], the current depth in
      [prfdepth].
    - Otherwise, [nproofs = 0], [prfname = None], [prfdepth = 0]
    - The text of the command is stored (for Show Script currently).
    - A command can be tagged later as non-"reachable" when the current proof
      at the time of this command has been ended by Qed/Abort/Restart,
      meaning we can't backtrack there.
*)

type info = {
  label : int;
  nproofs : int;
  prfname : Id.t option;
  prfdepth : int;
  ngoals : int;
  cmd : vernac_expr;
  mutable reachable : bool;
}

let history : info Stack.t = Stack.create ()

(** Is this stack active (i.e. nonempty) ?
    The stack is currently inactive when compiling files (coqc). *)

let is_active () = not (Stack.is_empty history)

(** For debug purpose, a dump of the history *)

let dump_history () =
  let l = ref [] in
  Stack.iter (fun i -> l:=i::!l) history;
  !l

(** Basic manipulation of the command history stack *)

exception Invalid

let pop () = ignore (Stack.pop history)

let npop n =
 (* Since our history stack always contains an initial entry,
    it's invalid to try to completely empty it *)
 if n < 0 || n >= Stack.length history then raise Invalid
 else for _i = 1 to n do pop () done

let top () =
  try Stack.top history with Stack.Empty -> raise Invalid

(** Search the history stack for a suitable location. We perform first
    a non-destructive search: in case of search failure, the stack is
    unchanged. *)

exception Found of info

let search test =
  try
    Stack.iter (fun i -> if test i then raise (Found i)) history;
    raise Invalid
  with Found i ->
    while i != Stack.top history do pop () done

(** An auxiliary function to retrieve the number of remaining subgoals *)

let get_ngoals () =
  try
    let prf = Proof_global.give_me_the_proof () in
    List.length (Evd.sig_it (Proof.V82.background_subgoals prf))
  with Proof_global.NoCurrentProof -> 0

(** Register the end of a command and store the current state *)

let mark_command ast =
  Lib.add_frozen_state();
  Lib.mark_end_of_command();
  Stack.push
    { label = Lib.current_command_label ();
      nproofs = List.length (Pfedit.get_all_proof_names ());
      prfname =
        (try Some (Pfedit.get_current_proof_name ())
         with Proof_global.NoCurrentProof -> None);
      prfdepth = max 0 (Pfedit.current_proof_depth ());
      reachable = true;
      ngoals = get_ngoals ();
      cmd = ast }
    history

(** Backtrack by aborting [naborts] proofs, then setting proof-depth back to
    [pnum] and finally going to state number [snum]. *)

let raw_backtrack snum pnum naborts =
  for _i = 1 to naborts do Pfedit.delete_current_proof () done;
  Pfedit.undo_todepth pnum;
  Lib.reset_label snum

(** Re-sync the state of the system (label, proofs) with the top
    of the history stack. We may end on some earlier state to avoid
    re-opening proofs. This function will return the final label
    and the number of extra backtracking steps performed. *)

let sync nb_opened_proofs =
  (* Backtrack by enough additional steps to avoid re-opening proofs.
     Typically, when a Qed has been crossed, we backtrack to the proof start.
     NB: We cannot reach the empty stack, since the first entry in the
     stack has no opened proofs and is tagged as reachable.
  *)
  let extra = ref 0 in
  while not (top()).reachable do incr extra; pop () done;
  let target = top ()
  in
  (* Now the opened proofs at target is a subset of the opened proofs before
     the backtrack, we simply abort the extra proofs (if any).
     NB: It is critical here that proofs are nested in a regular way
     (i.e. no more Resume or Suspend commands as earlier). This way, we can
     simply count the extra proofs to abort instead of taking care of their
     names.
  *)
  let naborts = nb_opened_proofs - target.nproofs in
  (* We are now ready to do a low-level backtrack *)
  raw_backtrack target.label target.prfdepth naborts;
  (target.label, !extra)

(** Backtracking by a certain number of (non-state-preserving) commands.
    This is used by Coqide.
    It may actually undo more commands than asked : for instance instead
    of jumping back in the middle of a finished proof, we jump back before
    this proof. The number of extra backtracked command is returned at
    the end. *)

let back count =
  if Int.equal count 0 then 0
  else
    let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
    npop count;
    snd (sync nb_opened_proofs)

(** Backtracking to a certain state number, and reset proofs accordingly.
    We may end on some earlier state if needed to avoid re-opening proofs.
    Return the final state number. *)

let backto snum =
  if Int.equal snum (Lib.current_command_label ()) then snum
  else
    let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
    search (fun i -> Int.equal i.label snum);
    fst (sync nb_opened_proofs)

(** Old [Backtrack] code with corresponding update of the history stack.
    [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for
    compatibility with ProofGeneral. It's completely up to ProofGeneral
    to decide where to go and how to adapt proofs. Note that the choices
    of ProofGeneral are currently not always perfect (for instance when
    backtracking an Undo). *)

let backtrack snum pnum naborts =
  raw_backtrack snum pnum naborts;
  search (fun i -> Int.equal i.label snum)

(** [reset_initial] resets the system and clears the command history
    stack, only pushing back the initial entry. It should be equivalent
    to [backto Lib.first_command_label], but sligthly more efficient. *)

let reset_initial () =
  let init_label = Lib.first_command_label in
  if Int.equal (Lib.current_command_label ()) init_label then ()
  else begin
    Pfedit.delete_all_proofs ();
    Lib.reset_label init_label;
    Stack.clear history;
    Stack.push
      { label = init_label;
	nproofs = 0;
	prfname = None;
	prfdepth = 0;
	ngoals = 0;
	reachable = true;
	cmd = VernacNop }
      history
  end

(** Reset to the last known state just before defining [id] *)

let reset_name id =
  let lbl =
    try Lib.label_before_name id with Not_found -> raise Invalid
  in
  ignore (backto lbl)

(** When a proof is ended (via either Qed/Admitted/Restart/Abort),
    old proof steps should be marked differently to avoid jumping back
    to them:
     - either this proof isn't there anymore in the proof engine
     - either it's there but it's a more recent attempt after a Restart,
       so we shouldn't mix the two.
    We also mark as unreachable the proof steps cancelled via a Undo. *)

let mark_unreachable ?(after=0) prf_lst =
  let fix i = match i.prfname with
    | None -> raise Not_found (* stop hacking the history outside of proofs *)
    | Some p ->
      if List.mem p prf_lst && i.prfdepth > after
      then i.reachable <- false
  in
  try Stack.iter fix history with Not_found -> ()

(** Parse the history stack for printing the script of a proof *)

let get_script prf =
  let script = ref [] in
  let select i = match i.prfname with
    | None -> raise Not_found
    | Some p when Id.equal p prf && i.reachable -> script := i :: !script
    | _ -> ()
  in
  (try Stack.iter select history with Not_found -> ());
  (* Get rid of intermediate commands which don't grow the proof depth *)
  let rec filter n = function
    | [] -> []
    | {prfdepth=d; cmd=c; ngoals=ng}::l when n < d -> (c,ng) :: filter d l
    | {prfdepth=d}::l -> filter d l
  in
  (* initial proof depth (after entering the lemma statement) is 1 *)
  filter 1 !script