1(* =====================================================================
2 * DESCRIPTION  : Implementation of term nets, from GTT.
3 * MODIFIED     : Donald Syme, 1995, to add local constants
4 *
5 * MODIFIED    : Donald Syme, November 1995, to be keyed up to
6 *               higher order matching, based on JRH's code from GTT.
7 * ===================================================================== *)
8
9signature Ho_Net =
10sig
11 type 'a net
12 type term = Term.term
13
14 val empty      : 'a net
15 val enter      : term list * term * 'a -> 'a net -> 'a net
16 val lookup     : term -> 'a net -> 'a list
17 val merge_nets : 'a net * 'a net -> 'a net
18 val fold'      : ('a -> 'b -> 'b) -> 'a net -> 'b -> 'b
19 val vfilter    : ('a -> bool) -> 'a net -> 'a net
20
21end
22