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