(* 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/
 *)

exception Error of string 

module L = List

module type Engine =
sig
  type goal
  type conjecture
  type metasenv = conjecture list
  type tactic

  val goal_of_conjecture: conjecture -> goal
  val is_goal_in_metasenv: metasenv -> goal -> bool

  val apply_tactic:
    tactic -> metasenv -> goal ->
      metasenv * 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 Make (E:Engine) =
struct
  type goal_switch = Open of E.goal | Closed of E.goal
  type 'a stack = 'a list
  type status =
    E.metasenv * ((int * goal_switch) list * E.goal list * E.goal list) stack

  type tactical =
    | Tactic of E.tactic
    | Skip

  type t =
    | Dot
    | Semicolon
    | Branch
    | Shift of int option
    | Merge
    | Select of E.goal list
    | End_select
    | Tactical of tactical

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

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

  let stack_map f g h stack =
    L.map (fun (a,b,c) -> f a, g b, h c) stack

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

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

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