author | blanchet |
Fri, 17 Sep 2010 01:56:19 +0200 | |
changeset 39501 | aaa7078fff55 |
parent 39444 | beabb8443ee4 |
child 39502 | cffceed8e7fa |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *) |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39444
diff
changeset
|
3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
signature TermNet = |
|
7 |
sig |
|
8 |
||
9 |
(* ------------------------------------------------------------------------- *) |
|
10 |
(* A type of term sets that can be efficiently matched and unified. *) |
|
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
||
13 |
type parameters = {fifo : bool} |
|
14 |
||
15 |
type 'a termNet |
|
16 |
||
17 |
(* ------------------------------------------------------------------------- *) |
|
18 |
(* Basic operations. *) |
|
19 |
(* ------------------------------------------------------------------------- *) |
|
20 |
||
21 |
val new : parameters -> 'a termNet |
|
22 |
||
23 |
val null : 'a termNet -> bool |
|
24 |
||
25 |
val size : 'a termNet -> int |
|
26 |
||
27 |
val insert : 'a termNet -> Term.term * 'a -> 'a termNet |
|
28 |
||
29 |
val fromList : parameters -> (Term.term * 'a) list -> 'a termNet |
|
30 |
||
31 |
val filter : ('a -> bool) -> 'a termNet -> 'a termNet |
|
32 |
||
33 |
val toString : 'a termNet -> string |
|
34 |
||
35 |
val 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 |
||
44 |
val match : 'a termNet -> Term.term -> 'a list |
|
45 |
||
46 |
val matched : 'a termNet -> Term.term -> 'a list |
|
47 |
||
48 |
val unify : 'a termNet -> Term.term -> 'a list |
|
49 |
||
50 |
end |