equal
deleted
inserted
replaced
|
1 (* ========================================================================= *) |
|
2 (* THE KNUTH-BENDIX TERM ORDERING *) |
|
3 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 signature KnuthBendixOrder = |
|
7 sig |
|
8 |
|
9 (* ------------------------------------------------------------------------- *) |
|
10 (* The weight of all constants must be at least 1, and there must be at most *) |
|
11 (* one unary function with weight 0. *) |
|
12 (* ------------------------------------------------------------------------- *) |
|
13 |
|
14 type kbo = |
|
15 {weight : Term.function -> int, |
|
16 precedence : Term.function * Term.function -> order} |
|
17 |
|
18 val default : kbo |
|
19 |
|
20 val compare : kbo -> Term.term * Term.term -> order option |
|
21 |
|
22 end |