Improve some error messages, add radixsort example

examples/radix_sort.hvm

@@ -0,0 +1,98 @@
+data Map = Free | Used | (Both a b)
+data Arr = Null | (Leaf x) | (Node a b)
+
+(Swap s a b) = switch s {
+  0: (Both a b)
+  _: (Both b a)
+}
+
+// Sort : Arr -> Arr
+(Sort t) = (ToArr 0 (ToMap t))
+
+// ToMap : Arr -> Map
+(ToMap Null)       = Free
+(ToMap (Leaf a))   = (Radix a)
+(ToMap (Node a b)) = (Merge (ToMap a) (ToMap b))
+
+// ToArr : U60 -> Map -> Arr
+(ToArr x Free) = Null
+(ToArr x Used) = (Leaf x)
+(ToArr x (Both a b)) =
+  let a = (ToArr (+ (* x 2) 0) a)
+  let b = (ToArr (+ (* x 2) 1) b)
+  (Node a b)
+
+// Merge : Map -> Map -> Map
+(Merge Free       Free)       = Free
+(Merge Free       Used)       = Used
+(Merge Used       Free)       = Used
+(Merge Used       Used)       = Used
+(Merge Free       (Both c d)) = (Both c d)
+(Merge (Both a b) Free)       = (Both a b)
+(Merge (Both a b) (Both c d)) = (Both (Merge a c) (Merge b d))
+(Merge (Both a b) Used) = *
+(Merge Used (Both a b)) = *
+
+// Radix : U60 -> Map
+(Radix n) =
+  let r = Used
+  let r = (Swap (& n 1) r Free)
+  let r = (Swap (& n 2) r Free)
+  let r = (Swap (& n 4) r Free)
+  let r = (Swap (& n 8) r Free)
+  let r = (Swap (& n 16) r Free)
+  (Radix2 n r)
+
+(Radix2 n r) =
+  let r = (Swap (& n 32) r Free)
+  let r = (Swap (& n 64) r Free)
+  let r = (Swap (& n 128) r Free)
+  let r = (Swap (& n 256) r Free)
+  let r = (Swap (& n 512) r Free)
+  (Radix3 n r)
+
+(Radix3 n r) =
+  let r = (Swap (& n 1024) r Free)
+  let r = (Swap (& n 2048) r Free)
+  let r = (Swap (& n 4096) r Free)
+  let r = (Swap (& n 8192) r Free)
+  let r = (Swap (& n 16384) r Free)
+  (Radix4 n r)
+
+(Radix4 n r) =
+  let r = (Swap (& n 32768) r Free)
+  let r = (Swap (& n 65536) r Free)
+  let r = (Swap (& n 131072) r Free)
+  let r = (Swap (& n 262144) r Free)
+  let r = (Swap (& n 524288) r Free)
+  (Radix5 n r)
+
+(Radix5 n r) =
+  let r = (Swap (& n 1048576) r Free)
+  let r = (Swap (& n 2097152) r Free)
+  let r = (Swap (& n 4194304) r Free)
+  let r = (Swap (& n 8388608) r Free)
+  r
+
+
+// Reverse : Arr -> Arr
+(Reverse Null)       = Null
+(Reverse (Leaf a))   = (Leaf a)
+(Reverse (Node a b)) = (Node (Reverse b) (Reverse a))
+
+// Sum : Arr -> U60
+(Sum Null)       = 0
+(Sum (Leaf x))   = x
+(Sum (Node a b)) = (+ (Sum a) (Sum b))
+
+// Gen : U60 -> Arr
+(Gen n) = (Gen.go n 0)
+  (Gen.go n x) = switch n {
+    0: (Leaf x)
+    _:
+      let a = (* x 2)
+      let b = (| (* x 2) 1)
+      (Node (Gen.go n-1 a) (Gen.go n-1 b))
+  }
+
+Main = (Sum (Sort (Reverse (Gen 4))))

src/hvmc_net/mutual_recursion.message

@@ -1,24 +1,21 @@
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
 {cycles}
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

src/term/transform/fix_match_terms.rs

@@ -1,5 +1,5 @@
 use crate::{
-  diagnostics::{Diagnostics, WarningType},
+  diagnostics::{Diagnostics, WarningType, ERR_INDENT_SIZE},
   maybe_grow,
   term::{Adts, Constructors, Ctx, MatchRule, Name, NumType, Term},
 };
