|
1 (* ========================================================================= *) |
|
2 (* ORDERED REWRITING FOR FIRST ORDER TERMS *) |
|
3 (* Copyright (c) 2003-2006 Joe Hurd, distributed under the GNU GPL version 2 *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 signature Rewrite = |
|
7 sig |
|
8 |
|
9 (* ------------------------------------------------------------------------- *) |
|
10 (* A type of rewrite systems. *) |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 |
|
13 datatype orient = LeftToRight | RightToLeft |
|
14 |
|
15 type reductionOrder = Term.term * Term.term -> order option |
|
16 |
|
17 type equationId = int |
|
18 |
|
19 type equation = Rule.equation |
|
20 |
|
21 type rewrite |
|
22 |
|
23 (* ------------------------------------------------------------------------- *) |
|
24 (* Basic operations. *) |
|
25 (* ------------------------------------------------------------------------- *) |
|
26 |
|
27 val new : reductionOrder -> rewrite |
|
28 |
|
29 val peek : rewrite -> equationId -> (equation * orient option) option |
|
30 |
|
31 val size : rewrite -> int |
|
32 |
|
33 val equations : rewrite -> equation list |
|
34 |
|
35 val toString : rewrite -> string |
|
36 |
|
37 val pp : rewrite Parser.pp |
|
38 |
|
39 (* ------------------------------------------------------------------------- *) |
|
40 (* Add equations into the system. *) |
|
41 (* ------------------------------------------------------------------------- *) |
|
42 |
|
43 val add : rewrite -> equationId * equation -> rewrite |
|
44 |
|
45 val addList : rewrite -> (equationId * equation) list -> rewrite |
|
46 |
|
47 (* ------------------------------------------------------------------------- *) |
|
48 (* Rewriting (the order must be a refinement of the rewrite order). *) |
|
49 (* ------------------------------------------------------------------------- *) |
|
50 |
|
51 val rewrConv : rewrite -> reductionOrder -> Rule.conv |
|
52 |
|
53 val rewriteConv : rewrite -> reductionOrder -> Rule.conv |
|
54 |
|
55 val rewriteLiteralsRule : |
|
56 rewrite -> reductionOrder -> LiteralSet.set -> Rule.rule |
|
57 |
|
58 val rewriteRule : rewrite -> reductionOrder -> Rule.rule |
|
59 |
|
60 val rewrIdConv : rewrite -> reductionOrder -> equationId -> Rule.conv |
|
61 |
|
62 val rewriteIdConv : rewrite -> reductionOrder -> equationId -> Rule.conv |
|
63 |
|
64 val rewriteIdLiteralsRule : |
|
65 rewrite -> reductionOrder -> equationId -> LiteralSet.set -> Rule.rule |
|
66 |
|
67 val rewriteIdRule : rewrite -> reductionOrder -> equationId -> Rule.rule |
|
68 |
|
69 (* ------------------------------------------------------------------------- *) |
|
70 (* Inter-reduce the equations in the system. *) |
|
71 (* ------------------------------------------------------------------------- *) |
|
72 |
|
73 val reduce' : rewrite -> rewrite * equationId list |
|
74 |
|
75 val reduce : rewrite -> rewrite |
|
76 |
|
77 val isReduced : rewrite -> bool |
|
78 |
|
79 (* ------------------------------------------------------------------------- *) |
|
80 (* Rewriting as a derived rule. *) |
|
81 (* ------------------------------------------------------------------------- *) |
|
82 |
|
83 val rewrite : equation list -> Thm.thm -> Thm.thm |
|
84 |
|
85 val orderedRewrite : reductionOrder -> equation list -> Thm.thm -> Thm.thm |
|
86 |
|
87 end |