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