{-# LANGUAGE GADTs, PartialTypeSignatures #-}

module Tests_06(runTests, boolTests) where

import Template_06(Rat(..), normaliseRat, createRat, MonoidC(..), VoteSeq(..), normaliseVote, combine)
import Test.LeanCheck
import Test.LeanCheck.Error (errorToNothing)
import Data.Tuple (swap)
import GHC.Num (integerFromInt)
import GHC.Conc (numCapabilities)
import Data.Data (isNorepType)

-- Generic Setup 
data Test = forall a. Testable a => Test String String a

runTests = flip mapM_ tests
  (\ (Test ex name t) -> putStrLn ("running " ++ ex ++ "(" ++ name ++ ")" ++ "-tests") >> checkFor 1000 t)

-- Tests for this week 

instance Listable Rat where
  tiers = cons2 Rat

eqRat (Rat x1 y1) (Rat x2 y2) = (x1,y1) == (x2,y2)
sameValue (Rat x1 y1) (Rat x2 y2) = x1 * y2 == x2 * y1
validRat (Rat _ y) = y /= 0

scaleRat s (Rat x y) = Rat (s * x) (s * y)

-- 1.1
normaliseScaleTest s r = validRat r ==> s /= 0 ==> normaliseRat (scaleRat s r) `eqRat` normaliseRat r
normaliseIdempotentTest r = validRat r ==> normaliseRat (normaliseRat r) `eqRat` normaliseRat r
normaliseValueTest r = validRat r ==> normaliseRat r `sameValue` r

-- 1.2
eqRatTest s r = validRat r ==> s /= 0 ==> scaleRat s r == r
diffRatTest1 s x y = y /= 0 ==> x /= 0 ==> s /= 1 ==> Rat (s * x) y /= Rat x y
diffRatTest2 s x y = y /= 0 ==> x /= 0 ==> s /= 1 ==> Rat x (s * y) /= Rat x y

-- 1.3
showRatTest1 s r = validRat r ==> s /= 0 ==> show (scaleRat s r) == show r
showRatTest2 r@(Rat x 1) = not $ elem '/' $ show r
showRatTest2 r@(Rat x (-1)) = not $ elem '/' $ show r
showRatTest2 _ = True
showRatTest3 r1 r2 = validRat r1 ==> validRat r2 ==> r1 == r2 ==> show r1 == show r2
showRatTest4 () = show (Rat (-4) (-1)) == "4" && show (Rat (-3) 2) == "-3/2" && show (Rat 3 (-2)) == "-3/2"

-- 1.4
ratAddComm r1 r2 = validRat r1 ==> validRat r2 ==> r1 + r2 == r2 + r1
ratAddAssoc r1 r2 r3 = validRat r1 ==> validRat r2 ==> validRat r3 ==> r1 + (r2 + r3) == (r1 + r2) + r3
ratMultComm r1 r2 = validRat r1 ==> validRat r2 ==> r1 * r2 == r2 * r1
ratMultAssoc r1 r2 r3 = validRat r1 ==> validRat r2 ==> validRat r3 ==> r1 * (r2 * r3) == (r1 * r2) * r3
ratAddZero r = validRat r ==> r + 0 == r
ratMultZero r = validRat r ==> r * 0 == 0
ratMultOne r = validRat r ==> r * 1 == r
ratAddNegate r = validRat r ==> r + negate r == 0
ratDistrib r1 r2 r3 = validRat r1 ==> validRat r2 ==> validRat r3 ==> r1 * (r2 + r3) == r1 * r2 + r1 * r3

  
newtype VoteBSeq = VSB [Bool]

toVoteSeq (VSB s) = VS (map (\ b -> if b then 'U' else 'D') s)

instance Listable VoteBSeq where
  tiers = cons1 VSB
  
instance Show VoteBSeq where
  show s = case toVoteSeq s of VS l -> "(VS " ++ show l ++ ")"


-- 2.1
monoidCBinopAssoc n m o = binop n (binop m o) == binop (binop n m) o
monoidCNeutral n = binop n neutral == n && binop neutral n == n
integerMonoidLaws :: Integer -> Integer -> Integer -> Bool
integerMonoidLaws n m o = monoidCBinopAssoc n m o && monoidCNeutral n
boolMonoidLaws :: Bool -> Bool -> Bool -> Bool
boolMonoidLaws n m o = monoidCBinopAssoc n m o && monoidCNeutral n
listMonoidLaws :: [Int] -> [Int] -> [Int] -> Bool
listMonoidLaws n m o = monoidCBinopAssoc n m o && monoidCNeutral n


-- 2.2
numToString n 
  | n < 0 = replicate (abs n) 'D'
  | otherwise = replicate n 'U'
numToVS :: Int -> VoteSeq
numToVS n = VS (numToString n)
blowUpString xs = concat $ replicate 3 "UD" ++ xs : replicate 3 "DD" ++ replicate 3 "UU"
normaliseTest n = let xs = numToString n in xs == normaliseVote (blowUpString xs)
isNormalised [] = True
isNormalised [x] = True
isNormalised (x:xs) = all (==x) xs 

-- 2.3
voteSeqEqTest n = let xs = numToString n in VS xs == VS (blowUpString xs)
voteSeqDiffTest n m = let 
    x = numToVS n 
    y = numToVS m 
  in n /= m ==> x /= y
voteSeqAdditionNormalized :: VoteBSeq -> VoteBSeq -> Bool
voteSeqAdditionNormalized x y = case binop (toVoteSeq x) (toVoteSeq y) of VS zs -> isNormalised zs
voteSeqAdditionCorrectResult n m = let
    x = numToVS n 
    y = numToVS m
    z = numToVS (n + m)
  in binop x y == z
voteSeqNeutral n = let x = numToVS n in binop x neutral == x && binop neutral x == x
voteSeqShow n = let s = blowUpString (numToString n) in
  (show (numToVS n) == show (numToString n)) && (show (VS s) == show s)

-- 2.4
combineInteger :: [Integer] -> Bool
combineInteger xs = combine xs == foldl1 (*) (1:xs)
combineBool :: [Bool] -> Bool
combineBool xs = combine xs == foldl1 (&&) (True:xs)
combineList :: [[Int]] -> Bool
combineList xs = combine xs == foldl1 (++) ([]:xs)


tests :: [Test]
tests = [
  Test "1.1" "normaliseRat (Rat (s * x) (s * y)) = normaliseRat (Rat x y)" normaliseScaleTest
  , Test "1.1" "normaliseRat (normalizeRat r) = normalizeRat r" normaliseIdempotentTest
  , Test "1.1" "normaliseRat does not change value" normaliseValueTest
  , Test "1.2" "s /= 0 ==> Rat (s * x) (s * y) == Rat x y" eqRatTest
  , Test "1.2" "s /= 1 ==> x /= 0 ==> Rat (s * x) y /= Rat x y" diffRatTest1
  , Test "1.2" "s /= 1 ==> x /= 0 ==> Rat x (s * y) /= Rat x y" diffRatTest2
  , Test "1.3" "s /= 0 ==> show (Rat (s * x) (s * y)) == show (Rat x y)" showRatTest1
  , Test "1.3" "isInteger r ==> show r does not contain /" showRatTest2
  , Test "1.3" "r1 == r2 ==> show r1 == show r2" showRatTest3
  , Test "1.3" "example invocations from exercise sheets" showRatTest4
  , Test "1.4" "r1 + r2 == r2 + r1" ratAddComm
  , Test "1.4" "r1 + (r2 + r3) == (r1 + r2) + r3" ratAddAssoc
  , Test "1.4" "r1 * r2 == r2 * r1" ratMultComm
  , Test "1.4" "r1 * (r2 * r3) == (r1 * r2) * r3" ratMultAssoc
  , Test "1.4" "r + 0 == r" ratAddZero
  , Test "1.4" "r * 0 == 0" ratMultZero
  , Test "1.4" "r * 1 == r" ratMultOne
  , Test "1.4" "r + negate r == 0" ratAddNegate
  , Test "1.4" "r1 * (r2 + r3) == r1 * r2 + r1 * r3" ratDistrib
  , Test "2.1" "monoid laws for Integer are satisfied" integerMonoidLaws
  , Test "2.1" "monoid laws for Bool are satisfied" boolMonoidLaws
  , Test "2.1" "monoid laws for [a] are satisfied" listMonoidLaws
  , Test "2.2" "normaliseVote xs doesn't contain canceling pairs" normaliseTest
  , Test "2.3" "VS xs == VS ys returns True if xs and ys represent same total vote" voteSeqEqTest
  , Test "2.3" "VS xs /= VS ys returns True if xs and ys represent different total vote" voteSeqEqTest
  , Test "2.3" "result of VoteSeq addition (binop) is normalized" voteSeqAdditionNormalized
  , Test "2.3" "result of VoteSeq addition (binop) is correct" voteSeqAdditionCorrectResult
  , Test "2.3" "x + e = e + x = x" voteSeqNeutral
  , Test "2.3" "show returns internal string representation" voteSeqShow
  , Test "2.4" "combine works correct for our Integer monoid" combineInteger
  , Test "2.4" "combine works correct for our Bool monoid" combineBool
  , Test "2.4" "combine works correct for our list monoid" combineList
  ]

boolTests :: [((String,String), Bool)]
boolTests = map (\ (Test ex n t) -> ((ex,n), holds 1000 t)) tests