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