# Compositional Flexible Memory Representations for Algebraic Data Types

Thaïs Baudon, Gabriel Radanne, Laure Gonnord

<figure><img src="image_1.png" /></figure>

## To cite this version:

Thaïs Baudon, Gabriel Radanne, Laure Gonnord. Compositional Flexible Memory Representations for Algebraic Data Types. 9495, Inria. 2022. [hal-03940742](https://hal.science/hal-03940742v1)

HAL Id: hal-03940742

https://hal.science/hal-03940742v1

Submitted on 21 Aug 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Inria

Compositional Flexible
Memory Representations
for Algebraic Data Types

Thaïs BAUDON, Laure GONNORD, Gabriel RADANNE

RESEARCH
REPORT

Nº 9495

Decembre 2022

Project-Teams CASH
<figure><img src="image_3.png" /></figure>
<figure><img src="image_4.png" /></figure>

# Compositional Flexible Memory Representations for Algebraic Data Types

Thaïs BAUDON*, Laure GONNORD†, Gabriel RADANNE‡

Project-Teams CASH

Research Report n° 9495 — Decembre 2022 — 36 pages

**Abstract:** Initially present only in functional languages such as OCaml and Haskell, Algebraic Data Types have now become pervasive in mainstream languages, providing nice data abstractions and an elegant way to express functions though *pattern matching*. Numerous approaches have been designed to compile rich pattern matching to cleverly designed, efficient decision trees. However, these approaches are specific to a choice of *memory representation* which must accommodate garbage collection and polymorphism.

ADTs now appear in languages more liberal in their memory representation. Notably, Rust is now introducing more and more memory optimisations. As memory representation and compilation are interdependent, it raises the question of pattern matching compilation for highly customised layouts.

We propose to ease the experimentation of new, custom layouts in the early stages of compiler development by providing specification tools and a complete synthesis chain to generate pattern matching compilation procedures.

In this article, we present a novel way to specify *compositional* memory layouts, for which we automatically synthesise elementary builders and accessors, yielding a correct representation-specific compilation algorithm. This approach is implemented in a prototype tool *ribbit*.

**Key-words:** Algebraic Data Types, Memory Layouts, Pattern Matching, Compilation

RESEARCH CENTRE
GRENOBLE - RHÔNE-ALPES

Inovallée

655 avenue de l'Europe Montbonnot

38334 Saint Ismier Cedex

<footnote>* ENS de Lyon, LIP (UMR CNRS/ENS Lyon/UCB Lyon1/INRIA),F-69000 Lyon, France</footnote>

<footnote>† Grenoble-INP/LCIS & LIP</footnote>

<footnote>‡ Inria, LIP (UMR CNRS/ENS Lyon/UCB Lyon1/INRIA),F-69000 Lyon, France</footnote>
Compositional Flexible Memory Representations for Algebraic
Data Types

**Résumé** : Initialement présents dans les langages fonctionnels comme Ocaml et Haskell, les types algébriques sont maintenant de plus en plus présents dans les langages mainstream comme Rust. Ils permettent une abstraction commode des données et une façon élégante de décrire des fonctions via le filtrage de motifs (*pattern-matching*).

Ce rapport de recherche présente un framework facilitant la création et l'experimentation de nouvelle
représentation mémoire en fournissant un outil de specification pour les représentations, et une chaine de
synthèse completer pour générer les procedures de compilation attenante. La correction de l'algorithme est
prouvée sous une hypothèse de validité de la représentation. L'algorithme est implémenté dans l'outil ribbit.

Mots-clés : HPC, types algébriques, filtrage, compilation
# Contents

<table><tr><td>1 Introduction</td><td>4</td></tr><tr><td>2 Memory Representation of ADTs</td><td>5</td></tr><tr><td>2.1 Red-Black Trees in OCaml and Rust</td><td>5</td></tr><tr><td>2.2 Pattern Matching Optimising Compilation</td><td>6</td></tr><tr><td>2.3 Defining a Memory Representation</td><td>6</td></tr><tr><td>2.3.1 Composability</td><td>7</td></tr><tr><td>2.3.2 Distinguishability</td><td>7</td></tr><tr><td>2.3.3 Synthesis</td><td>7</td></tr><tr><td>3 Patterns and Pattern Matching</td><td>8</td></tr><tr><td>3.1 Patterns, Syntax and Semantics</td><td>8</td></tr><tr><td>3.2 Templated Compilation of Pattern Matching</td><td>9</td></tr><tr><td>4 Input Specification for Memory Layouts</td><td>12</td></tr><tr><td>4.1 Notations: Source and Memory Operations</td><td>12</td></tr><tr><td>4.2 Input Ingredients for Compositional Layouts</td><td>13</td></tr><tr><td>4.3 Example: OCaml Layout Specification</td><td>13</td></tr><tr><td>5 Synthesis of Memory Representations</td><td>14</td></tr><tr><td>5.1 Structural Interpolation</td><td>15</td></tr><tr><td>5.1.1 PREREPR<sub>t</sub> and REPRTY<sub>t</sub></td><td>16</td></tr><tr><td>5.1.2 Distinguishability Constraints</td><td>16</td></tr><tr><td>5.1.3 Composability Constraints</td><td>16</td></tr><tr><td>5.2 Representation Completion</td><td>17</td></tr><tr><td>5.3 Synthesis of Pattern Matching Primitives</td><td>18</td></tr><tr><td>6 Extensions</td><td>19</td></tr><tr><td>7 Related Works</td><td>20</td></tr><tr><td>7.1 Memory Representation and ADTs</td><td>20</td></tr><tr><td>7.2 Pattern Matching Compilation</td><td>20</td></tr><tr><td>8 Conclusion</td><td>21</td></tr><tr><td>A Source patterns</td><td>24</td></tr><tr><td>B Memory patterns</td><td>24</td></tr><tr><td>C Decision tree generation algorithm for INSPECTANDSPLIT<sup>•</sup></td><td>25</td></tr><tr><td>C.1 Memory context relations</td><td>25</td></tr><tr><td>C.2 Decision tree generation algorithm</td><td>25</td></tr><tr><td>D Full example: OCaml representation</td><td>27</td></tr><tr><td>D.1 Input specification</td><td>27</td></tr><tr><td>D.2 Primitive type t<sub>int</sub></td><td>27</td></tr><tr><td>D.3 Sum types t<sub>ABC</sub> and t</td><td>27</td></tr><tr><td>D.4 Structural interpolation</td><td>28</td></tr><tr><td>D.5 Representation completion</td><td>30</td></tr><tr><td>D.6 Pattern matching primitives</td><td>31</td></tr><tr><td>D.6.1 Composability primitives: UNWRAP<sup>•</sup></td><td>31</td></tr><tr><td>D.6.2 Distinguishability primitives: INSPECTANDSPLIT<sup>•</sup></td><td>31</td></tr><tr><td>D.7 Pattern matching compilation</td><td>32</td></tr></table>
# 1 Introduction

Algebraic Data Types (ADTs) are an essential tool to model data. They allow to group together information in a consistent way through the use of records, also called product types, and to organise options through the use of variants, also called sum types. A proper ADT support enables to:

* Model data in a way that is close to the programmer's intuition, abstracting away the details of the memory representation of said data.

* Safely handle data by ensuring via pattern-matching that its manipulation is well-typed, exhaustive and non-redundant.

* Optimise manipulation of data thanks to rich constructs understood by the compiler.

Despite these promises, Algebraic Data Types were initially only present in functional programming languages such as OCaml and Haskell. Recently, they have gained a foothold in more mainstream languages such as Typescript, Scala, Rust and even soon Java. They are however still lacking in high-performance lower-level languages. One difficulty for language designers wishing to add pattern matching to their language is that compiling a rich pattern matching language to efficient code is a non-trivial task, which is not commonly available in shared compiler frameworks such as LLVM. Indeed, such frameworks only provide optimisations for C-like switches on integers (or integer-like enumerations). Additionally, existing works on pattern matching Maranget (2008); Wadler (1987); Sestoft (1996) provide very efficient compilation schemes, but are geared towards memory representations found in GC-managed functional languages such as OCaml and Haskell: uniform representations with liberal usage of boxing. Highly non-uniform data representations such as the ones found in C++ do not easily fit.

More generally, the descriptive nature of ADTs should enable compilers to aggressively optimise the representation of terms. The simplest example is the *Option* type, whose values are either *Some* value or *None*. An easy way to represent such type is to box the value in the *Some* constructor below a pointer. However, if that value is an integer ranging from 0 to 10, we can represent it unboxed and use 11 for *None*. This optimisation is regularly done by programmers manually in for instance C++, at the price of error-prone manipulations. More complex optimisations on nested and rich data types are even more error-prone.

While these transformation are not generally easy, compilers have all the information at hand to perform them automatically on the whole program. This trove of potential optimisations has been brushed upon in recent versions of Rust, but remains largely unexplored. One reason for this lack of exploration is that ensuring the correctness of such optimising transformation is difficult. Indeed, the choice of memory representation of values in a language generally has far reaching consequences in the whole compiler, the language runtime but also it's foreign function interface and garbage collector. Compiler designers are thus legitimately careful about changes in the memory representation, where mistakes could lead to complex compilation bugs.

Unfortunately, there is no ultimate memory representation: each language has very specific demands concerning its memory representation. Some languages require great uniformity, for instance to allow for a tracing GC, other aim for the most compact representation. This prevent the development of a single highly efficient and formally proven memory representation that could be used in many languages.

We propose to address these difficulties from the perspective of a compiler designer that desires to explore various "memory optimisations" for monomorphic types and their performance regarding the pattern-matching procedure:

* We introduce a notion of *compositional* memory representation for Algebraic Data Types and define a novel specification for the compiler developer to provide such a representation.

* From this specification, and for each type of the input program, we automatically synthesise a function from values to their memory representation, along with a state-of-the-art optimising pattern matching compilation procedure tailored to the specified memory representation.

* Our synthesis procedure automatically checks that the provided specification is correct, and enforces the validity of the generated representation and the associated pattern matching compilation algorithm.

* Our framework is implemented in a tool *ribbit*.
```rust
//Colors for the Red-Black Trees
enum Color { Red, Black }

//Red-Black Trees of content T
enum RBT<T> {
    Node (Color, T, &RBT<T>, &RBT<T>),
    Empty,
}

pub fn cardinal<T>(v: RBT<T>) -> u32 {
    match v {
        Tree::Node，则：，，1，r) => 1+cardinal(*1)+cardinal(*r),
        Tree::Empty => 0
    }
}
```

<figure><img src="image_5.png" /><figcaption>Figure 2: Intermediate representation of the `cardinal` function in Rust and OCaml</figcaption></figure>

## 2 Memory Representation of ADTs

To explore in more detail the memory representation of algebraic data types, we now investigate two languages which implements ADTs: Rust and OCaml. While these languages have some common lineage, they have a very different attitude towards code emission: OCaml is a GC-managed language which factors predictability and regularity. Rust on the other hand favours performance and absolute control over low-level details. These differences result in drastically different choices in memory representation. We now focus on a concrete example of algebraic datatype which requires both expressivity and performance: Red-Black Trees.

### 2.1 Red-Black Trees in OCaml and Rust

A Rust version of *Red-Black Trees* is depicted in Fig. 1. We first define `Color`, which is either the constant `Red` or `Black`. The type definition of `RBT<T>` expresses trees as recursive data structures of content `T`. It has two cases: `Empty`, and `Node` which contains a colour, a value, and two pointers (denoted `&(..)`) to its left and right subtrees. For instance, `Node(Red, 1515, &Node(Black, 0, &Empty, &Empty), &Empty)` is a tree of type `RBT<u64>`.

The `cardinal` function takes a tree and returns its cardinal using *pattern matching*. If its argument is of the “shape” of the left-hand side of the rule then the value of the right-hand side (body) is evaluated. In Rust, pattern matching is introduced by the keyword `match` and alternatives are depicted under the form of a list of the form `p ⇒ b` where `p` is a *pattern* and `b` its body. Moreover, patterns can be nested, and the body can use named subterms. In our example, `Empty` yields a cardinal of 0 and `Node，则：，1，r)` yields a cardinal of `1+cardinal(1)+cardinal(r)`.

We now look at how Rust and OCaml compile the `cardinal` function. Both compilers provide an intermediate representation (IR) in which the pattern matching is represented as a decision tree which manipulates the underlying memory representation. We showcase simplified versions of the parts of interest in Fig. 2. OCaml’s Lambda IR represents matching using the built-in primitive `field` to access subterms inside the
<figure><img src="image_6.png" /><figcaption>Figure 3: Output of our *ribbit* compiler for the balancing code of Fig. 1 in the OCaml memory representation
This output is a decision tree whose root is on the left. Decision (square) nodes compute values from their input (low-level representation),
then branch depending on this value. Round nodes denote the final returned value of the procedure (the numbering of the matched
branch).</figcaption></figure>

representation. It uses the `if` primitive to discriminate between cases. Rust's MIR<fnref n="1" /> uses slightly lower level
operations such as dereferencing and field accesses, and a `switch` construct on memory words.

In both cases, `Red`, `Black` and `Empty` are represented as unboxed integers. The similarity stops there.
In OCaml, sum types are represented uniformly: argument-less constructors are unboxed integers, and con-
structors with arguments are pointers to a block, which always starts with a tag and some fields. In the `Node`
case, the block contains a tag and four fields. This totals 6 memory words. In Rust, `Node` is directly a struct
containing only four words. Indeed, Rust recognises that the tag (which differentiate `Node` and `Empty`) and
the colour can be both packed in a single 64bits field. The resulting type uses 4 memory words.

## 2.2 Pattern Matching Optimising Compilation

Red-Black trees famously rely on a fairly complex balancing step, which redistributes the colours depending
on the internal invariant of the data structure. Thanks to nested patterns, this step can be expressed very
compactly using the following matching:

```ocaml
match c, v, t1, t2 {
  Black, z, &Node(Red, y, &Node(Red, x, a, b), c), d
  | Black, z, &Node(Red, x, a, &Node(Red, y, b, c)), d
  | Black, x, a, &Node(Red, z, &Node(Red, y, b, c), d)
  | Black, x, a, &Node(Red, y, b, &Node(Red, z, c, d))
  => Node(Red, y, &Node(Black,x,a,b), &Node(Black,z,c,d)),
     a, b, c, d => Node (a, b, c, d),
}
```

This pattern matching inspects four arguments at the same time: the current colour `c`, the current value `v` and the sub-trees `t1` and `t2`. Since this pattern matching is at the core of a performance-sensitive data structure, we naturally want it to be as efficient as possible. This is why many pattern matching implementations come with clever heuristics and techniques to output optimised decision trees Kosarev et al. (2020); Maranget (2008); Sestoft (1996). The resulting code is highly non-trivial, as can be seen in Fig. 3.

## 2.3 Defining a Memory Representation

So far, we have kept a prudish veil on how one actually defines the memory representation of values in a
language like Rust or OCaml. This is largely because it is composed of an uncountable collection of decision
spread around the whole design of the compiler and its runtime: it affects the compilation of expressions,
creation of values, field accesses, foreign function interfaces, runtime and garbage collection code and, what
concerns us most in this article, pattern matching compilation. All these elements must naturally be kept
synchronised, at the risk of causing delicate compiler bugs. Even in a language like Rust, which favour
optimised memory layouts, incremental improvements to the representation of values has progressed slowly
due to the far-reaching nature of such changes to the compiler.

<footnote n="1">¹the Middle Intermediate Representation (MIR) is a control flow graph. We reconstruct some of its logic here for ease of reading.</footnote>
In this article, we present a framework to easily define the memory representation of a language. Our framework automatically checks, using constraint solving, that the proposed representation is well-formed – for instance, that constructors can effectively be differentiated – and synthesise two functions: one to compile pattern matches and one to turn values into their memory representation.

Our framework is based on two main insights.

1. A reasonable memory layout of values should be **composable**: for a value $v$, its subvalues can be found in its representation. For instance `Node(Red, 1515, &Node(Black, 0, &Empty, &Empty))`, `&Empty`) contains the subvalue `Node(Black, 0, &Empty, &Empty)` in its representation.

