From a0dbd04791cd91c125fc31c602145f709d1a03b7 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Tue, 27 Feb 2024 17:47:20 -0300
Subject: [PATCH] Improve docs and update examples with new match syntax

---
 README.md                        | 11 ++++++-----
 cspell.json                      |  1 +
 docs/compiler-options.md         |  8 ++++----
 docs/native-numbers.md           | 18 +++++++-----------
 docs/writing-fusing-functions.md |  2 +-
 examples/example.hvm             |  2 +-
 examples/fusing_not.hvm          |  2 +-
 7 files changed, 21 insertions(+), 23 deletions(-)

diff --git a/README.md b/README.md
index 5829ddc52..cc8624154 100644
--- a/README.md
+++ b/README.md
@@ -130,7 +130,7 @@ data List = (List.cons head tail) | (List.nil)
 ListEx2 = (List.cons 1 (List.cons 2 (List.cons 3 List.nil)))
 ```
 
-Match different kinds of terms, both matches are equivalent:
+It's possible to match different kinds of terms. These three forms are equivalent:
 ```rs
 match list {
   (List.cons hd tl):  (Some hd)
@@ -162,7 +162,7 @@ Which is the equivalent of nesting match terms:
 ```rs
 match 4 {
   0: "zero"
-  1+a: match (- a 4) {
+  1+a: match (- (+ a (+ 0 1)) 5) {
     0: "five"
     _:  ...
   }
@@ -171,9 +171,10 @@ match 4 {
 
 Match multiple terms:
 ```rs
-match True, True {
-  True True:  True
-  _ _: False
+λa λb match a, b {
+  (Some True) (x, y): (Some (x, y))
+  (Some False) (x, y): (Some (y, x))
+  None *: None
 }
 ```
 
diff --git a/cspell.json b/cspell.json
index fca40f4d3..7bd1f52e8 100644
--- a/cspell.json
+++ b/cspell.json
@@ -42,6 +42,7 @@
     "namegen",
     "nams",
     "numop",
+    "nums",
     "oper",
     "opre",
     "oprune",
diff --git a/docs/compiler-options.md b/docs/compiler-options.md
index 7ae6f75f7..4aaeb2c22 100644
--- a/docs/compiler-options.md
+++ b/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
diff --git a/docs/native-numbers.md b/docs/native-numbers.md
index 5edf79caa..d464345c5 100644
--- a/docs/native-numbers.md
+++ b/docs/native-numbers.md
@@ -37,19 +37,19 @@ HVM-lang also includes a `match` syntax for native numbers. The `0` case is chos
 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 
   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 
   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, and return the sum of (fib (n-2 + 1)) and (fib n-2)
+    2+: (+ (fibonacci (+ n-2 1)) (fibonacci n-2))
   }
 
 main = (fibonacci 15)
diff --git a/docs/writing-fusing-functions.md b/docs/writing-fusing-functions.md
index fbb640cd5..6128033e2 100644
--- a/docs/writing-fusing-functions.md
+++ b/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.
diff --git a/examples/example.hvm b/examples/example.hvm
index 5170f5a92..ca7fe5a40 100644
--- a/examples/example.hvm
+++ b/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
diff --git a/examples/fusing_not.hvm b/examples/fusing_not.hvm
index af1262d10..0de7599b2 100644
--- a/examples/fusing_not.hvm
+++ b/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.