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