-- Copyright 2022 University of Freiburg
-- Janek Spaderna <janek.spaderna@pluto.uni-freiburg.de>
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE TemplateHaskell #-}

module Ex04 where

import Test.QuickCheck

-------------------------------------------------------------------------------
-- Exercise 1 (list functions IV -- infinite lists)

iterate' :: (a -> a) -> a -> [a]
iterate' f a = a : iterate' f (f a)

prop_iter_prefix :: Fun Integer Integer -> Integer -> Int -> Bool
prop_iter_prefix f start n =
  take n (iterate' (applyFun f) start)
    == take n (iterate (applyFun f) start)

cycle' :: [a] -> [a]
cycle' as = asCycled
  where
    asCycled = as ++ asCycled

prop_cycle_prefix :: Integer -> [Integer] -> Int -> Bool
prop_cycle_prefix x xs n =
  -- `cycle` only behaves correctly for non-empty lists.
  take n (cycle (x : xs))
    == take n (cycle' (x : xs))

-- Alternative definitions that don't fit the exercise
-- ===================================================
--
-- cycle as = as ++ cycle as
-- -------------------------
--
-- Does not result in a cyclic data structure.
--
--
-- ... where asCycled = asCycled ++ as
-- -----------------------------------
--
-- Can never produce a single value.

-------------------------------------------------------------------------------
-- Exercise 2 (folding & laziness)

-- 1. `foldr` can work on finite and infinite lists, `foldl` can only work on
--    finite list.
--
--    `foldl` has to recurse through the whole list before evaluating any
--    applications of the accumulator function.
--
--    `foldr` evaluates the accumulator function on the first (:)-cell. Its
--    second argument is the unevaluated recursion through the list.

nilEx2 :: ()
nilEx2 = ()

fEx2 :: Integer -> () -> ()
fEx2 _ _ = ()

terminatingEx2 :: ()
terminatingEx2 = foldr fEx2 nilEx2 [0 ..]

-- 2. Without any machinery to force evaluation of intermediate sums, both
--    `foldl (+) 0 nums` and `foldr (+) 0 nums` build a sequence of `n` nested
--    calls to the (+) operator, one left associative, one right associative.
--
--    This is called a space leak.

-------------------------------------------------------------------------------
-- Exercise 3 (vectors)

data Vec = Vec Double Double

instance Eq Vec where
  Vec x1 y1 == Vec x2 y2 = x1 == x2 && y1 == y2

instance Show Vec where
  show (Vec x y) = "Vec " ++ show x ++ " " ++ show y

instance Num Vec where
  Vec x1 y1 + Vec x2 y2 = Vec (x1 + x2) (y1 + y2)
  Vec x1 y1 * Vec x2 y2 = Vec (x1 * x2) (y1 * y2)
  abs (Vec x y) = Vec (abs x) (abs y)
  signum (Vec x y) = Vec (signum x) (signum y)
  fromInteger i = Vec (fromInteger i) (fromInteger i)
  negate (Vec x y) = Vec (negate x) (negate y)

-------------------------------------------------------------------------------
-- Exercise 4 (monoids)

data Sum = Sum Integer
  deriving (Eq)

instance Semigroup Sum where
  Sum x <> Sum y = Sum (x + y)

instance Monoid Sum where
  mempty = Sum 0

prop_sum_assoc :: Integer -> Integer -> Integer -> Bool
prop_sum_assoc x y z =
  Sum x <> (Sum y <> Sum z) == (Sum x <> Sum y) <> Sum z

prop_sum_left_id :: Integer -> Bool
prop_sum_left_id x = mempty <> Sum x == Sum x

prop_sum_right_id :: Integer -> Bool
prop_sum_right_id x = Sum x <> mempty == Sum x

data Product = Product Integer
  deriving (Eq)

instance Semigroup Product where
  Product x <> Product y = Product (x * y)

instance Monoid Product where
  mempty = Product 1

prop_product_assoc :: Integer -> Integer -> Integer -> Bool
prop_product_assoc x y z =
  Product x <> (Product y <> Product z) == (Product x <> Product y) <> Product z

prop_product_left_id :: Integer -> Bool
prop_product_left_id x = mempty <> Product x == Product x

prop_product_right_id :: Integer -> Bool
prop_product_right_id x = Product x <> mempty == Product x

foldMap' :: Monoid m => (a -> m) -> [a] -> m
foldMap' _ [] = mempty
foldMap' f (a : as) = f a <> foldMap' f as

foldMap'foldr :: Monoid m => (a -> m) -> [a] -> m
foldMap'foldr f = foldr (\a m -> f a <> m) mempty

sum' :: [Integer] -> Integer
sum' xs = result
  where
    Sum result = foldMap' Sum xs

product' :: [Integer] -> Integer
product' xs = result
  where
    Product result = foldMap' Product xs

prop_empty_sum :: Bool
prop_empty_sum = sum' [] == 0

prop_little_gauss :: Integer -> Property
prop_little_gauss n = n >= 0 ==> sum' [1 .. n] == n * (n + 1) `div` 2

prop_empty_product :: Bool
prop_empty_product = product' [] == 1

prop_product :: [Integer] -> Bool
prop_product xs = product xs == product' xs

-------------------------------------------------------------------------------
-------------------------------------------------------------------------------

return []

checkAll :: IO Bool
checkAll = $quickCheckAll