From a87862a99f818d3dff0f8f6aaa3ab3e00b29019a Mon Sep 17 00:00:00 2001
From: Martin Fredin <fredin.martin@gmail.com>
Date: Sat, 29 Apr 2023 16:02:51 +0200
Subject: [PATCH] Fix sample programs

---
 sample-programs/basic-0.crf              | 20 -----------
 sample-programs/basic-1.crf              | 13 -------
 sample-programs/basic-10.crf             | 10 ------
 sample-programs/basic-2.crf              |  6 ----
 sample-programs/basic-3.crf              |  2 --
 sample-programs/basic-4.crf              |  2 --
 sample-programs/basic-5.crf              |  8 -----
 sample-programs/basic-6.crf              | 15 ---------
 sample-programs/basic-7.crf              |  8 -----
 sample-programs/basic-8.crf              | 20 -----------
 sample-programs/basic-9.crf              | 10 ------
 sample-programs/example-programs/ex1.crf |  1 -
 sample-programs/example-programs/ex2.crf |  4 ---
 sample-programs/example-programs/ex3.crf | 11 ------
 sample-programs/example-programs/ex4.crf |  9 -----
 sample-programs/example-programs/ex5.crf |  0
 sample-programs/example-programs/ex6.crf | 43 ------------------------
 sample-programs/mono-1.crf               |  2 ++
 sample-programs/mono-2.crf               |  9 +++--
 19 files changed, 8 insertions(+), 185 deletions(-)
 delete mode 100644 sample-programs/basic-0.crf
 delete mode 100644 sample-programs/basic-1.crf
 delete mode 100644 sample-programs/basic-10.crf
 delete mode 100644 sample-programs/basic-2.crf
 delete mode 100644 sample-programs/basic-3.crf
 delete mode 100644 sample-programs/basic-4.crf
 delete mode 100644 sample-programs/basic-5.crf
 delete mode 100644 sample-programs/basic-6.crf
 delete mode 100644 sample-programs/basic-7.crf
 delete mode 100644 sample-programs/basic-8.crf
 delete mode 100644 sample-programs/basic-9.crf
 delete mode 100644 sample-programs/example-programs/ex1.crf
 delete mode 100644 sample-programs/example-programs/ex2.crf
 delete mode 100644 sample-programs/example-programs/ex3.crf
 delete mode 100644 sample-programs/example-programs/ex4.crf
 delete mode 100644 sample-programs/example-programs/ex5.crf
 delete mode 100644 sample-programs/example-programs/ex6.crf

