{-# LANGUAGE TypeFamilies, TypeOperators, NoMonomorphismRestriction #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
{-# LANGUAGE OverlappingInstances #-}

-- Applicative Symantics: Syntax-semantics interface

module Sem where

import Abstract
import Logic
import Control.Applicative
import Applicatives


-- Interpreting Abstract as Logic

newtype Sem r a = Sem (SemT r a)

-- Mapping of types

type family SemT (r :: * -> *) a :: *
type instance SemT r NP = r E
type instance SemT r CN = (r E -> r T)
type instance SemT r S  = r T
type instance SemT r M  = r T
type instance SemT r (a :-> b) = SemT r a -> SemT r b

-- ------------------------------------------------------------------------
-- Basic semantics
-- Interpreting Abstract language as Logic

instance Logic r => Abstract (Sem r) where
    john    = Sem john'
    mary    = Sem mary'
    left    = Sem $ app left'
    ignored = Sem $ \obj subj -> (ignored' `app` subj) `app` obj
    woman   = Sem $ app woman'
    dot     = Sem $ app dot'
    Sem x <#> Sem y = Sem (x y)

-- General implementation of the conjunction
instance Logic r => ACnj (Sem r) where
    and  = Sem $ conj

-- Only matrix sentences can be given meaning
runSem :: Logic r => Sem r M -> r T
runSem (Sem x) = x

-- Simple test

-- "Mary left."
t01Sem = runSem t01 :: SL T
--  (left' mary')

-- "John ignored Mary."
t02Sem = runSem t02 :: SL T
-- (ignore' john' mary')

-- "John ignored Mary and Mary left."
t03Sem = runSem t03 :: SL T
--  (conj (ignore' john' mary') (left' mary'))

-- ------------------------------------------------------------------------
-- Anaphora: interpreted in Dynamic Logic
-- Only Entities can be referred to by pronouns (at least for now)

-- Add two constants to Logic so it becomes Dynamic Logic
class DynLogic r where
    update :: r E -> r E
    select :: r E

    -- Don't seem to need:
    -- local_update :: Gender -> r E -> r E -> r E

-- Implement later:
-- data Gender = Fem | Mas | Neu

newtype DL r a = DL (r a) deriving DynLogic

instance (Logic r, DynLogic r) => APro (Sem r) where
    she = Sem select

-- Stash away individuals so they could be referred to later
instance (Logic r, DynLogic r) => Logic (DL r) where
    john'    = DL (update john')
    mary'    = DL (update mary')
    left'    = DL left'
    ignored' = DL ignored'
    woman'   = DL (woman')  -- Later on, put gender
    dot'     = DL dot'
    conj'    = DL conj'
    impl'    = DL impl'
    ind v    = DL (update (ind v))
    exists (v,DL x) = DL (exists (v,x))
    forall (v,DL x) = DL (forall (v,x))
    app (DL x) (DL y) = DL (app x y)

{-
-- In case gender, projection is decided syntactically,
-- at the A stage
newtype SemAn r a = SemAn (r (SemT a))

instance (Logic r, DynLogic r) => Abstract (SemAn r) where
    mary = SemAn (update Mas mary')
    left = SemAn left'
    and  = SemAn conj
    dot  = SemAn dot'
    SemAn x <#> SemAn y = SemAn (app' x y)
-}

-- implementation of DynLogic

-- type AnState r = [(Gender, r E)]
type AnState r = [r E]

-- NB: Partiality
instance Logic r => DynLogic (A (State (AnState r)) r) where
    update (A (State x)) = A $ State (\s -> let (ra, s') = x s
					    in (ra, (ra:s')))
    select = A $ State (\s -> case s of
			       (h:_) -> (h,s)
			       _     -> error "Pronoun not bound")

runAn :: Logic r => (DL (A (State (AnState r)) r)) T -> r T
runAn (DL (A x)) = fst $ unState x []

-- NB: composition of languages in the inferred type
runSAn :: Logic r => Sem (DL (A (State (AnState r)) r)) M -> r T
runSAn x = runAn . runSem $ x

-- NB: partiality

tp1Sem = runSAn tp1 :: SL T
-- "she left."
-- *** Exception: Pronoun not bound

tp2Sem = runSAn tp2 :: SL T
-- "John ignored Mary and she left."
-- (conj (ignore' john' mary') (left' mary'))

-- ------------------------------------------------------------------------
-- Quantification

-- Quantification applicative (for details, see the implementation below)
type Quan r = A (CPSA GenVarSt (r T)) r

data QSel = QExists | QForall

-- Lift through DynLogic: Quan is above DynLogic
instance (Logic r, DynLogic r) => DynLogic (Quan r) where
    update (A e) = A (update <$> e)
    select       = A (pure select)

instance Logic r => AInd (Sem (Quan r)) where
    a = Sem $ quan QExists

runCPS :: Logic r => (Quan r) T -> r T
runCPS (A (CPSA x)) = x (\v _ -> v) ("v",0)

-- NB: Check the inferred type
runSEAn x = runAn . runCPS . runSem $ x

-- "a woman left."
tq1Sem_e = runSEAn tq1 :: SL T
-- E v0.(conj (woman' v0) ( (left' v0)))


-- Implementation
type GenVarSt = (String,Int)
newvar :: GenVarSt -> (VarName,GenVarSt)
newvar (prefix,cnt) = (prefix ++ show cnt, (prefix, cnt + 1))

quan :: Logic r => QSel -> (Quan r E -> Quan r T) -> (Quan r) E
quan qsel = \cn -> A . CPSA $ \k s ->
	let (vn,s') = newvar s
            var     = ind vn
	in unCPSA (unA (cn (A (pure var)))) 
	        (\cnv s' -> 
		 case qsel of
		 QExists -> exists (vn,conj cnv (k var s'))
		 QForall -> forall (vn,impl cnv (k var s'))
		) s'

-- ------------------------------------------------------------------------
-- Two levels of quantification: existentials and universals
-- (existential is above, the universal is underneath)

-- The most straightforward description of layering
type Quan2 r = Quan (Quan r)

instance Logic r => AInd (Sem (Quan2 r)) where
    a = Sem $ quan QExists

instance Logic r => AEvr (Sem (Quan2 r)) where
    every = Sem $ quan2 QForall 

-- conj creates an island for the universal
instance Logic r => ACnj (Sem (Quan2 r)) where
    and = Sem $ \(A x) (A y) -> A $ conj_reset <$> x <*> y

conj_reset :: Logic r => Quan r T -> Quan r T -> Quan r T
conj_reset (A x) (A y) = conj (A (reset x)) (A (reset y))

run2CPS :: Logic r => (Quan2 r) T -> r T
run2CPS (A (CPSA x)) = 
    let (A (CPSA after_ex)) = x (\v _ -> v) ("ve",0)
    in  after_ex (\v _ -> v) ("vu",0)

-- NB: Check the inferred type
runSEUAn x = runAn . run2CPS . runSem $ x

-- "a woman left."
tq1Sem = runSEUAn tq1 :: SL T
-- E ve0.(conj (woman' ve0) ( (left' ve0)))

-- "every woman left."
tq2Sem = runSEUAn tq2 :: SL T
-- U vu0.(impl (woman' vu0) ( (left' vu0)))


-- NB: notice the scope of the quantification!
-- "John left and every woman left."
tq3Sem = runSEUAn tq3 :: SL T
-- (conj (left' john') (U vu0.(impl (woman' vu0) (left' vu0))))

-- "John ignored a woman and she left."
tqp1Sem = runSEUAn tqp1 :: SL T
-- E ve0.(conj (woman' ve0) ( (conj (ignore' john' ve0) (left' ve0))))

-- I didn't implement the scope extrusion check, just to see the
-- bad formula. Doesn't the result look odd?
-- "John ignored every woman and she left."
tqp2Sem = runSEUAn tqp2 :: SL T
--  (conj (U vu0.(impl (woman' vu0) (ignore' john' vu0))) (left' vu0))


quan2 :: Logic r =>
	QSel -> (Quan (Quan r) E -> Quan (Quan r) T) -> (Quan (Quan r)) E
quan2 qsel cn = A (pure (quan qsel cn'))
 where cn' qre = runCPS (cn (A (pure qre)))