1(* ===================================================================== *)
2(* FILE          : Net.sig                                               *)
3(* DESCRIPTION   : Signature for term nets.                              *)
4(*                                                                       *)
5(* AUTHOR        : ICL HOL group.                                        *)
6(* DATE          : August 26, 1991                                       *)
7(* Modified      : September 23, 1997, Ken Larsen                        *)
8(* Rewritten and                                                         *)
9(* Expanded      : July 17, 1999, Konrad Slind                           *)
10(* ===================================================================== *)
11
12signature Net =
13sig
14  type 'a net
15  type term = Term.term
16
17  val empty     : 'a net
18  val insert    : term * 'a -> 'a net -> 'a net
19  val match     : term -> 'a net -> 'a list
20  val index     : term -> 'a net -> 'a list
21  val delete    : term * ('a -> bool) -> 'a net -> 'a net
22  val filter    : ('a -> bool) -> 'a net -> 'a net
23  val union     : 'a net -> 'a net -> 'a net
24  val map       : ('a -> 'b) -> 'a net -> 'b net
25  val itnet     : ('a -> 'b -> 'b) -> 'a net -> 'b -> 'b
26  val size      : 'a net -> int
27  val listItems : 'a net -> 'a list
28
29  val enter     : term * 'a -> 'a net -> 'a net  (* for compatibility *)
30  val lookup    : term -> 'a net -> 'a list      (* for compatibility *)
31
32
33(*---------------------------------------------------------------------------
34
35    A term net is a collection of items, each of which can be thought
36    of as being indexed by a path which is computed from a term which
37    is supplied when the item is inserted into the net. Type information,
38    and the names of variables, is not represented in paths, so more than
39    one term may be indexed by the same path, i.e., the extraction
40    operations are not exact. In this sense, term nets are akin to
41    hash tables.
42
43   [empty] is the empty term net.
44
45   [insert (tm, x) net]
46
47    The term tm is used as a key to compute a path at which to
48    store x in net. If the path does not already exist in net,
49    it is created. Note that insert merely adds x to the net;
50    if x has already been stored under tm, then it is not overwritten.
51
52   [match tm net]
53
54    Term nets can be used to cut down on the number of match attempts
55    that a matching function would have to make, say when rewriting
56    with a collection of theorems. "match tm net" will return every
57    element that has been inserted into the net using a term M as the
58    key, such that M possibly matches tm. The matches are returned in
59    "most specific match first" order.
60
61   [index tm net]
62
63    An alternative use of term nets ignores any paths in the net
64    arising from clearly non-alpha-convertible terms. "index" is a more
65    discriminating entrypoint than "match", in the sense that the set
66    of results is always a subset of those returned for matches.
67
68   [delete (tm,P) net] uses tm as an index into the net. There can be
69     more than one element indexable by tm. The net resulting from
70     removing all such elements that also meet the predicate P is
71     returned.
72
73   [filter P net] The net resulting from removing all elements meeting
74      P is returned.
75
76   [union net1 net2] joins net1 and net2. Looking up or fetching
77     an element from the result should return the union of the
78     results of separately fetching or looking up in net1 and net2.
79
80   [map f net] returns a new net, each element of which has had f
81     applied to it.
82
83   [itnet f net b] folds function f through net, with base value b.
84
85   [size net] returns the number of elements in the net.
86
87   [listItems net] lists the elements in the net, in no particular order.
88
89   [enter (tm,x) net] An outdated version of insert, kept for compatibility.
90
91   [lookup tm net] An outdated version of match, kept for compatibility.
92
93 ---------------------------------------------------------------------------*)
94end
95