The basic type of rewrites. A RewriteM m f l rewrites a term of signature f, sort l, to another such term, with effects in monad m

Rewrite m f l is equivalent to TranslateM m f l (f l).

A rewrite with no effects

An effectful rewrite that runs on terms of any sort

A rewrite that runs on terms of any sort and has no effects

Lifts a translation into the Maybe monad, allowing it to fail

Turns a rewrite that may fail into one that unconditionally succeeds, replacing failures with identity.

The rewrite that always fails

Turns a rewrite that runs on a single sort to one that runs on any sort, failing for all other sorts.

Turns a failable rewrite on one sort l into a rewrite that always succeeds, and runs on any sort, performing the identity rewrite on terms of sort other than l. Defined tryR . dynamicR

Turns a rewrite that runs on a single sort to one that runs on any sort, failing for all other sorts. Equivalent to dynamicR

Applies two rewrites in suceesion, succeeding if one or both succeed

Left-biased choice -- (f <+ g) runs f, and, if it fails, then runs g

Applies a rewrite to all immediate subterms of the current term. Ignores holes.

Like allR, but runs on the children in reverse order

Applies a rewrite to all immediate subterms of the current term, succeeding if any succeed

Applies a rewrite to the first immediate subterm of the current term where it can succeed

Runs a stateful computation on all immediate children of the current term.

Let f be a rewrite with an extra Int parameter, intended to be called f i t, where t is a term and i is the index of t among its parent's children. Then allIdxR f x runs f on all children of x.

Runs a rewrite in a top-down traversal Defined: alltdR f = f >=> allR (alltdR f)

Runs a rewrite in a bottom-up traversal. Defined: allbuR f = allR (allbuR f) >=> f

Runs a rewrite in a top-down traversal, succeeding if any succeed. Defined: anytdR f = f >+> anyR (anytdR f)

Runs a rewrite in a bottom-up traversal, succeeding if any succeed. Defined: anybuR f = anyR (anybuR f) >+> f

Like allbuR, but runs in right-to-left order

Runs a rewrite in a top-down traversal, succeeding if any succeed, and pruning below successes. Defined: prunetdRF f = f <+ anyR (prunetdRF f)

Like prunetdRF, but the outer level always succeeds. Defined tryR . prunetdRF

Applies a rewrite to the first node where it can succeed in a top-down traversal. Defined: onetdR f = f <+ oneR (onetdR f)

Applies a rewrite to the first node where it can succeed in a bottom-up traversal. Defined: onebuR f = oneR (onebuR f) <+ f

The identity rewrite

Wraps a rewrite with one that performs a debug-print of each visited node

isSortR (Proxy :: Proxy l) performs the identity rewrite at terms of sort l, and fails for all other terms.

A single-sorted translation in the Identity monad

A monadic translation for a single sort

A monadic translation for all sorts

Takes a boolean function of a term, and converts False values to failure in the monad

Guarded choice: guardedT g t e runs t ("then branch") on its input if g succeeds, and otherwise runs e ("else branch")

Fold a tree in a top-down manner. Includes some rudimentary parallelism.

An always successful top-down fold, replacing failures with mempty.

Runs a translation in a top-down manner, combining its effects. Succeeds if any succeeds. When run using MaybeT, returns its result for the last node where it succeded

f + g runs f and g in sequence, ignoring the output of f, and returning the output of g.

isSortT (Proxy :: Proxy l) is the translate that succeeds for terms of sort l, and fails elsewhere

The translation that always fails

Takes a translation, and replaces success with failure, and replaces failure with the identity rewrite

Allows a one-sorted translation to be applied to any sort, failing at sorts different form the original

Runs a failable computation, replacing failure with mempty

Runs a translation on each node which returns a value in some monoid, and combines the results.