(* Copyright (C) 2000, 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/.
 *)

(******************************************************************************)
(*                                                                            *)
(*                               PROJECT HELM                                 *)
(*                                                                            *)
(*                      Enrico Tassi <tassi@cs.unibo.it>                      *)
(*                                 23/04/2004                                 *)
(*                                                                            *)
(* This module implements the aciclic graph of universes.                     *)
(*                                                                            *)
(******************************************************************************)

open Printf

(******************************************************************************)
(** Types and default values                                                 **)
(******************************************************************************)

type universe = int

module UniverseType = struct
  type t = universe
  let compare = Pervasives.compare
end

module SOF = Set.Make(UniverseType)

type entry = {
	eq_closure : SOF.t;
	ge_closure : SOF.t;
	gt_closure : SOF.t;
	in_eq_of   : SOF.t;
	in_ge_of   : SOF.t;
	in_gt_of   : SOF.t;
	one_s_eq   : SOF.t;
	one_s_ge   : SOF.t;
	one_s_gt   : SOF.t;
}

module MAL = Map.Make(UniverseType)

type arc_type = GE | GT | EQ

type arc = arc_type * universe * universe

type bag = entry MAL.t * (arc list)

let empty_entry = {
	eq_closure=SOF.empty;
	ge_closure=SOF.empty;
	gt_closure=SOF.empty;
	in_eq_of=SOF.empty;
	in_ge_of=SOF.empty;
	in_gt_of=SOF.empty;
	one_s_eq=SOF.empty;
	one_s_ge=SOF.empty;
	one_s_gt=SOF.empty;
}

let empty_bag = (MAL.empty, [])

let env_bag = ref empty_bag

(******************************************************************************)
(** Pretty printings                                                         **)
(******************************************************************************)

let string_of_universe u = string_of_int u

let string_of_arc_type u =
  match u with
    EQ -> "EQ" 
  | GT -> "GT"
  | GE -> "EQ"

let string_of_arc u = 
  let atype,a,b = u in
  (string_of_arc_type atype) ^ " " ^ 
   (string_of_universe a) ^ " " ^ (string_of_universe b) ^ "; "
;;

let string_of_universe_set l = 
  SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""

let string_of_arc_list l = 
  List.fold_left (fun s x -> s ^ (string_of_arc x) ^ " ") "" l

let string_of_node n =
  "{"^
  "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^ 
  "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^ 
  "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^ 
  "i_eq: " ^ (string_of_universe_set n.in_eq_of) ^ "; " ^ 
  "i_ge: " ^ (string_of_universe_set n.in_ge_of) ^ "; " ^ 
  "i_gt: " ^ (string_of_universe_set n.in_gt_of) ^ "}\n"
  
let string_of_mal m =
  let rc = ref "" in
  MAL.iter (fun k v -> rc := !rc ^ sprintf "%d --> %s" k (string_of_node v)) m;
  !rc

let string_of_bag b = 
  let (m,l) = b in
  let s_m = string_of_mal m in
  let s_l = string_of_arc_list l in
   s_m ^"["^s_l^"]"

(******************************************************************************)
(** Helpers                                                                  **)
(******************************************************************************)

(*
    we need to merge the 2 graphs... here the code 
*)
let repr u m =
  try 
    MAL.find u m
  with
    Not_found -> 
      try 
        let m',_ = !env_bag in
        MAL.find u m'
      with
        Not_found -> empty_entry
    
(*
    FIXME: May be faster if we make it by hand
*)
let merge_closures f nodes m =  
  SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty

(******************************************************************************)
(** Real stuff GT                                                            **)
(******************************************************************************)

