Control.Rewrite

Strategy combinators: a pass as a composition of small local rules instead of a hand-written recursive match.

A rewrite is a partial function on nodes, (a) -> Option(a), where None means “this rule does not apply here”. That one convention is what makes left-biased choice, try, and a fixpoint expressible; a rule that always succeeded could not say where it declined, and a traversal could not tell a no-op from a hit. A strategy is an ordinary higher-order function over rewrites, so the whole layer is plain Prism and stays readable as such.

The row tail ! {| e} runs through every signature, so one rewrite works pure and effectful: a rule may draw fresh names from Control.Fresh, record refusals through Control.Validate, or read an environment through Control.Reader, and the pure case is the same code at the empty row. The traversal schemes never mention an effect; they thread whatever the rule brings.

Determinism is structural. Children are visited in the layer’s kids order, which for the surface tree is source order, so a rewrite’s node sequence is a pure function of the tree. The fixpoint closer takes explicit fuel and reports whether it converged, so a diverging rule set is a failed assertion rather than a hang.

Types

Rewrite

alias Rewrite(a, e) = (a) -> Option(a) ! {| e}

A partial rewrite on nodes of sort a: Some for a rule that applied here, None for one that declined.

The row variable e is the whole story on effects. It is open and it is threaded, never discharged: a rule that needs nothing instantiates it to the empty row and reads as a pure function, and a rule that draws fresh names or records refusals instantiates it to whatever it uses. No combinator below handles, masks, or requires an effect, so a caller never installs a handler to satisfy the traversal, only to satisfy its own rule.

RwFix

type RwFix(a) = RwFix { tree: a, steps: Int, converged: Bool }

The outcome of a fueled fixpoint: the tree it reached, how many steps it took, and whether it converged. converged is false exactly when the fuel ran out with the rewrite still applying, which is the only way a caller learns that a rule set does not terminate on this input.

Functions and Values

rw_id

rw_id : forall a. (a) -> Option(a)

The rewrite that accepts every node and changes nothing: the unit of rw_then and the right-hand side of rw_try. Never declines, always terminates.

rw_fail

rw_fail : forall a. (a) -> Option(a)

The rewrite that declines everywhere: the unit of rw_or_else. Always declines, always terminates.

rw_then

rw_then : forall e0 a. ((a) -> Option(a) ! {e0}, (a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0}

Run s1, then s2 on its result. Declines if either declines, so a sequence is all-or-nothing and s2 never sees a node s1 refused. Terminates whenever both do.

rw_or_else

rw_or_else : forall e0 a. ((a) -> Option(a) ! {e0}, (a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0}

Left-biased choice: run s1, and only if it declines run s2 on the original node, not on anything s1 produced. Declines only when both decline. The bias is the point; a rule list is an rw_or_else chain and the first matching rule wins, exactly as a hand-written match would. Terminates whenever both do.

(rw_or_else(positive, times_ten)(2), rw_or_else(positive, times_ten)(-2))

(Some(3), Some(-20))

rw_try

rw_try : forall e0 a. ((a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0}

Make a rewrite total: s where it applies, the node unchanged where it declines. The result never declines, which is what the traversal schemes want when a rule is meant to fire only in places. Terminates whenever s does.

rw_at

rw_at : forall e0 a. ((a) -> Bool ! {e0}, (a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0}

Run s only at nodes satisfying q, declining everywhere else and declining wherever s itself declines. The cheap way to scope a rule without folding the test into the rule itself. Terminates whenever q and s do.

rw_where

rw_where : forall e0 a. ((a) -> Bool ! {e0}) -> (a) -> Option(a) ! {e0}

The rewrite that accepts exactly the nodes satisfying q, unchanged, and declines at the rest. Useful as the left half of an rw_then guard. Terminates whenever q does.

rw_apply

rw_apply : forall e0 a. ((a) -> Option(a) ! {e0}, a) -> a ! {e0}

Run a rewrite for its result, keeping x when it declines, so the decline becomes a no-op rather than a value the caller has to unwrap. The usual way to finish: a traversal wrapped in rw_try never declines, and this drops the Option. Terminates whenever s does.

rw_all

rw_all : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0}

Run s on every immediate child and rebuild. Declines if any child declines, and then declines as a whole: no partial rebuild is ever returned, so a failed child cannot leave a half-rewritten node. At a leaf there is nothing to decline, so it accepts unchanged, which is the base case every recursive scheme bottoms out on. One pass over the children, so it terminates whenever s does.

rw_one

rw_one : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0}

Run s on the leftmost child that accepts, leaving the others alone. Declines when no child accepts, so at a leaf it always declines. That decline is essential because it tells the fixpoint schemes below there is no redex left. One pass over the children, so it terminates whenever s does.

rw_bottom_up

rw_bottom_up : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0} ! {e0}

Children first, then the node: rewrite every child with rw_bottom_up, then run s on the rebuilt node. Declines if s declines anywhere, at any depth, because rw_all and rw_then are both all-or-nothing, so the usual spelling is rw_bottom_up(p, rw_try(rule)) and the bare form is for a rule that really must fire at every node.

Terminates whenever s does. The recursion descends the input tree, and each of its nodes is visited exactly once, so nothing s produces is ever traversed. A rule that grows the tree is therefore safe here.

rw_top_down

rw_top_down : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0} ! {e0}

The node first, then children. Same all-or-nothing decline discipline as rw_bottom_up, and a node rewritten here is not revisited, so a rule that produces a shape it also matches fires only once per position; closing that over is what rw_outermost is for.

