(* Copyright (C) 2002, 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://cs.unibo.it/helm/.
 *)

(* open CicReduction
open ProofEngineTypes
open UriManager *)

(** DEBUGGING *)

  (** perform debugging output? *)
let debug = false
let debug_print = fun _ -> ()

  (** debugging print *)
let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s)))

let id_tac = 
 let id_tac (proof,goal) = 
  let _, metasenv, _, _ = proof in
  let _, _, _ = CicUtil.lookup_meta goal metasenv in
  (proof,[goal])
 in 
  ProofEngineTypes.mk_tactic id_tac

let fail_tac =
 let fail_tac (proof,goal) =
  let _, metasenv, _, _ = proof in
  let _, _, _ = CicUtil.lookup_meta goal metasenv in
   raise (ProofEngineTypes.Fail (lazy "fail tactical"))
 in
  ProofEngineTypes.mk_tactic fail_tac

type goal = ProofEngineTypes.goal

    (** TODO needed until tactics start returning both opened and closed goals
     * First part of the function performs a diff among goals ~before tactic
     * application and ~after it. Second part will add as both opened and closed
     * the goals which are returned as opened by the tactic *)
let goals_diff ~before ~after ~opened =
  let sort_opened opened add =
    opened @ (List.filter (fun g -> not (List.mem g opened)) add)
  in
  let remove =
    List.fold_left
      (fun remove e -> if List.mem e after then remove else e :: remove)
      [] before
  in
  let add =
    List.fold_left
      (fun add e -> if List.mem e before then add else e :: add)
      []
      after
  in
  let add, remove = (* adds goals which have been both opened _and_ closed *)
    List.fold_left
      (fun (add, remove) opened_goal ->
        if List.mem opened_goal before
        then opened_goal :: add, opened_goal :: remove
        else add, remove)
      (add, remove)
      opened
  in
  sort_opened opened add, remove

module type T =
sig
  type tactic
  val first: tactics: (string * tactic) list -> tactic
  val thens: start: tactic -> continuations: tactic list -> tactic
  val then_: start: tactic -> continuation: tactic -> tactic
  val seq: tactics: tactic list -> tactic
  val repeat_tactic: tactic: tactic -> tactic
  val do_tactic: n: int -> tactic: tactic -> tactic 
  val try_tactic: tactic: tactic -> tactic 
  val solve_tactics: tactics: (string * tactic) list -> tactic

  val tactic: tactic -> tactic
  val skip: tactic
  val dot: tactic
  val semicolon: tactic
  val branch: tactic
  val shift: tactic
  val pos: int -> tactic
  val merge: tactic
  val focus: int list -> tactic
  val unfocus: tactic
end

