From cf69b99e5afe3d808c3b1d9580d89a6b93f1891f Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Mon, 18 Mar 2024 16:37:56 -0300
Subject: [PATCH 1/3] Add builtin and syntax sugar for Nats

---
 src/term/builtins.hvm                         |  3 +-
 src/term/builtins.rs                          | 10 +++++
 src/term/display.rs                           |  1 +
 src/term/mod.rs                               | 11 ++++++
 src/term/net_to_term.rs                       |  4 +-
 src/term/parser/parser.rs                     |  9 ++++-
 src/term/term_to_net.rs                       |  5 ++-
 src/term/transform/inline.rs                  |  4 +-
 src/term/transform/resugar_builtins.rs        | 37 ++++++++++++++++---
 tests/golden_tests/cli/debug_u60_to_nat.hvm   |  2 +-
 tests/golden_tests/run_file/nat_add.hvm       |  4 ++
 .../simplify_matches/already_flat.hvm         |  2 +-
 .../snapshots/cli__debug_u60_to_nat.hvm.snap  |  6 +--
 ...mpile_file_o_all__list_merge_sort.hvm.snap |  6 +--
 .../encode_pattern_match__common.hvm.snap     | 16 ++++----
 .../encode_pattern_match__expr.hvm.snap       | 16 ++++----
 tests/snapshots/run_file__nat_add.hvm.snap    |  9 +++++
 .../simplify_matches__already_flat.hvm.snap   |  4 +-
 18 files changed, 110 insertions(+), 39 deletions(-)
 create mode 100644 tests/golden_tests/run_file/nat_add.hvm
 create mode 100644 tests/snapshots/run_file__nat_add.hvm.snap

diff --git a/src/term/builtins.hvm b/src/term/builtins.hvm
index cede389c8..506d7dcba 100644
--- a/src/term/builtins.hvm
+++ b/src/term/builtins.hvm
@@ -1,3 +1,4 @@
 data String = (String.cons head tail) | (String.nil)
 data List   = (List.cons head tail) | (List.nil)
-data Result = (Result.ok val) | (Result.err val)
\ No newline at end of file
+data Result = (Result.ok val) | (Result.err val)
+data Nat    = (Nat.succ pred) | (Nat.zero)
diff --git a/src/term/builtins.rs b/src/term/builtins.rs
index fea2684c1..2d8f580b2 100644
--- a/src/term/builtins.rs
+++ b/src/term/builtins.rs
@@ -17,6 +17,10 @@ pub const RESULT: &str = "Result";
 pub const RESULT_OK: &str = "Result.ok";
 pub const RESULT_ERR: &str = "Result.err";
 
+pub const NAT: &str = "Nat";
+pub const NAT_SUCC: &str = "Nat.succ";
+pub const NAT_ZERO: &str = "Nat.zero";
+
 impl Book {
   pub fn builtins() -> Book {
     parse_book(BUILTINS, Book::default, true).expect("Error parsing builtin file, this should not happen")
@@ -37,6 +41,7 @@ impl Term {
     match self {
       Term::Lst { els } => *self = Term::encode_list(std::mem::take(els)),
       Term::Str { val } => *self = Term::encode_str(val),
+      Term::Nat { val } => *self = Term::encode_nat(*val),
       Term::Let { pat, val, nxt } => {
         pat.encode_builtins();
         val.encode_builtins();
@@ -87,6 +92,11 @@ impl Term {
       Term::call(Term::r#ref(SCONS), [Term::Num { val: u64::from(char) }, acc])
     })
   }
+
+  pub fn encode_nat(val: u64) -> Term {
+    (0 .. val).fold(Term::r#ref(NAT_ZERO), |acc, _| Term::app(Term::r#ref(NAT_SUCC), acc))
+  }
+
   pub fn encode_ok(val: Term) -> Term {
     Term::call(Term::r#ref(RESULT_OK), [val])
   }
diff --git a/src/term/display.rs b/src/term/display.rs
index e1d82a232..5dc647d3a 100644
--- a/src/term/display.rs
+++ b/src/term/display.rs
@@ -79,6 +79,7 @@ impl fmt::Display for Term {
       }
       Term::Era => write!(f, "*"),
       Term::Num { val } => write!(f, "{val}"),
+      Term::Nat { val } => write!(f, "#{val}"),
       Term::Str { val } => write!(f, "{val:?}"),
       Term::Opx { op, fst, snd } => {
         write!(f, "({} {} {})", op, fst, snd)
diff --git a/src/term/mod.rs b/src/term/mod.rs
index e6fc6fade..83bb70d20 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -122,6 +122,9 @@ pub enum Term {
   Num {
     val: u64,
   },
+  Nat {
+    val: u64,
+  },
   Str {
     val: GlobalString,
   },
@@ -316,6 +319,7 @@ impl Clone for Term {
       }
       Self::Sup { tag, els } => Self::Sup { tag: tag.clone(), els: els.clone() },
       Self::Num { val } => Self::Num { val: *val },
+      Self::Nat { val } => Self::Nat { val: *val },
       Self::Str { val } => Self::Str { val: val.clone() },
       Self::Lst { els } => Self::Lst { els: els.clone() },
       Self::Opx { op, fst, snd } => Self::Opx { op: *op, fst: fst.clone(), snd: snd.clone() },
@@ -464,6 +468,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -487,6 +492,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -531,6 +537,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -568,6 +575,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -607,6 +615,7 @@ impl Term {
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -631,6 +640,7 @@ impl Term {
       | Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
@@ -655,6 +665,7 @@ impl Term {
       | Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
+      | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
       | Term::Era
diff --git a/src/term/net_to_term.rs b/src/term/net_to_term.rs
index 8cd155c87..2f683a369 100644
--- a/src/term/net_to_term.rs
+++ b/src/term/net_to_term.rs
@@ -347,7 +347,7 @@ impl Term {
         }
         n
       }
-      Term::Lst { .. } => unreachable!(),
+      Term::Nat { .. } | Term::Lst { .. } => unreachable!(),
       Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Ref { .. } | Term::Era | Term::Err => 0,
     };
 
@@ -419,7 +419,7 @@ impl Term {
           rule.body.fix_names(id_counter, book);
         }
       }
-      Term::Let { .. } | Term::Use { .. } | Term::Lst { .. } => unreachable!(),
+      Term::Let { .. } | Term::Use { .. } | Term::Nat { .. } | Term::Lst { .. } => unreachable!(),
       Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {}
     }
   }
diff --git a/src/term/parser/parser.rs b/src/term/parser/parser.rs
index 3d731e553..bf5f92b28 100644
--- a/src/term/parser/parser.rs
+++ b/src/term/parser/parser.rs
@@ -207,6 +207,13 @@ where
     }),
   );
 
+  let nat = just(Token::Hash).ignore_then(select!(Token::Num(num) => Term::Nat { val: num }).or(
+    select!(Token::Error(LexingError::InvalidNumberLiteral) => ()).validate(|_, span, emit| {
+      emit.emit(Rich::custom(span, "found invalid nat literal expected number"));
+      Term::Nat { val: 0 }
+    }),
+  ));
+
   let term_sep = just(Token::Semicolon).or_not();
   let list_sep = just(Token::Comma).or_not();
 
@@ -359,7 +366,7 @@ where
       // OBS: `num_op` has to be before app, idk why?
       // OBS: `app` has to be before `tup` to not overflow on huge app terms
       // TODO: What happens on huge `tup` and other terms?
-      num_op, app, tup, global_var, var, number, list, str, chr, sup, global_lam, lam, dup, let_, use_,
+      num_op, app, tup, global_var, var, number, nat, list, str, chr, sup, global_lam, lam, dup, let_, use_,
       match_, era,
     ))
   })
diff --git a/src/term/term_to_net.rs b/src/term/term_to_net.rs
index 00ebd6de6..e68a29b6a 100644
--- a/src/term/term_to_net.rs
+++ b/src/term/term_to_net.rs
@@ -239,8 +239,9 @@ impl EncodeTermState<'_> {
           self.inet.link(Port(node, 1), Port(node, 2));
           Some(Port(node, 0))
         }
-        Term::Str { .. } => unreachable!(), // Removed in desugar str
-        Term::Lst { .. } => unreachable!(), // Removed in desugar list
+        Term::Nat { .. } => unreachable!(), // Removed in encode_nat
+        Term::Str { .. } => unreachable!(), // Removed in encode_str
+        Term::Lst { .. } => unreachable!(), // Removed in encode_list
         // core: & fst ~ <op snd ret>
         Term::Opx { op, fst, snd } => {
           let opx = self.inet.new_node(Op2 { opr: op.to_hvmc_label() });
diff --git a/src/term/transform/inline.rs b/src/term/transform/inline.rs
index 4c241c8dc..9b822d7c6 100644
--- a/src/term/transform/inline.rs
+++ b/src/term/transform/inline.rs
@@ -51,15 +51,15 @@ impl Term {
         },
 
         Term::Chn { .. } | Term::Lnk { .. } => false,
-        Term::Str { .. } | Term::Lst { .. } => false,
         Term::Let { .. } => false,
-        Term::Use { .. } => unreachable!(),
         Term::App { .. } => false,
         Term::Dup { .. } => false,
         Term::Opx { .. } => false,
         Term::Mat { .. } => false,
         Term::Ref { .. } => false,
 
+        Term::Nat { .. } | Term::Str { .. } | Term::Lst { .. } | Term::Use { .. } => unreachable!(),
+
         Term::Err => unreachable!(),
       })
     }
