WIP improve pattern matching docs

docs/pattern-matching.md

@@ -1,15 +1,17 @@
 # Pattern Matching
 
-HVM-Lang offers pattern matching capabilities. You can use pattern matching in defining rules and with the `match` expression.
+HVM-Lang offers pattern matching capabilities. You can use pattern matching in function definitions and with the `match` expression.
+
+Pattern matching definitions are just a syntax sugar to match expressions:
 
-In example, definitions are a syntax sugar to match expressions:
 ```rust
+// These two are equivalent
 (Foo 0 false (Cons h1 (Cons h2 t))) = (A h1 h2 t)
 (Foo 0 * *) = B
 (Foo 1+n false *) = n
 (Foo 1+n true *) = 0
 
-Foo = @arg1 @arg2 @arg3 match arg1 arg2 arg3 {
+Foo = λarg1 λarg2 λarg3 match arg1 arg2 arg3 {
   (Foo 0 false (Cons h1 (Cons h2 t))): (A h1 h2 t)
   (Foo 0 * *): B
   (Foo 1+n false *): n
@@ -18,8 +20,16 @@ Foo = @arg1 @arg2 @arg3 match arg1 arg2 arg3 {
 ```
 
 Pattern matching on numbers has two forms.
-With the successor pattern it will expect a sequence of numbers up to the `n+var` pattern:
+With the successor pattern `n+var` it will expect to cover every case up to `n`:
+
 ```rust
+// Error: Case '2' not covered.
+match n {
+  1: B;
+  0: A;
+  3+: ...;
+}
+
 match n {
   0: A
   1: B
@@ -38,6 +48,7 @@ match n {
 ```
 
 With the wildcard pattern you can use any number freely:
+
 ```rust
 match n {
   23: A
@@ -58,17 +69,27 @@ match (- n 32) {
 }
 ```
 
+Notice that this definition is valid, since `*` will cover both `1+p` and `0` cases when the first argument is `False`.
+
+```rust
+pred_if False *   if_false = if_false
+pred_if True  1+p *        = p
+pred_if True  0   *        = 0
+```
+
 Match on tuples become let tuple destructors, which are compiled to a native tuple destructor in hvm-core.
+
 ```rust
 match x {
   (f, s): s
 }
 
 // Becomes:
-let (f, s) = (1, 2); s
+let (f, s) = x; s
 ```
 
 Match on vars becomes a rebinding of the variable with a let expression.
+
 ```rust
 match x {
   c: (Some c)
@@ -78,7 +99,8 @@ match x {
 let c = x; (Some c)
 ```
 
-Pattern matching on strings and lists desugars to a list of matches on List/String.cons and List.String.nil
+Pattern matching on strings and lists desugars to a list of matches on List/String.cons and List/String.nil
+
 ```rust
 Hi "hi" = 1
 Hi _ = 0
@@ -96,7 +118,8 @@ Foo (List.cons x List.nil) = x
 Foo _ = 3
 ```
 
-Match on ADT constructors can change based on the current encoding.
+Matches on ADT constructors are compiled to different expressions depending on the chosen encoding.
+
 ```rust
 data Maybe = (Some val) | None
 
@@ -109,10 +132,11 @@ match x {
 #Maybe (x #Maybe.Some.val λval val 0)
 
 // Otherwise, if the current encoding is 'adt-scott' it becomes:
-(x @val val 0)
+(x λval val 0)
 ```
 
 If constructor fields are not specified, we implicitly bind them based on the name given in the ADT declaration.
+
 ```rust
 data Maybe = (Some value) | None
 
@@ -129,6 +153,7 @@ match x {
 ```
 
 Nested pattern matching allows for matching and deconstructing data within complex structures.
+
 ```rust
 data Tree = (Leaf value) | (Node left right)
 
@@ -138,14 +163,19 @@ match tree {
   Leaf: (Single tree.value)
 }
 
-// Becomes:
+// Which is roughly equivalent to:
 match tree {
   (Node left right): match left {
+    (Node left.left left.right):
+      let left = (Node left.left left.right);
+      (Merge left right)
     (Leaf a): match right {
+      (Node right.left right.right):
+        let left = (Leaf a);
+        let right = (Node right.left right.right);
+        (Merge left right)
       (Leaf b): (Combine a b)
-      _: (Merge left right)
     }
-    _: (Merge left right)
   }
   (Leaf value): (Single value)
 }