From 2f62c017ec873b05aa4f50bcc45f4a80be1f31a5 Mon Sep 17 00:00:00 2001
From: sebastianselander <sebastian.selander@gmail.com>
Date: Fri, 5 May 2023 15:42:18 +0200
Subject: [PATCH] Fixed grammar and more peano stuff

---
 Grammar.cf       |  8 ++++++++
 test_program.crf | 49 ++++++++++++++++++++++++++++++++++++++----------
 2 files changed, 47 insertions(+), 10 deletions(-)

diff --git a/Grammar.cf b/Grammar.cf
index 2db8b14..f0a06b9 100644
--- a/Grammar.cf
+++ b/Grammar.cf
@@ -1,3 +1,10 @@
+
+-------------------------------------------------------------------------------
+-- * PROGRAM
+-------------------------------------------------------------------------------
+
+Program. Program ::= [Def];
+
 -------------------------------------------------------------------------------
 -- * TOP-LEVEL
 -------------------------------------------------------------------------------
@@ -101,3 +108,4 @@ token Symbol (["@#%^&*_-+=|?/<>,•:[]"]+) ;
 
 comment "--";
 comment "{-" "-}";
+
diff --git a/test_program.crf b/test_program.crf
index 6e528dc..3c7b31a 100644
--- a/test_program.crf
+++ b/test_program.crf
@@ -3,14 +3,8 @@ data Nat where
   Zero : Nat
   Succ : Nat -> Nat
 
-toInt : Nat -> Int
-toInt a = case a of
-    Succ n => 1 + toInt n
-    Zero => 0
-
-fromInt a = case a of
-    0 => Zero
-    n => Succ (fromInt (a - 1))
+-- Returns 10_000
+main = toInt (fromInt 10000)
 
 -- Peano arithmetic --
 
@@ -26,5 +20,40 @@ mul left right = case right of
     Zero => Zero
     Succ n => add left (mul left n)
 
--- Returns 10_000
-main = toInt (mul (fromInt 100) (fromInt 100))
+eq : Nat -> Nat -> Nat
+eq a b = case a of
+    Zero => case b of 
+        Zero => Succ Zero
+        _    => Zero
+    Succ n => case b of
+        Zero => Zero
+        Succ m => eq n m
+
+less : Nat -> Nat -> Nat
+less a b = case a of
+    Zero => case b of
+        Zero => Zero
+        Succ n => Succ Zero
+    Succ n => case b of
+        Zero => Zero
+        Succ m => less n m
+
+greater : Nat -> Nat -> Nat
+greater a b = case b of
+    Zero => case a of
+        Zero => Zero
+        Succ n => Succ Zero
+    Succ n => case a of
+        Zero => Zero
+        Succ m => less n m
+
+-- Aux
+
+toInt : Nat -> Int
+toInt a = case a of
+    Succ n => 1 + toInt n
+    Zero => 0
+
+fromInt a = case a of
+    0 => Zero
+    n => Succ (fromInt (a - 1))