2. To yield itself to pattern matching, the memory representation of values should be **distinguishable**: one should be able to determine if an RBT value is a `Node` or an `Empty`.

To specify such a memory representation, called compositional, one should provide two operations for each type: 1. where to place subterms in the memory representation, 2. how to distinguish values. For simplicity, we only show the definition for the `RBT<u64>` type. A full compiler would provide such information for all types.

### 2.3.1 Composability

For each type, we require the position of its subterm. Concretely, this is a mapping from source values with holes to memory values with holes:

$$ 
\begin{align*}
\mathit{Node}(c : \mathit{Color}, \dots) &\rightarrow \{\{\mathit{L}_{64}, \dots\}\} \text{ with } c'[0, 1] = 2 * c + 1 \\
\mathit{Node}(\dots, i : \mathit{u64}, \dots) &\rightarrow \{\{\mathit{L}_{64}, \dots\}\} \\
\mathit{Node}(\dots, \dots, l, \dots) &\rightarrow \{\{\mathit{L}_{64}, \dots\}\} \\
\mathit{Node}(\dots, \dots, r) &\rightarrow \{\{\mathit{L}_{64}, \dots\}\} \\
\&t \rightarrow \mathit{Ptr}_{64,3l} &
\end{align*}
$$

There are many things to note here. `{}` indicates a structure: a sequence of memory word of various sizes. `_*` is an optionally sized position in the representation. Some fields are directly sized: the integer content $i$ for instance is explicitly sized as 64 bit. The sizes of $l$ and $r$, the two subtree pointers, are left unspecified and will be inferred. Numerical representation can be tweaked as we move to the memory representation: for instance, the colour $c$ is stored in the first two bits of the header word, appropriately shifted. We also indicate that the pointer is 64-bits wide, and that 3-bits are always 0 for alignment.

To enforce composability, we enforce that the “source” patterns on the left hand side should be shallow – without any subpatterns. Note that there are no mapping for `Empty`, since it doesn’t have subvalues.

### 2.3.2 Distinguishability

To distinguish values, we require a collection of discriminants that express where in memory to look, and which value would be associated to each constructor. We only need one discriminant for `RBT`:

$$ \{\{\mathit{L}_{64}, \dots\}\} \text{ with } \mathit{tag} = h[0, 0] \Rightarrow \left\{ \begin{array}{l} \mathit{Empty} \mapsto \mathit{tag} = 0 \\ \mathit{Node} \mapsto \mathit{tag} = 1 \end{array} \right\} $$

This reads as follow: “Let tag be the lowest bit of the first field of the given RBT value, if the constructor of the value is `Empty` it has `tag = 0`, if it is `Node` is has `tag = 1`”.

### 2.3.3 Synthesis

These two information are in fact completely sufficient to fully determine the memory representation of values. Our synthesis proceeds as follow:

1. We first derives a “general shape” of values. Here, this indicate that `RBT` memory values are of the shape `{\{Word<sub>64</sub>\}}` in the `Empty` case – a struct with a single 64bits integer – and `{\{Word<sub>64</sub>, Word<sub>64</sub>, Ptr<sub>64,3</sub>RBT, Ptr<sub>64,3</sub>RBT\}}` in the `Node` case – a struct with four 64bits words.
2. Based on this general shape, the missing information is inferred using constraint solving. For instance, it will determine that the word in the *Empty* case will always be 0, to distinguish with the *Node* case. This step also checks the correctness of the representation.

3. Thanks to this last step, the memory representation is fully defined. The framework synthesis a REPR• functions which returns the memory value of any given value. For instance REPR•<RBT<u64> (Node(Red, 1515, Empty, Empty) {2, 1515, Ptr<64,3>{0}}, Ptr<64,3>{0})}

4. Finally, our framework synthesise a compilation function from pattern to decision trees.

Our synthesis framework has been implemented in a tool called *ribbit*. It provides the full chain from specification of the memory representation (for now, as OCaml code), to constraint solving (using the SMT solver Z3) to pattern matching compilation. We showcase the compilation of the balancing function provided above in Fig. 3.

In the rest of this article, we formally define a language with pattern matching (Section 3), propose an input specification for *compositional representations* (Section 4) and details our synthesis procedure (Section 5). We finally sketch some extensions to our framework (Section 6).

# 3 Patterns and Pattern Matching

In this section, we present a language of patterns as well as a *generic* algorithm to compile pattern matching to decision trees.

## 3.1 Patterns, Syntax and Semantics

The PAT language, described in Fig. 4, roughly follows the syntax of ML-style languages, restricted to simple types and patterns. A matching, denoted *m*, is composed of a list of patterns. The bodies of the clauses are left unspecified here and can be composed of any expression language. Patterns, denoted *p*, are composed of constructor patterns along with variables (*x*), wildcards (`_`) and “or”-patterns (*p₁ | p₂*). Type expressions, denoted *τ*, are composed of sums, written $\sum_{0 \le i < n} K_i(t_{i,0}, \dots, t_{i,n_i-1})$ or $K_0(\tau_{0,0}, \dots, \tau_{0,n_0-1}) + \dots + K_{n-1}(\tau_{n-1,0}, \dots, \tau_{n-1,n_{n-1}-1})$, and of primitive types (essentially fixed-width signed or unsigned integers). Type environments, denoted *Γ*, contains both variable and type names, both associated to type expressions. Values, denoted *v*, follow a subset of the pattern grammar. Finally, value environments, denoted *σ*, associate variables to their values.

For ease of presentation, we assume the following:

* Types are monomorphic: all code has been specialised.

