Update recursion error message and update docs

docs/lazy-definitions.md

@@ -1,42 +1,59 @@
 # Making recursive definitions lazy
 
-The HVM-Core is an eager runtime, for both CPU and parallel GPU implementations. Terms that use recursive terms will unroll indefinitely.
+In strict-mode, terms that use recursive terms will unroll indefinitely.
 
-This means that for example, the following code will hang, despite being technically correct and working on Haskell:
+This is a simple piece of code that works on many other functional programming languages, but hangs on HVM:
 
-```rs
-data Nat = Z | (S p)
+```rust
+Cons = λx λxs λcons λnil (cons x xs)
+Nil  =        λcons λnil nil
 
-Y = λf (λx (f (x x)) λx (f (x x)))
+Map = λf λlist
+  let cons = λx λxs (Cons (f x) (Map f xs))
+  let nil = Nil
+  (list cons nil)
 
-Nat.add = (Y λaddλaλb match a {
-	Z: b
-	(S p): (S (add p b))
-})
+Main = (Map λx (+ x 1) (Cons 1 Nil))
+```
 
-main = (Nat.add (S (S (S Z))) (S Z))
+The recursive `Map` definition never gets reduced.
+Using the debug mode `-d` we can see the steps:
+
+```
+(Map λa (+ a 1) (Cons 1 Nil))
+---------------------------------------
+(Map λa (+ a 1) λb λ* (b 1 Nil))
+---------------------------------------
+(Cons (λa (+ a 1) 1) (Map λa (+ a 1) Nil))
+---------------------------------------
+(Cons (λa (+ a 1) 1) (Nil λb λc (Cons (λa (+ a 1) b) (Map λa (+ a 1) c)) Nil))
+---------------------------------------
+...
 ```
 
-Because of that, its recommended to use a [supercombinator](https://en.wikipedia.org/wiki/Supercombinator) formulation to make terms be unrolled lazily, preventing infinite expansion in recursive function bodies.
+For similar reasons, if we try using Y combinator it also won't work.
 
-The `Nat.add` definition below can be a supercombinator if linearized.
+```rust
+Y = λf (λx (f (x x)) λx (f (x x)))
 
-```rs
-Nat.add = λaλb match a {
-	Z: b
-	(S p): (S (Nat.add p b))
-}
+Map = (Y λrec λf λlist
+  let cons = λx λxs (Cons (f x) (rec f xs))
+  let nil = Nil
+  (list cons nil f))
 ```
 
-```rs
-// Linearized Nat.add
-Nat.add = λa match a {
-	Z: λb b
-	(S p): λb (S (Nat.add p b))
-}
+By linearizing `f`, the `Map` function "fully reduces" first and then applies `f`.
+
+```rust
+Map = λf λlist
+  let cons = λx λxs λf (Cons (f x) (Map f xs))
+  let nil = λf Nil
+  (list cons nil f)
 ```
 
-This code will work as expected, because `Nat.add` is unrolled lazily only when it is used as an argument to a lambda.
+This code will work as expected, since `cons` and `nil` are lambdas without free variables, they will be automatically floated to new definitions if the [float-combinators](compiler-options#float-combinators) option is active, allowing them to be unrolled lazily by hvm.
+
+It's recommended to use a [supercombinator](https://en.wikipedia.org/wiki/Supercombinator) formulation to make terms be unrolled lazily, preventing infinite expansion in recursive function bodies.
 
 ### Automatic optimization
 

src/hvmc_net/mutual_recursion.message

@@ -14,5 +14,9 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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))
+
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.

tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap

@@ -20,7 +20,11 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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))
+
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 
 

tests/snapshots/mutual_recursion__a_b_c.hvm.snap

@@ -21,5 +21,9 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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))
+
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.

tests/snapshots/mutual_recursion__multiple.hvm.snap

@@ -24,5 +24,9 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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))
+
 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

@@ -20,5 +20,9 @@ Just append the `-L` option to `HVM-Lang`, and it will run in lazy-mode. It has
 
 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))
+
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.