Termination is conditional, unlike rw_bottom_up. The children traversed are those of the rewritten node, so a rule that reproduces a matching node below itself descends forever. Where that is possible, use rw_bottom_up, or use rw_outermost, whose fuel bounds it.

rw_everywhere

rw_everywhere : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}, a) -> a ! {e0}

Run s everywhere it applies, bottom up, and keep the result. The common case: a total pass built from a partial rule. Cannot decline, because rw_try turns every refusal into “leave this node alone”; a rule that applies nowhere returns the tree unchanged. Terminates whenever s does.

rw_everywhere(json_layer(), bump, JArr([JInt(1), JBool(true), JInt(2)]))

Json.JArr([Json.JInt(2), Json.JBool(true), Json.JInt(3)])

rw_everywhere_td

rw_everywhere_td : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}, a) -> a ! {e0}

Run s everywhere it applies, top down, and keep the result. Cannot decline, on the same grounds as rw_everywhere, and carries rw_top_down’s conditional termination: a rule that rebuilds a matching node below itself does not terminate here.

rw_once_bottom_up

rw_once_bottom_up : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0} ! {e0}

The single leftmost-innermost application of s: try the children first, and only if none accepted try the node, so exactly one node changes. Declines when s applies nowhere in the tree, which is the termination test the fixpoint schemes read. Terminates whenever s does: one pass, no rewritten output is traversed.

rw_once_top_down

rw_once_top_down : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}) -> (a) -> Option(a) ! {e0} ! {e0}

The single outermost-leftmost application of s: try the node first, and only if it declined try the children, so exactly one node changes. Declines when s applies nowhere in the tree. Terminates whenever s does: the descent happens only along the declining path, so no rewritten node is revisited within one application.

rw_repeat

rw_repeat : forall e0 a. ((a) -> Option(a) ! {e0}, Int, a) -> Control.Rewrite.RwFix(a) ! {e0}

Apply s to its own output until it declines, at most fuel times.

Always terminates, whatever s does, and that is the whole reason it exists. The termination condition is explicit: stop when s declines, reporting converged = true and the number of applications; or stop when fuel applications have been made and s still accepts, reporting converged = false and the tree as it stood before the refused step. There is deliberately no unfueled closer, because a rewrite loop that may not terminate should be a value a test can assert on rather than a hang. Zero or negative fuel yields the input unchanged, converged only if s declines on it.

let r = rw_repeat(down, 10, 3)
(r.tree, r.steps, r.converged)

(0, 3, true)

rw_innermost

rw_innermost : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}, Int, a) -> Control.Rewrite.RwFix(a) ! {e0}

Rewrite to a fixpoint innermost-first: repeat the single leftmost-innermost application until no rule applies. The normalizing order, so a rule that exposes a new redex below itself is picked up on the next step.

Always terminates, bounded by fuel steps. It converges exactly when s declines at every node of the tree it reaches; converged = false means the fuel ran out with a redex still present, and is the honest report that this rule set does not normalize this input in that budget. Never declines: the result is a record, and a rule that applies nowhere converges in zero steps.

rw_outermost

rw_outermost : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}, Int, a) -> Control.Rewrite.RwFix(a) ! {e0}

Rewrite to a fixpoint outermost-first: repeat the single outermost-leftmost application until no rule applies. The lazy order, which reaches a normal form for rules whose innermost order diverges, and the fueled way to run a rule that rw_top_down would descend into forever.

Always terminates, bounded by fuel steps, with the same convergence report as rw_innermost. Never declines.

rw_choose

rw_choose : forall e0 a. (List((a) -> Option(a) ! {e0})) -> (a) -> Option(a) ! {e0}

The first rule in the list that applies, run on the original node. Declines only when every rule declines, and an empty list is rw_fail. A rule table is an ordinary list, read in order, so priority is where the reader can see it. Terminates whenever every rule does; the list is finite and each rule is tried at most once.

rw_pipeline

rw_pipeline : forall e0 a. (List((a) -> Option(a) ! {e0})) -> (a) -> Option(a) ! {e0}

Run every rule in order, each on the previous result, keeping the node where a rule declines. Unlike rw_choose this is a pipeline, not a choice: all of them run. Never declines, so a stage’s refusal is invisible to the caller and an empty list is rw_id. Terminates whenever every rule does; each runs exactly once.

rw_lift

rw_lift : forall e0 a. ((a) -> a ! {e0}) -> (a) -> Option(a) ! {e0}

Lift a total node function into a rewrite that always accepts. The bridge for an existing (a) -> a helper. Never declines, which makes it unsuitable as a fixpoint body: rw_repeat would never see the decline it stops on. Use rw_lift_changed there. Terminates whenever f does.

rw_lift_changed

rw_lift_changed : forall e0 a. ((a) -> a ! {e0}, (a, a) -> Bool ! {e0}) -> (a) -> Option(a) ! {e0}

Lift a total node function into a rewrite that accepts only where it changed something, given an equality. Declines exactly where f is the identity, which is what turns a normalizer into a rule a fixpoint can close over: the loop stops when the function stops moving. Terminates whenever f and same do.

rw_steps

rw_steps : forall e0 a. (Control.Layer.Layer(a), (a) -> Option(a) ! {e0}, a) -> List(a) ! {e0}

Every result of applying s at each node of the tree in turn, one rewritten tree per node that accepted, in preorder. The enumeration a search or a mutation-testing pass wants: not one normal form, but every single-step neighbour.

Never declines; a rule that applies nowhere yields the empty list, and a decline at a node simply contributes nothing there. Terminates whenever s does, visiting each node of the input tree exactly once and never traversing a rewritten result.