diff --git a/Cargo.lock b/Cargo.lock
index 9aeca9db..a385c4ed 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -65,6 +65,12 @@ dependencies = [
  "windows-sys",
 ]
 
+[[package]]
+name = "arrayvec"
+version = "0.7.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "96d30a06541fbafbc7f82ed10c06164cfbd2c401138f6addd8404629c4b16711"
+
 [[package]]
 name = "autocfg"
 version = "1.1.0"
@@ -410,6 +416,7 @@ checksum = "379dada1584ad501b383485dd706b8afb7a70fcbc7f4da7d780638a5a6124a60"
 name = "hvm-core"
 version = "0.2.19"
 dependencies = [
+ "arrayvec",
  "clap",
  "criterion",
  "insta",
diff --git a/Cargo.toml b/Cargo.toml
index 529cb961..231c7982 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -23,6 +23,7 @@ panic = "abort"
 debug = "full"
 
 [dependencies]
+arrayvec = "0.7.4"
 clap = { version = "4.5.1", features = ["derive"] }
 nohash-hasher = { version = "0.2.0" }
 stacker = "0.1.15"
diff --git a/benches/benches.rs b/benches/benches.rs
index 3b902c65..7b3e722a 100644
--- a/benches/benches.rs
+++ b/benches/benches.rs
@@ -90,9 +90,21 @@ fn interact_benchmark(c: &mut Criterion) {
 
   let cases = [
     ("era-era", (Era, Era)),
-    ("era-con", (Era, Ctr { lab: 0, lft: Era.into(), rgt: Era.into() })),
-    ("con-con", ((Ctr { lab: 0, lft: Era.into(), rgt: Era.into() }), Ctr { lab: 0, lft: Era.into(), rgt: Era.into() })),
-    ("con-dup", ((Ctr { lab: 0, lft: Era.into(), rgt: Era.into() }), Ctr { lab: 2, lft: Era.into(), rgt: Era.into() })),
+    ("era-con", (Era, Ctr { lab: 0, ports: [Era.into(), Era.into()].into() })),
+    (
+      "con-con",
+      ((Ctr { lab: 0, ports: [Era.into(), Era.into()].into() }, Ctr {
+        lab: 0,
+        ports: [Era.into(), Era.into()].into(),
+      })),
+    ),
+    (
+      "con-dup",
+      ((Ctr { lab: 0, ports: [Era.into(), Era.into()].into() }, Ctr {
+        lab: 2,
+        ports: [Era.into(), Era.into()].into(),
+      })),
+    ),
   ];
 
   for (name, redex) in cases {
diff --git a/cspell.json b/cspell.json
index e6e76aba..18d82ff2 100644
--- a/cspell.json
+++ b/cspell.json
@@ -4,10 +4,12 @@
   "words": [
     "anni",
     "annihilations",
+    "arrayvec",
     "backlinks",
     "backoffs",
     "combinators",
     "condvar",
+    "ctrs",
     "dereferencable",
     "dref",
     "dups",
@@ -47,6 +49,7 @@
     "sigabrt",
     "skippable",
     "struct",
+    "succ",
     "supercombinators",
     "targ",
     "tids",
diff --git a/examples/church_encoding/church.hvmc b/examples/church_encoding/church.hvmc
index 4d264fd9..3d0985da 100644
--- a/examples/church_encoding/church.hvmc
+++ b/examples/church_encoding/church.hvmc
@@ -1,8 +1,8 @@
 @S = ((a (b c)) ({3 (c d) a} (b d)))
 @Z = (* (a a))
-@add = ((a (b c)) ((d (e b)) ({11 a d} (e c))))
+@add = ((a (b c)) ((d (e b)) ({9 a d} (e c))))
 @c2 = ({5 (a b) (c a)} (c b))
-@c3 = ({7 (a b) {9 (c a) (d c)}} (d b))
+@c3 = ({7 (a b) {7 (c a) (d c)}} (d b))
 @c4 = a
 & @S ~ (b a)
 & @S ~ (c b)
diff --git a/examples/lambda_calculus/hoas.hvmc b/examples/lambda_calculus/hoas.hvmc
index cf5e2f21..d0e931ab 100644
--- a/examples/lambda_calculus/hoas.hvmc
+++ b/examples/lambda_calculus/hoas.hvmc
@@ -16,14 +16,14 @@
 & @App ~ (b (d f))
 @C3 = a
 & @Lam ~ (@C3$S0 a)
-@C3$S0 = ({5 a {7 b c}} d)
+@C3$S0 = ({5 a {5 b c}} d)
 & @Lam ~ ((e f) d)
 & @App ~ (a (g f))
 & @App ~ (b (h g))
 & @App ~ (c (e h))
 @C4 = a
 & @Lam ~ (@C4$S0 a)
-@C4$S0 = ({9 a {11 b {13 c d}}} e)
+@C4$S0 = ({7 a {7 b {7 c d}}} e)
 & @Lam ~ ((f g) e)
 & @App ~ (a (h g))
 & @App ~ (b (i h))
@@ -31,7 +31,7 @@
 & @App ~ (d (f j))
 @C6 = a
 & @Lam ~ (@C6$S0 a)
-@C6$S0 = ({15 a {17 b {19 c {21 d {23 e f}}}}} g)
+@C6$S0 = ({9 a {9 b {9 c {9 d {9 e f}}}}} g)
 & @Lam ~ ((h i) g)
 & @App ~ (a (j i))
 & @App ~ (b (k j))
@@ -41,7 +41,7 @@
 & @App ~ (f (h n))
 @C8 = a
 & @Lam ~ (@C8$S0 a)
-@C8$S0 = ({25 a {27 b {29 c {31 d {33 e {35 f g}}}}}} h)
+@C8$S0 = ({11 a {11 b {11 c {11 d {11 e {11 f g}}}}}} h)
 & @Lam ~ ((i j) h)
 & @App ~ (a (k j))
 & @App ~ (b (l k))
@@ -53,14 +53,14 @@
 @CS = a
 & @Lam ~ (@CS$S0 a)
 @CS$S0 = (a b)
-& @Lam ~ (({37 c d} e) b)
+& @Lam ~ (({13 c d} e) b)
 & @Lam ~ ((f g) e)
 & @App ~ (c (h g))
 & @App ~ (i (f h))
 & @App ~ (a (d i))
 @FOO = a
 & @Lam ~ (@FOO$S0 a)
-@FOO$S0 = ({39 a b} c)
+@FOO$S0 = ({15 a b} c)
 & @App ~ (a (b c))
 @False = a
 & @Lam ~ (@False$S0 a)
diff --git a/examples/machine_u32/num_match.hvmc b/examples/machine_u32/num_match.hvmc
index 698a9813..15c12302 100644
--- a/examples/machine_u32/num_match.hvmc
+++ b/examples/machine_u32/num_match.hvmc
@@ -1,4 +1,5 @@
 @main = a
 & @pred ~ (#10 a)
-@pred = (?<(#0 (a a)) b> b)
+@pred = (?<(a b) d> d)
+& (a b) ~ (#0 (c c))
 
diff --git a/examples/sort/bitonic/bitonic_sort_lam.hvmc b/examples/sort/bitonic/bitonic_sort_lam.hvmc
index 259d2f1d..89601038 100644
--- a/examples/sort/bitonic/bitonic_sort_lam.hvmc
+++ b/examples/sort/bitonic/bitonic_sort_lam.hvmc
@@ -13,7 +13,8 @@
 @flow$S1 = (a (b ({5 c d} e)))
 & @down ~ (f (d e))
 & @warp ~ (a (b (c f)))
-@gen = (?<(@gen$S0 @gen$S1) a> a)
+@gen = (?<(a b) c> c)
+& (a b) ~ (@gen$S0 @gen$S1)
 @gen$S0 = (a b)
 & @Leaf ~ (a b)
 @gen$S1 = ({7 a b} ({9 <* #2 c> <* #2 <+ #1 d>>} e))
@@ -55,7 +56,8 @@
 @sum$S0 = (a (b c))
 & @sum ~ (a <+ d c>)
 & @sum ~ (b d)
-@swap = (?<(@swap$S0 @swap$S2) a> a)
+@swap = (?<(a b) c> c)
+& (a b) ~ (@swap$S0 @swap$S2)
 @swap$S0 = (a (b c))
 & @Node ~ (a (b c))
 @swap$S1 = (a (b c))
diff --git a/examples/sort/merge/merge_sort.hvmc b/examples/sort/merge/merge_sort.hvmc
index 75b6774b..5f636967 100644
--- a/examples/sort/merge/merge_sort.hvmc
+++ b/examples/sort/merge/merge_sort.hvmc
@@ -1,7 +1,7 @@
-@Leaf = (a {8 {10 a b} {8 * b}})
-@List.cons = (a (b {2 {6 a {4 b c}} {2 * c}}))
+@Leaf = (a {4 {4 a b} {4 * b}})
+@List.cons = (a (b {2 {2 a {2 b c}} {2 * c}}))
 @List.nil = {2 * {2 a a}}
-@Node = (a (b {8 * {8 {14 a {12 b c}} c}}))
+@Node = (a (b {4 * {4 {4 a {4 b c}} c}}))
 @main = a
 & @sum ~ (b a)
 & @sort ~ (c b)
@@ -12,13 +12,15 @@
 @merge$S1 = (a (b (c ((c (a (b d))) d))))
 @merge$S2 = (a (b (c ((a (b (c d))) d))))
 @merge$S3 = (* @merge$S2)
-@merge$S4 = ({3 a b} (c ({5 << a ?<(@merge$S1 @merge$S3) d>> e} (f g))))
-& ((h ((i i) (j k))) k) ~ (d (((l m) ((f n) ((c o) m))) g))
-& @merge ~ (n (o l))
-& @List.cons ~ (b j)
-& @List.cons ~ (e h)
+@merge$S4 = ({3 a b} (c ({5 << a ?<(d e) f>> g} (h i))))
+& (d e) ~ (@merge$S1 @merge$S3)
+& ((j ((k k) (l m))) m) ~ (f (((n o) ((h p) ((c q) o))) i))
+& @merge ~ (p (q n))
+& @List.cons ~ (b l)
+& @List.cons ~ (g j)
 @merge$S5 = (a (b ((@merge$S0 (@merge$S4 (a (b c)))) c)))
-@range = (?<(@range$S0 @range$S1) a> a)
+@range = (?<(a b) c> c)
+& (a b) ~ (@range$S0 @range$S1)
 @range$S0 = (a b)
 & @Leaf ~ (a b)
 @range$S1 = ({7 a b} ({9 <* #2 <+ #1 c>> <* #2 d>} e))
diff --git a/examples/sort/radix/radix_sort_lam.hvmc b/examples/sort/radix/radix_sort_lam.hvmc
index cbddfe16..85359c30 100644
--- a/examples/sort/radix/radix_sort_lam.hvmc
+++ b/examples/sort/radix/radix_sort_lam.hvmc
@@ -5,10 +5,11 @@
 @Single = (a (* ((a b) (* b))))
 @Used = (* @Used$S0)
 @Used$S0 = (a (* a))
-@gen = (?<(@gen$S0 @gen$S1) a> a)
+@gen = (?<(a b) c> c)
+& (a b) ~ (@gen$S0 @gen$S1)
 @gen$S0 = (a b)
 & @Single ~ (a b)
-@gen$S1 = ({51 a b} (<<< #1 {53 c <| #1 d>}> e))
+@gen$S1 = ({7 a b} (<<< #1 {9 c <| #1 d>}> e))
 & @Concat ~ (f (g e))
 & @gen ~ (b (d g))
 & @gen ~ (a (c f))
@@ -33,7 +34,7 @@
 & @merge ~ (d (b g))
 & @merge ~ (c (a f))
 @merge$S9 = (a (b ((@merge$S5 (@merge$S7 (@merge$S8 (a (b c))))) c)))
-@radix = ({3 <& #8388608 a> {5 <& #4194304 b> {7 <& #2097152 c> {9 <& #1048576 d> {11 <& #524288 e> {13 <& #262144 f> {15 <& #131072 g> {17 <& #65536 h> {19 <& #32768 i> {21 <& #16384 j> {23 <& #8192 k> {25 <& #4096 l> {27 <& #2048 m> {29 <& #1024 n> {31 <& #512 o> {33 <& #256 p> {35 <& #128 q> {37 <& #64 r> {39 <& #32 s> {41 <& #16 t> {43 <& #8 u> {45 <& #4 v> {47 <& #2 w> <& #1 x>}}}}}}}}}}}}}}}}}}}}}}} y)
+@radix = ({3 <& #8388608 a> {3 <& #4194304 b> {3 <& #2097152 c> {3 <& #1048576 d> {3 <& #524288 e> {3 <& #262144 f> {3 <& #131072 g> {3 <& #65536 h> {3 <& #32768 i> {3 <& #16384 j> {3 <& #8192 k> {3 <& #4096 l> {3 <& #2048 m> {3 <& #1024 n> {3 <& #512 o> {3 <& #256 p> {3 <& #128 q> {3 <& #64 r> {3 <& #32 s> {3 <& #16 t> {3 <& #8 u> {3 <& #4 v> {3 <& #2 w> <& #1 x>}}}}}}}}}}}}}}}}}}}}}}} y)
 & @swap ~ (a (z (@Free y)))
 & @swap ~ (b (ab (@Free z)))
 & @swap ~ (c (bb (@Free ab)))
@@ -72,7 +73,8 @@
 @sum$S0 = (a (b c))
 & @sum ~ (a <+ d c>)
 & @sum ~ (b d)
-@swap = (?<(@swap$S0 @swap$S2) a> a)
+@swap = (?<(a b) c> c)
+& (a b) ~ (@swap$S0 @swap$S2)
 @swap$S0 = (a (b c))
 & @Node ~ (a (b c))
 @swap$S1 = (a (b c))
@@ -82,7 +84,7 @@
 @to_arr$S0 = (* @Empty)
 @to_arr$S1 = (a b)
 & @Single ~ (a b)
-@to_arr$S2 = (a (b ({49 <* #2 <+ #1 c>> <* #2 <+ #0 d>>} e)))
+@to_arr$S2 = (a (b ({5 <* #2 <+ #1 c>> <* #2 <+ #0 d>>} e)))
 & @Concat ~ (f (g e))
 & @to_arr ~ (b (c g))
 & @to_arr ~ (a (d f))
diff --git a/src/ast.rs b/src/ast.rs
index 46502e60..0e9adb7f 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -10,10 +10,12 @@
 //!
 //! [interaction calculus]: https://en.wikipedia.org/wiki/Interaction_nets#Interaction_calculus
 
+use arrayvec::ArrayVec;
+
 use crate::{
   ops::Op,
   run::Lab,
-  util::{deref, maybe_grow},
+  util::{array_vec, deref, maybe_grow},
 };
 use std::{collections::BTreeMap, fmt, str::FromStr};
 
@@ -49,7 +51,7 @@ pub struct Net {
 /// Here, the wires at the leaves of the tree are represented with
 /// [`Tree::Var`], where the variable name is shared between both sides of the
 /// wire.
-#[derive(Clone, Hash, PartialEq, Eq, Debug, Default)]
+#[derive(Hash, PartialEq, Eq, Debug, Default)]
 pub enum Tree {
   #[default]
   /// A nilary eraser node.
@@ -58,13 +60,21 @@ pub enum Tree {
   Num { val: u64 },
   /// A nilary node, referencing a named net.
   Ref { nam: String },
-  /// A binary interaction combinator.
+  /// A n-ary interaction combinator.
   Ctr {
     /// The label of the combinator. (Combinators with the same label
     /// annihilate, and combinators with different labels commute.)
     lab: Lab,
-    lft: Box<Tree>,
-    rgt: Box<Tree>,
+    /// The auxiliary ports of this node.
+    ///
+    /// - 0 ports: this behaves identically to an eraser node.
+    /// - 1 port: this behaves identically to a wire.
+    /// - 2 ports: this is a standard binary combinator node.
+    /// - 3+ ports: equivalent to right-chained binary nodes; `(a b c)` is
+    ///   equivalent to `(a (b c))`.
+    ///
+    /// The length of this vector must be less than [`MAX_ARITY`].
+    ports: Vec<Tree>,
   },
   /// A binary node representing an operation on native integers.
   ///
@@ -81,20 +91,108 @@ pub enum Tree {
   ///
   /// The principal port connects to the integer to be matched on.
   Mat {
-    /// An auxiliary port; connects to the branches of this match.
-    ///
-    /// This should be connected to something of the form:
-    /// ```text
-    /// (+value_if_zero (-predecessor_of_number +value_if_non_zero))
-    /// ```
-    sel: Box<Tree>,
+    /// An auxiliary port; connects to the zero branch.
+    zero: Box<Tree>,
+    /// An auxiliary port; connects to the a CTR with label 0 containing the
+    /// predecessor and the output of the succ branch.
+    succ: Box<Tree>,
     /// An auxiliary port; connects to the output.
-    ret: Box<Tree>,
+    out: Box<Tree>,
+  },
+  /// An Scott-encoded ADT node.
+  ///
+  /// This is always equivalent to:
+  /// ```text
+  /// {$lab
+  ///   * * * ...                // one era node per `variant_index`
+  ///   {$lab $f0 $f1 $f2 ... R} // each field, in order, followed by a var node
+  ///   * * * ...                // one era node per `variant_count - variant_index - 1`
+  ///   R                        // a var node
+  /// }
+  /// ```
+  ///
+  /// For example:
+  /// ```text
+  /// data Option = None | (Some value):
+  ///   None:
+  ///     (0:2) = Adt { lab: 0, variant_index: 0, variant_count: 2, fields: [] }
+  ///     (R * R) = Ctr { lab: 0, ports: [Var { nam: "R" }, Era, Var { nam: "R" }]}
+  ///   (Some 123):
+  ///     (1:2 #123) = Adt { lab: 0, variant_index: 0, variant_count: 2, fields: [Num { val: 123 }] }
+  ///     (* (#123 R) R) = Ctr { lab: 0, ports: [Era, Ctr { lab: 0, ports: [Num { val: 123 }, Var { nam: "R" }] }, Var { nam: "R" }]}
+  /// ```
+  Adt {
+    lab: Lab,
+    /// The index of the variant of this ADT node.
+    ///
+    /// Must be less than `variant_count`.
+    variant_index: usize,
+    /// The number of variants in the data type.
+    ///
+    /// Must be greater than `0` and less than `MAX_ADT_VARIANTS`.
+    variant_count: usize,
+    /// The fields of this ADT node.
+    ///
+    /// Must have a length less than `MAX_ADT_FIELDS`.
+    fields: Vec<Tree>,
   },
   /// One side of a wire; the other side will have the same name.
   Var { nam: String },
 }
 
+pub const MAX_ARITY: usize = 8;
+pub const MAX_ADT_VARIANTS: usize = MAX_ARITY - 1;
+pub const MAX_ADT_FIELDS: usize = MAX_ARITY - 1;
+
+impl Net {
+  pub fn trees(&self) -> impl Iterator<Item = &Tree> {
+    std::iter::once(&self.root).chain(self.redexes.iter().map(|(x, y)| [x, y]).flatten())
+  }
+  pub fn trees_mut(&mut self) -> impl Iterator<Item = &mut Tree> {
+    std::iter::once(&mut self.root).chain(self.redexes.iter_mut().map(|(x, y)| [x, y]).flatten())
+  }
+}
+
+impl Tree {
+  #[inline(always)]
+  pub fn children(&self) -> impl Iterator<Item = &Tree> {
+    ArrayVec::<_, MAX_ARITY>::into_iter(match self {
+      Tree::Era | Tree::Num { .. } | Tree::Ref { .. } | Tree::Var { .. } => array_vec::from_array([]),
+      Tree::Ctr { ports, .. } => array_vec::from_iter(ports),
+      Tree::Op { rhs, out, .. } => array_vec::from_array([rhs, out]),
+      Tree::Mat { zero, succ, out } => array_vec::from_array([zero, succ, out]),
+      Tree::Adt { fields, .. } => array_vec::from_iter(fields),
+    })
+  }
+
+  #[inline(always)]
+  pub fn children_mut(&mut self) -> impl Iterator<Item = &mut Tree> {
+    ArrayVec::<_, MAX_ARITY>::into_iter(match self {
+      Tree::Era | Tree::Num { .. } | Tree::Ref { .. } | Tree::Var { .. } => array_vec::from_array([]),
+      Tree::Ctr { ports, .. } => array_vec::from_iter(ports),
+      Tree::Op { rhs, out, .. } => array_vec::from_array([rhs, out]),
+      Tree::Mat { zero, succ, out } => array_vec::from_array([zero, succ, out]),
+      Tree::Adt { fields, .. } => array_vec::from_iter(fields),
+    })
+  }
+
+  pub(crate) fn lab(&self) -> Option<Lab> {
+    match self {
+      Tree::Ctr { lab, ports } if ports.len() >= 2 => Some(*lab),
+      Tree::Adt { lab, .. } => Some(*lab),
+      _ => None,
+    }
+  }
+
+  pub fn legacy_mat(arms: Tree, out: Tree) -> Option<Tree> {
+    let Tree::Ctr { lab: 0, ports } = arms else { None? };
+    let Ok([zero, succ]) = <[_; 2]>::try_from(ports) else { None? };
+    let zero = Box::new(zero);
+    let succ = Box::new(succ);
+    Some(Tree::Mat { zero, succ, out: Box::new(out) })
+  }
+}
+
 /// The state of the HVMC parser.
 struct Parser<'i> {
   /// The remaining characters in the input. An empty string indicates EOF.
@@ -147,15 +245,52 @@ impl<'i> Parser<'i> {
             '{' => self.parse_int()? as Lab,
             _ => unreachable!(),
           };
-          let lft = Box::new(self.parse_tree()?);
-          let rgt = Box::new(self.parse_tree()?);
-          self.consume(match char {
-            '(' => ")",
-            '[' => "]",
-            '{' => "}",
+          let close = match char {
+            '(' => ')',
+            '[' => ']',
+            '{' => '}',
             _ => unreachable!(),
-          })?;
-          Ok(Tree::Ctr { lab, lft, rgt })
+          };
+          self.skip_trivia();
+          if self.peek_char().is_some_and(|x| x == ':') {
+            let variant_index = self.parse_int()?;
+            self.consume(":")?;
+            let variant_count = self.parse_int()?;
+            let mut fields = Vec::new();
+            self.skip_trivia();
+            while self.peek_char() != Some(close) {
+              fields.push(self.parse_tree()?);
+              self.skip_trivia();
+            }
+            self.advance_char();
+            if variant_count == 0 {
+              Err("variant count cannot be zero".to_owned())?;
+            }
+            if variant_count > (MAX_ADT_VARIANTS as u64) {
+              Err("adt has too many variants".to_owned())?;
+            }
+            if variant_index >= variant_count {
+              Err("variant index out of range".to_owned())?;
+            }
+            let variant_index = variant_index as usize;
+            let variant_count = variant_count as usize;
+            if fields.len() > MAX_ADT_FIELDS {
+              Err("adt has too many fields".to_owned())?;
+            }
+            Ok(Tree::Adt { lab, variant_index, variant_count, fields })
+          } else {
+            let mut ports = Vec::new();
+            self.skip_trivia();
+            while self.peek_char() != Some(close) {
+              ports.push(self.parse_tree()?);
+              self.skip_trivia();
+            }
+            self.advance_char();
+            if ports.len() > MAX_ARITY {
+              Err("ctr has too many ports".to_owned())?;
+            }
+            Ok(Tree::Ctr { lab, ports })
+          }
         }
         // Ref = "@" Name
         Some('@') => {
@@ -182,10 +317,19 @@ impl<'i> Parser<'i> {
         Some('?') => {
           self.advance_char();
           self.consume("<")?;
-          let sel = Box::new(self.parse_tree()?);
-          let ret = Box::new(self.parse_tree()?);
-          self.consume(">")?;
-          Ok(Tree::Mat { sel, ret })
+          let zero = self.parse_tree()?;
+          let succ = self.parse_tree()?;
+          self.skip_trivia();
+          if self.peek_char() == Some('>') {
+            self.advance_char();
+            Tree::legacy_mat(zero, succ).ok_or_else(|| "invalid legacy match".to_owned())
+          } else {
+            let zero = Box::new(zero);
+            let succ = Box::new(succ);
+            let out = Box::new(self.parse_tree()?);
+            self.consume(">")?;
+            Ok(Tree::Mat { zero, succ, out })
+          }
         }
         // Var = Name
         _ => Ok(Tree::Var { nam: self.parse_name()? }),
@@ -335,16 +479,68 @@ impl fmt::Display for Tree {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     maybe_grow(move || match self {
       Tree::Era => write!(f, "*"),
-      Tree::Ctr { lab, lft, rgt } => match lab {
-        0 => write!(f, "({lft} {rgt})"),
-        1 => write!(f, "[{lft} {rgt}]"),
-        _ => write!(f, "{{{lab} {lft} {rgt}}}"),
-      },
+      Tree::Ctr { lab, ports } => {
+        match lab {
+          0 => write!(f, "("),
+          1 => write!(f, "["),
+          _ => write!(f, "{{{lab}"),
+        }?;
+        let mut space = *lab > 1;
+        for port in ports {
+          if space {
+            write!(f, " ")?;
+          }
+          write!(f, "{port}")?;
+          space = true;
+        }
+        match lab {
+          0 => write!(f, ")"),
+          1 => write!(f, "]"),
+          _ => write!(f, "}}"),
+        }?;
+        Ok(())
+      }
+      Tree::Adt { lab, variant_index, variant_count, fields } => {
+        match lab {
+          0 => write!(f, "("),
+          1 => write!(f, "["),
+          _ => write!(f, "{{{lab}"),
+        }?;
+        write!(f, ":{}:{}", variant_index, variant_count)?;
+        for field in fields {
+          write!(f, " {field}")?;
+        }
+        match lab {
+          0 => write!(f, ")"),
+          1 => write!(f, "]"),
+          _ => write!(f, "}}"),
+        }?;
+        Ok(())
+      }
       Tree::Var { nam } => write!(f, "{nam}"),
       Tree::Ref { nam } => write!(f, "@{nam}"),
       Tree::Num { val } => write!(f, "#{val}"),
       Tree::Op { op, rhs, out } => write!(f, "<{op} {rhs} {out}>"),
-      Tree::Mat { sel, ret } => write!(f, "?<{sel} {ret}>"),
+      Tree::Mat { zero, succ, out } => write!(f, "?<{zero} {succ} {out}>"),
+    })
+  }
+}
+impl Clone for Tree {
+  fn clone(&self) -> Tree {
+    maybe_grow(|| match self {
+      Tree::Era => Tree::Era,
+      Tree::Num { val } => Tree::Num { val: val.clone() },
+      Tree::Ref { nam } => Tree::Ref { nam: nam.clone() },
+      Tree::Ctr { lab, ports } => Tree::Ctr { lab: lab.clone(), ports: ports.clone() },
+      Tree::Op { op, rhs, out } => Tree::Op { op: op.clone(), rhs: rhs.clone(), out: out.clone() },
+      Tree::Mat { zero, succ, out } => Tree::Mat { zero: zero.clone(), succ: succ.clone(), out: out.clone() },
+      Tree::Adt { lab, variant_index, variant_count, fields } => Tree::Adt {
+        lab: lab.clone(),
+        variant_index: variant_index.clone(),
+        variant_count: variant_count.clone(),
+        fields: fields.clone(),
+      },
+      Tree::Var { nam } => Tree::Var { nam: nam.clone() },
     })
   }
 }
diff --git a/src/host.rs b/src/host.rs
index ec5bfba5..de52bc29 100644
--- a/src/host.rs
+++ b/src/host.rs
@@ -12,12 +12,10 @@ use std::{
 };
 
 mod calc_labels;
-mod encode_def;
-mod encode_net;
+mod encode;
 mod readback;
 
 use calc_labels::calculate_label_sets;
-pub(crate) use encode_def::encode_def;
 
 /// Stores a bidirectional mapping between names and runtime defs.
 #[derive(Default)]
@@ -88,9 +86,7 @@ impl Host {
     // Now that `defs` is fully populated, we can fill in the instructions of
     // each of the new defs.
     for (nam, net) in book.iter() {
-      let data = encode_def(net, |nam| {
-        Port::new_ref(&self.defs[nam] /* calculate_label_sets already ensures all ref names are in self.defs */)
-      });
+      let data = self.encode_def(net);
       match self.defs.get_mut(nam).unwrap() {
         DefRef::Owned(def) => def.downcast_mut::<InterpretedDef>().unwrap().data = data,
         DefRef::Static(_) => unreachable!(),
diff --git a/src/host/calc_labels.rs b/src/host/calc_labels.rs
index 13026e5b..79e57ced 100644
--- a/src/host/calc_labels.rs
+++ b/src/host/calc_labels.rs
@@ -167,27 +167,21 @@ impl<'b, F: FnMut(&'b str) -> LabSet> State<'b, F> {
   }
 
   fn visit_tree(&mut self, tree: &'b Tree, depth: Option<usize>, mut out: Option<&mut LabSet>) -> usize {
-    maybe_grow(move || match tree {
-      Tree::Era | Tree::Var { .. } | Tree::Num { .. } => usize::MAX,
-      Tree::Ctr { lab, lft, rgt } => {
+    maybe_grow(move || {
+      if let Some(lab) = tree.lab() {
         if let Some(out) = out.as_deref_mut() {
-          out.add(*lab);
+          out.add(lab);
         }
-        usize::min(self.visit_tree(lft, depth, out.as_deref_mut()), self.visit_tree(rgt, depth, out.as_deref_mut()))
       }
-      Tree::Ref { nam } => {
+      if let Tree::Ref { nam } = tree {
         if self.book.contains_key(nam) {
-          self.visit_def(nam, depth.map(|x| x + 1), out)
-        } else {
-          if let Some(out) = out {
-            out.union(&(self.lookup)(nam));
-          }
-          usize::MAX
+          return self.visit_def(nam, depth.map(|x| x + 1), out);
+        }
+        if let Some(out) = &mut out {
+          out.union(&(self.lookup)(nam));
         }
       }
-      Tree::Op { rhs: lft, out: rgt, .. } | Tree::Mat { sel: lft, ret: rgt } => {
-        usize::min(self.visit_tree(lft, depth, out.as_deref_mut()), self.visit_tree(rgt, depth, out.as_deref_mut()))
-      }
+      tree.children().map(|child| self.visit_tree(child, depth, out.as_deref_mut())).fold(usize::MAX, usize::min)
     })
   }
 }
diff --git a/src/host/encode.rs b/src/host/encode.rs
new file mode 100644
index 00000000..31bd7717
--- /dev/null
+++ b/src/host/encode.rs
@@ -0,0 +1,214 @@
+use super::*;
+use crate::{ops::Op, run::Lab, util::maybe_grow};
+
+impl Host {
+  /// Converts an ast net to a list of instructions to create the net.
+  ///
+  /// `get_def` must return the `Port` corresponding to a given `Ref` name.
+  pub(crate) fn encode_def(&self, net: &Net) -> InterpretedDef {
+    let mut def = InterpretedDef { instr: Vec::new(), trgs: 1 };
+    let mut state = State { host: self, encoder: &mut def, scope: Default::default() };
+    state.visit_net(net, TrgId::new(0));
+    state.finish();
+    def
+  }
+
+  /// Encode `tree` directly into `trg`, skipping the intermediate `Def`
+  /// representation.
+  pub fn encode_tree<M: Mode>(&self, net: &mut run::Net<M>, trg: run::Trg, tree: &Tree) {
+    let mut state = State { host: self, encoder: net, scope: Default::default() };
+    state.visit_tree(tree, trg);
+    state.finish();
+  }
+
+  /// Encode the root of `ast_net` directly into `trg` and encode its redexes
+  /// into `net` redex list.
+  pub fn encode_net<M: Mode>(&self, net: &mut run::Net<M>, trg: run::Trg, ast_net: &Net) {
+    let mut state = State { host: self, encoder: net, scope: Default::default() };
+    state.visit_net(ast_net, trg);
+    state.finish();
+  }
+}
+
+struct State<'a, E: Encoder> {
+  host: &'a Host,
+  encoder: &'a mut E,
+  scope: HashMap<&'a str, E::Trg>,
+}
+
+impl<'a, E: Encoder> State<'a, E> {
+  fn finish(self) {
+    assert!(self.scope.is_empty(), "unbound variables: {:?}", self.scope.keys());
+  }
+  fn visit_net(&mut self, net: &'a Net, trg: E::Trg) {
+    self.visit_tree(&net.root, trg);
+    net.redexes.iter().for_each(|(a, b)| self.visit_redex(a, b));
+  }
+  fn visit_redex(&mut self, a: &'a Tree, b: &'a Tree) {
+    let (port, tree) = match (a, b) {
+      (Tree::Era, t) | (t, Tree::Era) => (Port::ERA, t),
+      (Tree::Ref { nam }, t) | (t, Tree::Ref { nam }) => (Port::new_ref(&self.host.defs[nam]), t),
+      (Tree::Num { val }, t) | (t, Tree::Num { val }) => (Port::new_num(*val), t),
+      (t, u) => {
+        let (av, aw, bv, bw) = self.encoder.wires();
+        self.visit_tree(t, av);
+        self.visit_tree(u, bv);
+        self.encoder.link(aw, bw);
+        return;
+      }
+    };
+    let trg = self.encoder.make_const(port);
+    self.visit_tree(tree, trg);
+  }
+  fn visit_tree(&mut self, tree: &'a Tree, trg: E::Trg) {
+    maybe_grow(move || match tree {
+      Tree::Era => self.encoder.link_const(trg, Port::ERA),
+      Tree::Num { val } => self.encoder.link_const(trg, Port::new_num(*val)),
+      Tree::Ref { nam } => self.encoder.link_const(trg, Port::new_ref(&self.host.defs[nam])),
+      Tree::Ctr { lab, ports } => {
+        if ports.is_empty() {
+          return self.visit_tree(&Tree::Era, trg);
+        }
+        let mut trg = trg;
+        for port in &ports[0 .. ports.len() - 1] {
+          let (l, r) = self.encoder.ctr(*lab, trg);
+          self.visit_tree(port, l);
+          trg = r;
+        }
+        self.visit_tree(ports.last().unwrap(), trg);
+      }
+      Tree::Adt { lab, variant_index, variant_count, fields } => {
+        let mut trg = trg;
+        for _ in 0 .. *variant_index {
+          let (l, r) = self.encoder.ctr(*lab, trg);
+          self.visit_tree(&Tree::Era, l);
+          trg = r;
+        }
+        let (mut l, mut r) = self.encoder.ctr(*lab, trg);
+        for field in fields {
+          let (x, y) = self.encoder.ctr(*lab, l);
+          self.visit_tree(field, x);
+          l = y;
+        }
+        for _ in 0 .. (*variant_count - *variant_index - 1) {
+          let (x, y) = self.encoder.ctr(*lab, r);
+          self.visit_tree(&Tree::Era, x);
+          r = y;
+        }
+        self.encoder.link(l, r);
+      }
+      Tree::Op { op, rhs: lft, out: rgt } => {
+        let (l, r) = self.encoder.op(*op, trg);
+        self.visit_tree(lft, l);
+        self.visit_tree(rgt, r);
+      }
+      Tree::Mat { zero, succ, out } => {
+        let (a, o) = self.encoder.mat(trg);
+        let (z, s) = self.encoder.ctr(0, a);
+        self.visit_tree(zero, z);
+        self.visit_tree(succ, s);
+        self.visit_tree(out, o);
+      }
+      Tree::Var { nam } => match self.scope.entry(nam) {
+        Entry::Occupied(e) => self.encoder.link(e.remove(), trg),
+        Entry::Vacant(e) => {
+          e.insert(trg);
+        }
+      },
+    })
+  }
+}
+
+trait Encoder {
+  type Trg;
+  fn link_const(&mut self, trg: Self::Trg, port: Port);
+  fn link(&mut self, a: Self::Trg, b: Self::Trg);
+  fn make_const(&mut self, port: Port) -> Self::Trg;
+  fn ctr(&mut self, lab: Lab, trg: Self::Trg) -> (Self::Trg, Self::Trg);
+  fn op(&mut self, op: Op, trg: Self::Trg) -> (Self::Trg, Self::Trg);
+  fn op_num(&mut self, op: Op, trg: Self::Trg, rhs: u64) -> Self::Trg;
+  fn mat(&mut self, trg: Self::Trg) -> (Self::Trg, Self::Trg);
+  fn wires(&mut self) -> (Self::Trg, Self::Trg, Self::Trg, Self::Trg);
+}
+
+impl InterpretedDef {
+  fn new_trg_id(&mut self) -> TrgId {
+    let index = self.trgs;
+    self.trgs += 1;
+    TrgId::new(index)
+  }
+}
+
+impl Encoder for InterpretedDef {
+  type Trg = TrgId;
+  fn link_const(&mut self, trg: Self::Trg, port: Port) {
+    self.instr.push(Instruction::LinkConst { trg, port });
+  }
+  fn link(&mut self, a: Self::Trg, b: Self::Trg) {
+    self.instr.push(Instruction::Link { a, b });
+  }
+  fn make_const(&mut self, port: Port) -> Self::Trg {
+    let trg = self.new_trg_id();
+    self.instr.push(Instruction::Const { trg, port });
+    trg
+  }
+  fn ctr(&mut self, lab: Lab, trg: Self::Trg) -> (Self::Trg, Self::Trg) {
+    let lft = self.new_trg_id();
+    let rgt = self.new_trg_id();
+    self.instr.push(Instruction::Ctr { lab, trg, lft, rgt });
+    (lft, rgt)
+  }
+  fn op(&mut self, op: Op, trg: Self::Trg) -> (Self::Trg, Self::Trg) {
+    let rhs = self.new_trg_id();
+    let out = self.new_trg_id();
+    self.instr.push(Instruction::Op { op, trg, rhs, out });
+    (rhs, out)
+  }
+  fn op_num(&mut self, op: Op, trg: Self::Trg, rhs: u64) -> Self::Trg {
+    let out = self.new_trg_id();
+    self.instr.push(Instruction::OpNum { op, trg, rhs, out });
+    out
+  }
+  fn mat(&mut self, trg: Self::Trg) -> (Self::Trg, Self::Trg) {
+    let lft = self.new_trg_id();
+    let rgt = self.new_trg_id();
+    self.instr.push(Instruction::Mat { trg, lft, rgt });
+    (lft, rgt)
+  }
+  fn wires(&mut self) -> (Self::Trg, Self::Trg, Self::Trg, Self::Trg) {
+    let av = self.new_trg_id();
+    let aw = self.new_trg_id();
+    let bv = self.new_trg_id();
+    let bw = self.new_trg_id();
+    self.instr.push(Instruction::Wires { av, aw, bv, bw });
+    (av, aw, bv, bw)
+  }
+}
+
+impl<'a, M: Mode> Encoder for run::Net<'a, M> {
+  type Trg = run::Trg;
+  fn link_const(&mut self, trg: Self::Trg, port: Port) {
+    self.link_trg_port(trg, port)
+  }
+  fn link(&mut self, a: Self::Trg, b: Self::Trg) {
+    self.link_trg(a, b)
+  }
+  fn make_const(&mut self, port: Port) -> Self::Trg {
+    run::Trg::port(port)
+  }
+  fn ctr(&mut self, lab: Lab, trg: Self::Trg) -> (Self::Trg, Self::Trg) {
+    self.do_ctr(lab, trg)
+  }
+  fn op(&mut self, op: Op, trg: Self::Trg) -> (Self::Trg, Self::Trg) {
+    self.do_op(op, trg)
+  }
+  fn op_num(&mut self, op: Op, trg: Self::Trg, rhs: u64) -> Self::Trg {
+    self.do_op_num(op, trg, rhs)
+  }
+  fn mat(&mut self, trg: Self::Trg) -> (Self::Trg, Self::Trg) {
+    self.do_mat(trg)
+  }
+  fn wires(&mut self) -> (Self::Trg, Self::Trg, Self::Trg, Self::Trg) {
+    self.do_wires()
+  }
+}
diff --git a/src/host/encode_def.rs b/src/host/encode_def.rs
deleted file mode 100644
index a6748e1c..00000000
--- a/src/host/encode_def.rs
+++ /dev/null
@@ -1,107 +0,0 @@
-use crate::util::maybe_grow;
-
-use super::*;
-
-/// Converts an ast net to a list of instructions to create the net.
-///
-/// `get_def` must return the `Port` corresponding to a given `Ref` name.
-pub(crate) fn encode_def<F: FnMut(&str) -> Port>(net: &Net, get_def: F) -> InterpretedDef {
-  let mut state =
-    State { get_def, scope: Default::default(), instr: Default::default(), end: Default::default(), next_index: 1 };
-
-  state.visit_tree(&net.root, TrgId::new(0));
-
-  net.redexes.iter().for_each(|(a, b)| state.visit_redex(a, b));
-
-  assert!(state.scope.is_empty(), "unbound variables: {:?}", state.scope.keys());
-
-  state.instr.append(&mut state.end);
-
-  InterpretedDef { instr: state.instr, trgs: state.next_index }
-}
-
-struct State<'a, F: FnMut(&str) -> Port> {
-  get_def: F,
-  scope: HashMap<&'a str, TrgId>,
-  instr: Vec<Instruction>,
-  end: Vec<Instruction>,
-  next_index: usize,
-}
-
-impl<'a, F: FnMut(&str) -> Port> State<'a, F> {
-  fn id(&mut self) -> TrgId {
-    let i = self.next_index;
-    self.next_index += 1;
-    TrgId::new(i)
-  }
-  fn visit_redex(&mut self, a: &'a Tree, b: &'a Tree) {
-    let (port, tree) = match (a, b) {
-      (Tree::Era, t) | (t, Tree::Era) => (Port::ERA, t),
-      (Tree::Ref { nam }, t) | (t, Tree::Ref { nam }) => ((self.get_def)(&nam), t),
-      (Tree::Num { val }, t) | (t, Tree::Num { val }) => (Port::new_num(*val), t),
-      (t, u) => {
-        let av = self.id();
-        let aw = self.id();
-        let bv = self.id();
-        let bw = self.id();
-        self.instr.push(Instruction::Wires { av, aw, bv, bw });
-        self.end.push(Instruction::Link { a: aw, b: bw });
-        self.visit_tree(t, av);
-        self.visit_tree(u, bv);
-        return;
-      }
-    };
-    let trg = self.id();
-    self.instr.push(Instruction::Const { port, trg });
-    self.visit_tree(tree, trg);
-  }
-  fn visit_tree(&mut self, tree: &'a Tree, trg: TrgId) {
-    maybe_grow(move || match tree {
-      Tree::Era => {
-        self.instr.push(Instruction::LinkConst { trg, port: Port::ERA });
-      }
-      Tree::Ref { nam } => {
-        self.instr.push(Instruction::LinkConst { trg, port: (self.get_def)(&nam) });
-      }
-      Tree::Num { val } => {
-        self.instr.push(Instruction::LinkConst { trg, port: Port::new_num(*val) });
-      }
-      Tree::Var { nam } => match self.scope.entry(nam) {
-        Entry::Occupied(e) => {
-          let other = e.remove();
-          self.instr.push(Instruction::Link { a: other, b: trg });
-        }
-        Entry::Vacant(e) => {
-          e.insert(trg);
-        }
-      },
-      Tree::Ctr { lab, lft, rgt } => {
-        let l = self.id();
-        let r = self.id();
-        self.instr.push(Instruction::Ctr { lab: *lab, trg, lft: l, rgt: r });
-        self.visit_tree(lft, l);
-        self.visit_tree(rgt, r);
-      }
-      Tree::Op { op, rhs, out } => {
-        if let Tree::Num { val } = &**rhs {
-          let o = self.id();
-          self.instr.push(Instruction::OpNum { op: *op, rhs: *val, trg, out: o });
-          self.visit_tree(out, o);
-        } else {
-          let r = self.id();
-          let o = self.id();
-          self.instr.push(Instruction::Op { op: *op, trg, rhs: r, out: o });
-          self.visit_tree(rhs, r);
-          self.visit_tree(out, o);
-        }
-      }
-      Tree::Mat { sel, ret } => {
-        let l = self.id();
-        let r = self.id();
-        self.instr.push(Instruction::Mat { trg, lft: l, rgt: r });
-        self.visit_tree(sel, l);
-        self.visit_tree(ret, r);
-      }
-    })
-  }
-}
diff --git a/src/host/encode_net.rs b/src/host/encode_net.rs
deleted file mode 100644
index 9a6c7054..00000000
--- a/src/host/encode_net.rs
+++ /dev/null
@@ -1,67 +0,0 @@
-//! Code for directly encoding a [`hvmc::ast::Net`] or a [`hvmc::ast::Tree`]
-//! into a [`hvmc::run::Net`]
-
-use std::collections::{hash_map::Entry, HashMap};
-
-use crate::{
-  ast::{Net, Tree},
-  host::Host,
-  run::{self, Mode, Port, Trg},
-};
-
-impl Host {
-  /// Encode `tree` directly into `trg`, skipping the intermediate `Def`
-  /// representation.
-  pub fn encode_tree<M: Mode>(&self, net: &mut run::Net<M>, trg: Trg, tree: &Tree) {
-    EncodeState { host: self, net, vars: Default::default() }.encode(trg, tree);
-  }
-  /// Encode the root of `ast_net` directly into `trg` and encode its redexes
-  /// into `net` redex list.
-  pub fn encode_net<M: Mode>(&self, net: &mut run::Net<M>, trg: Trg, ast_net: &Net) {
-    let mut state = EncodeState { host: self, net, vars: Default::default() };
-    for (l, r) in &ast_net.redexes {
-      let (ap, a, bp, b) = state.net.do_wires();
-      state.encode(ap, l);
-      state.encode(bp, r);
-      state.net.link_trg(a, b);
-    }
-    state.encode(trg, &ast_net.root);
-  }
-}
-
-struct EncodeState<'c, 'n, M: Mode> {
-  host: &'c Host,
-  net: &'c mut run::Net<'n, M>,
-  vars: HashMap<&'c str, Trg>,
-}
-
-impl<'c, 'n, M: Mode> EncodeState<'c, 'n, M> {
-  fn encode(&mut self, trg: Trg, tree: &'c Tree) {
-    match tree {
-      Tree::Era => self.net.link_trg_port(trg, Port::ERA),
-      Tree::Num { val } => self.net.link_trg_port(trg, Port::new_num(*val)),
-      Tree::Ref { nam } => self.net.link_trg_port(trg, Port::new_ref(&self.host.defs[nam])),
-      Tree::Ctr { lab, lft, rgt } => {
-        let (l, r) = self.net.do_ctr(*lab, trg);
-        self.encode(l, lft);
-        self.encode(r, rgt);
-      }
-      Tree::Op { op, rhs: lft, out: rgt } => {
-        let (l, r) = self.net.do_op(*op, trg);
-        self.encode(l, lft);
-        self.encode(r, rgt);
-      }
-      Tree::Mat { sel, ret } => {
-        let (s, r) = self.net.do_mat(trg);
-        self.encode(s, sel);
-        self.encode(r, ret);
-      }
-      Tree::Var { nam } => match self.vars.entry(nam) {
-        Entry::Occupied(e) => self.net.link_trg(e.remove(), trg),
-        Entry::Vacant(e) => {
-          e.insert(trg);
-        }
-      },
-    }
-  }
-}
diff --git a/src/host/readback.rs b/src/host/readback.rs
index 08a5c6db..72126391 100644
--- a/src/host/readback.rs
+++ b/src/host/readback.rs
@@ -64,11 +64,13 @@ impl<'a> ReadbackState<'a> {
       }
       Tag::Ctr => {
         let node = port.traverse_node();
-        Tree::Ctr { lab: node.lab, lft: Box::new(self.read_wire(node.p1)), rgt: Box::new(self.read_wire(node.p2)) }
+        Tree::Ctr { lab: node.lab, ports: vec![self.read_wire(node.p1), self.read_wire(node.p2)] }
       }
       Tag::Mat => {
         let node = port.traverse_node();
-        Tree::Mat { sel: Box::new(self.read_wire(node.p1)), ret: Box::new(self.read_wire(node.p2)) }
+        let arms = self.read_wire(node.p1);
+        let out = self.read_wire(node.p2);
+        Tree::legacy_mat(arms, out).expect("invalid mat node")
       }
     })
   }
diff --git a/src/lib.rs b/src/lib.rs
index 3084efd7..b38219eb 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1,6 +1,6 @@
-#![feature(const_type_id, extern_types, inline_const, new_uninit)]
+#![feature(const_type_id, extern_types, inline_const, generic_const_exprs, new_uninit)]
 #![cfg_attr(feature = "trace", feature(const_type_name))]
-#![allow(non_snake_case)]
+#![allow(non_snake_case, incomplete_features)]
 
 pub mod ast;
 pub mod compile;
diff --git a/src/main.rs b/src/main.rs
index 1acba438..985f41a9 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -209,15 +209,37 @@ struct RunArgs {
 
 #[derive(clap::ValueEnum, Clone, Debug)]
 pub enum TransformPass {
+  #[value(alias = "all")]
   All,
+  #[value(alias = "no-all")]
   NoAll,
+  #[value(alias = "pre")]
   PreReduce,
+  #[value(alias = "no-pre")]
   NoPreReduce,
+  #[value(alias = "coalesce")]
+  CoalesceCtrs,
+  #[value(alias = "no-coalesce")]
+  NoCoalesceCtrs,
+  #[value(alias = "adts")]
+  EncodeAdts,
+  #[value(alias = "no-adts")]
+  NoEncodeAdts,
 }
 
 #[derive(Default)]
 pub struct TransformPasses {
   pre_reduce: bool,
+  coalesce_ctrs: bool,
+  encode_adts: bool,
+}
+
+impl TransformPasses {
+  fn set_all(&mut self) {
+    self.pre_reduce = true;
+    self.coalesce_ctrs = true;
+    self.encode_adts = true;
+  }
 }
 
 impl TransformPass {
@@ -226,10 +248,14 @@ impl TransformPass {
     let mut opts = TransformPasses::default();
     for arg in args {
       match arg {
-        All => opts.pre_reduce = true,
-        NoAll => opts.pre_reduce = false,
+        All => opts.set_all(),
+        NoAll => opts = Default::default(),
         PreReduce => opts.pre_reduce = true,
         NoPreReduce => opts.pre_reduce = false,
+        CoalesceCtrs => opts.coalesce_ctrs = true,
+        NoCoalesceCtrs => opts.coalesce_ctrs = false,
+        EncodeAdts => opts.encode_adts = true,
+        NoEncodeAdts => opts.encode_adts = false,
       }
     }
     opts
@@ -293,6 +319,16 @@ fn load_book(files: &[String], transform_opts: &TransformOpts) -> Book {
       transform_opts.pre_reduce_rewrites,
     );
   }
+  for (_, def) in &mut book.nets {
+    for tree in def.trees_mut() {
+      if transform_passes.coalesce_ctrs {
+        tree.coalesce_constructors();
+      }
+      if transform_passes.encode_adts {
+        tree.encode_scott_adts();
+      }
+    }
+  }
   book
 }
 
@@ -374,8 +410,7 @@ fn compile_executable(target: &str, host: &host::Host) -> Result<(), io::Error>
     fuzz
     host {
       calc_labels
-      encode_def
-      encode_net
+      encode
       readback
     }
     lib
@@ -398,9 +433,12 @@ fn compile_executable(target: &str, host: &host::Host) -> Result<(), io::Error>
     trace
     transform {
       pre_reduce
+      encode_adts
+      coalesce_ctrs
     }
     util {
       apply_tree
+      array_vec
       bi_enum
       create_var
       deref
diff --git a/src/transform.rs b/src/transform.rs
index a5220e51..460dd479 100644
--- a/src/transform.rs
+++ b/src/transform.rs
@@ -1 +1,3 @@
+pub mod coalesce_ctrs;
+pub mod encode_adts;
 pub mod pre_reduce;
diff --git a/src/transform/coalesce_ctrs.rs b/src/transform/coalesce_ctrs.rs
new file mode 100644
index 00000000..2efe5d94
--- /dev/null
+++ b/src/transform/coalesce_ctrs.rs
@@ -0,0 +1,26 @@
+use crate::{
+  ast::{Tree, MAX_ARITY},
+  util::maybe_grow,
+};
+
+impl Tree {
+  /// Join chains of CTR nodes, such as `(a (b (c d)))` into n-ary nodes `(a b c
+  /// d)`
+  pub fn coalesce_constructors(&mut self) {
+    maybe_grow(|| match self {
+      Tree::Ctr { lab, ports } => {
+        ports.iter_mut().for_each(Tree::coalesce_constructors);
+        match ports.pop() {
+          Some(Tree::Ctr { lab: inner_lab, ports: mut inner_ports })
+            if inner_lab == *lab && ports.len() + inner_ports.len() < MAX_ARITY =>
+          {
+            ports.extend(inner_ports.drain(..));
+          }
+          Some(other) => ports.push(other),
+          None => (),
+        }
+      }
+      other => other.children_mut().for_each(Tree::coalesce_constructors),
+    })
+  }
+}
diff --git a/src/transform/encode_adts.rs b/src/transform/encode_adts.rs
new file mode 100644
index 00000000..fa1ba0a4
--- /dev/null
+++ b/src/transform/encode_adts.rs
@@ -0,0 +1,51 @@
+use crate::{ast::Tree, util::maybe_grow};
+
+impl Tree {
+  /// Encode scott-encoded ADTs into optimized compact ADT nodes
+  pub fn encode_scott_adts(&mut self) {
+    maybe_grow(|| match self {
+      &mut Tree::Ctr { lab, ref mut ports } => {
+        fn get_variant_index(lab: u16, ports: &[Tree]) -> Option<usize> {
+          let Some(Tree::Var { nam: ret_var }) = ports.last() else { return None };
+
+          let mut variant_index = None;
+          for (idx, i) in ports[0 .. ports.len() - 1].iter().enumerate() {
+            match i {
+              Tree::Era => {}
+              Tree::Ctr { lab: inner_lab, ports } if *inner_lab == lab && variant_index.is_none() => {
+                // Ensure that the last port is the return variable
+                let Some(Tree::Var { nam }) = ports.last() else { return None };
+                if nam != ret_var {
+                  return None;
+                }
+                variant_index = Some(idx);
+              }
+              // Nilary variant
+              Tree::Var { nam } if nam == ret_var && variant_index.is_none() => {
+                variant_index = Some(idx);
+              }
+              // Does not encode an ADT.
+              _ => return None,
+            }
+          }
+          variant_index
+        }
+
+        if let Some(variant_index) = get_variant_index(lab, ports) {
+          let fields = match ports.swap_remove(variant_index) {
+            Tree::Ctr { ports: mut fields, .. } => {
+              fields.pop();
+              fields
+            }
+            Tree::Var { .. } => vec![],
+            _ => unreachable!(),
+          };
+          *self = Tree::Adt { lab, variant_index, variant_count: ports.len(), fields };
+        }
+
+        self.children_mut().for_each(Tree::encode_scott_adts);
+      }
+      other => other.children_mut().for_each(Tree::encode_scott_adts),
+    })
+  }
+}
diff --git a/src/transform/pre_reduce.rs b/src/transform/pre_reduce.rs
index d1e9261b..d1f11833 100644
--- a/src/transform/pre_reduce.rs
+++ b/src/transform/pre_reduce.rs
@@ -21,7 +21,7 @@ use std::{
 
 use crate::{
   ast::{Book, Net, Tree},
-  host::{encode_def, DefRef, Host},
+  host::{DefRef, Host},
   run::{self, Def, Heap, InterpretedDef, LabSet, Rewrites},
   util::maybe_grow,
 };
@@ -108,15 +108,11 @@ struct State<'a> {
 
 impl<'a> State<'a> {
   fn visit_tree(&mut self, tree: &Tree) {
-    maybe_grow(move || match tree {
-      Tree::Era | Tree::Num { .. } | Tree::Var { .. } => (),
-      Tree::Ref { nam } => {
+    maybe_grow(move || {
+      if let Tree::Ref { nam } = tree {
         self.pre_reduce(nam);
       }
-      Tree::Ctr { lft, rgt, .. } | Tree::Op { rhs: lft, out: rgt, .. } | Tree::Mat { sel: lft, ret: rgt } => {
-        self.visit_tree(lft);
-        self.visit_tree(rgt);
-      }
+      tree.children().for_each(|child| self.visit_tree(child))
     })
   }
   fn visit_net(&mut self, net: &Net) {
@@ -147,7 +143,7 @@ impl<'a> State<'a> {
     let net = self.host.readback(&mut rt);
 
     // Mutate the host in-place with the pre-reduced net.
-    let instr = encode_def(&net, |nam| run::Port::new_ref(&self.host.defs[nam]));
+    let instr = self.host.encode_def(&net);
     if let DefRef::Owned(def_box) = self.host.defs.get_mut(nam).unwrap() {
       let interpreted_def: &mut crate::run::Def<InterpretedDef> = def_box.downcast_mut().unwrap();
       interpreted_def.data = instr;
diff --git a/src/util.rs b/src/util.rs
index 1e8e81cc..7090843d 100644
--- a/src/util.rs
+++ b/src/util.rs
@@ -1,4 +1,5 @@
 mod apply_tree;
+pub(crate) mod array_vec;
 mod bi_enum;
 mod create_var;
 mod deref;
diff --git a/src/util/apply_tree.rs b/src/util/apply_tree.rs
index bb7a68ab..61dd221e 100644
--- a/src/util/apply_tree.rs
+++ b/src/util/apply_tree.rs
@@ -16,7 +16,7 @@ impl Net {
     let fresh_str = create_var(fresh + 1);
 
     let fun = core::mem::take(&mut self.root);
-    let app = Tree::Ctr { lab: 0, lft: Box::new(arg), rgt: Box::new(Tree::Var { nam: fresh_str.clone() }) };
+    let app = Tree::Ctr { lab: 0, ports: vec![arg, Tree::Var { nam: fresh_str.clone() }] };
     self.root = Tree::Var { nam: fresh_str };
     self.redexes.push((fun, app));
   }
@@ -37,18 +37,11 @@ impl Tree {
   /// This function can be called multiple times with many trees to
   /// ensure that `fresh` does not conflict with any of them.
   pub(crate) fn ensure_no_conflicts(&self, fresh: &mut usize) {
-    match self {
-      Tree::Var { nam } => {
-        if let Some(var_num) = var_to_num(nam) {
-          *fresh = (*fresh).max(var_num);
-        }
+    if let Tree::Var { nam } = self {
+      if let Some(var_num) = var_to_num(nam) {
+        *fresh = (*fresh).max(var_num);
       }
-      // Recurse on children
-      Tree::Ctr { lft, rgt, .. } | Tree::Op { rhs: lft, out: rgt, .. } | Tree::Mat { sel: lft, ret: rgt } => {
-        lft.ensure_no_conflicts(fresh);
-        rgt.ensure_no_conflicts(fresh);
-      }
-      Tree::Era | Tree::Num { .. } | Tree::Ref { .. } => {}
     }
+    self.children().for_each(|child| child.ensure_no_conflicts(fresh));
   }
 }
diff --git a/src/util/array_vec.rs b/src/util/array_vec.rs
new file mode 100644
index 00000000..824f5212
--- /dev/null
+++ b/src/util/array_vec.rs
@@ -0,0 +1,29 @@
+use arrayvec::ArrayVec;
+
+struct Assert<const COND: bool>;
+
+trait IsTrue {}
+
+impl IsTrue for Assert<true> {}
+
+#[allow(private_bounds)]
+pub(crate) fn from_array<T, const LEN: usize, const CAP: usize>(array: [T; LEN]) -> ArrayVec<T, CAP>
+where
+  Assert<{ LEN <= CAP }>: IsTrue,
+{
+  let mut vec = ArrayVec::new();
+  unsafe {
+    for el in array {
+      vec.push_unchecked(el)
+    }
+  }
+  vec
+}
+
+pub(crate) fn from_iter<T, const CAP: usize>(iter: impl IntoIterator<Item = T>) -> ArrayVec<T, CAP> {
+  let mut vec = ArrayVec::new();
+  for item in iter {
+    vec.push(item);
+  }
+  vec
+}
diff --git a/tests/programs/chained_ops.hvmc b/tests/programs/chained_ops.hvmc
index 37f0baf1..bd32fd58 100644
--- a/tests/programs/chained_ops.hvmc
+++ b/tests/programs/chained_ops.hvmc
@@ -1,5 +1,5 @@
 @main = a
-& ({3 <* b <- c <* d e>>> {5 <* f <- #20 g>> h}} ({7 i {9 j k}} e)) ~ (#70 (#50 a))
+& ({3 <* b <- c <* d e>>> {3 <* f <- #20 g>> h}} ({5 i {5 j k}} e)) ~ (#70 (#50 a))
 & #70 ~ <* k l>
 & #80 ~ <+ l m>
 & #10 ~ <* m <+ n d>>
diff --git a/tests/programs/church_mul.hvmc b/tests/programs/church_mul.hvmc
index bab1582b..e0ee62f9 100644
--- a/tests/programs/church_mul.hvmc
+++ b/tests/programs/church_mul.hvmc
@@ -1,4 +1,4 @@
-@C_20 = ({3 (a b) {5 (c a) {7 (d c) {9 (e d) {11 (f e) {13 (g f) {15 (h g) {17 (i h) {19 (j i) {21 (k j) {23 (l k) {25 (m l) {27 (n m) {29 (o n) {31 (p o) {33 (q p) {35 (r q) {37 (s r) {39 (t s) (u t)}}}}}}}}}}}}}}}}}}} (u b))
+@C_20 = ({3 (a b) {3 (c a) {3 (d c) {3 (e d) {3 (f e) {3 (g f) {3 (h g) {3 (i h) {3 (j i) {3 (k j) {3 (l k) {3 (m l) {3 (n m) {3 (o n) {3 (p o) {3 (q p) {3 (r q) {3 (s r) {3 (t s) (u t)}}}}}}}}}}}}}}}}}}} (u b))
 @Mult = ((a (b c)) ((d a) (d (b c))))
 @main = a
 & @Mult ~ (@C_20 (@C_20 a))
diff --git a/tests/programs/heavy_pre_reduction.hvmc b/tests/programs/heavy_pre_reduction.hvmc
index 7dbb0b07..41c42cb3 100644
--- a/tests/programs/heavy_pre_reduction.hvmc
+++ b/tests/programs/heavy_pre_reduction.hvmc
@@ -1,8 +1,8 @@
 @C1 = ((a b) (a b))
 @C2 = ({3 (a b) (c a)} (c b))
-@C3 = ({21 (a b) {23 (c a) (d c)}} (d b))
-@C4 = ({15 (a b) {17 (c a) {19 (d c) (e d)}}} (e b))
-@C6 = ({5 (a b) {7 (c a) {9 (d c) {11 (e d) {13 (f e) (g f)}}}}} (g b))
+@C3 = ({9 (a b) {9 (c a) (d c)}} (d b))
+@C4 = ({7 (a b) {7 (c a) {7 (d c) (e d)}}} (e b))
+@C6 = ({5 (a b) {5 (c a) {5 (d c) {5 (e d) {5 (f e) (g f)}}}}} (g b))
 @black_plus = a
 & @HVM.black_box ~ (@plus a)
 @erase = ((@HVM.black_box (a b)) (a b))
@@ -16,12 +16,12 @@
 & @fib ~ (b a)
 & @C4 ~ (@C2 b)
 @fib = ((@fib$S0 ([@C1 @C1] [* a])) a)
-@fib$S0 = ([a {27 b c}] [b d])
+@fib$S0 = ([a {13 b c}] [b d])
 & @plus ~ (a (c d))
 @main = *
 @main_fast = a
 & @black_plus ~ (@expensive (@expensive a))
 @main_slow = a
 & @black_plus ~ (@expensive_1 (@expensive_2 a))
-@plus = ((a (b c)) ((d (e b)) ({25 a d} (e c))))
+@plus = ((a (b c)) ((d (e b)) ({11 a d} (e c))))
 
diff --git a/tests/programs/stress_tests/all_tree.hvmc b/tests/programs/stress_tests/all_tree.hvmc
index 6d040190..1a2aa747 100644
--- a/tests/programs/stress_tests/all_tree.hvmc
+++ b/tests/programs/stress_tests/all_tree.hvmc
@@ -9,8 +9,9 @@
 & @all ~ (a d)
 @and = (((a a) (@and$S0 b)) b)
 @and$S0 = (* @False)
-@gen = (?<(a @gen$S0) b> b)
-& @Leaf ~ (@True a)
+@gen = (?<(a b) d> d)
+& (a b) ~ (c @gen$S0)
+& @Leaf ~ (@True c)
 @gen$S0 = ({3 a b} c)
 & @Node ~ (d (e c))
 & @gen ~ (b e)
diff --git a/tests/programs/stress_tests/apelacion.hvmc b/tests/programs/stress_tests/apelacion.hvmc
index db6b16ee..c6d242fb 100644
--- a/tests/programs/stress_tests/apelacion.hvmc
+++ b/tests/programs/stress_tests/apelacion.hvmc
@@ -1,11 +1,13 @@
 @main = a
 & @rec ~ (#6 a)
-@rec = (?<(a @rec$S0) b> b)
-& @sum ~ (#1000000 (#0 a))
+@rec = (?<(a b) d> d)
+& (a b) ~ (c @rec$S0)
+& @sum ~ (#1000000 (#0 c))
 @rec$S0 = ({5 a b} c)
 & @rec ~ (a <+ d c>)
 & @rec ~ (b d)
-@sum = (?<((a a) @sum$S0) b> b)
+@sum = (?<(a b) d> d)
+& (a b) ~ ((c c) @sum$S0)
 @sum$S0 = ({3 a <+ b c>} (b d))
 & @sum ~ (a (c d))
 
diff --git a/tests/programs/stress_tests/fib_rec.hvmc b/tests/programs/stress_tests/fib_rec.hvmc
index 63d81e94..f3d8e058 100644
--- a/tests/programs/stress_tests/fib_rec.hvmc
+++ b/tests/programs/stress_tests/fib_rec.hvmc
@@ -1,10 +1,12 @@
 @add = (<+ a b> (a b))
-@fib = (?<(#1 @fib$S2) a> a)
+@fib = (?<(a b) c> c)
+& (a b) ~ (#1 @fib$S2)
 @fib$S0 = (* #1)
 @fib$S1 = (a (b c))
 & @fib ~ (b <+ d c>)
 & @fib ~ (a d)
-@fib$S2 = ({3 ?<(@fib$S0 @fib$S1) (a b)> a} b)
+@fib$S2 = ({3 ?<(a b) (c d)> c} d)
+& (a b) ~ (@fib$S0 @fib$S1)
 @main = a
 & @fib ~ (#30 a)
 
diff --git a/tests/programs/stress_tests/sum_rec.hvmc b/tests/programs/stress_tests/sum_rec.hvmc
index c518ac5f..960b33ae 100644
--- a/tests/programs/stress_tests/sum_rec.hvmc
+++ b/tests/programs/stress_tests/sum_rec.hvmc
@@ -1,7 +1,8 @@
 @add = (<+ a b> (a b))
 @main = a
 & @sum ~ (#26 a)
-@sum = (?<(#1 @sum$S0) a> a)
+@sum = (?<(a b) c> c)
+& (a b) ~ (#1 @sum$S0)
 @sum$S0 = ({3 a b} c)
 & @add ~ (d (e c))
 & @sum ~ (b e)
diff --git a/tests/programs/stress_tests/sum_tail.hvmc b/tests/programs/stress_tests/sum_tail.hvmc
index ac5ac281..d87e3e59 100644
--- a/tests/programs/stress_tests/sum_tail.hvmc
+++ b/tests/programs/stress_tests/sum_tail.hvmc
@@ -1,6 +1,7 @@
 @main = a
 & @sum ~ (#10000000 (#0 a))
-@sum = (?<((a a) @sum$S0) b> b)
+@sum = (?<(a b) d> d)
+& (a b) ~ ((c c) @sum$S0)
 @sum$S0 = ({3 a <+ b c>} (b d))
 & @sum ~ (a (c d))
 
diff --git a/tests/programs/stress_tests/sum_tree.hvmc b/tests/programs/stress_tests/sum_tree.hvmc
index bbeb8756..2efcd423 100644
--- a/tests/programs/stress_tests/sum_tree.hvmc
+++ b/tests/programs/stress_tests/sum_tree.hvmc
@@ -1,8 +1,9 @@
 @Leaf = (a ((a b) (* b)))
 @Node = (a (b (* ((a (b c)) c))))
 @add = (<+ a b> (a b))
-@gen = (?<(a @gen$S0) b> b)
-& @Leaf ~ (#1 a)
+@gen = (?<(a b) d> d)
+& (a b) ~ (c @gen$S0)
+& @Leaf ~ (#1 c)
 @gen$S0 = ({3 a b} c)
 & @Node ~ (d (e c))
 & @gen ~ (b e)
diff --git a/tests/programs/stress_tests/tuple_rots.hvmc b/tests/programs/stress_tests/tuple_rots.hvmc
index 45b34173..38226b5c 100644
--- a/tests/programs/stress_tests/tuple_rots.hvmc
+++ b/tests/programs/stress_tests/tuple_rots.hvmc
@@ -1,5 +1,6 @@
 @MkTup8 = (a (b (c (d (e (f (g (h ((a (b (c (d (e (f (g (h i)))))))) i)))))))))
-@app = (?<(@app$S0 @app$S1) a> a)
+@app = (?<(a b) c> c)
+& (a b) ~ (@app$S0 @app$S1)
 @app$S0 = (* (a a))
 @app$S1 = (a ({3 b (c d)} (c e)))
 & @app ~ (a (b (d e)))
diff --git a/tests/snapshots/tests__pre_reduce_run@church_encoding__church.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@church_encoding__church.hvmc.snap
index b8effcda..8a38229c 100644
--- a/tests/snapshots/tests__pre_reduce_run@church_encoding__church.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@church_encoding__church.hvmc.snap
@@ -3,7 +3,7 @@ source: tests/tests.rs
 expression: output
 input_file: examples/church_encoding/church.hvmc
 ---
-({11 {7 (a {5 b c}) {9 (d a) ({5 c e} d)}} {3 (f e) {3 (g f) {3 (h g) {3 (i h) *}}}}} (i b))
+({9 {7 (a {5 b c}) {7 (d a) ({5 c e} d)}} {3 (f e) {3 (g f) {3 (h g) {3 (i h) *}}}}} (i b))
 pre-reduce:
 RWTS   :              44
 - ANNI :              25
diff --git a/tests/snapshots/tests__pre_reduce_run@church_mul.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@church_mul.hvmc.snap
index d744e724..a05b16e1 100644
--- a/tests/snapshots/tests__pre_reduce_run@church_mul.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@church_mul.hvmc.snap
@@ -3,7 +3,7 @@ source: tests/tests.rs
 expression: output
 input_file: tests/programs/church_mul.hvmc
 ---
-({3 (a {3 b {5 c {7 d {9 e {11 f {13 g {15 h {17 i {19 j {21 k {23 l {25 m {27 n {29 o {31 p {33 q {35 r {37 s {39 t u}}}}}}}}}}}}}}}}}}}) {5 (v a) {7 (w v) {9 (x w) {11 (y x) {13 (z y) {15 (aa z) {17 (ab aa) {19 (ac ab) {21 (ad ac) {23 (ae ad) {25 (af ae) {27 (ag af) {29 (ah ag) {31 (ai ah) {33 (aj ai) {35 (ak aj) {37 (al ak) {39 (am al) ({3 c {5 d {7 e {9 f {11 g {13 h {15 i {17 j {19 k {21 l {23 m {25 n {27 o {29 p {31 q {33 r {35 s {37 t {39 u an}}}}}}}}}}}}}}}}}}} am)}}}}}}}}}}}}}}}}}}} (an b))
+({3 (a {3 b {3 c {3 d {3 e {3 f {3 g {3 h {3 i {3 j {3 k {3 l {3 m {3 n {3 o {3 p {3 q {3 r {3 s {3 t u}}}}}}}}}}}}}}}}}}}) {3 (v a) {3 (w v) {3 (x w) {3 (y x) {3 (z y) {3 (aa z) {3 (ab aa) {3 (ac ab) {3 (ad ac) {3 (ae ad) {3 (af ae) {3 (ag af) {3 (ah ag) {3 (ai ah) {3 (aj ai) {3 (ak aj) {3 (al ak) {3 (am al) ({3 c {3 d {3 e {3 f {3 g {3 h {3 i {3 j {3 k {3 l {3 m {3 n {3 o {3 p {3 q {3 r {3 s {3 t {3 u an}}}}}}}}}}}}}}}}}}} am)}}}}}}}}}}}}}}}}}}} (an b))
 pre-reduce:
 RWTS   :              50
 - ANNI :              25
diff --git a/tests/snapshots/tests__pre_reduce_run@machine_u32__num_match.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@machine_u32__num_match.hvmc.snap
index 5821d4c9..cbeb479e 100644
--- a/tests/snapshots/tests__pre_reduce_run@machine_u32__num_match.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@machine_u32__num_match.hvmc.snap
@@ -5,8 +5,8 @@ input_file: examples/machine_u32/num_match.hvmc
 ---
 #9
 pre-reduce:
-RWTS   :               8
-- ANNI :               3
+RWTS   :               9
+- ANNI :               4
 - COMM :               0
 - ERAS :               1
 - DREF :               3
diff --git a/tests/snapshots/tests__pre_reduce_run@sort__bitonic__bitonic_sort_lam.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@sort__bitonic__bitonic_sort_lam.hvmc.snap
index e4ef59b1..33657a5b 100644
--- a/tests/snapshots/tests__pre_reduce_run@sort__bitonic__bitonic_sort_lam.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@sort__bitonic__bitonic_sort_lam.hvmc.snap
@@ -5,8 +5,8 @@ input_file: examples/sort/bitonic/bitonic_sort_lam.hvmc
 ---
 #523776
 pre-reduce:
-RWTS   :       1_563_230
-- ANNI :         944_667
+RWTS   :       1_563_234
+- ANNI :         944_671
 - COMM :          96_766
 - ERAS :         221_692
 - DREF :         209_486
diff --git a/tests/snapshots/tests__pre_reduce_run@sort__merge__merge_sort.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@sort__merge__merge_sort.hvmc.snap
index f110d205..71665a19 100644
--- a/tests/snapshots/tests__pre_reduce_run@sort__merge__merge_sort.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@sort__merge__merge_sort.hvmc.snap
@@ -3,10 +3,10 @@ source: tests/tests.rs
 expression: output
 input_file: examples/sort/merge/merge_sort.hvmc
 ---
-{8 * {8 {14 {8 * {8 {14 {8 {10 #3 a} {8 * a}} {12 {8 {10 #2 b} {8 * b}} c}} c}} {12 {8 * {8 {14 {8 {10 #1 d} {8 * d}} {12 {8 {10 #0 e} {8 * e}} f}} f}} g}} g}}
+{4 * {4 {4 {4 * {4 {4 {4 {4 #3 a} {4 * a}} {4 {4 {4 #2 b} {4 * b}} c}} c}} {4 {4 * {4 {4 {4 {4 #1 d} {4 * d}} {4 {4 {4 #0 e} {4 * e}} f}} f}} g}} g}}
 pre-reduce:
-RWTS   :             445
-- ANNI :              65
+RWTS   :             449
+- ANNI :              69
 - COMM :             242
 - ERAS :              79
 - DREF :              43
diff --git a/tests/snapshots/tests__pre_reduce_run@sort__radix__radix_sort_lam.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@sort__radix__radix_sort_lam.hvmc.snap
index 6fdd1da1..739b3419 100644
--- a/tests/snapshots/tests__pre_reduce_run@sort__radix__radix_sort_lam.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@sort__radix__radix_sort_lam.hvmc.snap
@@ -5,8 +5,8 @@ input_file: examples/sort/radix/radix_sort_lam.hvmc
 ---
 #549755289600
 pre-reduce:
-RWTS   :   1_134_559_381
-- ANNI :     622_854_182
+RWTS   :   1_134_559_385
+- ANNI :     622_854_186
 - COMM :      28_311_560
 - ERAS :     251_658_239
 - DREF :     171_966_556
diff --git a/tests/snapshots/tests__pre_reduce_run@stress_tests__all_tree.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@stress_tests__all_tree.hvmc.snap
index 889ea2cf..dd26fd83 100644
--- a/tests/snapshots/tests__pre_reduce_run@stress_tests__all_tree.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@stress_tests__all_tree.hvmc.snap
@@ -5,8 +5,8 @@ input_file: tests/programs/stress_tests/all_tree.hvmc
 ---
 (a (* a))
 pre-reduce:
-RWTS   :     503_316_491
-- ANNI :     218_103_811
+RWTS   :     503_316_494
+- ANNI :     218_103_814
 - COMM :      83_886_075
 - ERAS :     117_440_507
 - DREF :      50_331_667
diff --git a/tests/snapshots/tests__pre_reduce_run@stress_tests__apelacion.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@stress_tests__apelacion.hvmc.snap
index 641b305b..3529be08 100644
--- a/tests/snapshots/tests__pre_reduce_run@stress_tests__apelacion.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@stress_tests__apelacion.hvmc.snap
@@ -5,8 +5,8 @@ input_file: tests/programs/stress_tests/apelacion.hvmc
 ---
 #31999968000000
 pre-reduce:
-RWTS   :      31_000_664
-- ANNI :      11_000_203
+RWTS   :      33_000_671
+- ANNI :      13_000_210
 - COMM :       6_000_063
 - ERAS :       3_000_130
 - DREF :       5_000_075
diff --git a/tests/snapshots/tests__pre_reduce_run@stress_tests__fib_rec.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@stress_tests__fib_rec.hvmc.snap
index e2607543..2327080f 100644
--- a/tests/snapshots/tests__pre_reduce_run@stress_tests__fib_rec.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@stress_tests__fib_rec.hvmc.snap
@@ -5,8 +5,8 @@ input_file: tests/programs/stress_tests/fib_rec.hvmc
 ---
 #1346269
 pre-reduce:
-RWTS   :      29_028_663
-- ANNI :      10_573_732
+RWTS   :      29_028_667
+- ANNI :      10_573_736
 - COMM :       2_178_308
 - ERAS :       5_702_885
 - DREF :       4_356_625
diff --git a/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_rec.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_rec.hvmc.snap
index c02969c7..37c59818 100644
--- a/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_rec.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_rec.hvmc.snap
@@ -5,8 +5,8 @@ input_file: tests/programs/stress_tests/sum_rec.hvmc
 ---
 #67108864
 pre-reduce:
-RWTS   :     671_088_646
-- ANNI :     201_326_595
+RWTS   :     671_088_649
+- ANNI :     201_326_598
 - COMM :      67_108_863
 - ERAS :     134_217_727
 - DREF :      67_108_871
diff --git a/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_tail.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_tail.hvmc.snap
index 6fa705ce..455da6de 100644
--- a/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_tail.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_tail.hvmc.snap
@@ -5,8 +5,8 @@ input_file: tests/programs/stress_tests/sum_tail.hvmc
 ---
 #49999995000000
 pre-reduce:
-RWTS   :      90_000_011
-- ANNI :      30_000_004
+RWTS   :      90_000_013
+- ANNI :      30_000_006
 - COMM :      20_000_000
 - ERAS :      10_000_001
 - DREF :      10_000_005
diff --git a/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_tree.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_tree.hvmc.snap
index 302b4c95..76839269 100644
--- a/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_tree.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@stress_tests__sum_tree.hvmc.snap
@@ -5,8 +5,8 @@ input_file: tests/programs/stress_tests/sum_tree.hvmc
 ---
 #16777216
 pre-reduce:
-RWTS   :     436_207_629
-- ANNI :     167_772_167
+RWTS   :     436_207_632
+- ANNI :     167_772_170
 - COMM :      83_886_075
 - ERAS :     100_663_292
 - DREF :      33_554_449
diff --git a/tests/snapshots/tests__pre_reduce_run@stress_tests__tuple_rots.hvmc.snap b/tests/snapshots/tests__pre_reduce_run@stress_tests__tuple_rots.hvmc.snap
index 91e2d6b1..92038d46 100644
--- a/tests/snapshots/tests__pre_reduce_run@stress_tests__tuple_rots.hvmc.snap
+++ b/tests/snapshots/tests__pre_reduce_run@stress_tests__tuple_rots.hvmc.snap
@@ -5,8 +5,8 @@ input_file: tests/programs/stress_tests/tuple_rots.hvmc
 ---
 ((#1 (#2 (#3 (#4 (#5 (#6 (#7 (#8 a)))))))) a)
 pre-reduce:
-RWTS   :      40_000_036
-- ANNI :      28_000_021
+RWTS   :      40_000_038
+- ANNI :      28_000_023
 - COMM :       2_000_000
 - ERAS :       2_000_002
 - DREF :       6_000_012
diff --git a/tests/snapshots/tests__run@church_encoding__church.hvmc.snap b/tests/snapshots/tests__run@church_encoding__church.hvmc.snap
index 9ae4b357..44ba320a 100644
--- a/tests/snapshots/tests__run@church_encoding__church.hvmc.snap
+++ b/tests/snapshots/tests__run@church_encoding__church.hvmc.snap
@@ -3,7 +3,7 @@ source: tests/tests.rs
 expression: output
 input_file: examples/church_encoding/church.hvmc
 ---
-({11 {7 (a {5 b c}) {9 (d a) ({5 c e} d)}} {3 (f e) {3 (g f) {3 (h g) {3 (i h) *}}}}} (i b))
+({9 {7 (a {5 b c}) {7 (d a) ({5 c e} d)}} {3 (f e) {3 (g f) {3 (h g) {3 (i h) *}}}}} (i b))
 RWTS   :              65
 - ANNI :              25
 - COMM :               1
diff --git a/tests/snapshots/tests__run@church_mul.hvmc.snap b/tests/snapshots/tests__run@church_mul.hvmc.snap
index 37a8caeb..27e41100 100644
--- a/tests/snapshots/tests__run@church_mul.hvmc.snap
+++ b/tests/snapshots/tests__run@church_mul.hvmc.snap
@@ -3,7 +3,7 @@ source: tests/tests.rs
 expression: output
 input_file: tests/programs/church_mul.hvmc
 ---
-({3 (a {3 b {5 c {7 d {9 e {11 f {13 g {15 h {17 i {19 j {21 k {23 l {25 m {27 n {29 o {31 p {33 q {35 r {37 s {39 t u}}}}}}}}}}}}}}}}}}}) {5 (v a) {7 (w v) {9 (x w) {11 (y x) {13 (z y) {15 (aa z) {17 (ab aa) {19 (ac ab) {21 (ad ac) {23 (ae ad) {25 (af ae) {27 (ag af) {29 (ah ag) {31 (ai ah) {33 (aj ai) {35 (ak aj) {37 (al ak) {39 (am al) ({3 c {5 d {7 e {9 f {11 g {13 h {15 i {17 j {19 k {21 l {23 m {25 n {27 o {29 p {31 q {33 r {35 s {37 t {39 u an}}}}}}}}}}}}}}}}}}} am)}}}}}}}}}}}}}}}}}}} (an b))
+({3 (a {3 b {3 c {3 d {3 e {3 f {3 g {3 h {3 i {3 j {3 k {3 l {3 m {3 n {3 o {3 p {3 q {3 r {3 s {3 t u}}}}}}}}}}}}}}}}}}}) {3 (v a) {3 (w v) {3 (x w) {3 (y x) {3 (z y) {3 (aa z) {3 (ab aa) {3 (ac ab) {3 (ad ac) {3 (ae ad) {3 (af ae) {3 (ag af) {3 (ah ag) {3 (ai ah) {3 (aj ai) {3 (ak aj) {3 (al ak) {3 (am al) ({3 c {3 d {3 e {3 f {3 g {3 h {3 i {3 j {3 k {3 l {3 m {3 n {3 o {3 p {3 q {3 r {3 s {3 t {3 u an}}}}}}}}}}}}}}}}}}} am)}}}}}}}}}}}}}}}}}}} (an b))
 RWTS   :             167
 - ANNI :              25
 - COMM :              19
diff --git a/tests/snapshots/tests__run@machine_u32__num_match.hvmc.snap b/tests/snapshots/tests__run@machine_u32__num_match.hvmc.snap
index da9a068e..0ff6b67b 100644
--- a/tests/snapshots/tests__run@machine_u32__num_match.hvmc.snap
+++ b/tests/snapshots/tests__run@machine_u32__num_match.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: examples/machine_u32/num_match.hvmc
 ---
 #9
-RWTS   :               8
-- ANNI :               3
+RWTS   :               9
+- ANNI :               4
 - COMM :               0
 - ERAS :               1
 - DREF :               3
diff --git a/tests/snapshots/tests__run@sort__bitonic__bitonic_sort_lam.hvmc.snap b/tests/snapshots/tests__run@sort__bitonic__bitonic_sort_lam.hvmc.snap
index cf2b4c81..98df337d 100644
--- a/tests/snapshots/tests__run@sort__bitonic__bitonic_sort_lam.hvmc.snap
+++ b/tests/snapshots/tests__run@sort__bitonic__bitonic_sort_lam.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: examples/sort/bitonic/bitonic_sort_lam.hvmc
 ---
 #523776
-RWTS   :       2_263_483
-- ANNI :       1_344_981
+RWTS   :       2_293_690
+- ANNI :       1_375_188
 - COMM :          96_766
 - ERAS :         222_714
 - DREF :         508_403
diff --git a/tests/snapshots/tests__run@sort__merge__merge_sort.hvmc.snap b/tests/snapshots/tests__run@sort__merge__merge_sort.hvmc.snap
index af262be4..9e605d4f 100644
--- a/tests/snapshots/tests__run@sort__merge__merge_sort.hvmc.snap
+++ b/tests/snapshots/tests__run@sort__merge__merge_sort.hvmc.snap
@@ -3,9 +3,9 @@ source: tests/tests.rs
 expression: output
 input_file: examples/sort/merge/merge_sort.hvmc
 ---
-{8 * {8 {14 {8 * {8 {14 {8 {10 #3 a} {8 * a}} {12 {8 {10 #2 b} {8 * b}} c}} c}} {12 {8 * {8 {14 {8 {10 #1 d} {8 * d}} {12 {8 {10 #0 e} {8 * e}} f}} f}} g}} g}}
-RWTS   :             467
-- ANNI :              64
+{4 * {4 {4 {4 * {4 {4 {4 {4 #3 a} {4 * a}} {4 {4 {4 #2 b} {4 * b}} c}} c}} {4 {4 * {4 {4 {4 {4 #1 d} {4 * d}} {4 {4 {4 #0 e} {4 * e}} f}} f}} g}} g}}
+RWTS   :             474
+- ANNI :              71
 - COMM :             242
 - ERAS :              79
 - DREF :              66
diff --git a/tests/snapshots/tests__run@sort__radix__radix_sort_lam.hvmc.snap b/tests/snapshots/tests__run@sort__radix__radix_sort_lam.hvmc.snap
index ef27fa11..d428deb2 100644
--- a/tests/snapshots/tests__run@sort__radix__radix_sort_lam.hvmc.snap
+++ b/tests/snapshots/tests__run@sort__radix__radix_sort_lam.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: examples/sort/radix/radix_sort_lam.hvmc
 ---
 #549755289600
-RWTS   :   1_473_249_271
-- ANNI :     818_937_828
+RWTS   :   1_500_512_246
+- ANNI :     846_200_803
 - COMM :      28_311_560
 - ERAS :     251_658_239
 - DREF :     314_572_800
diff --git a/tests/snapshots/tests__run@stress_tests__all_tree.hvmc.snap b/tests/snapshots/tests__run@stress_tests__all_tree.hvmc.snap
index 472fcd0f..80fa0a99 100644
--- a/tests/snapshots/tests__run@stress_tests__all_tree.hvmc.snap
+++ b/tests/snapshots/tests__run@stress_tests__all_tree.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: tests/programs/stress_tests/all_tree.hvmc
 ---
 (a (* a))
-RWTS   :     788_529_125
-- ANNI :     369_098_737
+RWTS   :     822_083_556
+- ANNI :     402_653_168
 - COMM :      83_886_075
 - ERAS :     117_440_507
 - DREF :     184_549_375
diff --git a/tests/snapshots/tests__run@stress_tests__apelacion.hvmc.snap b/tests/snapshots/tests__run@stress_tests__apelacion.hvmc.snap
index 4e5acb9b..53b685ba 100644
--- a/tests/snapshots/tests__run@stress_tests__apelacion.hvmc.snap
+++ b/tests/snapshots/tests__run@stress_tests__apelacion.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: tests/programs/stress_tests/apelacion.hvmc
 ---
 #31999968000000
-RWTS   :   1_397_001_651
-- ANNI :     508_000_698
+RWTS   :   1_524_001_905
+- ANNI :     635_000_952
 - COMM :     254_000_063
 - ERAS :     127_000_254
 - DREF :     254_000_319
diff --git a/tests/snapshots/tests__run@stress_tests__fib_rec.hvmc.snap b/tests/snapshots/tests__run@stress_tests__fib_rec.hvmc.snap
index fbc174a9..69cc04c1 100644
--- a/tests/snapshots/tests__run@stress_tests__fib_rec.hvmc.snap
+++ b/tests/snapshots/tests__run@stress_tests__fib_rec.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: tests/programs/stress_tests/fib_rec.hvmc
 ---
 #1346269
-RWTS   :      34_413_727
-- ANNI :      13_266_266
+RWTS   :      39_284_572
+- ANNI :      18_137_111
 - COMM :       2_178_308
 - ERAS :       5_702_885
 - DREF :       7_049_155
diff --git a/tests/snapshots/tests__run@stress_tests__sum_rec.hvmc.snap b/tests/snapshots/tests__run@stress_tests__sum_rec.hvmc.snap
index 08e2d81e..ed9ce843 100644
--- a/tests/snapshots/tests__run@stress_tests__sum_rec.hvmc.snap
+++ b/tests/snapshots/tests__run@stress_tests__sum_rec.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: tests/programs/stress_tests/sum_rec.hvmc
 ---
 #67108864
-RWTS   :   1_140_850_678
-- ANNI :     469_762_043
+RWTS   :   1_275_068_405
+- ANNI :     603_979_770
 - COMM :      67_108_863
 - ERAS :     134_217_727
 - DREF :     268_435_455
diff --git a/tests/snapshots/tests__run@stress_tests__sum_tail.hvmc.snap b/tests/snapshots/tests__run@stress_tests__sum_tail.hvmc.snap
index 75b78d11..fe9d3bb5 100644
--- a/tests/snapshots/tests__run@stress_tests__sum_tail.hvmc.snap
+++ b/tests/snapshots/tests__run@stress_tests__sum_tail.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: tests/programs/stress_tests/sum_tail.hvmc
 ---
 #49999995000000
-RWTS   :     110_000_008
-- ANNI :      40_000_003
+RWTS   :     120_000_009
+- ANNI :      50_000_004
 - COMM :      20_000_000
 - ERAS :      10_000_001
 - DREF :      20_000_003
diff --git a/tests/snapshots/tests__run@stress_tests__sum_tree.hvmc.snap b/tests/snapshots/tests__run@stress_tests__sum_tree.hvmc.snap
index df3e28cf..3eb1fdd8 100644
--- a/tests/snapshots/tests__run@stress_tests__sum_tree.hvmc.snap
+++ b/tests/snapshots/tests__run@stress_tests__sum_tree.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: tests/programs/stress_tests/sum_tree.hvmc
 ---
 #16777216
-RWTS   :     738_197_475
-- ANNI :     335_544_307
+RWTS   :     771_751_906
+- ANNI :     369_098_738
 - COMM :      83_886_075
 - ERAS :     100_663_292
 - DREF :     167_772_155
diff --git a/tests/snapshots/tests__run@stress_tests__tuple_rots.hvmc.snap b/tests/snapshots/tests__run@stress_tests__tuple_rots.hvmc.snap
index 9e061352..e1c0486c 100644
--- a/tests/snapshots/tests__run@stress_tests__tuple_rots.hvmc.snap
+++ b/tests/snapshots/tests__run@stress_tests__tuple_rots.hvmc.snap
@@ -4,8 +4,8 @@ expression: output
 input_file: tests/programs/stress_tests/tuple_rots.hvmc
 ---
 ((#1 (#2 (#3 (#4 (#5 (#6 (#7 (#8 a)))))))) a)
-RWTS   :      62_000_037
-- ANNI :      46_000_012
+RWTS   :      64_000_038
+- ANNI :      48_000_013
 - COMM :       2_000_000
 - ERAS :       2_000_002
 - DREF :      10_000_022
diff --git a/tests/transform.rs b/tests/transform.rs
index d3e289c1..22a2ed98 100644
--- a/tests/transform.rs
+++ b/tests/transform.rs
@@ -3,7 +3,7 @@
 pub mod loaders;
 
 use hvmc::util::show_rewrites;
-use insta::assert_snapshot;
+use insta::{assert_display_snapshot, assert_snapshot};
 use loaders::*;
 
 #[test]
@@ -36,3 +36,32 @@ pub fn test_fast_pre_reduce() {
   - OPER :               0
   "###)
 }
+
+#[test]
+pub fn test_adt_encoding() {
+  use hvmc::ast::{Net, Tree};
+  use std::str::FromStr;
+  pub fn parse_and_encode(net: &str) -> String {
+    let mut net = Net::from_str(net).unwrap();
+    println!("{net}");
+    net.trees_mut().for_each(Tree::coalesce_constructors);
+    println!("{net}");
+    net.trees_mut().for_each(Tree::encode_scott_adts);
+    format!("{net}")
+  }
+  assert_display_snapshot!(parse_and_encode("(a (b (c d)))"), @"(a b c d)");
+  assert_display_snapshot!(parse_and_encode("(a (b c (d e)))"), @"(a b c d e)");
+  assert_display_snapshot!(parse_and_encode("(a b c d e f g h)"), @"(a b c d e f g h)");
+  assert_display_snapshot!(parse_and_encode("(a b c d (e f g h (i j k l)))"), @"(a b c d (e f g h (i j k l)))");
+
+  assert_display_snapshot!(parse_and_encode("(* ((a R) R))"), @"(:1:2 a)");
+  assert_display_snapshot!(parse_and_encode("((a R) (* R))"), @"(:0:2 a)");
+  assert_display_snapshot!(parse_and_encode("(* (* ((a R) R)))"), @"(:2:3 a)");
+  assert_display_snapshot!(parse_and_encode("(* ((a R) (* R)))"), @"(:1:3 a)");
+  assert_display_snapshot!(parse_and_encode("((a (b R)) R)"), @"(:0:1 a b)");
+  assert_display_snapshot!(parse_and_encode("((a (b (c R))) R)"), @"(:0:1 a b c)");
+  assert_display_snapshot!(parse_and_encode("(* ((a (b (c R))) R))"), @"(:1:2 a b c)");
+  assert_display_snapshot!(parse_and_encode("{4 * {4 {4 a {4 b {4 c R}}} R}}"), @"{4:1:2 a b c}");
+  assert_display_snapshot!(parse_and_encode("(* x x)"), @"(:1:2)");
+  assert_display_snapshot!(parse_and_encode("(((((* x x) x) * x) x) * x)"), @"(:0:2 (:0:2 (:1:2)))");
+}