(* 
    todo is the SOF of nodes that needs to be recomputed, 
    m is the MAL map, s is the already touched nodes 
*)
let rec redo_gt_closure todo m s =
  if SOF.is_empty todo then m
  else
    begin
    (* we choose the node to recompute *)
    let u = SOF.choose todo in
    if not (SOF.mem u s) then
      let ru = repr u m in
      let ru' = {ru with gt_closure = 
       (* the new gt closure is the gt-closures + ge-closures + eq-closures 
          of the one step gt-connected nodes *)
       SOF.union ru.one_s_gt (merge_closures 
        (fun x -> SOF.union x.eq_closure 
	 (SOF.union x.gt_closure x.ge_closure)) ru.one_s_gt m) } in
      let m' = MAL.add u ru' m in
      let s' = SOF.add u s in
      redo_gt_closure (SOF.union (SOF.remove u todo) ru'.in_gt_of) m' s'
    else
      (* if already done go next. FIXME: think if it is right
         maybe we should check if we changed something or not *)
      redo_gt_closure (SOF.remove u todo) m s
    end

(*
    calculates the closures of u and adjusts the in_*_of of v, then
    starts redo_*_closure to adjust the colure of nodew thet have 
    (clusure u) in theyr closures
*)
let add_gt_arc u v m =
  let ru = repr u m in
  let rv = repr v m in 
  let ru' = {
    (* new node: we add the v gt-closure and v to our gt-closure *)
    eq_closure = ru.eq_closure;
    ge_closure = ru.ge_closure;
    gt_closure = SOF.add v 
     (SOF.union ru.gt_closure 
      (SOF.union rv.ge_closure 
       (SOF.union rv.eq_closure rv.gt_closure)));
    in_eq_of = ru.in_eq_of;
    in_ge_of = ru.in_ge_of;
    in_gt_of = ru.in_gt_of;
    one_s_eq = ru.one_s_eq;
    one_s_ge = ru.one_s_ge;
    one_s_gt = SOF.add v ru.one_s_gt;
  } in
  (* may add the sanity check *)
  let rv' = { rv with in_gt_of = SOF.add u rv.in_gt_of } in
  let m' = MAL.add u ru' m in
  let m'' = MAL.add v rv' m' in
  redo_gt_closure ru'.in_gt_of m'' SOF.empty

(*                                                                            
    given the 2 nodes plus the current bag, adds the arc, recomputes the 
    closures and returns the new map
*)                                                                            
let add_gt u v b =
  let m,l = b in
  let m' = add_gt_arc u v m in
  let l' = (GT,u,v)::l in
  (m',l')

(******************************************************************************)
(** Real stuff GE                                                            **)
(******************************************************************************)

(* 
    todo is the SOF of nodes that needs to be recomputed, 
    m is the MAL map, s is the already touched nodes 
*)
let rec redo_ge_closure todo m s =
  if SOF.is_empty todo then m,s
  else
    begin
    let u = SOF.choose todo in
    if not (SOF.mem u s) then
      begin
        let ru = repr u m in
	(* the ge-closure is recomputed as the ge-closures of  
	   ge connected nodes plus theys eq-closure *)
        let ru' = {ru with ge_closure = merge_closures 
          (fun x -> SOF.union x.eq_closure x.ge_closure) ru.one_s_ge m } in
        let m' = MAL.add u ru' m in
        let s' = SOF.add u s in
        redo_ge_closure (SOF.union (SOF.remove u todo) ru'.in_ge_of) m' s'
      end
    else
      redo_ge_closure (SOF.remove u todo) m s
    end

(*
    calculates the closures of u and adjusts the in_*_of of v, then
    starts redo_*_closure to adjust the colure of nodew thet have 
    (clusure u) in theyr closures
*)
let add_ge_arc u v m =
  let ru = repr u m in
   let rv = repr v m in 
  let ru' = {
    eq_closure = ru.eq_closure;
    ge_closure = SOF.add v 
     (SOF.union ru.ge_closure 
      (SOF.union rv.eq_closure rv.ge_closure));
    gt_closure = ru.gt_closure;
    in_eq_of = ru.in_eq_of;
    in_ge_of = ru.in_ge_of;
    in_gt_of = ru.in_gt_of;
    one_s_eq = ru.one_s_eq;
    one_s_ge = SOF.add v ru.one_s_ge;
    one_s_gt = ru.one_s_gt;
  } in
  let rv' = { rv with in_gt_of = SOF.add u rv.in_ge_of } in
  let m' = MAL.add u ru' m in
  let m'' = MAL.add v rv' m' in
  let m''',td = redo_ge_closure ru'.in_ge_of m'' SOF.empty in
  (* closing ge may provoke aome changes in gt-closures *)
  redo_gt_closure (SOF.union ru'.in_gt_of 
   (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_gt_of)) 
    td SOF.empty )) m''' SOF.empty

