From 0516c0036448b9aaf57d6f218f6c60c698097135 Mon Sep 17 00:00:00 2001
From: Yazalde Filimone <yazaldefilimon@gmail.com>
Date: Wed, 23 Sep 2026 17:01:11 +0200
Subject: [PATCH 1/4] feat(cli): add color choice and no-color options

---
 src/cli/mod.rs             | 19 +++++++++++++++++--
 src/cli/options/options.rs | 12 +++++++++---
 2 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/src/cli/mod.rs b/src/cli/mod.rs
index 653a80d..25deb32 100644
--- a/src/cli/mod.rs
+++ b/src/cli/mod.rs
@@ -3,7 +3,7 @@ pub mod options;
 use clap::Parser;
 use std::path::PathBuf;
 
-use self::options::{Emit, Encoding, Options};
+use self::options::{ColorChoice, Emit, Encoding, Options};
 
 #[derive(Debug, Parser)]
 #[command(
@@ -74,6 +74,15 @@ pub struct Cli {
   #[arg(short = 'q', long, help = "Quiet output")]
   pub quiet: bool,
 
+  #[arg(
+    long,
+    value_name = "WHEN",
+    default_value = "auto",
+    value_enum,
+    help = "Coloring: auto, always, never"
+  )]
+  pub color: ColorChoice,
+
   #[arg(long, help = "Disable color output")]
   pub no_color: bool,
 }
@@ -85,6 +94,12 @@ impl Cli {
       .or(self.input_flag)
       .expect("input file is required");
 
+    let color = if self.no_color {
+      ColorChoice::Never
+    } else {
+      self.color
+    };
+
     Options {
       input,
       output: self.output,
@@ -96,7 +111,7 @@ impl Cli {
       limit: self.limit,
       verbose: self.verbose,
       quiet: self.quiet,
-      no_color: self.no_color,
+      color,
     }
   }
 }
diff --git a/src/cli/options/options.rs b/src/cli/options/options.rs
index e800970..af86546 100644
--- a/src/cli/options/options.rs
+++ b/src/cli/options/options.rs
@@ -1,6 +1,13 @@
 use clap::ValueEnum;
 use std::path::PathBuf;
 
+#[derive(Debug, Clone, Copy, PartialEq, Eq, ValueEnum)]
+pub enum ColorChoice {
+  Auto,
+  Always,
+  Never,
+}
+
 #[derive(Debug, Clone)]
 pub struct Options {
   pub input: PathBuf,
@@ -14,8 +21,7 @@ pub struct Options {
   pub limit: usize,
   pub verbose: bool,
   pub quiet: bool,
-  #[allow(dead_code)]
-  pub no_color: bool,
+  pub color: ColorChoice,
 }
 
 impl Options {
@@ -32,7 +38,7 @@ impl Options {
       limit: 10000,
       verbose: false,
       quiet: false,
-      no_color: false,
+      color: ColorChoice::Auto,
     }
   }
 }

From af0cd0556271c7d92ed7fedf1727f24723e53e4b Mon Sep 17 00:00:00 2001
From: Yazalde Filimone <yazaldefilimon@gmail.com>
Date: Wed, 23 Sep 2026 17:05:59 +0200
Subject: [PATCH 2/4] feat(core): preserve lambda parameter names

---
 src/core/term.rs            | 20 +++++++++++++++++---
 src/evaluator/substitute.rs |  8 ++++++--
 src/parser/parser.rs        |  6 ++++--
 3 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/src/core/term.rs b/src/core/term.rs
