helm/software/components/ng_refiner/nDiscriminationTree.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 type path_string
  16
  17 val pp_path_string : path_string -> string
  18
  19 module DiscriminationTreeIndexing :
  20   functor (A : Set.S) ->
  21     sig
  22
  23       type t
  24       val iter : t -> (path_string -> A.t -> unit) -> unit
  25
  26       val empty : t
  27       val index : t -> NCic.term -> A.elt -> t
  28       val remove_index : t -> NCic.term -> A.elt -> t
  29       val in_index : t -> NCic.term -> (A.elt -> bool) -> bool
  30       val retrieve_generalizations : t -> NCic.term -> A.t
  31       val retrieve_unifiables : t -> NCic.term -> A.t
  32     end
  33
  34