(*                                                                            
    given the 2 nodes plus the current bag, adds the arc, recomputes the 
    closures and returns the new map
*) 
let add_ge u v b =
  let m,l = b in
  let m' = add_ge_arc u v m in
  let l' = (GE,u,v)::l in
  (m',l')
  
(******************************************************************************)
(** Real stuff EQ                                                            **)
(******************************************************************************)

let rec redo_eq_closure todo m s =
  if SOF.is_empty todo then m,s
  else begin
    let u = SOF.choose todo in
    if not (SOF.mem  u s) then
      begin
        let ru = repr u m in
        let eq_closure = merge_closures 
          (fun x -> x.eq_closure) ru.one_s_eq m in
        let ru' = {ru with eq_closure = eq_closure
        ; in_eq_of = eq_closure ; one_s_eq = eq_closure } in
        let m' = MAL.add u ru' m in
        let s' = SOF.add u s in
        redo_eq_closure (SOF.union (SOF.remove u todo) ru'.in_eq_of) m' s'
      end
    else
      redo_eq_closure (SOF.remove u todo) m s
  end

(*
    calculates the closures of u and adjusts the in_*_of of v, then
    starts redo_*_closure to adjust the colure of nodew thet have 
    (clusure u) in theyr closures
*)
let add_eq_arc u v m =
  let ru = repr u m in
  let rv = repr v m in 
  (* since eq is symmetric we have to chage more *)
  let eq_closure = SOF.add u (SOF.add v 
     (SOF.union ru.eq_closure rv.eq_closure)) in
  let ru' = {
    eq_closure = eq_closure;
    ge_closure = SOF.union ru.ge_closure rv.ge_closure;
    gt_closure = SOF.union ru.gt_closure rv.gt_closure;
    in_eq_of = eq_closure;
    in_ge_of = SOF.union ru.in_ge_of rv.in_ge_of;
    in_gt_of = SOF.union ru.in_gt_of rv.in_gt_of;
    one_s_eq = eq_closure;
    one_s_ge = SOF.union ru.one_s_ge rv.one_s_ge;
    one_s_gt = SOF.union ru.one_s_gt rv.one_s_gt;
  } in
  (* this is a collapse *)
  let rv' = ru' in
  let m' = MAL.add u ru' m in
  let m'' = MAL.add v rv' m' in
  let m''',td = redo_eq_closure ru'.in_eq_of m'' SOF.empty in
  (* redoing a eq may change some ge and some gt *)
  let m'''',td' = redo_ge_closure 
   (SOF.union ru'.in_ge_of 
    (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_ge_of)) 
    td SOF.empty)) m''' SOF.empty in
  redo_gt_closure (SOF.union ru'.in_gt_of 
   (SOF.fold (fun u s -> SOF.union s ((repr u m'''').in_gt_of)) 
    td' SOF.empty)) m'''' SOF.empty

(*                                                                            
    given the 2 nodes plus the current bag, adds the arc, recomputes the 
    closures and returns the new map
*) 
let add_eq u v b =
  let m,l = b in
  let m' = add_eq_arc u v m in
  let l' = (EQ,u,v)::l in
  (m',l')

(******************************************************************************)
(** Oyther real code                                                         **)
(******************************************************************************)

exception UniverseInconsistency of string 

let error arc node1 closure_type node2 closure =
  let s = "  ===== Universe Inconsistency detected =====\n\n" ^
   "\tUnable to add ("^ (string_of_arc arc) ^ ") cause " ^ 
   (string_of_universe node1) ^ " is in the " ^
   (string_of_arc_type closure_type) ^ " closure {" ^
   (string_of_universe_set closure) ^ "} of " ^ 
   (string_of_universe node2) ^ "\n\n" ^
   "  ===== Universe Inconsistency detected =====\n" in
  prerr_endline s;
  raise (UniverseInconsistency s)

(*  
    we merge the env_bag with b
*)
let qed b = 
  let m,l = b in
  let m',l' = !env_bag in
  let m'' = ref m' in
  MAL.iter (fun k v -> m'':= MAL.add k v !m'') m;
  let l'' = l @ l' in
  env_bag := (!m'',l'')
  
let add_eq u v b =
  (* should we check to no add twice the same?? *)
  let m,_ = b in
  let ru = repr u m in
  if SOF.mem v ru.gt_closure then
    error (EQ,u,v) v GT u ru.gt_closure
  else
    begin
    let rv = repr v m in
    if SOF.mem u rv.gt_closure then
      error (EQ,u,v) u GT v rv.gt_closure
    else
      add_eq u v b
    end

let add_ge u v b =
  (* should we check to no add twice the same?? *)
  let m,_ = b in
  let rv = repr v m in
  if SOF.mem u rv.gt_closure then
    error (GE,u,v) u GT v rv.gt_closure
  else
    add_ge u v b
  
let add_gt u v b =
  (* should we check to no add twice the same?? *)
  let m,_ = b in
  let rv = repr v m in
  if SOF.mem u rv.gt_closure then
    error (GT,u,v) u GT v rv.gt_closure
  else
    begin
      if SOF.mem u rv.ge_closure then
        error (GT,u,v) u GE v rv.ge_closure
      else
        begin
          if SOF.mem u rv.eq_closure then
            error (GT,u,v) u EQ v rv.eq_closure
	  else
	    add_gt u v b
	end
    end
  
  

(******************************************************************************)
(** World interface                                                          **)
(******************************************************************************)

type universe_graph = bag

let work_bag = ref empty_bag
let current_index = ref (-1)

let get_working () = !work_bag
let get_global  () = !env_bag 
let set_working b = work_bag := b

let fresh () =
  current_index := !current_index + 1;
  !current_index

let qed () = 
  qed !work_bag

let print_global_graph () =
  let s = string_of_bag !env_bag in
  prerr_endline s

let print_working_graph () =
  let s = string_of_bag !work_bag in
  prerr_endline s

type history_ticket = int

let get_history_ticket b =
  let m,l = b in
  List.length l

let redo_history t b b'=
  let rec get_history l n =
    if n == 0 then
      []
    else
      begin
      match l with 
        [] -> failwith "erroer, lista piu' corta della history"
      | h::tl -> h::(get_history tl (n - 1))
      end
  in
  let rec redo_commands l b =
    match l with
      [] -> b
    | (GE,u,v)::tl -> redo_commands tl (add_ge u v b)
    | (GT,u,v)::tl -> redo_commands tl (add_gt u v b)
    | (EQ,u,v)::tl -> redo_commands tl (add_eq u v b)
  in
  let (m,l) = b in
  let todo = List.rev (get_history l ((List.length l) - t)) in
  try 
    redo_commands todo b'
  with 
    UniverseInconsistency s -> failwith s
  (*| _ -> failwith "Unexpected exception"*)

let add_gt u v =
  try 
    work_bag := add_gt u v !work_bag; true
  with
    UniverseInconsistency s -> false
  (*| _ -> failwith "Unexpected exception"*)

let add_ge u v = 
  try 
    work_bag := add_ge u v !work_bag;true
  with
    UniverseInconsistency s -> false
  (*| _ -> failwith "Unexpected exception"*)

let add_eq u v =
  try 
    work_bag := add_eq u v !work_bag;true
  with
    UniverseInconsistency s -> false
  (*| _ -> failwith "Unexpected exception"*)

let saved_data = ref (empty_bag,0)

let directly_to_env_begin () =
  saved_data := (!work_bag, get_history_ticket !env_bag);
  work_bag := empty_bag
  
let directly_to_env_end () = 
  qed ();
  let (b,t) = !saved_data in
  work_bag := redo_history t !env_bag b
 
let reset_working () = work_bag := empty_bag

(******************************************************************************)
(** Fake implementatoin                                                      **)
(******************************************************************************)

let reset_working = function _ -> ()
let directly_to_env_end = function _ -> ()
let directly_to_env_begin = function _ -> ()
let add_eq = fun _ _ -> true
let add_ge = fun _ _ -> true
let add_gt = fun _ _ -> true
let get_working = function a -> empty_bag
let set_working = function a -> ()