[sc-475] Add documentation for new match options

README.md

@@ -130,6 +130,56 @@ data List = (List.cons head tail) | (List.nil)
 ListEx2 = (List.cons 1 (List.cons 2 (List.cons 3 List.nil)))
 ```
 
+It's possible to match different kinds of terms. These three forms are equivalent:
+```rs
+match list {
+  (List.cons hd tl):  (Some hd)
+  List.nil:  None
+}
+
+// If we don't provide field bindings, it will implicitly use
+// the fields of the declared data type
+match list {
+  List.cons:  (Some list.head)
+  List.nil:  None
+}
+
+match bind = list {
+  List.cons:  (Some bind.head)
+  List.nil:  None
+}
+```
+
+Match native numbers:
+```rs
+match 4 {
+  0:  "zero"
+  5:  "five"
+  4:  "four"
+  _:  "other"
+}
+```
+
+Which is the equivalent of nesting match terms:
+```rs
+match 4 {
+  0: "zero"
+  1+a: match (- (+ a (+ 0 1)) 5) {
+    0: "five"
+    _:  ...
+  }
+}
+```
+
+Match multiple terms:
+```rs
+λa λb match a, b {
+  (Some True) (x, y): (Some (x, y))
+  (Some False) (x, y): (Some (y, x))
+  None *: None
+}
+```
+
 ### More features
 
 Key:

cspell.json

@@ -42,6 +42,7 @@
     "namegen",
     "nams",
     "numop",
+    "nums",
     "oper",
     "opre",
     "oprune",

docs/compiler-options.md

@@ -142,20 +142,20 @@ When the `linearize-matches` option is used, linearizes only vars that are used
 
 Example:
 ```rs
-λa λb match a { 0: b; +: b }
+λa λb match a { 0: b; 1+: b }
 
 // Is transformed to
-λa λb (match a { 0: λc c; +: λd d } b)
+λa λb (match a { 0: λc c; 1+: λ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 }
+λa λb λc match a { 0: b; 1+: c }
 
 // Is transformed to
-λa λb λc (match a { 0: λd λ* d; +: λ* λe e } b c)
+λa λb λc (match a { 0: λd λ* d; 1+: λ* λe e } b c)
 ```
 
 ## float-combinators

docs/native-numbers.md

@@ -34,22 +34,22 @@ main = (~ 42 10)
 
 HVM-lang also includes a `match` syntax for native numbers. The `0` case is chosen when `n` is 0, and the `+` case is chosen when `n` is greater than 0. The previous number, by default, bound to `n-1`.
 ```rs
-Number.to_church = λn λf λx 
+Number.to_church = λn λf λx
   match n {
     0: x
-    +: (f (Number.to_church n-1 f x))
+    1+: (f (Number.to_church n-1 f x))
   }
 // Alternative syntax
-Number.to_church = λn λf λx 
+Number.to_church = λn λf λx
   match n {
     0: x
-    +p: (f (Number.to_church p f x))
+    1+p: (f (Number.to_church p f x))
   }
 // Alternative syntax with name binding
-Number.to_church = λn λf λx 
+Number.to_church = λn λf λx
   match num = n {
     0: x
-    +: (f (Number.to_church num-1 f x)
+    1+: (f (Number.to_church num-1 f x)
   }
 ```
 
@@ -60,14 +60,10 @@ fibonacci = λn // n is the argument
   match n {
     // If the number is 0, then return 0
     0: 0
-    // If the number is greater than 0, bind it predecessor to `a`
-    +a:
-    match a {
-      // If the predecessor is 0, then return 1
-      0: 1
-      // Otherwise, bind n-2 to `b` and return the sum of (fib n-1) and (fib n-2)
-      +b: (+ (fibonacci a) (fibonacci b))
-    }
+    // If the number is 1, then return 1
+    1: 1
+    // Otherwise, return the sum of (fib (n-2 + 1)) and (fib n-2)
+    2+: (+ (fibonacci (+ n-2 1)) (fibonacci n-2))
   }
 
 main = (fibonacci 15)

docs/writing-fusing-functions.md

@@ -130,7 +130,7 @@ not = λboolean (boolean false true)
 fusing_not = λboolean λt λf (boolean f t)
 // Creates a Church numeral out of a native number
 to_church 0 = λf λx x
-to_church +p = λf λx (f (to_church p f x))
+to_church 1+p = λf λx (f (to_church p f x))
 main =
 	let two = λf λx (f (f x))
 	let two_pow_512 = ((to_church 512) two) // Composition of church-encoded numbers is equivalent to exponentiation.

examples/example.hvm

@@ -22,7 +22,7 @@
 (Num.pred) = λn 
   match n { 
     0: 0
-    +: n-1
+    1+: n-1
   }
 
 // Write new data types like this

examples/fusing_not.hvm

@@ -4,7 +4,7 @@ not = λboolean (boolean false true)
 fusing_not = λboolean λt λf (boolean f t)
 // Creates a Church numeral out of a native number
 to_church 0 = λf λx x
-to_church +p = λf λx (f (to_church p f x))
+to_church 1+p = λf λx (f (to_church p f x))
 main = 
 	let two = λf λx (f (f x))
 	let two_pow_512 = ((to_church 512) two) // Composition of church-encoded numbers is equivalent to exponentiation.