diff --git a/src/term/transform/resugar_builtins.rs b/src/term/transform/resugar_builtins.rs
index 92571b540..847e04e8c 100644
--- a/src/term/transform/resugar_builtins.rs
+++ b/src/term/transform/resugar_builtins.rs
@@ -1,14 +1,41 @@
-use crate::term::{Term, LCONS, LNIL, SCONS, SNIL};
+use crate::term::{Term, LCONS, LNIL, NAT_SUCC, NAT_ZERO, SCONS, SNIL};
 
 impl Term {
   pub fn resugar_builtins(&mut self) {
     self.resugar_strings();
+    self.resugar_nats();
     self.resugar_lists();
   }
 
+  pub fn resugar_nats(&mut self) {
+    Term::recursive_call(move || match self {
+      // (Nat.succ pred)
+      Term::App { fun: box Term::Ref { nam: ctr }, arg: box pred, .. } => {
+        pred.resugar_nats();
+
+        if ctr == NAT_SUCC {
+          if let Term::Nat { val } = pred {
+            *self = Term::Nat { val: *val + 1 };
+          } else {
+            let n = std::mem::take(pred);
+            *self = Term::call(Term::Ref { nam: ctr.clone() }, [n]);
+          }
+        }
+      }
+      // (Nat.zero)
+      Term::Ref { nam: def_name } if def_name == NAT_ZERO => *self = Term::Nat { val: 0 },
+
+      _ => {
+        for child in self.children_mut() {
+          child.resugar_nats();
+        }
+      }
+    });
+  }
+
   /// Rebuilds the String syntax sugar, converting `(Cons 97 Nil)` into `"a"`.
   pub fn resugar_strings(&mut self) {
-    match self {
+    Term::recursive_call(move || match self {
       // (String.cons Num tail)
       Term::App {
         fun: box Term::App { fun: box Term::Ref { nam: ctr }, arg: box head, .. },
@@ -48,12 +75,12 @@ impl Term {
           child.resugar_strings();
         }
       }
-    }
+    });
   }
 
   /// Rebuilds the List syntax sugar, converting `(Cons head Nil)` into `[head]`.
   pub fn resugar_lists(&mut self) {
-    match self {
+    Term::recursive_call(move || match self {
       // (List.cons el tail)
       Term::App {
         fun: box Term::App { fun: box Term::Ref { nam: ctr }, arg: box head, .. },
@@ -84,6 +111,6 @@ impl Term {
           child.resugar_lists();
         }
       }
-    }
+    });
   }
 }
diff --git a/tests/golden_tests/cli/debug_u60_to_nat.hvm b/tests/golden_tests/cli/debug_u60_to_nat.hvm
index 066ca8c8d..3bd4686e5 100644
--- a/tests/golden_tests/cli/debug_u60_to_nat.hvm
+++ b/tests/golden_tests/cli/debug_u60_to_nat.hvm
@@ -1,4 +1,4 @@
-data Nat = (Z) | (S nat)
+data Nat_ = (Z) | (S nat)
 
 (U60ToNat 0)   = Z
 (U60ToNat 1+p) = (S (U60ToNat p))