* All types are named with unique identifiers, whose definitions are stored in the type environment Γ. This allows us to segment types and break recursions. For instance the definition $\tau = A + B(i32)$ yields the type naming environment $\Gamma = \{t \mapsto A + B(t'); t' \mapsto i32\}$. Recursive types result in a cycle in the type environment.

* Patterns are *exhaustive*: all possible cases are handled.

**Dynamic Semantics** The semantics of patterns take the form of a judgement $p \vdash v \to \sigma$ meaning that pattern *p* matches value *v* and binds the variables bound in *σ*. We also define the matching judgement $\text{Match}\{p_1 | \dots | p_n\} \vdash v \to i, \sigma$ which additionally returns the index of the matched branch. In a full-fledged language, it would then trigger the evaluation of the body of the branch in question. The semantic rules are standard and shown in Appendix A.

**Static Semantics** The typing judgement, denoted $\Gamma \vdash p : t \to \Gamma'$, indicates that pattern *p* is of type *t* (defined in *Γ*) and returns a new environment $\Gamma'$ containing the new variables bound in *p*. It follows the standard rules for typing patterns, shown in Appendix A.

**Example 1** (Running example: definition). As a running example for the rest of the paper, we consider the type *t* defined in the following type naming environment:
## Patterns

<table><tr><td>p</td><td>::=</td><td> Wildcard</td></tr><tr><td></td><td>|</td><td> Variable</td></tr><tr><td></td><td>|</td><td> (Disjunction)</td></tr><tr><td></td><td>|</td><td> Constructor pattern</td></tr></table>

## Matching

$$m ::= \text{Match } \{p_1 | \dots | p_n\} \qquad (\text{Matching})$$

## Types

$$ \begin{array}{l} t ::= T \qquad (\text{Primitive type}) \\ | \sum_n K_i(t_0, \dots, t_{n-1}) \qquad (\text{Sum type}) \\ \Gamma ::= \{\bar{x}_i \mapsto \bar{\tau}_i; t_j \mapsto \tau_j\} \qquad (\text{Type env.}) \end{array} $$

## Values

$$ \begin{array}{l} v ::= z \in \mathbb{Z} \qquad (\text{Integer constant}) \\ | K(v_0, \dots, v_{n-1}) \qquad (\text{Constructor value}) \\ \sigma ::= \{x_0 \mapsto v_0; \dots; x_{n-1} \mapsto v_{n-1}\} \qquad (\text{Value env.}) \end{array} $$

<caption>Figure 4: PAT, our simplified language of patterns and types</caption>

$$ \Gamma = \left\{ \begin{array}{l} t \mapsto \text{None} + \text{Some}(t_{\text{ABC}}); \\ t_{\text{ABC}} \mapsto \text{A} + \text{B} + \text{C}(t_{\text{int}}); \quad t_{\text{int}} \mapsto \text{u32} \end{array} \right\} $$

We define the following matching problem:

$$ m_0 = \text{Match} \left\{ \begin{array}{l} | (p_0) \text{None} | \text{Some}(A) \\ | (p_1) \text{Some}(B) \\ | (p_2) \text{Some}(C(n)) \end{array} \right\} $$

* The pattern $p_0$ matches either value None or Some(A). We write $m_0 \triangleright \text{None} \rightarrow 0, \emptyset$ and $m_0 \triangleright \text{Some}(A) \rightarrow 0, \emptyset$.

* The third pattern $p_2$ matches any value of type $t$ of the form Some(C(n)), where $n$ is a value of type $t_{\text{int}}$, and binds its value to the given name. For instance, $m_0 \triangleright \text{Some}(C(42)) \rightarrow 2, \{n \mapsto 42\}$

Additionally, these patterns are well-typed:

$$ \Gamma \vdash p_0 : t \rightarrow \Gamma $$

$$ \Gamma \vdash p_2 : t \rightarrow \Gamma \cup \{n : \text{u32}\} $$

♦

## 3.2 Templated Compilation of Pattern Matching

We now quickly rephrase Maranget (2008)'s state-of-the-art pattern matching compilation algorithm to decision trees, illustrated in Example 3. Decision trees $T \in \text{Trees}$, whose grammar is described in Fig. 5, formalise the description of *nested switch cases* that we illustrated in Fig. 3.

The function `COMPILE_t`: `PAT` → `Trees` takes as input a pattern matching problem for values of a given type $t$ and outputs an equivalent decision tree for memory representations of such values. In the rest of this article, we assume that $\Gamma$ is always provided implicitly.

**Decision trees** Decision trees are composed of nodes of the form `switch(e) { C }`, consisting of an expression $e$ computing the memory value under scrutiny and of a list of cases $C$. A decision tree leaf is of the form
## Expressions

$e ::= \Delta$ (Main input)

| $e \oplus z$ where $\oplus \in \{\wedge, \vee, +, \leq, \neq, \dots\}$ (Bitwise and arithmetic operations)

| $*e$ (Pointer dereferencing)

| $e.i$ (i-th block field access)

| ... (Memory-dependent operations)

## Switch cases

$C ::= z \mapsto \mathcal{T} \cdot C$ (Regular case)

| $\mathcal{T} \mapsto \mathcal{T}$ (Default case)

| $\emptyset$ (No default case)

## Decision trees

$\mathcal{T} \in \text{Trees}$

$\mathcal{T} ::= \text{switch}(e) \{C\}$ (Decision node)

| $\text{success}(j, \{\overline{x_i \mapsto e_i}\})$ (Branch j with bindings)

| $\text{unreachable}$ (Unreachable leaf)

<caption>Figure 5: Decision trees and their expressions</caption>

$\text{success}(j, \sigma)$, which successfully returns a branch index $j$ and a set of binding expressions $\sigma$. Since we only consider exhaustive patterns, there are no failure cases.

At toplevel, decision trees take as input the main input of the whole matching, denoted $\Delta$. The scrutinee of a switch is an expression manipulating memory values (thus an expression over $\Delta$). These expressions are partially target-dependent but composed at least of dereferencing, field access and simple bitwise and arithmetic operations. The output bindings $\sigma$ are also target-dependent.

The dynamic semantics of these decision trees are similar to those of pattern matching, thus we omit their description and provide a simple example.

**Example 2** (Decision tree). The following decision tree matches an option type in the OCaml representation:

$$ \text{switch}(\Delta \& 1) \begin{cases} 1 \mapsto \text{success}(0, \emptyset) \\ 0 \mapsto \text{success}(1, \{n \mapsto *\Delta.1\}) \end{cases} $$

This first determines whether the least significant bit of $\Delta$ is 1 or 0. This determines whether a value is None (the integer 1) or a Some (a pointer). If None, we succeed with branch 0. If Some, we succeed with branch 1 and a binding environment mapping $n$ to the value inside Some, as computed by $*\Delta.1$. ♦

**Pattern matching compilation algorithm** Our algorithm $\text{COMPILE}_{t_0}(\mathcal{P})$ compiles a pattern matching problem to an equivalent decision tree using the now classic approach of *pattern matrices*. Its arguments are:

* the type of the main input value (at toplevel) $t_0$;

* a *pattern matrix* $\mathcal{P}$ in which each row encodes a case of the matching problem and each column a term to be scrutinised (allowing us, for instance, to split product patterns and choose which field to inspect first). At the end of each row, we also record its index and a binding environment. The column headers indicate which parts of the main input this column is matching against, as a subterm of the toplevel value.

$\text{COMPILE}_t$ proceeds by recursively emitting switch nodes (depicted as branching nodes in our graphical representation) and reducing the pattern matrix until exhaustion. It has five cases, depending on the shape of $\mathcal{P}$:

**empty** If $\mathcal{P}$ is empty, the algorithm fails, as exhaustive patterns should have a valid pattern for every case.

**wildcard** If the first row consists only of wildcards, the matching can only succeed as this branch accepts all values.
<figure><img src="image_7.png" /><figcaption>Figure 6: Execution of `COMPILE_t(m₀)` on the running example. Blue coloured parts depict the final decision tree (that can be used to match any value of type `t`); other parts depict pattern matrices used during the compilation procedure.</figcaption></figure>

**variable** If there exists a variable pattern $p_i^\ell$ in some row $\ell$ (and the previous rows contain no variable patterns), we introduce $p_i^\ell$ into this row's binding environment.

**or** If there exists an "or"-pattern $p_i^\ell = p_1 | p_2$ in some row $\ell$ (and the previous rows contain no "or"-patterns), we split it into two new rows.

**switch** Otherwise, an actual switch node must be generated. The aim of this switch node is to inspect the head constructor of the value contained in one of the inputs, compare it to the patterns of its column in $\mathcal{P}$, then branch to its associated subtree that performs the remaining computations (on other columns and nested values).

**Example 3** (Running example: `COMPILE_{\Delta}` function). Fig. 6 depicts the execution of `COMPILE_t(m₀)` on the running example (Example 1). The produced decision tree can then be used to “match” the memory representation of any value `v` of type `t`. It first applies the **or** rule, then the **switch** rule to decide whether the head constructor of `v` is *None* or *Some*. In the former case, it immediately stops, returning 0. In the latter case, it continues through the left branch of the tree while getting access to the subvalue “under *Some*”, for which it should decide whether it is *A*, *B* or a *C*. Finally, if this subvalue is a *C*, it should get access to the subvalue “under *C*”. Note that the detailed operation of how to discriminate between constructors such as *A*, *B* and *C* is still undefined at this point. This is indeed highly dependent on precise details of the chosen internal memory layout. ♦

**Representation dependence** While Maranget (2008)'s algorithm produces good decision trees, it was originally specific to a given memory representation (the OCaml one). In order to allow for custom representations, we must provide additional representation-specific functions to:

* extract the representation of a subvalue from the memory representation of its parent value (`UNWRAP_t^*`);

* retrieve the head constructor of a source value from its memory representation (`INSPECTANDSPLIT_t^*`).

Unfortunately, specifying these functions for each type and constructor is particularly complex. In particular, ensuring the correctness of such functions when written by hand in compiler code is delicate. Instead, we propose to *synthesise* such representation-specific functions for any custom memory representation, based on a higher-level description of the memory layout of values. In the following sections, we show how to automatically derive the *full compilation algorithm for any type*, including representation-specific functions, from a user-provided *high-level description* of the desired memory representation.
<figure><img src="image_8.png" /><figcaption>Figure 7: Memory values, types and contexts</figcaption></figure>

# 4 Input Specification for Memory Layouts

A layout, or *memory representation*, specifies how to encode values of any source type in memory, so as to be able to encode each typed value in a fully deterministic way. This section formally explains how to provide an input specification for our synthesis algorithm.

## 4.1 Notations: Source and Memory Operations

In this section, we define similar notions on the source language PAT and on memory contents. From now on, hats will denote memory-related notions: $h \in \text{Contexts}$ denotes a *source context* while $\hat{h} \in \text{Contexts}$ denotes a *memory context*.

**Source contexts, subterms of a type** Source contexts are used to deconstruct values and types. A constructor context is a constructor pattern in which all subpatterns are wildcards, except one which is another context. All contexts end with a single *hole* $\square$. The grammar for source contexts (*Contexts*) is defined below:

$$ 
\begin{array}{l}
h ::= \square \hfill (\text{Hole}) \\
\qquad | K(\_, \dots, \_, h, \_, \dots, \_) \hfill (\text{Constructor context})
\end{array}
$$

We can now define the *subterms* of a sum type expression as a set of contexts where subterms are located:

$$ \text{SubTerms}(\sum_n K_i (\overline{t_{i,j}^{n_i}})) = \left\{ K_i \left( \dots, \square, \dots, \square \right) \right\}_{\substack{0 \le i < n \\ 0 \le j < n_i}} $$

We also write $\text{SubTerms}(t)$ instead of $\text{SubTerms}(\Gamma(t))$ when $\Gamma$ is implicit from the context.

**Example 4** (Running example: subterms). From the definition of types in Example 1, we obtain:

$$ \text{SubTerms}(t) = \{\text{Some}(\square)\} \qquad \text{SubTerms}(t_{\text{ABC}}) = \{C(\square)\} $$

Constant constructors such as *None* do not yield any subterm context.

♦
**Memory Values and Types** In order to work on the internal representation of values, we consider an abstraction of memory, similar to LLVM IR's types, shown in Fig. 7. A memory value is always typed and is either a fixed-size word encoding an integer $z \in \mathbb{Z}$, written Word$_{l}$(z) and typed Word$_{l}$, a fixed-size pointer to another memory value $\hat{v}$ of type $\hat{\tau}$ with a fixed number a of address alignment bits (filled with 0s), written Ptr$_{l,a}$ and typed Ptr$_{l,a}$, or a contiguous block containing a finite number of heterogeneous memory values (fields), written $\llbracket \hat{v}_0, \dots, \hat{v}_{n-1} \rrbracket$ and typed $\llbracket \hat{\tau}_0, \dots, \hat{\tau}_{n-1} \rrbracket$. We also define a (finite) disjoint union of memory values (resp. types) to denote the possibility of several concrete memory values (resp. types) at a given location, along with a wildcard _ to denote an unspecified memory value (resp. type). The typing rules for the judgment $\vdash \hat{v} : \hat{\tau}$ are straightforward and omitted for the sake of brevity.

**Memory Contexts** A memory context, defined in Fig. 7, indicates a position within a memory value and an optional transformation of the word at this position. It consists of a coarse-grained hierarchy of structural elements – namely pointers and blocks – ending with an optionally sized “hole” _l and of finer-grained operations on the word designated by the hole. The hole of a memory context applied to a word (resp. pointer) value should match the size of this word (resp. the number of alignment bits). The hole of a memory context applied to a block must be unsized and contain the identity operation (i.e., $\Box_*$).

**Example 5** (Running example: memory contexts). Consider $t_{ABC}$ from our running example (Example 1). Its memory representation in OCaml (which we will refine later in Section 4.3) is of type $\hat{\tau} = \text{Word}_{64} \sqcup \text{Ptr}_{64,3} \llbracket \text{Word}_{64}, \text{Word}_{64} \rrbracket$. The OCaml representation maps the concrete source values A, B and C(42) to the following memory values:

$$A \mapsto \text{Word}_{64}(1)$$

$$B \mapsto \text{Word}_{64}(3)$$

$$C(42) \mapsto \text{Ptr}_{64,3} \llbracket \text{Word}_{64}(2), \text{Word}_{64}(85) \rrbracket$$

The two constant constructors A and B are mapped to odd constant values. The C constructor is mapped to a 64-bit-wide, 3-bit-aligned pointer (thus an even number), pointing to a block containing its tag 2 and a value. The integer value 42 is located in the second field of this block. As we will see in more detail in Section 4.3, integers are encoded through a 1-bit left shift and an increment $(42 \times 2 + 1 = 85)$. ♦

## 4.2 Input Ingredients for Compositional Layouts

Let t a source type such that $\Gamma(t) = \sum_n K_i(t_{i,j}^{n_i})$. In order to synthesise a full (compositional) memory representation, the user should provide:

* POSITION$_t$: SubTerms(t) $\rightarrow \tilde{\text{Contexts}}$ defines how the representation of each subvalue is composed into the representation of its parent value;

* DISCRS$_t$: $\tilde{\text{Contexts}} \times (\{K_i\}_n \rightarrow \mathbb{Z})$ is a set of discriminants. A discriminant consists of a memory context indicating where to look, and a partial mapping from constructors to integer values that can be found at this position. The discriminants should be defined such that, for each distinct pair of constructors, at least one discriminant is defined for both constructors and maps them to distinct integer values, i.e.:

$$\forall 0 \le i < j < n, \exists (\hat{h}, \text{split}) \in \text{DISCRS}_t^*, \text{split}(K_i) \ne \text{split}(K_j)$$

## 4.3 Example: OCaml Layout Specification

We now demonstrate how to specify the OCaml memory representation of values Minsky and Madhavapeddy (2021) in our framework. All computation details can be found in Appendix D.

**Informal specification** OCaml memory values are either unboxed immediates or pointers to blocks, both one word wide. OCaml blocks are contiguous word-aligned structs. Every block starts with a header word containing various metadata including a tag indicating the constructor of the underlying value. For simplicity, we ignore the remaining metadata here. An important optimisation is that argument-less constructors are represented as unboxed integers, rather than empty blocks. The integer value is the index of the constructor. In OCaml, None has the same representation as the integer value 0 (i.e., Word$_{64}$(1)), without any boxing.
To distinguish pointers from unboxed values at runtime, the least significant bit of every memory value is used as a *pointer flag*. Concretely, a memory value whose lowest bit is set to 1 contains an unboxed constant in its remaining 63 bits, while a lowest bit set to 0 indicates that the memory value is a pointer. Finally, addresses are word-aligned, guaranteeing that their 3 last bits are always 0 (for 64-bit-wide words).

**Formal OCaml layout specification** Let $t$ such that $\Gamma(t) = \sum_n K_i (\overline{t_{i,j}^{n_i}})$.

The POSITION• function gives the position of a subvalue in the “pointer-to-block” memory structure:

$$ \text{POSITION}_{t}^{\bullet} \left( K_{i} \left( \dots, \square_{j}, \dots, - \right) \right) = \text{Ptr}_{64,3} \left\{ \dots, \overline{\square_{j+1}, \dots, -} \right\} $$

The three discriminants express how to distinguish between constructors:

* $D_{\ge 0}$ distinguishes between unit and non-unit constructors by inspecting the lowest bit, which is always 1 (resp. 0) for unit (resp. non-unit) constructors:

$$ D_{\ge 0} = \left( \overline{\square[0,0]_j}; \left\{ K_i \mapsto \begin{cases} 1 & \text{if } n_i = 0 \\ 0 & \text{otherwise} \end{cases} \mid 0 \le i < n \right\} \right) $$

* $D_{=0}$ distinguishes individual unit constructors:

$$ D_{=0} = (\overline{\square_{64}}; \{K_i \mapsto 2 \times i + 1 \mid n_i = 0\}) $$

In this case, the value must be an unboxed integer, which we can inspect right away.

* $D_{>0}$ distinguishes individual non-unit constructors:

$$ D_{>0} = (\text{Ptr}_{64,3} \{\overline{\square_{64}, \dots}\}; \{K_i \mapsto i \mid n_i > 0\}) $$

In this case, the value must be a pointer to a block.

We then have $\text{DISCRS}_t^\bullet = \{D_{\ge 0}, D_{=0}, D_{>0}\}$.

**Example 6** (Running example: $t_{ABC}$ ingredients). Consider $t_{ABC}$ in our running example. As we saw in Example 5, the unit constructors $A$ and $B$ are distinguishable from $C$ by inspecting the lowest bit of the representation (which acts as a pointer flag); we also define a discriminant to distinguish $A$ from $B$ and another that solely affects $C$ (so as to obtain the expected memory structure).

$$ \text{DISCRS}_{t_{ABC}}^{\bullet} = \left\{ \left( \overline{\square[0,0]_{64}}, \begin{cases} A \mapsto 1 & C \mapsto 0 \\ B \mapsto 1 & \end{cases} \right), \right. \\ \left. (\overline{\square_{64}}, \{A \mapsto 1 \mid B \mapsto 3\}), \right. \\ \left. (\text{Ptr}_{64,3} \{\overline{\square_{64}, \dots}\}, \{C \mapsto 2\}) \right\} $$

We also define the composition of $\text{REPR}_{t_{\text{int}}}^\bullet(n)$

within $\text{REPR}_{t_{ABC}}^\bullet(C(n))$:

$$ \text{POSITION}_{t_{ABC}}^{\bullet}(C(\square)) = \text{Ptr}_{64,3} \{\overline{-, \square_{\ast}, \dots}\} $$

# 5 Synthesis of Memory Representations

We now give our complete synthesis procedure, whose overall pipeline is shown in Fig. 8, which takes as input the specification functions of Section 4.2.

It proceeds by generating partial intermediate representations of a type $t$ for each tag, which can be either a constructor or a wildcard $\top$. It then completes these intermediate representations using constraint solving. This is done in three steps:

1. *Structural interpolation* (Section 5.1) determines the memory type $\text{REPR}_{t}^{\bullet}(tag)$ of the representation of any value of type $t$ whose constructor fits tag, as well as a *memory pattern* $\text{PREREPR}_{t}^{\bullet}(tag)$ which encodes all statically known representation elements. This step proceeds by collecting all necessary structural information from the input specification and computing an “intersection” of all collected constraints. If this step succeeds, its result is a memory pattern with some remaining unsolved word contents.
<figure><img src="image_9.png" /><figcaption>Figure 8: Representation synthesis pipeline</figcaption></figure>

$$ \phi ::= \top | (\text{ops} = x_h) | (\text{ops} = z) | \phi \wedge \phi \\ \hat{p} \in \widehat{\text{Patterns}} ::= t@h | \text{Word}_\ell(\phi) | \text{Ptr}_{\ell,a}\hat{p} | \{\overline{\hat{p}}?\} | \sqcup \hat{p} $$

<caption>Figure 9: Memory patterns and word formulas</caption>

2. **Representation completion** (Section 5.2) fully determines the contents of each word. After ensuring that the intersection of all patterns is non-empty, there still remain under-specified parts. The goal of this step is to synthesise a *unique memory value*. We translate unsolved word descriptions to SMT formulas on fixed-size bitvectors. Solving these formulas yields a model that assigns a concrete value or a subterm symbol to each word, which finishes the complete synthesis of the $\text{REPR}_t^\bullet$ function. If a formula is unsatisfiable, it means that we cannot obtain a suitable representation.

3. **Synthesis of pattern matching primitives** (Section 5.3) produces the primitives needed by our templated COMPILE<sub>t</sub> algorithm. More precisely, for each source type t, we generate a function $\text{UNWRAP}_t^\bullet$ that extracts the representation of a subvalue from the representation of its parent value and $\text{INSPECTANDSPLIT}_t^\bullet$, which determines the constructor of a source value from its representation.

Each of these three steps may fail, indicating that the input specification is invalid. The rest of the section follows the synthesis pipeline. Since the representation of a type is dependent on the representation of its subtypes, we process the types of an environment Γ in the reverse prefix order.

## 5.1 Structural Interpolation

$\text{PREREPR}_t^\bullet(\text{tag})$ is representation template in which structural elements are fully determined but word contents remain unsolved. $\text{REPRTY}_t^\bullet(\text{tag})$ gives the memory type for a given tag. To generate them, we use *memory patterns*, shown in Fig. 9. Memory patterns are memory value skeletons in which word contents are specified by a formula $\phi$. A formula is either true ($\top$) or a conjunction of clauses of the form $(\text{ops}_1 = x_1) \wedge \dots \wedge (\text{ops}_m = x_m)$, where $x_k$ are concrete integers or subterm symbols and $\text{ops}_k$ are sequences of operations applied to the word contents ■. Memory patterns also feature an application case $t@h$, which stands for the (unsolved) memory representation of the subterm of type t at position h. The remaining pattern cases are similar to the previously defined memory values and types.

Memory patterns are equipped with *union* and *intersection* operations, defined in Appendix B, which allow to build them up incrementally. For instance, the following rule expresses that a pointer pattern is compatible with any word pattern whose width “fits” in its address alignment bits; the specified word contents must then be zero.

$$ \frac{\ell' \le a \quad (0)_{\ell'} \text{ satisfies } \phi}{\text{Ptr}_{\ell,a}\hat{p} \cap \text{Word}_{\ell'}(\phi) = \text{Ptr}_{\ell,a}\hat{p}} $$

Memory patterns also have an *instantiation* operation, noted $\hat{h}[\hat{p}]$ which builds a pattern from $\hat{h}$, where the hole is replaced by $\hat{p}$. This is also defined in Appendix B.
**Example 7** (Memory patterns). Word<sub>64</sub> ([0, 0] = 1) denotes any 64-bit-wide word whose lowest bit is 1. In our running example, the memory pattern t<sub>int</sub>@C(□) matches memory values representing a value of type t<sub>int</sub>. Ultimately, it will represent REPR<sub>t<sub>int</sub></sub>(v) where v is the subvalue “under C”.
♦

5.1.1 PREREPR• and REPRTY•

Let t a type and tag one of its constructors, or $\top$. PREREPR<sub>t</sub><sup>•</sup>(tag) is the intersection of all constraints pertaining to this memory layout: composability constraints, denoted $\hat{p}_t^c$ and distinguishability constraints, denoted $\hat{p}_t^d$.

$$
\mathrm{PREREPR}_{t}^{\bullet}(tag) = \hat{p}_{t}^{d}(tag) \cap \bigcap_{h \in \mathrm{SubTerms}(t, tag)} \hat{p}_{t}^{c}(h)
$$

This memory pattern intersection may be empty, in which case representation generation fails and the input
specification is deemed invalid since it provided incompatible memory patterns. Composability constraints
are defined by iterating over subterms. Crucially, this yields a natural base case for constructors without
subterms. REPRTY<sub>t</sub><sup>•</sup>(tag) is a restriction of PREREPR<sub>t</sub><sup>•</sup>(tag), where formulas are erased, yielding a memory
type. We will now define each of these constraints.

5.1.2 Distinguishability Constraints

Distinguishability constraints $\hat{p}_t^d tag$ encode that, for any given sum type $t$, the head constructor of any
memory value can be identified by inspecting some predefined memory locations. Concretely, we accumulate
all constraints on a given constructor, and then merge all constructor-specific constraints.

Let $t$ such that $\Gamma(t) = \sum_n K_i (\hat{t}_{i,j}^{n_i})$ and $K_i$ one of its constructors. We collect constraints by iterating over each discriminant and its constructors, collecting coarse-grained contexts, word operations, widths and values. For unsized memory holes (i.e., *), we use the maximal value width.

$$
C =_{\text{def}} \left\{
\begin{array}{@{}l@{}}
(\hat{h}, \ell, \text{ops}, z) \text{ where} \\
(\hat{h}', \text{split}) \in \text{DISCRS}_{t}^{\bullet} \\
(K_i \mapsto z) \in \text{split} \\
\hat{h}_{[\text{ops}_{\ell'}]} = \hat{h}' \\
\ell = (\text{if } (\ell' \text{ is } *) \text{ then } \max_{(K \mapsto z) \in \text{split}} \text{width}(z) \text{ else } \ell')
\end{array}
\right\}
$$

We now define the *specific* distinguishability pattern $\hat{p}_t^d(K_i)$ that applies to a given constructor $K_i$ by
instanciating contexts, intersecting the resulting patterns and taking the conjunction of word formulas:

$$
\hat{p}_t^d(K_i) = \bigcap_{(\hat{h}_i, \ell_i, \text{ops}_i, z_i) \in C} \hat{h}_i[\text{Word}_{\ell_i}(\text{ops}_i = z_i)]
$$

The *generic* distinguishability pattern of *t* captures the structural characteristics common to all constructors:

$$
\hat{p}_t^d(\top) = \bigcup_{K \in \text{Constrs}(t)} \hat{p}_t^d(K)
$$

5.1.3 Composability Constraints

Composability constraints $\hat{p}_t^c(h)$ encode that the memory representation of a value that fits $h$ must contain
the memory representation of its subvalue at POSITION<sub>t</sub><sup>•</sup>(h). Our goal is to collect representation constraints
for each subterm position $h$, then merge them all.

Let $t'$ be the subtype of $t$ at the hole in $h$. Inductively, we have defined the *generic representation type* of $t$: $\hat{\tau}' = \text{REPRTY}_t'(\top)$. Let $\hat{h}_{[\text{ops}_{\ell_0}]} = \text{POSITION}_t'(h)$. For the representation to be consistent, the memory hole at $\hat{h}$ must have type $\hat{\tau}'$. There are two cases:

* The memory value at position $\hat{h}$ is a proper $\ell$-bit wide word. We thus have $\hat{\tau}' = \text{Word}_\ell$ and $\ell_0 = \ell$ or $\ell_0 = *$. To link the various constraints, we introduce $x_h$, a variable that contains the integer contents at position $h$. We output the constraint $\hat{p}_t^c(h) = \hat{h}[\text{Word}_\ell(\text{ops} = x_h)]$.
* The memory value at position $\hat{h}$ is a not a word (for instance, it is a block). We necessarily have $\text{ops}_{\ell_0} = \Box_*$. Since the stored memory value is not a word, we simply recall the constraints pertaining to the position $h$ with its type $t'$ using an application pattern: $\hat{p}_t^c(h) = \hat{h}[t'@h]$.

**Example 8 (Running example: constraints).** Consider the type $t_{ABC}$ from our running example and the input ingredients of Example 6:

* $t_{ABC}$ is a sum type with three variants. For the sake of brevity, we only give $\hat{p}_{t_{ABC}}^d(C)$, which is an intersection of two memory patterns since two discriminants involve $C$:

$$ \hat{p}_{t_{ABC}}^d(C) = \text{Ptr}_{64,3} \{\{\text{Word}_{64}(\Box = 2), \dots\}\} \cap \text{Word}_1(\Box[0, 0] = 0) $$

This pattern matches memory values that have characteristics of both a 64-bit-wide, 3-bit-aligned pointer to a block with at least one field, whose first field is a 64-bit-wide word whose contents $\Box$ satisfy $\Box = 2$, and of a word or address of at least one bit whose lowest bit is 0.

* $t_{ABC}$ has one subterm $C(\Box)$. Its composability pattern is:

$$ \begin{aligned} \hat{p}_{t_{ABC}}^c(C(\Box)) &= \text{Ptr}_{64,3} \{\{\dots, \Box_*, \dots\} \} [\text{Word}_{64}(\Box = x_{C(\Box)})] \\ &= \text{Ptr}_{64,3} \{\{\dots, \text{Word}_{64}(\Box = x_{C(\Box)})\} \} \end{aligned} $$

which expresses that the representation of $C(n)$ must be a pointer to a block with at least two fields, whose second field is a word containing an (unknown) integer value $y$ such that $y = x_{C(\Box)}$, where $x_{C(\Box)}$ denotes the integer contents of $\text{REPR}_{t_{int}}^\bullet(n)$.

♦

## 5.2 Representation Completion

We have now collected all constraints on our representation into a memory pattern that contains formulas. The next step of representation synthesis consists in solving each word formula. More precisely, given $\text{PREREPR}_t^\bullet(K)$ for some constructor $K$ of $t$, we consider each memory context $\hat{h}$ such that the memory pattern $\text{Word}_{\ell_{\hat{h}}}(\phi_{\hat{h}})$ is at position $\hat{h}$ in the memory pattern $\text{PREREPR}_t^\bullet(K)$.

Let $x_{h_1}, \dots, x_{h_m}$ be all the subvalue representation variables that appear in $\phi_{\hat{h}}$. Let $\ell_1, \dots, \ell_m$ the widths of these subvalues' representations (i.e., $\text{REPRTY}_{t_k}^\bullet = \text{Word}_{\ell_k}$). Our goal is to synthesise a function that, given the subvalues' representations, builds the word of the parent value (which we denoted $\Box$ in our formula). Let $y_{\hat{h}}$ this function from bitvectors of widths $\ell_1, \dots, \ell_m$ to an $\ell_{\hat{h}}$-bit-wide bitvector. Let $\phi'_{\hat{h}} = \phi_{\hat{h}}[\Box \to y_{\hat{h}}(x_{h_1}, \dots, x_{h_m})]$ the formula with $\Box$ substituted with its (symbolic) value. Solving $\phi'_{\hat{h}}$ then consists in finding a function interpretation for $y$ that satisfies it, denoted $f_{\hat{h}}$. If $\phi'_{\hat{h}}$ is unsatisfiable, the input specification is deemed invalid.

We solve each such formula $\phi'_{\hat{h}}$ in $\text{PREREPR}_t^\bullet(K)$ and obtain suitable $f_{\hat{h}}$ interpretations. This gives us fully set values for each memory word, allowing us to define the representation function for source values of constructor $K$. In order to define the full representation function, we perform the same procedure for each constructor $K_i$ of $t$. We finally set:

$$ \begin{aligned} \text{REPR}_t^\bullet(K_i(\overline{v_j})) &= \text{PREREPR}_t^\bullet(K_i) [\text{Word}_{\ell_{\hat{h}}}(\phi_{\hat{h}}) \to \text{Word}_{\ell_{\hat{h}}}(e_{\hat{h}})] \\ \text{where } e_{\hat{h}} &= f_{\hat{h}}(\text{REPR}_{t_1}^\bullet(v_{h_1}), \dots, \text{REPR}_{t_m}^\bullet(v_{h_m})) \end{aligned} $$

**Example 9 (Running example: completion).** We admit the following representation function for the primitive type $t_{int}$: $\text{REPR}_{t_{int}}^\bullet(n) = \text{Word}_{64}(2 \times n + 1)$ (see Section 6). Let us now build $\text{REPR}_{t_{ABC}}^\bullet(K)$ for each constructor $K \in \{A, B, C\}$:

* $K = A$. Collecting constraints yields this unsolved representation:

$$ \begin{aligned} \text{PREREPR}_{t_{ABC}}^\bullet(A) &= \text{Word}_{64}(\Box[0, 0] = 1) \cap \text{Word}_{64}(\Box = 1) \\ &= \text{Word}_{64}(\Box[0, 0] = 1 \land \Box = 1) \end{aligned} $$

from which we extract the formula $\phi = (y[0, 0] = 1 \land y = 1)$ whose unknown is $y \in \{0, 1\}^{64}$ (a bitvector of size 64). The model $y = \text{Word}_{64}(1)$ satisfies $\phi$, hence $\text{REPR}_{t_{ABC}}^\bullet(A) = \text{Word}_{64}(1)$. Similarly, we obtain $\text{REPR}_{t_{ABC}}^\bullet(B) = \text{Word}_{64}(3)$.
* $K = C$. After simplification, the constraints for $C$ (from Example 8) give the following unsolved representation, in which the 64-bit-wide bitvector SMT variable $x_C(\square)$ symbolises the representation of the subvalue "under $C$":

$$ \mathrm{PREREPR}_{t_{\mathrm{ABC}}}(C) = \mathrm{Ptr}_{64,3} \left\{ \left\{ \begin{array}{l} \mathrm{Word}_{64} (\blacksquare = 2), \\ \mathrm{Word}_{64} (\blacksquare = x_{C(\square)}) \end{array} \right\} \right\} $$

The first word description leads to a constant value of 2, the second one is solved by $y = x_{C(\square)}$ and we finally get:

$$ \mathrm{REPR}_{t_{\mathrm{ABC}}}(C(n)) = \mathrm{Ptr}_{64,3} \left\{ \left\{ \mathrm{Word}_{64}(2), \mathrm{Word}_{64}(\mathrm{REPR}_{t_{\mathrm{int}}}(n)) \right\} \right\} $$

♦

## 5.3 Synthesis of Pattern Matching Primitives

We have previously asserted that the specification yield a consistent memory layout and synthesised a representation function to build memory values? We finally synthesise the pattern matching primitives introduced in Section 3.2.

**UNWRAP\_t: SubTerms(t) → Exps**

UNWRAP\_t(h) builds an expression to access the representation of the subvalue at position $h$ in a value of type $t$. The input ingredient POSITION\_t\_h(h) returns a memory context $\hat{h}$ providing this information. To obtain UNWRAP\_t\_h(h), we translate $\hat{h}$ to a target expression, as defined in Fig. 5. For instance, if POSITION\_t\_h(h) = $\{\{\dots, \square, \dots, \dots\}$, then UNWRAP\_t\_h(h) = $\Delta.i$.

**INSPECTANDSPLIT\_t: (Constrs(t) → Trees) → Trees**

INSPECTANDSPLIT\_t brach (branch) builds a decision tree given a function branch from $t$ constructors to decision trees. This primitive is more complex to build, and requires careful exploration of $t$ discriminants to emit the minimal amount of switch nodes. We proceed by iteratively generating intermediate decision trees for decreasing sets of possible constructors, starting from all constructors of $t$. We then glue these intermediate decision trees with switch nodes.

More precisely, we define the decision tree $\mathcal{T}_K$ by induction on the current set of constructors $K$:

* If $K = \{K\}$ contains a single constructor, we return $\mathcal{T}_K = branch(K)$.

* Otherwise, let us consider $H$ the set of discriminants which effectively distinguish values in $K$:

$$ H = \left\{ \hat{h} \mid \begin{array}{l} (\hat{h}, split) \in \mathrm{DISCRS}_{t} \\ \exists K, K' \in K \cap split, split(K) \neq split(K') \end{array} \right\} $$

$H$ might contain several discriminants. We choose the "shallowest" one, i.e. that doesn't look far into the representation, and name it $\hat{h}_0$. Thanks to the precondition on DISCRS\_, we show (in Appendix C) that this shallowest discriminant always exists. By our distinguishability constraints, $\hat{h}_0$ is a valid context for all values whose constructor is in $K$.

We can now build our switch node. Let $e$ the target expression returning the value located at $\hat{h}_0$ (built similarly to UNWRAP\_t). By definition, the possible values of $e$ are $V = \{z | K \in K \cap split, split(K) = z\}$. For each $z_i$ in $V$, let $K_{z_i} = \{K \in K | split(K) = z_i \lor K \notin split\}$ the constructors compatible with this result. Let $K_{\tau} = \{K \in K | K \notin split\}$ the remaining constructors. We finally obtain:

$$ \mathcal{T}_K = \text{switch}(e) \left\{ \begin{array}{l} z_0 \mapsto \mathcal{T}_{K_{z_0}} \\ \vdots \\ z_{m-1} \mapsto \mathcal{T}_{K_{z_{m-1}}} \\ \top \mapsto \mathcal{T}_{K_{\tau}} \end{array} \right. \quad \text{where } z_i \in V $$
<figure><img src="image_10.png" /><figcaption>Figure 10: Output of ribbit for our running example COMPILE_t(m₀) with the OCaml representation.</figcaption></figure>

Appendix C shows the detailed algorithm and its proof.

Finally, our representation-parametrised COMPILE_t function presented in Section 3.2 is complete and can compile any pattern matching on t values to an equivalent decision tree. We state its correctness w.r.t. the memory layout:

**Theorem 1.** Let $\Gamma$ a type environment; $t \in \Gamma$, $m$ a matching such that $\Gamma \vdash m : t \to \Gamma'$ and $\mathcal{T} = \text{COMPILE}_t(m)$. Then for any value $v$ of type $t$ such that $m \triangleright v \to i, \sigma$, the evaluation of $\mathcal{T}$ on $\text{REPR}_t^\bullet(v)$ succeeds with $i, \{x \mapsto \text{REPR}_{\Gamma(x)}^\bullet \sigma(x)\}$.

**Example 10** (Running example: INSPECTANDSPLIT$^\bullet$ generation). Let us build $\mathcal{T}_{A,B,C}$. The shallowest discriminant (See Example 6) is $D_{AB,C}$ that inspects the lowest bit of the representation, thus $e = \Delta \& 1$ that has values 0 (for C) or 1 (for A or B). The recursion for C gives branch(C). The recursion using $D_{A,B}$ is similar. We finally obtain the helper function:

$$ \text{INSPECTANDSPLIT}^\bullet_{t_{ABC}}(\text{branch}) = \text{def} \\ \text{switch}(\Delta \& 1) \left\{ \begin{array}{l} 0 \mapsto \text{branch}(C) \\ 1 \mapsto \text{switch}(\Delta) \left\{ \begin{array}{l} 1 \mapsto \text{branch}(A) \\ 3 \mapsto \text{branch}(B) \end{array} \right\} \end{array} \right\} $$

After generating all helper functions, a final call to COMPILE_t(m₀) produces the final decision tree depicted in Fig. 10. Notice that switch nodes now use concrete expressions operating on memory values to extract subvalues' representations and distinguish between constructors.

For space reasons, we only gave a partial development of our running example in the OCaml representation. For the (far too extensive) details see Appendix D. ♦

# 6 Extensions

So far, we only showed the basic pattern constructs: sum types. Modern pattern languages have many additional constructs. We now sketch several extensions of our framework. These extensions are implemented in our prototype.

**Reference and product types** References and product are degenerate cases of sum types with only one case. Our framework trivially extends to these constructs, with the simplification that DISCRS$^\bullet$ is always empty for these types (as there is nothing to be distinguished).
**Primitive types** Users may wish to pattern match on primitive types. At first glance, primitive types are similar to sum types where each constant is a unit constructor. Unfortunately, the number of distinct values ($2^{64}$ for native integers) makes such definition of DISCRS• too large and the solving step intractable. Furthermore, primitives types are not always finite (big integers).

To alleviate this issue, we extend the notion of DISCRS• to work on *sets of values* which should be treated the same, as if we had several sum type constructors with a single field containing the individual value. Formally, for each *T* a primitive type, we require an additional ingredient VALSETS•<sub>*T*</sub> which defines a partition of the values of *T*. We then require discriminants to work on these sets of values: DISCRS•<sub>*T*</sub> ⊂ <u>Contexts</u> × (VALSETS•<sub>*T*</sub> → ℤ). The rest of our synthesis procedure readily extends to these additional specifications.

**Bit-stealing** A more interesting extension is an optimisation known as *bit-stealing* in which address alignment bits are used to store additional integer values. For instance, our RBT example can be represented even more compactly by using aligned pointers and storing the color in the lowest bit. Our framework already support leveraging pointer alignment: the OCaml representation exploits the fact that the lowest bit of pointers is always 0. To bit-steal, we extend pointers appropriately: Ptr<el,a>(z) ↦ $\hat{v}$ is a l-wide pointer to $\hat{v}$ with z in the a lowest-bits. Pattern intersection and solving are easily adapted.

# 7 Related Works

## 7.1 Memory Representation and ADTs

Memory representation in functional polymorphic garbage-collected languages was identified quickly as an important area for performance improvements. Peterson (1989) proposes techniques to avoid tagging, while Leroy (1992); Jones and Launchbury (1991) suggest ways to unbox values. Our work encourages new development in this area, by allowing to combine these works with efficient pattern matching compilation. Leroy (1990) presents a calculus which can mix a uniform polymorphic representation and monomorphic optimised representation, which we could use to make several representations cohabit. Colin et al. (2018) details how to extend our source language to handle recursive types in the presence of unboxing. Many of these works are implemented in some capacity in OCaml and Haskell.

Iannetta et al. (2021); Koparkar et al. (2021) propose drastically different representations for Algebraic Data Types, where almost everything is flattened, allowing excellent cache behaviour and parallelism. Our work would augment these approaches with efficient decision tree generation.

## 7.2 Pattern Matching Compilation

Pattern languages for algebraic data types were first introduced by the HOPE language Burstall et al. (1980). Its general form has been adopted mostly as-is in mainstream languages with rich static typing such as Haskell, OCaml, F#, Scala or Rust, but also more recently in more general languages such as Python and soon Java. This diversity of host languages, with their very varied compilation techniques and memory representations, make our framework all the more relevant.

We focused on the core of pattern matching language, with some minor extensions like disjunctive patterns. Other extensions include ranges, guards, matching of polymorphic variants Garrigue (1998), and exception patterns (in recent OCaml versions). These are orthogonal to our work.

As for pattern-matching compilation, many works exists since the first introduction of pattern matrices in the context of the LML language Augustsson (1985). Fessant and Maranget (2001) first proposed optimisation for backtracking automata, introducing the “row and column” approach to split the pattern matrix. Their technique is currently used in OCaml. This approach was later refined by Maranget (2008) to produce good decision trees, which we base our work on. It delivers excellent performance, while being reasonable to compute in practice. Most approaches to improve the current state-of-art algorithms rely on heuristics for the choice of column to split. A study of heuristics is done in Scott and Ramsey (2000). Both conclude that the choice of heuristic only has minor performance consequences in most cases, but can matter for very particular matches. We believe the choice of memory representation has a much bigger impact on performance.
# 8 Conclusion

We have presented a specification and synthesis framework for *composable* memory representation, suitable for Algebraic Data Types implementation and compilation. Our framework not only synthesise optimising compilation procedure, but also checks the validity of the provided specification. As a case study, we used our method to recover a complete description for the OCaml representation and associated pattern-matching compilation. To our knowledge, this is the first generic specification of memory representation linked with Algebraic Data Types compilation purpose. We have also implemented our technique in a prototype tool called *ribbit* and shown its output on concrete examples.

Our technique paves the way towards the formalisation and description of new optimisation techniques for memory representation. In recent versions, Rust has been introducing more and more complex memory representation optimisations, which are so far unspecified and could benefit from our synthesis framework. Furthermore, we believe there is a trove of optimisations yet to be explored when it comes to the memory representation of Algebraic Data Types. Some promising leads are to apply super-optimisation to individual performance-sensitive data structures, or to allow programmers to specify whether types should be optimised for space, cache behaviour, or even sharing. We hope this work serves as a stepping stone for these further optimisations.
## References

Lennart Augustsson. 1985. Compiling Pattern Matching. In *Functional Programming Languages and Computer Architecture, FPCA 1985, Nancy, France, September 16-19, 1985, Proceedings (Lecture Notes in Computer Science, Vol. 201)*, Jean-Pierre Jouannaud (Ed.). Springer, 368-381. https://doi.org/10.1007/3-540-15975-4_48

Rod M. Burstall, David B. MacQueen, and Donald Sannella. 1980. HOPE: An Experimental Applicative Language. In *Proceedings of the 1980 LISP Conference, Stanford, California, USA, August 25-27, 1980*. ACM, 136-143. https://doi.org/10.1145/800087.802799

Simon Colin, Rodolphe Lepigre, and Gabriel Scherer. 2018. Unboxing Mutually Recursive Type Definitions in OCaml. *arXiv preprint arXiv:1811.02300* (2018).

Fabrice Le Fessant and Luc Maranget. 2001. Optimizing Pattern Matching. In *Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), Firenze (Florence), Italy, September 3-5, 2001*, Benjamin C. Pierce (Ed.). ACM, 26-37. https://doi.org/10.1145/507635.507641

Jacques Garrigue. 1998. Programming with polymorphic variants. In *ML Workshop*, Vol. 13. Baltimore.

Paul Iannetta, Laure Gonnord, and Gabriel Radanne. 2021. Compiling pattern matching to in-place modifications. In *GPCE '21: Concepts and Experiences, Chicago, IL, USA, October 17 - 18, 2021*, Eli Tilevich and Coen De Roover (Eds.). ACM, 123-129. https://doi.org/10.1145/3486609.3487204

Simon L. Peyton Jones and John Launchbury. 1991. Unboxed Values as First Class Citizens in a Non-Strict Functional Language. In *Functional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings (Lecture Notes in Computer Science, Vol. 523)*, John Hughes (Ed.). Springer, 636-666. https://doi.org/10.1007/3540543961_30

Chaitanya Koparkar, Mike Rainey, Michael Vollmer, Milind Kulkarni, and Ryan R. Newton. 2021. Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations. *Proc. ACM Program. Lang. 5*, ICFP, Article 91 (aug 2021), 29 pages. https://doi.org/10.1145/3473596

Dmitry Kosarev, Petr Lozov, and Dmitry Boulytchev. 2020. Relational Synthesis for Pattern Matching. In *Processings of the 18th Programming Languages and Systems Asian Symposium, APLAS 2020, Fukuoka, Japan, 2020 (Lecture Notes in Computer Science, Vol. 12470)*, Bruno C. d. S. Oliveira (Ed.). Springer, 293-310. https://doi.org/10.1007/978-3-030-64437-6_15

Xavier Leroy. 1990. Efficient Data Representation in Polymorphic Languages. In *Programming Language Implementation and Logic Programming, 2nd International Workshop PLILP'90, Linköping, Sweden, August 20-22, 1990, Proceedings (Lecture Notes in Computer Science, Vol. 456)*, Pierre Deransart and Jan Maluszynski (Eds.). Springer, 255-276. https://doi.org/10.1007/BFb0024189

Xavier Leroy. 1992. Unboxed Objects and Polymorphic Typing. In *Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992*, Ravi Sethi (Ed.). ACM Press, 177-188. https://doi.org/10.1145/143165.143205

Luc Maranget. 2008. Compiling pattern matching to good decision trees. In *Proceedings of the ACM Workshop on ML, 2008, Victoria, BC, Canada, September 21, 2008*, Eijiro Sumii (Ed.). ACM, 35-46. https://doi.org/10.1145/1411304.1411311

Yaron Minsky and Anil Madhavapeddy. 2021. *Real World OCaml*. Chapter Memory Representation of Values. https://dev.realworlddocaml.org/runtime-memory-layout.html

John Peterson. 1989. Untagged Data in Tagged Environments: Choosing Optimal Representations at Compile Time. In *Proceedings of the fourth international conference on Functional programming languages and computer architecture, FPCA 1989, London, UK, September 11-13, 1989*, Joseph E. Stoy (Ed.). ACM, 89-99. https://doi.org/10.1145/99370.99377
Kevin Scott and Norman Ramsey. 2000. When do match-compilation heuristics matter. *University of Virginia, Charlottesville, VA* (2000).

Peter Sestoft. 1996. ML pattern match compilation and partial evaluation. In *Partial Evaluation*. Springer, 446–464.

Philip Wadler. 1987. Efficient compilation of pattern-matching. *The implementation of functional programming languages* (1987).
# A Source patterns

In this appendix, we give an *exhaustive* presentation of our source pattern language, including its complete formal semantics. It includes all the extensions described in Section 6. This extends Section 3.1.

We first recall the complete grammar in Fig. 11.

**Dynamic Semantics** Fig. 12 defines the dynamic operational semantics of patterns. $p \triangleright v \rightarrow \sigma$ stands for "p matches value v and binds the variables in $\sigma$". Most of the rules are straightforward, with the following peculiarities:

* The bound value environment returned by the matching is populated by variables, through the VAR rule.

* We enforce that there is no shadowing: variables must be bound only once, as asserted by the side-condition in the CONSTRUCTOR rules.

* Alternatives are left-leaning: we first try to match with the left branch (ALTL rule) before trying the right branch (ALT R rule).

We also define the matching judgement in rule MATCHING: Match $\{p_1 | \dots | p_n\} \triangleright v \rightarrow i, \sigma$ which behaves as the normal judgement, but additionally returns the index of the branch which was matched. In a full language, it would then trigger the evaluation of the body of the branch in question.

**Typing** Fig. 13 defines the typing judgement $\Gamma \vdash p : t \rightarrow \Gamma'$: "pattern p has type t and binds variables whose types are defined in environment $\Gamma'$. Typing follows the semantics closely:

* As before, the bound typing environment $\Gamma'$ is populated by variables through the VAR rule.

* We enforce that there is no shadowing in the TUPLE and CONSTRUCTOR rules.

* Bound environments must be identical in all branches, as enforced by the ALT rule.

# B Memory patterns

Memory patterns are memory value skeletons in which possible values of address alignment bits and word contents are constrained by SMT formulae. They are notably used for structural interpolation, in Section 5.1. In this section, we flesh out their auxiliary operations, notably union, intersection and instanciation.

We first recall their grammar in Fig. 14. $t@h$ denotes the application of $\text{PREREPR}_i^\bullet$ to the subvalue at position $h$. Note the extension of pointer pattern to accommodate for bit-stealing. Other cases closely follow the grammar of memory values: fixed-width words whose contents are specified by an SMT formula $\phi$, fixed-width and fixed-alignment pointers (to another memory pattern) whose address alignment bits are specified by an SMT formula $\phi$, blocks containing a finite number of fields (which are either memory patterns or the wildcard `_)` and disjoint unions of memory patterns. $\phi$ is either $\top$ (always true) or a conjunction of clauses $\bigwedge_i (\text{ops}_i = x_i)$ where each $x_i$ is either a concrete integer value or a subterm symbol and each `ops_i` is a sequence of operations applied to the word contents.

**Union and intersection** Memory patterns are equipped with intersection and union operations.

The intersection of two memory patterns, defined in Fig. 15, is empty if they are incompatible (that is, if they specify different memory structures) or another memory pattern that captures both patterns' structural information and word contents otherwise. Intersection performs width extension: the intersection of two words is a word of the same width as the widest initial word. Also note that $(t@h)$ only intersects with memory patterns that do not constrain memory values more than $\text{PREREPR}_i^\bullet(\top)$ – indeed, $(t@h)$ denotes any memory value that matches $\text{PREREPR}_i^\bullet(\top)$.

The union of two memory patterns, defined in Fig. 16, merges their common memory structures and adds disjoint unions between incompatible structures and different SMT formulae. The resulting memory pattern captures all information that applies to any memory value that matches either of the initial patterns.

**Instantiation** *Memory context instantiation*, defined in Fig. 17, formalizes the substitutions in memory patterns. $\hat{h}[\hat{p}]$ is a memory pattern whose structure is that of the memory context $\hat{h}$, where the holes has been replaced by $\hat{p}$ enhanced with the inner word operations.
# C Decision tree generation algorithm for INSPECTANDSPLIT•

In Section 5.3, we give a definition of INSPECTANDSPLIT• using a recursive algorithm to build decision trees. This definition uses the concept of shallowest context, without defining it. In this appendix, we flesh out this definition and formalize and prove the algorithm to build decision trees.

## C.1 Memory context relations

We first define a partial prefix order ≺ on memory contexts in Fig. 18. Intuitively, if $\hat{h} \prec \hat{h}'$, then any memory value that is compatible with $\hat{h}'$ is also compatible with $\hat{h}$. Accordingly, we assert that any transformation on words is a prefix of pointer dereferencing, as the former is compatible with any word or pointer of appropriate width whereas the latter only applies to pointers.

Two memory contexts may be “compatible” in that they both apply to at least one common memory value, without one being a prefix of the other. We formalise this relation in Fig. 19.

We also define a “semi-ordered compatibility” relation × from which we derive a notion of minimum memory context:

$$ \hat{h} \times \hat{h}' \iff \hat{h} = \hat{h}' \lor \hat{h} \prec \hat{h}' \lor \hat{h} \succ \hat{h}' \qquad \min \hat{H} = \{ \hat{h} \in \hat{H} \mid \forall \hat{h}' \in \hat{H}, \hat{h} \times \hat{h}' \} $$

Finally, the following results are needed to prove the existence of at least one minimal relevant discriminant:

**Lemma 1.** Let $\hat{H}$ a non-empty, finite set of memory contexts and $\hat{P}$ a set of memory patterns instantiating all contexts of $\hat{H}$ (i.e., $\forall \hat{h} \in \hat{H}, \exists \hat{p} \in \hat{P}, \exists \hat{p}', \hat{p} = \hat{h}[\hat{p}']$). Then we have

$$ \bigcap_{\hat{p} \in \hat{P}} \hat{p} \neq \emptyset \Rightarrow \min \hat{H} \neq \emptyset $$

*Proof.* We first show that for any memory contexts $\hat{h}$ and $\hat{h}'$ and any memory patterns $\hat{p}$ and $\hat{p}'$ such that $\hat{h}[\hat{p}] \cap \hat{h}'[\hat{p}'] \neq \emptyset$, we have $\hat{h} \times \hat{h}'$ or $\hat{h}' \times \hat{h}$. This result is immediate by induction on pattern intersection rules.

Therefore, for all $\hat{h}, \hat{h}' \in \hat{H}$, we have $\hat{h} \times \hat{h}'$ or $\hat{h}' \times \hat{h}$. Since $\hat{H}$ is a finite ordered set, there exists at least one $\hat{h} \in \hat{H}$ such that $\forall \hat{h}' \in \hat{H}, \hat{h}' \prec \hat{h}$, that is $\forall \hat{h}' \in \hat{H}, \hat{h}' \times \hat{h}$, which proves the existence of at least one minimal memory context of $\hat{H}$. ◇

**Lemma 2.** Let $\hat{h}_0, \hat{h}_1, \hat{h}_2$ and $\hat{p}, \hat{p}'$ such that $\hat{h}_0 \times \hat{h}_1$ and $\hat{h}_1[\hat{p}] \cap \hat{h}_2[\hat{p}'] \neq \emptyset$. Then we have $\hat{h}_0 \times \hat{h}_2$.

*Proof.* By induction on memory pattern intersection. ◇

<figure><img src="image_11.png" /></figure>

<figure><img src="image_12.png" /></figure>

## C.2 Decision tree generation algorithm

Recall the definition of INSPECTANDSPLIT•(branch) where t is a sum type and branch a function from t constructors to decision trees: INSPECTANDSPLIT•(branch) = $T_{Constrs}(t)$, where $T_K$ is defined as follows for a set of constructors $K$:

* if $K$ is empty, it is undefined and we omit any decision tree branch leading to $T_\emptyset$;

* if $K$ contains one constructor $K$, we branch to its associated continuation with $T_{\{K\}} = branch(K)$;

* otherwise, we pick a minimal relevant discriminant $(\hat{h}, split) \in DISCRS_t$ such that

$$ \hat{h} \in \min \left\{ \hat{h} \mid \begin{array}{l} (\hat{h}, split) \in DISCRS_t \\ \exists K, K' \in K \cap split, split(K) \neq split(K') \end{array} \right\} $$

Let $e$ the target expression returning the value located at $\hat{h}_0$ (built similarly to UNWRAP•). We build the following switch node:

$$ T_K = \text{switch}(e) \left\{ c \mapsto T_{K(c)} \mid \begin{array}{l} c \in \mathbb{Z} \cup \{\top\} \\ K_c \neq \emptyset \end{array} \right\} $$

with $K_z = \{K \in K \mid (K, z) \in split \lor K \notin split\}$ for $z \in \mathbb{Z}$ and $K_\top = \{K \in K \mid K \notin split\}$.
The correctness of this algorithm relies on the two following results.

**Lemma 3** (Strictly decreasing constructor set). Let $\mathcal{K} \subseteq \text{Constrs}(t)$ with $|\mathcal{K}| > 1$. For any source value $v$ whose head constructor $K$ is in $\mathcal{K}$, the execution of $\mathcal{T}_{\mathcal{K}}$ on $\text{REPR}_{t}^{\bullet}(v)$ branches to a recursively defined decision tree $\mathcal{T}_{\mathcal{K}}$ with $K \in \mathcal{K}' \subseteq \mathcal{K}$.

*Proof.* Let $(\hat{h}, split)$ the minimal relevant discriminant picked for this step. Let $v$ a source value whose head constructor $K$ is in $\mathcal{K}$. Let us first remark that in any case, the execution of $\mathcal{T}_{\mathcal{K}}$ on $\text{REPR}_{t}^{\bullet}(v)$ branches to $\mathcal{T}_{\mathcal{K}}(c)$ for some $c \in \mathbb{Z} \cup \{\top\}$.

We first show that each such set $\mathcal{K}(c)$ is a strict subset of $\mathcal{K}$. By definition of $(\hat{h}, split)$, there are at least two distinct constructors $K$ and $K'$ in $\mathcal{K} \cap split$ such that $split(K) \neq split(K')$. It follows that at least one of these constructors is absent from each $\mathcal{K}(c)$ for $c \in \mathbb{Z} \cup \{\top\}$, hence $\mathcal{K}(c) \subseteq \mathcal{K}$.

We now show that we always have $K \in \mathcal{K}(c)$. This is immediate if $K \notin split$. Otherwise, we have $K \in split$ and we show that the switch node branches to $\mathcal{T}_{\mathcal{K}(split(K))}$: upon evaluation on the input $\text{REPR}_{t}^{\bullet}(v)$, the switch expression $e$ yields the memory value located at $\hat{h}$. By construction, $\text{REPR}_{t}^{\bullet}$ is such that this memory value is a word whose contents are $split(K)$. Indeed, for all $K \in split$, $\text{PREREPR}_{t}^{\bullet}(K)$ was built from an intersection of memory patterns including $\hat{p} = \hat{h}'$ [$\text{Word}_{\ell}(\text{ops} = split(K))$] where $\hat{h}'[\text{ops}_{\ell}] = \hat{h}$ ($\ell$ and $\ell'$ are irrelevant here). This implies that the memory value located at $\hat{h}'$ in $\text{REPR}_{t}^{\bullet}(v)$ exists and is a word whose contents $\blacksquare$ are such that $\text{ops} = split(K)$, that is, the memory value located at $\hat{h}$ in $\text{REPR}_{t}^{\bullet}(v)$ exists and is a word whose contents are equal to $split(K)$. $\diamond$

**Lemma 4** (Existence of at least one minimal relevant discriminant). Assume that the representation is valid, that is, $\text{REPR}_{t}^{\bullet}(K)$ exists for each constructor $K$ of $t$. Then for all $\mathcal{K} \subseteq \text{Constrs}(t)$ such that $|\mathcal{K}| > 1$, we have

$$ \min \left\{ \hat{h} \mid \begin{array}{l} (\hat{h}, split) \in \text{DISCRS}_{t}^{\bullet} \\ \exists K, K' \in \mathcal{K} \cap split, split(K) \neq split(K') \end{array} \right\} \neq \emptyset $$

*Proof.* According to the distinguishability condition on $\text{DISCRS}_{t}^{\bullet}$, there exists a discriminant $(\hat{h}, split) \in \text{DISCRS}_{t}^{\bullet}$ such that $K, K' \in split$ and $split(K) \neq split(K')$ for any constructor $K' \neq K$, therefore $\hat{H}$ is non-empty.

For any constructor $K$ of type $t$, let

$$ \hat{H}_{K} = \hat{H} \cap \left\{ \hat{h} \mid \begin{array}{l} (\hat{h}, split) \in \text{DISCRS}_{t}^{\bullet} \\ K_i \in split \end{array} \right\} $$

Recall the definition of the distinguishability pattern of any constructor $K$. Owing to representation validity, we have

$$ \hat{p}_{t}^{d}(K) = \bigcap_{(\hat{h}_{i}, \ell_{i}, \text{ops}_{i}, z_{i}) \in \mathcal{C}} \hat{h}_{i}[\text{Word}_{\ell_{i}}(\text{ops}_{i} = z_{i})] \neq \emptyset $$

where

$$ C = \left\{ \begin{array}{l} (\hat{h}, \ell, \text{ops}, z) \text{ where} \\ (\hat{h}', split) \in \text{DISCRS}_{t}^{\bullet} \\ (K \mapsto z) \in split \\ \hat{h}[\text{ops}_{\ell}] = \hat{h}' \\ \ell = (\text{if } (\ell' \text{ is } *) \text{ then } \max_{(K' \mapsto z') \in split} \text{width}(z) \text{ else } \ell') \end{array} \right\} $$

Notice that for any relevant discriminant $(\hat{h}, split) \in \text{DISCRS}_{t}^{\bullet}$ such that $K \in split$, there exists $(\hat{h}_{i}, \ell_{i}, \text{ops}_{i}, z_{i}) \in$
C such that $\hat{h} = \hat{h}_i[\underline{\text{ops}_{i,j}^{\ell'_i}}]$; we can write

$$ 
\begin{aligned}
& \hat{h}_i[\text{Word}_{\ell_i}(\text{ops}_i = z_i)] \\
& = \hat{h}_i[\underline{\text{ops}_{i,j}^{\ell'_i}}[\text{Word}_{\ell_i}(\blacksquare = z_i)]] \\
& = (\hat{h}_i[\underline{\text{ops}_{i,j}^{\ell'_i}}]) [\text{Word}_{\ell_i}(\blacksquare = z_i)] \\
& = \hat{h}[\text{Word}_{\ell_i}(\blacksquare = z_i)]
\end{aligned}
$$

That is, each considered memory context is instantiated once in this non-empty pattern intersection. We can thus apply Lemma 1 to show that for all $K \in \mathcal{K}$, $\min \hat{H}_K \neq \emptyset$.

We must now prove that $\min \hat{H} = \min \{\min \hat{H}_K\}_{K \in \mathcal{K}}$ is not empty. Let $K, K' \in \mathcal{K}$ such that $K \neq K'$.

Using the same distinguishability condition argument as before, we have $\hat{H}_K \cap \hat{H}_{K'} \neq \emptyset$ and apply Lemma 2 on both constructors' distinguishability patterns to show that any minimal context for either constructor is compatible with all minimal contexts for the other constructor, and thus $\min (\min \hat{H}_K \cup \min \hat{H}_{K'}) \neq \emptyset$. $\diamond$

Using these two results, we show that $\text{INSPECTANDSPLIT}_i^\bullet$ descends through switch nodes that successively restrict the set of potential constructors, ending with the decision tree associated with the specific identified constructor.

We can thus assert the correctness of our pattern matching compilation scheme:

**Theorem 2.** Let $\Gamma$ a type environment; let $t \in \Gamma$ a type. Let $m$ a matching such that $\Gamma \vdash m : t \to \Gamma'$ and $\mathcal{T} = \text{COMPILE}_t(m)$. Then for any value $v$ of type $t$ such that $m \triangleright v \to i, \sigma$, the evaluation of $\mathcal{T}$ on $\text{REPR}_t^\bullet(v)$ succeeds with $i, \{x \mapsto \text{REPR}_{\Gamma(x)}\sigma(x)\}$.

# D Full example: OCaml representation

Recall the type environment from our running example:

$$ 
\begin{aligned}
\Gamma = & \{ t \mapsto \text{None} + \text{Some}(t_{\text{ABC}}); \\
& t_{\text{ABC}} \mapsto A + B + C(t_{\text{int}}); \\
& t_{\text{int}} \mapsto u32 \}
\end{aligned}
$$

In this section, we detail the complete representation synthesis pipeline and pattern matching compilation for the OCaml representation, with all extensions enabled. (Note that the bit-stealing extension is not actually used in this representation, which is why all addresses' alignment bits are set to 0.)

## D.1 Input specification

## D.2 Primitive type $t_{\text{int}}$

In OCaml, all integer values follow the same memory layout. Let $S = [0; 2^{32} - 1]$ the set of $u32$ values. We encode any integer value $n \in S$ on 64 bits, then transform it through a one-bit left shift and an increment to set its pointer flag (lowest bit) to 1. As $S$ is the only defined value set and no other representation constraints apply, no discriminant is needed for $t_{\text{int}}$. We thus define the following ingredients:

$$ \text{VALSETS}_{t_{\text{int}}}^{\bullet} = \{S\} \qquad \text{DISCRS}_{t_{\text{int}}}^{\bullet} = \emptyset \qquad \text{POSITION}_{t_{\text{int}}}^{\bullet}(S(\square)) = \underline{(\blacksquare - 1)/2}[0, 31]_{64} $$

## D.3 Sum types $t_{\text{ABC}}$ and $t$

Sum types ingredients are similar across individual types. The main distinction done is between unit and non-unit constructors, which are represented by 64-bit-wide words and 64-bit-wide pointers to blocks, respectively.
We define the following ingredients for $t_{ABC}$:

$$ \begin{array}{l} \text{POSITION}_{t_{ABC}}^{\bullet}(C(\square)) = \text{Ptr}_{64,3} \{\llbracket - , \llbracket \bullet, \ldots \rrbracket \} \\ \text{DISCRS}_{t_{ABC}}^{\bullet} = \left\{ \begin{array}{l} D_{AB,C} = \left( \frac{\llbracket \bullet, 0 \rrbracket_{*}}{C \mapsto 0} , \left\{ \begin{array}{l} A \mapsto 1 \\ B \mapsto 1 \end{array} \right\} \right), \\ D_{A,B} = (\llbracket \bullet_{64}, \{A \mapsto 1 \ B \mapsto 3\} \rrbracket, \\ D_{C} = (\text{Ptr}_{64,3} \{\llbracket \bullet_{64}, \ldots \rrbracket, \{C \mapsto 2\} \}) \end{array} \right\} \end{array} $$

We define the following ingredients for $t$:

$$ \begin{array}{l} \text{POSITION}_{t}^{\bullet}(\text{Some}(\square)) = \text{Ptr}_{64,3} \{\llbracket - , \llbracket \bullet, \ldots \rrbracket \} \\ \text{DISCRS}_{t}^{\bullet} = \left\{ \begin{array}{l} D_{\text{None},\text{Some}} = \left( \frac{\llbracket \bullet, 0 \rrbracket_{*}}{\text{Some} \mapsto 0} , \left\{ \begin{array}{l} \text{None} \mapsto 1 \\ \text{Some} \mapsto 0 \end{array} \right\} \right), \\ D_{\text{None}} = (\llbracket \bullet_{64}, \{\text{None} \mapsto 1\} \rrbracket, \\ D_{\text{Some}} = (\text{Ptr}_{64,3} \{\llbracket \bullet_{64}, \ldots \rrbracket, \{\text{Some} \mapsto 1\} \}) \end{array} \right\} \end{array} $$

## D.4 Structural interpolation

**Example 11** (Building the unsolved representation of a primitive type: $t_{int}$). $t_{int}$ only has one value set $S$. No discriminant applies: by convention, we define $\hat{p}_{t_{int}}^d(S) = -$. We derive its only composability pattern from $POSITION_{t_{int}}^\bullet(S(\square))$ to build its unsolved representation:

$$ \begin{array}{l} \text{PREREPR}_{t_{\text{int}}}^{\bullet}(\top) = \text{PREREPR}_{t_{\text{int}}}^{\bullet}(S) \\ \qquad = \hat{p}_{t_{\text{int}}}^{c}(S) = \text{Word}_{64} (((\bullet - 1)/2)[0, 31] = x_{\square}) \\ \text{REPRTY}_{t_{\text{int}}}^{\bullet}(\top) = \text{REPRTY}_{t_{\text{int}}}^{\bullet}(S) = \text{Word}_{64} \end{array} $$

♦

**Example 12** (Composing word representations: $t_{ABC}$). We first compute the unsolved representations of both unit constructors $A$ and $B$, which solely consists of their distinguishability pattern. Two discriminants apply: $D_{A,B}$ and $D_{AB,C}$. We decompose and recombine $D_{AB,C}$ into the memory pattern $\text{Word}_1(\llbracket 0, 0 \rrbracket = 1)$ and get

$$ \begin{align*} \text{PREREPR}_{t_{ABC}}^{\bullet}(A) &= \hat{p}_{t_{ABC}}^{d}(A) \\ &= \text{Word}_{64}(\bullet = 1) \cap \text{Word}_{1}(\llbracket 0, 0 \rrbracket = 1) \\ &= \text{Word}_{64}(\bullet = 1 \land \llbracket 0, 0 \rrbracket = 1) \\ \text{PREREPR}_{t_{ABC}}^{\bullet}(B) &= \hat{p}_{t_{ABC}}^{d}(B) \\ &= \text{Word}_{64}(\bullet = 3) \cap \text{Word}_{1}(\llbracket 0, 0 \rrbracket = 1) \\ &= \text{Word}_{64}(\bullet = 3 \land \llbracket 0, 0 \rrbracket = 1) \end{align*} $$

We therefore have $\text{REPRTY}_{t_{ABC}}^\bullet(A) = \text{REPRTY}_{t_{ABC}}^\bullet(B) = \text{Word}_{64}$.

For the non-unit constructor $C$, we need both a composability and a distinguishability memory pattern. Two discriminants apply: $D_C$ and $D_{AB,C}$, hence

$$ \begin{align*} \hat{p}_{t_{ABC}}^{d}(C) &= \text{Ptr}_{64,3}(\top) \rightarrow \{\llbracket \text{Word}_{64}(\bullet = 2), \ldots \rrbracket \} \\ & \phantom{=} \cap \text{Word}_{1}(\llbracket 0, 0 \rrbracket = 0) \\ &= \text{Ptr}_{64,3}(\top \land \llbracket 0, 0 \rrbracket = 0) \rightarrow \{\llbracket \text{Word}_{64}(\bullet = 2), \ldots \rrbracket \} \end{align*} $$

We derive the composability pattern from $POSITION_{t_{ABC}}^\bullet(C(\square))$ and $\text{REPRTY}_{t_{int}}^\bullet(\top) = \text{REPRTY}_{t_{int}}^\bullet(S) = \text{Word}_{64}$:

$$ \hat{p}_{t_{ABC}}^{c}(C(\square)) = \text{Ptr}_{64,3}(\top) \rightarrow \{\llbracket - , \text{Word}_{64}(\bullet = x_{C}(\square)), \ldots \rrbracket \} $$
Note that the representation of the subvalue “under C” has been integrated as an SMT variable $x_C(\square)$. Hence

$$ \begin{aligned} \text{PREREPR}_{t_{\text{ABC}}}(C) &= \hat{p}_{t_{\text{ABC}}}^{d}(C) \cap \hat{p}_{t_{\text{ABC}}}^{c}(C(\square)) \\ &= \text{Ptr}_{64,3}(\top \wedge \Box[0,0] = 0 \wedge \top) \\ &\rightarrow \{\{\text{Word}_{64} (\Box = 2), \text{Word}_{64} (\Box = x_C(\square))\}\} \end{aligned} $$

and $\text{REPRTY}_{t_{\text{ABC}}}(C) = \text{Ptr}_{64,3} \{\{\text{Word}_{64}, \text{Word}_{64}\}\}$.

We finally compute the union of these partial representations to get the generic unsolved representation and its memory type:

$$ \begin{aligned} \text{PREREPR}_{t_{\text{ABC}}}(\top) &= \text{PREREPR}_{t_{\text{ABC}}}(A) \cup \text{PREREPR}_{t_{\text{ABC}}}(B) \cup \text{PREREPR}_{t_{\text{ABC}}}(C) \\ &= \text{PREREPR}_{t_{\text{ABC}}}(A) \cup \text{PREREPR}_{t_{\text{ABC}}}(B) \cup \text{PREREPR}_{t_{\text{ABC}}}(C) \\ \text{REPRTY}_{t_{\text{ABC}}}(\top) &= \text{REPRTY}_{t_{\text{ABC}}}(A) \cup \text{REPRTY}_{t_{\text{ABC}}}(B) \cup \text{REPRTY}_{t_{\text{ABC}}}(C) \\ &= \text{Word}_{64} \cup \text{Word}_{64} \cup \text{Ptr}_{64,3} \{\{\text{Word}_{64}, \text{Word}_{64}\}\} \\ &= \text{Word}_{64} \cup \text{Ptr}_{64,3} \{\{\text{Word}_{64}, \text{Word}_{64}\}\} \end{aligned} $$

♦

**Example 13** (Composing non-word representations: $t$). The unsolved representation of the unit constructor *None* is very similar to that of *A* and *B* from the previous example: two discriminants $D_{\text{None}}$ and $D_{\text{None,Some}}$ apply and we get

$$ \begin{aligned} \text{PREREPR}_{t}(\text{None}) &= \hat{p}_{t}^{d}(\text{None}) \\ &= \text{Word}_{64} (\Box = 1) \cap \text{Word}_{1} (\Box[0,0] = 1) \\ &= \text{Word}_{64} (\Box = 1 \wedge \Box[0,0] = 1) \\ \text{REPRTY}_{t}(\text{None}) &= \text{Word}_{64} \end{aligned} $$

The unsolved representation of the non-unit constructor *Some* is the intersection of its only composability pattern and of its distinguishability pattern, involving two discriminants $D_{\text{Some}}$ and $D_{\text{None,Some}}$.

$$ \begin{aligned} \hat{p}_{t}^{d}(\text{Some}) &= \text{Ptr}_{64,3}(\top) \rightarrow \{\{\text{Word}_{64} (\Box = 1), \dots\}\} \\ &\cap \text{Word}_{1} (\Box[0,0] = 0) \\ &= \text{Ptr}_{64,3}(\top \wedge \Box[0,0] = 0) \rightarrow \{\{\text{Word}_{64} (\Box = 1), \dots\}\} \end{aligned} $$

Since $\text{REPRTY}_{t_{\text{ABC}}}(\top)$ is not a word type, we integrate the subvalue representation as an application pattern rather than an SMT variable:

$$ \hat{p}_{t}^{c}(\text{Some}(\square)) = \text{Ptr}_{64,3}(\top) \rightarrow \{\{\text{, } t_{\text{ABC}}@\text{Some}(\square), \dots\}\} $$

and we get

$$ \begin{aligned} \text{PREREPR}_{t}^{c}(\text{Some}) &= \hat{p}_{t}^{d}(\text{Some}) \cap \hat{p}_{t}^{c}(\text{Some}(\square)) \\ &= \text{Ptr}_{64,3}(\top \wedge \Box[0,0] = 0) \rightarrow \{\{\text{Word}_{64} (\Box = 1), \dots\}\} \\ &\cap \text{Ptr}_{64,3}(\top) \rightarrow \{\{\text{, } t_{\text{ABC}}@\text{Some}(\square), \dots\}\} \\ &= \text{Ptr}_{64,3}(\top \wedge \Box[0,0] = 0 \wedge \top) \\ &= \rightarrow \{\{\text{Word}_{64} (\Box = 1), t_{\text{ABC}}@\text{Some}(\square)\}\} \\ \text{REPRTY}_{t}^{c}(\text{Some}) &= \text{Ptr}_{64,3} \{\{\text{Word}_{64}, \text{REPRTY}_{t_{\text{ABC}}}(\top)\}\} \end{aligned} $$
And we can finally build the generic unsolved representation and memory type:

$$
\begin{align*}
\text{PREREPR}_t^\bullet(\top) &= \text{PREREPR}_t^\bullet(\text{None}) \cup \text{PREREPR}_t^\bullet(\text{Some}) \\
&= \text{Word}_{64} (\blacksquare = 1 \land \blacksquare[0, 0] = 1) \\
&\sqcup \text{Ptr}_{64,3}(\top \land \blacksquare[0, 0] = 0 \land \top) \\
&\to \{\text{Word}_{64} (\blacksquare = 1), t_{\text{ABC}}@\text{Some}(\square)\} \\
\text{REPRTY}_t^\bullet(\top) &= \text{REPRTY}_t^\bullet(\text{None}) \cup \text{REPRTY}_t^\bullet(\text{Some}) \\
&= \text{Word}_{64} \sqcup \text{Ptr}_{64,3} \{\text{Word}_{64}, \text{REPRTY}_{t_{\text{ABC}}}^\bullet(\top)\}
\end{align*}
$$

♦

## D.5 Representation completion

**Example 14 (Representation completion of a primitive type: $t_{int}$).** We complete the unsolved representation of the only value set of $t_{int}$. $\text{PREREPR}_{t_{int}}^\bullet(S) = \text{Word}_{64}(\phi)$ contains one formula at the position $\blacksquare_*$ that we express as the following atomic SMT problem:

$$
\begin{array}{l}
(\phi) \quad y_{\blacksquare_*} : \{0, 1\}^{32} \rightarrow \{0, 1\}^{64} \\
\qquad \text{such that } \forall x_{\square} : \{0, 1\}^{32}, (y_{\blacksquare_*}(x_{\square}) - 1)/2[0, 31] = x_{\square}
\end{array}
$$

where the variable $x_{\square}$ symbolises the source integer value as a bitvector of width 32. We immediately solve it with the following model: $y_{\blacksquare_*}(x_{\square}) = (2 \times x_{\square} + 1)_{64}$, hence $\text{REPR}_{t_{int}}^\bullet(n) = \text{Word}_{64}(2 \times n + 1)$. ♦

**Example 15 (Representation completion of $t_{ABC}$).** Recall the unsolved representation patterns from the previous section. $\text{PREREPR}_{t_{ABC}}^\bullet(A) = \text{Word}_{64}(\phi)$ contains one formula at the position $\blacksquare_*$ that we express as the following atomic SMT problem:

$$
(\phi) \quad y_{\blacksquare_*} : \{0, 1\}^{64} \text{ such that } y_{\blacksquare_*} = 1 \wedge y_{\blacksquare_*}[0, 0] = 1
$$

which we solve with the model $y_{\blacksquare_*} = (1)_{64}$, which satisfies $\phi$, hence $\text{REPR}_{t_{ABC}}^\bullet(A) = \text{Word}_{64}(1)$.

We carry out the same steps to solve $\text{PREREPR}_{t_{ABC}}^\bullet(B)$: $y_{\blacksquare_*} = 3$ satisfies $y_{\blacksquare_*} = 3 \wedge y_{\blacksquare_*}[0, 0] = 1$ and thus $\text{REPR}_{t_{ABC}}^\bullet(B) = \text{Word}_{64}(3)$.

Solving $\text{PREREPR}_{t_{ABC}}^\bullet(C)$ is slightly more involved: it contains three formulas at positions $\hat{h}_0 = \text{Ptr}_{64,3} \{\blacksquare_*, \dots\}$, $\hat{h}_1 = \text{Ptr}_{64,3} \{\blacksquare_*, \dots\}$ and $\blacksquare_*$, which we express through the following atomic SMT problems:

$$
\begin{align*}
(\phi_0) \quad & y_{\hat{h}_0} \in \{0, 1\}^{64} \text{ such that } y_{\hat{h}_0} = 2 \\
(\phi_1) \quad & y_{\hat{h}_1} \in \{0, 1\}^{64} \rightarrow \{0, 1\}^{64} \\
& \text{such that } \forall x_{C(\square)} : \{0, 1\}^{64}, y_{\hat{h}_1}(x_{C(\square)}) = x_{C(\square)} \\
(\phi) \quad & y_{\blacksquare_*} \in \{0, 1\}^3 \text{ such that } \top \wedge y_{\blacksquare_*}[0, 0] = 0 \wedge \top
\end{align*}
$$

We immediately solve these with the following models:

$$
\begin{align*}
y_{\hat{h}_0} &= (2)_{64} \text{ satisfies } \phi_0 \\
y_{\hat{h}_1}(x_{C(\square)}) &= x_{C(\square)} \text{ satisfies } \phi_1 \\
y_{\blacksquare_*} &= (0)_3 \text{ satisfies } \phi
\end{align*}
$$

and thus get, for any value $v$ of type $t_{int}$:

$$
\text{REPR}_{t_{\text{ABC}}}^{\bullet}(C(v)) = \text{Ptr}_{64,3}(0) \rightarrow \{\text{Word}_{64}(2), \text{Word}_{64}(\text{REPR}_{t_{\text{int}}}^{\bullet}(v))\}
$$

♦
**Example 16** (Representation completion of $t$). Recall the unsolved representation patterns from the previous section. $\text{PREREPR}_t^*(\text{None}) = \text{Word}_{64}(\phi)$ contains one formula at the position $\Box_*$ that we express as the following atomic SMT problem:

$$ (\phi) y_{\Box_*} : \{0, 1\}^{64} \text{ such that } y_{\Box_*} = 1 \wedge y_{\Box_*}[0, 0] = 1 $$

The model $y_{\Box_*} = (1)_{64}$ satisfies $\phi$, hence $\text{REPR}_t^*(\text{None}) = \text{Word}_{64}(1)$.

$\text{PREREPR}_t^*(\text{Some})$ contains three formulas at positions $\hat{h}_0 = \text{Ptr}_{64,3} \{\{\Box_*, \dots, \}}\}$, $\hat{h}_1 = \text{Ptr}_{64,3} \{\{-, \Box_*, \dots, \}}\}$ and $\Box_*$ that we express as the following atomic SMT problems:

$$ (\phi_0) y_{\hat{h}_0} : \{0, 1\}^{64} \text{ such that } y_{\hat{h}_0} = 1 $$

$$ (\phi_1) y_{\hat{h}_1} : \{0, 1\}^{64} \rightarrow \{0, 1\}^{64} \text{ such that } \forall x : \{0, 1\}^{64}, y_{\hat{h}_1}(x) = x $$

$$ y_{\Box_*} : \{0, 1\}^3 \text{ such that } \top $$

which we solve with the following models:

$$ y_{\hat{h}_0} = (1)_{64} \text{ satisfies } \phi_0 $$

$$ y_{\hat{h}_1}(x) = x \text{ satisfies } \phi_1 $$

$$ y_{\Box_*} = (0)_3 \text{ satisfies } \top $$

and we thus have, for any source value $v$ of type $t_{ABC}$:

$$ \begin{aligned} \text{REPR}_t^*(\text{Some}(v)) &= \\ \text{Ptr}_{64,3}(0) &\rightarrow \{\{\text{Word}_{64}(1), \text{Word}_{64}(\text{REPR}_{t_{ABC}}^*(v))\}\} \end{aligned} $$

Notice that $\text{REPR}_{t_{ABC}}^*(v)$ corresponds to $x_{\text{Some}(\Box)}$ in $\text{PREREPR}_t^*(\text{Some})$.

♦

## D.6 Pattern matching primitives

We finally synthesise pattern matching primitives $\text{UNWRAP}^*$ and $\text{INSPECTANDSPLIT}^*$ for each sum type.

### D.6.1 Composability primitives: UNWRAP$^*$

Since the composability ingredients for the only subterm of both sum types $t_{ABC}$ and $t$ are identical, their composability primitives – which are generated by converting a memory context ingredient to a target expression – are also identical.

From the memory context

$$ \text{POSITION}_{t_{ABC}}^*(C(\Box)) = \text{POSITION}_{t}^*(\text{Some}(\Box)) = \text{Ptr}_{64,3} \{\{-, \Box_*, \dots, \}}\} $$

we obtain

$$ \text{UNWRAP}_{t_{ABC}}^*(C(\Box)) = (*\Delta).1 $$

$$ \text{UNWRAP}_{t}^*(\text{Some}(\Box)) = (*\Delta).1 $$

With both types, the evaluation of this expression on the representation of a non-unit source value yields the representation of its subvalue under the constructor, as expected. Indeed, $(* (\text{Ptr}_{64,3}(0) \rightarrow \{\{\hat{v}_0, \hat{v}_1\}\}) \cdot 1)$ evaluates to $\hat{v}_1$.

### D.6.2 Distinguishability primitives: INSPECTANDSPLIT$^*$

The different signatures of $t_{ABC}$ and $t$ result in distinct decision trees to distinguish between constructors. Indeed, $\text{INSPECTANDSPLIT}_{t_{ABC}}^*$ features an extra switch node to distinguish between unit constructors A and B.

**Example 17** ($t_{ABC}$). Let $\text{branch} : \{A, B, C\} \rightarrow \text{Trees}$. The generation of $\text{INSPECTANDSPLIT}_{t_{ABC}}^*(\text{branch})$ begins with its toplevel decision tree $\mathcal{T}_{\{A,B,C\}}$.
The only minimal relevant discriminant for {$A, B, C$} is $D_{AB,C}$, which inspects the pointer flag to distinguish between unit and non-unit constructors. We emit the following switch node, in which recursively defined trees are present:

$$ \mathcal{T}_{\{A,B,C\}} = \text{switch}(\Delta \ \& \ 1) \left\{ \begin{array}{l} 1 \mapsto \mathcal{T}_{\{A,B\}} \\ 0 \mapsto \mathcal{T}_{\{C\}} \\ \top \mapsto \mathcal{T}_{\emptyset} \end{array} \right\} \quad \text{(unreachable)} $$

We now compute $\mathcal{T}_{\{A,B\}}$, whose minimal relevant discriminant is $D_{A,B}$, and $\mathcal{T}_{\{C\}}$:

$$ \mathcal{T}_{\{A,B\}} = \text{switch}(\Delta) \left\{ \begin{array}{l} 1 \mapsto \mathcal{T}_{\{A\}} \\ 3 \mapsto \mathcal{T}_{\{B\}} \\ \top \mapsto F(\emptyset) \end{array} \right\} \quad \text{(unreachable)} \qquad \mathcal{T}_{\{C\}} = \text{branch}(C) $$

Finally, we compute the last subtrees $\mathcal{T}_{\{A\}} = \text{branch}(A)$ and $\mathcal{T}_{\{B\}} = \text{branch}(B)$. Combining all previously defined subtrees yields the full decision tree: $\text{INSPECTANDSPLIT}_{\text{t}_{\text{ABC}}}(\text{branch}) =$

$$ \text{switch}(\Delta \ \& \ 1) \left\{ \begin{array}{l} 1 \mapsto \text{switch}(\Delta) \left\{ \begin{array}{l} 1 \mapsto \text{branch}(A) \\ 3 \mapsto \text{branch}(B) \end{array} \right\} \\ 0 \mapsto \text{branch}(C) \end{array} \right\} $$

♦

**Example 18** (t). Let `branch`: `{None, Some}` → `Trees`. The generation of $\text{INSPECTANDSPLIT}_{\text{t}}^{\bullet}(\text{branch})$ begins with its toplevel decision tree $\mathcal{T}_{\{None, Some\}}$. Its only minimal relevant discriminant is $D_{None, Some}$, which inspects the pointer flag to distinguish between `None` and `Some`. This step is sufficient to fully distinguish all constructors: we have $\mathcal{T}_{None} = \text{branch}(\text{None})$, $\mathcal{T}_{Some} = \text{branch}(\text{Some})$ and obtain the following decision tree: $\text{INSPECTANDSPLIT}_{\text{t}}^{\bullet}(\text{branch}) =$

$$ \text{switch}(\Delta \ \& \ 1) \left\{ \begin{array}{l} 1 \mapsto \text{branch}(\text{None}) \\ 0 \mapsto \text{branch}(\text{Some}) \end{array} \right\} $$

♦

## D.7 Pattern matching compilation

Recall the pattern matching problem from our running example:

$$ m_0 = \text{Match} \left\{ \begin{array}{l} |(p_0) \text{ None} | \text{ Some}(A) \\ |(p_1) \text{ Some}(B) \\ |(p_2) \text{ Some}(C(n)) \end{array} \right\} $$

We can now apply our templated compilation procedure `COMPILE_t` to $m_0$ by instantiating $\text{INSPECTANDSPLIT}^{\bullet}$ and $\text{UNWRAP}^{\bullet}$ calls.

**Example 19** (OCaml pattern matching compilation of our running example). Our compilation procedure generates the following parametrised decision tree for the input $m_0$:

$$ \begin{array}{l} \text{COMPILE}_t(m_0) = \text{INSPECTANDSPLIT}_t^{\bullet} \\ \quad \left( \begin{array}{l} \text{None} \mapsto \text{success}(0) \\ \text{Some} \mapsto \text{INSPECTANDSPLIT}_{\text{t}_{\text{ABC}}}^{\bullet} \\ \quad \left( \begin{array}{l} A \mapsto \text{success}(0) \\ B \mapsto \text{success}(1) \\ C \mapsto \text{success}(2, \{n \mapsto \text{UNWRAP}_{\text{t}_{\text{ABC}}}^{\bullet}(C(\Box))\}) \end{array} \right) \\ \quad [\Delta/\text{UNWRAP}_{\text{t}}^{\bullet}(\text{Some}(\Box))] \end{array} \right) $$

We first determine whether we are dealing with `None` or a `Some` value; in the latter case, we determine whether the value “under Some” is a unit constructor or `C`, in which case we bind the representation of
the integer value “under C” to the symbol $n$. We can now replace the symbolic calls to pattern matching primitives with their expressions to obtain the final decision tree:

$$ \text{COMPILE}_t(m_0) = \text{switch}(\Delta \& 1) $$

$$ \left\{ \begin{array}{l} 1 \mapsto \text{success}(0) \\ 0 \mapsto \text{switch}(((*\Delta).1) \& 1) \\ \quad \left\{ \begin{array}{l} 1 \mapsto \text{switch}((*\Delta).1) \left\{ \begin{array}{l} 1 \mapsto \text{success}(0) \\ 3 \mapsto \text{success}(1) \end{array} \right\} \\ 0 \mapsto \text{success}(2, \{n \mapsto ((*\Delta).1).1\}) \end{array} \right\} \end{array} \right\} $$

Notice how `UNWRAP<sub>t</sub>(Some(□))` calls are composed into the `INSPECTANDSPLIT<sub>t<sub>ABC</sub></sub>` decision tree so as to inspect the representation of the `subvalue` “under Some”, which is `(*Δ).1`. ♦
## Patterns

<table><tr><td>p ::=</td><td>Wildcard</td></tr><tr><td>| x</td><td>Variable</td></tr><tr><td>| (p | p')</td><td>Disjunction</td></tr><tr><td>| z ∈ Z</td><td>Integer constant pattern</td></tr><tr><td>| &amp;p</td><td>Reference pattern</td></tr><tr><td>| &lt;p<sub>0</sub>, ..., p<sub>n-1</sub>&gt;</td><td>Product pattern</td></tr><tr><td>| K(p<sub>0</sub>, ..., p<sub>n-1</sub>)</td><td>Constructor pattern</td></tr></table>

## Matching

$$m ::= \text{Match } \{p_0 | \cdots | p_{n-1}\} \quad (\text{Matching})$$

## Types

$$ \begin{array}{l} t ::= T \text{ (e.g., i32, u16)} \hfill (\text{Primitive type}) \\ | \& t \hfill (\text{Reference type}) \\ | \prod_n t_i \hfill (\text{Product type}) \\ | \sum_n K_i(t_{i,0}, \ldots, t_{i,n_i-1}) \hfill (\text{Sum type}) \\ \Gamma ::= \left\{ \begin{array}{l} x_0 : t_0; \ldots; x_{n-1} : t_{n-1}; \\ t_0 \mapsto \tau_0; \ldots; t_{n'-1} \mapsto \tau_{n'-1} \end{array} \right\} \hfill (\text{Type environment}) \end{array} $$

## Values

$$ \begin{array}{l} v ::= z \in \mathbb{Z} \hfill (\text{Integer constant}) \\ | \& v \hfill (\text{Reference}) \\ | \langle v_0, \ldots, v_{n-1} \rangle \hfill (\text{Product}) \\ | K(v_0, \ldots, v_{n-1}) \hfill (\text{Constructor}) \\ \sigma ::= \{x_0 \mapsto v_0; \ldots; x_{n-1} \mapsto v_{n-1}\} \hfill (\text{Value env.}) \end{array} $$

<figure><img src="image_13.png" /><figcaption>Figure 12: Semantics of patterns: $p \triangleright v \to \sigma$</figcaption></figure>
<figure><img src="image_14.png" /><figcaption>Figure 13: Typing of patterns: $\vdash p : t \rightarrow \Gamma$</figcaption></figure>

$$
\begin{align*}
\phi ::= & \top \mid (\text{ops} = x_h) \mid (\text{ops} = z) \mid \phi \wedge \phi \\
\hat{p} ::= & t@h \mid \text{Word}_\ell(\phi) \mid \text{Ptr}_{\ell,a}(\phi) \rightarrow \hat{p} \mid \{\overline{\hat{p}^?}\} \mid \Box \hat{p}
\end{align*}
$$

<caption>Figure 14: Memory patterns values and types</caption>

$$
\begin{align*}
(t@h) \cap (t@h) = t@h
& \frac{\text{PREREPR}_t^\bullet(\top) \cap \hat{p} = \text{PREREPR}_t^\bullet(\top)}{(t@h) \cap \hat{p} = t@h} & \frac{\ell \le \ell'}{\text{Word}_\ell(\phi) \cap \text{Word}_{\ell'}(\phi') = \text{Word}_{\ell'}(\phi \wedge \phi')} \\
& \frac{\ell' \le a}{\text{Ptr}_{\ell,a}(\phi) \rightarrow \hat{p} \cap \text{Word}_{\ell'}(\phi') = \text{Ptr}_{\ell,a}(\phi \wedge \phi') \rightarrow \hat{p}} & \frac{\hat{p} \cap \hat{p}' = \hat{p}''}{\text{Ptr}_{\ell,a}(\phi) \rightarrow \hat{p} \cap \text{Ptr}_{\ell,a}(\phi') \rightarrow \hat{p}' = \text{Ptr}_{\ell,a}(\phi \wedge \phi') \rightarrow \hat{p}''} \\
& \frac{n \le n' \quad \forall i < n, \hat{p}_i \cap \hat{p}'_i = \hat{p}''_i}{\{\overline{\hat{p}_i}^n, \dots\} \cap \{\overline{\hat{p}'_i}^{n'}, \dots\} = \{\overline{\hat{p}''_i}, \overline{\hat{p}''_{n+i}}^{n'-n}\}} & \frac{\forall i, \hat{p} \cap \hat{p}_i = \hat{p}'_i}{\hat{p} \cap \Box_n \hat{p}_i = \Box_n \hat{p}'_i}
\end{align*}
$$

<caption>Figure 15: Intersection</caption>

$$
\begin{align*}
(t@h) \cup (t@h) = t@h
& \frac{\text{PREREPR}_t^\bullet(\top) \cup \hat{p} = \text{PREREPR}_t^\bullet(\top)}{(t@h) \cup \hat{p} = t@h} & \text{Word}_\ell(\phi) \cup \text{Word}_\ell(\phi) = \text{Word}_\ell(\phi) \\
& \frac{\hat{p} \cup \hat{p}' = \hat{p}''}{\text{Ptr}_{\ell,a}\hat{p}(\phi) \cup \text{Ptr}_{\ell,a}\hat{p}(\phi) = \text{Ptr}_{\ell,a}\hat{p}''(\phi)} \\
& \frac{\hat{p}_{i_0} \cup \hat{p}'_{i_0} = \hat{p}''_{i_0}}{\{\overline{\hat{p}_i}^n, \dots\} \cup \{\overline{\hat{p}^{i_0}}_{i_0}, \overline{\hat{p}^{n-i_0-1}}_{i_0}, \dots\} = \{\overline{\hat{p}_i}^{i_0}, \hat{p}'_{i_0}, \overline{\hat{p}^{n-i_0-1}}_{i_0}, \dots\}} & \frac{\forall i, \hat{p} \cup \hat{p}_i = \hat{p}'_i}{\hat{p} \cup \Box_n \hat{p}_i = \Box_n \hat{p}'_i} \\
& \frac{\text{no other rule applies}}{\hat{p} \cup \hat{p}' = \hat{p} \sqcup \hat{p}'}
\end{align*}
$$

<caption>Figure 16: Union</caption>
Inria

RESEARCH CENTRE
GRENOBLE - RHÔNE-ALPES

Inovallée

655 avenue de l'Europe Montbonnot

38334 Saint Ismier Cedex

Publisher

Inria

Domaine de Voluceau - Rocquencourt

BP 105 - 78153 Le Chesnay Cedex

inria.fr

ISSN 0249-6399