[sc-653] Reorder compiled redexes recursive last

cspell.json

@@ -15,6 +15,7 @@
     "combinators",
     "concat",
     "ctrs",
+    "cuda",
     "Dall",
     "datatypes",
     "Deque",

src/diagnostics.rs

@@ -235,15 +235,6 @@ impl DiagnosticsConfig {
     }
   }
 
-  pub fn default_strict() -> Self {
-    // TODO: Pre-reduce recursion check disabled while execution not implemented for hvm32
-    Self { recursion_cycle: Severity::Error, ..Self::default() }
-  }
-
-  pub fn default_lazy() -> Self {
-    Self { recursion_cycle: Severity::Allow, ..Self::default() }
-  }
-
   pub fn warning_severity(&self, warn: WarningType) -> Severity {
     match warn {
       WarningType::UnusedDefinition => self.unused_definition,
@@ -258,7 +249,9 @@ impl DiagnosticsConfig {
 
 impl Default for DiagnosticsConfig {
   fn default() -> Self {
-    Self::new(Severity::Warning, false)
+    let mut cfg = Self::new(Severity::Warning, false);
+    cfg.recursion_cycle = Severity::Error;
+    cfg
   }
 }
 

src/hvmc_net/mod.rs

@@ -1,2 +1,3 @@
 pub mod check_net_size;
 pub mod mutual_recursion;
+pub mod reorder_redexes;

src/hvmc_net/mutual_recursion.rs

@@ -1,5 +1,6 @@
 use crate::{
   diagnostics::{Diagnostics, WarningType, ERR_INDENT_SIZE},
+  maybe_grow,
   term::transform::definition_merge::MERGE_SEPARATOR,
 };
 use hvmc::ast::{Book, Tree};
@@ -101,8 +102,9 @@ impl Graph {
   }
 }
 
+/// Collect active refs from the tree.
 fn collect_refs(current: Ref, tree: &Tree, graph: &mut Graph) {
-  match tree {
+  maybe_grow(|| match tree {
     Tree::Ref { nam } => graph.add(current, nam.clone()),
     Tree::Ctr { ports, .. } => {
       if let Some(last) = ports.last() {
@@ -114,7 +116,7 @@ fn collect_refs(current: Ref, tree: &Tree, graph: &mut Graph) {
         collect_refs(current.clone(), subtree, graph);
       }
     }
-  }
+  });
 }
 
 impl From<&Book> for Graph {
@@ -122,13 +124,17 @@ impl From<&Book> for Graph {
     let mut graph = Self::new();
 
     for (r#ref, net) in book.iter() {
-      // Collect active refs from root.
+      // Collect active refs from the root.
       collect_refs(r#ref.clone(), &net.root, &mut graph);
-      for (left, _) in net.redexes.iter() {
+
-        // If left is an active reference, add to the graph.
+      // Collect active refs from redexes.
+      for (left, right) in net.redexes.iter() {
         if let Tree::Ref { nam } = left {
           graph.add(r#ref.clone(), nam.clone());
         }
+        if let Tree::Ref { nam } = right {
+          graph.add(r#ref.clone(), nam.clone());
+        }
       }
     }
 

src/hvmc_net/reorder_redexes.rs

@@ -0,0 +1,120 @@
+use hvmc::ast::{Book, Net, Tree};
+use std::collections::{HashMap, HashSet};
+
+use crate::maybe_grow;
+
+/// Reorder redexes in the book to have more efficient execution.
+///
+/// Especially for hvm-cuda, we want to keep the number of nodes/vars/redexes
+/// low so we put redexes with recursive refs last (at the bottom of the stack).
+pub fn reorder_redexes_recursive_last(book: &mut Book) {
+  // Direct dependencies
+  let deps = book.iter().map(|(nam, net)| (nam.clone(), dependencies(net))).collect::<HashMap<_, _>>();
+
+  // Look at dependencies to find if recursive
+  let recursive_nets = cycles(&deps).into_iter().flatten().collect::<HashSet<_>>();
+
+  for net in book.values_mut() {
+    reorder_redexes_net(net, &recursive_nets);
+  }
+}
+
+/// Reorder redexes to have recursive last (bottom of the stack).
+fn reorder_redexes_net(net: &mut Net, recursive_nets: &HashSet<String>) {
+  let mut recursive_redexes = vec![];
+  let mut non_recursive_redexes = vec![];
+
+  for (a, b) in std::mem::take(&mut net.redexes) {
+    if tree_has_recursive(&a, recursive_nets) || tree_has_recursive(&b, recursive_nets) {
+      recursive_redexes.push((a, b));
+    } else {
+      non_recursive_redexes.push((a, b));
+    }
+  }
+  let mut redexes = recursive_redexes;
+  redexes.append(&mut non_recursive_redexes);
+  net.redexes = redexes;
+}
+
+/// Whether a tree has a reference to a recursive net or not.
+fn tree_has_recursive(tree: &Tree, recursive_nets: &HashSet<String>) -> bool {
+  maybe_grow(|| {
+    if let Tree::Ref { nam } = tree {
+      recursive_nets.contains(nam)
+    } else {
+      for child in tree.children() {
+        if tree_has_recursive(child, recursive_nets) {
+          return true;
+        }
+      }
+      false
+    }
+  })
+}
+
+type DepGraph = HashMap<String, HashSet<String>>;
+type Cycles = Vec<Vec<String>>;
+
+/// Find all cycles in the dependency graph.
+pub fn cycles(deps: &DepGraph) -> Cycles {
+  let mut cycles = vec![];
+  let mut stack = vec![];
+  let mut visited = HashSet::new();
+  for nam in deps.keys() {
+    if !visited.contains(nam) {
+      find_cycles(deps, nam, &mut visited, &mut stack, &mut cycles);
+    }
+  }
+  cycles
+}
+
+fn find_cycles(
+  deps: &DepGraph,
+  nam: &String,
+  visited: &mut HashSet<String>,
+  stack: &mut Vec<String>,
+  cycles: &mut Cycles,
+) {
+  maybe_grow(|| {
+    // Check if the current ref is already in the stack, which indicates a cycle.
+    if let Some(cycle_start) = stack.iter().position(|n| n == nam) {
+      // If found, add the cycle to the cycles vector.
+      cycles.push(stack[cycle_start ..].to_vec());
+      return;
+    }
+    // If the ref has not been visited yet, mark it as visited.
+    if visited.insert(nam.clone()) {
+      // Add the current ref to the stack to keep track of the path.
+      stack.push(nam.clone());
+      // Get the dependencies of the current ref.
+      if let Some(dependencies) = deps.get(nam) {
+        // Search for cycles from each dependency.
+        for dep in dependencies {
+          find_cycles(deps, dep, visited, stack, cycles);
+        }
+      }
+      stack.pop();
+    }
+  })
+}
+
+/// Gather the set of net that this net directly depends on (has a ref in the net).
+fn dependencies(net: &Net) -> HashSet<String> {
+  let mut deps = HashSet::new();
+  dependencies_tree(&net.root, &mut deps);
+  for (a, b) in &net.redexes {
+    dependencies_tree(a, &mut deps);
+    dependencies_tree(b, &mut deps);
+  }
+  deps
+}
+
+fn dependencies_tree(tree: &Tree, deps: &mut HashSet<String>) {
+  if let Tree::Ref { nam } = tree {
+    deps.insert(nam.clone());
+  } else {
+    for subtree in tree.children() {
+      dependencies_tree(subtree, deps);
+    }
+  }
+}

src/lib.rs

@@ -6,6 +6,7 @@ use hvmc::ast::Net;
 use hvmc_net::{
   check_net_size::{check_net_sizes, MAX_NET_SIZE},
   mutual_recursion,
+  reorder_redexes::reorder_redexes_recursive_last,
 };
 use net::hvmc_to_net::hvmc_to_net;
 use std::{process::Output, str::FromStr};
@@ -38,6 +39,7 @@ pub fn compile_book(
   args: Option<Vec<Term>>,
 ) -> Result<CompileResult, Diagnostics> {
   let mut diagnostics = desugar_book(book, opts.clone(), diagnostics_cfg, args)?;
+
   let (mut core_book, labels) = book_to_nets(book, &mut diagnostics)?;
 
   if opts.eta {
@@ -45,7 +47,6 @@ pub fn compile_book(
   }
 
   mutual_recursion::check_cycles(&core_book, &mut diagnostics)?;
-
   if opts.eta {
     core_book.values_mut().for_each(Net::eta_reduce);
   }
@@ -65,6 +66,10 @@ pub fn compile_book(
 
   check_net_sizes(&core_book, &mut diagnostics)?;
 
+  if opts.recursive_last {
+    reorder_redexes_recursive_last(&mut core_book);
+  }
+
   Ok(CompileResult { core_book, labels, diagnostics })
 }
 
@@ -103,8 +108,8 @@ pub fn desugar_book(
   // Auto match linearization
   match opts.linearize_matches {
     OptLevel::Disabled => (),
-    OptLevel::Enabled => ctx.book.linearize_match_binds(),
+    OptLevel::Alt => ctx.book.linearize_match_binds(),
-    OptLevel::Extra => ctx.book.linearize_matches(),
+    OptLevel::Enabled => ctx.book.linearize_matches(),
   }
   // Manual match linearization
   ctx.book.linearize_match_with();
@@ -175,7 +180,7 @@ pub fn run_book(
     return Err(format!("Error reading result from hvm. Output :\n{}{}{}", err, status, out).into());
   };
 
-  let (term, diags) = readback_hvm_net(&net, &book, &labels, run_opts.linear);
+  let (term, diags) = readback_hvm_net(&net, &book, &labels, run_opts.linear_readback);
   Ok((term, stats.to_string(), diags))
 }
 
@@ -189,23 +194,16 @@ pub fn readback_hvm_net(net: &Net, book: &Book, labels: &Labels, linear: bool) -
 
 #[derive(Clone, Copy, Debug, Default)]
 pub struct RunOpts {
-  pub linear: bool,
+  pub linear_readback: bool,
-  pub lazy_mode: bool,
   pub pretty: bool,
 }
 
-impl RunOpts {
-  pub fn lazy() -> Self {
-    Self { lazy_mode: true, ..Self::default() }
-  }
-}
-
 #[derive(Clone, Copy, Debug, Default)]
 pub enum OptLevel {
-  #[default]
   Disabled,
+  #[default]
   Enabled,
-  Extra,
+  Alt,
 }
 
 impl OptLevel {
@@ -214,7 +212,7 @@ impl OptLevel {
   }
 
   pub fn is_extra(&self) -> bool {
-    matches!(self, OptLevel::Extra)
+    matches!(self, OptLevel::Enabled)
   }
 }
 
@@ -237,6 +235,9 @@ pub struct CompileOpts {
 
   /// Enables [term::transform::inline].
   pub inline: bool,
+
+  /// Enables [hvmc_net::reorder_redexes::reorder_redexes_recursive_last].
+  pub recursive_last: bool,
 }
 
 impl CompileOpts {
@@ -249,24 +250,23 @@ impl CompileOpts {
       float_combinators: true,
       merge: true,
       inline: true,
-      linearize_matches: OptLevel::Extra,
+      recursive_last: true,
+      linearize_matches: OptLevel::Enabled,
     }
   }
 
   /// Set all opts as false and keep the current adt encoding.
   #[must_use]
   pub fn set_no_all(self) -> Self {
-    Self::default()
+    Self {
-  }
+      eta: false,
-
+      prune: false,
-  /// All optimizations disabled, except float_combinators and linearize_matches
+      linearize_matches: OptLevel::Disabled,
-  pub fn default_strict() -> Self {
+      float_combinators: false,
-    Self { float_combinators: true, linearize_matches: OptLevel::Extra, eta: true, ..Self::default() }
+      merge: false,
-  }
+      inline: false,
-
+      recursive_last: false,
-  // Disable optimizations that don't work or are unnecessary on lazy mode
+    }
-  pub fn default_lazy() -> Self {
-    Self::default()
   }
 
   pub fn check_for_strict(&self) {
@@ -284,14 +284,16 @@ impl CompileOpts {
 }
 
 impl Default for CompileOpts {
+  /// Enables eta, linearize_matches, float_combinators and reorder_redexes_recursive_last.
   fn default() -> Self {
     Self {
-      eta: false,
+      eta: true,
       prune: false,
       linearize_matches: OptLevel::Enabled,
-      float_combinators: false,
+      float_combinators: true,
       merge: false,
       inline: false,
+      recursive_last: true,
     }
   }
 }

src/main.rs

@@ -34,9 +34,6 @@ enum Mode {
     )]
     comp_opts: Vec<OptArgs>,
 
-    #[arg(short = 'L', help = "Lazy mode")]
-    lazy_mode: bool,
-
     #[command(flatten)]
     warn_opts: CliWarnOpts,
 
@@ -54,9 +51,6 @@ enum Mode {
     )]
     comp_opts: Vec<OptArgs>,
 
-    #[arg(short = 'L', help = "Lazy mode")]
-    lazy_mode: bool,
-
     #[command(flatten)]
     warn_opts: CliWarnOpts,
 
@@ -65,9 +59,6 @@ enum Mode {
   },
   /// Compiles the program and runs it with the hvm.
   Run {
-    #[arg(short = 'L', help = "Lazy mode")]
-    lazy_mode: bool,
-
     #[arg(short = 'p', help = "Debug and normalization pretty printing")]
     pretty: bool,
 
@@ -106,9 +97,6 @@ enum Mode {
     #[arg(short = 'p', help = "Debug and normalization pretty printing")]
     pretty: bool,
 
-    #[arg(short = 'L', help = "Lazy mode")]
-    lazy_mode: bool,
-
     #[command(flatten)]
     warn_opts: CliWarnOpts,
 
@@ -166,7 +154,7 @@ pub enum OptArgs {
   Prune,
   NoPrune,
   LinearizeMatches,
-  LinearizeMatchesExtra,
+  LinearizeMatchesAlt,
   NoLinearizeMatches,
   FloatCombinators,
   NoFloatCombinators,
@@ -174,11 +162,13 @@ pub enum OptArgs {
   NoMerge,
   Inline,
   NoInline,
+  RecursiveLast,
+  NoRecursiveLast,
 }
 
-fn compile_opts_from_cli(args: &Vec<OptArgs>, lazy_mode: bool) -> CompileOpts {
+fn compile_opts_from_cli(args: &Vec<OptArgs>) -> CompileOpts {
   use OptArgs::*;
-  let mut opts = if lazy_mode { CompileOpts::default_lazy() } else { CompileOpts::default_strict() };
+  let mut opts = CompileOpts::default();
 
   for arg in args {
     match arg {
@@ -194,9 +184,11 @@ fn compile_opts_from_cli(args: &Vec<OptArgs>, lazy_mode: bool) -> CompileOpts {
       NoMerge => opts.merge = false,
       Inline => opts.inline = true,
       NoInline => opts.inline = false,
+      RecursiveLast => opts.recursive_last = true,
+      NoRecursiveLast => opts.recursive_last = false,
 
       LinearizeMatches => opts.linearize_matches = OptLevel::Enabled,
-      LinearizeMatchesExtra => opts.linearize_matches = OptLevel::Extra,
+      LinearizeMatchesAlt => opts.linearize_matches = OptLevel::Alt,
       NoLinearizeMatches => opts.linearize_matches = OptLevel::Disabled,
     }
   }
@@ -242,26 +234,18 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
   };
 
   match cli.mode {
-    Mode::Check { comp_opts, lazy_mode, warn_opts, path } => {
+    Mode::Check { comp_opts, warn_opts, path } => {
-      let diagnostics_cfg = set_warning_cfg_from_cli(
+      let diagnostics_cfg = set_warning_cfg_from_cli(DiagnosticsConfig::default(), warn_opts);
-        if lazy_mode { DiagnosticsConfig::default_lazy() } else { DiagnosticsConfig::default_strict() },
+      let compile_opts = compile_opts_from_cli(&comp_opts);
-        lazy_mode,
-        warn_opts,
-      );
-      let compile_opts = compile_opts_from_cli(&comp_opts, lazy_mode);
 
       let mut book = load_book(&path)?;
       let diagnostics = check_book(&mut book, diagnostics_cfg, compile_opts)?;
       eprintln!("{}", diagnostics);
     }
 
-    Mode::Compile { path, comp_opts, warn_opts, lazy_mode } => {
+    Mode::Compile { path, comp_opts, warn_opts } => {
-      let diagnostics_cfg = set_warning_cfg_from_cli(
+      let diagnostics_cfg = set_warning_cfg_from_cli(DiagnosticsConfig::default(), warn_opts);
-        if lazy_mode { DiagnosticsConfig::default_lazy() } else { DiagnosticsConfig::default_strict() },
+      let opts = compile_opts_from_cli(&comp_opts);
-        lazy_mode,
-        warn_opts,
-      );
-      let opts = compile_opts_from_cli(&comp_opts, lazy_mode);
 
       let mut book = load_book(&path)?;
       let compile_res = compile_book(&mut book, opts, diagnostics_cfg, None)?;
@@ -270,14 +254,10 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
       println!("{}", compile_res.core_book);
     }
 
-    Mode::Desugar { path, comp_opts, warn_opts, pretty, lazy_mode } => {
+    Mode::Desugar { path, comp_opts, warn_opts, pretty } => {
-      let diagnostics_cfg = set_warning_cfg_from_cli(
+      let diagnostics_cfg = set_warning_cfg_from_cli(DiagnosticsConfig::default(), warn_opts);
-        if lazy_mode { DiagnosticsConfig::default_lazy() } else { DiagnosticsConfig::default_strict() },
-        lazy_mode,
-        warn_opts,
-      );
 
-      let opts = compile_opts_from_cli(&comp_opts, lazy_mode);
+      let opts = compile_opts_from_cli(&comp_opts);
 
       let mut book = load_book(&path)?;
       let diagnostics = desugar_book(&mut book, opts, diagnostics_cfg, None)?;
@@ -290,17 +270,17 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
       }
     }
 
-    Mode::Run { lazy_mode, run_opts, pretty, comp_opts, warn_opts, arguments, path } => {
+    Mode::Run { run_opts, pretty, comp_opts, warn_opts, arguments, path } => {
       let RunArgs { linear, print_stats } = run_opts;
 
       let diagnostics_cfg =
-        set_warning_cfg_from_cli(DiagnosticsConfig::new(Severity::Allow, arg_verbose), lazy_mode, warn_opts);
+        set_warning_cfg_from_cli(DiagnosticsConfig::new(Severity::Allow, arg_verbose), warn_opts);
 
-      let compile_opts = compile_opts_from_cli(&comp_opts, lazy_mode);
+      let compile_opts = compile_opts_from_cli(&comp_opts);
 
       compile_opts.check_for_strict();
 
-      let run_opts = RunOpts { linear, lazy_mode, pretty };
+      let run_opts = RunOpts { linear_readback: linear, pretty };
 
       let book = load_book(&path)?;
       let (term, stats, diags) = run_book(book, run_opts, compile_opts, diagnostics_cfg, arguments)?;
@@ -319,12 +299,8 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
   Ok(())
 }
 
-fn set_warning_cfg_from_cli(
+fn set_warning_cfg_from_cli(mut cfg: DiagnosticsConfig, warn_opts: CliWarnOpts) -> DiagnosticsConfig {
-  mut cfg: DiagnosticsConfig,
+  fn set(cfg: &mut DiagnosticsConfig, severity: Severity, cli_val: WarningArgs) {
-  lazy_mode: bool,
-  warn_opts: CliWarnOpts,
-) -> DiagnosticsConfig {
-  fn set(cfg: &mut DiagnosticsConfig, severity: Severity, cli_val: WarningArgs, lazy_mode: bool) {
     match cli_val {
       WarningArgs::All => {
         cfg.irrefutable_match = severity;
@@ -332,9 +308,7 @@ fn set_warning_cfg_from_cli(
         cfg.unreachable_match = severity;
         cfg.unused_definition = severity;
         cfg.repeated_bind = severity;
-        if !lazy_mode {
+        cfg.recursion_cycle = severity;
-          cfg.recursion_cycle = severity;
-        }
       }
       WarningArgs::IrrefutableMatch => cfg.irrefutable_match = severity,
       WarningArgs::RedundantMatch => cfg.redundant_match = severity,
@@ -356,9 +330,9 @@ fn set_warning_cfg_from_cli(
     let mut denies = warn_opts.denies.into_iter();
     for id in warn_opts_ids {
       match id.as_ref() {
-        "allows" => set(&mut cfg, Severity::Allow, allows.next().unwrap(), lazy_mode),
+        "allows" => set(&mut cfg, Severity::Allow, allows.next().unwrap()),
-        "denies" => set(&mut cfg, Severity::Error, denies.next().unwrap(), lazy_mode),
+        "denies" => set(&mut cfg, Severity::Error, denies.next().unwrap()),
-        "warns" => set(&mut cfg, Severity::Warning, warns.next().unwrap(), lazy_mode),
+        "warns" => set(&mut cfg, Severity::Warning, warns.next().unwrap()),
         _ => unreachable!(),
       }
     }

src/term/term_to_net.rs

@@ -17,8 +17,8 @@ use super::{num_to_name, FanKind, Op};
 #[derive(Debug, Clone)]
 pub struct ViciousCycleErr;
 
-pub fn book_to_nets(book: &Book, info: &mut Diagnostics) -> Result<(hvmc::ast::Book, Labels), Diagnostics> {
+pub fn book_to_nets(book: &Book, diags: &mut Diagnostics) -> Result<(hvmc::ast::Book, Labels), Diagnostics> {
-  info.start_pass();
+  diags.start_pass();
 
   let mut hvmc = hvmc::ast::Book::default();
   let mut labels = Labels::default();
@@ -31,8 +31,11 @@ pub fn book_to_nets(book: &Book, info: &mut Diagnostics) -> Result<(hvmc::ast::B
 
       let name = if def.name == *main { book.hvmc_entrypoint().to_string() } else { def.name.0.to_string() };
 
-      if let Some(net) = info.take_inet_err(net, name.clone()) {
+      match net {
-        hvmc.insert(name, net);
+        Ok(net) => {
+          hvmc.insert(name, net);
+        }
+        Err(err) => diags.add_inet_error(err, name),
       }
     }
   }
@@ -40,7 +43,7 @@ pub fn book_to_nets(book: &Book, info: &mut Diagnostics) -> Result<(hvmc::ast::B
   labels.con.finish();
   labels.dup.finish();
 
-  Ok((hvmc, labels))
+  diags.fatal((hvmc, labels))
 }
 
 /// Converts an LC term into an IC net.

tests/golden_tests.rs

@@ -117,9 +117,8 @@ fn compile_term() {
 fn compile_file() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let mut book = do_parse_book(code, path)?;
-    let compile_opts = CompileOpts::default_strict();
+    let compile_opts = CompileOpts::default();
-    let mut diagnostics_cfg = DiagnosticsConfig::default_strict();
+    let diagnostics_cfg = DiagnosticsConfig { unused_definition: Severity::Allow, ..Default::default() };
-    diagnostics_cfg.unused_definition = Severity::Allow;
 
     let res = compile_book(&mut book, compile_opts, diagnostics_cfg, None)?;
     Ok(format!("{}{}", res.diagnostics, res.core_book))
@@ -130,10 +129,12 @@ fn compile_file() {
 fn compile_file_o_all() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let mut book = do_parse_book(code, path)?;
-    let opts = CompileOpts::default_strict().set_all();
+    let opts = CompileOpts::default().set_all();
-    let mut diagnostics_cfg = DiagnosticsConfig::default_strict();
+    let diagnostics_cfg = DiagnosticsConfig {
-    diagnostics_cfg.recursion_cycle = Severity::Warning;
+      recursion_cycle: Severity::Warning,
-    diagnostics_cfg.unused_definition = Severity::Allow;
+      unused_definition: Severity::Allow,
+      ..Default::default()
+    };
 
     let res = compile_book(&mut book, opts, diagnostics_cfg, None)?;
     Ok(format!("{}{}", res.diagnostics, res.core_book))
@@ -144,8 +145,8 @@ fn compile_file_o_all() {
 fn compile_file_o_no_all() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let mut book = do_parse_book(code, path)?;
-    let compile_opts = CompileOpts::default_strict().set_no_all();
+    let compile_opts = CompileOpts::default().set_no_all();
-    let diagnostics_cfg = DiagnosticsConfig::default_strict();
+    let diagnostics_cfg = DiagnosticsConfig::default();
     let res = compile_book(&mut book, compile_opts, diagnostics_cfg, None)?;
     Ok(format!("{}", res.core_book))
   })
@@ -154,11 +155,17 @@ fn compile_file_o_no_all() {
 #[test]
 fn linear_readback() {
   run_golden_test_dir(function_name!(), &|code, path| {
+    let _guard = RUN_MUTEX.lock().unwrap();
     let book = do_parse_book(code, path)?;
-    let compile_opts = CompileOpts::default_strict().set_all();
+    let compile_opts = CompileOpts::default().set_all();
-    let diagnostics_cfg = DiagnosticsConfig::default_strict();
+    let diagnostics_cfg = DiagnosticsConfig::default();
-    let (term, _, diags) =
+    let (term, _, diags) = run_book(
-      run_book(book, RunOpts { linear: true, ..Default::default() }, compile_opts, diagnostics_cfg, None)?;
+      book,
+      RunOpts { linear_readback: true, ..Default::default() },
+      compile_opts,
+      diagnostics_cfg,
+      None,
+    )?;
     let res = format!("{diags}{term}");
     Ok(res)
   });
@@ -169,7 +176,7 @@ fn run_file() {
   run_golden_test_dir_multiple(function_name!(), &[(&|code, path| {
     let _guard = RUN_MUTEX.lock().unwrap();
     let book = do_parse_book(code, path)?;
-    let compile_opts = CompileOpts::default_strict();
+    let compile_opts = CompileOpts::default();
     let diagnostics_cfg = DiagnosticsConfig {
       unused_definition: Severity::Allow,
       ..DiagnosticsConfig::new(Severity::Error, true)
@@ -185,8 +192,9 @@ fn run_file() {
 #[test]
 #[ignore = "while lazy execution is not implemented for hvm32"]
 fn run_lazy() {
-  run_golden_test_dir(function_name!(), &|code, path| {
+  run_golden_test_dir(function_name!(), &|_code, _path| {
-    let _guard = RUN_MUTEX.lock().unwrap();
+    todo!()
+    /* let _guard = RUN_MUTEX.lock().unwrap();
     let book = do_parse_book(code, path)?;
     let compile_opts = CompileOpts::default_lazy();
     let diagnostics_cfg = DiagnosticsConfig {
@@ -198,7 +206,7 @@ fn run_lazy() {
 
     let (term, _, diags) = run_book(book, run_opts, compile_opts, diagnostics_cfg, None)?;
     let res = format!("{diags}{term}");
-    Ok(res)
+    Ok(res) */
   })
 }
 
@@ -255,7 +263,7 @@ fn parse_file() {
 fn encode_pattern_match() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let mut result = String::new();
-    let diagnostics_cfg = DiagnosticsConfig::default_strict();
+    let diagnostics_cfg = DiagnosticsConfig::default();
     let mut book = do_parse_book(code, path)?;
     let mut ctx = Ctx::new(&mut book, diagnostics_cfg);
     ctx.check_shared_names();
@@ -286,7 +294,7 @@ fn encode_pattern_match() {
 #[test]
 fn desugar_file() {
   run_golden_test_dir(function_name!(), &|code, path| {
-    let compile_opts = CompileOpts::default_strict();
+    let compile_opts = CompileOpts::default();
     let diagnostics_cfg = DiagnosticsConfig {
       unused_definition: Severity::Allow,
       ..DiagnosticsConfig::new(Severity::Error, true)
@@ -305,7 +313,7 @@ fn hangs() {
   run_golden_test_dir(function_name!(), &move |code, path| {
     let _guard = RUN_MUTEX.lock().unwrap();
     let book = do_parse_book(code, path)?;
-    let compile_opts = CompileOpts::default_strict().set_all();
+    let compile_opts = CompileOpts::default().set_all();
     let diagnostics_cfg = DiagnosticsConfig::new(Severity::Allow, false);
 
     let thread =
@@ -328,7 +336,7 @@ fn compile_entrypoint() {
     let mut book = do_parse_book(code, path)?;
     book.entrypoint = Some(Name::new("foo"));
     let diagnostics_cfg = DiagnosticsConfig { ..DiagnosticsConfig::new(Severity::Error, true) };
-    let res = compile_book(&mut book, CompileOpts::default_strict(), diagnostics_cfg, None)?;
+    let res = compile_book(&mut book, CompileOpts::default(), diagnostics_cfg, None)?;
     Ok(format!("{}{}", res.diagnostics, res.core_book))
   })
 }
@@ -340,7 +348,7 @@ fn run_entrypoint() {
     let _guard = RUN_MUTEX.lock().unwrap();
     let mut book = do_parse_book(code, path)?;
     book.entrypoint = Some(Name::new("foo"));
-    let compile_opts = CompileOpts::default_strict().set_all();
+    let compile_opts = CompileOpts::default().set_all();
     let diagnostics_cfg = DiagnosticsConfig { ..DiagnosticsConfig::new(Severity::Error, true) };
     let (term, _, diags) = run_book(book, RunOpts::default(), compile_opts, diagnostics_cfg, None)?;
     let res = format!("{diags}{term}");
@@ -374,8 +382,7 @@ fn mutual_recursion() {
     let diagnostics_cfg =
       DiagnosticsConfig { recursion_cycle: Severity::Error, ..DiagnosticsConfig::new(Severity::Allow, true) };
     let mut book = do_parse_book(code, path)?;
-    let mut opts = CompileOpts::default_strict();
+    let opts = CompileOpts { merge: true, ..CompileOpts::default() };
-    opts.merge = true;
     let res = compile_book(&mut book, opts, diagnostics_cfg, None)?;
     Ok(format!("{}{}", res.diagnostics, res.core_book))
   })
@@ -400,8 +407,8 @@ fn io() {
     (&|code, path| {
       let _guard = RUN_MUTEX.lock().unwrap();
       let book = do_parse_book(code, path)?;
-      let compile_opts = CompileOpts::default_strict();
+      let compile_opts = CompileOpts::default();
-      let diagnostics_cfg = DiagnosticsConfig::default_strict();
+      let diagnostics_cfg = DiagnosticsConfig::default();
       let (term, _, diags) = run_book(book, RunOpts::default(), compile_opts, diagnostics_cfg, None)?;
       let res = format!("{diags}{term}");
       Ok(format!("Strict mode:\n{res}"))
@@ -410,7 +417,6 @@ fn io() {
 }
 
 #[test]
-//#[ignore = "while execution is not implemented for hvm32"]
 fn examples() -> Result<(), Diagnostics> {
   let examples_path = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("examples");
 
@@ -426,8 +432,8 @@ fn examples() -> Result<(), Diagnostics> {
     let code = std::fs::read_to_string(path).map_err(|e| e.to_string())?;
 
     let book = do_parse_book(&code, path).unwrap();
-    let compile_opts = CompileOpts::default_strict();
+    let compile_opts = CompileOpts::default();
-    let diagnostics_cfg = DiagnosticsConfig::default_strict();
+    let diagnostics_cfg = DiagnosticsConfig::default();
     let (term, _, diags) = run_book(book, RunOpts::default(), compile_opts, diagnostics_cfg, None)?;
     let res = format!("{diags}{term}");
 
@@ -448,9 +454,9 @@ fn examples() -> Result<(), Diagnostics> {
 fn scott_triggers_unused() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let mut book = do_parse_book(code, path)?;
-    let opts = CompileOpts::default_strict();
+    let opts = CompileOpts::default();
     let diagnostics_cfg =
-      DiagnosticsConfig { unused_definition: Severity::Error, ..DiagnosticsConfig::default_strict() };
+      DiagnosticsConfig { unused_definition: Severity::Error, ..DiagnosticsConfig::default() };
     let res = compile_book(&mut book, opts, diagnostics_cfg, None)?;
     Ok(format!("{}{}", res.diagnostics, res.core_book))
   })

tests/golden_tests/cli/desugar_linearize_matches.hvm

@@ -1 +1 @@
-main = λa λb switch a { 0: b; _: b }
+main = λa λb λc switch a { 0: b; _: c }

tests/golden_tests/cli/desugar_linearize_matches_alt.args

@@ -0,0 +1,3 @@
+desugar
+tests/golden_tests/cli/desugar_linearize_matches_alt.hvm
+-Olinearize-matches-alt

tests/golden_tests/cli/desugar_linearize_matches_alt.hvm

@@ -0,0 +1 @@
+main = λa λb switch a { 0: b; _: b }

tests/golden_tests/cli/desugar_linearize_matches_extra.args

@@ -1,3 +0,0 @@
-desugar
-tests/golden_tests/cli/desugar_linearize_matches_extra.hvm
--Olinearize-matches-extra

tests/golden_tests/cli/desugar_linearize_matches_extra.hvm

@@ -1 +0,0 @@
-main = λa λb λc switch a { 0: b; _: c }

tests/golden_tests/compile_file/redex_order_recursive.hvm

@@ -1,4 +1,4 @@
-tail_recursive = @a (a @x (+ 1 (tail_recursive x)) 0)
+tail_recursive = @x (x @pred @acc (tail_recursive pred (+ 1 acc)) @acc 0)
 
 fold = @bm (bm
   @lft @rgt (add (fold lft) (fold rgt))

tests/snapshots/cli__compile_no_opts.hvm.snap

@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/cli/compile_no_opts.hvm
 ---
 error: invalid value 'no-pre-reduce' for '-O <COMP_OPTS>'
-  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-extra, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline]
+  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-alt, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline, recursive-last, no-recursive-last]
 
   tip: a similar value exists: 'no-prune'
 

tests/snapshots/cli__compile_pre_reduce.hvm.snap

@@ -3,6 +3,6 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/cli/compile_pre_reduce.hvm
 ---
 error: invalid value 'pre-reduce' for '-O <COMP_OPTS>'
-  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-extra, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline]
+  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-alt, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline, recursive-last, no-recursive-last]
 
 For more information, try '--help'.

tests/snapshots/cli__compile_wrong_opt.hvm.snap

@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/cli/compile_wrong_opt.hvm
 ---
 error: invalid value 'foo' for '-O <COMP_OPTS>'
-  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-extra, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline]
+  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-alt, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline, recursive-last, no-recursive-last]
 
   tip: a similar value exists: 'float-combinators'
 

tests/snapshots/cli__desugar_bool_scott.hvm.snap

@@ -3,6 +3,6 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/cli/desugar_bool_scott.hvm
 ---
 error: invalid value 'adt-scott' for '-O <COMP_OPTS>'
-  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-extra, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline]
+  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-alt, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline, recursive-last, no-recursive-last]
 
 For more information, try '--help'.

tests/snapshots/cli__desugar_bool_tagged.hvm.snap

@@ -3,6 +3,6 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/cli/desugar_bool_tagged.hvm
 ---
 error: invalid value 'adt-tagged-scott' for '-O <COMP_OPTS>'
-  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-extra, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline]
+  [possible values: all, no-all, eta, no-eta, prune, no-prune, linearize-matches, linearize-matches-alt, no-linearize-matches, float-combinators, no-float-combinators, merge, no-merge, inline, no-inline, recursive-last, no-recursive-last]
 
 For more information, try '--help'.

tests/snapshots/cli__desugar_linearize_matches.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/cli/desugar_linearize_matches.hvm
 ---
-(main) = λa switch a { 0: λb b; _: λ* λc c; }
+(main) = λa λb λc (switch a { 0: λd λ* d; _: λ* λ* λe e; } b c)

tests/snapshots/cli__desugar_linearize_matches_alt.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/cli/desugar_linearize_matches_alt.hvm
+---
+(main) = λa switch a { 0: λb b; _: λ* λc c; }

tests/snapshots/compile_file__redex_order_recursive.hvm.snap

@@ -18,8 +18,8 @@ input_file: tests/golden_tests/compile_file/redex_order_recursive.hvm
 
 @main = *
 
-@tail_recursive = ((@tail_recursive__C0 (0 a)) a)
+@tail_recursive = ((@tail_recursive__C0 ((* 0) a)) a)
 
-@tail_recursive__C0 = (a c)
+@tail_recursive__C0 = (a (b d))
+  & @tail_recursive ~ (a (c d))
   & $(b c) ~ [+1]
-  & @tail_recursive ~ (a b)

tests/snapshots/compile_file__vicious_circles.hvm.snap

@@ -7,5 +7,3 @@ In compiled inet 'disconnected_self_lam':
   Found term that compiles into an inet with a vicious cycle
 In compiled inet 'dup_self':
   Found term that compiles into an inet with a vicious cycle
-
-@main = (@dup_self @disconnected_self_lam)

tests/snapshots/compile_file_o_all__ex2.hvm.snap

@@ -16,8 +16,8 @@ input_file: tests/golden_tests/compile_file_o_all/ex2.hvm
   & @low ~ a
 
 @decO = (a c)
-  & @I ~ (b c)
   & @dec ~ (a b)
+  & @I ~ (b c)
 
 @low = ((@lowO (@lowI (@E a))) a)
 

tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap

@@ -11,8 +11,8 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 @Map = ((@Map__C0 ((* @False__M_Nil) a)) a)
 
 @Map__C0 = (a (c ({(a b) d} f)))
-  & @Cons ~ (b (e f))
   & @Map ~ (c (d e))
+  & @Cons ~ (b (e f))
 
 @Merge = (b ((@Merge__C2 ((* (a a)) (b c))) c))
 
@@ -22,9 +22,9 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
   & @Cons ~ (a (@False__M_Nil b))
 
 @MergePair__C1 = (c (f ({a e} (b h))))
-  & @Cons ~ (d (g h))
   & @Merge ~ (a (b (c d)))
   & @MergePair ~ (e (f g))
+  & @Cons ~ (d (g h))
 
 @MergePair__C2 = (b ((@MergePair__C1 (@MergePair__C0 (a (b c)))) (a c)))
 
@@ -36,12 +36,12 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
   & @Cons ~ a
 
 @Merge__C1 = ({b {g l}} ({h q} ({(a (b c)) {e m}} ({a {d n}} ({f o} t)))))
+  & @Merge ~ (e (f (i j)))
+  & @Merge ~ (m (p (q r)))
   & @If ~ (c (k (s t)))
   & @Cons ~ (d (j k))
-  & @Merge ~ (e (f (i j)))
   & @Cons ~ (g (h i))
   & @Cons ~ (l (r s))
-  & @Merge ~ (m (p (q r)))
   & @Cons ~ (n (o p))
 
 @Merge__C2 = (b (c (a ((@Merge__C1 (@Merge__C0 (a (b (c d))))) d))))

tests/snapshots/compile_file_o_all__list_reverse.hvm.snap

@@ -5,8 +5,8 @@ input_file: tests/golden_tests/compile_file_o_all/list_reverse.hvm
 @concat = ((@concat__C0 ((a a) b)) b)
 
 @concat__C0 = (a (b (c e)))
-  & @cons ~ (a (d e))
   & @concat ~ (b (c d))
+  & @cons ~ (a (d e))
 
 @cons = (a (b ((a (b c)) (* c))))
 

tests/snapshots/mutual_recursion__len.hvm.snap

@@ -5,8 +5,8 @@ input_file: tests/golden_tests/mutual_recursion/len.hvm
 @Len = ((@Len__C0 (0 a)) a)
 
 @Len__C0 = (* (a c))
-  & $(b c) ~ [+1]
   & @Len ~ (a b)
+  & $(b c) ~ [+1]
 
 @List.cons = (a (b ((a (b c)) (* c))))