Refactor lift_combinaotors to work with linearize_matches change

docs/compiler-options.md

@@ -8,7 +8,7 @@
 | `-Oref-to-ref` `-Ono-ref-to-ref` | Disabled | [ref-to-ref](#ref-to-ref) |
 | `-Oprune` `-Ono-prune` | Disabled | [definition-pruning](#definition-pruning) |
 | `-Opre-reduce` `-Ono-pre-reduce` | Disabled | [pre-reduce](#pre-reduce) |
-| `-Osupercombinators` `-Ono-supercombinators` | Enabled  | [supercombinators](#supercombinators) |
+| `-Olift_combinators` `-Ono-lift_combinators` | Enabled  | [lift-combinators](#lift-combinators) |
 | `-Osimplify-main` `-Ono-simplify-main` | Disabled | [simplify-main](#simplify-main) |
 | `-Omerge` `-Ono-merge` | Disabled | [definition-merging](#definition-merging) |
 | `-Oinline` `-Ono-inline` | Disabled | [inline](#inline) |
@@ -134,7 +134,7 @@ main = (bar)
 @main = @bar
 ```
 
-## Supercombinators
+## Lift-Combinators
 
 Extracts closed terms to new definitions. See [lazy definitions](lazy-definitions#automatic-optimization).
 Since HVM-Core is an eager runtime, this pass is enabled by default to prevent infinite expansions.

src/lib.rs

@@ -134,12 +134,16 @@ pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result<Vec<Warning>,
   ctx.book.desugar_implicit_match_binds();
 
   ctx.check_ctrs_arities()?;
-  // Must be between [`Book::desugar_implicit_match_binds`] and [`Ctx::linearize_simple_matches`]
+  // Must be between [`Book::desugar_implicit_match_binds`] and [`Ctx::linearize_matches`]
   ctx.check_unbound_vars()?;
 
   ctx.book.convert_match_def_to_term();
   ctx.simplify_matches()?;
-  ctx.linearize_simple_matches()?;
+
+  if !matches!(opts.linearize_matches, OptLevel::Disabled) {
+    ctx.linearize_matches()?;
+  }
+
   ctx.book.encode_simple_matches(opts.adt_encoding);
 
   // sanity check
@@ -155,8 +159,8 @@ pub fn desugar_book(book: &mut Book, opts: CompileOpts) -> Result<Vec<Warning>,
   if opts.eta {
     ctx.book.eta_reduction();
   }
-  if opts.supercombinators {
-    ctx.book.detach_supercombinators();
+  if opts.lift_combinators {
+    ctx.book.lift_combinators(matches!(opts.linearize_matches, OptLevel::Extra));
   }
   if opts.ref_to_ref {
     ctx.simplify_ref_to_ref()?;
@@ -331,6 +335,14 @@ impl RunOpts {
   }
 }
 
+#[derive(Clone, Copy, Debug, Default)]
+pub enum OptLevel {
+  #[default]
+  Disabled,
+  Enabled,
+  Extra,
+}
+
 #[derive(Clone, Copy, Debug, Default)]
 pub struct CompileOpts {
   /// Selects the encoding for the ADT syntax.
@@ -348,8 +360,11 @@ pub struct CompileOpts {
   /// Enables [hvmc_net::pre_reduce].
   pub pre_reduce: bool,
 
-  /// Enables [term::transform::detach_supercombinators].
-  pub supercombinators: bool,
+  /// Enables [term::transform::linearize_matches].
+  pub linearize_matches: OptLevel,
+
+  /// Enables [term::transform::lift_combinators].
+  pub lift_combinators: bool,
 
   /// Enables [term::transform::simplify_main_ref].
   pub simplify_main: bool,
@@ -369,11 +384,12 @@ impl CompileOpts {
       ref_to_ref: true,
       prune: true,
       pre_reduce: true,
-      supercombinators: true,
+      lift_combinators: true,
       simplify_main: true,
       merge: true,
       inline: true,
       adt_encoding: Default::default(),
+      linearize_matches: OptLevel::Extra,
     }
   }
 
@@ -387,23 +403,26 @@ impl CompileOpts {
     Self { adt_encoding: self.adt_encoding, ..Self::default() }
   }
 
-  /// All optimizations disabled, except detach supercombinators.
+  /// All optimizations disabled, except lift_combinators and linearize_matches
   pub fn light() -> Self {
-    Self { supercombinators: true, ..Self::default() }
+    Self { lift_combinators: true, linearize_matches: OptLevel::Extra, ..Self::default() }
   }
 
   // Disable optimizations that don't work or are unnecessary on lazy mode
   pub fn lazy_mode(&mut self) {
-    self.supercombinators = false;
+    self.lift_combinators = false;
+    if let OptLevel::Extra = self.linearize_matches {
+      self.linearize_matches = OptLevel::Enabled;
+    }
     self.pre_reduce = false;
   }
 }
 
 impl CompileOpts {
   pub fn check(&self, lazy_mode: bool) {
-    if !self.supercombinators && !lazy_mode {
+    if !self.lift_combinators && !lazy_mode {
       println!(
-        "Warning: Running in strict mode without enabling the supercombinators pass can lead to some functions expanding infinitely."
+        "Warning: Running in strict mode without enabling the lift_combinators pass can lead to some functions expanding infinitely."
       );
     }
   }

src/main.rs

@@ -4,7 +4,7 @@ use hvml::{
   diagnostics::Info,
   load_file_to_book, run_book,
   term::{display::display_readback_errors, AdtEncoding, Book, Name},
-  CompileOpts, RunInfo, RunOpts, WarnState, WarningOpts,
+  CompileOpts, OptLevel, RunInfo, RunOpts, WarnState, WarningOpts,
 };
 use std::{
   path::{Path, PathBuf},
@@ -38,7 +38,7 @@ enum Mode {
       value_delimiter = ' ',
       action = clap::ArgAction::Append,
       long_help = r#"Enables or disables the given optimizations
-      supercombinators is enabled by default."#,
+      lift_combinators is enabled by default on strict mode."#,
     )]
     comp_opts: Vec<OptArgs>,
 
@@ -82,7 +82,7 @@ enum Mode {
       value_delimiter = ' ',
       action = clap::ArgAction::Append,
       long_help = r#"Enables or disables the given optimizations
-      supercombinators is enabled by default."#,
+      lift_combinators is enabled by default on strict mode."#,
     )]
     comp_opts: Vec<OptArgs>,
 
@@ -91,12 +91,15 @@ enum Mode {
   },
   /// Runs the lambda-term level desugaring passes.
   Desugar {
+    #[arg(short = 'L', help = "Lazy mode")]
+    lazy_mode: bool,
+
     #[arg(
       short = 'O',
       value_delimiter = ' ',
       action = clap::ArgAction::Append,
       long_help = r#"Enables or disables the given optimizations
-      supercombinators is enabled by default."#,
+      lift_combinators is enabled by default on strict mode."#,
     )]
     comp_opts: Vec<OptArgs>,
 
@@ -185,15 +188,18 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Info> {
       let mut opts = OptArgs::opts_from_cli(&comp_opts);
 
       if lazy_mode {
-        opts.lazy_mode()
+        opts.lazy_mode();
       }
 
       let mut book = load_book(&path)?;
       let compiled = compile_book(&mut book, opts)?;
       println!("{}", compiled.display_with_warns(warning_opts)?);
     }
-    Mode::Desugar { path, comp_opts } => {
-      let opts = OptArgs::opts_from_cli(&comp_opts);
+    Mode::Desugar { path, comp_opts, lazy_mode } => {
+      let mut opts = OptArgs::opts_from_cli(&comp_opts);
+      if lazy_mode {
+        opts.lazy_mode();
+      }
       let mut book = load_book(&path)?;
       // TODO: Shouldn't the desugar have `warn_opts` too? maybe WarningOpts::allow_all() by default
       let _warns = desugar_book(&mut book, opts)?;
@@ -221,7 +227,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Info> {
 
       if lazy_mode {
         single_core = true;
-        opts.lazy_mode()
+        opts.lazy_mode();
       }
 
       let book = load_book(&path)?;
@@ -288,8 +294,11 @@ pub enum OptArgs {
   NoRefToRef,
   PreReduce,
   NoPreReduce,
-  Supercombinators,
-  NoSupercombinators,
+  LinearizeMatches,
+  LinearizeMatchesExtra,
+  NoLinearizeMatches,
+  LiftCombinators,
+  NoLiftCombinators,
   SimplifyMain,
   NoSimplifyMain,
   Merge,
@@ -316,16 +325,21 @@ impl OptArgs {
         NoRefToRef => opts.ref_to_ref = false,
         PreReduce => opts.pre_reduce = true,
         NoPreReduce => opts.pre_reduce = false,
-        Supercombinators => opts.supercombinators = true,
-        NoSupercombinators => opts.supercombinators = false,
+        LiftCombinators => opts.lift_combinators = true,
+        NoLiftCombinators => opts.lift_combinators = false,
         SimplifyMain => opts.simplify_main = true,
         NoSimplifyMain => opts.simplify_main = false,
         Merge => opts.merge = true,
         NoMerge => opts.merge = false,
         Inline => opts.inline = true,
         NoInline => opts.inline = false,
+
         AdtScott => opts.adt_encoding = AdtEncoding::Scott,
         AdtTaggedScott => opts.adt_encoding = AdtEncoding::TaggedScott,
+
+        LinearizeMatches => opts.linearize_matches = OptLevel::Enabled,
+        LinearizeMatchesExtra => opts.linearize_matches = OptLevel::Extra,
+        NoLinearizeMatches => opts.linearize_matches = OptLevel::Disabled,
       }
     }
     opts