index 9c0b5af..a582091 100644
--- a/src/core/term.rs
+++ b/src/core/term.rs
@@ -11,6 +11,7 @@ pub struct Term {
   pub variables: Arena<Variable>,
   pub lambdas: Arena<Lambda>,
   pub applies: Arena<Apply>,
+  pub parameters: Arena<Option<SymbolId>>,
   pub annotations: Arena<Option<TypeId>>,
   pub free_variables: Vec<SymbolId>,
   variable_cache: Vec<Option<TermId>>,
@@ -38,6 +39,7 @@ impl Term {
       variables: Arena::new(),
       lambdas: Arena::new(),
       applies: Arena::new(),
+      parameters: Arena::new(),
       annotations: Arena::new(),
       free_variables: Vec::new(),
       variable_cache: Vec::with_capacity(32),
@@ -81,25 +83,37 @@ impl Term {
     id
   }
 
+  #[allow(dead_code)]
   pub fn add_lambda(&mut self, lambda: Lambda) -> TermId {
-    self.add_annotated(lambda, None)
+    self.add_annotated(lambda, None, None)
   }
 
-  pub fn add_annotated(&mut self, lambda: Lambda, annotation: Option<TypeId>) -> TermId {
+  pub fn add_annotated(
+    &mut self,
+    lambda: Lambda,
+    parameter: Option<SymbolId>,
+    annotation: Option<TypeId>,
+  ) -> TermId {
     if annotation.is_none()
+      && parameter.is_none()
       && let Some(&id) = self.lambda_cache.get(&lambda.body)
     {
       return id;
     }
     let index = self.lambdas.add(lambda);
+    self.parameters.add(parameter);
     self.annotations.add(annotation);
     let id = TermId::lambda(index);
-    if annotation.is_none() {
+    if annotation.is_none() && parameter.is_none() {
       self.lambda_cache.insert(lambda.body, id);
     }
     id
   }
 
+  pub fn parameter(&self, id: LambdaId) -> Option<SymbolId> {
+    *self.parameters.get(Id::new(id.index()))
+  }
+
   pub fn annotation(&self, id: LambdaId) -> Option<TypeId> {
     *self.annotations.get(Id::new(id.index()))
   }
diff --git a/src/evaluator/substitute.rs b/src/evaluator/substitute.rs
index e16b9d5..0dfc67a 100644
--- a/src/evaluator/substitute.rs
+++ b/src/evaluator/substitute.rs
@@ -37,7 +37,9 @@ fn shift_lambda(ctx: &mut Context, term: TermId, id: LambdaId, delta: i32, cutof
     return term;
   }
   let new_lambda = Lambda { body: new_body };
-  ctx.terms.add_lambda(new_lambda)
+  let parameter = ctx.terms.parameter(id);
+  let annotation = ctx.terms.annotation(id);
+  ctx.terms.add_annotated(new_lambda, parameter, annotation)
 }
 
 fn shift_apply(ctx: &mut Context, term: TermId, id: ApplyId, delta: i32, cutoff: u32) -> TermId {
@@ -90,7 +92,9 @@ fn substitute_lambda(
     return term;
   }
   let new_lambda = Lambda { body: new_body };
-  ctx.terms.add_lambda(new_lambda)
+  let parameter = ctx.terms.parameter(id);
+  let annotation = ctx.terms.annotation(id);
+  ctx.terms.add_annotated(new_lambda, parameter, annotation)
 }
 
 fn substitute_apply(
diff --git a/src/parser/parser.rs b/src/parser/parser.rs
index 43515d7..002ef05 100644
--- a/src/parser/parser.rs
+++ b/src/parser/parser.rs
@@ -65,9 +65,11 @@ impl<'a> Parser<'a> {
     }
 
     let mut current = body;
-    for (_, annotation) in parameters.into_iter().rev() {
+    for (param_name, annotation) in parameters.into_iter().rev() {
       let lambda = Lambda { body: current };
-      current = self.terms.add_annotated(lambda, annotation);
+      current = self
+        .terms
+        .add_annotated(lambda, Some(param_name), annotation);
     }
 
     Ok(current)

From 82215ae625950555fa7f11bdc17bc14266067796 Mon Sep 17 00:00:00 2001
From: Yazalde Filimone <yazaldefilimon@gmail.com>
Date: Wed, 23 Sep 2026 17:07:02 +0200
Subject: [PATCH 3/4] perf(printer): optimize name picking and string
 allocations

---
 src/printer/mod.rs | 90 +++++++++++++++++++++++++++++-----------------
 1 file changed, 58 insertions(+), 32 deletions(-)

diff --git a/src/printer/mod.rs b/src/printer/mod.rs
index 9a0645c..9c75e34 100644
--- a/src/printer/mod.rs
+++ b/src/printer/mod.rs
@@ -1,9 +1,16 @@
+use std::fmt::Write;
+
 use crate::{
   context::Context,
   core::{ApplyId, LambdaId, TermId, TypeId},
   symbol::SymbolId,
 };
 
+const CANDIDATES: &[&str] = &[
+  "x", "y", "z", "w", "v", "u", "t", "s", "r", "q", "p", "a", "b", "c", "d", "e", "f", "g", "h",
+  "i", "j", "k", "l", "m", "n", "o",
+];
+
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub struct Options {
   pub collapse: bool,
@@ -18,21 +25,42 @@ impl Default for Options {
 pub struct Printer<'a> {
   ctx: &'a Context,
   options: Options,
+  free_vars_mask: u32,
 }
 
 impl<'a> Printer<'a> {
   pub fn new(ctx: &'a Context) -> Self {
-    Self { ctx, options: Options::default() }
+    let mut free_vars_mask = 0u32;
+    for (i, &cand) in CANDIDATES.iter().enumerate() {
+      let mut iterator = ctx.terms.free_variables.iter();
+      if iterator.any(|&sym| ctx.symbols.resolve(sym) == cand) {
+        free_vars_mask |= 1 << i;
+      }
+    }
+    Self { ctx, options: Options::default(), free_vars_mask }
   }
 
   #[allow(dead_code)]
   pub fn with_options(ctx: &'a Context, options: Options) -> Self {
-    Self { ctx, options }
+    let mut printer = Self::new(ctx);
+    printer.options = options;
+    printer
   }
 
   pub fn print_term(&self, term_id: TermId) -> String {
-    let mut out = String::new();
-    let mut names = Vec::new();
+    let mut out = String::with_capacity(64);
+    let mut names = Vec::with_capacity(16);
+    self.format_term(term_id, &mut names, &mut out);
+    out
+  }
+
+  pub fn print_term_in_scope(&self, term_id: TermId, scope: &[LambdaId]) -> String {
+    let mut out = String::with_capacity(64);
+    let mut names = Vec::with_capacity(scope.len() + 16);
+    for &lam_id in scope {
+      let name = self.pick_name(&names, Some(lam_id));
+      names.push(name);
+    }
     self.format_term(term_id, &mut names, &mut out);
     out
   }
@@ -44,44 +72,42 @@ impl<'a> Printer<'a> {
     out
   }
 
-  fn resolve_symbol(&self, symbol: SymbolId) -> &str {
+  fn resolve_symbol(&self, symbol: SymbolId) -> &'a str {
     self.ctx.symbols.resolve(symbol)
   }
 
-  fn pick_name(&self, names: &[String]) -> String {
-    const CANDIDATES: &[&str] = &[
-      "x", "y", "z", "w", "v", "u", "t", "s", "r", "q", "p", "a", "b", "c", "d", "e", "f", "g",
-      "h", "i", "j", "k", "l", "m", "n", "o",
-    ];
-    for &candidate in CANDIDATES {
-      let already_used = names.iter().any(|n| n == candidate);
-      let is_free = self
-        .ctx
-        .terms
-        .free_variables
-        .iter()
-        .any(|&sym| self.resolve_symbol(sym) == candidate);
-      if !already_used && !is_free {
-        return candidate.to_string();
+  fn pick_name(&self, names: &[&str], lam_id: Option<LambdaId>) -> &'a str {
+    if let Some(id) = lam_id
+      && let Some(sym) = self.ctx.terms.parameter(id)
+    {
+      let orig = self.resolve_symbol(sym);
+      if !names.contains(&orig) {
+        return orig;
+      }
+    }
+
+    for (i, &candidate) in CANDIDATES.iter().enumerate() {
+      if (self.free_vars_mask & (1 << i)) == 0 && !names.contains(&candidate) {
+        return candidate;
       }
     }
-    format!("x{}", names.len())
+    CANDIDATES[names.len() % CANDIDATES.len()]
   }
 
-  fn format_term(&self, term_id: TermId, names: &mut Vec<String>, out: &mut String) {
+  fn format_term(&self, term_id: TermId, names: &mut Vec<&'a str>, out: &mut String) {
     match term_id.kind() {
       crate::core::TermKind::Variable(var_id) => {
         let var = &self.ctx.terms.variables[var_id];
         let index = var.index as usize;
         if index < names.len() {
-          let name = &names[names.len() - 1 - index];
+          let name = names[names.len() - 1 - index];
           out.push_str(name);
         } else {
           let free_idx = index - names.len();
           if let Some(&sym) = self.ctx.terms.free_variables.get(free_idx) {
             out.push_str(self.resolve_symbol(sym));
           } else {
-            out.push_str(&format!("_{index}"));
+            let _ = write!(out, "_{index}");
           }
         }
       },
@@ -91,10 +117,10 @@ impl<'a> Printer<'a> {
         } else {
           let lam = &self.ctx.terms.lambdas[lam_id];
           let annotation = self.ctx.terms.annotation(lam_id);
-          let name = self.pick_name(names);
+          let name = self.pick_name(names, Some(lam_id));
           out.push('λ');
-          names.push(name.clone());
-          self.format_parameter(&name, annotation, out);
+          names.push(name);
+          self.format_parameter(name, annotation, out);
           out.push_str(". ");
           self.format_term(lam.body, names, out);
           names.pop();
@@ -109,7 +135,7 @@ impl<'a> Printer<'a> {
   fn format_collapsed_lambda(
     &self,
     mut current_id: LambdaId,
-    names: &mut Vec<String>,
+    names: &mut Vec<&'a str>,
     out: &mut String,
   ) {
     out.push('λ');
@@ -119,14 +145,14 @@ impl<'a> Printer<'a> {
     loop {
       let lam = &self.ctx.terms.lambdas[current_id];
       let annotation = self.ctx.terms.annotation(current_id);
-      let name = self.pick_name(names);
-      names.push(name.clone());
+      let name = self.pick_name(names, Some(current_id));
+      names.push(name);
       pushed_count += 1;
 
       if !first {
         out.push(' ');
       }
-      self.format_parameter(&name, annotation, out);
+      self.format_parameter(name, annotation, out);
       first = false;
 
       if let Some(next_id) = lam.body.as_lambda() {
@@ -151,7 +177,7 @@ impl<'a> Printer<'a> {
     }
   }
 
-  fn format_apply(&self, apply_id: ApplyId, names: &mut Vec<String>, out: &mut String) {
+  fn format_apply(&self, apply_id: ApplyId, names: &mut Vec<&'a str>, out: &mut String) {
     let apply = &self.ctx.terms.applies[apply_id];
 
     if apply.function.is_lambda() {

From 651322f0480ef6dbd5bc6b0ec36ab2cec99cb8b8 Mon Sep 17 00:00:00 2001
From: Yazalde Filimone <yazaldefilimon@gmail.com>
Date: Wed, 23 Sep 2026 17:08:09 +0200
Subject: [PATCH 4/4] feat(trace): add pretty terminal tracer

---
 src/context.rs                                | 18 +++-
 src/driver.rs                                 |  9 ++
 src/evaluator/beta.rs                         |  8 +-
 src/evaluator/mod.rs                          | 32 +++---
 src/evaluator/strategy/applicative.rs         | 39 ++++----
 src/evaluator/strategy/call_by_value.rs       | 17 +---
 src/evaluator/strategy/normal.rs              | 39 ++++----
 src/lib.rs                                    |  1 +
 src/trace/event.rs                            | 31 ++++++
 src/trace/mod.rs                              |  5 +
 src/trace/text.rs                             | 99 +++++++++++++++++++
 ...simple__full_normal_form_under_binder.snap |  2 +-
 tests/snapshots/02_booleans__not_true.snap    |  2 +-
 tests/snapshots/03_church__add_two_one.snap   |  2 +-
 tests/snapshots/03_church__arithmetic.snap    |  2 +-
 tests/snapshots/03_church__exponent.snap      |  2 +-
 tests/snapshots/03_church__leq_false.snap     |  2 +-
 tests/snapshots/03_church__leq_true.snap      |  2 +-
 tests/snapshots/03_church__mul_two_three.snap |  2 +-
 .../03_church__subtraction_positive.snap      |  2 +-
 .../03_church__subtraction_saturation.snap    |  2 +-
 tests/snapshots/03_church__succ_zero.snap     |  2 +-
 .../04_combinators__b_combinator.snap         |  4 +-
 .../04_combinators__c_combinator.snap         |  4 +-
 .../04_combinators__kleene_pred.snap          |  2 +-
 .../04_combinators__w_combinator.snap         |  4 +-
 ...s_and_captures__barendregt_deep_shift.snap |  2 +-
 ..._captures__free_var_capture_avoidance.snap |  2 +-
 ...nd_captures__nested_capture_avoidance.snap |  4 +-
 ...pairs_and_recursion__church_pred_zero.snap |  2 +-
 ...irs_and_recursion__church_predecessor.snap |  2 +-
 .../06_pairs_and_recursion__factorial.snap    |  2 +-
 .../06_pairs_and_recursion__fibonacci.snap    |  2 +-
 .../06_pairs_and_recursion__list_map.snap     |  2 +-
 34 files changed, 260 insertions(+), 92 deletions(-)
 create mode 100644 src/trace/event.rs
 create mode 100644 src/trace/mod.rs
 create mode 100644 src/trace/text.rs

diff --git a/src/context.rs b/src/context.rs
index a002664..0124d73 100644
--- a/src/context.rs
+++ b/src/context.rs
@@ -1,11 +1,18 @@
 use crate::{
   cli::options::Options,
-  core::{Term, Type},
+  core::{LambdaId, Term, TermId, Type},
   loader::Loader,
   messages::Messages,
-  symbol::interner::Interner,
+  symbol::{SymbolId, interner::Interner},
 };
 
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub struct Redex {
+  pub lambda: LambdaId,
+  pub argument: TermId,
+  pub variable: Option<SymbolId>,
+}
+
 pub struct Context {
   pub options: Options,
   pub messages: Messages,
@@ -13,9 +20,13 @@ pub struct Context {
   pub symbols: Interner,
   pub terms: Term,
   pub types: Type,
+  pub redex: Option<Redex>,
+  pub current_scope: Vec<LambdaId>,
+  pub redex_scope: Vec<LambdaId>,
 }
 
 impl Context {
+  #[inline]
   pub fn new(options: Options) -> Self {
     Self {
       options,
@@ -24,6 +35,9 @@ impl Context {
       symbols: Interner::new(),
       terms: Term::new(),
       types: Type::new(),
+      redex: None,
+      current_scope: Vec::with_capacity(32),
+      redex_scope: Vec::with_capacity(32),
     }
   }
 }
diff --git a/src/driver.rs b/src/driver.rs
index 6ff4b80..5977800 100644
--- a/src/driver.rs
+++ b/src/driver.rs
@@ -119,6 +119,15 @@ impl<'a> Driver<'a> {
       return Ok(());
     }
 
+    if self.ctx.options.trace {
+      if let Some(term_stats) = term_stats {
+        println!();
+        let stats = crate::stats::Stats::new(term_stats, eval_stats);
+        stats.print();
+      }
+      return Ok(());
+    }
+
     if let Some(term_stats) = term_stats {
       if self.ctx.options.verbose {
         let printer = Printer::new(self.ctx);
diff --git a/src/evaluator/beta.rs b/src/evaluator/beta.rs
index 2ad9cbe..e469669 100644
--- a/src/evaluator/beta.rs
+++ b/src/evaluator/beta.rs
@@ -1,11 +1,17 @@
 use crate::{
-  context::Context,
+  context::{Context, Redex},
   core::{LambdaId, TermId},
   evaluator::substitute,
   result,
 };
 
 pub fn reduce(ctx: &mut Context, lambda_id: LambdaId, argument: TermId) -> result::Result<TermId> {
+  if ctx.options.trace {
+    let variable = ctx.terms.parameter(lambda_id);
+    ctx.redex_scope.clear();
+    ctx.redex_scope.extend_from_slice(&ctx.current_scope);
+    ctx.redex = Some(Redex { lambda: lambda_id, argument, variable });
+  }
   let lambda = *ctx.terms.lambdas.get(lambda_id);
   let result = substitute::substitute(ctx, 0, argument, lambda.body);
   Ok(result)
diff --git a/src/evaluator/mod.rs b/src/evaluator/mod.rs
index ab710ee..99db10a 100644
--- a/src/evaluator/mod.rs
+++ b/src/evaluator/mod.rs
@@ -10,8 +10,8 @@ use crate::{
   context::Context,
   core::{Apply, Lambda, LambdaId, TermId},
   error,
-  printer::Printer,
   result::{self, Failed},
+  trace::{Reduction, ReductionRule, TextTracer},
 };
 use strategy::Strategy;
 
@@ -29,6 +29,7 @@ pub struct Evaluator<'a> {
   strategy: strategy::Strategy,
   trace: bool,
   spine: Vec<TermId>,
+  tracer: Option<TextTracer>,
   pub stats: EvalStats,
 }
 
@@ -41,7 +42,8 @@ impl<'a> Evaluator<'a> {
     let strategy = Strategy::new(strategy_options);
     let stats = EvalStats::default();
     let spine = Vec::with_capacity(128);
-    Self { ctx, strategy, trace, spine, stats }
+    let tracer = if trace { Some(TextTracer::new(ctx)) } else { None };
+    Self { ctx, strategy, trace, spine, tracer, stats }
   }
 
   pub fn eval(&mut self, mut term: TermId) -> result::Result<TermId> {
@@ -71,11 +73,22 @@ impl<'a> Evaluator<'a> {
       let Some(next) = next_opt else {
         self.stats.duration = start.elapsed();
         self.stats.created_terms = self.ctx.terms.total_terms().saturating_sub(initial_terms);
+        if let Some(tracer) = &mut self.tracer {
+          tracer.on_finish(self.ctx, term);
+        }
         return Ok(term);
       };
 
-      if self.trace {
-        self.debug_step(term, next);
+      if let Some(tracer) = &mut self.tracer {
+        let redex = self.ctx.redex.take();
+        let reduction = Reduction {
+          step: steps + 1,
+          rule: ReductionRule::Beta,
+          before: term,
+          after: next,
+          redex,
+        };
+        tracer.on_step(self.ctx, &reduction);
       }
 
       term = next;
@@ -159,7 +172,9 @@ impl<'a> Evaluator<'a> {
       return Ok(term);
     }
     let new_lambda = Lambda { body: normalized_body };
-    let new_id = self.ctx.terms.add_lambda(new_lambda);
+    let parameter = self.ctx.terms.parameter(lambda_id);
+    let annotation = self.ctx.terms.annotation(lambda_id);
+    let new_id = self.ctx.terms.add_annotated(new_lambda, parameter, annotation);
     Ok(new_id)
   }
 
@@ -174,11 +189,4 @@ impl<'a> Evaluator<'a> {
     }
     Ok(term)
   }
-
-  fn debug_step(&self, term: TermId, next: TermId) {
-    let printer = Printer::new(self.ctx);
-    let term_str = printer.print_term(term);
-    let next_str = printer.print_term(next);
-    eprintln!("{term_str} -> {next_str}");
-  }
 }
diff --git a/src/evaluator/strategy/applicative.rs b/src/evaluator/strategy/applicative.rs
index 7b3dcc0..6920455 100644
--- a/src/evaluator/strategy/applicative.rs
+++ b/src/evaluator/strategy/applicative.rs
@@ -17,47 +17,48 @@ pub fn reduce(
       if let Some(function) = reduce(apply.function, ctx, options)? {
         let new_apply = Apply { function, argument: apply.argument };
         let new_id = ctx.terms.add_apply(new_apply);
-        let result = Some(new_id);
-        return Ok(result);
+        return Ok(Some(new_id));
       }
 
       if let Some(argument) = reduce(apply.argument, ctx, options)? {
         let new_apply = Apply { function: apply.function, argument };
         let new_id = ctx.terms.add_apply(new_apply);
-        let result = Some(new_id);
-        return Ok(result);
+        return Ok(Some(new_id));
       }
 
       if let Some(lambda_id) = apply.function.as_lambda() {
         let reduced = beta::reduce(ctx, lambda_id, apply.argument)?;
-        let result = Some(reduced);
-        return Ok(result);
+        return Ok(Some(reduced));
       }
 
-      let result = None;
-      Ok(result)
+      Ok(None)
     },
     TermKind::Lambda(id) => {
       if options.lazy {
-        let result = None;
-        return Ok(result);
+        return Ok(None);
+      }
+
+      if ctx.options.trace {
+        ctx.current_scope.push(id);
       }
 
       let lambda = *ctx.terms.lambdas.get(id);
       let body_step = reduce(lambda.body, ctx, options)?;
+
+      if ctx.options.trace {
+        ctx.current_scope.pop();
+      }
+
       if let Some(new_body) = body_step {
         let new_lambda = Lambda { body: new_body };
-        let new_id = ctx.terms.add_lambda(new_lambda);
-        let result = Some(new_id);
-        return Ok(result);
+        let parameter = ctx.terms.parameter(id);
+        let annotation = ctx.terms.annotation(id);
+        let new_id = ctx.terms.add_annotated(new_lambda, parameter, annotation);
+        return Ok(Some(new_id));
       }
 
-      let result = None;
-      Ok(result)
-    },
-    TermKind::Variable(_) => {
-      let result = None;
-      Ok(result)
+      Ok(None)
     },
+    TermKind::Variable(_) => Ok(None),
   }
 }
diff --git a/src/evaluator/strategy/call_by_value.rs b/src/evaluator/strategy/call_by_value.rs
index ac7caea..365233d 100644
--- a/src/evaluator/strategy/call_by_value.rs
+++ b/src/evaluator/strategy/call_by_value.rs
@@ -17,29 +17,22 @@ pub fn reduce(
       if let Some(function) = reduce(apply.function, ctx, options)? {
         let new_apply = Apply { function, ..apply };
         let new_id = ctx.terms.add_apply(new_apply);
-        let result = Some(new_id);
-        return Ok(result);
+        return Ok(Some(new_id));
       }
 
       if let Some(argument) = reduce(apply.argument, ctx, options)? {
         let new_apply = Apply { argument, ..apply };
         let new_id = ctx.terms.add_apply(new_apply);
-        let result = Some(new_id);
-        return Ok(result);
+        return Ok(Some(new_id));
       }
 
       if let Some(lambda_id) = apply.function.as_lambda() {
         let reduced = beta::reduce(ctx, lambda_id, apply.argument)?;
-        let result = Some(reduced);
-        return Ok(result);
+        return Ok(Some(reduced));
       }
 
-      let result = None;
-      Ok(result)
-    },
-    TermKind::Lambda(_) | TermKind::Variable(_) => {
-      let result = None;
-      Ok(result)
+      Ok(None)
     },
+    TermKind::Lambda(_) | TermKind::Variable(_) => Ok(None),
   }
 }
diff --git a/src/evaluator/strategy/normal.rs b/src/evaluator/strategy/normal.rs
index e11e6d8..051ac30 100644
--- a/src/evaluator/strategy/normal.rs
+++ b/src/evaluator/strategy/normal.rs
@@ -16,50 +16,51 @@ pub fn reduce(
       match apply.function.kind() {
         TermKind::Lambda(lambda_id) => {
           let reduced = beta::reduce(ctx, lambda_id, apply.argument)?;
-          let result = Some(reduced);
-          Ok(result)
+          Ok(Some(reduced))
         },
         _ => {
           if let Some(function) = reduce(apply.function, ctx, options)? {
             let new_apply = Apply { function, argument: apply.argument };
             let new_id = ctx.terms.add_apply(new_apply);
-            let result = Some(new_id);
-            return Ok(result);
+            return Ok(Some(new_id));
           }
 
           if let Some(argument) = reduce(apply.argument, ctx, options)? {
             let new_apply = Apply { function: apply.function, argument };
             let new_id = ctx.terms.add_apply(new_apply);
-            let result = Some(new_id);
-            return Ok(result);
+            return Ok(Some(new_id));
           }
 
-          let result = None;
-          Ok(result)
+          Ok(None)
         },
       }
     },
     TermKind::Lambda(id) => {
       if options.lazy {
-        let result = None;
-        return Ok(result);
+        return Ok(None);
+      }
+
+      if ctx.options.trace {
+        ctx.current_scope.push(id);
       }
 
       let lambda = *ctx.terms.lambdas.get(id);
       let body_step = reduce(lambda.body, ctx, options)?;
+
+      if ctx.options.trace {
+        ctx.current_scope.pop();
+      }
+
       if let Some(new_body) = body_step {
         let new_lambda = Lambda { body: new_body };
-        let new_id = ctx.terms.add_lambda(new_lambda);
-        let result = Some(new_id);
-        return Ok(result);
+        let parameter = ctx.terms.parameter(id);
+        let annotation = ctx.terms.annotation(id);
+        let new_id = ctx.terms.add_annotated(new_lambda, parameter, annotation);
+        return Ok(Some(new_id));
       }
 
-      let result = None;
-      Ok(result)
-    },
-    TermKind::Variable(_) => {
-      let result = None;
-      Ok(result)
+      Ok(None)
     },
+    TermKind::Variable(_) => Ok(None),
   }
 }
diff --git a/src/lib.rs b/src/lib.rs
index 6ebda92..ead4597 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -13,3 +13,4 @@ pub mod result;
 pub mod source;
 pub mod stats;
 pub mod symbol;
+pub mod trace;
diff --git a/src/trace/event.rs b/src/trace/event.rs
new file mode 100644
index 0000000..278136a
--- /dev/null
+++ b/src/trace/event.rs
@@ -0,0 +1,31 @@
+use crate::{context::Redex, core::TermId};
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[allow(dead_code)]
+pub enum ReductionRule {
+  Alpha,
+  Beta,
+  Eta,
+  Delta,
+}
+
+impl ReductionRule {
+  pub fn symbol(&self) -> &'static str {
+    match self {
+      Self::Alpha => "α",
+      Self::Beta => "β",
+      Self::Eta => "η",
+      Self::Delta => "δ",
+    }
+  }
+}
+
+#[derive(Debug, Clone, Copy)]
+pub struct Reduction {
+  #[allow(dead_code)]
+  pub step: usize,
+  pub rule: ReductionRule,
+  pub before: TermId,
+  pub after: TermId,
+  pub redex: Option<Redex>,
+}
diff --git a/src/trace/mod.rs b/src/trace/mod.rs
new file mode 100644
index 0000000..0cf9861
--- /dev/null
+++ b/src/trace/mod.rs
@@ -0,0 +1,5 @@
+mod event;
+mod text;
+
+pub use event::*;
+pub use text::*;
diff --git a/src/trace/text.rs b/src/trace/text.rs
new file mode 100644
index 0000000..95ff565
--- /dev/null
+++ b/src/trace/text.rs
@@ -0,0 +1,99 @@
+use std::io::{self, BufWriter, IsTerminal, Stdout, Write};
+
+use crate::{
+  cli::options::ColorChoice, context::Context, core::TermId, printer::Printer,
+  trace::event::Reduction,
+};
+
+const DIM: &str = "\x1b[90m";
+const CYAN: &str = "\x1b[36m";
+const YELLOW: &str = "\x1b[33m";
+const GREEN: &str = "\x1b[32m";
+const RESET: &str = "\x1b[0m";
+
+pub struct TextTracer {
+  color: bool,
+  first: bool,
+  buffered: Option<TermId>,
+  out: BufWriter<Stdout>,
+}
+
+impl TextTracer {
+  pub fn new(ctx: &Context) -> Self {
+    let no_color_env = std::env::var_os("NO_COLOR").is_some();
+    let color = match ctx.options.color {
+      ColorChoice::Always => true,
+      ColorChoice::Never => false,
+      ColorChoice::Auto => !no_color_env && io::stdout().is_terminal(),
+    };
+    let out = BufWriter::new(io::stdout());
+    Self { color, first: true, buffered: None, out }
+  }
+
+  #[allow(dead_code)]
+  pub fn with_color(color: bool) -> Self {
+    let out = BufWriter::new(io::stdout());
+    Self { color, first: true, buffered: None, out }
+  }
+
+  pub fn on_step(&mut self, ctx: &Context, reduction: &Reduction) {
+    let printer = Printer::new(ctx);
+
+    if self.first {
+      let before = printer.print_term(reduction.before);
+      let _ = writeln!(self.out, "{before}");
+      self.first = false;
+    } else if let Some(prev) = self.buffered.take() {
+      let prev_str = printer.print_term(prev);
+      let _ = writeln!(self.out, "{prev_str}");
+    }
+
+    self.write_transition(ctx, &printer, reduction);
+    self.buffered = Some(reduction.after);
+  }
+
+  fn write_transition(&mut self, ctx: &Context, printer: &Printer, reduction: &Reduction) {
+    let rule = reduction.rule.symbol();
+
+    if let Some(redex) = &reduction.redex {
+      let var = redex.variable.map_or("x", |s| ctx.symbols.resolve(s));
+      let val = printer.print_term_in_scope(redex.argument, &ctx.redex_scope);
+
+      if self.color {
+        let _ =
+          writeln!(self.out, "{DIM}│{RESET} {CYAN}{rule}{RESET} ({var} {YELLOW}↦{RESET} {val})");
+        let _ = writeln!(self.out, "{DIM}↓{RESET}");
+      } else {
+        let _ = writeln!(self.out, "│ {rule} ({var} ↦ {val})");
+        let _ = writeln!(self.out, "↓");
+      }
+    } else if self.color {
+      let _ = writeln!(self.out, "{DIM}│{RESET} {CYAN}{rule}{RESET}");
+      let _ = writeln!(self.out, "{DIM}↓{RESET}");
+    } else {
+      let _ = writeln!(self.out, "│ {rule}");
+      let _ = writeln!(self.out, "↓");
+    }
+  }
+
+  pub fn on_finish(&mut self, ctx: &Context, final_term: TermId) {
+    let printer = Printer::new(ctx);
+    let term = printer.print_term(final_term);
+
+    if self.buffered.take().is_some() || self.first {
+      if self.color {
+        let _ = writeln!(self.out, "{GREEN}{term}{RESET}");
+      } else {
+        let _ = writeln!(self.out, "{term}");
+      }
+    }
+
+    let _ = self.out.flush();
+  }
+}
+
+impl Drop for TextTracer {
+  fn drop(&mut self) {
+    let _ = self.out.flush();
+  }
+}
diff --git a/tests/snapshots/01_simple__full_normal_form_under_binder.snap b/tests/snapshots/01_simple__full_normal_form_under_binder.snap
index c9639ac..74f085f 100644
--- a/tests/snapshots/01_simple__full_normal_form_under_binder.snap
+++ b/tests/snapshots/01_simple__full_normal_form_under_binder.snap
@@ -3,7 +3,7 @@ source: tests/golden.rs
 expression: snapshot_content
 input_file: tests/golden/01_simple/full_normal_form_under_binder.lam
 ---
-λx. λy. y x
+λx. λz. z x
 
 term
   nodes: 8
diff --git a/tests/snapshots/02_booleans__not_true.snap b/tests/snapshots/02_booleans__not_true.snap
index db4dec7..eb30ce4 100644
--- a/tests/snapshots/02_booleans__not_true.snap
+++ b/tests/snapshots/02_booleans__not_true.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    6
   reduces:  6
-  allocs:   9
+  allocs:   11
   time:     [time]
diff --git a/tests/snapshots/03_church__add_two_one.snap b/tests/snapshots/03_church__add_two_one.snap
index e8925c9..4000796 100644
--- a/tests/snapshots/03_church__add_two_one.snap
+++ b/tests/snapshots/03_church__add_two_one.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    18
   reduces:  18
-  allocs:   46
+  allocs:   49
   time:     [time]
diff --git a/tests/snapshots/03_church__arithmetic.snap b/tests/snapshots/03_church__arithmetic.snap
index e5ed3e5..11a5521 100644
--- a/tests/snapshots/03_church__arithmetic.snap
+++ b/tests/snapshots/03_church__arithmetic.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    18
   reduces:  18
-  allocs:   65
+  allocs:   66
   time:     [time]
diff --git a/tests/snapshots/03_church__exponent.snap b/tests/snapshots/03_church__exponent.snap
index 0029a54..77751fa 100644
--- a/tests/snapshots/03_church__exponent.snap
+++ b/tests/snapshots/03_church__exponent.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    19
   reduces:  19
-  allocs:   44
+  allocs:   48
   time:     [time]
diff --git a/tests/snapshots/03_church__leq_false.snap b/tests/snapshots/03_church__leq_false.snap
index 4e2a40d..cbc9e7d 100644
--- a/tests/snapshots/03_church__leq_false.snap
+++ b/tests/snapshots/03_church__leq_false.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    80
   reduces:  80
-  allocs:   264
+  allocs:   268
   time:     [time]
diff --git a/tests/snapshots/03_church__leq_true.snap b/tests/snapshots/03_church__leq_true.snap
index bc7c4c8..2e7e7c5 100644
--- a/tests/snapshots/03_church__leq_true.snap
+++ b/tests/snapshots/03_church__leq_true.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    86
   reduces:  86
-  allocs:   231
+  allocs:   243
   time:     [time]
diff --git a/tests/snapshots/03_church__mul_two_three.snap b/tests/snapshots/03_church__mul_two_three.snap
index a39a22a..340ed91 100644
--- a/tests/snapshots/03_church__mul_two_three.snap
+++ b/tests/snapshots/03_church__mul_two_three.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    36
   reduces:  36
-  allocs:   86
+  allocs:   99
   time:     [time]
diff --git a/tests/snapshots/03_church__subtraction_positive.snap b/tests/snapshots/03_church__subtraction_positive.snap
index bdefcdb..0cafb25 100644
--- a/tests/snapshots/03_church__subtraction_positive.snap
+++ b/tests/snapshots/03_church__subtraction_positive.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    136
   reduces:  136
-  allocs:   359
+  allocs:   367
   time:     [time]
diff --git a/tests/snapshots/03_church__subtraction_saturation.snap b/tests/snapshots/03_church__subtraction_saturation.snap
index efd51a6..9135269 100644
--- a/tests/snapshots/03_church__subtraction_saturation.snap
+++ b/tests/snapshots/03_church__subtraction_saturation.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    103
   reduces:  103
-  allocs:   235
+  allocs:   254
   time:     [time]
diff --git a/tests/snapshots/03_church__succ_zero.snap b/tests/snapshots/03_church__succ_zero.snap
index 841e0d1..20c8cb3 100644
--- a/tests/snapshots/03_church__succ_zero.snap
+++ b/tests/snapshots/03_church__succ_zero.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    5
   reduces:  5
-  allocs:   8
+  allocs:   10
   time:     [time]
diff --git a/tests/snapshots/04_combinators__b_combinator.snap b/tests/snapshots/04_combinators__b_combinator.snap
index b390ff9..fafd650 100644
--- a/tests/snapshots/04_combinators__b_combinator.snap
+++ b/tests/snapshots/04_combinators__b_combinator.snap
@@ -3,7 +3,7 @@ source: tests/golden.rs
 expression: snapshot_content
 input_file: tests/golden/04_combinators/b_combinator.lam
 ---
-λx. λy. λz. x (y z)
+λf. λg. λx. f (g x)
 
 term
   nodes: 20
@@ -12,5 +12,5 @@ term
 eval
   steps:    4
   reduces:  4
-  allocs:   13
+  allocs:   16
   time:     [time]
diff --git a/tests/snapshots/04_combinators__c_combinator.snap b/tests/snapshots/04_combinators__c_combinator.snap
index 7b677cc..180758a 100644
--- a/tests/snapshots/04_combinators__c_combinator.snap
+++ b/tests/snapshots/04_combinators__c_combinator.snap
@@ -3,7 +3,7 @@ source: tests/golden.rs
 expression: snapshot_content
 input_file: tests/golden/04_combinators/c_combinator.lam
 ---
-λx. λy. λz. x z y
+λf. λx. λy. f y x
 
 term
   nodes: 20
@@ -12,5 +12,5 @@ term
 eval
   steps:    4
   reduces:  4
-  allocs:   14
+  allocs:   17
   time:     [time]
diff --git a/tests/snapshots/04_combinators__kleene_pred.snap b/tests/snapshots/04_combinators__kleene_pred.snap
index 010c2a3..dd08721 100644
--- a/tests/snapshots/04_combinators__kleene_pred.snap
+++ b/tests/snapshots/04_combinators__kleene_pred.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    15
   reduces:  15
-  allocs:   48
+  allocs:   102
   time:     [time]
diff --git a/tests/snapshots/04_combinators__w_combinator.snap b/tests/snapshots/04_combinators__w_combinator.snap
index bb718dc..a9d8a81 100644
--- a/tests/snapshots/04_combinators__w_combinator.snap
+++ b/tests/snapshots/04_combinators__w_combinator.snap
@@ -3,7 +3,7 @@ source: tests/golden.rs
 expression: snapshot_content
 input_file: tests/golden/04_combinators/w_combinator.lam
 ---
-λx. λy. x y y
+λf. λx. f x x
 
 term
   nodes: 16
@@ -12,5 +12,5 @@ term
 eval
   steps:    3
   reduces:  3
-  allocs:   7
+  allocs:   9
   time:     [time]
diff --git a/tests/snapshots/05_scopes_and_captures__barendregt_deep_shift.snap b/tests/snapshots/05_scopes_and_captures__barendregt_deep_shift.snap
index a218027..4711919 100644
--- a/tests/snapshots/05_scopes_and_captures__barendregt_deep_shift.snap
+++ b/tests/snapshots/05_scopes_and_captures__barendregt_deep_shift.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    4
   reduces:  4
-  allocs:   8
+  allocs:   9
   time:     [time]
diff --git a/tests/snapshots/05_scopes_and_captures__free_var_capture_avoidance.snap b/tests/snapshots/05_scopes_and_captures__free_var_capture_avoidance.snap
index b2edaf7..5ecb516 100644
--- a/tests/snapshots/05_scopes_and_captures__free_var_capture_avoidance.snap
+++ b/tests/snapshots/05_scopes_and_captures__free_var_capture_avoidance.snap
@@ -3,7 +3,7 @@ source: tests/golden.rs
 expression: snapshot_content
 input_file: tests/golden/05_scopes_and_captures/free_var_capture_avoidance.lam
 ---
-λx. y
+λy. y
 
 term
   nodes: 5
diff --git a/tests/snapshots/05_scopes_and_captures__nested_capture_avoidance.snap b/tests/snapshots/05_scopes_and_captures__nested_capture_avoidance.snap
index cf14893..14c7695 100644
--- a/tests/snapshots/05_scopes_and_captures__nested_capture_avoidance.snap
+++ b/tests/snapshots/05_scopes_and_captures__nested_capture_avoidance.snap
@@ -3,7 +3,7 @@ source: tests/golden.rs
 expression: snapshot_content
 input_file: tests/golden/05_scopes_and_captures/nested_capture_avoidance.lam
 ---
-λy. x
+λx. x
 
 term
   nodes: 10
@@ -12,5 +12,5 @@ term
 eval
   steps:    2
   reduces:  2
-  allocs:   5
+  allocs:   7
   time:     [time]
diff --git a/tests/snapshots/06_pairs_and_recursion__church_pred_zero.snap b/tests/snapshots/06_pairs_and_recursion__church_pred_zero.snap
index 0662768..23bb7b5 100644
--- a/tests/snapshots/06_pairs_and_recursion__church_pred_zero.snap
+++ b/tests/snapshots/06_pairs_and_recursion__church_pred_zero.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    13
   reduces:  13
-  allocs:   45
+  allocs:   46
   time:     [time]
diff --git a/tests/snapshots/06_pairs_and_recursion__church_predecessor.snap b/tests/snapshots/06_pairs_and_recursion__church_predecessor.snap
index a6f4a48..1bf01b9 100644
--- a/tests/snapshots/06_pairs_and_recursion__church_predecessor.snap
+++ b/tests/snapshots/06_pairs_and_recursion__church_predecessor.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    30
   reduces:  30
-  allocs:   83
+  allocs:   84
   time:     [time]
diff --git a/tests/snapshots/06_pairs_and_recursion__factorial.snap b/tests/snapshots/06_pairs_and_recursion__factorial.snap
index 1b5b958..79402fa 100644
--- a/tests/snapshots/06_pairs_and_recursion__factorial.snap
+++ b/tests/snapshots/06_pairs_and_recursion__factorial.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    652
   reduces:  652
-  allocs:   691
+  allocs:   2772
   time:     [time]
diff --git a/tests/snapshots/06_pairs_and_recursion__fibonacci.snap b/tests/snapshots/06_pairs_and_recursion__fibonacci.snap
index a320200..b3d5562 100644
--- a/tests/snapshots/06_pairs_and_recursion__fibonacci.snap
+++ b/tests/snapshots/06_pairs_and_recursion__fibonacci.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    237
   reduces:  237
-  allocs:   305
+  allocs:   595
   time:     [time]
diff --git a/tests/snapshots/06_pairs_and_recursion__list_map.snap b/tests/snapshots/06_pairs_and_recursion__list_map.snap
index 5d88abc..55e0dc2 100644
--- a/tests/snapshots/06_pairs_and_recursion__list_map.snap
+++ b/tests/snapshots/06_pairs_and_recursion__list_map.snap
@@ -12,5 +12,5 @@ term
 eval
   steps:    57
   reduces:  57
-  allocs:   238
+  allocs:   240
   time:     [time]