From 3a9793f9134fe29a669298c33386b649d2fbb29c Mon Sep 17 00:00:00 2001
From: Nilstrieb <nilstrieb@gmail.com>
Date: Fri, 9 Jul 2021 14:07:50 +0200
Subject: [PATCH] lets go

---
 chapter4/Types.idr | 92 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 92 insertions(+)
 create mode 100644 chapter4/Types.idr

diff --git a/chapter4/Types.idr b/chapter4/Types.idr
new file mode 100644
index 0000000..6ed2e37
--- /dev/null
+++ b/chapter4/Types.idr
@@ -0,0 +1,92 @@
+module Types
+
+data Direction = North
+                | East
+                | South
+                | West
+
+turnClockwise : Direction -> Direction
+turnClockwise North = East
+turnClockwise East = South
+turnClockwise South = West
+turnClockwise West = North
+
+
+||| Represents shapes
+data Shape = ||| A triangle, with its base length and height
+              Triangle Double Double
+            |  ||| A Rectangle, with its length and height
+              Rectangle Double Double
+            | ||| A circle, with its radius
+              Circle Double
+
+%name Shape shape, shape1, shape2
+
+area : Shape -> Double
+area (Triangle base height) = base * height * 0.5
+area (Rectangle length height) = length * height
+area (Circle radius) = pi * radius * radius
+
+data Picture = Primitive Shape
+              | Combine Picture Picture
+              | Rotate Double Picture
+              | Translate Double Double Picture
+
+%name Picture pic, pic1, pic2
+
+rectangle : Picture
+rectangle = Primitive (Rectangle 20 10)
+circle : Picture
+circle = Primitive (Circle 5)
+triangle : Picture
+triangle = Primitive (Triangle 10 10)
+testPicture : Picture 
+testPicture = Combine (Translate 5 5 rectangle)
+              (Combine (Translate 35 5 circle)
+              (Translate 15 25 triangle))
+
+
+pictureArea : Picture -> Double
+pictureArea (Primitive shape) = area shape
+pictureArea (Combine pic pic1) = pictureArea pic + pictureArea pic1
+pictureArea (Rotate x pic) = pictureArea pic
+pictureArea (Translate x y pic) = pictureArea pic
+
+data Biggest = NoTriangle | Size Double
+
+biggestTriangle : Picture -> Maybe Double
+biggestTriangle (Primitive triangle@(Triangle x y)) = Just (area triangle)
+biggestTriangle (Combine pic pic1) = case (biggestTriangle pic) of
+                                      Nothing => biggestTriangle pic1
+                                      (Just size) => case (biggestTriangle pic1) of
+                                        Nothing => Just size
+                                        Just size1 => Just (max size size1)
+biggestTriangle (Rotate x pic) = biggestTriangle pic
+biggestTriangle (Translate x y pic) = biggestTriangle pic
+biggestTriangle _ = Nothing
+
+safeDivide : Double -> Double -> Maybe Double
+safeDivide x y = if y == 0 then Nothing
+                            else Just (x / y)
+
+
+-- Binary Trees
+data BSTree : Type -> Type where
+      Empty : Ord elem => BSTree elem
+      Node : Ord elem => (left: BSTree elem) -> (val : elem) -> (right : BSTree elem) -> BSTree elem
+
+%name BSTree tree, tree1
+
+insert : elem -> BSTree elem -> BSTree elem
+insert x Empty = Node Empty x Empty
+insert x orig@(Node left val right) = case compare x val of
+                                      LT => Node (insert x left) val right
+                                      EQ => orig
+                                      GT => Node left val (insert x right)
+
+listToTree : Ord elem => List elem -> BSTree elem
+listToTree xs = listToTreeInner xs Empty
+  where
+    listToTreeInner : List elem -> BSTree elem -> BSTree elem
+    listToTreeInner [] tree = tree
+    listToTreeInner (x :: xs) tree = insert x (listToTreeInner xs tree)