[sc 455] improve match linearization pass

docs/compiler-options.md

@@ -8,7 +8,8 @@
 | `-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) |
+| `-Olinearize-matches` `-Olinearize-matches-extra` `-Ono-linearize-matches` | Extra  | [linearize-matches](#linearize-matches) |
+| `-Ofloat_combinators` `-Ono-float_combinators` | Enabled  | [float-combinators](#float-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 +135,30 @@ main = (bar)
 @main = @bar
 ```
 
-## Supercombinators
+## linearize-matches
+
+Linearizes the variables between match cases, transforming them into combinators when possible.  
+When the `linearize-matches` option is used, linearizes only vars that are used in more than one arm.
+
+Example:
+```rs
+λa λb match a { 0: b; +: b }
+
+// Is transformed to
+λa λb (match a { 0: λc c; +: λd d } b)
+```
+
+When the `linearize-matches-extra` option is used, linearizes all vars used in the arms.
+
+example:
+```rs
+λa λb λc match a { 0: b; +: c }
+
+// Is transformed to
+λa λb λc (match a { 0: λd λ* d; +: λ* λe e } b c)
+```
+
+## float-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.

docs/lazy-definitions.md

@@ -49,4 +49,4 @@ The lambda terms without free variables are extracted to new definitions.
 ToMachine0 = λp (+ 1 (ToMachine p))
 ToMachine = λn (n ToMachine0 0)
 ```
-Definitions are lazy in the runtime. Lifting lambda terms to new definitions will prevent infinite expansion.
+Definitions are lazy in the runtime. Floating lambda terms into new definitions will prevent infinite expansion.

src/lib.rs

@@ -83,7 +83,7 @@ pub fn create_host(book: Arc<Book>, labels: Arc<Labels>, compile_opts: CompileOp
         match term {
           Term::Str { val } => {
             println!("{}", val);
-          },
+          }
           _ => (),
         }
       }
@@ -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 opts.linearize_matches.enabled() {
+    ctx.linearize_simple_matches(opts.linearize_matches.is_extra())?;
+  }
+
   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.float_combinators {
+    ctx.book.float_combinators();
   }
   if opts.ref_to_ref {
     ctx.simplify_ref_to_ref()?;
@@ -331,6 +335,24 @@ impl RunOpts {
   }
 }
 
+#[derive(Clone, Copy, Debug, Default)]
+pub enum OptLevel {
+  #[default]
+  Disabled,
+  Enabled,
+  Extra,
+}
+
+impl OptLevel {
+  pub fn enabled(&self) -> bool {
+    !matches!(self, OptLevel::Disabled)
+  }
+
+  pub fn is_extra(&self) -> bool {
+    matches!(self, OptLevel::Extra)
+  }
+}
+
 #[derive(Clone, Copy, Debug, Default)]
 pub struct CompileOpts {
   /// Selects the encoding for the ADT syntax.
@@ -348,8 +370,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::float_combinators].
+  pub float_combinators: bool,
 
   /// Enables [term::transform::simplify_main_ref].
   pub simplify_main: bool,
@@ -369,11 +394,12 @@ impl CompileOpts {
       ref_to_ref: true,
       prune: true,
       pre_reduce: true,
-      supercombinators: true,
+      float_combinators: true,
       simplify_main: true,
       merge: true,
       inline: true,
       adt_encoding: Default::default(),
+      linearize_matches: OptLevel::Extra,
     }
   }
 
@@ -387,24 +413,34 @@ impl CompileOpts {
     Self { adt_encoding: self.adt_encoding, ..Self::default() }
   }
 
-  /// All optimizations disabled, except detach supercombinators.
+  /// All optimizations disabled, except float_combinators and linearize_matches
   pub fn light() -> Self {
-    Self { supercombinators: true, ..Self::default() }
+    Self { float_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.float_combinators = false;
+    if self.linearize_matches.is_extra() {
+      self.linearize_matches = OptLevel::Enabled;
+    }
     self.pre_reduce = false;
   }
 }
 
 impl CompileOpts {
   pub fn check(&self, lazy_mode: bool) {
-    if !self.supercombinators && !lazy_mode {
-      println!(
-        "Warning: Running in strict mode without enabling the supercombinators pass can lead to some functions expanding infinitely."
-      );
+    if !lazy_mode {
+      if !self.float_combinators {
+        println!(
+          "Warning: Running in strict mode without enabling the float_combinators pass can lead to some functions expanding infinitely."
+        );
+      }
+      if !self.linearize_matches.enabled() {
+        println!(
+          "Warning: Running in strict mode without enabling the linearize_matches 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."#,
+      float_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."#,
+      float_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."#,
+      float_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,
+  FloatCombinators,
+  NoFloatCombinators,
   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,
+        FloatCombinators => opts.float_combinators = true,
+        NoFloatCombinators => opts.float_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