module COSPhw2_NL where

import Data.List
import COSPhw2_FOL

------- CONTEXT-FREE GRAMMAR --------

data Sent = Sent NP VP                  deriving Show
data NP   = Alice | NP1 DET CN          deriving Show
data DET  = The | Every | Some | No     deriving Show
data CN   = Princess                    deriving Show
data VP   = VP1 IV | VP2 TV NP          deriving Show 
data IV   = Laughs                      deriving Show
data TV   = Hates | Admires             deriving Show


------- SEMANTIC REPRESENTATIONS ----

-- LF: we take our semantic representations to be formulas of FOL (logical forms)

type LF = Formula SimpleTerm

-- The LF of a sentence is obtained by applying the LF of the NP to the LF of the VP

lfSent :: Sent -> LF
lfSent (Sent np vp) = (lfNP np) (lfVP vp)

-- In line with Montague-style semantics, all NPs are functions;
-- proper names, which intuitively are constants, are type-raised to
-- funtions which given a predicate, return the result of applying
-- that predicate to the proper name.
-- The LF of quantified NPs is obtained by applying the LF of the
-- determiner to the LF of the common noun. For the LF of determiners
-- see below.

lfNP :: NP -> (SimpleTerm -> LF) -> LF
lfNP Alice         = \ p -> p (Cons (Constant "Alice"))
lfNP (NP1 det cn)  = (lfDET det) (lfCN cn) 

lfCN :: CN -> SimpleTerm -> LF
lfCN Princess = \ t -> Atom "Princess" [t] 

-- The LF of a determiner is obtained by quantifying over a variable
-- to which two properties are applied: p (the restriction,
-- contributed by the noun in the quantified NP) and q (the scope,
-- contributed by the VP of the sentence)
-- The function fresh makes sure each variable is bound by only one
-- quantifier (see the relevant code at the end of the file)

lfDET :: DET -> (SimpleTerm -> LF) -> (SimpleTerm -> LF) -> LF

lfDET Some  p q = Exists v (Conj [p (Var v), q (Var v)]) 
        where v = Variable "x" [fresh[p,q]]
lfDET Every p q = Forall v (Impl (p (Var v)) (q (Var v))) 
        where v = Variable "x" [fresh[p,q]]
lfDET No    p q = Neg (Exists v (Conj [p (Var v),q (Var v)]))
        where v = Variable "x" [fresh[p,q]]
lfDET The p q = Exists v1 (Conj 
                 [Forall v2 (Equi (p (Var v2)) 
                                  (Eq (Var v1) (Var v2))), 
                  q (Var v1)])
      where
           i  = fresh[p,q]
           v1 = Variable "x" [i]
           v2 = Variable "x" [i+1]


-- the complex semantics of NPs complicates the representation of
-- VPs with transitive verbs: the LF of the object NP is applied to
-- the LF of the verb, which ends up saturating the object argument. 
-- The LF of the VP indicates that the subject argument is still missing.

lfVP :: VP -> SimpleTerm -> LF
lfVP (VP1 iv)    = \ subj -> lfIV iv subj
lfVP (VP2 tv np) = \ subj -> lfNP np (\ obj -> lfTV tv (subj,obj))

lfIV :: IV -> SimpleTerm -> LF
lfIV Laughs = \ t -> Atom "Laugh" [t]

lfTV :: TV -> (SimpleTerm,SimpleTerm) -> LF
lfTV Hates    = \ (t1,t2) -> Atom "Hate"   [t1,t2]
lfTV Admires  = \ (t1,t2) -> Atom "Admire" [t1,t2]



-- some example sentences for which we can compute the LF:

s1 = lfSent (Sent (Alice) (VP1 Laughs)) 
s2 = lfSent (Sent (NP1 Some Princess) (VP2 Hates (NP1 Some Princess)))
s3 = lfSent (Sent (NP1 Some Princess) (VP2 Admires (Alice)))
s4 = lfSent (Sent (Alice) (VP2 Hates (NP1 Every Princess)))



-- fresh: used in the definitions of lfDET above
-- To get formulas with more than one quantifier right, we need to
-- make sure that the variables bound by each quantifier are
-- different. The following bit of code does that by adding indices to
-- quantifier-bound variables.

bInLF :: LF -> [Int]
bInLF (Atom _ _)                  = []
bInLF (Eq _ _)                    = []
bInLF (Neg lf)                    = bInLF lf 
bInLF (Impl lf1 lf2)              = bInLFs [lf1,lf2] 
bInLF (Equi lf1 lf2)              = bInLFs [lf1,lf2]

bInLF (Conj lfs)                  = bInLFs lfs 
bInLF (Disj lfs)                  = bInLFs lfs 
bInLF (Forall (Variable _ [i]) f) = i : bInLF f 
bInLF (Exists (Variable _ [i]) f) = i : bInLF f 

bInLFs :: [LF] -> [Int]
bInLFs = nub . concat . map bInLF

freshIndex  :: [LF] -> Int
freshIndex lfs = i+1
       where i = maximum (0:(bInLFs lfs))

fresh :: [SimpleTerm -> LF] -> Int
fresh preds   = freshIndex (map ($ dummy) preds) 
  where dummy = Cons (Constant "")