6      !"#$%&'()*+, - . / 0 1 2 3 4 5 6 7 8 9 :;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~  Safe-Inferred23lex p is similar to p( but also consumes trailing white space.par p accpets p enclosed in parentheses ('(' and ')'). ident tabooQ parses a non-empty sequence of non-space characters not containing elements of taboo. Safe-Inferred2dropCommonPrefix xs ys removes the common prefix of xs and ys, and returns the remaining lists as a pair."dropCommonPrefix [1,2,3] [1,2,4,1] ([3], [4,1]) Safe-Inferred23A position in a term. Arguments are counted from 0.VA position describes a path in the tree representation of a term. The empty position []* denotes the root of the term. A position [0,1]] denotes the 2nd child of the 1st child of the root (counting children from left to right). p `above` q checks whether p is above q5 (in the tree representation of a term). A position p is above a position q , whenever p is a prefix of q. p `below` q checks whether p is below q, that is to say that q is above p.p `parallelTo` q checks whether p is parallel to q, that is to say that p and q do not lie on the same path. p `leftOf` q checks whether p is left of q. This is only possible if p and q@ do not lie on the same path (i.e., are parallel to each other). p `rightOf` q checks whether p is right of q. Safe-Inferred2Function applicationVariable Folding terms.Bfold (\v -> 1) (\f xs -> 1 + sum xs) (Fun 'f' [Var 1, Fun 'g' []])3 -- size of the given term 5Mapping terms: Rename function symbols and variables.+map succ pred (Fun 'f' [Var 2, Fun 'g' []])Fun 'e' [Var 3,Fun 'f' []]     Safe-Inferred2 Given a pretty printer f) for function symbols and pretty printer v for variables prettyTerm f v$ produces a pretty printer for terms     Safe-Inferred23 Like  b, but the result is wrapped in the IO monad, making this function useful for interactive testing.parseIO ["x","y"] "f(x,c)"Fun "f" [Var "x",Fun "c" []] fromString xs s parsers a term from the string s, where elements of xs are considered as variables. parse fun var is a parser for terms, where fun and varD are parsers for function symbols and variables, respectively. The var( parser has a higher priority than the fun parser. Hence, whenever var/ succeeds, the token is treated as a variable.INote that the user has to take care of handling trailing white space in fun and var. parseWST xsz is a parser for terms following the conventions of the ancient ASCII input format of the termination competition: every Char. that is neither a white space (according to ) nor one of '(', ')', or ',', is considered a letter. An identifier is a non-empty sequence of letters and it is treated as variable iff it is contained in xs.parseFun ident$ parses function symbols defined by ident.parseVar ident vars parses variables as defined by identE and with the additional requirement that the result is a member of vars.      Safe-Inferred25Rewrite rule with left-hand side and right-hand side. Safe-Inferred2kA generalised? substitution: a finite, partial map from variables to terms with a different variable type.gA substitution, mapping variables to terms. Substitutions are equal to the identity almost everywhere. Safe-Inferred2iMatch two terms. If matching succeeds, return the resulting subtitution. We have the following property: 8match t u == Just s ==> apply s t == gapply s t == u Safe-Inferred2dAnnotate each occurrence of a function symbol with its actual arity, i.e., its number of arguments.'withArity (Fun 'f' [Var 1, Fun 'f' []])"Fun ('f',2) [Var 1,Fun ('f',0) []]'Return the subterm at a given position.'Return the list of all proper subterms.;properSubterms (Fun 'g' [Fun 'f' [Var 1], Fun 'f' [Var 1]])-[Fun 'f' [Var 1],Var 1,Fun 'f' [Var 1],Var 1] Return the list of all subterms.!subterms t = t : properSubterms t&replace a subterm at a given position. AReturn the list of all variables in the term, from left to right.5vars (Fun 'g' [Var 3, Fun 'f' [Var 1, Var 2, Var 3]]) [3,1,2,3]!Difference List version of   . We have varsDL t vs = vars t ++ vs.")Return the root symbol of the given term."root (Fun 'f' [Var 1, Fun 'g' []]) Right 'f' root (Var 1)Left 1#HReturn the list of all function symbols in the term, from left to right.,funs (Fun 'f' [Var 3, Fun 'g' [Fun 'f' []]])"fgf"$Difference List version of # . We have funsDL t vs = funs t ++ vs.%Return  if the term is a variable,  otherwise.&Return ( if the term is a function application,  otherwise.'ECheck whether the term is a ground term, i.e., contains no variables.(MCheck whether the term is linear, i.e., contains each variable at most once.)?Check whether the first term is an instance of the second term.*3Check whether two terms are variants of each other.+Rename the variables in a term./rename (+ 1) (Fun 'f' [Var 1, Fun 'g' [Var 2]])"(Fun 'f' [Var 2, Fun 'g' [Var 3]]) !"#$%&'()*+ !"#$%&'()*+#$ !"+%&'()* !"#$%&'()*+  Safe-Inferred23,-.,-.-,.,-. Safe-Inferred2  !"#$%&'()*+ #  Safe-Inferred2////  Safe-Inferred240000  Safe-Inferred22Non-empty context3Hole123123132132  Safe-Inferred24gApply a substitution, assuming that it's the identity on variables not mentionend in the substitution.5 Liftting of 4G to rules: applies the given substitution to left- and right-hand side.6 Liftting of 4 to contexts.7yApply a substitution, assuming that it's total. If the term contains a variable not defined by the substitution, return .8Compose substitutions. We have 8(s1 `compose` s2) `apply` t = s1 `apply` (s2 `apply` t).9gMerge two substitutions. The operation fails if some variable is different terms by the substitutions.456789456789456789456789None23:|Unify two terms. If unification succeeds, return a most general unifier of the given terms. We have the following property: 2unify t u == Just s ==> apply s t == apply s u O(n log(n)), where n} is the apparent size of the arguments. Note that the apparent size of the result may be exponential due to shared subterms.;~Unify two terms. This is a simple implementation for testing purposes, and may be removed in future versions of this library. :;:;:; :;None2,-.0456789:;748None2<BTest whether the given predicate is true for both sides of a rule.=&Apply a function to the lhs of a rule.>&Apply a function to the rhs of a rule.? Lifting of + to L: renames left- and right-hand sides. >>> rename (+ 1) $ Rule {lhs = (Fun f [Var 1, Fun g [Var 2]]), rhs = Fun g [Var 1]} Rule {lhs = (Fun f [Var 2, Fun g [Var 3]]), rhs = Fun g [Var 2]}@ Lifting of # to F: returns the list of function symbols in left- and right-hand sides.Ufuns $ Rule {lhs = Fun 'f' [Var 3, Fun 'g' [Fun 'f' []]], rhs = Fun 'h' [Fun 'f' []]}"fgfhf"ADifference List version of @ . We have funsDL r vs = funs r ++ vs.B Lifting of   to ?: returns the list of variables in left- and right-hand sides.`vars $ Rule {lhs = Fun 'g' [Var 3, Fun 'f' [Var 1, Var 2, Var 3]], rhs = Fun 'g' [Var 4, Var 3]} [3,1,2,3,4,3]CDifference List version of B . We have varsDL r vs = vars r ++ vs.D6Check whether both sides of the given rule are linear.E=Check whether the left hand side of the given rule is linear.F>Check whether the right hand side of the given rule is linear.G?Check whether both sides of the given rule is are ground terms.HDCheck whether the left hand side of the given rule is a ground term.IECheck whether the right hand side of the given rule is a ground term.J}Check whether the given rule is erasing, i.e., if some variable occurs in the left hand side but not in the right hand side.KCheck whether the given rule is creating, i.e., if some variable occurs in its right hand side that does not occur in its left hand side.This is the dual of J . The term creatingB is non-standard. Creating rules are usually forbidden. See also O.LCheck whether the given rule is duplicating, i.e., if some variable occurs more often in its right hand side than in its left hand side.MXCheck whether the given rule is collapsing, i.e., if its right hand side is a variable.NWCheck whether the given rule is expanding, i.e., if its left hand sides is a variable.This is the dual of M . The term  expandingC is non-standard. Expanding rules are usually forbidden. See also O.OJCheck whether the given rule is non-creating and non-expanding. See also K and NP?Check whether the first rule is an instance of the second rule.Q3Check whether two rules are variants of each other.<=>?@ABCDEFGHIJKLMNOPQ<=>?@ABCDEFGHIJKLMNOPQ@ABC=>?<DEFGHIJKLMNOPQ<=>?@ABCDEFGHIJKLMNOPQNone2/<=>?@ABCDEFGHIJKLMNOPQNone2RSTUVWXYZ[\]^_`abcdefghiRSTUVWXYZ[\]^_`abcdefghifhgbedc^_`aRSTUVWXYZ[]\iRSTUVWXYZ[]\^_`abedcfhgiNone2jkljkllkjjklNone2mA rewrite strategy.nmA reduct. It contains the resulting term, the position that the term was rewritten at, and the applied rule.t1Full rewriting: Apply rules anywhere in the term.LReducts are returned in pre-order: the first is a leftmost, outermost redex.u2Outer rewriting: Apply rules at outermost redexes.,Reducts are returned in left to right order.v2Inner rewriting: Apply rules at innermost redexes.,Reducts are returned in left to right order.w9Root rewriting: Apply rules only at the root of the term.KThis is mainly useful as a building block for various rewriting strategies.xNested rewriting: Apply a rewriting strategy to all arguments of a function symbol, left to right. For variables, the result will be empty.8This is another building block for rewriting strategies.yReturn a list of contexts of a list. Each returned element is an element index (starting from 0), a function that replaces the list element by a new one, and the original element. mnopqrstuvwxy mnopqrstuvwxy nopqrsmtuvwxymnopqrstuvwxyNone2zGA critical pair. Critical pairs (should) have the following properties: $top == Context.ofTerm top pos (Term.map Left id (Rule.lhs leftRule)) left == Context.ofTerm top pos (Term.map Left id (Rule.rhs leftRule)) top == Substitution.apply subst (Term.map Right id (Rule.lhs rightRule)) right == Substitution.apply subst (Term.map Right id (Rule.rhs rightRule))  Furthermore, pos is a non-variable position of (lhs rightRule) and subst6 is a most general substitution with these properties.| left reduct}source~ right reductrule applied on left side!position of left rule applicationrule applied on right side(common substitution of the rewrite steps z{|}~ z{|}~ z{|}~z{|}~ Safe-Inferred2OApply a context to a term (i.e., replace the hole in the context by the term).XCompose two contexts (i.e., replace the hole in the left context by the right context).HCreate a context from a term by placing the hole at a specific position. Safe-Inferred2123132None2lhss rs( returns the list of left-hand sides of rslhss rs) returns the list of right-hand sides of rsLifting of Term.# to list of rules.Difference List version of  . We have funsDL r vs = funs r ++ vs.Lifting of Term.  to list of rules.Difference List version of  . We have varsDL r vs = vars r ++ vs.Returns  iff all given rules satisfy DReturns  iff all given rules satisfy EReturns  iff all given rules satisfy FReturns  iff all given rules satisfy  !Returns  iff all given rules satisfy HReturns  iff all given rules satisfy IReturns $ iff any of the given rules satisfy JReturns $ iff any of the given rules satisfy KReturns $ iff any of the given rules satisfy LReturns $ iff any of the given rules satisfy MReturns $ iff any of the given rules satisfy NReturns  iff all rules satisfy OXRestrict the rules to those only using function symbols satisfying the given predicate."None2mnopqrstuvwtNone23B #None2&RSTUVWXYZ[\]^_`abcdefghijkl RSTUVWXYZNone20Determine all critical pairs for a pair of TRSs.6Determine all inner critical pairs for a pair of TRSs.A critical pair is inner- if the left rewrite step is not a root step.2Determine outer critical pairs for a pair of TRSs.A critical pair is outer) if the left rewrite step is a root step.9Determine all critical pairs of a single TRS with itself.Unlike cps, cps'$ takes symmetries into account. See  and  for details.?Determine all inner critical pairs of a single TRS with itself.The result of  cpsIn' trs differs from  cpsIn trs trsF in that overlaps of a rule with itself are returned once, not twice.?Determine all outer critical pairs of a single TRS with itself.The result of  cpsOut' trs differs from cpsOut trs trs in two aspects::The trivial overlaps of rules with themselves are omitted.gSymmetry is taken into account: Overlaps between distinct rules are returned once instead of twice.  $None2z{|}~ z{|}~%&'()*+,-./0123456  789:;<=>?@ABCDEFGHIJKLMN 3 2 1 O P Q Q R S T U V W XYZ[\]NFGCDK^_J`abcdefgLMhhijklmnopqrsstuvwxyz{|}~v\]SWFGCDK^_J`abcdeg12 f3Ckljoterm-rewriting-0.2Data.Rewriting.PosData.Rewriting.Term.TypeData.Rewriting.Term.PrettyData.Rewriting.Term.ParseData.Rewriting.Rule.Type Data.Rewriting.Substitution.Type!Data.Rewriting.Substitution.MatchData.Rewriting.Term.Ops!Data.Rewriting.Substitution.ParseData.Rewriting.Rule.Pretty"Data.Rewriting.Substitution.PrettyData.Rewriting.Context.TypeData.Rewriting.Substitution.Ops!Data.Rewriting.Substitution.UnifyData.Rewriting.Rule.OpsData.Rewriting.Problem.TypeData.Rewriting.Problem.PrettyData.Rewriting.Rules.Rewrite Data.Rewriting.CriticalPair.TypeData.Rewriting.Context.OpsData.Rewriting.Rules.OpsData.Rewriting.Problem.ParseData.Rewriting.CriticalPair.OpsData.Rewriting.Utils.ParseData.Rewriting.Utils Data.CharisSpaceData.Rewriting.TermData.Rewriting.SubstitutionData.Rewriting.RuleData.Rewriting.ContextRuleisGroundLinearData.Rewriting.RulesData.Rewriting.ProblemData.Rewriting.CriticalPairPosabovebelow parallelToleftOfrightOfTermFunVarfoldmap prettyTermparseIO fromStringparseparseWSTparseFunparseVarlhsrhsGSubstSubstfromMaptoMapmatch withArity subtermAtproperSubtermssubterms replaceAtvarsvarsDLrootfunsfunsDLisVarisFunisGroundisLinear isInstanceOf isVariantOfrename prettyRule prettySubstCtxtHoleapply applyRule applyCtxtgApplycomposemergeunifyunifyRefbothleftright isLeftLinear isRightLinear isLeftGround isRightGround isErasing isCreating isDuplicating isCollapsing isExpandingisValidProblem startTermsstrategytheoryrules variablessymbolscommentTheory EquationsSymbolProperty RulesPair strictRules weakRulesStrategy OutermostFull Innermost StartTerms BasicTermsAllTermsallRules prettyWST' prettyWST prettyProblemReductresultposrulesubst fullRewrite outerRewrite innerRewrite rootRewritenested listContextsCPtopleftRuleleftPos rightRuleofTermlhssrhss restrictFunsProblemParseErrorSomeParseErrorUnsupportedDeclaration FileReadErrorUnsupportedStrategyUnknownParseError parseFileIOfromFilefromCharStreamcpscpsIncpsOutcps'cpsIn'cpsOut'lexparidentdropCommonPrefix parallelToRef $fPrettyTermidentWSTGSunGScomposeMghc-prim GHC.TypesTrueFalsebinding $fPrettyRule prettyGSubst$fPrettyGSubst$fPrettyGSubst0base Data.MaybeNothingAnnotFunPFunAVarAUnifyMfunarisolveexpandmkNodeacyclicandMvarsSvarsMS printWhen$fPrettyProblem WSTParser ParserState modifyProblemparsedVariables startterms$fErrorProblemParseErrorContextcpWcontextscpcpOutcpIn