(* Copyright (C) 2004-2005, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://helm.cs.unibo.it/
 *)

open Printf

open MatitaTypes

  (** raised when one of the script margins (top or bottom) is reached *)
exception Margin

let safe_substring s i j =
  try String.sub s i j with Invalid_argument _ -> assert false

let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
let blanks_RE = Pcre.regexp "^\\s*$"

let first_line s =
  let s = Pcre.replace ~rex:heading_nl_RE s in
  try
    let nl_pos = String.index s '\n' in
    String.sub s 0 nl_pos
  with Not_found -> s

let prepend_text header base =
  if Pcre.pmatch ~rex:heading_nl_RE base then
    sprintf "\n%s%s" header base
  else
    sprintf "%s\n%s" header base

  (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
let goal_ast n =
  let module A = TacticAst in
  let loc = CicAst.dummy_floc in
  A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))

let eval_statement status user_goal s =
  let st = CicTextualParser2.parse_statement (Stream.of_string s) in
  match st with
  | TacticAst.Command (loc, _) | TacticAst.Tactical (loc, _) ->
      let parsed_text_length = snd (CicAst.loc_of_floc loc) in
      let parsed_text = safe_substring s 0 parsed_text_length in
      let goal_changed = ref false in
      let status =
        match status.proof_status with
        | Incomplete_proof (_, goal) when goal <> user_goal ->
            goal_changed := true;
            MatitaEngine.eval_ast status (goal_ast user_goal)
        | _ -> status
      in
      let new_status = MatitaEngine.eval_ast status st in
      let new_aliases =
        match st with
        | TacticAst.Command (_, TacticAst.Alias _) ->
            DisambiguateTypes.Environment.empty
        | _ -> MatitaSync.alias_diff ~from:status new_status
      in
      let new_text =
        if DisambiguateTypes.Environment.is_empty new_aliases then
          parsed_text
        else
          prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases)
            parsed_text
      in
      let new_text =
        if !goal_changed then
          prepend_text
            (TacticAstPp.pp_tactic (TacticAst.Goal (loc, user_goal))(* ^ "\n"*))
            new_text
        else
          new_text
      in
      [ new_status, new_text ], parsed_text_length
  | TacticAst.Macro (loc, mac) ->
      (match mac with (* TODO *)
       | _ -> failwith "not implemented")

class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) () =
object (self)
  initializer self#reset ()

  val mutable statements = [];    (** executed statements *)
  val mutable history = [ init ];
    (** list of states before having executed statements. Head element of this
      * list is the current state, last element is the state at the beginning of
      * the script.
      * Invariant: this list length is 1 + length of statements *)

  (** goal as seen by the user (i.e. metano corresponding to current tab) *)
  val mutable userGoal = ~-1

  (** text mark and tag representing locked part of a script *)
  val locked_mark =
    buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
  val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]

    (* history can't be empty, the invariant above grant that it contains at
     * least the init status *)
  method status = match history with hd :: _ -> hd | _ -> assert false

  method private _advance ?statement () =
    let s = match statement with Some s -> s | None -> self#getFuture in
    if Pcre.pmatch ~rex:blanks_RE s then raise Margin;
    MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
    let (entries, parsed_len) = eval_statement self#status userGoal s in
    let (new_statuses, new_statements) = List.split entries in
(*
prerr_endline "evalStatement returned";
List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
*)
    history <- List.rev new_statuses @ history;
    statements <- List.rev new_statements @ statements;
    let start = buffer#get_iter_at_mark (`MARK locked_mark) in
    if statement = None then begin
      let stop = start#copy#forward_chars parsed_len in
      buffer#delete ~start ~stop
    end;
    let new_text = String.concat "" new_statements in
    buffer#insert ~iter:start new_text;
    self#moveMark (String.length new_text);

  method private _retract () =
    match statements, history with
    | last_statement :: _, cur_status :: prev_status :: _ ->
        MatitaSync.time_travel ~present:cur_status ~past:prev_status;
        statements <- List.tl statements;
        history <- List.tl history;
        self#moveMark (- (String.length last_statement))
    | _ -> raise Margin

  method advance ?statement () =
    try
      self#_advance ?statement ()
    with Margin -> ()

  method retract () = try self#_retract () with Margin -> ()

  method private getFuture =
    buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
      ~stop:buffer#end_iter ()

  (** @param rel_offset relative offset from current position of locked_mark *)
  method private moveMark rel_offset =
    let mark = `MARK locked_mark in
    buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
    let current_mark_pos = buffer#get_iter_at_mark mark in
    let new_mark_pos =
      match rel_offset with
      | 0 -> current_mark_pos
      | n when n > 0 -> current_mark_pos#forward_chars n
      | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
    in
    buffer#move_mark mark ~where:new_mark_pos;
    buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
    self#notify

  val mutable observers = []

  method addObserver (o: MatitaTypes.status -> unit) =
    observers <- o :: observers

  method private notify =
    let status = self#status in
    List.iter (fun o -> o status) observers

  method loadFrom fname =
    buffer#set_text (MatitaMisc.input_file fname);
    self#goto_top

  method saveTo fname =
    let oc = open_out fname in
    output_string oc (buffer#get_text ~start:buffer#start_iter
                        ~stop:buffer#end_iter ());
    close_out oc

  method private goto_top =
    MatitaSync.time_travel ~present:self#status ~past:init;
    statements <- [];
    history <- [ init ];
    userGoal <- ~-1;
    self#notify;
    buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
    buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter

  method reset () =
    self#goto_top;
    buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter

  method goto (pos: [`Top | `Bottom | `Cursor]) () =
    match pos with
    | `Top -> self#goto_top
    | `Bottom ->
        (try while true do self#_advance () done with Margin -> ())
    | `Cursor ->
        let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
        let cursor_iter () = buffer#get_iter_at_mark `INSERT in
        let rec forward_until_cursor () = (* go forward until locked > cursor *)
          self#_advance ();
          if (locked_iter ())#compare (cursor_iter ()) < 0 then
            forward_until_cursor ()
        in
        let rec back_until_cursor () = (* go backward until locked < cursor *)
          self#_retract ();
          if (locked_iter ())#compare (cursor_iter ()) > 0 then
            back_until_cursor ()
        in
        let cmp = (locked_iter ())#compare (cursor_iter ()) in
        (try
          if cmp < 0 then       (* locked < cursor *)
            forward_until_cursor ()
          else if cmp > 0 then  (* locked > cursor *)
            back_until_cursor ()
          else                  (* cursor = locked *)
              ()
        with Margin -> ())

  method onGoingProof () =
    match self#status.proof_status with
    | No_proof | Proof _ -> false
    | Incomplete_proof _ -> true
    | Intermediate _ -> assert false

  method proofStatus = MatitaMisc.get_proof_status self#status
  method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
  method proofContext = MatitaMisc.get_proof_context self#status
  method setGoal n = userGoal <- n

  (* debug *)
  method dump () =
    MatitaLog.debug "script status:";
    MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
    MatitaLog.debug (sprintf "%d statements:" (List.length statements));
    List.iter MatitaLog.debug statements;

end

let _script = ref None

let script ~buffer ~init () =
  let s = new script ~buffer ~init () in
  _script := Some s;
  s

let instance () = match !_script with None -> assert false | Some s -> s