-- # Software Tools for Discrete Mathematics
module Stdm11Functions where

import Stdm06LogicOperators
import Stdm08SetTheory
import Stdm10Relations

-- # Chapter 11.  Functions
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

data FunVals a = Undefined | Value a
  deriving (Eq, Show)

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)

imageValues :: (Eq a, Show a) => Set (FunVals a) -> Set a
imageValues f_codomain =
  [v | (Value v) <- f_codomain]

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 ::
  (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

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']

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 ::
  (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

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 ..]