From 7697acd137a8526f5df9d09efa1e24f62d965203 Mon Sep 17 00:00:00 2001
From: Nicolas Abril <nicolas.abril@protonmail.ch>
Date: Wed, 29 May 2024 09:15:13 +0200
Subject: [PATCH] Make with clauses take a bind and an argument

---
 src/fun/check/unbound_vars.rs                 |   2 +
 src/fun/display.rs                            |  58 +++--
 src/fun/mod.rs                                | 217 +++++++-----------
 src/fun/net_to_term.rs                        |  14 +-
 src/fun/parser.rs                             |  67 +++---
 src/fun/term_to_net.rs                        |  13 +-
 src/fun/transform/desugar_bend.rs             |  13 +-
 src/fun/transform/desugar_fold.rs             |  21 +-
 src/fun/transform/desugar_match_defs.rs       |  14 +-
 src/fun/transform/desugar_open.rs             |   3 +-
 src/fun/transform/encode_adts.rs              |   2 +-
 src/fun/transform/encode_match_terms.rs       |  32 ++-
 src/fun/transform/fix_match_terms.rs          |   9 +-
 src/fun/transform/float_combinators.rs        |  10 +-
 src/fun/transform/linearize_matches.rs        | 141 +++++++-----
 src/fun/transform/linearize_vars.rs           |  53 ++++-
 src/fun/transform/unique_names.rs             | 134 +++++++++--
 src/imp/gen_map_get.rs                        |  27 ++-
 src/imp/mod.rs                                |  27 ++-
 src/imp/order_kwargs.rs                       |  16 +-
 src/imp/parser.rs                             |  80 ++++---
 src/imp/to_fun.rs                             |  42 ++--
 src/lib.rs                                    |   3 +-
 tests/golden_tests.rs                         |   8 +
 .../definition_merge.bend                     |   4 +-
 .../run_file/list_reverse_imp.bend            |  14 ++
 .../encode_pattern_match__bool.bend.snap      |  16 +-
 ...encode_pattern_match__concat_def.bend.snap |   4 +-
 ..._pattern_match__definition_merge.bend.snap |  16 +-
 ...e_pattern_match__flatten_era_pat.bend.snap |   4 +-
 ...e_pattern_match__list_merge_sort.bend.snap |  12 +-
 .../run_file__list_reverse_imp.bend.snap      |   9 +
 .../simplify_matches__already_flat.bend.snap  |   2 +-
 ...plify_matches__double_unwrap_box.bend.snap |   2 +-
 ...ify_matches__double_unwrap_maybe.bend.snap |   2 +-
 ...y_matches__flatten_with_terminal.bend.snap |   2 +-
 ...ify_matches__linearize_match_all.bend.snap |   2 +-
 ...lify_matches__redundant_with_era.bend.snap |   2 +-
 38 files changed, 687 insertions(+), 410 deletions(-)
 create mode 100644 tests/golden_tests/run_file/list_reverse_imp.bend
 create mode 100644 tests/snapshots/run_file__list_reverse_imp.bend.snap

diff --git a/src/fun/check/unbound_vars.rs b/src/fun/check/unbound_vars.rs
index d8baba9a..414a69e4 100644
--- a/src/fun/check/unbound_vars.rs
+++ b/src/fun/check/unbound_vars.rs
@@ -78,7 +78,9 @@ pub fn check_uses<'a>(
       if let Some(pat) = term.pattern() {
         check_global_binds(pat, globals)
       }