module Make (S: Continuationals.Status) : T with type tactic = S.tactic =
struct
  module C = Continuationals.Make (S)

  type tactic = S.tactic

  let fold_eval status ts =
    let istatus =
      List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts
    in
    S.inject istatus

  (**
    naive implementation of ORELSE tactical, try a sequence of tactics in turn:
    if one fails pass to the next one and so on, eventually raises (failure "no
    tactics left")
  *)
  let first ~tactics =
    let rec first ~(tactics: (string * tactic) list) istatus =
      info (lazy "in Tacticals.first");
      match tactics with
      | (descr, tac)::tactics ->
          info (lazy ("Tacticals.first IS TRYING " ^ descr));
          (try
            let res = S.apply_tactic tac istatus in
            info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
            res
          with
          e ->
            match e with
            | (ProofEngineTypes.Fail _)
            | (CicTypeChecker.TypeCheckerFailure _)
            | (CicUnification.UnificationFailure _) ->
                info (lazy (
                  "Tacticals.first failed with exn: " ^
                  Printexc.to_string e));
                  first ~tactics istatus
            | _ -> raise e) (* [e] must not be caught ; let's re-raise it *)
      | [] -> raise (ProofEngineTypes.Fail (lazy "first: no tactics left"))
    in
    S.mk_tactic (first ~tactics)

  let thens ~start ~continuations =
    S.mk_tactic
      (fun istatus ->
        fold_eval istatus
          ([ C.Tactical (C.Tactic start); C.Branch ]
          @ (HExtlib.list_concat ~sep:[ C.Shift ]
              (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
          @ [ C.Merge ]))

  let then_ ~start ~continuation =
    S.mk_tactic
      (fun istatus ->
        let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
        let opened,closed = S.goals ostatus in
         match opened with
            [] -> ostatus
          | _ ->
            fold_eval (S.focus ~-1 ostatus)
              [ C.Semicolon;
                C.Tactical (C.Tactic continuation) ])

  let seq ~tactics =
    S.mk_tactic
      (fun istatus ->
        fold_eval istatus
          (HExtlib.list_concat ~sep:[ C.Semicolon ]
            (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))

  (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno
   * applicato la tattica *)

  let rec step f output_status opened closed =
    match opened with
    | [] -> output_status, [], closed
    | head :: tail -> 
        let status = S.focus head output_status in
        let output_status' = f status in
        let opened', closed' = S.goals output_status' in
        let output_status'', opened'', closed'' =
          step f output_status' tail []
        in
        output_status'', opened' @ opened'', closed' @ closed''

  (* This keep on appling tactic until it fails. When <tactic> generates more
   * than one goal, you have a tree of application on the tactic, repeat_tactic
   * works in depth on this tree *)
  let repeat_tactic ~tactic =
   let rec repeat_tactic ~tactic status =
    info (lazy "in repeat_tactic");
    try
     let output_status = S.apply_tactic tactic status in
     let opened, closed = S.goals output_status in
     let output_status, opened', closed' =
       step (repeat_tactic ~tactic) output_status opened closed
     in
     S.set_goals (opened', closed') output_status
    with 
     (ProofEngineTypes.Fail _) as e ->
      info (lazy
        ("Tacticals.repeat_tactic failed after nth time with exception: "
         ^ Printexc.to_string e));
      S.apply_tactic S.id_tactic status
   in 
    S.mk_tactic (repeat_tactic ~tactic)

  (* This tries to apply tactic n times *)
  let do_tactic ~n ~tactic =
   let rec do_tactic ~n ~tactic status =
    if n = 0 then
     S.apply_tactic S.id_tactic status
    else
     try 
      let output_status = S.apply_tactic tactic status in
      let opened, closed = S.goals output_status in
       let output_status, opened', closed' =
         step (do_tactic ~n:(n-1) ~tactic) output_status opened closed
       in
       S.set_goals (opened', closed') output_status
     with 
      (ProofEngineTypes.Fail _) as e ->
       info (lazy
          ("Tacticals.do_tactic failed after nth time with exception: "
           ^ Printexc.to_string e)) ;
       S.apply_tactic S.id_tactic status
   in
    S.mk_tactic (do_tactic ~n ~tactic)

  (* This applies tactic and catches its possible failure *)
  let try_tactic ~tactic =
   let rec try_tactic ~tactic status =
    info (lazy "in Tacticals.try_tactic");
    try
     S.apply_tactic tactic status
    with
     (ProofEngineTypes.Fail _) as e -> 
      info (lazy (
        "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
      S.apply_tactic S.id_tactic status
   in
    S.mk_tactic (try_tactic ~tactic)

  (* This tries tactics until one of them doesn't _solve_ the goal *)
  (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
  let solve_tactics ~tactics =
   let rec solve_tactics ~(tactics: (string * tactic) list) status =
    info (lazy "in Tacticals.solve_tactics");
    match tactics with
    | (descr, currenttactic)::moretactics ->
        info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
        (try
          let output_status = S.apply_tactic currenttactic status in
          let opened, closed = S.goals output_status in
           match opened with 
            | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^ 
                     " solved the goal!!!"));
  (* questo significa che non ci sono piu' goal, o che current_tactic non ne ha
   * aperti di nuovi? (la 2a!) ##### nel secondo caso basta per dire che
   * solve_tactics has solved the goal?  (si!) *)
                    output_status
            | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
                   solve_tactics ~tactics:(moretactics) status
         with
          (ProofEngineTypes.Fail _) as e ->
           info (lazy (
              "Tacticals.solve_tactics: current tactic failed with exn: "
              ^ Printexc.to_string e));
           solve_tactics ~tactics status
        )
    | [] ->
        raise (ProofEngineTypes.Fail
          (lazy "solve_tactics cannot solve the goal"))
   in
    S.mk_tactic (solve_tactics ~tactics)

  let cont_proxy cont = S.mk_tactic (C.eval cont)

  let tactic t = cont_proxy (C.Tactical (C.Tactic t))
  let skip = cont_proxy (C.Tactical C.Skip)
  let dot = cont_proxy C.Dot
  let semicolon = cont_proxy C.Semicolon
  let branch = cont_proxy C.Branch
  let shift = cont_proxy C.Shift
  let pos i = cont_proxy (C.Pos i)
  let merge = cont_proxy C.Merge
  let focus goals = cont_proxy (C.Focus goals)
  let unfocus = cont_proxy C.Unfocus
end

module ProofEngineStatus =
struct
  module Stack = Continuationals.Stack

  type input_status =
    ProofEngineTypes.status (* (proof, goal) *) * Stack.t

  type output_status =
    (ProofEngineTypes.proof * goal list * goal list) * Stack.t

  type tactic = ProofEngineTypes.tactic

  let id_tactic = id_tac

  let mk_tactic f =
    ProofEngineTypes.mk_tactic
      (fun (proof, goal) as pstatus ->
        let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
        let istatus = pstatus, stack in
(*         let ostatus = f istatus in
        let ((proof, opened, _), _) = ostatus in *)
        let (proof, _, _), stack = f istatus in
        let opened = Continuationals.Stack.open_goals stack in
        proof, opened)

  let apply_tactic tac ((proof, _) as pstatus, stack) =
    let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in
(* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *)
    let before = ProofEngineTypes.goals_of_proof proof in
    let after = ProofEngineTypes.goals_of_proof proof' in
    let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
(* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *)
    (proof', opened_goals, closed_goals), stack

  let goals ((_, opened, closed), _) = opened, closed
  let set_goals (opened, closed) ((proof, _, _), stack) =
    (proof, opened, closed), stack

  let get_stack = snd
  let set_stack stack (opstatus, _) = opstatus, stack

  let inject ((proof, _), stack) = ((proof, [], []), stack)
  let focus goal ((proof, _, _), stack) = (proof, goal), stack
end

module ProofEngineTacticals = Make (ProofEngineStatus)

include ProofEngineTacticals