(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id$ *)

module Index(B : Orderings.Blob) = struct
  module U = FoUtils.Utils(B)

  module ClauseOT =
    struct 
      type t = Terms.direction * (* direction if it is an equality *)
	  bool *                 (* true if indexed literal is positive *)
	  int *                  (* position of literal in clause *)
	  B.t Terms.clause
 
      let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) = 
        let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in
        if c <> 0 then c else U.compare_clause uc1 uc2
      ;;
    end

  module ClauseSet : 
    Set.S with type elt = Terms.direction * (* direction if it is an equality *)
                          bool *       (* true if indexed literal is positive *)
			  int *        (* position of literal in clause *)
			  B.t Terms.clause
    = Set.Make(ClauseOT)

  open Discrimination_tree

  module FotermIndexable : Indexable with
    type constant_name = B.t and
    type input = B.t Terms.foterm 
  =
    struct

      type input = B.t Terms.foterm
      type constant_name = B.t

      let path_string_of =
        let rec aux arity = function
          | Terms.Leaf a -> [Constant (a, arity)]
          | Terms.Var i -> assert (arity = 0); [Variable]
          | Terms.Node (Terms.Var _::_) ->
	      (* FIXME : should this be allowed or not ? *)
	      assert false
          | Terms.Node ([] | [ _ ] ) -> assert false
          | Terms.Node (Terms.Node _::_) -> assert false	      
          | Terms.Node (hd::tl) ->
              aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) 
        in 
          aux 0
      ;;

      let compare e1 e2 = 
        match e1,e2 with 
        | Constant (a1,ar1), Constant (a2,ar2) ->
            let c = B.compare a1 a2 in
            if c <> 0 then c else Pervasives.compare ar1 ar2
        | Variable, Variable -> 0
        | Constant _, Variable -> ~-1
        | Variable, Constant _ -> 1
        | Proposition, _ | _, Proposition
        | Datatype, _ | _, Datatype
        | Dead, _ | _, Dead
        | Bound _, _ | _, Bound _ -> assert false
      ;;

      let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;

    end

    module DT : DiscriminationTree with
      type constant_name = B.t and 
      type input = B.t Terms.foterm and 
      type data = ClauseSet.elt and 
      type dataset = ClauseSet.t
    = Make(FotermIndexable)(ClauseSet)

  let index_literal t c is_pos pos = function
    | Terms.Equation (l,_,_,Terms.Gt) -> 
          DT.index t l (Terms.Left2Right,is_pos,pos,c)
    | Terms.Equation (_,r,_,Terms.Lt) ->
          DT.index t r (Terms.Right2Left,is_pos,pos,c)
    | Terms.Equation (l,r,_,Terms.Incomparable) ->
          DT.index
           (DT.index t l (Terms.Left2Right,is_pos,pos,c))
           r (Terms.Right2Left,is_pos,pos,c)
    | Terms.Equation (_,_,_,Terms.Eq) -> assert false
    | Terms.Predicate p ->
          DT.index t p (Terms.Nodir,is_pos,pos,c)
  ;;

  let index_clause t (_,nlit,plit,_,_ as c) =
    let index_iter is_pos  (t,pos) (lit,sel) =
      if sel then index_literal t c is_pos pos lit,pos+1 else t,pos+1
    in
    let (res,_) = List.fold_left (index_iter false) (t,0) nlit in
      fst (List.fold_left (index_iter true) (res,0) plit)
  ;;

  type active_set = B.t Terms.clause list * DT.t

end