Improve lazy mode diagnostics and usability with the rebase

And update tests

Cargo.lock

@@ -211,7 +211,7 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
 [[package]]
 name = "hvm-core"
 version = "0.2.14"
-source = "git+https://github.com/HigherOrderCO/hvm-core?branch=lazy_mode#2bf5893b9deed6c804f353da28edac0b461ea572"
+source = "git+https://github.com/HigherOrderCO/hvm-core?branch=lazy_mode#b8b24fb7c02b8348e9c83501557730a167bcc2cc"
 dependencies = [
  "nohash-hasher",
 ]

src/lib.rs

@@ -34,7 +34,7 @@ pub fn compile_book(book: &mut Book, opts: Opts) -> Result<CompileResult, String
   let (main, warnings) = desugar_book(book, opts)?;
   let (nets, hvmc_names, labels) = book_to_nets(book, main);
   let mut core_book = nets_to_hvmc(nets, &hvmc_names)?;
-  if opts.pre_reduce && !opts.lazy {
+  if opts.pre_reduce {
     pre_reduce_book(&mut core_book, opts.pre_reduce)?;
   }
   if opts.prune {
@@ -98,6 +98,7 @@ pub fn run_book(
   parallel: bool,
   debug: bool,
   linear: bool,
+  lazy: bool,
   warning_opts: WarningOpts,
   opts: Opts,
 ) -> Result<(Term, DefNames, RunInfo), String> {
@@ -117,7 +118,7 @@ pub fn run_book(
   let debug_hook =
     if debug { Some(|net: &_| debug_hook(net, &book, &hvmc_names, &labels, linear)) } else { None };
 
-  let (res_lnet, stats) = run_compiled(&core_book, mem_size, parallel, opts.lazy, debug_hook);
+  let (res_lnet, stats) = run_compiled(&core_book, mem_size, parallel, lazy, debug_hook);
   let net = hvmc_to_net(&res_lnet, &|id| hvmc_names.hvmc_name_to_id[&id]);
   let (res_term, readback_errors) = net_to_term(&net, &book, &labels, linear);
   let info = RunInfo { stats, readback_errors, net: res_lnet };
@@ -186,8 +187,6 @@ pub struct Opts {
 
   /// Enables [term::transform::definition_merge]
   pub merge_definitions: bool,
-
-  pub lazy: bool
 }
 
 impl Opts {
@@ -202,7 +201,6 @@ impl Opts {
       simplify_main: true,
       pre_reduce_refs: true,
       merge_definitions: true,
-      lazy: false
     }
   }
 
@@ -325,14 +323,14 @@ pub struct RunStats {
 fn expand(net: &mut hvmc::run::Net, book: &hvmc::run::Book) {
   match net {
     hvmc::run::Net::Eager(net) => net.net.expand(book),
-    _ => {}
+    _ => unreachable!(),
   }
 }
 
 fn reduce(net: &mut hvmc::run::Net, book: &hvmc::run::Book, limit: usize) -> usize {
   match net {
     hvmc::run::Net::Eager(net) => net.net.reduce(book, limit),
-    _ => panic!("Unsupported configuration, disable debug mode `-D` or enable less optimizations `-O=0`"),
+    _ => unreachable!(),
   }
 }
 

src/main.rs

@@ -51,6 +51,9 @@ enum Mode {
     #[arg(short = '1', help = "Single-core mode (no parallelism)")]
     single_core: bool,
 
+    #[arg(short = 'L', help = "Lazy mode")]
+    lazy_mode: bool,
+  
     #[arg(short = 'l', help = "Linear readback (show explicit dups)")]
     linear: bool,
 
@@ -167,15 +170,30 @@ fn execute_cli_mode(cli: Cli, verbose: &dyn Fn(&hvml::term::Book)) -> Result<(),
       desugar_book(&mut book, Opts::light())?;
       println!("{book}");
     }
-    Mode::Run { path, mem, debug, single_core, linear, arg_stats, cli_opts, wopts } => {
+    Mode::Run { path, mem, debug, mut single_core, linear, arg_stats, cli_opts, wopts, lazy_mode } => {
       let warning_opts = wopts.get_warning_opts(WarningOpts::allow_all());
-      let opts = OptArgs::opts_from_cli(&cli_opts);
+      let mut opts = OptArgs::opts_from_cli(&cli_opts);
       opts.check();
+
+      if lazy_mode {
+        if debug {
+          return Err("Unsupported configuration, can not use debug mode `-d` with lazy mode `-L`".to_string());
+        }
+        single_core = true;
+        opts.supercombinators = false;
+        opts.pre_reduce = false;
+      } else {
+        // TODO: make the behavior of dups and sups the same as before when not using lazy mode
+        eprintln!(
+          "WARNING: Eager evaluation may have wrong results with unlabeled dups/sups, consider using lazy mode `-L`"
+        )
+      }
+
       let book = load_file_to_book(&path)?;
       verbose(&book);
       let mem_size = mem / std::mem::size_of::<(hvmc::run::APtr, hvmc::run::APtr)>();
       let (res_term, def_names, info) =
-        run_book(book, mem_size, !single_core, debug, linear, warning_opts, opts)?;
+        run_book(book, mem_size, !single_core, debug, linear, lazy_mode, warning_opts, opts)?;
       let RunInfo { stats, readback_errors, net: lnet } = info;
       let total_rewrites = total_rewrites(&stats.rewrites) as f64;
       let rps = total_rewrites / stats.run_time / 1_000_000.0;

src/term/display.rs

@@ -58,7 +58,7 @@ impl Term {
       }
       Term::Dup { tag, fst, snd, val, nxt } => write!(
         f,
-        "let{} {{{} {}}} = {}; {}",
+        "let {}{{{} {}}} = {}; {}",
         tag.display(),
         fst.as_ref().map_or("*", |x| x.as_str()),
         snd.as_ref().map_or("*", |x| x.as_str()),

tests/golden_tests.rs

@@ -116,7 +116,7 @@ fn run_file() {
     let book = do_parse_book(code, path)?;
     // 1 million nodes for the test runtime. Smaller doesn't seem to make it any faster
     let (res, def_names, info) =
-      run_book(book, 1 << 20, true, false, false, WarningOpts::deny_all(), Opts::heavy())?;
+      run_book(book, 1 << 20, true, false, false, false, WarningOpts::deny_all(), Opts::heavy())?;
     Ok(format!("{}{}", info.readback_errors.display(&def_names), res.display(&def_names)))
   })
 }
@@ -194,7 +194,7 @@ fn hangs() {
     let lck = Arc::new(RwLock::new(false));
     let got = lck.clone();
     std::thread::spawn(move || {
-      let _ = run_book(book, 1 << 20, true, false, false, WarningOpts::deny_all(), Opts::heavy());
+      let _ = run_book(book, 1 << 20, true, false, false, false, WarningOpts::deny_all(), Opts::heavy());
       *got.write().unwrap() = true;
     });
     std::thread::sleep(std::time::Duration::from_secs(expected_normalization_time));

tests/golden_tests/compile_file_o_all/exp.hvm

@@ -1 +1,2 @@
+// currently broken without lazy_mode
 main = ((λfλx (f (f x))) (λfλx (f (f x))))

tests/golden_tests/run_file/exp.hvm

@@ -1 +1,2 @@
+// currently broken without lazy_mode
 main = ((λfλx (f (f x))) (λfλx (f (f x))))

tests/golden_tests/run_file/recursive_combinator_nested.hvm

@@ -1,4 +1,4 @@
 // Tests that `({Foo @* a} 9)` is correctly extracted as a combinator, otherwise the file would hang when running
-Foo = @a match a { 0: ({Foo @* a} 9); +p: p }
+Foo = @a match a { 0: (#a {Foo @* a} 9); +p: p }
 
 main = (Foo 0)

tests/snapshots/compile_file__unused_dup_var_linearization.hvm.snap

@@ -3,5 +3,5 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/unused_dup_var_linearization.hvm
 ---
 @main = a
-& (b b) ~ {3 * {5 {9 c *} {7 (c a) *}}}
+& (b b) ~ {0 * {0 {0 c *} {0 (c a) *}}}
 

tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap

@@ -7,22 +7,22 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 @Map = ({4 @P {4 @N a}} a)
 @N = (* @Nil)
 @Nil = {4 * {4 a a}}
-@P = {8 a {6 {4 @P {4 @N (b c)}} ({3 (a d) b} {4 {8 d {6 c e}} {4 * e}})}}
+@P = {8 a {6 {4 @P {4 @N (b c)}} ({0 (a d) b} {4 {8 d {6 c e}} {4 * e}})}}
 @Pure = (a {4 {8 a {6 @Nil b}} {4 * b}})
 @U = {8 a {6 {4 @m {4 @i (b (a c))}} (b c)}}
 @V = (* @Nil)
 @W = (a ({4 @U {4 @V (a b)}} b))
 @Z = {8 a {6 {4 @s {4 @t (b (a c))}} (b c)}}
 @a = (* @Nil)
-@f = {8 {15 a {17 b c}} {6 {19 d {4 @f {4 @g (e (f (g h)))}}} ({5 (i (a {2 @J {2 @K ({4 {8 j {6 k l}} {4 * l}} ({4 {8 c {6 h m}} {4 * m}} n))}})) {7 o e}} ({9 i {11 j f}} ({13 {4 @h {4 @i (o ({4 {8 b {6 d p}} {4 * p}} k))}} g} n)))}}
+@f = {8 {0 a {0 b c}} {6 {0 d {4 @f {4 @g (e (f (g h)))}}} ({0 (i (a {2 @J {2 @K ({4 {8 j {6 k l}} {4 * l}} ({4 {8 c {6 h m}} {4 * m}} n))}})) {0 o e}} ({0 i {0 j f}} ({0 {4 @h {4 @i (o ({4 {8 b {6 d p}} {4 * p}} k))}} g} n)))}}
 @g = (* @w)
 @h = {8 a {6 b (c ({4 @f {4 @g (c (a (b d)))}} d))}}
 @i = (* (a a))
-@m = {8 a {6 {4 @Z {4 @a (b {4 @m {4 @i (c (d e))}})}} ({21 c {23 f b}} ({4 @h {4 @i (f (a d))}} e))}}
+@m = {8 a {6 {4 @Z {4 @a (b {4 @m {4 @i (c (d e))}})}} ({0 c {0 f b}} ({4 @h {4 @i (f (a d))}} e))}}
 @main = (a (b c))
 & @W ~ (a (d c))
 & @Map ~ (b (@Pure d))
-@s = {8 a {6 {4 @Z {4 @a (b c)}} ({23 d b} ({4 @h {4 @i (d (a e))}} {4 {8 e {6 c f}} {4 * f}}))}}
+@s = {8 a {6 {4 @Z {4 @a (b c)}} ({0 d b} ({4 @h {4 @i (d (a e))}} {4 {8 e {6 c f}} {4 * f}}))}}
 @t = (* @x)
 @w = (a (b {4 {8 a {6 b c}} {4 * c}}))
 @x = (a {4 {8 a {6 @Nil b}} {4 * b}})

tests/snapshots/compile_file_o_all__match_dup_and_reconstruction.hvm.snap

@@ -4,7 +4,7 @@ input_file: tests/golden_tests/compile_file_o_all/match_dup_and_reconstruction.h
 ---
 @A = {4 a (b [b a])}
 @Boxed = (a {2 {4 a b} b})
-@Got = ({3 {2 @A (a b)} a} b)
+@Got = ({0 {2 @A (a b)} a} b)
 @main = a
 & @Got ~ (b a)
 & @Boxed ~ (#10 b)

tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap

@@ -6,7 +6,7 @@ input_file: tests/golden_tests/compile_file_o_all/scrutinee_reconstruction.hvm
 @C = {4 * @E}
 @E = (a (* a))
 @None = {2 * {2 a a}}
-@Option.or = ({3 {2 @C {2 @B (a b)}} a} b)
+@Option.or = ({0 {2 @C {2 @B (a b)}} a} b)
 @Some = (a {2 {4 a b} {2 * b}})
 @main = a
 & @Option.or ~ (b (@None a))

tests/snapshots/compile_file_o_all__spacing.hvm.snap

@@ -2,5 +2,5 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/spacing.hvm
 ---
-@main = ({3 (a b) a} b)
+@main = ({0 (a b) a} b)
 

tests/snapshots/compile_term__infer_dup.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_term/infer_dup.hvm
 ---
-({3 (a b) a} b)
+({0 (a b) a} b)

tests/snapshots/compile_term__let_substitution.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_term/let_substitution.hvm
 ---
-({3 (a b) a} b)
+({0 (a b) a} b)

tests/snapshots/compile_term__lets.hvm.snap

@@ -4,6 +4,6 @@ input_file: tests/golden_tests/compile_term/lets.hvm
 ---
 a
 & (b b) ~ (c (d (e a)))
-& (f f) ~ {9 (g (h (i e))) {11 g {13 h i}}}
-& (j j) ~ {5 (k (l d)) {7 k l}}
-& (m m) ~ {3 (n c) n}
+& (f f) ~ {0 (g (h (i e))) {0 g {0 h i}}}
+& (j j) ~ {0 (k (l d)) {0 k l}}
+& (m m) ~ {0 (n c) n}

tests/snapshots/desugar_file__dup_linearization.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/desugar_file/dup_linearization.hvm
 ---
-(main) = let {a_1 a_1_dup} = *; let {a_2 a_2_dup} = a_1_dup; let {a_3 a_3_dup} = a_2_dup; let {a_4 a_5} = a_3_dup; ((a_5, a_1), (a_2, (a_3, a_4)))
+(main) = let #0{a_1 a_1_dup} = *; let #0{a_2 a_2_dup} = a_1_dup; let #0{a_3 a_3_dup} = a_2_dup; let #0{a_4 a_5} = a_3_dup; ((a_5, a_1), (a_2, (a_3, a_4)))

tests/snapshots/run_file__recursive_combinator_nested.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/recursive_combinator_nested.hvm
 ---
-#1 {8 0}
+#a{8 0}

tests/snapshots/run_file__sup_app.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/sup_app.hvm
 ---
-#id {3 3}
+#id{3 3}

tests/snapshots/run_file__superposed_is_even.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/superposed_is_even.hvm
 ---
-#0 {#0 {T F} #0 {T F}}
+#0{#0{T F} #0{T F}}