-- Applicative Symantics

-- The language of meaning: First-order predicate logic

module Logic where

import Control.Applicative

-- Logical types
data E
data T

type VarName = String

class Logic r where
    john'    :: r E
    mary'    :: r E
    left'    :: r (E -> T)
    ignored' :: r (E -> E -> T)
    woman'   :: r (E -> T)
    man'     :: r (E -> T)
    conj'    :: r (T -> T -> T)
    impl'    :: r (T -> T -> T)
    dot'     :: r (T -> T)
    app      :: r (a -> b) -> r a -> r b

    ind      :: VarName -> r E
    exists   :: (VarName, r T) -> r T
    forall   :: (VarName, r T) -> r T

-- A bit of syntactic sugar
conj a b = (conj' `app` a) `app` b
impl a b = (impl' `app` a) `app` b

-- Lifting to any applicative

newtype A i r a = A{unA :: i (r a)}
instance (Applicative i, Logic r) => Logic (A i r) where
    john'    = A $ pure john'
    mary'    = A $ pure mary'
    left'    = A $ pure left'
    ignored' = A $ pure ignored'
    woman'   = A $ pure woman'
    man'     = A $ pure man'
    dot'     = A $ pure dot'
    conj'    = A $ pure conj'
    impl'    = A $ pure impl'
    ind v    = A $ pure (ind v)
    exists (v, A e) = A ( (\x -> (exists (v,x))) <$> e)
    forall (v, A e) = A ( (\x -> (forall (v,x))) <$> e)
    app (A x) (A y) = A (app <$> x <*> y)


-- We now interpret Logic terms as Strings, so we can show
-- our formulas.
-- Actually, not quite strings: we need a bit of _context_:
-- the precedence, to make the formulas look prettier.

data SL a = SL { unSL :: Int -> String }
instance Logic SL where
  john'            = SL (\_ -> "john'")
  mary'            = SL (\_ -> "mary'")
  left'            = SL (\_ -> "left'")
  ignored'         = SL (\_ -> "ignore'")
  woman'           = SL (\_ -> "woman'")
  man'             = SL (\_ -> "man'")

  dot'             = SL (\_ -> "") -- XXX check well-formedness/scope

  conj'            = SL (\_ -> "conj")
  impl'            = SL (\_ -> "impl")

  ind v            = SL (\_ -> v)
  exists (v,SL e)  = SL (\p -> paren (p>10) ("E " ++ v ++ "." ++ e 11))
  forall (v,SL e)  = SL (\p -> paren (p>10) ("U " ++ v ++ "." ++ e 11))

  app (SL f) (SL x)  = SL (\p -> paren (p > 10) (f 10 ++ " " ++ x 11))

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

tl1 = left' `app` mary' :: SL T
-- left' mary'