{-# OPTIONS -W #-}
{-# LANGUAGE TypeFamilies, FlexibleContexts, NoMonomorphismRestriction #-}

module Lambda.Semantics where

-- | Here we encode the "target language", the language
-- to express denotations (or, meanings)
-- Following Montague, our language for denotations
-- is essentially Church's "Simple Theory of Types"
-- also known as simply-typed lambda-calculus
-- It is a form of a higher-order predicate logic.
--
data Entity = John | Mary
  deriving (Eq, Show)

-- | We define the grammar of the target language the same way
-- we have defined the grammar for (source) fragment
--
class Lambda lrepr where
  john'  :: lrepr Entity
  mary'  :: lrepr Entity
  like'  :: lrepr (Entity -> Entity -> Bool)
  own'   :: lrepr (Entity -> Entity -> Bool)
  farmer':: lrepr (Entity -> Bool)
  donkey':: lrepr (Entity -> Bool)

  true   :: lrepr Bool
  neg    :: lrepr Bool -> lrepr Bool
  conj   :: lrepr Bool -> lrepr Bool -> lrepr Bool
  exists :: lrepr ((Entity -> Bool) -> Bool)

  app    :: lrepr (a -> b) -> lrepr a -> lrepr b
  lam    :: (lrepr a -> lrepr b) -> lrepr (a -> b)

-- Examples
lsen1 = neg (conj (neg (neg true)) (neg true))
lsen2 = lam (\x -> neg x) 
lsen3 = app (lam (\x -> neg x)) true

disj x y = neg (conj (neg x) (neg y))
-- disj true (neg true)
ldisj = lam (\x -> lam (\y -> disj x y))
lsen4  = disj true (neg true)
lsen4' = app (app ldisj true) (neg true)

lsen5 = app exists (lam (\x -> app (app like' mary') x))


-- | Syntactic sugar
exists_ r = lam (\p ->      app exists
                            (lam (\x -> conj (app r x)      (app p x) )) )
forall_ r = lam (\p -> neg (app exists
                            (lam (\x -> conj (app r x) (neg (app p x))))))
forall = forall_ (lam (\_ -> true))


-- | The first interpretation: evaluating in the world with John, Mary,
-- and Bool as truth values.
-- Lambda functions are interpreted as Haskell functions and Lambda
-- applications are interpreted as Haskell applications.
-- The interpreter R is metacircular (and so, efficient).
--
data R a = R { unR :: a }
instance Lambda R where
  john'                  = R John
  mary'                  = R Mary
  like'                  = R (\o s -> elem (s,o) [(John,Mary), (Mary,John)])
  own'                   = R (\o s -> elem (s,o) [(Mary,John)])
  farmer'                = R (\s -> s == Mary)
  donkey'                = R (\s -> s == John)

  true                   = R True
  neg (R True)           = R False
  neg (R False)          = R True
  conj (R True) (R True) = R True
  conj _        _        = R False
  exists                 = R (\f -> any f domain)

  app (R f) (R x)        = R (f x)
  lam f                  = R (\x -> unR (f (R x)))


domain = [John, Mary]

instance (Show a) => Show (R a) where
  show (R x) = show x


-- | "Running" the examples
lsen1_r = lsen1 :: R Bool
lsen2_r = lsen2 :: R (Bool -> Bool)
lsen3_r = lsen3 :: R Bool

ldisj_r  = ldisj  :: R (Bool -> Bool -> Bool)

lsen4_r  = lsen4  :: R Bool
lsen4'_r = lsen4' :: R Bool

lsen5_r = lsen5   :: R Bool

-- | We now interpret Lambda terms as Strings, so we can show
-- our formulas.
-- Actually, not quite strings: we need a bit of _context_:
-- the precedence and the number of variables already bound in the context.
-- The latter number lets us generate unique variable names.
--
data C a = C { unC :: Int -> Int -> String }
instance Lambda C where
  john'            = C (\_ _ -> "john'")
  mary'            = C (\_ _ -> "mary'")
  like'            = C (\_ _ -> "like'")
  own'             = C (\_ _ -> "own'")
  farmer'          = C (\_ _ -> "farmer'")
  donkey'          = C (\_ _ -> "donkey'")

  true             = C (\_ _ -> "T")
  neg (C x)        = C (\i p -> paren (p > 10) ("-" ++ x i 11))
  conj (C x) (C y) = C (\i p -> paren (p > 3) (x i 4 ++ " & " ++ y i 3))
  exists           = C (\_ _ -> "E")

  app (C f) (C x)  = C (\i p -> paren (p > 10) (f i 10 ++ " " ++ x i 11))
  lam f            = C (\i p -> let x    = "x" ++ show i
                                    body = unC (f (C (\_ _ -> x))) (i + 1) 0
                                in paren (p > 0) ("L" ++ x ++ ". " ++ body))

instance Show (C a) where
  show (C x) = x 1 0
paren True  text = "(" ++ text ++ ")"
paren False text = text

-- | We can now see the examples
--
lsen1_c = lsen1 :: C Bool
lsen2_c = lsen2 :: C (Bool -> Bool)
lsen3_c = lsen3 :: C Bool

ldisj_c  = ldisj  :: C (Bool -> Bool -> Bool)

-- | The displayed difference between lsen4 and lsen4'
-- shows that beta-redices have been reduced. NBE.
lsen4_c  = lsen4  :: C Bool
lsen4'_c = lsen4' :: C Bool

lsen5_c = lsen5   :: C Bool


-- | Normalizing the terms: performing the apparent redices
--
type family Known (lrepr :: * -> *) (a :: *)
type instance Known lrepr (a -> b) = P lrepr a -> P lrepr b
type instance Known lrepr Bool     = [lrepr Bool]
data P lrepr a = P { unP :: lrepr a, known :: Maybe (Known lrepr a) }

instance (Lambda lrepr) => Lambda (P lrepr) where
  john'                      = unknown john'
  mary'                      = unknown mary'
  like'                      = unknown like'
  own'                       = unknown own'
  farmer'                    = unknown farmer'
  donkey'                    = unknown donkey'

  true                       = P true (Just [])
  neg (P x _)                = unknown (neg x)
  conj x (P _ (Just []))     = x
  conj x y                   = let conjuncts (P _ (Just zs)) = zs
                                   conjuncts (P z Nothing) = [z]
                               in P (foldr conj (unP y) (conjuncts x))
                                    (Just (conjuncts x ++ conjuncts y))
  exists                     = unknown exists

  app (P _ (Just f)) x       = f x
  app (P f Nothing ) (P x _) = unknown (app f x)
  lam f                      = P (lam (\x -> unP (f (unknown x)))) (Just f)


instance (Show (lrepr a)) => Show (P lrepr a) where
  show (P x _) = show x
unknown x = P x Nothing

-- | Now we can see beautified terms
--
lsen1_pc = lsen1 :: (P C) Bool
lsen2_pc = lsen2 :: (P C) (Bool -> Bool)
lsen3_pc = lsen3 :: (P C) Bool

ldisj_pc  = ldisj  :: (P C) (Bool -> Bool -> Bool)

-- | There is no longer difference between lsen4 and lsen4'
lsen4_pc  = lsen4  :: (P C) Bool
lsen4'_pc = lsen4' :: (P C) Bool

lsen5_pc = lsen5   :: (P C) Bool