diff --git a/tests/golden_tests/run_file/nat_add.hvm b/tests/golden_tests/run_file/nat_add.hvm
new file mode 100644
index 000000000..974967212
--- /dev/null
+++ b/tests/golden_tests/run_file/nat_add.hvm
@@ -0,0 +1,4 @@
+(Nat.add (Nat.zero)   x) = x
+(Nat.add (Nat.succ p) x) = (Nat.succ (Nat.add p x))
+
+(Main) = (Nat.add #25 #9)
diff --git a/tests/golden_tests/simplify_matches/already_flat.hvm b/tests/golden_tests/simplify_matches/already_flat.hvm
index ca328fa63..cc84e99da 100644
--- a/tests/golden_tests/simplify_matches/already_flat.hvm
+++ b/tests/golden_tests/simplify_matches/already_flat.hvm
@@ -20,4 +20,4 @@ Rule5 (CtrA3 a) (CtrB3 b) = (a b)
 Rule5 a b = (a b)
 
 Rule6 a = a
-Rule6 b = b
\ No newline at end of file
+Rule6 b = b
diff --git a/tests/snapshots/cli__debug_u60_to_nat.hvm.snap b/tests/snapshots/cli__debug_u60_to_nat.hvm.snap
index fa90a4051..36579150e 100644
--- a/tests/snapshots/cli__debug_u60_to_nat.hvm.snap
+++ b/tests/snapshots/cli__debug_u60_to_nat.hvm.snap
@@ -24,10 +24,10 @@ input_file: tests/golden_tests/cli/debug_u60_to_nat.hvm
 ---------------------------------------
 (S (S (S (S Z))))
 ---------------------------------------
-(S (S (S #Nat λ* #Nat λa #Nat (a Z))))
+(S (S (S #Nat_ λ* #Nat_ λa #Nat_ (a Z))))
 ---------------------------------------
-(S (S #Nat λ* #Nat λa #Nat (a #Nat λ* #Nat λb #Nat (b Z))))
+(S (S #Nat_ λ* #Nat_ λa #Nat_ (a #Nat_ λ* #Nat_ λb #Nat_ (b Z))))
 ---------------------------------------
-(S #Nat λ* #Nat λa #Nat (a #Nat λ* #Nat λb #Nat (b #Nat λ* #Nat λc #Nat (c Z))))
+(S #Nat_ λ* #Nat_ λa #Nat_ (a #Nat_ λ* #Nat_ λb #Nat_ (b #Nat_ λ* #Nat_ λc #Nat_ (c Z))))
 ---------------------------------------
 (S (S (S (S Z))))
diff --git a/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap b/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap
index 1887b6f36..a39aaff85 100644
--- a/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap
@@ -6,19 +6,19 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 @If$C0 = (a (* a))
 @If$C1 = (* (a a))
 @Map = ({4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 a}} a)
-@Map$C0 = {4 a {4 {4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({5 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
+@Map$C0 = {4 a {4 {4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({7 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
 @Merge$C0 = {4 {9 a {9 b c}} {4 {11 d {4 @Merge$C0 {4 @Merge$C1 (e (f (g h)))}}} ({13 (i (a {2 @If$C0 {2 @If$C1 ({4 {4 j {4 k l}} {4 * l}} ({4 {4 c {4 h m}} {4 * m}} n))}})) {13 o e}} ({15 i {15 j f}} ({17 {4 @Merge$C2 {4 @Merge$C3 (o ({4 {4 b {4 d p}} {4 * p}} k))}} g} n)))}}
 @Merge$C1 = (* @Cons)
 @Merge$C2 = {4 a {4 b (c ({4 @Merge$C0 {4 @Merge$C1 (c (a (b d)))}} d))}}
 @Merge$C3 = (* (a a))
-@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({7 d b} ({4 @Merge$C2 {4 @Merge$C3 (d (a e))}} {4 {4 e {4 c f}} {4 * f}}))}}
+@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({5 d b} ({4 @Merge$C2 {4 @Merge$C3 (d (a e))}} {4 {4 e {4 c f}} {4 * f}}))}}
 @MergePair$C1 = (a {4 {4 a {4 @Nil b}} {4 * b}})
 @MergePair$C2 = (* @MergePair$C1)
 @MergePair$C3 = {4 a {4 {4 @MergePair$C0 {4 @MergePair$C2 (b (a c))}} (b c)}}
 @Nil = {4 * {4 a a}}
 @Pure = (a {4 {4 a {4 @Nil b}} {4 * b}})
 @Unpack = (a ({4 @Unpack$C2 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (a b)}} b))
-@Unpack$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b {4 @Unpack$C0 {4 @Unpack$C1 (c (d e))}})}} ({3 c {7 f b}} ({4 @Merge$C2 {4 @Merge$C3 (f (a d))}} e))}}
+@Unpack$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b {4 @Unpack$C0 {4 @Unpack$C1 (c (d e))}})}} ({3 c {5 f b}} ({4 @Merge$C2 {4 @Merge$C3 (f (a d))}} e))}}
 @Unpack$C1 = (* (a a))
 @Unpack$C2 = {4 a {4 {4 @Unpack$C0 {4 @Unpack$C1 (b (a c))}} (b c)}}
 @Unpack$C3_$_MergePair$C4_$_Map$C1 = (* @Nil)
diff --git a/tests/snapshots/encode_pattern_match__common.hvm.snap b/tests/snapshots/encode_pattern_match__common.hvm.snap
index 3a378f4b4..3d7ae2bea 100644
--- a/tests/snapshots/encode_pattern_match__common.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__common.hvm.snap
@@ -15,6 +15,10 @@ TaggedScott:
 
 (Yellow) = #Light λ* #Light λb #Light λ* b
 
+(Red) = #Light λa #Light λ* #Light λ* a
+
+(False) = #Bool λ* #Bool λb b
+
 (Filled) = λa #Box λb #Box λ* #Box (b a)
 
 (Empty) = #Box λ* #Box λb b
@@ -33,10 +37,6 @@ TaggedScott:
 
 (True) = #Bool λa #Bool λ* a
 
-(False) = #Bool λ* #Bool λb b
-
-(Red) = #Light λa #Light λ* #Light λ* a
-
 Scott:
 (West) = λ* λ* λ* λd d
 
@@ -50,6 +50,10 @@ Scott:
 
 (Yellow) = λ* λb λ* b
 
+(Red) = λa λ* λ* a
+
+(False) = λ* λb b
+
 (Filled) = λa λb λ* (b a)
 
 (Empty) = λ* λb b
@@ -67,7 +71,3 @@ Scott:
 (Nil) = λ* λb b
 
 (True) = λa λ* a
-
-(False) = λ* λb b
-
-(Red) = λa λ* λ* a
diff --git a/tests/snapshots/encode_pattern_match__expr.hvm.snap b/tests/snapshots/encode_pattern_match__expr.hvm.snap
index 3baca1515..9156735ed 100644
--- a/tests/snapshots/encode_pattern_match__expr.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__expr.hvm.snap
@@ -15,6 +15,10 @@ TaggedScott:
 
 (Tup) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λj #Expr λ* #Expr (j a b)
 
+(Dup) = λa λb λc λd #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λk #Expr λ* #Expr λ* #Expr (k a b c d)
+
+(Let) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λi #Expr λ* #Expr λ* #Expr λ* #Expr (i a b c)
+
 (Var) = λa #Expr λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (b a)
 
 (Num) = λa #Expr λ* #Expr λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (c a)
@@ -25,10 +29,6 @@ TaggedScott:
 
 (If) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λh #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (h a b c)
 
-(Let) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λi #Expr λ* #Expr λ* #Expr λ* #Expr (i a b c)
-
-(Dup) = λa λb λc λd #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λk #Expr λ* #Expr λ* #Expr (k a b c d)
-
 Scott:
 (Div) = λ* λ* λ* λd d
 
@@ -42,6 +42,10 @@ Scott:
 
 (Tup) = λa λb λ* λ* λ* λ* λ* λ* λ* λj λ* (j a b)
 
+(Dup) = λa λb λc λd λ* λ* λ* λ* λ* λ* λk λ* λ* (k a b c d)
+
+(Let) = λa λb λc λ* λ* λ* λ* λ* λi λ* λ* λ* (i a b c)
+
 (Var) = λa λb λ* λ* λ* λ* λ* λ* λ* λ* (b a)
 
 (Num) = λa λ* λc λ* λ* λ* λ* λ* λ* λ* (c a)
@@ -51,7 +55,3 @@ Scott:
 (Fun) = λa λb λ* λ* λ* λf λ* λ* λ* λ* λ* (f a b)
 
 (If) = λa λb λc λ* λ* λ* λ* λh λ* λ* λ* λ* (h a b c)
-
-(Let) = λa λb λc λ* λ* λ* λ* λ* λi λ* λ* λ* (i a b c)
-
-(Dup) = λa λb λc λd λ* λ* λ* λ* λ* λ* λk λ* λ* (k a b c d)
diff --git a/tests/snapshots/run_file__nat_add.hvm.snap b/tests/snapshots/run_file__nat_add.hvm.snap
new file mode 100644
index 000000000..df5debc9a
--- /dev/null
+++ b/tests/snapshots/run_file__nat_add.hvm.snap
@@ -0,0 +1,9 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/run_file/nat_add.hvm
+---
+Lazy mode:
+#34
+
+Strict mode:
+#34
diff --git a/tests/snapshots/simplify_matches__already_flat.hvm.snap b/tests/snapshots/simplify_matches__already_flat.hvm.snap
index 3a246c9c8..f17f812af 100644
--- a/tests/snapshots/simplify_matches__already_flat.hvm.snap
+++ b/tests/snapshots/simplify_matches__already_flat.hvm.snap
@@ -26,8 +26,8 @@ input_file: tests/golden_tests/simplify_matches/already_flat.hvm
 
 (CtrA2) = λa λb #Bar λ* #Bar λd #Bar λ* #Bar (d a b)
 
-(CtrA) = #Foo λa #Foo λ* a
+(CtrA1) = λa #Bar λb #Bar λ* #Bar λ* #Bar (b a)
 
 (CtrB) = λa #Foo λ* #Foo λc #Foo (c a)
 
-(CtrA1) = λa #Bar λb #Bar λ* #Bar λ* #Bar (b a)
+(CtrA) = #Foo λa #Foo λ* a

From 6b7cbeb7be287db19c1d62d627c7880a8d383fb3 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Tue, 19 Mar 2024 13:59:17 -0300
Subject: [PATCH 2/3] Update cspell and add nat resugar test

---
 cspell.json                                    | 1 +
 tests/golden_tests/run_file/nat_add_num.hvm    | 4 ++++
 tests/snapshots/run_file__nat_add_num.hvm.snap | 9 +++++++++
 3 files changed, 14 insertions(+)
 create mode 100644 tests/golden_tests/run_file/nat_add_num.hvm
 create mode 100644 tests/snapshots/run_file__nat_add_num.hvm.snap

diff --git a/cspell.json b/cspell.json
index e115c5a75..3ee82f47a 100644
--- a/cspell.json
+++ b/cspell.json
@@ -44,6 +44,7 @@
     "mult",
     "namegen",
     "nams",
+    "nats",
     "numop",
     "nums",
     "oper",
diff --git a/tests/golden_tests/run_file/nat_add_num.hvm b/tests/golden_tests/run_file/nat_add_num.hvm
new file mode 100644
index 000000000..f1c67dd6d
--- /dev/null
+++ b/tests/golden_tests/run_file/nat_add_num.hvm
@@ -0,0 +1,4 @@
+(Nat.add (Nat.zero)   x) = x
+(Nat.add (Nat.succ p) x) = (Nat.succ (Nat.add p x))
+
+main = (Nat.add #4 0)
diff --git a/tests/snapshots/run_file__nat_add_num.hvm.snap b/tests/snapshots/run_file__nat_add_num.hvm.snap
new file mode 100644
index 000000000..f9a1ddb92
--- /dev/null
+++ b/tests/snapshots/run_file__nat_add_num.hvm.snap
@@ -0,0 +1,9 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/run_file/nat_add_num.hvm
+---
+Lazy mode:
+(Nat.succ (Nat.succ (Nat.succ (Nat.succ 0))))
+
+Strict mode:
+(Nat.succ (Nat.succ (Nat.succ (Nat.succ 0))))

From 3da5db0c01f24359c80846e0ec1a70a8fb78cb4b Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Tue, 19 Mar 2024 14:37:30 -0300
Subject: [PATCH 3/3] Change swap_remove to shift_remove

---
 src/term/transform/definition_pruning.rs      |  2 +-
 .../cli__desugar_bool_scott.hvm.snap          |  4 +-
 .../cli__desugar_bool_tagged.hvm.snap         |  4 +-
 ...ompile_file_o_all__adt_option_and.hvm.snap |  6 +--
 .../compile_file_o_all__expr.hvm.snap         | 22 ++++----
 ...mpile_file_o_all__list_merge_sort.hvm.snap | 14 +++---
 .../encode_pattern_match__and3.hvm.snap       |  8 +--
 .../encode_pattern_match__bool.hvm.snap       |  8 ++-
 .../encode_pattern_match__bool_tup.hvm.snap   |  8 ++-
 .../encode_pattern_match__common.hvm.snap     | 50 +++++++++----------
 ...e_pattern_match__definition_merge.hvm.snap | 16 +++---
 .../encode_pattern_match__expr.hvm.snap       | 48 +++++++++---------
 ...ncode_pattern_match__is_some_some.hvm.snap |  8 +--
 ...de_pattern_match__list_merge_sort.hvm.snap | 16 +++---
 ..._match__match_adt_unscoped_in_arm.hvm.snap |  8 ++-
 ..._match__match_adt_unscoped_lambda.hvm.snap |  8 +--
 ...ern_match__match_adt_unscoped_var.hvm.snap |  8 +--
 ...de_pattern_match__match_many_args.hvm.snap | 16 +++---
 ...n_match__match_num_adt_tup_parser.hvm.snap |  8 +--
 ...ncode_pattern_match__match_syntax.hvm.snap |  8 +--
 ...ttern_match__non_matching_fst_arg.hvm.snap |  8 +--
 ...ern_match__pattern_match_encoding.hvm.snap | 16 +++---
 .../encode_pattern_match__var_only.hvm.snap   |  8 +--
 .../encode_pattern_match__weekday.hvm.snap    | 24 ++++-----
 .../simplify_matches__already_flat.hvm.snap   | 16 +++---
 .../simplify_matches__bits_dec.hvm.snap       |  4 +-
 ...lify_matches__double_unwrap_maybe.hvm.snap |  4 +-
 ...fy_matches__flatten_with_terminal.hvm.snap |  4 +-
 .../simplify_matches__nested.hvm.snap         |  8 +--
 .../simplify_matches__nested_0ary.hvm.snap    |  4 +-
 30 files changed, 180 insertions(+), 186 deletions(-)

diff --git a/src/term/transform/definition_pruning.rs b/src/term/transform/definition_pruning.rs
index 69897cc64..2644e0f87 100644
--- a/src/term/transform/definition_pruning.rs
+++ b/src/term/transform/definition_pruning.rs
@@ -71,7 +71,7 @@ impl Ctx<'_> {
     for def_name in unused {
       let def = &self.book.defs[&def_name];
       if prune_all || def.builtin {
-        self.book.defs.swap_remove(&def_name);
+        self.book.defs.shift_remove(&def_name);
       } else if !def_name.is_generated() {
         self.info.add_rule_warning(UnusedDefinitionWarning, WarningType::UnusedDefinition, def_name);
       }
diff --git a/tests/snapshots/cli__desugar_bool_scott.hvm.snap b/tests/snapshots/cli__desugar_bool_scott.hvm.snap
index b66ce163b..3789e55b6 100644
--- a/tests/snapshots/cli__desugar_bool_scott.hvm.snap
+++ b/tests/snapshots/cli__desugar_bool_scott.hvm.snap
@@ -4,6 +4,6 @@ input_file: tests/golden_tests/cli/desugar_bool_scott.hvm
 ---
 (main) = True
 
-(False) = λ* λb b
-
 (True) = λa λ* a
+
+(False) = λ* λb b
diff --git a/tests/snapshots/cli__desugar_bool_tagged.hvm.snap b/tests/snapshots/cli__desugar_bool_tagged.hvm.snap
index ca24321d9..1cdc4fe75 100644
--- a/tests/snapshots/cli__desugar_bool_tagged.hvm.snap
+++ b/tests/snapshots/cli__desugar_bool_tagged.hvm.snap
@@ -4,6 +4,6 @@ input_file: tests/golden_tests/cli/desugar_bool_tagged.hvm
 ---
 (main) = True
 
-(False) = #Boolean λ* #Boolean λb b
-
 (True) = #Boolean λa #Boolean λ* a
+
+(False) = #Boolean λ* #Boolean λb b
diff --git a/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap b/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap
index d01cbac5e..82e994b55 100644
--- a/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap
@@ -3,10 +3,10 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/adt_option_and.hvm
 ---
 @None = {2 * {2 a a}}
-@Option.and = ({2 @Option.and$C2 {2 @Option.and$C3_$_Option.and$C1 a}} a)
+@Option.and = ({2 @Option.and$C2 {2 @Option.and$C1_$_Option.and$C3 a}} a)
 @Option.and$C0 = {2 a (b {2 {2 [b a] c} {2 * c}})}
-@Option.and$C2 = {2 a ({2 @Option.and$C0 {2 @Option.and$C3_$_Option.and$C1 (a b)}} b)}
-@Option.and$C3_$_Option.and$C1 = (* @None)
+@Option.and$C1_$_Option.and$C3 = (* @None)
+@Option.and$C2 = {2 a ({2 @Option.and$C0 {2 @Option.and$C1_$_Option.and$C3 (a b)}} b)}
 @Some = (a {2 {2 a b} {2 * b}})
 @main = a
 & @Option.and ~ (b (c a))
diff --git a/tests/snapshots/compile_file_o_all__expr.hvm.snap b/tests/snapshots/compile_file_o_all__expr.hvm.snap
index 06634c3e2..373e053fb 100644
--- a/tests/snapshots/compile_file_o_all__expr.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__expr.hvm.snap
@@ -2,17 +2,17 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/expr.hvm
 ---
-@App = (a (b {4 * {4 * {4 {4 a {4 b c}} {4 * {4 * {4 * {4 * {4 * {4 * c}}}}}}}}}))
-@Dup = (a (b (c (d {4 * {4 * {4 * {4 * {4 * {4 * {4 {4 a {4 b {4 c {4 d e}}}} {4 * {4 * e}}}}}}}}}))))
-@Let = (a (b (c {4 * {4 * {4 * {4 * {4 * {4 {4 a {4 b {4 c d}}} {4 * {4 * {4 * d}}}}}}}}})))
-@Mul = {2 * @Mul$C1}
-@Mul$C0 = {2 a {2 * a}}
-@Mul$C1 = {2 * @Mul$C0}
-@Num = (a {4 * {4 {4 a b} {4 * {4 * {4 * {4 * {4 * {4 * {4 * b}}}}}}}}})
-@Op2 = (a (b (c {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 {4 a {4 b {4 c d}}} d}}}}}}}}})))
-@Sub = {2 * @Sub$C0}
-@Sub$C0 = {2 a {2 * {2 * a}}}
-@Var = (a {4 {4 a b} {4 * {4 * {4 * {4 * {4 * {4 * {4 * {4 * b}}}}}}}}})
+@App = (a (b {2 * {2 * {2 {2 a {2 b c}} {2 * {2 * {2 * {2 * {2 * {2 * c}}}}}}}}}))
+@Dup = (a (b (c (d {2 * {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c {2 d e}}}} {2 * {2 * e}}}}}}}}}))))
+@Let = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} {2 * {2 * {2 * d}}}}}}}}})))
+@Mul = {4 * @Mul$C1}
+@Mul$C0 = {4 a {4 * a}}
+@Mul$C1 = {4 * @Mul$C0}
+@Num = (a {2 * {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
+@Op2 = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} d}}}}}}}}})))
+@Sub = {4 * @Sub$C0}
+@Sub$C0 = {4 a {4 * {4 * a}}}
+@Var = (a {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
 @main = a
 & @Let ~ (b (c (d a)))
 & @Dup ~ (e (f (g (h d))))
diff --git a/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap b/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap
index a39aaff85..08abf53ea 100644
--- a/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap
@@ -5,23 +5,23 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 @Cons = (a (b {4 {4 a {4 b c}} {4 * c}}))
 @If$C0 = (a (* a))
 @If$C1 = (* (a a))
-@Map = ({4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 a}} a)
-@Map$C0 = {4 a {4 {4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({7 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
-@Merge$C0 = {4 {9 a {9 b c}} {4 {11 d {4 @Merge$C0 {4 @Merge$C1 (e (f (g h)))}}} ({13 (i (a {2 @If$C0 {2 @If$C1 ({4 {4 j {4 k l}} {4 * l}} ({4 {4 c {4 h m}} {4 * m}} n))}})) {13 o e}} ({15 i {15 j f}} ({17 {4 @Merge$C2 {4 @Merge$C3 (o ({4 {4 b {4 d p}} {4 * p}} k))}} g} n)))}}
+@Map = ({4 @Map$C0 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 a}} a)
+@Map$C0 = {4 a {4 {4 @Map$C0 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (b c)}} ({3 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
+@Map$C1_$_MergePair$C4_$_Unpack$C3 = (* @Nil)
+@Merge$C0 = {4 {5 a {5 b c}} {4 {7 d {4 @Merge$C0 {4 @Merge$C1 (e (f (g h)))}}} ({9 (i (a {2 @If$C0 {2 @If$C1 ({4 {4 j {4 k l}} {4 * l}} ({4 {4 c {4 h m}} {4 * m}} n))}})) {9 o e}} ({11 i {11 j f}} ({13 {4 @Merge$C2 {4 @Merge$C3 (o ({4 {4 b {4 d p}} {4 * p}} k))}} g} n)))}}
 @Merge$C1 = (* @Cons)
 @Merge$C2 = {4 a {4 b (c ({4 @Merge$C0 {4 @Merge$C1 (c (a (b d)))}} d))}}
 @Merge$C3 = (* (a a))
-@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({5 d b} ({4 @Merge$C2 {4 @Merge$C3 (d (a e))}} {4 {4 e {4 c f}} {4 * f}}))}}
+@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (b c)}} ({15 d b} ({4 @Merge$C2 {4 @Merge$C3 (d (a e))}} {4 {4 e {4 c f}} {4 * f}}))}}
 @MergePair$C1 = (a {4 {4 a {4 @Nil b}} {4 * b}})
 @MergePair$C2 = (* @MergePair$C1)
 @MergePair$C3 = {4 a {4 {4 @MergePair$C0 {4 @MergePair$C2 (b (a c))}} (b c)}}
 @Nil = {4 * {4 a a}}
 @Pure = (a {4 {4 a {4 @Nil b}} {4 * b}})
-@Unpack = (a ({4 @Unpack$C2 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (a b)}} b))
-@Unpack$C0 = {4 a {4 {4 @MergePair$C3 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b {4 @Unpack$C0 {4 @Unpack$C1 (c (d e))}})}} ({3 c {5 f b}} ({4 @Merge$C2 {4 @Merge$C3 (f (a d))}} e))}}
+@Unpack = (a ({4 @Unpack$C2 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (a b)}} b))
+@Unpack$C0 = {4 a {4 {4 @MergePair$C3 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (b {4 @Unpack$C0 {4 @Unpack$C1 (c (d e))}})}} ({17 c {15 f b}} ({4 @Merge$C2 {4 @Merge$C3 (f (a d))}} e))}}
 @Unpack$C1 = (* (a a))
 @Unpack$C2 = {4 a {4 {4 @Unpack$C0 {4 @Unpack$C1 (b (a c))}} (b c)}}
