{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-|
Module      : Analysis.Factivity.Factivity
Description : Factivity lexicon.
Copyright   : (c) Julian Grove and Aaron Steven White, 2025
License     : MIT
Maintainer  : julian.grove@gmail.com
-}

module Analysis.Factivity.Factivity where

import Analysis.Factivity.Signature
import Framework.Grammar.CCG
import Framework.Grammar.Lexica.SynSem
import Framework.Grammar.Lexica.SynSem.Convenience as Convenience
import Framework.Lambda

--------------------------------------------------------------------------------
-- * Lexica for factivity

instance Interpretation Factivity SynSem where
  combineR :: SynSem -> SynSem -> [SynSem]
combineR = SynSem -> SynSem -> [SynSem]
Convenience.combineR
  combineL :: SynSem -> SynSem -> [SynSem]
combineL = SynSem -> SynSem -> [SynSem]
Convenience.combineL
  
  lexica :: [Lexicon SynSem]
lexica = [Lexicon SynSem
lex]
    where lex :: Lexicon SynSem
lex = \case
            String
"knows"       -> [ SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"s",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term -> Term
lam Term
s (Term -> Term
purePP (Term -> Term -> Term
lam Term
p (Term -> Term -> Term
lam Term
x (Term -> Term -> Term
lam Term
i (Term -> Term -> Term -> Term
ITE (Term -> Term
TauKnow Term
s) (Term -> Term -> Term
And (Term -> Term
epi Term
i Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
p) (Term
p Term -> Term -> Term
@@ Term
i)) (Term -> Term
epi Term
i Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
p))))) Term -> Term -> Term
@@ Term
s))
                                 } ]
            String
"linguist"    -> [ SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"n",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x (Term -> Term -> Term
lam Term
i (Term -> Term
ling Term
i Term -> Term -> Term
@@ Term
x))))
                                 } ]
            String
"philosopher" -> [ SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"n",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x (Term -> Term -> Term
lam Term
i (Term -> Term
phil Term
i Term -> Term -> Term
@@ Term
x))))
                                 } ]
            String
"jo"          -> [ SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"np",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (String -> Term
sCon String
"j"))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np"),
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x (Term
x Term -> Term -> Term
@@ String -> Term
sCon String
"j")))
                                 } ]
            String
"bo"          -> [ SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"np",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (String -> Term
sCon String
"b"))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np"),
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x (Term
x Term -> Term -> Term
@@ String -> Term
sCon String
"b")))
                                 } ]
            String
"every"       -> [ SynSem {
                                 syn :: Cat
syn = (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np") Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"np") Cat -> Cat -> Cat
// String -> Cat
Base String
"n",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
c (Term -> Term -> Term
lam Term
k (Term -> Term -> Term
lam Term
y (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"∀" Term -> Term -> Term
@@ (Term -> Term -> Term
lam Term
x (String -> Term
sCon String
"(⇒)" Term -> Term -> Term
@@ (Term
c Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
k Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y Term -> Term -> Term
@@ Term
i)))))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np") Cat -> Cat -> Cat
// String -> Cat
Base String
"n",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
c (Term -> Term -> Term
lam Term
k (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"∀" Term -> Term -> Term
@@ (Term -> Term -> Term
lam Term
x (String -> Term
sCon String
"(⇒)" Term -> Term -> Term
@@ (Term
c Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
k Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i))))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
// String -> Cat
Base String
"np") Cat -> Cat -> Cat
// String -> Cat
Base String
"n",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
c (Term -> Term -> Term
lam Term
k (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"∀" Term -> Term -> Term
@@ (Term -> Term -> Term
lam Term
x (String -> Term
sCon String
"(⇒)" Term -> Term -> Term
@@ (Term
c Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
k Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i))))))))
                                 } ]
            String
"a"           -> [ SynSem {
                                 syn :: Cat
syn = (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np") Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"np") Cat -> Cat -> Cat
// String -> Cat
Base String
"n",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
c (Term -> Term -> Term
lam Term
k (Term -> Term -> Term
lam Term
y (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"∃" Term -> Term -> Term
@@ (Term -> Term -> Term
lam Term
x (String -> Term
sCon String
"(∧)" Term -> Term -> Term
@@ (Term
c Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
k Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y Term -> Term -> Term
@@ Term
i)))))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np") Cat -> Cat -> Cat
// String -> Cat
Base String
"n",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
c (Term -> Term -> Term
lam Term
k (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"∃" Term -> Term -> Term
@@ (Term -> Term -> Term
lam Term
x (String -> Term
sCon String
"(∧)" Term -> Term -> Term
@@ (Term
c Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
k Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i))))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
// String -> Cat
Base String
"np") Cat -> Cat -> Cat
// String -> Cat
Base String
"n",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
c (Term -> Term -> Term
lam Term
k (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"∃" Term -> Term -> Term
@@ (Term -> Term -> Term
lam Term
x (String -> Term
sCon String
"(∧)" Term -> Term -> Term
@@ (Term
c Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
k Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i))))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"n",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x Term
x))
                                 } ]
            String
"likely"      -> [ SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"deg" Cat -> Cat -> Cat
// String -> Cat
Base String
"s",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (
                                     Term -> Term -> Term
lam Term
s (Term -> Term
purePP (Term -> Term -> Term
lam Term
p (Term -> Term -> Term
lam Term
d (Term -> Term -> Term
lam Term
i (
                                                                     String -> Term
sCon String
"(≥)" Term -> Term -> Term
@@ (
                                                                         Term -> Term
Pr (Term -> Term -> Term -> Term
let' Term
j (Term -> Term
CG Term
s) (Term -> Term
Return (Term
p Term -> Term -> Term
@@ ([String] -> Term -> Term -> Term
overwrite [String]
contextParams Term
i Term
j))))
                                                                         ) Term -> Term -> Term
@@ Term
d
                                                                     )))) Term -> Term -> Term
@@ Term
s)
                                     )
                                 } ]
            String
