(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Rewrite =
sig
(* ------------------------------------------------------------------------- *)
(* Orientations of equations. *)
(* ------------------------------------------------------------------------- *)
datatype orient = LeftToRight | RightToLeft
val toStringOrient : orient -> string
val ppOrient : orient Print.pp
val toStringOrientOption : orient option -> string
val ppOrientOption : orient option Print.pp
(* ------------------------------------------------------------------------- *)
(* A type of rewrite systems. *)
(* ------------------------------------------------------------------------- *)
type reductionOrder = Term.term * Term.term -> order option
type equationId = int
type equation = Rule.equation
type rewrite
(* ------------------------------------------------------------------------- *)
(* Basic operations. *)
(* ------------------------------------------------------------------------- *)
val new : reductionOrder -> rewrite
val peek : rewrite -> equationId -> (equation * orient option) option
val size : rewrite -> int
val equations : rewrite -> equation list
val toString : rewrite -> string
val pp : rewrite Print.pp
(* ------------------------------------------------------------------------- *)
(* Add equations into the system. *)
(* ------------------------------------------------------------------------- *)
val add : rewrite -> equationId * equation -> rewrite
val addList : rewrite -> (equationId * equation) list -> rewrite
(* ------------------------------------------------------------------------- *)
(* Rewriting (the order must be a refinement of the rewrite order). *)
(* ------------------------------------------------------------------------- *)
val rewrConv : rewrite -> reductionOrder -> Rule.conv
val rewriteConv : rewrite -> reductionOrder -> Rule.conv
val rewriteLiteralsRule :
rewrite -> reductionOrder -> LiteralSet.set -> Rule.rule
val rewriteRule : rewrite -> reductionOrder -> Rule.rule
val rewrIdConv : rewrite -> reductionOrder -> equationId -> Rule.conv
val rewriteIdConv : rewrite -> reductionOrder -> equationId -> Rule.conv
val rewriteIdLiteralsRule :
rewrite -> reductionOrder -> equationId -> LiteralSet.set -> Rule.rule
val rewriteIdRule : rewrite -> reductionOrder -> equationId -> Rule.rule
(* ------------------------------------------------------------------------- *)
(* Inter-reduce the equations in the system. *)
(* ------------------------------------------------------------------------- *)
val reduce' : rewrite -> rewrite * equationId list
val reduce : rewrite -> rewrite
val isReduced : rewrite -> bool
(* ------------------------------------------------------------------------- *)
(* Rewriting as a derived rule. *)
(* ------------------------------------------------------------------------- *)
val rewrite : equation list -> Thm.thm -> Thm.thm
val orderedRewrite : reductionOrder -> equation list -> Thm.thm -> Thm.thm
end