(* Copyright (C) 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

exception Error of string Lazy.t

module type Engine =
sig
  type goal
  type proof
  type tactic

  val is_goal_closed: goal -> proof -> bool
  val goals_of_proof: proof -> goal list

  val apply_tactic:
    tactic -> proof -> goal ->
      proof * goal list * goal list
end

(** like List.assoc returning a pair: binding matching the given key,
 * associative list without the returned binding
 * @raise Not_found *)
let list_assoc_extract key =
  let rec aux acc =
    function
    | [] -> raise Not_found
    | (key', _) as hd :: tl when key = key' -> hd, (List.rev acc @ tl)
    | hd :: tl -> aux (hd :: acc) tl
  in
  aux []

module type C =
sig
  type goal
  type proof
  type tactic

  type status

  type tactical =
    | Tactic of tactic
    | Skip

  type t =
    | Dot
    | Semicolon

    | Branch
    | Shift of int option
    | Select of goal list
    | End

    | Tactical of tactical

  val eval: t -> status -> status
  val init: proof -> status

  val get_proof: status -> proof
  val set_proof: proof -> status -> status

  type goal_switch = Open of goal | Closed of goal
  val get_goals: status -> goal_switch list

  val is_completed: status -> bool
end

module Make (E:Engine) =
struct
  type goal = E.goal
  type proof = E.proof
  type tactic = E.tactic

  type goal_switch = Open of goal | Closed of goal
  type 'a stack = 'a list
  type stack_tag = BranchTag | SelectTag | NoTag
  type stack_entry = 
    (int * goal_switch) list * goal list * goal list * stack_tag
  type status = proof * stack_entry stack

  let get_proof = fst
  let set_proof p (_, s) = p, s
  let get_goals (_, stack) =
    match stack with
    | (goals, _, _, _) :: _ -> List.map snd goals
    | [] -> assert false

  type tactical =
    | Tactic of tactic
    | Skip

  type t =
    | Dot
    | Semicolon
    | Branch
    | Shift of int option
    | Select of goal list
    | End
    | Tactical of tactical

  let goal_of = function _, Open g -> g | _, Closed g -> g 
  let is_open = function _, Open _ -> true | _, Closed _ -> false 
  let open_all = List.map (fun p, g -> p, Open g)
    
  let union a b = a @ b
  
  let complementary part full = (* not really efficient *)
    List.fold_left (fun acc g -> if List.mem g part then acc else g::acc)
      full []

  let close to_close =
    List.map
      (function
      | p, Open g when List.mem g to_close -> p, Closed g
      | g -> g)

  let map_stack f g h = List.map (fun (a,b,c,tag) -> f a, g b, h c, tag)

  let dummy_pos = ~-1
  let add_dummy_pos g = dummy_pos, g
  let map_dummy_pos = List.map add_dummy_pos

  let map_open_pos =
    let rec aux pos =
      function
      | [] -> []
      | g :: tl -> (pos, Open g) :: aux (pos + 1) tl
    in
    aux 1

  let eval_tactical tactical proof switch =
    match tactical, switch with
    | Tactic tac, Open n -> E.apply_tactic tac proof n
    | Skip, Closed n -> proof, [], [n]
    | Tactic _, Closed _ -> raise (Error (lazy "can't apply tactic to a closed goal"))
    | Skip, Open _ -> raise (Error (lazy "can't skip an open goal"))

  let eval continuational status =
    match continuational, status with
    | _, (_, []) -> assert false
    | Tactical t, (proof, (env, todo, left,tag)::tail) ->
        assert (List.length env > 1);
        let proof, opened, closed =
          List.fold_left 
            (fun (proof, opened, closed) cur_goal ->
              if List.exists ((=) (goal_of cur_goal)) closed then
                proof, opened, closed 
              else
                let proof, newopened, newclosed = 
                  eval_tactical t proof (snd cur_goal)
                in
                proof, 
                union (complementary newclosed opened) newopened,
                union closed newclosed
            ) (proof, [],[]) env
        in
        let pos = ref 0 in
        let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in
        proof, 
        (open_all stack_opened,
         complementary closed todo,
         complementary opened left, tag)
        :: map_stack
            (close closed) (complementary closed) (complementary opened) tail 
    | Semicolon, (proof, stack) -> proof, stack
    | Dot, (proof, (env, todo, left, tag)::tail) ->
        let env, left = 
          match List.filter is_open env, left with 
          | [], [] -> raise (Error (lazy "There is nothig to do for '.'"))
          | g::env,left -> [g], union (List.map goal_of env) left
          | [], g::left -> [dummy_pos, Open g], left
        in
        proof, (env, todo, left, tag)::tail
    | Branch, (proof, (g1::tl, todo, left, tag)::tail) ->
        assert (List.length tl >= 1);
        proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail
    | Branch, (_, _) -> raise (Error (lazy "can't branch on a singleton context"))
    | Shift opt_pos, (proof, (leftopen, t, l,BranchTag)::
                             (goals, todo, left,tag)::tail) ->
        let next_goal, rem_goals =
          match opt_pos, goals with
          | None, g1 :: tl -> g1, tl
          | Some pos, _ ->
              (try
                list_assoc_extract pos goals
              with Not_found -> raise (Error (lazy (sprintf "position %d not found" pos))))
          | None, [] -> raise (Error (lazy "no more goals to shift"))
        in
        let t =
          union t (union (List.map goal_of (List.filter is_open leftopen)) l)
        in
        proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail
    | Shift _, (_, _) -> raise (Error (lazy "no more goals to shift"))
    | Select gl, (proof, stack) ->
        List.iter
          (fun g ->
            if E.is_goal_closed g proof then
              raise (Error (lazy "you can't select a closed goal")))
          gl;
        (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack)
    | End, (proof, stack) ->
        (match stack with 
        | ([], [], [], SelectTag)::tail -> proof, tail
        | (leftopen,t,l,BranchTag)::(not_processed,todo,left,tag)::tail ->
            let env = 
              (union (open_all (map_dummy_pos t))
                (union (open_all (map_dummy_pos l))
                  (union not_processed (List.filter is_open leftopen))))
            in
            proof, (env,todo,left,tag)::tail
        | _ -> raise (Error (lazy "can't end here")))

  let init proof =
    proof,
    [ map_open_pos (E.goals_of_proof proof),  [], [], NoTag ]

  let is_completed =
    function
    | (_, [[],[],[],NoTag]) -> true
    | _ -> false
end