module Karttunen1 where

import Finite
import Pretty

-- There are three individuals in the domain: Alice, Bob, and Carol.
data E = Alice | Bob | Carol
    deriving (Eq, Ord, Enum, Bounded, Show, Read)
instance Finite E where
    everything = enumEverything
    cardinality = enumCardinality
instance Pretty E

-- Because we are only concerned with the seeing relation, we simply take
-- a possible world to be a set of seer-seen pairs.
type World = E -> E -> Bool

-- A proposition is a set of possible worlds.
type Prop = World -> Bool

-- The transitive verb "saw" takes two arguments: the seen and the seer.
saw :: World -> E -> E -> Bool
saw w seen seer = w seer seen

-- Karttunen's extension for the question "Who did Alice see?": the set of
-- true answers.
q :: World -> Prop -> Bool
q w p = p w && (p == (\w' -> saw w' Alice Alice) ||
                p == (\w' -> saw w' Bob   Alice) ||
                p == (\w' -> saw w' Carol Alice))

-- The real world.
reality :: World
reality seer seen = seer == Alice && seen == Alice ||
                    seer == Alice && seen == Bob   ||
                    seer == Bob   && seen == Bob   ||
                    seer == Bob   && seen == Carol