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