 |
MimIR
MimIR is my Intermediate Representation
|
|
MimIR
MimIR is my Intermediate Representation
|
This guide summarizes the typical idioms and patterns you will want to use when working with MimIR as a developer. It focuses on the C++ API and IR-building workflow.
Let's jump straight into an example.
Driver is usually the first object you create. It owns a few global facilities such as Flags, the Log, and the current World. In this example, the log is configured to write debug output to std::cerr; see also Debugging Features.
Next, we load the core and ll plugins. A plugin has two halves — a .mim file declaring its annexes and a shared library providing their runtime behavior; see Plugins & Annexes for the overview and Plugins for the details. Calling mim::ast::load_plugins parses the .mim file and also loads the shared object, while the Driver keeps track of the resulting plugin state.
Now we can build actual code.
Def is the base class for all nodes/expressions in MimIR. Each Def is a node in a graph managed by the World. You can think of the World as a giant hash set that owns all Defs and provides factory methods to create them.
In this example, we construct the main function. In direct style, its type looks like this:
In continuation-passing style (CPS), the same type looks like this:
The type mem.M 0 tracks side effects. Since main introduces variables, we must create it as a mutable lambda; see Immutables vs. Mutables.
The body of main is simple: it invokes the return continuation ret with mem and argc:
It is also important to mark main as external. Otherwise, MimIR may remove it as dead code.
Finally, we optimize the program, emit an LLVM assembly file, compile it via clang, and execute the generated binary with ./hello a b c. We then print its exit code, which should be 4.
MimIR distinguishes between two kinds of Defs: immutables and mutables.
| Immutable | Mutable |
|---|---|
| must be const | may be non-const |
| ops form a DAG | ops may be cyclic |
| no recursion | may be recursive |
| no variables | may have variables; use mim::Def::var / mim::Def::has_var |
| build ops first, then the actual node | build the actual node first, then set the ops |
| hash-consed | each new instance is fresh |
| Def::rebuild | Def::stub |
Immutables are usually constructed in one step with World factory methods. The usual pattern is: build all operands first, then create the immutable node with w.app, w.tuple, w.pi, w.sigma, and similar helpers.
For ordinary applications, mim::World::app is the direct building block:
Here, mim::World::annex yields the raw axiom node itself. That is useful when you want to partially apply a curried annex, store it, inspect it, or build the application tree step by step from C++.
If you want the full curried call in one go, prefer mim::World::call:
w.call<Id>(...) starts from w.annex<Id>() and completes the curried application for you, including implicit arguments. So the rule of thumb is:
Mutables are built in three phases:
Use mim::Def::externalize for roots that must survive cleanup and whole-world rewrites. Top-level entry points, generated wrapper functions, and replacement nodes for former externals all follow this pattern.
As a more intricate example, we build a polymorphic identity function using MimIR's C++ API.
This example illustrates how mutables and immutables interact. All binders must be created as mutables in order to access the variable they introduce. All other nodes can remain immutable.
We first build the function type {T: *} → T → T (stored in pi). Since this type introduces the implicit variable T (stored in pT), the outer Pi must be created as a mutable. Before we can retrieve this variable, we must set the domain * (w.type()). This is also the reason why the Pi itself lives one universe level above, in w.type<1>(). The name "T" is purely for debugging and has no semantic meaning.
The codomain T → T is built as an immutable Pi that refers to pT, and is then assigned as the codomain of pi.
Next, we build the actual function. The outer lambda lamT has type pi and must be mutable, since it introduces the variable T (stored in lT) of type * (the domain of pi). Even though pi also introduces a T, lamT's variable is distinct: lT is not the same variable as pT.
We then build the inner lambda lamx, which must also be mutable because it introduces the variable x of type T.
Finally, we set the body of lamx to x (using a tt filter), and set the body of lamT to lamx, again using a tt filter.
A tt filter tells MimIR to immediately β-reduce the corresponding application, giving the effect of partial evaluation.
Here we use World::call to automatically infer the implicit argument (Nat) and apply the function to 42. Because both lambdas were constructed with a tt filter, MimIR reduces the application immediately. As a result, res does not point to a function or a residual call node, but directly to the reduced result, i.e. the literal 42.
In the example above we also see that variables are only created as needed. They are immutable, and their sole operand is the binder where they were introduced.
Which variables a Def actually refers to is answered by its free variables; see below.
Many analyses and rewrites need to know which variables a Def still refers to. For example, a Def can only be hoisted to an outer scope if it does not depend on the variables introduced further in.
Recall that the operand graph is a DAG of immutables that is only ever "broken" by mutables (see Immutables vs. Mutables). MimIR exploits this by splitting the analysis at the mutable boundary:
Since mutables can be re-set, their cached free_vars() may become stale. Each mutable therefore tracks its users — the mutables that reference it — so that mutating a mutable transitively invalidates the caches of everything that (indirectly) depends on it. You do not trigger this yourself; it happens as part of set / unset.
Free variables also underpin MimIR's scopeless nesting queries:
When you only need a yes/no answer — does this subtree contain any Var, Hole, mutable, or Proxy? — mim::Def::has_dep is far cheaper than materializing free_vars(). Like local_vars(), it is a per-node bitset (see mim::Dep) that only looks up to the next mutable:
MimIR provides several ways to scrutinize Defs. Matching built-ins, i.e. subclasses of Def, works a little differently from matching axioms.
Methods beginning with
Def::isa / Def::as perform a downcast that matches both mutables and immutables:
mim::Def::isa_imm / mim::Def::as_imm only match immutables:
mim::Def::isa_mut / mim::Def::as_mut only match mutables. They also remove the const qualifier, which gives you access to the non-const methods that only make sense for mutables:
If the scrutinee is already a Def*, then Def::isa / Def::as behave the same as mim::Def::isa_mut / mim::Def::as_mut, because the missing const already implies mutability:
Often, you want to match a literal and extract its value. Use Lit::isa / Lit::as:
The following table summarizes the most important casts:
A method beginning with expect behaves like the as in the same row, but throws a formatted exception (via fe::throwf) instead of asserting; it takes a description (a plain string or a format string plus arguments) of what was expected.
| dynamic_cast static_cast throwing | Returns | If def is a ... |
|---|---|---|
| def->isa<Lam>() def->as<Lam>() def->expect<Lam>(fmt, ...) | const Lam* | Lam |
| def->isa_imm<Lam>() def->as_imm<Lam>() | const Lam* | immutable Lam |
| def->isa_mut<Lam>() def->as_mut<Lam>() def->expect_mut<Lam>(fmt, ...) | Lam* | mutable Lam |
| Lit::isa(def) Lit::as(def) Lit::expect(def, fmt, ...) | std::optional<nat_t> nat_t | Lit |
| Lit::isa<f32>(def) Lit::as<f32>(def) Lit::expect<f32>(def, fmt, ...) | std::optional<f32> f32 | Lit |
There are also several specialized checks, usually provided as static methods. They return either a pointer to the matched entity or nullptr.
Here are a few examples:
You can match axioms via
The result is a mim::Axm::isa<Id, D>, which wraps a const D*. Here, Id is the enum corresponding to the matched axiom tag, and D is usually an App, because most axioms inhabit a function type. In other cases, it may wrap a plain Def or some other subclass.
By default, MimIR assumes that an axiom becomes "active" when its final curried argument is applied. For example, matching %mem.load only succeeds on the final App of the curried call
whereas
does not match.
In this example, the wrapped App refers to the final application, so:
Use mim::App::decurry if you want direct access to the preceding application. See the examples below.
If you design an axiom that returns a function, you can fine-tune the trigger point of mim::Axm::isa / mim::Axm::as.
To match an axiom without subtags, such as %mem.load, use:
To match an axiom with subtags, such as %core.wrap, use:
The following table summarizes the most important axiom matches:
| dynamic_cast static_cast | Returns | If def is a ... |
|---|---|---|
| isa<mem::load>(def) as<mem::load>(def) | mim::Axm::isa specialized for mem::load and App | final curried %mem.load application |
| isa<core::wrap>(def) as<core::wrap>(def) | mim::Axm::isa specialized for core::wrap and App | final curried %core.wrap application |
| isa(core::wrap::add, def) as(core::wrap::add, def) | mim::Axm::isa specialized for core::wrap and App | final curried %core.wrap.add application |
In MimIR, there are essentially three ways to talk about the number of elements of something.
The arity is the number of elements available to extract / insert. This number may itself be dynamic, for example in ‹n; 0›.
mim::Def::num_projs equals mim::Def::arity if the arity is a mim::Lit. Otherwise, it yields 1.
This concept mainly exists in the C++ API to give you the illusion of n-ary structure, e.g.
Internally, however, all functions still have exactly one domain and one codomain.
There are also thresholded variants prefixed with t, which take mim::Flags::scalarize_threshold (--scalarize-threshold) into account.
mim::Def::num_tprojs behaves like mim::Def::num_projs, but returns 1 if the arity exceeds the threshold. Similarly, mim::Def::tproj, mim::Def::tprojs, mim::Lam::tvars, and related methods follow the same rule.
See also:
TODO
| Expression | Class | arity | num_projs | num_tprojs |
|---|---|---|---|---|
| (0, 1, 2) | Tuple | 3 | 3 | 3 |
| ‹3; 0› | Pack | 3 | 3 | 3 |
| ‹n; 0› | Pack | n | 1 | 1 |
| [Nat, Bool, Nat] | Sigma | 3 | 3 | 3 |
| «3; Nat» | Arr | 3 | 3 | 3 |
| «n; Nat» | Arr | n | 1 | 1 |
| x: [Nat, Bool] | Var | 2 | 2 | 2 |
| ‹32; 0› | Pack | 32 | 32 | 1 |
The last line assumes mim::Flags::scalarize_threshold = 32.
There are several ways to iterate over a MimIR program. Which one is best depends on what you want to do and how much structure you need during the traversal.
The simplest approach is to start from World::annexes and World::externals and recursively visit Def::deps. Oftentimes, you can use World::roots if you don't need to distinguish between annexes and externals:
In practice, though, you will usually want to use the phase infrastructure instead.
1.16.1