@@ -248,11 +248,24 @@ impl std::fmt::Display for FixMatchErr {
       FixMatchErr::NonExhaustiveMatch { typ, missing } => {
         write!(f, "Non-exhaustive 'match' expression of type '{typ}'. Case '{missing}' not covered.")
       }
-      FixMatchErr::IrrefutableMatch { var } => write!(
-        f,
-        "Irrefutable 'match' expression. All cases after '{}' will be ignored. If this is not a mistake, consider using a 'let' expression instead.",
-        var.as_ref().unwrap_or(&Name::new("*"))
-      ),
+      FixMatchErr::IrrefutableMatch { var } => {
+        writeln!(
+          f,
+          "Irrefutable 'match' expression. All cases after variable pattern '{}' will be ignored.",
+          var.as_ref().unwrap_or(&Name::new("*")),
+        )?;
+        writeln!(
+          f,
+          "{:ERR_INDENT_SIZE$}Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition.",
+          "",
+        )?;
+        write!(
+          f,
+          "{:ERR_INDENT_SIZE$}If this is not a mistake, consider using a 'let' expression instead.",
+          ""
+        )
+      }
+
       FixMatchErr::UnreachableMatchArms { var } => write!(
         f,
         "Unreachable arms in 'match' expression. All cases after '{}' will be ignored.",

tests/golden_tests/compile_file/redex_order_recursive.hvm

@@ -0,0 +1,13 @@
+tail_recursive = @a (a @x (+ 1 (tail_recursive x)) 0)
+
+fold = @bm (bm
+  @lft @rgt (add (fold lft) (fold rgt))
+  @s @z (s @s @z z)
+)
+
+add = @a (a 
+  @p @b (add p @s @z (s b))
+  @b b
+)
+
+main = *

tests/golden_tests/compile_file_o_no_all/redex_order.hvm

@@ -3,8 +3,27 @@
 foo = @x (a (b (c x)))
 foo2 = (a (b (c 0)))
 
+bar = (a (b (c 0) (c (d 1))) (b (c (d 2)) (c 3)))
+//bar = (
+//  (
+//    a
+//    (
+//      (b (c 0))
+//      (c (d 1))
+//    )
+//  )
+//  (
+//    (
+//      b
+//      (c (d 2))
+//    )
+//    (c 3)
+//  )
+//)
+
 a = @x x
 b = @x x
 c = @x x
+d = @x x
 
 main = (foo foo2)

tests/golden_tests/run_file/radix_sort_ctr.hvm

@@ -96,4 +96,3 @@ data Arr = Null | (Leaf x) | (Node a b)
   }
 
 Main = (Sum (Sort (Reverse (Gen 4))))
-//Main = (Sort 0)

tests/snapshots/compile_file__redex_order_recursive.hvm.snap

@@ -0,0 +1,25 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/compile_file/redex_order_recursive.hvm
+---
+@add = ((@add__C0 ((a a) b)) b)
+
+@add__C0 = (a (b d))
+  & @add ~ (a (((b c) (* c)) d))
+
+@fold = ((@fold__C1 (@fold__C0 a)) a)
+
+@fold__C0 = (((* (a a)) b) (* b))
+
+@fold__C1 = (a (c e))
+  & @add ~ (b (d e))
+  & @fold ~ (a b)
+  & @fold ~ (c d)
+
+@main = *
+
+@tail_recursive = ((@tail_recursive__C0 (0 a)) a)
+
+@tail_recursive__C0 = (a c)
+  & $(b c) ~ [+1]
+  & @tail_recursive ~ (a b)

tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap

@@ -3,27 +3,24 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/repeated_name_trucation.hvm
 ---
 Warnings:
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
   * long_name_that_truncates -> long_name_that_truncates
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

tests/snapshots/compile_file_o_all__self_ref.hvm.snap

@@ -3,27 +3,24 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/self_ref.hvm
 ---
 Warnings:
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
   * Foo -> Foo
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

tests/snapshots/compile_file_o_no_all__bitonic_sort.hvm.snap

@@ -3,8 +3,8 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_no_all/bitonic_sort.hvm
 ---
 Errors:
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
   * Down -> Flow -> Down
   * Warp -> Warp
   * Gen -> Gen
@@ -13,22 +13,19 @@ The following recursive cycles are not compatible with strict-mode the way these
   * ...
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

tests/snapshots/compile_file_o_no_all__list_reverse.hvm.snap

@@ -3,28 +3,25 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_no_all/list_reverse.hvm
 ---
 Errors:
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
   * concat -> concat
   * reverse -> reverse
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

tests/snapshots/compile_file_o_no_all__redex_order.hvm.snap

@@ -6,8 +6,21 @@ input_file: tests/golden_tests/compile_file_o_no_all/redex_order.hvm
 
 @b = (a a)
 
+@bar = i
+  & @a ~ (d (h i))
+  & @b ~ (a (c d))
+  & @c ~ (0 a)
+  & @c ~ (b c)
+  & @d ~ (1 b)
+  & @b ~ (f (g h))
+  & @c ~ (e f)
+  & @d ~ (2 e)
+  & @c ~ (3 g)
+
 @c = (a a)
 
+@d = (a a)
+
 @foo = (a d)
   & @a ~ (c d)
   & @b ~ (b c)

tests/snapshots/compile_file_o_no_all__sum_tree.hvm.snap

@@ -3,28 +3,25 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_no_all/sum_tree.hvm
 ---
 Errors:
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
   * gen -> gen
   * sum -> sum
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

tests/snapshots/examples__radix_sort.hvm.snap

@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: examples/radix_sort.hvm
+---
+120

tests/snapshots/mutual_recursion__a_b_c.hvm.snap

@@ -3,27 +3,24 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/mutual_recursion/a_b_c.hvm
 ---
 Errors:
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
   * A -> B -> C -> A
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

tests/snapshots/mutual_recursion__merged.hvm.snap

@@ -3,30 +3,27 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/mutual_recursion/merged.hvm
 ---
 Errors:
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
   * Rec -> X -> Rec
   * Rec -> Y -> Rec
   * Rec2 -> X -> Rec2
   * Rec2 -> Y -> Rec2
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

tests/snapshots/mutual_recursion__multiple.hvm.snap

@@ -3,30 +3,27 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/mutual_recursion/multiple.hvm
 ---
 Errors:
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
   * A -> B -> C -> A
   * H -> I -> H
   * M -> M
   * N -> N
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

tests/snapshots/mutual_recursion__odd_even.hvm.snap

@@ -3,27 +3,24 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/mutual_recursion/odd_even.hvm
 ---
 Errors:
-Seems like you're trying to run some recursive function(s) on strict-mode.
-The following recursive cycles are not compatible with strict-mode the way these functions were written:
+Seems like you're trying to run some recursive function(s).
+The following functions were written in a way that create recursive cycles that are not compatible with the strict evaluation of HVM.
   * isEven -> isOdd -> isEven
 
 Due to the ultra-greedy nature of strict-mode, that might result in infinite loops.
-If the float-combinators optimization is not on, we recommend activating it.
+You have to refactor these function to use lazy references.
 
-You have 2 options:
+The float-combinators and linearize-matches-extra options can help with doing this automatically.
+They are turned on by default, but if you deactivated them, consider re-enabling.
 
-1. Easy Fix: use lazy-mode.
+When a function reference is in head position of an application it will be greedly expanded, leading to an infinite loop.
+This for example doesn't work: 'Foo = λa λb (b (λc (Foo a c)) a)'
+If the application is written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle.
+The example as combinators: 'Foo = λa λb (b (λc λa (Foo a c)) (λa a) a)
+Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
 
-Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has the advantage of not doing wasteful work, having an improved complexity class, and being compatible with unrestricted recursion. It has a small overhead though, and isn't compatible with GPU.
-
-2. Hard Fix: refactor the program to use lazy references.
-
-When a function reference is in head position of an application or is duplicated by the non-linear use of a `let` expression it will be greedly expanded, leading to an infinite loop.
-If the application is used written as a combinator, it will automatically lifted to a lazy reference, which usually breaks the recursion cycle. Alternatively, by using the built-in `data` and `match` syntax, hvm-lang will try to do this automatically.
-(e.g. If pattern matching on scott-encoded ADTs, write '@a @x(x @a (Foo a) a)' instead of '@a @x(x (Foo a))')
-
-For let expressions where the variable is non-linear (used more than once), you can instead employ `use` expressions to statically duplicate the offending recursive term.
-(e.g. write 'Foo = @f use x = Foo; (f x x)' instead of 'Foo = @f let x = Foo; (f x x)')
+For let expressions where the variable is non-linear, you can instead employ `use` expressions to statically duplicate the offending recursive term.
+(e.g. write 'Foo = λf use x = Foo; (f x x)' instead of 'Foo = λf let x = Foo; (f x x)')
 
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 

tests/snapshots/run_file__match_vars.hvm.snap

@@ -4,4 +4,6 @@ input_file: tests/golden_tests/run_file/match_vars.hvm
 ---
 Errors:
 In definition 'main':
-  Irrefutable 'match' expression. All cases after 'true' will be ignored. If this is not a mistake, consider using a 'let' expression instead.
+  Irrefutable 'match' expression. All cases after variable pattern 'true' will be ignored.
+  Note that to use a 'match' expression, the matched constructors need to be defined in a 'data' definition.
+  If this is not a mistake, consider using a 'let' expression instead.