(*
    ||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) : 
  sig
    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

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

    module DT : Discrimination_tree.DiscriminationTree with 
      type constant_name = B.t and 
      type input = B.t Terms.foterm and 
      type data = ClauseSet.elt and 
      type dataset = ClauseSet.t
    
    val index_clause :
          DT.t -> B.t Terms.clause -> DT.t

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

  end