-- D. Sannella. M Fourman, H. Peng and P. Wadler
-- Introduction to Computation: Haskell, Logic and Automata
-- Undergraduate Topics in Computer Science, Springer (2021)
-- ISBN 978-3-030-76907

-- Chapter 18 : Relations and Quantifiers

module Chap18_relations_and_quantifiers where

import Chap06_features_and_predicates (Thing (R, S, T, U, V, W, X, Y, Z), things, Predicate, isDisc, isTriangle, isWhite, isBlack, isGrey, isBig, isSmall)

import Chap14_sequent_calculus (neg, (&:&), (|:|))

-- Expressing logical statements

discsThatArentBlackAreEitherBigOrNotWhite =
  and [ (isBig |:| neg isWhite) x | x <- things, (isDisc &:& neg isBlack) x ]

-- Quantifiers

every :: [u] -> Predicate u -> Bool
every xs p = and [ p x | x <- xs ]

some :: [u] -> Predicate u -> Bool
some xs p = or [ p x | x <- xs ]

everyWhiteTriangleIsSmall = every (filter (isWhite &:& isTriangle) things) isSmall

everyDiscThatIsntBlackIsEitherBigOrNotWhite =
  every (filter (isDisc &:& neg isBlack) things)
        (isBig |:| neg isWhite)

someBigTriangleIsGrey = some (filter (isBig &:& isTriangle) things) isGrey

-- Relations

isBigger :: Thing -> Thing -> Bool
isBigger x y = isBig x && isSmall y


isAbove :: Thing -> Thing -> Bool
isAbove R _ = False
isAbove S x = x `elem` [R,U,V,X,Y]
isAbove T x = x `elem` [R,U,X,Y]
isAbove U x = x `elem` [R,X,Y]
isAbove V x = x `elem` [R,X,Y]
isAbove W x = x `elem` [R,X,Y]
isAbove X x = False
isAbove Y x = False
isAbove Z x = x `elem` [R,X,Y]

type Relation u = u -> u -> Bool

sIsAboveEveryBlackTriangle = every (filter (isBlack &:& isTriangle) things) (S `isAbove`)

everyWhiteDiscIsAboveX = every (filter (isWhite &:& isDisc) things) (`isAbove` X)

blackTriangles :: [Thing]
blackTriangles = filter (isBlack &:& isTriangle) things
greyDiscs :: [Thing]
greyDiscs = filter (isGrey &:& isDisc) things

everyBlackTriangleIsAboveEveryGreyDisc = every blackTriangles (\x -> every greyDiscs (x `isAbove`))

isAboveEveryGreyDisc :: Predicate Thing
isAboveEveryGreyDisc x = every greyDiscs (x `isAbove`)

everyBlackTriangleIsAboveEveryGreyDisc' = every blackTriangles isAboveEveryGreyDisc

bigBlackTriangles :: [Thing]
bigBlackTriangles =
  filter (isBig &:& isBlack &:& isTriangle) things

everyBigBlackTriangleIsAboveEveryGreyDisc = every bigBlackTriangles isAboveEveryGreyDisc

-- Another universe

data Person = Angela | Ben | Claudia | Diana | Emilia
                     | Fangkai | Gavin | Hao | Iain
people :: [Person]
people = [Angela, Ben, Claudia, Diana, Emilia,
                  Fangkai, Gavin, Hao, Iain]

loves :: Relation Person
Angela `loves` Ben = True
Angela `loves` _ = False
Ben `loves` Gavin = True
Ben `loves` _ = False
Claudia `loves` Angela = True
Claudia `loves` Ben = True
Claudia `loves` _ = False
Diana `loves` Hao = True
Diana `loves` Iain = True
Diana `loves` _ = False
Emilia `loves` Fangkai = True
Emilia `loves` _ = False
Fangkai `loves` Diana = True
Fangkai `loves` _ = False
Gavin `loves` Fangkai = True
Gavin `loves` _ = False
Hao `loves` Diana = True
Hao `loves` Fangkai = True
Hao `loves` _ = False
Iain `loves` Emilia = True
Iain `loves` _ = False

angelaLovesSomebody = some people (Angela `loves`)

everybodyLovesBen = every people (`loves` Ben)

somebodyLovesThemself = some people (\x -> x `loves` x)

somebodyLovesSomebodyWhoLovesThem = some people (\x -> some people (\y -> x `loves` y && y `loves` x))

-- Dependencies

forEveryPersonThereIsSomePersonWhoTheyLove = every people (\y -> some people (y `loves`))

thereIsSomePersonWhoEverybodyLoves = some people (\x -> every people (`loves` x))