Rewriting

In MimIR, rewriting means rebuilding an IR graph, usually into a target World, while preserving sharing and handling mutable nodes correctly. The rewriting infrastructure is used for tasks like copying IR between worlds, rebuilding terms after substitutions, and reconstructing terms after local changes. It is also the foundation of several phase families.

Rewriter

Rewriter walks a graph of Defs and constructs corresponding nodes in a target world. It memoizes the mapping from old to new nodes, so a node referenced multiple times is rebuilt once and shared - rewriting is graph-aware rather than tree-only.

The same map makes rewriting terminate on recursive structures. A mutable is rebuilt by first creating a stub, mapping old mutable to stub, and only then rewriting and filling its operands. A recursive reference thus resolves to the stub instead of recursing forever.

auto rw      = mim::Rewriter(new_world);
auto new_def = rw.rewrite(old_def);

Scopes

A rewrite often has to map an old node to something that is only valid locally: a binder's Var to a fresh representative, a loop index to one particular literal, and so on. For this, the map is a stack of scopes. push(old_vars, new_vars) opens a scope that owns two sets of Vars - one of the old world, one of the new - and pop() discards it together with all of its mappings. The bottom scope - the root - is always there.

A scope does not take every mapping recorded while it is open, though. map(old, new) files the mapping into the innermost scope whose old Vars old mentions or whose new Vars new mentions as free variables; any other mapping goes into the root. So only what actually depends on the local binding dies with the scope, while everything context-free stays shared across sibling scopes and beyond. For instance, rewrite_mut_Seq scalarizes «i: n; body» by rewriting body once per i, each time under

push(Vars(var));
map(var, world().lit_idx(n, i));
auto new_op = rewrite(seq->body());
pop();

Only those parts of body that mention var are rebuilt for every i; the rest is rewritten once and found in the root on the next iteration.

Dependencies propagate:

• If a mutable binder is mapped into a scope, its own Var joins that scope's old Vars, so whatever its body builds from that Var lands there, too.
• bind_old(var) and bind_new(var) add a Var to the innermost scope by hand. The latter is for a fresh binder of the new world whose Var should keep new nodes local - e.g. the continuation cps::phase::Conv introduces when lifting a call.

lookup() searches the scopes from innermost to root.

Nested Rewriters

Sometimes the same old node must be rewritten differently depending on where it occurs. Scalarize, for example, flattens a function type Cn [[A, B], C] to Cn [A, B, C] everywhere - except in what the signature of an interface Lam (an external, an annex, or a foreign declaration) mentions, which must keep its shape. A single map cannot hold both results.

Hence, such a rewrite runs a second Rewriter with a map of its own that rebuilds only what differs and hands everything else back to the outer one:

const Def* Scalarize::Keep::rewrite(const Def* old_def) {
    if (!has_cn(old_def) && !has_intersection(old_def)) return sca_.rewrite(old_def);
    bind_old(old_def->has_var());
    return Rewriter::rewrite(old_def); // rebuilds a Pi without flattening it
}

Whatever does not mention a Cn - or the Var of a binder rebuilt in here - is thus rewritten once and shared, while the nested map dies with the nested Rewriter. Where values of the two shapes meet, the RWPhase coerces between them.

Mutable Rewrites

Putting it together, a mutable is rebuilt as follows:

1. create the replacement stub,
2. map old mutable to stub immediately,
3. map binder-local substitutions - in a pushed scope if they must not outlive this rewrite,
4. rewrite and set the operands,
5. pop the scope again.

rewrite_stub implements steps 2 and 4, and finally tries to immutabilize the result in hindsight. Custom phases mirror this pattern when they need more control - e.g. to map an old Var to something other than the new mutable's Var. The crucial point is that recursive self-references must see the stub instead of triggering another rebuild of the same node.

If a rewrite replaces an external mutable with a fresh one, preserve the root explicitly by calling mim::Def::transfer_external or re-externalizing the replacement node.

Reshaping Aggregates

A rewrite that changes a mutable's number of ops - dropping components of a Sigma, say - cannot use the plain rewrite_stub: that one rewrites old->op(i) into new->op(i) for every i. The overload rewrite_stub(old, new, new2old) spells out the op indices instead: new->op(i) is rewritten from old->op(new2old[i]). Everything else stays the same - mapping the stub before descending into it, entering it as curr_mut(), and immutabilizing the result in hindsight unless something already captured the stub recursively. If you fill a stub entirely by hand, seal is that last step on its own.

Sieve computes such an index list from a predicate over the old components:

auto keep = mim::Sieve(old_sigma->ops(), [&](const Def* op) { return !old_world().inhabitant(op); });
if (keep.all()) return RWPhase::rewrite_mut_Sigma(old_sigma);
 
auto new_sigma = new_world().mut_sigma(rewrite(old_sigma->type()), keep.num_new());
return rewrite_stub(old_sigma, new_sigma, keep.new2old());

For an immutable aggregate, Sieve::gather picks the surviving ops directly.

Dropping a component shifts the indices of its successors, so every Extract and Insert into that aggregate needs its index adjusted. This is what keep[i] answers - or Sieve::Gone, if that component did not survive:

auto new_index = keep[mim::Lit::as(extract->index())];

Note

Only a Sigma ever needs this. An Arr's components all share one type, so it is dropped as a whole, and World::extract_fused splits a fused index at the Arr boundary - which leaves a Sigma's index scalar.

Adding Components

A rewrite that also adds components - mem::SEO threads a fresh φ parameter through a Lam for every promoted slot - cats them as further candidates behind the old ones:

auto keep = mim::Sieve(old_lam->tvars(), [&](const Def* var) { return is_kept(var); });
keep.cat(phis.size(), [&](size_t i) { return is_kept(phis[i]); });

They extend the very same index space, so one Sieve still answers the whole new layout: num_new is the new arity, keep[i] the new index of an old component, and keep.cat(i) the new index of an concat'ed one. all then means the new aggregate is the old one - nothing dropped and nothing appended. Since an appended component has no old op to rewrite from, new2old - and hence rewrite_stub - is unavailable once you append.

Warning

Dropping decides per type, but some shapes are not the phase's to change: an Axm's signature, or the dependent domain an App instantiates ([n: Nat, «n; *»] vs [Nat, []]). Where a reshaped value meets such a shape, it must be converted back - this is what every RWPhase does; SingleErasure relies on it.

Preserving Metadata

Most rebuilds preserve debug metadata explicitly. The default Rewriter restores the old debug info with new_def->set(old_def->dbg_key()), which just copies the interned index instead of re-interning the Dbg. Hand-written transformations commonly propagate names or add derived names with helpers such as mim::Def::debug_suffix.

If you create a replacement node that should still be recognizable in dumps, diagnostics, or generated code, preserve or adapt its debug payload immediately instead of treating naming as an afterthought.

VarRewriter

VarRewriter substitutes Vars and is nothing but a Rewriter whose root scope owns the substituted Vars: add(var, arg) maps var ↦ arg and bind_olds var.

On top of that, it only rebuilds what can change at all. A node without free variables in any scope's Vars is returned as is, so unaffected subgraphs are skipped entirely. Entering a mutable binds the mutable's own Var, since a binder that gets rebuilt changes its Var, too.

auto result = mim::VarRewriter(var, arg).rewrite(body);
 
auto rw = mim::VarRewriter(world);
rw.add(var1, arg1).add(var2, arg2);
auto result = rw.rewrite(def);

Use Rewriter to rebuild everything, e.g. into another world; use VarRewriter to substitute within the same world and rebuild only where necessary.

Previous	Next
Developer Guide	Phases