1(* ========================================================================= *)
2(* ORDERED REWRITING                                                         *)
3(* Copyright (c) 2003-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6signature mlibRewrite =
7sig
8
9type 'a pp = 'a mlibUseful.pp
10type term  = mlibTerm.term
11type thm   = mlibThm.thm
12
13type rewrs
14datatype orient = LtoR | RtoL | Both
15
16(* Basic operations *)
17val empty : (term * term -> order option) -> rewrs
18val reset : rewrs -> rewrs
19val peek  : rewrs -> int -> (thm * orient) option
20val size  : rewrs -> int
21val eqns  : rewrs -> thm list
22
23(* Add an equation into the system *)
24val add : int * thm -> rewrs -> rewrs
25
26(* Rewriting (the order must be a refinement of the initial order) *)
27val rewrite : rewrs -> (term * term -> order option) -> int * thm -> thm
28
29(* Inter-reduce the equations in the system *)
30val reduced : rewrs -> bool
31val reduce' : rewrs -> rewrs * int list          (* also returns new redexes *)
32val reduce  : rewrs -> rewrs
33
34(* Pretty-printing *)
35val pp_rewrs        : rewrs pp
36val rewrs_to_string : rewrs -> string
37
38(* Rewriting as a derived rule *)
39val REWRITE     : thm list -> thm -> thm
40val ORD_REWRITE : (term * term -> order option) -> thm list -> thm -> thm
41
42end
43