helm/software/components/ng_refiner/discrimination_tree.mli

   1
   2 (*
   3     ||M||  This file is part of HELM, an Hypertextual, Electronic
   4     ||A||  Library of Mathematics, developed at the Computer Science
   5     ||T||  Department, University of Bologna, Italy.
   6     ||I||
   7     ||T||  HELM is free software; you can redistribute it and/or
   8     ||A||  modify it under the terms of the GNU General Public License
   9     \   /  version 2 or (at your option) any later version.
  10      \ /   This software is distributed as is, NO WARRANTY.
  11       V_______________________________________________________________ *)
  12
  13 (* $Id$ *)
  14
  15 module DiscriminationTreeIndexing :
  16   functor (A : Set.S) ->
  17     sig
  18
  19       type t
  20       val iter : t -> (A.t -> unit) -> unit
  21
  22       val empty : t
  23       val index : t -> Cic.term -> A.elt -> t
  24       val remove_index : t -> Cic.term -> A.elt -> t
  25       val in_index : t -> Cic.term -> (A.elt -> bool) -> bool
  26       val retrieve_generalizations : t -> Cic.term -> A.t
  27       val retrieve_unifiables : t -> Cic.term -> A.t
  28     end
  29
  30