-- # Software Tools for Discrete Mathematics
module Stdm11Functions where

import Stdm06LogicOperators
import Stdm08SetTheory
import Stdm10Relations

-- # Chapter 11.  Functions

-- This is the type of image of input under f.
data FunVals a = Undefined | Value a
  deriving (Eq, Show)

-- | This is Fun!
-- >>> isFun [1,2,3] [4,5,6] [(1,Value 4),(2,Value 5),(3,Value 6)]
-- True

-- | This is not Fun...
-- >>> isFun [1,2,3] [4,5,6] [(1,Value 4),(1,Value 5),(1,Value 6)]
-- False
isFun ::
  (Eq a, Eq b, Show a, Show b) =>
  Set a ->
  Set b ->
  Set (a, FunVals b) ->
  Bool
isFun f_domain f_codomain fun =
  let actual_domain = domain fun
   in normalForm actual_domain
        /\ setEq actual_domain f_domain

-- |
-- >>> isPartialFunction [1,2,3] [2,3] [(1,Value 2),(2,Value 3),(3,Undefined)]
-- True

-- |
-- >>> isPartialFunction [1,2] [2,3] [(1,Value 2),(2,Value 3)]
-- False
isPartialFunction ::
  (Eq a, Eq b, Show a, Show b) =>
  Set a ->
  Set b ->
  Set (a, FunVals b) ->
  Bool
isPartialFunction f_domain f_codomain fun =
  isFun f_domain f_codomain fun
    /\ elem Undefined (codomain fun)

-- Some functions to compose below:
fun1 = [(1, Value 2), (3, Value 6), (3, Value 5)]
fun2 = [(2, Value 4), (6, Value 9), (7, Value 10)]

-- |
-- >>> functionalComposition fun1 fun2
-- [(1,Value 4),(3,Value 9)]
functionalComposition ::
  (Eq a, Eq b, Eq c, Show a, Show b, Show c) =>
  Set (a, FunVals b) ->
  Set (b, FunVals c) ->
  Set (a, FunVals c)
functionalComposition f1 f2 =
  normalizeSet [(a, c) | (a, Value b) <- f1, (b', c) <- f2, b == b']

-- | Helper for isSurjective
-- >>> imageValues (codomain [(1, Value 4), (2, Value 5), (3, Value 4)])
-- [4,5,4]
imageValues :: (Eq a, Show a) => Set (FunVals a) -> Set a
imageValues f_codomain = [v | (Value v) <- f_codomain]

-- |
-- >>> isSurjective [1,2,3] [4,5] [(1, Value 4), (2, Value 5), (3, Value 4)]
-- True

-- |
-- >>> isSurjective [1,2,3] [4,5] [(1, Value 4), (2, Value 4), (3, Value 4)]
-- False
isSurjective ::
  (Eq a, Eq b, Show a, Show b) =>
  Set a ->
  Set b ->
  Set (a, FunVals b) ->
  Bool
isSurjective f_domain f_codomain fun =
  isFun f_domain f_codomain fun
    /\ setEq f_codomain (normalizeSet (imageValues (codomain fun)))

-- |
-- >>> isInjective [1,2,3] [2,4] [(1,Value 2),(2,Value 4),(3,Value 2)]
-- False

-- |
-- >>> isInjective [1,2,3] [2,3,4] [(1,Value 2),(2,Value 4),(3,Undefined)]
-- True
isInjective ::
  (Eq a, Eq b, Show a, Show b) =>
  Set a ->
  Set b ->
  Set (a, FunVals b) ->
  Bool
isInjective f_domain f_codomain fun =
  let fun_image = imageValues (codomain fun)
   in isFun f_domain f_codomain fun
        /\ normalForm fun_image

-- |
-- >>> isBijective [1,2] [3,4] [(1,Value 3),(2,Value 4)]
-- True

-- |
-- >>> isBijective [1,2] [3,4] [(1,Value 3),(2,Value 3)]
-- False
isBijective ::
  (Eq a, Eq b, Show a, Show b) =>
  Set a ->
  Set b ->
  Set (a, FunVals b) ->
  Bool
isBijective f_domain f_codomain fun =
  isSurjective f_domain f_codomain fun
    /\ isInjective f_domain f_codomain fun

-- |
-- >>> isPermutation [1,2,3] [1,2,3] [(1,Value 2),(2, Value 3),(3, Undefined)]
-- False

-- |
-- >>> isPermutation [1,2,3] [1,2,3] [(1,Value 2),(2, Value 3),(3, Value 1)]
-- True
isPermutation ::
  (Eq a, Show a) => Set a -> Set a -> Set (a, FunVals a) -> Bool
isPermutation f_domain f_codomain fun =
  isBijective f_domain f_codomain fun
    /\ setEq f_domain f_codomain

-- Real numbers countable?

diagonal :: Int -> [(Int, Int)] -> [(Int, Int)]
diagonal stop rest =
  let interval = [1 .. stop]
   in zip interval (reverse interval) ++ rest

-- |
-- >>>
-- 
rationals :: [(Int, Int)]
rationals = foldr diagonal [] [1 ..]