+      //eprintln!("\nterm: {}", term);
       for (child, binds) in term.children_mut_with_binds() {
+        //eprintln!("child: {}\nbinds: {:?}", child, binds.clone().collect::<Vec<_>>());
         for bind in binds.clone() {
           push_scope(bind.as_ref(), scope);
         }
diff --git a/src/fun/display.rs b/src/fun/display.rs
index 29c9b68c..d08b3c9f 100644
--- a/src/fun/display.rs
+++ b/src/fun/display.rs
@@ -59,14 +59,17 @@ impl fmt::Display for Term {
       Term::App { tag, fun, arg } => {
         write!(f, "{}({} {})", tag.display_padded(), fun.display_app(tag), arg)
       }
-      Term::Mat { arg, bnd, with, arms } => {
+      Term::Mat { arg, bnd, with_bnd, with_arg, arms } => {
         write!(f, "match ")?;
         if let Some(bnd) = bnd {
           write!(f, "{} = ", bnd)?;
         }
         write!(f, "{} ", arg)?;
-        if !with.is_empty() {
-          write!(f, "with {} ", DisplayJoin(|| with, ", "))?;
+        if !with_bnd.is_empty() {
+          write!(f, "with ")?;
+          for (bnd, arg) in with_bnd.iter().zip(with_arg.iter()) {
+            write!(f, "{} = {}, ", var_as_str(bnd), arg)?;
+          }
         }
         write!(f, "{{ ")?;
         for arm in arms {
@@ -78,14 +81,17 @@ impl fmt::Display for Term {
         }
         write!(f, "}}")
       }
-      Term::Swt { arg, bnd, with, pred, arms } => {
+      Term::Swt { arg, bnd, with_bnd, with_arg, pred, arms } => {
         write!(f, "switch ")?;
         if let Some(bnd) = bnd {
           write!(f, "{bnd} = ")?;
         }
         write!(f, "{arg} ")?;
-        if !with.is_empty() {
-          write!(f, "with {} ", DisplayJoin(|| with, ", "))?;
+        if !with_bnd.is_empty() {
+          write!(f, "with ")?;
+          for (bnd, arg) in with_bnd.iter().zip(with_arg.iter()) {
+            write!(f, "{} = {}, ", var_as_str(bnd), arg)?;
+          }
         }
         write!(f, "{{ ")?;
         for (i, arm) in arms.iter().enumerate() {
@@ -101,14 +107,17 @@ impl fmt::Display for Term {
         }
         write!(f, "}}")
       }
-      Term::Fold { bnd, arg, with, arms } => {
+      Term::Fold { bnd, arg, with_bnd, with_arg, arms } => {
         write!(f, "fold ")?;
         if let Some(bnd) = bnd {
           write!(f, "{} = ", bnd)?;
         }
         write!(f, "{} ", arg)?;
-        if !with.is_empty() {
-          write!(f, "with {} ", DisplayJoin(|| with, ", "))?;
+        if !with_bnd.is_empty() {
+          write!(f, "with ")?;
+          for (bnd, arg) in with_bnd.iter().zip(with_arg.iter()) {
+            write!(f, "{} = {}, ", var_as_str(bnd), arg)?;
+          }
         }
         write!(f, "{{ ")?;
         for arm in arms {
@@ -120,7 +129,7 @@ impl fmt::Display for Term {
         }
         write!(f, "}}")
       }
-      Term::Bend { bind, init, cond, step, base } => {
+      Term::Bend { bnd: bind, arg: init, cond, step, base } => {
         write!(f, "bend ")?;
         for (bind, init) in bind.iter().zip(init) {
           if let Some(bind) = bind {
@@ -339,14 +348,17 @@ impl Term {
         Term::Oper { opr, fst, snd } => {
           write!(f, "({} {} {})", opr, fst.display_pretty(tab), snd.display_pretty(tab))
         }
-        Term::Mat { bnd, arg, with, arms } => {
+        Term::Mat { bnd, arg, with_bnd, with_arg, arms } => {
           write!(f, "match ")?;
           if let Some(bnd) = bnd {
             write!(f, "{} = ", bnd)?;
           }
           write!(f, "{} ", arg.display_pretty(tab))?;
-          if !with.is_empty() {
-            write!(f, "with {} ", DisplayJoin(|| with, ", "))?;
+          if !with_bnd.is_empty() {
+            write!(f, "with ")?;
+            for (bnd, arg) in with_bnd.iter().zip(with_arg.iter()) {
+              write!(f, "{} = {}, ", var_as_str(bnd), arg)?;
+            }
           }
           write!(f, "{{ ")?;
           for arm in arms {
@@ -358,14 +370,17 @@ impl Term {
           }
           write!(f, "\n{:tab$}}}", "")
         }
-        Term::Swt { bnd, arg, with, pred, arms } => {
+        Term::Swt { bnd, arg, with_bnd, with_arg, pred, arms } => {
           write!(f, "switch ")?;
           if let Some(bnd) = bnd {
             write!(f, "{bnd} = ")?;
           }
           write!(f, "{} ", arg.display_pretty(tab))?;
-          if !with.is_empty() {
-            write!(f, "with {} ", DisplayJoin(|| with, ", "))?;
+          if !with_bnd.is_empty() {
+            write!(f, "with ")?;
+            for (bnd, arg) in with_bnd.iter().zip(with_arg.iter()) {
+              write!(f, "{} = {}, ", var_as_str(bnd), arg)?;
+            }
           }
           writeln!(f, "{{")?;
           for (i, arm) in arms.iter().enumerate() {
@@ -381,14 +396,17 @@ impl Term {
           }
           write!(f, "{:tab$}}}", "")
         }
-        Term::Fold { bnd, arg, with, arms } => {
+        Term::Fold { bnd, arg, with_bnd, with_arg, arms } => {
           write!(f, "fold ")?;
           if let Some(bnd) = bnd {
             write!(f, "{} = ", bnd)?;
           }
           write!(f, "{} ", arg.display_pretty(tab))?;
-          if !with.is_empty() {
-            write!(f, "with {} ", DisplayJoin(|| with, ", "))?;
+          if !with_bnd.is_empty() {
+            write!(f, "with ")?;
+            for (bnd, arg) in with_bnd.iter().zip(with_arg.iter()) {
+              write!(f, "{} = {}, ", var_as_str(bnd), arg)?;
+            }
           }
           write!(f, "{{ ")?;
           for arm in arms {
@@ -400,7 +418,7 @@ impl Term {
           }
           write!(f, "\n{:tab$}}}", "")
         }
-        Term::Bend { bind, init, cond, step, base } => {
+        Term::Bend { bnd: bind, arg: init, cond, step, base } => {
           write!(f, "bend ")?;
           for (bind, init) in bind.iter().zip(init) {
             if let Some(bind) = bind {
diff --git a/src/fun/mod.rs b/src/fun/mod.rs
index afd29b14..4a1ad00b 100644
--- a/src/fun/mod.rs
+++ b/src/fun/mod.rs
@@ -130,28 +130,31 @@ pub enum Term {
   },
   /// Pattern matching on an ADT.
   Mat {
-    arg: Box<Term>,
     bnd: Option<Name>,
-    with: Vec<Name>,
+    arg: Box<Term>,
+    with_bnd: Vec<Option<Name>>,
+    with_arg: Vec<Term>,
     arms: Vec<MatchRule>,
   },
   /// Native pattern matching on numbers
   Swt {
-    arg: Box<Term>,
     bnd: Option<Name>,
-    with: Vec<Name>,
+    arg: Box<Term>,
+    with_bnd: Vec<Option<Name>>,
+    with_arg: Vec<Term>,
     pred: Option<Name>,
     arms: Vec<Term>,
   },
   Fold {
     bnd: Option<Name>,
     arg: Box<Term>,
-    with: Vec<Name>,
+    with_bnd: Vec<Option<Name>>,
+    with_arg: Vec<Term>,
     arms: Vec<MatchRule>,
   },
   Bend {
-    bind: Vec<Option<Name>>,
-    init: Vec<Term>,
+    bnd: Vec<Option<Name>>,
+    arg: Vec<Term>,
     cond: Box<Term>,
     step: Box<Term>,
     base: Box<Term>,
@@ -326,22 +329,31 @@ impl Clone for Term {
       Self::Str { val } => Self::Str { val: val.clone() },
       Self::List { els } => Self::List { els: els.clone() },
       Self::Oper { opr, fst, snd } => Self::Oper { opr: *opr, fst: fst.clone(), snd: snd.clone() },
-      Self::Mat { arg, bnd, with, arms } => {
-        Self::Mat { arg: arg.clone(), bnd: bnd.clone(), with: with.clone(), arms: arms.clone() }
-      }
-      Self::Swt { arg, bnd, with, pred, arms } => Self::Swt {
+      Self::Mat { arg, bnd, with_bnd, with_arg, arms } => Self::Mat {
         arg: arg.clone(),
         bnd: bnd.clone(),
-        with: with.clone(),
+        with_bnd: with_bnd.clone(),
+        with_arg: with_arg.clone(),
+        arms: arms.clone(),
+      },
+      Self::Swt { arg, bnd, with_bnd, with_arg, pred, arms } => Self::Swt {
+        arg: arg.clone(),
+        bnd: bnd.clone(),
+        with_bnd: with_bnd.clone(),
+        with_arg: with_arg.clone(),
         pred: pred.clone(),
         arms: arms.clone(),
       },
-      Self::Fold { bnd, arg, with, arms } => {
-        Self::Fold { bnd: bnd.clone(), arg: arg.clone(), with: with.clone(), arms: arms.clone() }
-      }
-      Self::Bend { bind, init, cond, step, base } => Self::Bend {
-        bind: bind.clone(),
-        init: init.clone(),
+      Self::Fold { bnd, arg, with_bnd, with_arg, arms } => Self::Fold {
+        bnd: bnd.clone(),
+        arg: arg.clone(),
+        with_bnd: with_bnd.clone(),
+        with_arg: with_arg.clone(),
+        arms: arms.clone(),
+      },
+      Self::Bend { bnd: bind, arg: init, cond, step, base } => Self::Bend {
+        bnd: bind.clone(),
+        arg: init.clone(),
         cond: cond.clone(),
         step: step.clone(),
         base: base.clone(),
@@ -412,6 +424,8 @@ impl Term {
   }
 
   /// Wraps a term in lambdas, so that the outermost lambda is the first given element.
+  ///
+  /// The lambda equivalent of [`Term::call`].
   pub fn rfold_lams(term: Term, pats: impl DoubleEndedIterator<Item = Option<Name>>) -> Self {
     pats.into_iter().rfold(term, |bod, nam| Self::lam(Pattern::Var(nam), bod))
   }
@@ -488,17 +502,17 @@ impl Term {
   pub fn children(&self) -> impl DoubleEndedIterator<Item = &Term> + Clone {
     multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt, Bend, Fold });
     match self {
-      Term::Mat { arg, bnd: _, with: _, arms } => {
-        ChildrenIter::Mat([arg.as_ref()].into_iter().chain(arms.iter().map(|r| &r.2)))
+      Term::Mat { arg, bnd: _, with_bnd: _, with_arg, arms } => {
+        ChildrenIter::Mat([arg.as_ref()].into_iter().chain(with_arg.iter()).chain(arms.iter().map(|r| &r.2)))
       }
-      Term::Swt { arg, bnd: _, with: _, pred: _, arms } => {
-        ChildrenIter::Swt([arg.as_ref()].into_iter().chain(arms))
+      Term::Swt { arg, bnd: _, with_bnd: _, with_arg, pred: _, arms } => {
+        ChildrenIter::Swt([arg.as_ref()].into_iter().chain(with_arg.iter()).chain(arms))
       }
-      Term::Bend { bind: _, init, cond, step, base } => {
+      Term::Bend { bnd: _, arg: init, cond, step, base } => {
         ChildrenIter::Bend(init.iter().chain([cond.as_ref(), step.as_ref(), base.as_ref()]))
       }
-      Term::Fold { bnd: _, arg, with: _, arms } => {
-        ChildrenIter::Fold([arg.as_ref()].into_iter().chain(arms.iter().map(|r| &r.2)))
+      Term::Fold { bnd: _, arg, with_bnd: _, with_arg, arms } => {
+        ChildrenIter::Fold([arg.as_ref()].into_iter().chain(with_arg.iter()).chain(arms.iter().map(|r| &r.2)))
       }
       Term::Fan { els, .. } | Term::List { els } => ChildrenIter::Vec(els),
       Term::Let { val: fst, nxt: snd, .. }
@@ -523,18 +537,18 @@ impl Term {
   pub fn children_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Term> {
     multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt, Bend, Fold });
     match self {
-      Term::Mat { arg, bnd: _, with: _, arms } => {
-        ChildrenIter::Mat([arg.as_mut()].into_iter().chain(arms.iter_mut().map(|r| &mut r.2)))
+      Term::Mat { arg, bnd: _, with_bnd: _, with_arg, arms } => ChildrenIter::Mat(
+        [arg.as_mut()].into_iter().chain(with_arg.iter_mut()).chain(arms.iter_mut().map(|r| &mut r.2)),
+      ),
+      Term::Swt { arg, bnd: _, with_bnd: _, with_arg, pred: _, arms } => {
+        ChildrenIter::Swt([arg.as_mut()].into_iter().chain(with_arg.iter_mut()).chain(arms))
       }
-      Term::Swt { arg, bnd: _, with: _, pred: _, arms } => {
-        ChildrenIter::Swt([arg.as_mut()].into_iter().chain(arms))
-      }
-      Term::Bend { bind: _, init, cond, step, base } => {
+      Term::Bend { bnd: _, arg: init, cond, step, base } => {
         ChildrenIter::Bend(init.iter_mut().chain([cond.as_mut(), step.as_mut(), base.as_mut()]))
       }
-      Term::Fold { bnd: _, arg, with: _, arms } => {
-        ChildrenIter::Fold([arg.as_mut()].into_iter().chain(arms.iter_mut().map(|r| &mut r.2)))
-      }
+      Term::Fold { bnd: _, arg, with_bnd: _, with_arg, arms } => ChildrenIter::Fold(
+        [arg.as_mut()].into_iter().chain(with_arg.iter_mut()).chain(arms.iter_mut().map(|r| &mut r.2)),
+      ),
       Term::Fan { els, .. } | Term::List { els } => ChildrenIter::Vec(els),
       Term::Let { val: fst, nxt: snd, .. }
       | Term::Ask { val: fst, nxt: snd, .. }
@@ -567,35 +581,36 @@ impl Term {
     &self,
   ) -> impl DoubleEndedIterator<Item = (&Term, impl DoubleEndedIterator<Item = &Option<Name>> + Clone)> + Clone
   {
-    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt, Bend, Fold });
-    multi_iterator!(BindsIter { Zero, One, Mat, Pat, Bend });
+    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt, Bend });
+    multi_iterator!(BindsIter { Zero, One, Mat, Pat, SwtNum, SwtSucc, Bend });
     match self {
-      Term::Mat { arg, bnd: _, with: _, arms } => ChildrenIter::Mat(
-        [(arg.as_ref(), BindsIter::Zero([]))]
-          .into_iter()
-          .chain(arms.iter().map(move |r| (&r.2, BindsIter::Mat(r.1.iter())))),
-      ),
-      Term::Swt { arg, bnd: _, with: _, pred, arms } => {
+      Term::Mat { arg, bnd, with_bnd, with_arg, arms }
+      | Term::Fold { bnd, arg, with_bnd, with_arg, arms } => {
+        let arg = [(arg.as_ref(), BindsIter::Zero([]))].into_iter();
+        let with_arg = with_arg.iter().map(|a| (a, BindsIter::Zero([])));
+        let arms = arms
+          .iter()
+          .map(move |r| (&r.2, BindsIter::Mat([bnd].into_iter().chain(r.1.iter()).chain(with_bnd.iter()))));
+        ChildrenIter::Mat(arg.chain(with_arg).chain(arms))
+      }
+      Term::Swt { arg, bnd, with_bnd, with_arg, pred, arms } => {
         let (succ, nums) = arms.split_last().unwrap();
         ChildrenIter::Swt(
           [(arg.as_ref(), BindsIter::Zero([]))]
             .into_iter()
-            .chain(nums.iter().map(move |x| (x, BindsIter::Zero([]))))
-            .chain([(succ, BindsIter::One([pred]))]),
+            .chain(with_arg.iter().map(|a| (a, BindsIter::Zero([]))))
+            .chain(nums.iter().map(move |x| (x, BindsIter::SwtNum([bnd].into_iter().chain(with_bnd.iter())))))
+            .chain([(succ, BindsIter::SwtSucc([bnd, pred].into_iter().chain(with_bnd.iter())))]),
         )
       }
-      Term::Bend { bind, init, cond, step, base } => {
+      Term::Bend { bnd: bind, arg: init, cond, step, base } => {
         ChildrenIter::Bend(init.iter().map(|x| (x, BindsIter::Zero([]))).chain([
           (cond.as_ref(), BindsIter::Bend(bind.iter())),
           (step.as_ref(), BindsIter::Bend(bind.iter())),
           (base.as_ref(), BindsIter::Bend(bind.iter())),
         ]))
       }
-      Term::Fold { bnd: _, arg, with: _, arms } => ChildrenIter::Fold(
-        [(arg.as_ref(), BindsIter::Zero([]))]
-          .into_iter()
-          .chain(arms.iter().map(move |r| (&r.2, BindsIter::Mat(r.1.iter())))),
-      ),
+
       Term::Fan { els, .. } | Term::List { els } => {
         ChildrenIter::Vec(els.iter().map(|el| (el, BindsIter::Zero([]))))
       }
@@ -627,35 +642,38 @@ impl Term {
     &mut self,
   ) -> impl DoubleEndedIterator<Item = (&mut Term, impl DoubleEndedIterator<Item = &Option<Name>> + Clone)>
   {
-    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt, Bend, Fold });
-    multi_iterator!(BindsIter { Zero, One, Mat, Pat, Bend });
+    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt, Bend });
+    multi_iterator!(BindsIter { Zero, One, Mat, SwtNum, SwtSucc, Pat, Bend });
     match self {
-      Term::Mat { arg, bnd: _, with: _, arms: rules } => ChildrenIter::Mat(
-        [(arg.as_mut(), BindsIter::Zero([]))]
-          .into_iter()
-          .chain(rules.iter_mut().map(move |r| (&mut r.2, BindsIter::Mat(r.1.iter())))),
-      ),
-      Term::Swt { arg, bnd: _, with: _, pred, arms: rules } => {
-        let (succ, nums) = rules.split_last_mut().unwrap();
+      Term::Mat { arg, bnd, with_bnd, with_arg, arms }
+      | Term::Fold { bnd, arg, with_bnd, with_arg, arms } => {
+        let arg = [(arg.as_mut(), BindsIter::Zero([]))].into_iter();
+        let with_arg = with_arg.iter_mut().map(|a| (a, BindsIter::Zero([])));
+        let arms = arms
+          .iter_mut()
+          .map(|r| (&mut r.2, BindsIter::Mat([&*bnd].into_iter().chain(r.1.iter()).chain(with_bnd.iter()))));
+        ChildrenIter::Mat(arg.chain(with_arg).chain(arms))
+      }
+      Term::Swt { arg, bnd, with_bnd, with_arg, pred, arms } => {
+        let (succ, nums) = arms.split_last_mut().unwrap();
         ChildrenIter::Swt(
           [(arg.as_mut(), BindsIter::Zero([]))]
             .into_iter()
-            .chain(nums.iter_mut().map(move |x| (x, BindsIter::Zero([]))))
-            .chain([(succ, BindsIter::One([&*pred]))]),
+            .chain(with_arg.iter_mut().map(|a| (a, BindsIter::Zero([]))))
+            .chain(
+              nums.iter_mut().map(|x| (x, BindsIter::SwtNum([&*bnd].into_iter().chain(with_bnd.iter())))),
+            )
+            .chain([(succ, BindsIter::SwtSucc([&*bnd, &*pred].into_iter().chain(with_bnd.iter())))]),
         )
       }
-      Term::Bend { bind, init, cond, step, base } => {
-        ChildrenIter::Bend(init.iter_mut().map(|x| (x, BindsIter::Zero([]))).chain([
-          (cond.as_mut(), BindsIter::Bend(bind.iter())),
-          (step.as_mut(), BindsIter::Bend(bind.iter())),
-          (base.as_mut(), BindsIter::Bend(bind.iter())),
+      Term::Bend { bnd, arg, cond, step, base } => {
+        ChildrenIter::Bend(arg.iter_mut().map(|x| (x, BindsIter::Zero([]))).chain([
+          (cond.as_mut(), BindsIter::Bend(bnd.iter())),
+          (step.as_mut(), BindsIter::Bend(bnd.iter())),
+          (base.as_mut(), BindsIter::Bend(bnd.iter())),
         ]))
       }
-      Term::Fold { bnd: _, arg, with: _, arms } => ChildrenIter::Fold(
-        [(arg.as_mut(), BindsIter::Zero([]))]
-          .into_iter()
-          .chain(arms.iter_mut().map(move |r| (&mut r.2, BindsIter::Mat(r.1.iter())))),
-      ),
+
       Term::Fan { els, .. } | Term::List { els } => {
         ChildrenIter::Vec(els.iter_mut().map(|el| (el, BindsIter::Zero([]))))
       }
@@ -681,63 +699,6 @@ impl Term {
       Term::Open { .. } => unreachable!("Open should be removed in earlier pass"),
     }
   }
-
-  /// Must only be called after fix_matches.
-  pub fn children_mut_with_binds_mut(
-    &mut self,
-  ) -> impl DoubleEndedIterator<Item = (&mut Term, impl DoubleEndedIterator<Item = &mut Option<Name>>)> {
-    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt, Fold });
-    multi_iterator!(BindsIter { Zero, One, Mat, Pat });
-    match self {
-      Term::Mat { arg, bnd: _, with: _, arms: rules } => ChildrenIter::Mat(
-        [(arg.as_mut(), BindsIter::Zero([]))]
-          .into_iter()
-          .chain(rules.iter_mut().map(move |r| (&mut r.2, BindsIter::Mat(r.1.iter_mut())))),
-      ),
-      Term::Swt { arg, bnd: _, with: _, pred, arms: rules } => {
-        let (succ, nums) = rules.split_last_mut().unwrap();
-        ChildrenIter::Swt(
-          [(arg.as_mut(), BindsIter::Zero([]))]
-            .into_iter()
-            .chain(nums.iter_mut().map(move |x| (x, BindsIter::Zero([]))))
-            .chain([(succ, BindsIter::One([pred]))]),
-        )
-      }
-      Term::Bend { .. } => {
-        unreachable!("Term::Bend can't implement children_mut_with_binds_mut")
-      }
-      Term::Fold { bnd: _, arg, with: _, arms } => ChildrenIter::Fold(
-        [(arg.as_mut(), BindsIter::Zero([]))]
-          .into_iter()
-          .chain(arms.iter_mut().map(move |r| (&mut r.2, BindsIter::Mat(r.1.iter_mut())))),
-      ),
-      Term::Fan { els, .. } | Term::List { els } => {
-        ChildrenIter::Vec(els.iter_mut().map(|el| (el, BindsIter::Zero([]))))
-      }
-      Term::Use { nam, val, nxt } => {
-        ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::One([nam]))])
-      }
-      Term::Let { pat, val, nxt, .. } | Term::Ask { pat, val, nxt, .. } => ChildrenIter::Two([
-        (val.as_mut(), BindsIter::Zero([])),
-        (nxt.as_mut(), BindsIter::Pat(pat.binds_mut())),
-      ]),
-      Term::App { fun: fst, arg: snd, .. } | Term::Oper { fst, snd, .. } => {
-        ChildrenIter::Two([(fst.as_mut(), BindsIter::Zero([])), (snd.as_mut(), BindsIter::Zero([]))])
-      }
-      Term::Lam { pat, bod, .. } => ChildrenIter::One([(bod.as_mut(), BindsIter::Pat(pat.binds_mut()))]),
-      Term::With { bod, .. } => ChildrenIter::One([(bod.as_mut(), BindsIter::Zero([]))]),
-      Term::Var { .. }
-      | Term::Link { .. }
-      | Term::Num { .. }
-      | Term::Nat { .. }
-      | Term::Str { .. }
-      | Term::Ref { .. }
-      | Term::Era
-      | Term::Err => ChildrenIter::Zero([]),
-      Term::Open { .. } => unreachable!("Open should be removed in earlier pass"),
-    }
-  }
-
   /* Common checks and transformations */
 
   /// Substitute the occurrences of a variable in a term with the given term.
diff --git a/src/fun/net_to_term.rs b/src/fun/net_to_term.rs
index 8ecf3c16..d1273d09 100644
--- a/src/fun/net_to_term.rs
+++ b/src/fun/net_to_term.rs
@@ -161,7 +161,14 @@ impl Reader<'_> {
                 (zero_term, succ_term)
               }
             };
-            Term::Swt { arg: Box::new(arg), bnd: Some(bnd), with: vec![], pred: None, arms: vec![zero, succ] }
+            Term::Swt {
+              arg: Box::new(arg),
+              bnd: Some(bnd),
+              with_arg: vec![],
+              with_bnd: vec![],
+              pred: None,
+              arms: vec![zero, succ],
+            }
           }
           _ => {
             self.error(ReadbackError::InvalidNumericMatch);
@@ -588,8 +595,11 @@ impl Term {
   pub fn collect_unscoped(&self, unscoped: &mut HashSet<Name>, scope: &mut Vec<Name>) {
     maybe_grow(|| match self {
       Term::Var { nam } if !scope.contains(nam) => _ = unscoped.insert(nam.clone()),
-      Term::Swt { arg, bnd, with: _, pred: _, arms } => {
+      Term::Swt { arg, bnd, with_bnd: _, with_arg, pred: _, arms } => {
         arg.collect_unscoped(unscoped, scope);
+        for arg in with_arg {
+          arg.collect_unscoped(unscoped, scope);
+        }
         arms[0].collect_unscoped(unscoped, scope);
         if let Some(bnd) = bnd {
           scope.push(Name::new(format!("{bnd}-1")));
diff --git a/src/fun/parser.rs b/src/fun/parser.rs
index 4de18bcb..b5a37512 100644
--- a/src/fun/parser.rs
+++ b/src/fun/parser.rs
@@ -16,7 +16,7 @@ use TSPL::Parser;
 // <Pattern>    ::= "(" <Name> <Pattern>* ")" | <NameEra> | <Number> | "(" <Pattern> ("," <Pattern>)+ ")"
 // <Term>       ::=
 //   <Number> | <NumOp> | <Tup> | <App> | <Group> | <Nat> | <Lam> | <UnscopedLam> | <Bend> | <Fold> |
-//   <Use> | <Dup> | <LetTup> | <Let> | <Bind> | <Match> | <Switch> | <Era> | <UnscopedVar> | <Var>
+//   <Use> | <Dup> | <LetTup> | <Let> | <Do> | <Match> | <Switch> | <Era> | <UnscopedVar> | <Var>
 // <Lam>        ::= <Tag>? ("λ"|"@") <NameEra> <Term>
 // <UnscopedLam>::= <Tag>? ("λ"|"@") "$" <Name> <Term>
 // <NumOp>      ::= "(" <Operator> <Term> <Term> ")"
@@ -25,7 +25,7 @@ use TSPL::Parser;
 // <Group>      ::= "(" <Term> ")"
 // <Use>        ::= "use" <Name> "=" <Term> ";"? <Term>
 // <Let>        ::= "let" <NameEra> "=" <Term> ";"? <Term>
-// <Bind>       ::= "with" <Name> "{" <Ask> "}"
+// <With>       ::= "with" <Name> "{" <Ask> "}"
 // <Ask>        ::= "ask" <Pattern> "=" <Term> ";" <Term> | <Term>
 // <LetTup>     ::= "let" "(" <NameEra> ("," <NameEra>)+ ")" "=" <Term> ";"? <Term>
 // <Dup>        ::= "let" <Tag>? "{" <NameEra> (","? <NameEra>)+ "}" "=" <Term> ";"? <Term>
@@ -471,7 +471,8 @@ impl<'a> TermParser<'a> {
         return Ok(Term::Swt {
           arg: Box::new(cnd),
           bnd: Some(Name::new("%cond")),
-          with: Vec::new(),
+          with_bnd: Vec::new(),
+          with_arg: Vec::new(),
           pred: Some(Name::new("%cond-1")),
           arms: vec![els, thn],
         });
@@ -480,17 +481,18 @@ impl<'a> TermParser<'a> {
       // Match
       if self.try_parse_keyword("match") {
         unexpected_tag(self)?;
-        let (bnd, arg, with) = self.parse_match_header()?;
-        let arms = self.list_like(|p| p.parse_match_arm(), "{", "}", ";", false, 1)?;
-        return Ok(Term::Mat { arg: Box::new(arg), bnd, with, arms });
+        let (bnd, arg) = self.parse_match_arg()?;
+        let (with_bnd, with_arg) = self.parse_with_clause()?;
+        let arms = self.list_like(|p| p.parse_match_arm(), "", "}", ";", false, 1)?;
+        return Ok(Term::Mat { arg: Box::new(arg), bnd, with_bnd, with_arg, arms });
       }
 
       // Switch
       if self.try_parse_keyword("switch") {
         unexpected_tag(self)?;
-        let (bnd, arg, with) = self.parse_match_header()?;
+        let (bnd, arg) = self.parse_match_arg()?;
+        let (with_bnd, with_arg) = self.parse_with_clause()?;
 
-        self.consume("{")?;
         self.try_consume("|");
         self.consume("0")?;
         self.consume(":")?;
@@ -520,7 +522,7 @@ impl<'a> TermParser<'a> {
           self.try_consume(";");
         }
         let pred = Some(Name::new(format!("{}-{}", bnd.as_ref().unwrap(), arms.len() - 1)));
-        return Ok(Term::Swt { arg: Box::new(arg), bnd, with, pred, arms });
+        return Ok(Term::Swt { arg: Box::new(arg), bnd, with_bnd, with_arg, pred, arms });
       }
 
       // With (monadic block)
@@ -536,9 +538,10 @@ impl<'a> TermParser<'a> {
       // Fold
       if self.try_parse_keyword("fold") {
         unexpected_tag(self)?;
-        let (bnd, arg, with) = self.parse_match_header()?;
-        let arms = self.list_like(|p| p.parse_match_arm(), "{", "}", ";", false, 1)?;
-        return Ok(Term::Fold { arg: Box::new(arg), bnd, with, arms });
+        let (bnd, arg) = self.parse_match_arg()?;
+        let (with_bnd, with_arg) = self.parse_with_clause()?;
+        let arms = self.list_like(|p| p.parse_match_arm(), "", "}", ";", false, 1)?;
+        return Ok(Term::Fold { arg: Box::new(arg), bnd, with_bnd, with_arg, arms });
       }
 
       // Bend
@@ -569,8 +572,8 @@ impl<'a> TermParser<'a> {
         let base = self.parse_term()?;
         self.consume("}")?;
         return Ok(Term::Bend {
-          bind,
-          init,
+          bnd: bind,
+          arg: init,
           cond: Box::new(cond),
           step: Box::new(step),
           base: Box::new(base),
@@ -636,6 +639,7 @@ impl<'a> TermParser<'a> {
     }))
   }
 
+  // A named arg with optional name.
   fn parse_match_arg(&mut self) -> ParseResult<(Option<Name>, Term)> {
     let ini_idx = *self.index();
     let mut arg = self.parse_term()?;
@@ -653,24 +657,29 @@ impl<'a> TermParser<'a> {
     }
   }
 
-  fn parse_match_header(&mut self) -> ParseResult<(Option<Name>, Term, Vec<Name>)> {
-    let (bnd, arg) = self.parse_match_arg()?;
+  /// A named arg with non-optional name.
+  fn parse_named_arg(&mut self) -> ParseResult<(Option<Name>, Term)> {
+    let nam = self.parse_bend_name()?;
     self.skip_trivia();
-    let with = if self.try_parse_keyword("with") {
-      self.skip_trivia();
-      let mut with = vec![self.parse_bend_name()?];
-      self.skip_trivia();
-      while !self.starts_with("{") {
-        self.try_consume(",");
-        self.skip_trivia();
-        with.push(self.parse_bend_name()?);
-        self.skip_trivia();
-      }
-      with
+    if self.starts_with("=") {
+      self.advance_one();
+      let arg = self.parse_term()?;
+      Ok((Some(nam), arg))
     } else {
-      vec![]
+      let arg = Term::Var { nam: nam.clone() };
+      Ok((Some(nam), arg))
+    }
+  }
+
+  fn parse_with_clause(&mut self) -> ParseResult<(Vec<Option<Name>>, Vec<Term>)> {
+    self.skip_trivia();
+    let res = if self.try_parse_keyword("with") {
+      self.list_like(|p| p.parse_named_arg(), "", "{", ",", false, 1)?.into_iter().unzip()
+    } else {
+      self.consume_exactly("{")?;
+      (vec![], vec![])
     };
-    Ok((bnd, arg, with))
+    Ok(res)
   }
 
   fn parse_match_arm(&mut self) -> ParseResult<MatchRule> {
diff --git a/src/fun/term_to_net.rs b/src/fun/term_to_net.rs
index 405a9a55..6bbea650 100644
--- a/src/fun/term_to_net.rs
+++ b/src/fun/term_to_net.rs
@@ -137,10 +137,13 @@ impl<'t, 'l> EncodeTermState<'t, 'l> {
           self.link(up, node.2);
         }
         // core: & arg ~ ?<(zero succ) ret>
-        Term::Swt { arg, bnd: _, with, pred: _, arms: rules } => {
+        Term::Swt { arg, bnd, with_bnd, with_arg, pred, arms,  } => {
           // At this point should be only num matches of 0 and succ.
-          assert!(with.is_empty());
-          assert!(rules.len() == 2);
+          assert!(bnd.is_none());
+          assert!(with_bnd.is_empty());
+          assert!(with_arg.is_empty());
+          assert!(pred.is_none());
+          assert!(arms.len() == 2);
 
           self.created_nodes += 2;
           let loaned = Tree::Swi { fst: Box::new(Tree::Con{fst: Box::new(Tree::Era), snd: Box::new(Tree::Era)}), snd: Box::new(Tree::Era)};
@@ -152,8 +155,8 @@ impl<'t, 'l> EncodeTermState<'t, 'l> {
             });
 
           self.encode_term(arg, Place::Tree(node));
-          self.encode_term(&rules[0], Place::Hole(zero));
-          self.encode_term(&rules[1], Place::Hole(succ));
+          self.encode_term(&arms[0], Place::Hole(zero));
+          self.encode_term(&arms[1], Place::Hole(succ));
           self.link(up, Place::Hole(out));
         }
         Term::Let { pat, val, nxt } => {
diff --git a/src/fun/transform/desugar_bend.rs b/src/fun/transform/desugar_bend.rs
index 1d54c4ea..5febc7ee 100644
--- a/src/fun/transform/desugar_bend.rs
+++ b/src/fun/transform/desugar_bend.rs
@@ -48,7 +48,7 @@ impl Term {
         if self.has_unscoped_diff() {
           return Err("Can't have non self-contained unscoped variables in a 'bend'".into());
         }
-        let Term::Bend { bind, init, cond, step, base } = self else { unreachable!() };
+        let Term::Bend { bnd, arg, cond, step, base } = self else { unreachable!() };
 
         let new_nam = Name::new(format!("{}{}{}", def_name, NEW_FN_SEP, fresh));
         *fresh += 1;
@@ -59,8 +59,8 @@ impl Term {
         free_vars.remove(&Name::new(RECURSIVE_KW));
         free_vars.extend(base.free_vars());
         free_vars.extend(cond.free_vars());
-        for bind in bind.iter().flatten() {
-          free_vars.remove(bind);
+        for bnd in bnd.iter().flatten() {
+          free_vars.remove(bnd);
         }
         let free_vars = free_vars.into_keys().collect::<Vec<_>>();
 
@@ -78,11 +78,12 @@ impl Term {
         let body = Term::Swt {
           arg: Box::new(std::mem::take(cond)),
           bnd: Some(Name::new("_")),
-          with: vec![],
+          with_bnd: vec![],
+          with_arg: vec![],
           pred: Some(Name::new("_-1")),
           arms: vec![std::mem::take(base.as_mut()), step],
         };
-        let body = Term::rfold_lams(body, std::mem::take(bind).into_iter());
+        let body = Term::rfold_lams(body, std::mem::take(bnd).into_iter());
         let body = Term::rfold_lams(body, free_vars.iter().cloned().map(Some));
 
         // Make a definition from the new function
@@ -93,7 +94,7 @@ impl Term {
         // Call the new function in the original term.
         let call =
           Term::call(Term::Ref { nam: new_nam }, free_vars.iter().map(|v| Term::Var { nam: v.clone() }));
-        *self = Term::call(call, init.drain(..));
+        *self = Term::call(call, arg.drain(..));
       }
 
       Ok(())
diff --git a/src/fun/transform/desugar_fold.rs b/src/fun/transform/desugar_fold.rs
index 368a04d0..f1cdaccf 100644
--- a/src/fun/transform/desugar_fold.rs
+++ b/src/fun/transform/desugar_fold.rs
@@ -67,7 +67,7 @@ impl Term {
         if self.has_unscoped_diff() {
           return Err("Can't have non self-contained unscoped variables in a 'fold'".into());
         }
-        let Term::Fold { bnd: _, arg, with, arms } = self else { unreachable!() };
+        let Term::Fold { bnd: _, arg, with_bnd, with_arg, arms } = self else { unreachable!() };
 
         // Gather the free variables
         let mut free_vars = HashSet::new();
@@ -78,7 +78,7 @@ impl Term {
           }
           free_vars.extend(arm_free_vars);
         }
-        for var in with.iter() {
+        for var in with_bnd.iter().flatten() {
           free_vars.remove(var);
         }
         let free_vars = free_vars.into_iter().collect::<Vec<_>>();
@@ -103,19 +103,16 @@ impl Term {
 
         // Create the new function
         let x_nam = Name::new("%x");
-        let mut body = Term::Mat {
+        let body = Term::Mat {
           arg: Box::new(Term::Var { nam: x_nam.clone() }),
           bnd: None,
-          with: with.clone(),
+          with_bnd: with_bnd.clone(),
+          with_arg: with_bnd.iter().map(|nam| Term::var_or_era(nam.clone())).collect(),
           arms: std::mem::take(arms),
         };
-        for nam in with.iter().rev() {
-          body = Term::lam(Pattern::Var(Some(nam.clone())), body);
-        }
-        for nam in free_vars.iter().rev() {
-          body = Term::lam(Pattern::Var(Some(nam.clone())), body);
-        }
-        body = Term::lam(Pattern::Var(Some(x_nam)), body);
+        let body = Term::rfold_lams(body, with_bnd.iter().cloned());
+        let body = Term::rfold_lams(body, free_vars.iter().map(|nam| Some(nam.clone())));
+        let body = Term::lam(Pattern::Var(Some(x_nam)), body);
         let def =
           Definition { name: new_nam.clone(), rules: vec![Rule { pats: vec![], body }], builtin: false };
         new_defs.push(def);
@@ -123,7 +120,7 @@ impl Term {
         // Call the new function
         let call = Term::call(Term::Ref { nam: new_nam.clone() }, [std::mem::take(arg.as_mut())]);
         let call = Term::call(call, free_vars.iter().cloned().map(|nam| Term::Var { nam }));
-        let call = Term::call(call, with.iter().cloned().map(|nam| Term::Var { nam }));
+        let call = Term::call(call, with_arg.iter().cloned());
         *self = call;
       }
       Ok(())
diff --git a/src/fun/transform/desugar_match_defs.rs b/src/fun/transform/desugar_match_defs.rs
index c0a88941..26d5db1f 100644
--- a/src/fun/transform/desugar_match_defs.rs
+++ b/src/fun/transform/desugar_match_defs.rs
@@ -313,7 +313,9 @@ fn num_rule(
   let default_body = simplify_rule_match(args.clone(), new_rules, default_with, ctrs, adts)?;
 
   // Linearize previously matched vars and current args.
-  let swt_with = with.into_iter().chain(args).collect::<Vec<_>>();
+  let with = with.into_iter().chain(args).collect::<Vec<_>>();
+  let with_bnd = with.iter().cloned().map(Some).collect::<Vec<_>>();
+  let with_arg = with.iter().cloned().map(|nam| Term::Var { nam }).collect::<Vec<_>>();
 
   let term = num_bodies.into_iter().enumerate().rfold(default_body, |term, (i, body)| {
     let val = if i > 0 {
@@ -328,7 +330,8 @@ fn num_rule(
     Term::Swt {
       arg: Box::new(val),
       bnd: Some(arg.clone()),
-      with: swt_with.clone(),
+      with_bnd: with_bnd.clone(),
+      with_arg: with_arg.clone(),
       pred: Some(pred_var.clone()),
       arms: vec![body, term],
     }
@@ -448,12 +451,15 @@ fn switch_rule(
   }
 
   // Linearize previously matched vars and current args.
-  let mat_with = with.into_iter().chain(old_args).collect::<Vec<_>>();
+  let with = with.into_iter().chain(old_args).collect::<Vec<_>>();
+  let with_bnd = with.iter().cloned().map(Some).collect::<Vec<_>>();
+  let with_arg = with.iter().cloned().map(|nam| Term::Var { nam }).collect::<Vec<_>>();
 
   let term = Term::Mat {
     arg: Box::new(Term::Var { nam: arg.clone() }),
     bnd: Some(arg.clone()),
-    with: mat_with,
+    with_bnd,
+    with_arg,
     arms: new_arms,
   };
   Ok(term)
diff --git a/src/fun/transform/desugar_open.rs b/src/fun/transform/desugar_open.rs
index 576e733f..5210f648 100644
--- a/src/fun/transform/desugar_open.rs
+++ b/src/fun/transform/desugar_open.rs
@@ -30,7 +30,8 @@ impl Term {
             *self = Term::Mat {
               arg: Box::new(Term::Var { nam: var.clone() }),
               bnd: Some(std::mem::take(var)),
-              with: vec![],
+              with_bnd: vec![],
+              with_arg: vec![],
               arms: vec![(Some(ctr.clone()), vec![], std::mem::take(bod))],
             }
           } else {
diff --git a/src/fun/transform/encode_adts.rs b/src/fun/transform/encode_adts.rs
index b5b239d6..a65b0a7c 100644
--- a/src/fun/transform/encode_adts.rs
+++ b/src/fun/transform/encode_adts.rs
@@ -52,7 +52,7 @@ fn encode_ctr_scott<'a>(
   let ctr = Term::Var { nam: ctr_name.clone() };
   let app = Term::call(ctr, ctr_args.clone().cloned().map(|nam| Term::Var { nam }));
   let lam = Term::rfold_lams(app, ctrs.into_iter().map(Some));
-  ctr_args.cloned().rfold(lam, |acc, arg| Term::lam(Pattern::Var(Some(arg)), acc))
+  Term::rfold_lams(lam, ctr_args.cloned().map(Some))
 }
 
 fn encode_ctr_num_scott<'a>(ctr_args: impl DoubleEndedIterator<Item = &'a Name> + Clone, tag: &str) -> Term {
diff --git a/src/fun/transform/encode_match_terms.rs b/src/fun/transform/encode_match_terms.rs
index b3488b39..84ed5f67 100644
--- a/src/fun/transform/encode_match_terms.rs
+++ b/src/fun/transform/encode_match_terms.rs
@@ -28,16 +28,18 @@ impl Term {
         child.encode_matches(adt_encoding)
       }
 
-      if let Term::Mat { arg, bnd: _, with, arms: rules } = self {
-        assert!(with.is_empty());
+      if let Term::Mat { arg, bnd: _, with_bnd, with_arg, arms } = self {
+        assert!(with_bnd.is_empty());
+        assert!(with_arg.is_empty());
         let arg = std::mem::take(arg.as_mut());
-        let rules = std::mem::take(rules);
+        let rules = std::mem::take(arms);
         *self = encode_match(arg, rules, adt_encoding);
-      } else if let Term::Swt { arg, bnd: _, with, pred, arms: rules } = self {
-        assert!(with.is_empty());
+      } else if let Term::Swt { arg, bnd: _, with_bnd, with_arg, pred, arms } = self {
+        assert!(with_bnd.is_empty());
+        assert!(with_arg.is_empty());
         let arg = std::mem::take(arg.as_mut());
         let pred = std::mem::take(pred);
-        let rules = std::mem::take(rules);
+        let rules = std::mem::take(arms);
         *self = encode_switch(arg, pred, rules);
       }
     })
@@ -60,7 +62,8 @@ fn encode_match(arg: Term, rules: Vec<MatchRule>, adt_encoding: AdtEncoding) ->
             Term::Swt {
               arg: Box::new(Term::Var { nam: Name::new("%tag") }),
               bnd: None,
-              with: vec![],
+              with_bnd: vec![],
+              with_arg: vec![],
               pred: None,
               arms: vec![std::mem::take(arm), make_switches(rest)],
             },
@@ -75,7 +78,8 @@ fn encode_match(arg: Term, rules: Vec<MatchRule>, adt_encoding: AdtEncoding) ->
         let term = Term::Swt {
           arg: Box::new(Term::Var { nam: Name::new("%tag") }),
           bnd: None,
-          with: vec![],
+          with_bnd: vec![],
+          with_arg: vec![],
           pred: None,
           arms: vec![arm, Term::Era],
         };
@@ -100,12 +104,20 @@ fn encode_switch(arg: Term, pred: Option<Name>, mut rules: Vec<Term>) -> Term {
   nums.iter_mut().enumerate().rfold(last_arm, |term, (i, rule)| {
     let arms = vec![std::mem::take(rule), term];
     if i == 0 {
-      Term::Swt { arg: Box::new(arg.clone()), bnd: None, with: vec![], pred: None, arms }
+      Term::Swt {
+        arg: Box::new(arg.clone()),
+        bnd: None,
+        with_bnd: vec![],
+        with_arg: vec![],
+        pred: None,
+        arms,
+      }
     } else {
       let swt = Term::Swt {
         arg: Box::new(Term::Var { nam: match_var.clone() }),
         bnd: None,
-        with: vec![],
+        with_bnd: vec![],
+        with_arg: vec![],
         pred: None,
         arms,
       };
diff --git a/src/fun/transform/fix_match_terms.rs b/src/fun/transform/fix_match_terms.rs
index b6efadd3..5fab79d4 100644
--- a/src/fun/transform/fix_match_terms.rs
+++ b/src/fun/transform/fix_match_terms.rs
@@ -86,7 +86,8 @@ impl Term {
       }
       // Add a use term to each arm rebuilding the matched variable
       match self {
-        Term::Mat { arg: _, bnd, with: _, arms } | Term::Fold { bnd, arg: _, with: _, arms } => {
+        Term::Mat { arg: _, bnd, with_bnd: _, with_arg: _, arms }
+        | Term::Fold { bnd, arg: _, with_bnd: _, with_arg: _, arms } => {
           for (ctr, fields, body) in arms {
             if let Some(ctr) = ctr {
               *body = Term::Use {
@@ -100,7 +101,7 @@ impl Term {
             }
           }
         }
-        Term::Swt { arg: _, bnd, with: _, pred, arms } => {
+        Term::Swt { arg: _, bnd, with_bnd: _, with_arg: _, pred, arms } => {
           let n_nums = arms.len() - 1;
           for (i, arm) in arms.iter_mut().enumerate() {
             let orig = if i == n_nums {
@@ -125,7 +126,9 @@ impl Term {
   }
 
   fn fix_match(&mut self, errs: &mut Vec<FixMatchErr>, ctrs: &Constructors, adts: &Adts) {
-    let (Term::Mat { arg: _, bnd, with: _, arms } | Term::Fold { bnd, arg: _, with: _, arms }) = self else {
+    let (Term::Mat { arg: _, bnd, with_bnd: _, with_arg: _, arms }
+    | Term::Fold { bnd, arg: _, with_bnd: _, with_arg: _, arms }) = self
+    else {
       unreachable!()
     };
     let bnd = bnd.clone().unwrap();
diff --git a/src/fun/transform/float_combinators.rs b/src/fun/transform/float_combinators.rs
index 9a2b062e..de697709 100644
--- a/src/fun/transform/float_combinators.rs
+++ b/src/fun/transform/float_combinators.rs
@@ -236,11 +236,11 @@ impl Term {
           }
         }))
       }
-      Term::Mat { arg, bnd: _, with: _, arms } => {
-        FloatIter::Mat([arg.as_mut()].into_iter().chain(arms.iter_mut().map(|r| &mut r.2)))
-      }
-      Term::Swt { arg, bnd: _, with: _, pred: _, arms } => {
-        FloatIter::Swt([arg.as_mut()].into_iter().chain(arms.iter_mut()))
+      Term::Mat { arg, bnd: _, with_bnd: _, with_arg, arms } => FloatIter::Mat(
+        [arg.as_mut()].into_iter().chain(with_arg.iter_mut()).chain(arms.iter_mut().map(|r| &mut r.2)),
+      ),
+      Term::Swt { arg, bnd: _, with_bnd: _, with_arg, pred: _, arms } => {
+        FloatIter::Swt([arg.as_mut()].into_iter().chain(with_arg.iter_mut()).chain(arms.iter_mut()))
       }
       Term::Fan { els, .. } | Term::List { els } => FloatIter::Vec(els),
       Term::Let { val: fst, nxt: snd, .. }
diff --git a/src/fun/transform/linearize_matches.rs b/src/fun/transform/linearize_matches.rs
index c2be48c0..09fcb15e 100644
--- a/src/fun/transform/linearize_matches.rs
+++ b/src/fun/transform/linearize_matches.rs
@@ -80,22 +80,32 @@ impl Term {
     })
   }
 
-  fn linearize_binds_single_match(&mut self, bind_terms: Vec<Term>) {
-    let (used_vars, with, arms) = match self {
-      Term::Mat { arg, bnd: _, with, arms } => {
+  fn linearize_binds_single_match(&mut self, mut bind_terms: Vec<Term>) {
+    let (used_vars, with_bnd, with_arg, arms) = match self {
+      Term::Mat { arg, bnd: _, with_bnd, with_arg, arms } => {
         let vars = arg.free_vars().into_keys().collect::<HashSet<_>>();
         let arms = arms.iter_mut().map(|arm| &mut arm.2).collect::<Vec<_>>();
-        (vars, with, arms)
+        (vars, with_bnd, with_arg, arms)
       }
-      Term::Swt { arg, bnd: _, with, pred: _, arms } => {
+      Term::Swt { arg, bnd: _, with_bnd, with_arg, pred: _, arms } => {
         let vars = arg.free_vars().into_keys().collect::<HashSet<_>>();
         let arms = arms.iter_mut().collect();
-        (vars, with, arms)
+        (vars, with_bnd, with_arg, arms)
       }
       _ => unreachable!(),
     };
 
-    let (non_linearized, linearized) = fixed_and_linearized_terms(used_vars, bind_terms);
+    // Add 'with' args as lets that can be moved
+    for (bnd, arg) in with_bnd.iter().zip(with_arg.iter()) {
+      let term = Term::Let {
+        pat: Box::new(Pattern::Var(bnd.clone())),
+        val: Box::new(arg.clone()),
+        nxt: Box::new(Term::Err),
+      };
+      bind_terms.push(term)
+    }
+
+    let (mut non_linearized, linearized) = fixed_and_linearized_terms(used_vars, bind_terms);
 
     // Add the linearized terms to the arms and recurse
     for arm in arms {
@@ -107,18 +117,31 @@ impl Term {
     let linearized_binds = linearized
       .iter()
       .flat_map(|t| match t {
-        Term::Lam { pat, .. } | Term::Let { pat, .. } => pat.binds().flatten().collect::<Vec<_>>(),
+        Term::Lam { pat, .. } | Term::Let { pat, .. } => pat.binds().flatten().cloned().collect::<Vec<_>>(),
         Term::Use { nam, .. } => {
           if let Some(nam) = nam {
-            vec![nam]
+            vec![nam.clone()]
           } else {
             vec![]
           }
         }
         _ => unreachable!(),
       })
-      .collect::<HashSet<_>>();
-    with.retain(|w| !linearized_binds.contains(w));
+      .collect::<BTreeSet<_>>();
+    update_with_clause(with_bnd, with_arg, &linearized_binds);
+
+    // Remove the non-linearized 'with' binds from the terms that need
+    // to be added back (since we didn't move them).
+    non_linearized.retain(|term| {
+      if let Term::Let { pat, .. } = term {
+        if let Pattern::Var(bnd) = pat.as_ref() {
+          if with_bnd.contains(bnd) {
+            return false;
+          }
+        }
+      }
+      true
+    });
 
     // Add the non-linearized terms back to before the match
     self.wrap_with_bind_terms(non_linearized);
@@ -315,6 +338,24 @@ fn binds_fixed_by_dependency(used_in_arg: HashSet<Name>, bind_terms: &[Term]) ->
   fixed_binds
 }
 
+fn update_with_clause(
+  with_bnd: &mut Vec<Option<Name>>,
+  with_arg: &mut Vec<Term>,
+  vars_to_lift: &BTreeSet<Name>,
+) {
+  let mut to_remove = Vec::new();
+  for i in 0..with_bnd.len() {
+    if let Some(with_bnd) = &with_bnd[i] {
+      if vars_to_lift.contains(with_bnd) {
+        to_remove.push(i);
+      }
+    }
+  }
+  for (removed, to_remove) in to_remove.into_iter().enumerate() {
+    with_bnd.remove(to_remove - removed);
+    with_arg.remove(to_remove - removed);
+  }
+}
 /* Linearize all used vars */
 
 impl Book {
@@ -351,15 +392,17 @@ impl Term {
 /// Obs: This does not modify unscoped variables.
 pub fn lift_match_vars(match_term: &mut Term) -> &mut Term {
   // Collect match arms with binds
-  let arms: Vec<_> = match match_term {
-    Term::Mat { arg: _, bnd: _, with: _, arms: rules } => {
-      rules.iter().map(|(_, binds, body)| (binds.iter().flatten().cloned().collect(), body)).collect()
+  let (with_bnd, with_arg, arms) = match match_term {
+    Term::Mat { arg: _, bnd: _, with_bnd, with_arg, arms: rules } => {
+      let args =
+        rules.iter().map(|(_, binds, body)| (binds.iter().flatten().cloned().collect(), body)).collect();
+      (with_bnd.clone(), with_arg.clone(), args)
     }
-    Term::Swt { arg: _, bnd: _, with: _, pred, arms } => {
+    Term::Swt { arg: _, bnd: _, with_bnd, with_arg, pred, arms } => {
       let (succ, nums) = arms.split_last_mut().unwrap();
       let mut arms = nums.iter().map(|body| (vec![], body)).collect::<Vec<_>>();
       arms.push((vec![pred.clone().unwrap()], succ));
-      arms
+      (with_bnd.clone(), with_arg.clone(), arms)
     }
     _ => unreachable!(),
   };
@@ -380,27 +423,36 @@ pub fn lift_match_vars(match_term: &mut Term) -> &mut Term {
 
   // Add lambdas to the arms
   match match_term {
-    Term::Mat { arg: _, bnd: _, with, arms } => {
-      with.retain(|with| !vars_to_lift.contains(with));
+    Term::Mat { arg: _, bnd: _, with_bnd, with_arg, arms } => {
+      update_with_clause(with_bnd, with_arg, &vars_to_lift);
       for arm in arms {
         let old_body = std::mem::take(&mut arm.2);
-        arm.2 =
-          vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::lam(Pattern::Var(Some(nam)), body));
+        arm.2 = Term::rfold_lams(old_body, vars_to_lift.iter().cloned().map(Some));
       }
     }
-    Term::Swt { arg: _, bnd: _, with, pred: _, arms } => {
-      with.retain(|with| !vars_to_lift.contains(with));
+    Term::Swt { arg: _, bnd: _, with_bnd, with_arg, pred: _, arms } => {
+      update_with_clause(with_bnd, with_arg, &vars_to_lift);
       for arm in arms {
         let old_body = std::mem::take(arm);
-        *arm =
-          vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::lam(Pattern::Var(Some(nam)), body));
+        *arm = Term::rfold_lams(old_body, vars_to_lift.iter().cloned().map(Some));
       }
     }
     _ => unreachable!(),
   }
 
   // Add apps to the match
-  *match_term = vars_to_lift.into_iter().fold(std::mem::take(match_term), Term::arg_call);
+  let args = vars_to_lift
+    .into_iter()
+    .map(|nam| {
+      if let Some(idx) = with_bnd.iter().position(|x| x == &nam) {
+        with_arg[idx].clone()
+      } else {
+        Term::Var { nam }
+      }
+    })
+    .collect::<Vec<_>>();
+  let term = Term::call(std::mem::take(match_term), args);
+  *match_term = term;
 
   get_match_reference(match_term)
 }
@@ -439,38 +491,23 @@ impl Term {
       }
     });
     match self {
-      Term::Mat { arg: _, bnd: _, with, arms: rules } => {
-        // Linearize the vars in the `with` clause, but only the used ones.
-        let with = retain_used_names(std::mem::take(with), rules.iter().map(|r| &r.2));
-        for rule in rules {
-          rule.2 = with
-            .iter()
-            .rfold(std::mem::take(&mut rule.2), |bod, nam| Term::lam(Pattern::Var(Some(nam.clone())), bod));
+      Term::Mat { arg: _, bnd: _, with_bnd, with_arg, arms } => {
+        for rule in arms {
+          rule.2 = Term::rfold_lams(std::mem::take(&mut rule.2), with_bnd.clone().into_iter());
         }
-        *self = Term::call(std::mem::take(self), with.into_iter().map(|nam| Term::Var { nam }));
+        *with_bnd = vec![];
+        let call_args = std::mem::take(with_arg).into_iter();
+        *self = Term::call(std::mem::take(self), call_args);
       }
-      Term::Swt { arg: _, bnd: _, with, pred: _, arms } => {
-        let with = retain_used_names(std::mem::take(with), arms.iter());
-        for arm in arms {
-          *arm = with
-            .iter()
-            .rfold(std::mem::take(arm), |bod, nam| Term::lam(Pattern::Var(Some(nam.clone())), bod));
+      Term::Swt { arg: _, bnd: _, with_bnd, with_arg, pred: _, arms } => {
+        for rule in arms {
+          *rule = Term::rfold_lams(std::mem::take(rule), with_bnd.clone().into_iter());
         }
-        *self = Term::call(std::mem::take(self), with.into_iter().map(|nam| Term::Var { nam }));
+        *with_bnd = vec![];
+        let call_args = std::mem::take(with_arg).into_iter();
+        *self = Term::call(std::mem::take(self), call_args);
       }
       _ => {}
     }
   }
 }
-
-/// From a Vec of variable names, return the ones that are used inside `terms`.
-fn retain_used_names<'a>(mut names: Vec<Name>, terms: impl IntoIterator<Item = &'a Term>) -> Vec<Name> {
-  let mut used_names = HashSet::new();
-  for term in terms.into_iter() {
-    let mut free_vars = term.free_vars();
-    free_vars.retain(|_, uses| *uses > 0);
-    used_names.extend(free_vars.into_keys());
-  }
-  names.retain(|nam| used_names.contains(nam));
-  names
-}
diff --git a/src/fun/transform/linearize_vars.rs b/src/fun/transform/linearize_vars.rs
index 8f411671..85e48384 100644
--- a/src/fun/transform/linearize_vars.rs
+++ b/src/fun/transform/linearize_vars.rs
@@ -1,6 +1,6 @@
 use crate::{
   fun::{Book, FanKind, Name, Pattern, Tag, Term},
-  maybe_grow,
+  maybe_grow, multi_iterator,
 };
 use std::collections::HashMap;
 
@@ -120,3 +120,54 @@ fn dup_name(nam: &Name, uses: u64) -> Name {
     Name::new(format!("{nam}_{uses}"))
   }
 }
+
+impl Term {
+  /// Because multiple children can share the same binds, this function is very restricted.
+  /// Should only be called after desugaring bends/folds/matches/switches.
+  pub fn children_mut_with_binds_mut(
+    &mut self,
+  ) -> impl DoubleEndedIterator<Item = (&mut Term, impl DoubleEndedIterator<Item = &mut Option<Name>>)> {
+    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Swt });
+    multi_iterator!(BindsIter { Zero, One, Pat });
+    match self {
+      Term::Swt { arg, bnd, with_bnd, with_arg, pred, arms } => {
+        debug_assert!(bnd.is_none());
+        debug_assert!(with_bnd.is_empty());
+        debug_assert!(with_arg.is_empty());
+        debug_assert!(pred.is_none());
+        ChildrenIter::Swt(
+          [(arg.as_mut(), BindsIter::Zero([]))]
+            .into_iter()
+            .chain(arms.iter_mut().map(|x| (x, BindsIter::Zero([])))),
+        )
+      }
+      Term::Fan { els, .. } | Term::List { els } => {
+        ChildrenIter::Vec(els.iter_mut().map(|el| (el, BindsIter::Zero([]))))
+      }
+      Term::Use { nam, val, nxt } => {
+        ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::One([nam]))])
+      }
+      Term::Let { pat, val, nxt, .. } | Term::Ask { pat, val, nxt, .. } => ChildrenIter::Two([
+        (val.as_mut(), BindsIter::Zero([])),
+        (nxt.as_mut(), BindsIter::Pat(pat.binds_mut())),
+      ]),
+      Term::App { fun: fst, arg: snd, .. } | Term::Oper { fst, snd, .. } => {
+        ChildrenIter::Two([(fst.as_mut(), BindsIter::Zero([])), (snd.as_mut(), BindsIter::Zero([]))])
+      }
+      Term::Lam { pat, bod, .. } => ChildrenIter::One([(bod.as_mut(), BindsIter::Pat(pat.binds_mut()))]),
+      Term::Do { bod, .. } => ChildrenIter::One([(bod.as_mut(), BindsIter::Zero([]))]),
+      Term::Var { .. }
+      | Term::Link { .. }
+      | Term::Num { .. }
+      | Term::Nat { .. }
+      | Term::Str { .. }
+      | Term::Ref { .. }
+      | Term::Era
+      | Term::Err => ChildrenIter::Zero([]),
+      Term::Mat { .. } => unreachable!("'match' should be removed in earlier pass"),
+      Term::Fold { .. } => unreachable!("'fold' should be removed in earlier pass"),
+      Term::Bend { .. } => unreachable!("'bend' should be removed in earlier pass"),
+      Term::Open { .. } => unreachable!("'open' should be removed in earlier pass"),
+    }
+  }
+}
diff --git a/src/fun/transform/unique_names.rs b/src/fun/transform/unique_names.rs
index f0042e58..33860326 100644
--- a/src/fun/transform/unique_names.rs
+++ b/src/fun/transform/unique_names.rs
@@ -34,26 +34,134 @@ pub struct UniqueNameGenerator {
 impl UniqueNameGenerator {
   // Recursively assign an id to each variable in the term, then convert each id into a unique name.
   pub fn unique_names_in_term(&mut self, term: &mut Term) {
-    match term {
+    // Note: we can't use the children iterators here because we mutate the binds,
+    // which are shared across multiple children.
+    maybe_grow(|| match term {
       Term::Var { nam } => *nam = self.use_var(nam),
-      Term::Mat { with, .. } | Term::Swt { with, .. } => {
-        for nam in with {
-          *nam = self.use_var(nam);
+
+      Term::Mat { bnd, arg, with_bnd, with_arg, arms }
+      | Term::Fold { bnd, arg, with_bnd, with_arg, arms } => {
+        // Process args
+        self.unique_names_in_term(arg);
+        for arg in with_arg {
+          self.unique_names_in_term(arg);
+        }
+
+        // Add binds shared by all arms
+        self.push(bnd.as_ref());
+        for bnd in with_bnd.iter() {
+          self.push(bnd.as_ref());
+        }
+
+        // Process arms
+        for arm in arms {
+          // Add binds unique to each arm
+          for bnd in arm.1.iter() {
+            self.push(bnd.as_ref());
+          }
+
+          // Process arm body
+          self.unique_names_in_term(&mut arm.2);
+
+          // Remove binds unique to each arm
+          for bnd in arm.1.iter_mut() {
+            *bnd = self.pop(bnd.as_ref());
+          }
+        }
+
+        // Remove binds shared by all arms
+        for bnd in with_bnd {
+          *bnd = self.pop(bnd.as_ref());
+        }
+        *bnd = self.pop(bnd.as_ref());
+      }
+
+      Term::Swt { bnd, arg, with_bnd, with_arg, pred, arms } => {
+        self.unique_names_in_term(arg);
+        for arg in with_arg {
+          self.unique_names_in_term(arg);
+        }
+
+        self.push(bnd.as_ref());
+        for bnd in with_bnd.iter() {
+          self.push(bnd.as_ref());
+        }
+
+        let (succ, nums) = arms.split_last_mut().unwrap();
+        for arm in nums.iter_mut() {
+          self.unique_names_in_term(arm);
+        }
+
+        self.push(pred.as_ref());
+        self.unique_names_in_term(succ);
+        *pred = self.pop(pred.as_ref());
+
+        for bnd in with_bnd {
+          *bnd = self.pop(bnd.as_ref());
+        }
+        *bnd = self.pop(bnd.as_ref());
+      }
+
+      Term::Bend { bnd, arg, cond, step, base } => {
+        for arg in arg {
+          self.unique_names_in_term(arg);
+        }
+        for bnd in bnd.iter() {
+          self.push(bnd.as_ref());
+        }
+        self.unique_names_in_term(cond);
+        self.unique_names_in_term(step);
+        self.unique_names_in_term(base);
+        for bnd in bnd {
+          *bnd = self.pop(bnd.as_ref());
         }
       }
-      _ => {}
-    }
-    maybe_grow(|| {
-      for (child, binds) in term.children_mut_with_binds_mut() {
-        let binds: Vec<_> = binds.collect();
-        for bind in binds.iter() {
-          self.push(bind.as_ref());
+
+      Term::Let { pat, val, nxt } | Term::Ask { pat, val, nxt } => {
+        self.unique_names_in_term(val);
+        for bnd in pat.binds() {
+          self.push(bnd.as_ref());
         }
-        self.unique_names_in_term(child);
-        for bind in binds.into_iter().rev() {
+        self.unique_names_in_term(nxt);
+        for bind in pat.binds_mut() {
           *bind = self.pop(bind.as_ref());
         }
       }
+      Term::Use { nam, val, nxt } => {
+        self.unique_names_in_term(val);
+        self.push(nam.as_ref());
+        self.unique_names_in_term(nxt);
+        *nam = self.pop(nam.as_ref());
+      }
+      Term::Lam { tag: _, pat, bod } => {
+        for bind in pat.binds() {
+          self.push(bind.as_ref());
+        }
+        self.unique_names_in_term(bod);
+        for bind in pat.binds_mut() {
+          *bind = self.pop(bind.as_ref());
+        }
+      }
+      Term::Fan { fan: _, tag: _, els } | Term::List { els } => {
+        for el in els {
+          self.unique_names_in_term(el);
+        }
+      }
+      Term::App { tag: _, fun: fst, arg: snd } | Term::Oper { opr: _, fst, snd } => {
+        self.unique_names_in_term(fst);
+        self.unique_names_in_term(snd);
+      }
+      Term::Do { typ: _, bod } => {
+        self.unique_names_in_term(bod);
+      }
+      Term::Link { .. }
+      | Term::Num { .. }
+      | Term::Nat { .. }
+      | Term::Str { .. }
+      | Term::Ref { .. }
+      | Term::Era
+      | Term::Err => {}
+      Term::Open { .. } => unreachable!("'open' should be removed in earlier pass"),
     })
   }
 
diff --git a/src/imp/gen_map_get.rs b/src/imp/gen_map_get.rs
index 3e34eb0e..024c76b2 100644
--- a/src/imp/gen_map_get.rs
+++ b/src/imp/gen_map_get.rs
@@ -57,31 +57,38 @@ impl Stmt {
           *self = gen_get(self, substitutions);
         }
       }
-      Stmt::Match { bind: _, arg, arms, nxt } | Stmt::Fold { bind: _, arg, arms, with: _, nxt } => {
+      Stmt::Match { bnd: _, arg, with_bnd: _, with_arg, arms, nxt }
+      | Stmt::Fold { bnd: _, arg, arms, with_bnd: _, with_arg, nxt } => {
         for arm in arms.iter_mut() {
           arm.rgt.gen_map_get(id);
         }
         if let Some(nxt) = nxt {
           nxt.gen_map_get(id);
         }
-        let substitutions = arg.substitute_map_gets(id);
+        let mut substitutions = arg.substitute_map_gets(id);
+        for arg in with_arg {
+          substitutions.extend(arg.substitute_map_gets(id));
+        }
         if !substitutions.is_empty() {
           *self = gen_get(self, substitutions);
         }
       }
-      Stmt::Switch { bind: _, arg, arms, nxt } => {
+      Stmt::Switch { bnd: _, arg, with_bnd: _, with_arg, arms, nxt } => {
         for arm in arms.iter_mut() {
           arm.gen_map_get(id);
         }
         if let Some(nxt) = nxt {
           nxt.gen_map_get(id);
         }
-        let substitutions = arg.substitute_map_gets(id);
+        let mut substitutions = arg.substitute_map_gets(id);
+        for arg in with_arg {
+          substitutions.extend(arg.substitute_map_gets(id));
+        }
         if !substitutions.is_empty() {
           *self = gen_get(self, substitutions);
         }
       }
-      Stmt::Bend { bind: _, init, cond, step, base, nxt } => {
+      Stmt::Bend { bnd: _, arg: init, cond, step, base, nxt } => {
         step.gen_map_get(id);
         base.gen_map_get(id);
         if let Some(nxt) = nxt {
@@ -146,7 +153,7 @@ impl Expr {
         Expr::Lam { bod, .. } => {
           go(bod, substitutions, id);
         }
-        Expr::Bin { lhs, rhs, .. } => {
+        Expr::Opr { lhs, rhs, .. } => {
           go(lhs, substitutions, id);
           go(rhs, substitutions, id);
         }
@@ -155,24 +162,24 @@ impl Expr {
             go(el, substitutions, id);
           }
         }
-        Expr::Constructor { kwargs, .. } => {
+        Expr::Ctr { kwargs, .. } => {
           for (_, arg) in kwargs.iter_mut() {
             go(arg, substitutions, id);
           }
         }
-        Expr::Comprehension { term, iter, cond, .. } => {
+        Expr::LstMap { term, iter, cond, .. } => {
           go(term, substitutions, id);
           go(iter, substitutions, id);
           if let Some(cond) = cond {
             go(cond, substitutions, id);
           }
         }
-        Expr::MapInit { entries } => {
+        Expr::Map { entries } => {
           for (_, entry) in entries {
             go(entry, substitutions, id);
           }
         }
-        Expr::Eraser | Expr::Str { .. } | Expr::Var { .. } | Expr::Chn { .. } | Expr::Num { .. } => {}
+        Expr::Era | Expr::Str { .. } | Expr::Var { .. } | Expr::Chn { .. } | Expr::Num { .. } => {}
       }
     }
     let mut substitutions = Substitutions::new();
diff --git a/src/imp/mod.rs b/src/imp/mod.rs
index 37021af6..2198d045 100644
--- a/src/imp/mod.rs
+++ b/src/imp/mod.rs
@@ -9,7 +9,7 @@ use interner::global::GlobalString;
 #[derive(Clone, Debug)]
 pub enum Expr {
   // "*"
-  Eraser,
+  Era,
   // [a-zA-Z_]+
   Var { nam: Name },
   // "$" [a-zA-Z_]+
@@ -21,7 +21,7 @@ pub enum Expr {
   // "lambda" {names}* ":" {bod}
   Lam { names: Vec<(Name, bool)>, bod: Box<Expr> },
   // {lhs} {op} {rhs}
-  Bin { op: Op, lhs: Box<Expr>, rhs: Box<Expr> },
+  Opr { op: Op, lhs: Box<Expr>, rhs: Box<Expr> },
   // "\"" ... "\""
   Str { val: GlobalString },
   // "[" ... "]"
@@ -31,11 +31,11 @@ pub enum Expr {
   // "{" {els} "}"
   Sup { els: Vec<Expr> },
   // {name} "{" {kwargs} "}"
-  Constructor { name: Name, args: Vec<Expr>, kwargs: Vec<(Name, Expr)> },
+  Ctr { name: Name, args: Vec<Expr>, kwargs: Vec<(Name, Expr)> },
   // "[" {term} "for" {bind} "in" {iter} ("if" {cond})? "]"
-  Comprehension { term: Box<Expr>, bind: Name, iter: Box<Expr>, cond: Option<Box<Expr>> },
+  LstMap { term: Box<Expr>, bind: Name, iter: Box<Expr>, cond: Option<Box<Expr>> },
   // "{" {entries} "}"
-  MapInit { entries: Vec<(Expr, Expr)> },
+  Map { entries: Vec<(Expr, Expr)> },
   // {map} "[" {key} "]"
   MapGet { nam: Name, key: Box<Expr> },
 }
@@ -106,7 +106,9 @@ pub enum Stmt {
   // <nxt>?
   Match {
     arg: Box<Expr>,
-    bind: Option<Name>,
+    bnd: Option<Name>,
+    with_bnd: Vec<Option<Name>>,
+    with_arg: Vec<Expr>,
     arms: Vec<MatchArm>,
     nxt: Option<Box<Stmt>>,
   },
@@ -116,7 +118,9 @@ pub enum Stmt {
   // <nxt>?
   Switch {
     arg: Box<Expr>,
-    bind: Option<Name>,
+    bnd: Option<Name>,
+    with_bnd: Vec<Option<Name>>,
+    with_arg: Vec<Expr>,
     arms: Vec<Stmt>,
     nxt: Option<Box<Stmt>>,
   },
@@ -126,8 +130,8 @@ pub enum Stmt {
   //   {base}
   // <nxt>?
   Bend {
-    bind: Vec<Option<Name>>,
-    init: Vec<Expr>,
+    bnd: Vec<Option<Name>>,
+    arg: Vec<Expr>,
     cond: Box<Expr>,
     step: Box<Stmt>,
     base: Box<Stmt>,
@@ -139,8 +143,9 @@ pub enum Stmt {
   // <nxt>?
   Fold {
     arg: Box<Expr>,
-    bind: Option<Name>,
-    with: Vec<Name>,
+    bnd: Option<Name>,
+    with_bnd: Vec<Option<Name>>,
+    with_arg: Vec<Expr>,
     arms: Vec<MatchArm>,
     nxt: Option<Box<Stmt>>,
   },
diff --git a/src/imp/order_kwargs.rs b/src/imp/order_kwargs.rs
index 1b15b532..e714c8b6 100644
--- a/src/imp/order_kwargs.rs
+++ b/src/imp/order_kwargs.rs
@@ -64,9 +64,9 @@ impl Stmt {
           nxt.order_kwargs(book)?;
         }
       }
-      Stmt::Bend { bind: _, init, cond, step, base, nxt } => {
-        for init in init {
-          init.order_kwargs(book)?;
+      Stmt::Bend { bnd: _, arg, cond, step, base, nxt } => {
+        for arg in arg {
+          arg.order_kwargs(book)?;
         }
         cond.order_kwargs(book)?;
         step.order_kwargs(book)?;
@@ -126,7 +126,7 @@ impl Expr {
         }
       }
       Expr::Lam { bod, .. } => bod.order_kwargs(book)?,
-      Expr::Bin { lhs, rhs, .. } => {
+      Expr::Opr { lhs, rhs, .. } => {
         lhs.order_kwargs(book)?;
         rhs.order_kwargs(book)?;
       }
@@ -135,14 +135,14 @@ impl Expr {
           el.order_kwargs(book)?;
         }
       }
-      Expr::Comprehension { term, iter, cond, .. } => {
+      Expr::LstMap { term, iter, cond, .. } => {
         term.order_kwargs(book)?;
         iter.order_kwargs(book)?;
         if let Some(cond) = cond {
           cond.order_kwargs(book)?;
         }
       }
-      Expr::Constructor { name, args, kwargs } => match get_args_def_or_ctr(name, book) {
+      Expr::Ctr { name, args, kwargs } => match get_args_def_or_ctr(name, book) {
         Some(names) => {
           go_order_kwargs(&names, args, kwargs)?;
           for arg in args {
@@ -151,13 +151,13 @@ impl Expr {
         }
         _ => return Err(format!("Constructor '{name}' not found.")),
       },
-      Expr::MapInit { entries } => {
+      Expr::Map { entries } => {
         for entry in entries {
           entry.1.order_kwargs(book)?;
         }
       }
       Expr::MapGet { .. }
-      | Expr::Eraser
+      | Expr::Era
       | Expr::Var { .. }
       | Expr::Chn { .. }
       | Expr::Num { .. }
diff --git a/src/imp/parser.rs b/src/imp/parser.rs
index 8626800a..646a278c 100644
--- a/src/imp/parser.rs
+++ b/src/imp/parser.rs
@@ -112,7 +112,7 @@ impl<'a> PyParser<'a> {
         self.advance_one();
         // Empty map
         if self.try_consume("}") {
-          return Ok(Expr::MapInit { entries: vec![] });
+          return Ok(Expr::Map { entries: vec![] });
         }
         let head = self.parse_expr(false)?;
         self.skip_trivia();
@@ -148,7 +148,7 @@ impl<'a> PyParser<'a> {
       // Era
       '*' => {
         self.advance_one();
-        Expr::Eraser
+        Expr::Era
       }
       // Number
       c if is_num_char(c) => {
@@ -216,7 +216,7 @@ impl<'a> PyParser<'a> {
     if self.starts_with("{") {
       if let Expr::Var { nam } = base {
         let kwargs = self.list_like(|p| p.data_kwarg(), "{", "}", ",", true, 0)?;
-        return Ok(Expr::Constructor { name: nam, args: Vec::new(), kwargs });
+        return Ok(Expr::Ctr { name: nam, args: Vec::new(), kwargs });
       } else {
         return self.expected_spanned("Constructor name", ini_idx, end_idx);
       }
@@ -236,7 +236,7 @@ impl<'a> PyParser<'a> {
     }
     let tail = self.list_like(|p| p.parse_map_entry(), "", "}", ",", true, 0)?;
     entries.extend(tail);
-    Ok(Expr::MapInit { entries })
+    Ok(Expr::Map { entries })
   }
 
   fn parse_sup(&mut self, head: Expr) -> ParseResult<Expr> {
@@ -285,7 +285,7 @@ impl<'a> PyParser<'a> {
         cond = Some(Box::new(self.parse_expr(false)?));
       }
       self.consume("]")?;
-      Ok(Expr::Comprehension { term: Box::new(head), bind, iter: Box::new(iter), cond })
+      Ok(Expr::LstMap { term: Box::new(head), bind, iter: Box::new(iter), cond })
     } else {
       // List
       let mut head = vec![head];
@@ -368,7 +368,7 @@ impl<'a> PyParser<'a> {
         if op.precedence() == prec {
           self.parse_oper()?;
           let rhs = self.parse_infix_expr(prec + 1, inline)?;
-          lhs = Expr::Bin { op, lhs: Box::new(lhs), rhs: Box::new(rhs) };
+          lhs = Expr::Opr { op, lhs: Box::new(lhs), rhs: Box::new(rhs) };
           self.skip_trivia_inline();
         } else {
           break;
@@ -579,9 +579,9 @@ impl<'a> PyParser<'a> {
   }
 
   fn parse_match(&mut self, indent: &mut Indent) -> ParseResult<(Stmt, Indent)> {
-    let (bind, arg) = self.parse_match_arg()?;
+    let (bnd, arg) = self.parse_match_arg()?;
     self.skip_trivia_inline();
-    self.consume_exactly(":")?;
+    let (with_bnd, with_arg) = self.parse_with_clause()?;
     self.consume_new_line()?;
     indent.enter_level();
 
@@ -596,10 +596,10 @@ impl<'a> PyParser<'a> {
     indent.exit_level();
     if nxt_indent == *indent {
       let (nxt, nxt_indent) = self.parse_statement(indent)?;
-      let stmt = Stmt::Match { arg: Box::new(arg), bind, arms, nxt: Some(Box::new(nxt)) };
+      let stmt = Stmt::Match { arg: Box::new(arg), bnd, with_bnd, with_arg, arms, nxt: Some(Box::new(nxt)) };
       Ok((stmt, nxt_indent))
     } else {
-      let stmt = Stmt::Match { arg: Box::new(arg), bind, arms, nxt: None };
+      let stmt = Stmt::Match { arg: Box::new(arg), bnd, with_bnd, with_arg, arms, nxt: None };
       Ok((stmt, nxt_indent))
     }
   }
@@ -621,6 +621,28 @@ impl<'a> PyParser<'a> {
     }
   }
 
+  fn parse_with_clause(&mut self) -> ParseResult<(Vec<Option<Name>>, Vec<Expr>)> {
+    self.skip_trivia_inline();
+    let res = if self.try_parse_keyword("with") {
+      self.list_like(|p| p.parse_with_arg(), "", ":", ",", true, 1)?.into_iter().unzip()
+    } else {
+      self.consume_exactly(":")?;
+      (vec![], vec![])
+    };
+    Ok(res)
+  }
+
+  fn parse_with_arg(&mut self) -> ParseResult<(Option<Name>, Expr)> {
+    let bind = self.parse_bend_name()?;
+    self.skip_trivia_inline();
+    if self.try_consume("=") {
+      let arg = self.parse_expr(false)?;
+      Ok((Some(bind), arg))
+    } else {
+      Ok((Some(bind.clone()), Expr::Var { nam: bind }))
+    }
+  }
+
   fn parse_match_case(&mut self, indent: &mut Indent) -> ParseResult<(MatchArm, Indent)> {
     self.parse_keyword("case")?;
     self.skip_trivia_inline();
@@ -644,9 +666,9 @@ impl<'a> PyParser<'a> {
   }
 
   fn parse_switch(&mut self, indent: &mut Indent) -> ParseResult<(Stmt, Indent)> {
-    let (bind, arg) = self.parse_match_arg()?;
+    let (bnd, arg) = self.parse_match_arg()?;
     self.skip_trivia_inline();
-    self.consume_exactly(":")?;
+    let (with_bnd, with_arg) = self.parse_with_clause()?;
     indent.enter_level();
 
     self.consume_indent_exactly(*indent)?;
@@ -680,10 +702,10 @@ impl<'a> PyParser<'a> {
     indent.exit_level();
     if nxt_indent == *indent {
       let (nxt, nxt_indent) = self.parse_statement(indent)?;
-      let stmt = Stmt::Switch { arg: Box::new(arg), bind, arms, nxt: Some(Box::new(nxt)) };
+      let stmt = Stmt::Switch { arg: Box::new(arg), bnd, with_bnd, with_arg, arms, nxt: Some(Box::new(nxt)) };
       Ok((stmt, nxt_indent))
     } else {
-      let stmt = Stmt::Switch { arg: Box::new(arg), bind, arms, nxt: None };
+      let stmt = Stmt::Switch { arg: Box::new(arg), bnd, with_bnd, with_arg, arms, nxt: None };
       Ok((stmt, nxt_indent))
     }
   }
@@ -722,22 +744,7 @@ impl<'a> PyParser<'a> {
     // Actually identical to match, except the return
     let (bind, arg) = self.parse_match_arg()?;
     self.skip_trivia_inline();
-    let with = if self.try_parse_keyword("with") {
-      self.skip_trivia_inline();
-      let mut with = vec![];
-      while !self.starts_with(":") {
-        with.push(self.parse_bend_name()?);
-        self.skip_trivia_inline();
-        if !self.starts_with(":") {
-          self.consume_exactly(",")?;
-        }
-        self.skip_trivia_inline();
-      }
-      with
-    } else {
-      vec![]
-    };
-    self.consume_exactly(":")?;
+    let (with_bnd, with_arg) = self.parse_with_clause()?;
     self.consume_new_line()?;
     indent.enter_level();
 
@@ -752,10 +759,11 @@ impl<'a> PyParser<'a> {
     indent.exit_level();
     if nxt_indent == *indent {
       let (nxt, nxt_indent) = self.parse_statement(indent)?;
-      let stmt = Stmt::Fold { arg: Box::new(arg), bind, arms, with, nxt: Some(Box::new(nxt)) };
+      let stmt =
+        Stmt::Fold { arg: Box::new(arg), bnd: bind, arms, with_bnd, with_arg, nxt: Some(Box::new(nxt)) };
       Ok((stmt, nxt_indent))
     } else {
-      let stmt = Stmt::Fold { arg: Box::new(arg), bind, arms, with, nxt: None };
+      let stmt = Stmt::Fold { arg: Box::new(arg), bnd: bind, arms, with_bnd, with_arg, nxt: None };
       Ok((stmt, nxt_indent))
     }
   }
@@ -800,8 +808,8 @@ impl<'a> PyParser<'a> {
     if nxt_indent == *indent {
       let (nxt, nxt_indent) = self.parse_statement(indent)?;
       let stmt = Stmt::Bend {
-        bind,
-        init,
+        bnd: bind,
+        arg: init,
         cond: Box::new(cond),
         step: Box::new(step),
         base: Box::new(base),
@@ -810,8 +818,8 @@ impl<'a> PyParser<'a> {
       Ok((stmt, nxt_indent))
     } else {
       let stmt = Stmt::Bend {
-        bind,
-        init,
+        bnd: bind,
+        arg: init,
         cond: Box::new(cond),
         step: Box::new(step),
         base: Box::new(base),
diff --git a/src/imp/to_fun.rs b/src/imp/to_fun.rs
index 67d83255..010af672 100644
--- a/src/imp/to_fun.rs
+++ b/src/imp/to_fun.rs
@@ -135,13 +135,14 @@ impl Stmt {
         let term = fun::Term::Swt {
           arg: Box::new(cond.to_fun()),
           bnd: Some(Name::new("%pred")),
-          with: Vec::new(),
+          with_bnd: vec![],
+          with_arg: vec![],
           pred: Some(Name::new("%pred-1")),
           arms,
         };
         wrap_nxt_assign_stmt(term, nxt, pat)?
       }
-      Stmt::Match { arg, bind, arms, nxt } => {
+      Stmt::Match { arg, bnd, with_bnd, with_arg, arms, nxt } => {
         let arg = arg.to_fun();
         let mut fun_arms = vec![];
         let mut arms = arms.into_iter();
@@ -150,6 +151,7 @@ impl Stmt {
           StmtToFun::Return(term) => (None, term),
           StmtToFun::Assign(pat, term) => (Some(pat), term),
         };
+        let with_arg = with_arg.into_iter().map(Expr::to_fun).collect();
         fun_arms.push((fst.lft, vec![], fst_rgt));
         for arm in arms {
           let (arm_pat, arm_rgt) = match arm.rgt.into_fun()? {
@@ -170,10 +172,10 @@ impl Stmt {
             (None, None) => fun_arms.push((arm.lft, vec![], arm_rgt)),
           }
         }
-        let term = fun::Term::Mat { arg: Box::new(arg), bnd: bind, with: Vec::new(), arms: fun_arms };
+        let term = fun::Term::Mat { arg: Box::new(arg), bnd, with_bnd, with_arg, arms: fun_arms };
         wrap_nxt_assign_stmt(term, nxt, fst_pat)?
       }
-      Stmt::Switch { arg, bind, arms, nxt } => {
+      Stmt::Switch { arg, bnd, with_bnd, with_arg, arms, nxt } => {
         let arg = arg.to_fun();
         let mut fun_arms = vec![];
         let mut arms = arms.into_iter();
@@ -182,6 +184,7 @@ impl Stmt {
           StmtToFun::Return(term) => (None, term),
           StmtToFun::Assign(pat, term) => (Some(pat), term),
         };
+        let with_arg = with_arg.into_iter().map(Expr::to_fun).collect();
         fun_arms.push(fst);
         for arm in arms {
           let (arm_pat, arm) = match arm.into_fun()? {
@@ -202,11 +205,11 @@ impl Stmt {
             (None, None) => fun_arms.push(arm),
           }
         }
-        let pred = Some(Name::new(format!("{}-{}", bind.clone().unwrap(), fun_arms.len() - 1)));
-        let term = fun::Term::Swt { arg: Box::new(arg), bnd: bind, with: Vec::new(), pred, arms: fun_arms };
+        let pred = Some(Name::new(format!("{}-{}", bnd.clone().unwrap(), fun_arms.len() - 1)));
+        let term = fun::Term::Swt { arg: Box::new(arg), bnd, with_bnd, with_arg, pred, arms: fun_arms };
         wrap_nxt_assign_stmt(term, nxt, fst_pat)?
       }
-      Stmt::Fold { arg, bind, arms, with, nxt } => {
+      Stmt::Fold { arg, bnd, with_bnd, with_arg, arms, nxt } => {
         let arg = arg.to_fun();
         let mut fun_arms = vec![];
         let mut arms = arms.into_iter();
@@ -216,6 +219,7 @@ impl Stmt {
           StmtToFun::Assign(pat, term) => (Some(pat), term),
         };
         fun_arms.push((fst.lft, vec![], fst_rgt));
+        let with_arg = with_arg.into_iter().map(Expr::to_fun).collect();
         for arm in arms {
           let (arm_pat, arm_rgt) = match arm.rgt.into_fun()? {
             StmtToFun::Return(term) => (None, term),
@@ -235,11 +239,11 @@ impl Stmt {
             (None, None) => fun_arms.push((arm.lft, vec![], arm_rgt)),
           }
         }
-        let term = fun::Term::Fold { arg: Box::new(arg), bnd: bind, with, arms: fun_arms };
+        let term = fun::Term::Fold { arg: Box::new(arg), bnd, with_bnd, with_arg, arms: fun_arms };
         wrap_nxt_assign_stmt(term, nxt, fst_pat)?
       }
-      Stmt::Bend { bind, init, cond, step, base, nxt } => {
-        let init = init.into_iter().map(Expr::to_fun).collect();
+      Stmt::Bend { bnd, arg, cond, step, base, nxt } => {
+        let arg = arg.into_iter().map(Expr::to_fun).collect();
         let cond = cond.to_fun();
         let (pat, step, base) = match (step.into_fun()?, base.into_fun()?) {
           (StmtToFun::Return(s), StmtToFun::Return(b)) => (None, s, b),
@@ -259,7 +263,7 @@ impl Stmt {
           }
         };
         let term =
-          fun::Term::Bend { bind, init, cond: Box::new(cond), step: Box::new(step), base: Box::new(base) };
+          fun::Term::Bend { bnd, arg, cond: Box::new(cond), step: Box::new(step), base: Box::new(base) };
         wrap_nxt_assign_stmt(term, nxt, pat)?
       }
       Stmt::With { typ, bod, nxt } => {
@@ -317,7 +321,7 @@ impl Stmt {
 impl Expr {
   pub fn to_fun(self) -> fun::Term {
     match self {
-      Expr::Eraser => fun::Term::Era,
+      Expr::Era => fun::Term::Era,
       Expr::Var { nam } => fun::Term::Var { nam },
       Expr::Chn { nam } => fun::Term::Link { nam },
       Expr::Num { val } => fun::Term::Num { val },
@@ -331,7 +335,7 @@ impl Expr {
         pat: Box::new(if link { fun::Pattern::Chn(name) } else { fun::Pattern::Var(Some(name)) }),
         bod: Box::new(acc),
       }),
-      Expr::Bin { op, lhs, rhs } => {
+      Expr::Opr { op, lhs, rhs } => {
         fun::Term::Oper { opr: op, fst: Box::new(lhs.to_fun()), snd: Box::new(rhs.to_fun()) }
       }
       Expr::Str { val } => fun::Term::Str { val },
@@ -346,12 +350,12 @@ impl Expr {
         tag: fun::Tag::Auto,
         els: els.into_iter().map(Self::to_fun).collect(),
       },
-      Expr::Constructor { name, args, kwargs } => {
+      Expr::Ctr { name, args, kwargs } => {
         assert!(kwargs.is_empty());
         let args = args.into_iter().map(Self::to_fun);
         fun::Term::call(fun::Term::Ref { nam: name }, args)
       }
-      Expr::Comprehension { term, bind, iter, cond } => {
+      Expr::LstMap { term, bind, iter, cond } => {
         const ITER_TAIL: &str = "%iter.tail";
         const ITER_HEAD: &str = "%iter.head";
 
@@ -363,7 +367,8 @@ impl Expr {
           fun::Term::Swt {
             arg: Box::new(cond.to_fun()),
             bnd: Some(Name::new("%comprehension")),
-            with: vec![],
+            with_bnd: vec![],
+            with_arg: vec![],
             pred: Some(Name::new("%comprehension-1")),
             arms: vec![fun::Term::Var { nam: Name::new(ITER_TAIL) }, cons_branch],
           }
@@ -379,14 +384,15 @@ impl Expr {
         fun::Term::Fold {
           bnd: Some(Name::new("%iter")),
           arg: Box::new(iter.to_fun()),
-          with: Vec::new(),
+          with_bnd: vec![],
+          with_arg: vec![],
           arms: vec![
             (Some(Name::new(LNIL)), vec![], fun::Term::r#ref(LNIL)),
             (Some(Name::new(LCONS)), vec![], cons_branch),
           ],
         }
       }
-      Expr::MapInit { entries } => map_init(entries),
+      Expr::Map { entries } => map_init(entries),
       Expr::MapGet { .. } => unreachable!(),
     }
   }
diff --git a/src/lib.rs b/src/lib.rs
index af90444e..4a5b91a0 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -112,9 +112,8 @@ pub fn desugar_book(
 
   ctx.check_unbound_vars()?;
 
-  ctx.book.make_var_names_unique();
-
   // Auto match linearization
+  ctx.book.make_var_names_unique();
   match opts.linearize_matches {
     OptLevel::Disabled => (),
     OptLevel::Alt => ctx.book.linearize_match_binds(),
diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs
index d341395a..a5394502 100644
--- a/tests/golden_tests.rs
+++ b/tests/golden_tests.rs
@@ -228,10 +228,14 @@ fn simplify_matches() {
     ctx.set_entrypoint();
     ctx.book.encode_adts(AdtEncoding::NumScott);
     ctx.fix_match_defs()?;
+    ctx.desugar_open()?;
     ctx.book.encode_builtins();
     ctx.resolve_refs()?;
     ctx.desugar_match_defs()?;
     ctx.fix_match_terms()?;
+    ctx.desugar_bend()?;
+    ctx.desugar_fold()?;
+    ctx.desugar_do_blocks()?;
     ctx.check_unbound_vars()?;
     ctx.book.make_var_names_unique();
     ctx.book.linearize_match_binds();
@@ -273,10 +277,14 @@ fn encode_pattern_match() {
       ctx.set_entrypoint();
       ctx.book.encode_adts(adt_encoding);
       ctx.fix_match_defs()?;
+      ctx.desugar_open()?;
       ctx.book.encode_builtins();
       ctx.resolve_refs()?;
       ctx.desugar_match_defs()?;
       ctx.fix_match_terms()?;
+      ctx.desugar_bend()?;
+      ctx.desugar_fold()?;
+      ctx.desugar_do_blocks()?;
       ctx.check_unbound_vars()?;
       ctx.book.make_var_names_unique();
       ctx.book.linearize_match_binds();
diff --git a/tests/golden_tests/encode_pattern_match/definition_merge.bend b/tests/golden_tests/encode_pattern_match/definition_merge.bend
index eb02978d..052cfe25 100644
--- a/tests/golden_tests/encode_pattern_match/definition_merge.bend
+++ b/tests/golden_tests/encode_pattern_match/definition_merge.bend
@@ -1,5 +1,5 @@
 type Either = (Left value) | (Right value)
-type Bool = Bool/True | Bool/False
+type Bool = True | False
 
 Foo (Either/Left  Bool/False) (Either/Left  Bool/False) = 1
 Foo (Either/Left  Bool/False) (Either/Left  Bool/True)  = 1
@@ -20,3 +20,5 @@ Foo (Either/Right Bool/False) (Either/Left Bool/False)  = 3
 Foo (Either/Right Bool/False) (Either/Left Bool/True)   = 3
 Foo (Either/Right Bool/True)  (Either/Left Bool/False)  = 3
 Foo (Either/Right Bool/True)  (Either/Left Bool/True)   = 3
+
+
diff --git a/tests/golden_tests/run_file/list_reverse_imp.bend b/tests/golden_tests/run_file/list_reverse_imp.bend
new file mode 100644
index 00000000..6ba96d66
--- /dev/null
+++ b/tests/golden_tests/run_file/list_reverse_imp.bend
@@ -0,0 +1,14 @@
+def reverse(list):
+  fold list with acc = []:
+    case List/Nil:
+      return acc
+    case List/Cons:
+      return list.tail(List/Cons(list.head, acc))
+
+def main:
+  bend n = 5:
+    when n != 0:
+      xs = List/Cons(n, fork(n - 1))
+    else:
+      xs = List/Nil
+  return reverse(xs)
\ No newline at end of file
diff --git a/tests/snapshots/encode_pattern_match__bool.bend.snap b/tests/snapshots/encode_pattern_match__bool.bend.snap
index 5fb408e5..57db838a 100644
--- a/tests/snapshots/encode_pattern_match__bool.bend.snap
+++ b/tests/snapshots/encode_pattern_match__bool.bend.snap
@@ -5,13 +5,13 @@ input_file: tests/golden_tests/encode_pattern_match/bool.bend
 Scott
 (not) = λa (a bool/false bool/true)
 
-(and) = λa (a λb (b bool/true bool/false) λc (c bool/false bool/false))
+(and) = λa (a λb (b bool/true bool/false) λd (d bool/false bool/false))
 
-(and2) = λa (a λb b λ* bool/false)
+(and2) = λa (a λb b λd let * = d; bool/false)
 
-(and3) = λa (a λb (b bool/true bool/false) λ* bool/false)
+(and3) = λa (a λb (b bool/true bool/false) λd let * = d; bool/false)
 
-(and4) = λa (a λb (b bool/true bool/false) λ* bool/false)
+(and4) = λa (a λb (b bool/true bool/false) λd let * = d; bool/false)
 
 (bool/true) = λa λ* a
 
@@ -20,13 +20,13 @@ Scott
 NumScott
 (not) = λa (a λb switch b { 0: bool/false; _: λ* bool/true; })
 
-(and) = λa (a λb switch b { 0: λc (c λd switch d { 0: bool/true; _: λ* bool/false; }); _: λ* λe (e λf switch f { 0: bool/false; _: λ* bool/false; }); })
+(and) = λa (a λb switch b { 0: λc (c λe switch e { 0: bool/true; _: λ* bool/false; }); _: λ* λf (f λh switch h { 0: bool/false; _: λ* bool/false; }); })
 
-(and2) = λa (a λb switch b { 0: λc c; _: λ* λ* bool/false; })
+(and2) = λa (a λb switch b { 0: λc c; _: λ* λe let * = e; bool/false; })
 
-(and3) = λa (a λb switch b { 0: λc (c λd switch d { 0: bool/true; _: λ* bool/false; }); _: λ* λ* bool/false; })
+(and3) = λa (a λb switch b { 0: λc (c λe switch e { 0: bool/true; _: λ* bool/false; }); _: λ* λf let * = f; bool/false; })
 
-(and4) = λa (a λb switch b { 0: λc (c λd switch d { 0: bool/true; _: λ* bool/false; }); _: λ* λ* bool/false; })
+(and4) = λa (a λb switch b { 0: λc (c λe switch e { 0: bool/true; _: λ* bool/false; }); _: λ* λf let * = f; bool/false; })
 
 (bool/true) = λa (a bool/true/tag)
 
diff --git a/tests/snapshots/encode_pattern_match__concat_def.bend.snap b/tests/snapshots/encode_pattern_match__concat_def.bend.snap
index 4bd08076..ac6c42c1 100644
--- a/tests/snapshots/encode_pattern_match__concat_def.bend.snap
+++ b/tests/snapshots/encode_pattern_match__concat_def.bend.snap
@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/concat_def.bend
 ---
 Scott
-(concat) = λa (a λb b λc λd λe (String/Cons c (concat d e)))
+(concat) = λa (a λb b λd λe λf (String/Cons d (concat e f)))
 
 (main) = (concat (String/Cons 97 (String/Cons 98 String/Nil)) (String/Cons 99 (String/Cons 100 String/Nil)))
 
@@ -12,7 +12,7 @@ Scott
 (String/Cons) = λa λb λ* λd (d a b)
 
 NumScott
-(concat) = λa (a λb switch b { 0: λc c; _: λ* λd λe λf (String/Cons d (concat e f)); })
+(concat) = λa (a λb switch b { 0: λc c; _: λ* λe λf λg (String/Cons e (concat f g)); })
 
 (main) = (concat (String/Cons 97 (String/Cons 98 String/Nil)) (String/Cons 99 (String/Cons 100 String/Nil)))
 
diff --git a/tests/snapshots/encode_pattern_match__definition_merge.bend.snap b/tests/snapshots/encode_pattern_match__definition_merge.bend.snap
index a06b69d9..b673bacc 100644
--- a/tests/snapshots/encode_pattern_match__definition_merge.bend.snap
+++ b/tests/snapshots/encode_pattern_match__definition_merge.bend.snap
@@ -3,31 +3,31 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/definition_merge.bend
 ---
 Scott
-(Foo) = λa (a λ* λc (c λ* 1 λ* 2) λ* λg (g λ* 3 λ* 3))
+(Foo) = λa (a λb (b λc (c λf (f 1 1) λg (g 2 2)) λh (h λk (k 1 1) λl (l 2 2))) λm (m λn (n λq (q 3 3) λr (r 3 3)) λs (s λv (v 3 3) λw (w 3 3))))
 
 (Either/Left) = λa λb λ* (b a)
 
 (Either/Right) = λa λ* λc (c a)
 
-(Bool/Bool/True) = λa λ* a
+(Bool/True) = λa λ* a
 
-(Bool/Bool/False) = λ* λb b
+(Bool/False) = λ* λb b
 
 NumScott
-(Foo) = λa (a λb switch b { 0: λ* λd (d λe switch e { 0: λ* 1; _: λ* λ* 2; }); _: λ* λ* λi (i λj switch j { 0: λ* 3; _: λ* λ* 3; }); })
+(Foo) = λa (a λb switch b { 0: λc (c λd switch d { 0: λe (e λh switch h { 0: λi (i λj switch j { 0: 1; _: λ* 1; }); _: λ* λk (k λl switch l { 0: 2; _: λ* 2; }); }); _: λ* λm (m λp switch p { 0: λq (q λr switch r { 0: 1; _: λ* 1; }); _: λ* λs (s λt switch t { 0: 2; _: λ* 2; }); }); }); _: λ* λu (u λv switch v { 0: λw (w λz switch z { 0: λab (ab λbb switch bb { 0: 3; _: λ* 3; }); _: λ* λcb (cb λdb switch db { 0: 3; _: λ* 3; }); }); _: λ* λeb (eb λhb switch hb { 0: λib (ib λjb switch jb { 0: 3; _: λ* 3; }); _: λ* λkb (kb λlb switch lb { 0: 3; _: λ* 3; }); }); }); })
 
 (Either/Left) = λa λb (b Either/Left/tag a)
 
 (Either/Right) = λa λb (b Either/Right/tag a)
 
-(Bool/Bool/True) = λa (a Bool/Bool/True/tag)
+(Bool/True) = λa (a Bool/True/tag)
 
-(Bool/Bool/False) = λa (a Bool/Bool/False/tag)
+(Bool/False) = λa (a Bool/False/tag)
 
 (Either/Left/tag) = 0
 
 (Either/Right/tag) = 1
 
-(Bool/Bool/True/tag) = 0
+(Bool/True/tag) = 0
 
-(Bool/Bool/False/tag) = 1
+(Bool/False/tag) = 1
diff --git a/tests/snapshots/encode_pattern_match__flatten_era_pat.bend.snap b/tests/snapshots/encode_pattern_match__flatten_era_pat.bend.snap
index 0c183c49..eada4938 100644
--- a/tests/snapshots/encode_pattern_match__flatten_era_pat.bend.snap
+++ b/tests/snapshots/encode_pattern_match__flatten_era_pat.bend.snap
@@ -7,7 +7,7 @@ Scott
 
 (Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f
 
-(Fn3) = λa let (b, *) = a; switch b { 0: λ* 0; _: λe λ* (+ e 1); }
+(Fn3) = λa let (b, c) = a; (switch b { 0: λ* λe let * = e; 0; _: λg λ* λi let * = i; (+ g 1); } c)
 
 (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
 
@@ -16,6 +16,6 @@ NumScott
 
 (Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f
 
-(Fn3) = λa let (b, *) = a; switch b { 0: λ* 0; _: λe λ* (+ e 1); }
+(Fn3) = λa let (b, c) = a; (switch b { 0: λ* λe let * = e; 0; _: λg λ* λi let * = i; (+ g 1); } c)
 
 (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
diff --git a/tests/snapshots/encode_pattern_match__list_merge_sort.bend.snap b/tests/snapshots/encode_pattern_match__list_merge_sort.bend.snap
index 120ffc84..6be31d66 100644
--- a/tests/snapshots/encode_pattern_match__list_merge_sort.bend.snap
+++ b/tests/snapshots/encode_pattern_match__list_merge_sort.bend.snap
@@ -3,11 +3,11 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/list_merge_sort.bend
 ---
 Scott
-(If) = λa (a λb λ* b λ* λe e)
+(If) = λa (a λb λc let * = c; b λf λg let * = f; g)
 
 (Pure) = λa (List_/Cons a List_/Nil)
 
-(Map) = λa (a λb λc λd let {d d_2} = d; (List_/Cons (d b) (Map c d_2)) λ* List_/Nil)
+(Map) = λa (a λb λc λd let {e e_2} = d; (List_/Cons (e b) (Map c e_2)) λf let * = f; List_/Nil)
 
 (MergeSort) = λa λb (Unpack a (Map b Pure))
 
@@ -15,7 +15,7 @@ Scott
 
 (MergePair) = λa λb (b λc λd λe (d λf λg λh let {h h_2} = h; λi (List_/Cons (Merge h i f) (MergePair h_2 g)) λ* λk (List_/Cons k List_/Nil) e c) λ* List_/Nil a)
 
-(Merge) = λa λb (b λc λd λe λf (f λg let {g g_2 g_3} = g; λh let {h h_2} = h; λi let {i i_2 i_3} = i; λj let {j j_2 j_3} = j; λk let {k k_2} = k; (If (i j g) (List_/Cons j_2 (Merge i_2 k (List_/Cons g_2 h))) (List_/Cons g_3 (Merge i_3 (List_/Cons j_3 k_2) h_2))) λ* λo λp (List_/Cons o p) e c d) λ* λr r a)
+(Merge) = λa λb (b λc λd λe λf (f λ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) (List_/Cons k_2 (Merge j_2 l (List_/Cons h_2 i))) (List_/Cons h_3 (Merge j_3 (List_/Cons k_3 l_2) i_2))) λ* λp λq (List_/Cons p q) e c d) λ* λs s a)
 
 (Bool/True) = λa λ* a
 
@@ -26,11 +26,11 @@ Scott
 (List_/Nil) = λ* λb b
 
 NumScott
-(If) = λa (a λb switch b { 0: λc λ* c; _: λ* λ* λf f; })
+(If) = λa (a λb switch b { 0: λc λd let * = d; c; _: λ* λg λh let * = g; h; })
 
 (Pure) = λa (List_/Cons a List_/Nil)
 
-(Map) = λa (a λb switch b { 0: λc λd λe let {e e_2} = e; (List_/Cons (e c) (Map d e_2)); _: λ* λ* List_/Nil; })
+(Map) = λa (a λb switch b { 0: λc λd λe let {f f_2} = e; (List_/Cons (f c) (Map d f_2)); _: λ* λg let * = g; List_/Nil; })
 
 (MergeSort) = λa λb (Unpack a (Map b Pure))
 
@@ -38,7 +38,7 @@ NumScott
 
 (MergePair) = λa λb (b λc switch c { 0: λd λe λf (e λg switch g { 0: λh λi λj let {j j_2} = j; λk (List_/Cons (Merge j k h) (MergePair j_2 i)); _: λ* λ* λm (List_/Cons m List_/Nil); } f d); _: λ* λ* List_/Nil; } a)
 
-(Merge) = λa λb (b λc switch c { 0: λd λe λf λg (g λh switch h { 0: λi let {i i_2 i_3} = i; λj let {j j_2} = j; λk let {k k_2 k_3} = k; λl let {l l_2 l_3} = l; λm let {m m_2} = m; (If (k l i) (List_/Cons l_2 (Merge k_2 m (List_/Cons i_2 j))) (List_/Cons i_3 (Merge k_3 (List_/Cons l_3 m_2) j_2))); _: λ* λ* λq λr (List_/Cons q r); } f d e); _: λ* λ* λt t; } a)
+(Merge) = λa λb (b λc switch c { 0: λd λe λf λg (g λi switch i { 0: λj let {j j_2 j_3} = j; λk let {k k_2} = k; λl let {l l_2 l_3} = l; λm let {m m_2 m_3} = m; λn let {n n_2} = n; (If (l m j) (List_/Cons m_2 (Merge l_2 n (List_/Cons j_2 k))) (List_/Cons j_3 (Merge l_3 (List_/Cons m_3 n_2) k_2))); _: λ* λ* λr λs (List_/Cons r s); } f d e); _: λ* λ* λu u; } a)
 
 (Bool/True) = λa (a Bool/True/tag)
 
diff --git a/tests/snapshots/run_file__list_reverse_imp.bend.snap b/tests/snapshots/run_file__list_reverse_imp.bend.snap
new file mode 100644
index 00000000..e6df2060
--- /dev/null
+++ b/tests/snapshots/run_file__list_reverse_imp.bend.snap
@@ -0,0 +1,9 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/run_file/list_reverse_imp.bend
+---
+NumScott:
+[1, 2, 3, 4, 5]
+
+Scott:
+[1, 2, 3, 4, 5]
diff --git a/tests/snapshots/simplify_matches__already_flat.bend.snap b/tests/snapshots/simplify_matches__already_flat.bend.snap
index 1b57c1cd..1e11decc 100644
--- a/tests/snapshots/simplify_matches__already_flat.bend.snap
+++ b/tests/snapshots/simplify_matches__already_flat.bend.snap
@@ -10,7 +10,7 @@ input_file: tests/golden_tests/simplify_matches/already_flat.bend
 
 (Rule4) = λa match a { Foo/CtrA: λb b; Foo/CtrB c: c; }
 
-(Rule5) = λa match a { Bar/CtrA1 b: λc (b c); Bar/CtrA2 d e: λf (d e f); Bar/CtrA3 g: λh (match h { Baz/CtrB0: λi (Bar/CtrA3 i); Baz/CtrB1 j: λk (Bar/CtrA3 k j); Baz/CtrB2 l: λm (Bar/CtrA3 m (Baz/CtrB2 l)); Baz/CtrB3 n: λo (o n); } g); }
+(Rule5) = λa match a { Bar/CtrA1 b: λc let d = c; (b d); Bar/CtrA2 e f: λg let h = g; (e f h); Bar/CtrA3 i: λj let k = j; (match k { Baz/CtrB0: λl (Bar/CtrA3 l); Baz/CtrB1 m: λn (Bar/CtrA3 n m); Baz/CtrB2 o: λp (Bar/CtrA3 p (Baz/CtrB2 o)); Baz/CtrB3 q: λr (r q); } i); }
 
 (Rule6) = λa a
 
diff --git a/tests/snapshots/simplify_matches__double_unwrap_box.bend.snap b/tests/snapshots/simplify_matches__double_unwrap_box.bend.snap
index 9d51b52e..bba06a8f 100644
--- a/tests/snapshots/simplify_matches__double_unwrap_box.bend.snap
+++ b/tests/snapshots/simplify_matches__double_unwrap_box.bend.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/double_unwrap_box.bend
 ---
-(DoubleUnbox) = λa match a { Boxed/Box b: match b { Boxed/Box c: λd c; }; }
+(DoubleUnbox) = λa match a { Boxed/Box b: match b { Boxed/Box c: λd let e = d; let f = e; c; }; }
 
 (Main) = (DoubleUnbox (Boxed/Box (Boxed/Box 0)) 5)
 
diff --git a/tests/snapshots/simplify_matches__double_unwrap_maybe.bend.snap b/tests/snapshots/simplify_matches__double_unwrap_maybe.bend.snap
index 5dbb1419..47244b40 100644
--- a/tests/snapshots/simplify_matches__double_unwrap_maybe.bend.snap
+++ b/tests/snapshots/simplify_matches__double_unwrap_maybe.bend.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/double_unwrap_maybe.bend
 ---
-(DoubleUnwrap) = λa match a { Maybe/Some b: match b { Maybe/Some c: λd c; Maybe/None: λe e; }; Maybe/None: λf f; }
+(DoubleUnwrap) = λa match a { Maybe/Some b: match b { Maybe/Some c: λd let e = d; let f = e; c; Maybe/None: λg let h = g; let i = h; i; }; Maybe/None: λj let k = j; k; }
 
 (Main) = (DoubleUnwrap (Maybe/Some Maybe/None) 5)
 
diff --git a/tests/snapshots/simplify_matches__flatten_with_terminal.bend.snap b/tests/snapshots/simplify_matches__flatten_with_terminal.bend.snap
index 5513fb0e..f5be9880 100644
--- a/tests/snapshots/simplify_matches__flatten_with_terminal.bend.snap
+++ b/tests/snapshots/simplify_matches__flatten_with_terminal.bend.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/flatten_with_terminal.bend
 ---
-(Foo) = λa switch a { 0: λb match b { A_t/A c: match c { B_t/B: B_t/B; }; }; _ d: λe *; }
+(Foo) = λa switch a { 0: λb let c = b; match c { A_t/A d: match d { B_t/B: B_t/B; }; }; _ e: λf let g = f; *; }
 
 (main) = (Foo 2 (A_t/A B_t/B))
 
diff --git a/tests/snapshots/simplify_matches__linearize_match_all.bend.snap b/tests/snapshots/simplify_matches__linearize_match_all.bend.snap
index 78f6b709..5235f9c7 100644
--- a/tests/snapshots/simplify_matches__linearize_match_all.bend.snap
+++ b/tests/snapshots/simplify_matches__linearize_match_all.bend.snap
@@ -10,7 +10,7 @@ input_file: tests/golden_tests/simplify_matches/linearize_match_all.bend
 
 (D) = λa switch a { 0: λb λc c; _ d: λe λf (d f); }
 
-(E) = λa match a { ConsList/Cons b c: λd (match d { ConsList/Cons e f: λg λh (g h e f); ConsList/Nil: λi λj (ConsList/Cons i j ConsList/Nil); } b c); ConsList/Nil: λk (ConsList/Nil k); }
+(E) = λa match a { ConsList/Cons b c: λd let e = d; (match e { ConsList/Cons f g: λh λi (h i f g); ConsList/Nil: λj λk (ConsList/Cons j k ConsList/Nil); } b c); ConsList/Nil: λl let m = l; (ConsList/Nil m); }
 
 (A2) = λa match a { ConsList/Cons b c: λd λe (b c d e); ConsList/Nil: λf λg (f g); }
 
diff --git a/tests/snapshots/simplify_matches__redundant_with_era.bend.snap b/tests/snapshots/simplify_matches__redundant_with_era.bend.snap
index 78a48999..b7c6e710 100644
--- a/tests/snapshots/simplify_matches__redundant_with_era.bend.snap
+++ b/tests/snapshots/simplify_matches__redundant_with_era.bend.snap
@@ -2,6 +2,6 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/redundant_with_era.bend
 ---
-(Fn2) = λa switch a { 0: λb let (c, d) = b; let (e, f) = d; f; _ g: λh let (i, j) = h; let (k, l) = j; l; }
+(Fn2) = λa switch a { 0: λb let c = b; let (d, e) = c; let (f, g) = e; g; _ h: λi let j = i; let (k, l) = j; let (m, n) = l; n; }
 
 (main) = *