(*
    ||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 type Comparable =
  sig
    type t
    val is_eq : t -> t -> bool
  end

module C : Comparable =
  struct 
    type t = NCic.term
    let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
  end

  (*
module C : Comparable =
  struct 
    type t = Cic.term
    let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
  end
*)

open Discrimination_tree

module ClauseOT : Set.OrderedType 
                with type t = Terms.direction * C.t Terms.unit_clause = 
 struct 
  type t = Terms.direction * C.t Terms.unit_clause
  let compare (d1,(id1,_,_,_)) (d2,(id2,_,_,_)) = 
          Pervasives.compare (d1,id1) (d2,id2)
 end

module ClauseSet = Set.Make(ClauseOT)

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

type input = C.t Terms.foterm
type constant_name = C.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 _::_) -> 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) ->
      if C.is_eq a1 a2 then Pervasives.compare ar1 ar2
      else Pervasives.compare e1 e2 (* TODO: OPTIMIZE *)
  | _ -> Pervasives.compare e1 e2
;;

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

end

module DiscriminationTree = Make(FotermIndexable)(ClauseSet)