1(* ========================================================================= *) 2(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature TermNet = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* A type of term sets that can be efficiently matched and unified. *) 11(* ------------------------------------------------------------------------- *) 12 13type parameters = {fifo : bool} 14 15type 'a termNet 16 17(* ------------------------------------------------------------------------- *) 18(* Basic operations. *) 19(* ------------------------------------------------------------------------- *) 20 21val new : parameters -> 'a termNet 22 23val null : 'a termNet -> bool 24 25val size : 'a termNet -> int 26 27val insert : 'a termNet -> Term.term * 'a -> 'a termNet 28 29val fromList : parameters -> (Term.term * 'a) list -> 'a termNet 30 31val filter : ('a -> bool) -> 'a termNet -> 'a termNet 32 33val toString : 'a termNet -> string 34 35val pp : 'a Print.pp -> 'a termNet Print.pp 36 37(* ------------------------------------------------------------------------- *) 38(* Matching and unification queries. *) 39(* *) 40(* These function return OVER-APPROXIMATIONS! *) 41(* Filter afterwards to get the precise set of satisfying values. *) 42(* ------------------------------------------------------------------------- *) 43 44val match : 'a termNet -> Term.term -> 'a list 45 46val matched : 'a termNet -> Term.term -> 'a list 47 48val unify : 'a termNet -> Term.term -> 'a list 49 50end 51