-@Unpack$C3_$_MergePair$C4_$_Map$C1 = (* @Nil)
 @main = (a (b c))
 & @Unpack ~ (a (d c))
 & @Map ~ (b (@Pure d))
diff --git a/tests/snapshots/encode_pattern_match__and3.hvm.snap b/tests/snapshots/encode_pattern_match__and3.hvm.snap
index f7b7ea219..64dc16ec9 100644
--- a/tests/snapshots/encode_pattern_match__and3.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__and3.hvm.snap
@@ -7,15 +7,15 @@ TaggedScott:
 
 (main) = (And (F, T, F))
 
-(F) = #Bool λ* #Bool λb b
-
 (T) = #Bool λa #Bool λ* a
 
+(F) = #Bool λ* #Bool λb b
+
 Scott:
 (And) = λa let (b, c, d) = a; (b λe λf (e λh (h T F) λ* F f) λ* λ* F c d)
 
 (main) = (And (F, T, F))
 
-(F) = λ* λb b
-
 (T) = λa λ* a
+
+(F) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__bool.hvm.snap b/tests/snapshots/encode_pattern_match__bool.hvm.snap
index fcb6ab70c..cd43bb09d 100644
--- a/tests/snapshots/encode_pattern_match__bool.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__bool.hvm.snap
@@ -13,10 +13,10 @@ TaggedScott:
 
 (and4) = λa λb (#bool (a λc #bool (c true false) λ* false) b)
 
-(false) = #bool λ* #bool λb b
-
 (true) = #bool λa #bool λ* a
 
+(false) = #bool λ* #bool λb b
+
 Scott:
 (not) = λa (a false true)
 
@@ -28,8 +28,6 @@ Scott:
 
 (and4) = λa λb (a λc (c true false) λ* false b)
 
-(false) = λ* λb b
-
 (true) = λa λ* a
 
-
+(false) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__bool_tup.hvm.snap b/tests/snapshots/encode_pattern_match__bool_tup.hvm.snap
index 6d34dd997..01ddad644 100644
--- a/tests/snapshots/encode_pattern_match__bool_tup.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__bool_tup.hvm.snap
@@ -7,17 +7,15 @@ TaggedScott:
 
 (main) = (foo (F, T))
 
-(F) = #Bool λ* #Bool λb b
-
 (T) = #Bool λa #Bool λ* a
 
+(F) = #Bool λ* #Bool λb b
+
 Scott:
 (foo) = λa let (b, c) = a; (b λd d λ* F c)
 
 (main) = (foo (F, T))
 
-(F) = λ* λb b
-
 (T) = λa λ* a
 
-
+(F) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__common.hvm.snap b/tests/snapshots/encode_pattern_match__common.hvm.snap
index 3d7ae2bea..00e2c5770 100644
--- a/tests/snapshots/encode_pattern_match__common.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__common.hvm.snap
@@ -3,22 +3,6 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/common.hvm
 ---
 TaggedScott:
-(West) = #Direction λ* #Direction λ* #Direction λ* #Direction λd d
-
-(East) = #Direction λ* #Direction λ* #Direction λc #Direction λ* c
-
-(South) = #Direction λ* #Direction λb #Direction λ* #Direction λ* b
-
-(North) = #Direction λa #Direction λ* #Direction λ* #Direction λ* a
-
-(Green) = #Light λ* #Light λ* #Light λc c
-
-(Yellow) = #Light λ* #Light λb #Light λ* b
-
-(Red) = #Light λa #Light λ* #Light λ* a
-
-(False) = #Bool λ* #Bool λb b
-
 (Filled) = λa #Box λb #Box λ* #Box (b a)
 
 (Empty) = #Box λ* #Box λb b
@@ -37,23 +21,23 @@ TaggedScott:
 
 (True) = #Bool λa #Bool λ* a
 
-Scott:
-(West) = λ* λ* λ* λd d
+(False) = #Bool λ* #Bool λb b
 
-(East) = λ* λ* λc λ* c
+(Red) = #Light λa #Light λ* #Light λ* a
 
-(South) = λ* λb λ* λ* b
+(Yellow) = #Light λ* #Light λb #Light λ* b
 
-(North) = λa λ* λ* λ* a
+(Green) = #Light λ* #Light λ* #Light λc c
 
-(Green) = λ* λ* λc c
+(North) = #Direction λa #Direction λ* #Direction λ* #Direction λ* a
 
-(Yellow) = λ* λb λ* b
+(South) = #Direction λ* #Direction λb #Direction λ* #Direction λ* b
 
-(Red) = λa λ* λ* a
+(East) = #Direction λ* #Direction λ* #Direction λc #Direction λ* c
 
-(False) = λ* λb b
+(West) = #Direction λ* #Direction λ* #Direction λ* #Direction λd d
 
+Scott:
 (Filled) = λa λb λ* (b a)
 
 (Empty) = λ* λb b
@@ -71,3 +55,19 @@ Scott:
 (Nil) = λ* λb b
 
 (True) = λa λ* a
+
+(False) = λ* λb b
+
+(Red) = λa λ* λ* a
+
+(Yellow) = λ* λb λ* b
+
+(Green) = λ* λ* λc c
+
+(North) = λa λ* λ* λ* a
+
+(South) = λ* λb λ* λ* b
+
+(East) = λ* λ* λc λ* c
+
+(West) = λ* λ* λ* λd d
diff --git a/tests/snapshots/encode_pattern_match__definition_merge.hvm.snap b/tests/snapshots/encode_pattern_match__definition_merge.hvm.snap
index 7c8c46579..9c8497d09 100644
--- a/tests/snapshots/encode_pattern_match__definition_merge.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__definition_merge.hvm.snap
@@ -5,21 +5,21 @@ input_file: tests/golden_tests/encode_pattern_match/definition_merge.hvm
 TaggedScott:
 (Foo) = λa λb (#Either (a #Either λc λd (#Bool (c λe #Either (e #Either λg #Bool (g 1 1) #Either λj #Bool (j 2 2)) λm #Either (m #Either λo #Bool (o 1 1) #Either λr #Bool (r 2 2))) d) #Either λu λv (#Bool (u λw #Either (w #Either λy #Bool (y 3 3) #Either λbb #Bool (bb 3 3)) λeb #Either (eb #Either λgb #Bool (gb 3 3) #Either λjb #Bool (jb 3 3))) v)) b)
 
-(False) = #Bool λ* #Bool λb b
-
-(True) = #Bool λa #Bool λ* a
+(Left) = λa #Either λb #Either λ* #Either (b a)
 
 (Right) = λa #Either λ* #Either λc #Either (c a)
 
-(Left) = λa #Either λb #Either λ* #Either (b a)
+(True) = #Bool λa #Bool λ* a
+
+(False) = #Bool λ* #Bool λb b
 
 Scott:
 (Foo) = λa λb (a λc λd (c λe (e λg (g 1 1) λj (j 2 2)) λm (m λo (o 1 1) λr (r 2 2)) d) λu λv (u λw (w λy (y 3 3) λbb (bb 3 3)) λeb (eb λgb (gb 3 3) λjb (jb 3 3)) v) b)
 
-(False) = λ* λb b
-
-(True) = λa λ* a
+(Left) = λa λb λ* (b a)
 
 (Right) = λa λ* λc (c a)
 
-(Left) = λa λb λ* (b a)
+(True) = λa λ* a
+
+(False) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__expr.hvm.snap b/tests/snapshots/encode_pattern_match__expr.hvm.snap
index 9156735ed..eb08398ac 100644
--- a/tests/snapshots/encode_pattern_match__expr.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__expr.hvm.snap
@@ -3,55 +3,55 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/expr.hvm
 ---
 TaggedScott:
-(Div) = #Op λ* #Op λ* #Op λ* #Op λd d
+(Var) = λa #Expr λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (b a)
 
-(Mul) = #Op λ* #Op λ* #Op λc #Op λ* c
+(Num) = λa #Expr λ* #Expr λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (c a)
 
-(Sub) = #Op λ* #Op λb #Op λ* #Op λ* b
+(App) = λa λb #Expr λ* #Expr λ* #Expr λe #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (e a b)
 
-(Add) = #Op λa #Op λ* #Op λ* #Op λ* a
+(Fun) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λf #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (f a b)
 
-(Op2) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λl #Expr (l a b c)
+(If) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λh #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (h a b c)
 
-(Tup) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λj #Expr λ* #Expr (j a b)
+(Let) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λi #Expr λ* #Expr λ* #Expr λ* #Expr (i a b c)
 
 (Dup) = λa λb λc λd #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λk #Expr λ* #Expr λ* #Expr (k a b c d)
 
-(Let) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λi #Expr λ* #Expr λ* #Expr λ* #Expr (i a b c)
+(Tup) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λj #Expr λ* #Expr (j a b)
 
-(Var) = λa #Expr λb #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (b a)
+(Op2) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λl #Expr (l a b c)
 
-(Num) = λa #Expr λ* #Expr λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (c a)
+(Add) = #Op λa #Op λ* #Op λ* #Op λ* a
 
-(App) = λa λb #Expr λ* #Expr λ* #Expr λe #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (e a b)
+(Sub) = #Op λ* #Op λb #Op λ* #Op λ* b
 
-(Fun) = λa λb #Expr λ* #Expr λ* #Expr λ* #Expr λf #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (f a b)
+(Mul) = #Op λ* #Op λ* #Op λc #Op λ* c
 
-(If) = λa λb λc #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr λh #Expr λ* #Expr λ* #Expr λ* #Expr λ* #Expr (h a b c)
+(Div) = #Op λ* #Op λ* #Op λ* #Op λd d
 
 Scott:
-(Div) = λ* λ* λ* λd d
+(Var) = λa λb λ* λ* λ* λ* λ* λ* λ* λ* (b a)
 
-(Mul) = λ* λ* λc λ* c
+(Num) = λa λ* λc λ* λ* λ* λ* λ* λ* λ* (c a)
 
-(Sub) = λ* λb λ* λ* b
+(App) = λa λb λ* λ* λe λ* λ* λ* λ* λ* λ* (e a b)
 
-(Add) = λa λ* λ* λ* a
+(Fun) = λa λb λ* λ* λ* λf λ* λ* λ* λ* λ* (f a b)
 
-(Op2) = λa λb λc λ* λ* λ* λ* λ* λ* λ* λ* λl (l a b c)
+(If) = λa λb λc λ* λ* λ* λ* λh λ* λ* λ* λ* (h a b c)
 
-(Tup) = λa λb λ* λ* λ* λ* λ* λ* λ* λj λ* (j a b)
+(Let) = λa λb λc λ* λ* λ* λ* λ* λi λ* λ* λ* (i a b c)
 
 (Dup) = λa λb λc λd λ* λ* λ* λ* λ* λ* λk λ* λ* (k a b c d)
 
-(Let) = λa λb λc λ* λ* λ* λ* λ* λi λ* λ* λ* (i a b c)
+(Tup) = λa λb λ* λ* λ* λ* λ* λ* λ* λj λ* (j a b)
 
-(Var) = λa λb λ* λ* λ* λ* λ* λ* λ* λ* (b a)
+(Op2) = λa λb λc λ* λ* λ* λ* λ* λ* λ* λ* λl (l a b c)
 
-(Num) = λa λ* λc λ* λ* λ* λ* λ* λ* λ* (c a)
+(Add) = λa λ* λ* λ* a
 
-(App) = λa λb λ* λ* λe λ* λ* λ* λ* λ* λ* (e a b)
+(Sub) = λ* λb λ* λ* b
 
-(Fun) = λa λb λ* λ* λ* λf λ* λ* λ* λ* λ* (f a b)
+(Mul) = λ* λ* λc λ* c
 
-(If) = λa λb λc λ* λ* λ* λ* λh λ* λ* λ* λ* (h a b c)
+(Div) = λ* λ* λ* λd d
diff --git a/tests/snapshots/encode_pattern_match__is_some_some.hvm.snap b/tests/snapshots/encode_pattern_match__is_some_some.hvm.snap
index b57cb189a..6e55f5904 100644
--- a/tests/snapshots/encode_pattern_match__is_some_some.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__is_some_some.hvm.snap
@@ -7,15 +7,15 @@ TaggedScott:
 
 (main) = (some_some (Some 1))
 
-(None) = #Option λ* #Option λb b
-
 (Some) = λa #Option λb #Option λ* #Option (b a)
 
+(None) = #Option λ* #Option λb b
+
 Scott:
 (some_some) = λa (a λb (b λ* 1 0) 0)
 
 (main) = (some_some (Some 1))
 
-(None) = λ* λb b
-
 (Some) = λa λb λ* (b a)
+
+(None) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap b/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap
index eb5dc0ba4..3ba0d1558 100644
--- a/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap
@@ -17,13 +17,13 @@ TaggedScott:
 
 (Merge) = λa λb λc (#List_ (b #List_ λd #List_ λe λf λg (#List_ (g #List_ λh let {h h_2 h_3} = h; #List_ λi let {i i_2} = i; λj let {j j_2 j_3} = j; λk let {k k_2 k_3} = k; λl let {l l_2} = l; (If (j k h) (Cons k_2 (Merge j_2 l (Cons h_2 i))) (Cons h_3 (Merge j_3 (Cons k_3 l_2) i_2))) λ* λp λq (Cons p q)) f d e) λ* λt t) a c)
 
-(Nil) = #List_ λ* #List_ λb b
-
-(Cons) = λa λb #List_ λc #List_ λ* #List_ (c a b)
+(True) = #Bool λa #Bool λ* a
 
 (False) = #Bool λ* #Bool λb b
 
-(True) = #Bool λa #Bool λ* a
+(Cons) = λa λb #List_ λc #List_ λ* #List_ (c a b)
+
+(Nil) = #List_ λ* #List_ λb b
 
 Scott:
 (If) = λa λb λc (a λd λ* d λ* λh h b c)
@@ -40,10 +40,10 @@ Scott:
 
 (Merge) = λa λb λc (b λd λe λf λg (g λh let {h h_2 h_3} = h; λi let {i i_2} = i; λj let {j j_2 j_3} = j; λk let {k k_2 k_3} = k; λl let {l l_2} = l; (If (j k h) (Cons k_2 (Merge j_2 l (Cons h_2 i))) (Cons h_3 (Merge j_3 (Cons k_3 l_2) i_2))) λ* λp λq (Cons p q) f d e) λ* λt t a c)
 
-(Nil) = λ* λb b
-
-(Cons) = λa λb λc λ* (c a b)
+(True) = λa λ* a
 
 (False) = λ* λb b
 
-(True) = λa λ* a
+(Cons) = λa λb λc λ* (c a b)
+
+(Nil) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__match_adt_unscoped_in_arm.hvm.snap b/tests/snapshots/encode_pattern_match__match_adt_unscoped_in_arm.hvm.snap
index e11619e13..964d40a2e 100644
--- a/tests/snapshots/encode_pattern_match__match_adt_unscoped_in_arm.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_adt_unscoped_in_arm.hvm.snap
@@ -5,15 +5,13 @@ input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_in_arm.hv
 TaggedScott:
 (main) = λa #bool (a λ$x $x λd d)
 
-(F) = #bool λ* #bool λb b
-
 (T) = #bool λa #bool λ* a
 
+(F) = #bool λ* #bool λb b
+
 Scott:
 (main) = λa (a λ$x $x λd d)
 
-(F) = λ* λb b
-
 (T) = λa λ* a
 
-
+(F) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap b/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap
index c8d86f534..63a423e23 100644
--- a/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap
@@ -5,13 +5,13 @@ input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hv
 TaggedScott:
 (main) = (#Maybe ((Some 1) λ$x * #Maybe λc c) $x)
 
-(Some) = λa #Maybe λ* #Maybe λc #Maybe (c a)
-
 (None) = #Maybe λa #Maybe λ* a
 
+(Some) = λa #Maybe λ* #Maybe λc #Maybe (c a)
+
 Scott:
 (main) = (Some 1 λ$x * λc c $x)
 
-(Some) = λa λ* λc (c a)
-
 (None) = λa λ* a
+
+(Some) = λa λ* λc (c a)
diff --git a/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap b/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap
index 9f6164d69..26852bb2f 100644
--- a/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap
@@ -9,10 +9,10 @@ TaggedScott:
 
 (main) = *
 
-(Some) = λa #Maybe λ* #Maybe λc #Maybe (c a)
-
 (None) = #Maybe λa #Maybe λ* a
 
+(Some) = λa #Maybe λ* #Maybe λc #Maybe (c a)
+
 Scott:
 (Foo) = λ$x (Some 1 $x λc c)
 
@@ -20,6 +20,6 @@ Scott:
 
 (main) = *
 
-(Some) = λa λ* λc (c a)
-
 (None) = λa λ* a
+
+(Some) = λa λ* λc (c a)
diff --git a/tests/snapshots/encode_pattern_match__match_many_args.hvm.snap b/tests/snapshots/encode_pattern_match__match_many_args.hvm.snap
index 848922354..a88531fa6 100644
--- a/tests/snapshots/encode_pattern_match__match_many_args.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_many_args.hvm.snap
@@ -19,13 +19,13 @@ TaggedScott:
 
 (main) = *
 
-(None) = #Option λ* #Option λb b
-
-(Some) = λa #Option λb #Option λ* #Option (b a)
+(C) = λa λb #L λc #L λ* #L (c a b)
 
 (N) = #L λ* #L λb b
 
-(C) = λa λb #L λc #L λ* #L (c a b)
+(Some) = λa #Option λb #Option λ* #Option (b a)
+
+(None) = #Option λ* #Option λb b
 
 Scott:
 (tail_tail) = λa (a λ* λc (c λ* λe e N) N)
@@ -44,10 +44,10 @@ Scott:
 
 (main) = *
 
-(None) = λ* λb b
-
-(Some) = λa λb λ* (b a)
+(C) = λa λb λc λ* (c a b)
 
 (N) = λ* λb b
 
-(C) = λa λb λc λ* (c a b)
+(Some) = λa λb λ* (b a)
+
+(None) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
index fff85613a..0d8cf8866 100644
--- a/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
@@ -11,10 +11,10 @@ TaggedScott:
 
 (String.nil) = #String λ* #String λb b
 
-(Err) = λa #Result_ λ* #Result_ λc #Result_ (c a)
-
 (Ok) = λa #Result_ λb #Result_ λ* #Result_ (b a)
 
+(Err) = λa #Result_ λ* #Result_ λc #Result_ (c a)
+
 Scott:
 (Parse) = λa λb (b λc λd λe (match (- c 40) { 0: λf λg (Ok (40, g, f)); 1+: λi match i { 0: λj λk (Ok (41, k, j)); 1+: λm match (- m 18446744073709551584) { 0: λn λo (Ok (0, o, n)); 1+: λq λs λt (Err ((String.cons (+ q 11) t), s)) } } } e d) λu (Err (String.nil, u)) a)
 
@@ -24,6 +24,6 @@ Scott:
 
 (String.nil) = λ* λb b
 
-(Err) = λa λ* λc (c a)
-
 (Ok) = λa λb λ* (b a)
+
+(Err) = λa λ* λc (c a)
diff --git a/tests/snapshots/encode_pattern_match__match_syntax.hvm.snap b/tests/snapshots/encode_pattern_match__match_syntax.hvm.snap
index 19fb245e1..2bd29012a 100644
--- a/tests/snapshots/encode_pattern_match__match_syntax.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_syntax.hvm.snap
@@ -5,13 +5,13 @@ input_file: tests/golden_tests/encode_pattern_match/match_syntax.hvm
 TaggedScott:
 (head) = λa #List_ (a #List_ λb #List_ λ* b Nil)
 
-(Nil) = #List_ λ* #List_ λb b
-
 (Cons) = λa λb #List_ λc #List_ λ* #List_ (c a b)
 
+(Nil) = #List_ λ* #List_ λb b
+
 Scott:
 (head) = λa (a λb λ* b Nil)
 
-(Nil) = λ* λb b
-
 (Cons) = λa λb λc λ* (c a b)
+
+(Nil) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap b/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap
index 4c1bb6e48..3968b94e0 100644
--- a/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap
@@ -5,13 +5,13 @@ input_file: tests/golden_tests/encode_pattern_match/non_matching_fst_arg.hvm
 TaggedScott:
 (Foo) = λa λb (#bool (b λc let {c c_2} = c; (Foo c c_2) λe e) a)
 
-(false) = #bool λ* #bool λb b
-
 (true) = #bool λa #bool λ* a
 
+(false) = #bool λ* #bool λb b
+
 Scott:
 (Foo) = λa λb (b λc let {c c_2} = c; (Foo c c_2) λe e a)
 
-(false) = λ* λb b
-
 (true) = λa λ* a
+
+(false) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__pattern_match_encoding.hvm.snap b/tests/snapshots/encode_pattern_match__pattern_match_encoding.hvm.snap
index 34e105a35..f2c7ed854 100644
--- a/tests/snapshots/encode_pattern_match__pattern_match_encoding.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__pattern_match_encoding.hvm.snap
@@ -7,27 +7,27 @@ TaggedScott:
 
 (main) = (Foo A 2)
 
-(E) = λa λb #MyType λ* #MyType λ* #MyType λ* #MyType λ* #MyType λg #MyType (g a b)
+(A) = λa #MyType λb #MyType λ* #MyType λ* #MyType λ* #MyType λ* #MyType (b a)
 
-(D) = λa λb #MyType λ* #MyType λ* #MyType λ* #MyType λf #MyType λ* #MyType (f a b)
+(B) = λa #MyType λ* #MyType λc #MyType λ* #MyType λ* #MyType λ* #MyType (c a)
 
 (C) = λa #MyType λ* #MyType λ* #MyType λd #MyType λ* #MyType λ* #MyType (d a)
 
-(B) = λa #MyType λ* #MyType λc #MyType λ* #MyType λ* #MyType λ* #MyType (c a)
+(D) = λa λb #MyType λ* #MyType λ* #MyType λ* #MyType λf #MyType λ* #MyType (f a b)
 
-(A) = λa #MyType λb #MyType λ* #MyType λ* #MyType λ* #MyType λ* #MyType (b a)
+(E) = λa λb #MyType λ* #MyType λ* #MyType λ* #MyType λ* #MyType λg #MyType (g a b)
 
 Scott:
 (Foo) = λa (a λ* 100 λ* 200 λ* 200 λ* λ* 200 λ* λ* 200)
 
 (main) = (Foo A 2)
 
-(E) = λa λb λ* λ* λ* λ* λg (g a b)
+(A) = λa λb λ* λ* λ* λ* (b a)
 
-(D) = λa λb λ* λ* λ* λf λ* (f a b)
+(B) = λa λ* λc λ* λ* λ* (c a)
 
 (C) = λa λ* λ* λd λ* λ* (d a)
 
-(B) = λa λ* λc λ* λ* λ* (c a)
+(D) = λa λb λ* λ* λ* λf λ* (f a b)
 
-(A) = λa λb λ* λ* λ* λ* (b a)
+(E) = λa λb λ* λ* λ* λ* λg (g a b)
diff --git a/tests/snapshots/encode_pattern_match__var_only.hvm.snap b/tests/snapshots/encode_pattern_match__var_only.hvm.snap
index 4751aae26..dee3fbef2 100644
--- a/tests/snapshots/encode_pattern_match__var_only.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__var_only.hvm.snap
@@ -7,15 +7,15 @@ TaggedScott:
 
 (main) = λ* Foo
 
-(True) = #Bool λ* #Bool λb b
-
 (False) = #Bool λa #Bool λ* a
 
+(True) = #Bool λ* #Bool λb b
+
 Scott:
 (Foo) = λa λ* λc (c a)
 
 (main) = λ* Foo
 
-(True) = λ* λb b
-
 (False) = λa λ* a
+
+(True) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__weekday.hvm.snap b/tests/snapshots/encode_pattern_match__weekday.hvm.snap
index 2e6136bd7..36d6fb3c7 100644
--- a/tests/snapshots/encode_pattern_match__weekday.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__weekday.hvm.snap
@@ -5,33 +5,33 @@ input_file: tests/golden_tests/encode_pattern_match/weekday.hvm
 TaggedScott:
 (main) = (λa a Saturday)
 
-(Sunday) = #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λg g
+(Monday) = #Weekday λa #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* a
 
-(Saturday) = #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λf #Weekday λ* f
+(Tuesday) = #Weekday λ* #Weekday λb #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* b
 
-(Friday) = #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λe #Weekday λ* #Weekday λ* e
+(Wednesday) = #Weekday λ* #Weekday λ* #Weekday λc #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* c
 
 (Thursday) = #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λd #Weekday λ* #Weekday λ* #Weekday λ* d
 
-(Wednesday) = #Weekday λ* #Weekday λ* #Weekday λc #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* c
+(Friday) = #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λe #Weekday λ* #Weekday λ* e
 
-(Tuesday) = #Weekday λ* #Weekday λb #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* b
+(Saturday) = #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λf #Weekday λ* f
 
-(Monday) = #Weekday λa #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* a
+(Sunday) = #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λ* #Weekday λg g
 
 Scott:
 (main) = (λa a Saturday)
 
-(Sunday) = λ* λ* λ* λ* λ* λ* λg g
+(Monday) = λa λ* λ* λ* λ* λ* λ* a
 
-(Saturday) = λ* λ* λ* λ* λ* λf λ* f
+(Tuesday) = λ* λb λ* λ* λ* λ* λ* b
 
-(Friday) = λ* λ* λ* λ* λe λ* λ* e
+(Wednesday) = λ* λ* λc λ* λ* λ* λ* c
 
 (Thursday) = λ* λ* λ* λd λ* λ* λ* d
 
-(Wednesday) = λ* λ* λc λ* λ* λ* λ* c
+(Friday) = λ* λ* λ* λ* λe λ* λ* e
 
-(Tuesday) = λ* λb λ* λ* λ* λ* λ* b
+(Saturday) = λ* λ* λ* λ* λ* λf λ* f
 
-(Monday) = λa λ* λ* λ* λ* λ* λ* a
+(Sunday) = λ* λ* λ* λ* λ* λ* λg g
diff --git a/tests/snapshots/simplify_matches__already_flat.hvm.snap b/tests/snapshots/simplify_matches__already_flat.hvm.snap
index f17f812af..725ffb1d3 100644
--- a/tests/snapshots/simplify_matches__already_flat.hvm.snap
+++ b/tests/snapshots/simplify_matches__already_flat.hvm.snap
@@ -14,20 +14,20 @@ input_file: tests/golden_tests/simplify_matches/already_flat.hvm
 
 (Rule6) = λa a
 
-(CtrB3) = λa #Baz λ* #Baz λ* #Baz λ* #Baz λe #Baz (e a)
+(CtrA) = #Foo λa #Foo λ* a
 
-(CtrB2) = λa #Baz λ* #Baz λ* #Baz λd #Baz λ* #Baz (d a)
+(CtrB) = λa #Foo λ* #Foo λc #Foo (c a)
 
-(CtrB1) = λa #Baz λ* #Baz λc #Baz λ* #Baz λ* #Baz (c a)
+(CtrA1) = λa #Bar λb #Bar λ* #Bar λ* #Bar (b a)
 
-(CtrB0) = #Baz λa #Baz λ* #Baz λ* #Baz λ* a
+(CtrA2) = λa λb #Bar λ* #Bar λd #Bar λ* #Bar (d a b)
 
 (CtrA3) = λa #Bar λ* #Bar λ* #Bar λd #Bar (d a)
 
-(CtrA2) = λa λb #Bar λ* #Bar λd #Bar λ* #Bar (d a b)
+(CtrB0) = #Baz λa #Baz λ* #Baz λ* #Baz λ* a
 
-(CtrA1) = λa #Bar λb #Bar λ* #Bar λ* #Bar (b a)
+(CtrB1) = λa #Baz λ* #Baz λc #Baz λ* #Baz λ* #Baz (c a)
 
-(CtrB) = λa #Foo λ* #Foo λc #Foo (c a)
+(CtrB2) = λa #Baz λ* #Baz λ* #Baz λd #Baz λ* #Baz (d a)
 
-(CtrA) = #Foo λa #Foo λ* a
+(CtrB3) = λa #Baz λ* #Baz λ* #Baz λ* #Baz λe #Baz (e a)
diff --git a/tests/snapshots/simplify_matches__bits_dec.hvm.snap b/tests/snapshots/simplify_matches__bits_dec.hvm.snap
index 8b024f424..a55750e2a 100644
--- a/tests/snapshots/simplify_matches__bits_dec.hvm.snap
+++ b/tests/snapshots/simplify_matches__bits_dec.hvm.snap
@@ -4,8 +4,8 @@ input_file: tests/golden_tests/simplify_matches/bits_dec.hvm
 ---
 (Data.Bits.dec) = λa match a { (Data.Bits.e): Data.Bits.e; (Data.Bits.o c): match c { (Data.Bits.e): Data.Bits.e; (Data.Bits.o e): (Data.Bits.i (Data.Bits.dec e)); (Data.Bits.i f): (Data.Bits.i (Data.Bits.dec f)) }; (Data.Bits.i g): match g { (Data.Bits.e): (Data.Bits.o Data.Bits.e); (Data.Bits.o i): (Data.Bits.o i); (Data.Bits.i j): (Data.Bits.o j) } }
 
-(Data.Bits.i) = λa #Data.Bits λ* #Data.Bits λ* #Data.Bits λd #Data.Bits (d a)
+(Data.Bits.e) = #Data.Bits λa #Data.Bits λ* #Data.Bits λ* a
 
 (Data.Bits.o) = λa #Data.Bits λ* #Data.Bits λc #Data.Bits λ* #Data.Bits (c a)
 
-(Data.Bits.e) = #Data.Bits λa #Data.Bits λ* #Data.Bits λ* a
+(Data.Bits.i) = λa #Data.Bits λ* #Data.Bits λ* #Data.Bits λd #Data.Bits (d a)
diff --git a/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap b/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap
index bbaa9329f..f652b8439 100644
--- a/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap
+++ b/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap
@@ -6,6 +6,6 @@ input_file: tests/golden_tests/simplify_matches/double_unwrap_maybe.hvm
 
 (Main) = (DoubleUnwrap (Some None) 5)
 
-(None) = #Maybe λ* #Maybe λb b
-
 (Some) = λa #Maybe λb #Maybe λ* #Maybe (b a)
+
+(None) = #Maybe λ* #Maybe λb b
diff --git a/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap b/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap
index 0ab34d346..e4b9d1c79 100644
--- a/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap
+++ b/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap
@@ -6,6 +6,6 @@ input_file: tests/golden_tests/simplify_matches/flatten_with_terminal.hvm
 
 (main) = (Foo 2 (A B))
 
-(B) = #B_t λa a
-
 (A) = λa #A_t λb #A_t (b a)
+
+(B) = #B_t λa a
diff --git a/tests/snapshots/simplify_matches__nested.hvm.snap b/tests/snapshots/simplify_matches__nested.hvm.snap
index 05498d595..35d5439d2 100644
--- a/tests/snapshots/simplify_matches__nested.hvm.snap
+++ b/tests/snapshots/simplify_matches__nested.hvm.snap
@@ -4,12 +4,12 @@ input_file: tests/golden_tests/simplify_matches/nested.hvm
 ---
 (Rule) = λa match a { (CtrA b c): (match c { (CtrB1 d): λe (e d); (CtrB2 f g): λh (match f { (CtrC): λi λj (i j) } h g) } b); (CtrB l): l }
 
-(CtrC) = #Baz λa a
+(CtrA) = λa λb #Foo λc #Foo λ* #Foo (c a b)
 
-(CtrB2) = λa λb #Bar λ* #Bar λd #Bar (d a b)
+(CtrB) = λa #Foo λ* #Foo λc #Foo (c a)
 
 (CtrB1) = λa #Bar λb #Bar λ* #Bar (b a)
 
-(CtrB) = λa #Foo λ* #Foo λc #Foo (c a)
+(CtrB2) = λa λb #Bar λ* #Bar λd #Bar (d a b)
 
-(CtrA) = λa λb #Foo λc #Foo λ* #Foo (c a b)
+(CtrC) = #Baz λa a
diff --git a/tests/snapshots/simplify_matches__nested_0ary.hvm.snap b/tests/snapshots/simplify_matches__nested_0ary.hvm.snap
index 724e58121..8cbee2793 100644
--- a/tests/snapshots/simplify_matches__nested_0ary.hvm.snap
+++ b/tests/snapshots/simplify_matches__nested_0ary.hvm.snap
@@ -4,6 +4,6 @@ input_file: tests/golden_tests/simplify_matches/nested_0ary.hvm
 ---
 (Unpack) = λa λb (match b { (Cons c d): λe (match d { (Cons f g): λh λi (h (Cons i (Cons f g))); (Nil): λ* λk k } e c); (Nil): λ* Nil } a)
 
-(Nil) = #list λ* #list λb b
-
 (Cons) = λa λb #list λc #list λ* #list (c a b)
+
+(Nil) = #list λ* #list λb b