"how"         -> [ SynSem {
                                 syn :: Cat
syn =  String -> Cat
Base String
"qDeg" Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
// String -> Cat
Base String
"ap") Cat -> Cat -> Cat
// (String -> Cat
Base String
"ap" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"deg"),
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x (Term -> Term -> Term
lam Term
y (Term -> Term -> Term
lam Term
z (Term
y Term -> Term -> Term
@@ (Term
x Term -> Term -> Term
@@ Term
z))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"qDeg" Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"deg"),
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x Term
x))
                                 } ]
            String
"is"          -> [ SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"ap",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x Term
x))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"np",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x Term
x))
                                 } ]
            String
"and"         -> [ SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np") Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np")) Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np")),
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
m (Term -> Term -> Term
lam Term
n (Term -> Term -> Term
lam Term
k (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"(∧)" Term -> Term -> Term
@@ (Term
n Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
m Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
i)))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
// String -> Cat
Base String
"np") Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
// String -> Cat
Base String
"np")) Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
// String -> Cat
Base String
"np")),
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
m (Term -> Term -> Term
lam Term
n (Term -> Term -> Term
lam Term
k (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"(∧)" Term -> Term -> Term
@@ (Term
n Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
m Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
i)))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np") Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"np") Cat -> Cat -> Cat
\\ ((String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np") Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"np")) Cat -> Cat -> Cat
// ((String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np") Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"np")),
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
m (Term -> Term -> Term
lam Term
n (Term -> Term -> Term
lam Term
k (Term -> Term -> Term
lam Term
x (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"(∧)" Term -> Term -> Term
@@ (Term
n Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
m Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i))))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"s" Cat -> Cat -> Cat
// String -> Cat
Base String
"s",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
m (Term -> Term -> Term
lam Term
n (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"(∧)" Term -> Term -> Term
@@ (Term
n Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
m Term -> Term -> Term
@@ Term
i))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np") Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np"),
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
m (Term -> Term -> Term
lam Term
n (Term -> Term -> Term
lam Term
x (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"(∧)" Term -> Term -> Term
@@ (Term
n Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
m Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
i)))))))
                                 }
                             , SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"np" Cat -> Cat -> Cat
\\ (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"np") Cat -> Cat -> Cat
// (String -> Cat
Base String
"s" Cat -> Cat -> Cat
\\ String -> Cat
Base String
"np" Cat -> Cat -> Cat
// String -> Cat
Base String
"np"),
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
m (Term -> Term -> Term
lam Term
n (Term -> Term -> Term
lam Term
x (Term -> Term -> Term
lam Term
y (Term -> Term -> Term
lam Term
i (String -> Term
sCon String
"(∧)" Term -> Term -> Term
@@ (Term
n Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y Term -> Term -> Term
@@ Term
i) Term -> Term -> Term
@@ (Term
m Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y Term -> Term -> Term
@@ Term
i))))))))
                                 }
                             ]
            String
"that"        -> [ SynSem {
                                 syn :: Cat
syn = String -> Cat
Base String
"s" Cat -> Cat -> Cat
// String -> Cat
Base String
"s",
                                 sem :: Typed
sem = Sig -> Term -> Typed
ty Sig
tauFact (Term -> Term
purePP (Term -> Term -> Term
lam Term
x Term
x))
                                 } ]

--------------------------------------------------------------------------------
-- * Priors and response functions


-- | Prior to be used for the factivity example.
factivityPrior :: Term
factivityPrior :: Term
factivityPrior = Term -> Term -> Term -> Term
let' Term
x (Term -> Term -> Term
LogitNormal Term
0 Term
1) (Term -> Term -> Term -> Term
let' Term
y (Term -> Term -> Term
LogitNormal Term
0 Term
1) (Term -> Term -> Term -> Term
let' Term
z (Term -> Term -> Term
LogitNormal Term
0 Term
1) (Term -> Term -> Term -> Term
let' Term
b (Term -> Term
Bern Term
x) (Term -> Term
Return (Term -> Term -> Term
UpdCG (Term -> Term -> Term -> Term
let' Term
c (Term -> Term
Bern Term
y) (Term -> Term -> Term -> Term
let' Term
d (Term -> Term
Bern Term
z) (Term -> Term
Return (Term -> Term -> Term
UpdLing (Term -> Term -> Term
lam Term
x Term
c) (Term -> Term -> Term
UpdEpi (Term -> Term -> Term
lam Term
x (Term -> Term -> Term
lam Term
p Term
d)) Term
_0))))) (Term -> Term -> Term
UpdTauKnow Term
b Term
ϵ))))))

-- | Respones function to be used for the factivity example.
factivityRespond :: Term -> Term -> Term
factivityRespond :: Term -> Term -> Term
factivityRespond = Term -> Term -> Term -> Term
respond (Term -> Term -> Term
lam Term
x (Term -> Term -> Term -> Term
Truncate (Term -> Term -> Term
Normal Term
x (String -> Term
Var String
"sigma")) Term
0 Term
1))