diff --git a/sample-programs/basic-0.crf b/sample-programs/basic-0.crf
deleted file mode 100644
index d9adeda..0000000
--- a/sample-programs/basic-0.crf
+++ /dev/null
@@ -1,20 +0,0 @@
-data Bool () where
-    True  : Bool ()
-    False : Bool ()
-
-not x = case x of
-    True => False
-    False => True
-
-even : Int -> Bool ()
-even x = not (odd x)
-odd x = not (even x)
-
-main = case even 64 of
-    True  => 1
-    False => 0
-
-
-
-
-
diff --git a/sample-programs/basic-1.crf b/sample-programs/basic-1.crf
deleted file mode 100644
index 59862d6..0000000
--- a/sample-programs/basic-1.crf
+++ /dev/null
@@ -1,13 +0,0 @@
-data Bool () where 
-    True  : Bool ()
-    False : Bool ()
-
-toBool x = case x of
-    0 => False
-    _ => True
-
-fromBool b = case b of
-    False => 0
-    True => 1
-
-main = fromBool (toBool 10)
diff --git a/sample-programs/basic-10.crf b/sample-programs/basic-10.crf
deleted file mode 100644
index f99e2c8..0000000
--- a/sample-programs/basic-10.crf
+++ /dev/null
@@ -1,10 +0,0 @@
-
-
-
-applyId : (forall a. a -> a) -> a -> a
-applyId f x = f x
-
-id : a -> a
-id x = x
-
-main = applyId id 4
diff --git a/sample-programs/basic-2.crf b/sample-programs/basic-2.crf
deleted file mode 100644
index 5ce4da5..0000000
--- a/sample-programs/basic-2.crf
+++ /dev/null
@@ -1,6 +0,0 @@
-add : Int -> Int -> Int ;
-add x = \y. x+y;
-
-main : Int ;
-main = (\z. z+z) ((add 4) 6) ;
-
diff --git a/sample-programs/basic-3.crf b/sample-programs/basic-3.crf
deleted file mode 100644
index 98c03b9..0000000
--- a/sample-programs/basic-3.crf
+++ /dev/null
@@ -1,2 +0,0 @@
-main : Int ;
-main = (\x. x+x+3) ((\x. x) 2) ;
diff --git a/sample-programs/basic-4.crf b/sample-programs/basic-4.crf
deleted file mode 100644
index 55ac9eb..0000000
--- a/sample-programs/basic-4.crf
+++ /dev/null
@@ -1,2 +0,0 @@
-f : Int -> Int ;
-f x = let g = (\y. y+1) in g (g x)
diff --git a/sample-programs/basic-5.crf b/sample-programs/basic-5.crf
deleted file mode 100644
index a6414f2..0000000
--- a/sample-programs/basic-5.crf
+++ /dev/null
@@ -1,8 +0,0 @@
-double : Int -> Int ;
-double n = n + n;
-
-id : forall a. a -> a ;
-id x = x ;
-
-main : Int ;
-main = id double 5;
diff --git a/sample-programs/basic-6.crf b/sample-programs/basic-6.crf
deleted file mode 100644
index ed51a1c..0000000
--- a/sample-programs/basic-6.crf
+++ /dev/null
@@ -1,15 +0,0 @@
-data Bool () where 
-    True  : Bool ()
-    False : Bool ()
-
--- Both valid
--- f : Bool () -> a -> Int
-f : Bool () -> (forall a. a -> Int)
-f b = case b of
-    False => (\x. 0 : forall a. a -> Int)
-    True  => (\x. 1 : forall a. a -> Int)
-
-
-main : Int
-main = (f True) 'h'
-
diff --git a/sample-programs/basic-7.crf b/sample-programs/basic-7.crf
deleted file mode 100644
index f0fc916..0000000
--- a/sample-programs/basic-7.crf
+++ /dev/null
@@ -1,8 +0,0 @@
-data Bool () where
-    True  : Bool ()
-    False : Bool ()
-
-ifThenElse : Bool () -> a -> a -> a
-ifThenElse b if else = case b of
-    True  => if
-    False => else
diff --git a/sample-programs/basic-8.crf b/sample-programs/basic-8.crf
deleted file mode 100644
index 958459b..0000000
--- a/sample-programs/basic-8.crf
+++ /dev/null
@@ -1,20 +0,0 @@
-data Maybe (a) where
-    Nothing : Maybe (a)
-    Just    : a -> Maybe (a)
-
-fromJust : Maybe (a) -> a
-fromJust a =
-    case a of
-        Just a => a
-
-fromMaybe : a -> Maybe (a) -> a
-fromMaybe a b =
-    case b of
-        Just a  => a
-        Nothing => a
-
-maybe : b -> (a -> b) -> Maybe (a) -> b
-maybe b f ma =
-    case ma of 
-        Just a => f a
-        Nothing => b
diff --git a/sample-programs/basic-9.crf b/sample-programs/basic-9.crf
deleted file mode 100644
index 9e76336..0000000
--- a/sample-programs/basic-9.crf
+++ /dev/null
@@ -1,10 +0,0 @@
-data List (a) where
-  Nil  : List (a)
-  Cons : a -> List (a) -> List (a)
-
-test xs = case xs of
-    Cons Nil _ => 0
-
-List a /= List (List a)
-
-a /= List a
diff --git a/sample-programs/example-programs/ex1.crf b/sample-programs/example-programs/ex1.crf
deleted file mode 100644
index c7ad3b2..0000000
--- a/sample-programs/example-programs/ex1.crf
+++ /dev/null
@@ -1 +0,0 @@
-main = 5 + 2;
\ No newline at end of file
diff --git a/sample-programs/example-programs/ex2.crf b/sample-programs/example-programs/ex2.crf
deleted file mode 100644
index 3510463..0000000
--- a/sample-programs/example-programs/ex2.crf
+++ /dev/null
@@ -1,4 +0,0 @@
-main = case 78 of {
-    5 => 45;
-    x => x + 24;
-};
\ No newline at end of file
diff --git a/sample-programs/example-programs/ex3.crf b/sample-programs/example-programs/ex3.crf
deleted file mode 100644
index 9f080ac..0000000
--- a/sample-programs/example-programs/ex3.crf
+++ /dev/null
@@ -1,11 +0,0 @@
-data Maybe () where {
-    Just : Int -> Maybe () ;
-    Nothing : Maybe () ;
-};
-
-demoFunc x = case x of {
-    Just y => y + 24;
-    Nothing => 0;
-};
-
-main = demoFunc (Just 5) ;
diff --git a/sample-programs/example-programs/ex4.crf b/sample-programs/example-programs/ex4.crf
deleted file mode 100644
index 9f412c6..0000000
--- a/sample-programs/example-programs/ex4.crf
+++ /dev/null
@@ -1,9 +0,0 @@
-data Maybe () where
-    Just : Int -> Maybe () 
-    Nothing : Maybe () 
-
-demoFunc x = case x of
-    Just x => x + 24
-    Nothing => 0
-
-main = demoFunc Nothing
diff --git a/sample-programs/example-programs/ex5.crf b/sample-programs/example-programs/ex5.crf
deleted file mode 100644
index e69de29..0000000
diff --git a/sample-programs/example-programs/ex6.crf b/sample-programs/example-programs/ex6.crf
deleted file mode 100644
index ebf8c6b..0000000
--- a/sample-programs/example-programs/ex6.crf
+++ /dev/null
@@ -1,43 +0,0 @@
-main = sum (repeat (sumlength (repeat 10 2000)) 5);
-
--- a simple list data type containing ints
-data List () where {
-    Cons : Int -> List () -> List ()
-    Nil  : List ()
-};
-
--- take the length of a list
-length : List () -> Int ;
-length x = case x of {
-    Cons _ xs => 1 + length xs ;
-    Nil => 0 ;
-};
--- sum a list
-sum : List () -> Int ; 
-sum x = case x of {
-    Cons a xs => a + sum xs ;
-    Nil => 0 ;
-};
-
--- sum + length of a list
-sumlength: List () -> Int ;
-sumlength x = sum x + length x ;
-
--- take the head of a list
-head : List () -> Int ;
-head x = case x of {
-    Cons h _ => h ;
-};
-
--- repeat an element n times
-repeat : Int -> Int -> List () ;
-repeat x n = repeatHelp Nil x n;
-repeatHelp : List () -> Int -> Int -> List () ;
-repeatHelp acc x n = case n of {
-    0 => acc ;
-    n => repeatHelp (Cons x acc) x (n + minusOne) ;
-};
-
--- represents minus one :)
-minusOne : Int ;
-minusOne = 9223372036854775807 + 9223372036854775807 + 1;
diff --git a/sample-programs/mono-1.crf b/sample-programs/mono-1.crf
index 568c674..c41e9b6 100644
--- a/sample-programs/mono-1.crf
+++ b/sample-programs/mono-1.crf
@@ -1,5 +1,7 @@
+const2 : a -> b -> a
 const2 x y = x
 
+f : a -> a
 f x = (const2 x 'c')
 
 main = f 5
diff --git a/sample-programs/mono-2.crf b/sample-programs/mono-2.crf
index 97e8c1f..76a92c2 100644
--- a/sample-programs/mono-2.crf
+++ b/sample-programs/mono-2.crf
@@ -1,13 +1,16 @@
-data Either(a b) where
-    Left: a -> Either (a b)
-    Right: b -> Either (a b)
+data Either (a b) where
+    Left  : a -> Either (a b)
+    Right : b -> Either (a b)
 
+unwrapLeft : Either (a b) -> a
 unwrapLeft x = case x of
     Left y => y
 
+unwrapRight : Either (a b) -> b
 unwrapRight x = case x of
     Right y => y
 
+wow : Either (Int Char)
 wow = Left 5
 
 main = unwrapLeft wow