Grand.hs

module Grand where


import Data.List
import Data.Maybe
import Control.Arrow
import Control.Monad (guard)
{-import Data.Maybe (listToMaybe,maybeToList)-}
import Data.Char (toLower)


class Syn a where
   negation  :: a -> a
   subterms :: a -> [Term]
   cnsIn :: a -> [CN]
   verbsIn :: a -> [V]  
   buildTermSub :: a -> a -> Maybe [(Term,Term)]
   buildPVSub :: a -> a -> Maybe [(PV,PV)]
   spellOut :: a -> [(Term, Term)] -> [(PV, PV)] -> a
   hasNegativeMarker :: a-> Bool
  


xAsDefaultTerm :: Maybe Term -> Term
xAsDefaultTerm = fromMaybe (CNasTerm $ PCN Pos X)
     
rAsDefaultPV :: Maybe PV -> PV
rAsDefaultPV = fromMaybe (PV Pos R)
    
plusStrict :: (Eq a) => Maybe [a] -> Maybe [a] -> Maybe [a]
plusStrict a b = a >>= \x -> b >>= \y -> return $ nub $ x ++ y

hunt :: (Eq a) => a ->  Maybe [(a,a)] -> Maybe a

hunt t Nothing = Nothing
hunt t (Just [])  = Nothing
hunt t (Just ((uu,vv):rest)) 
  | (t==uu)  =  (Just vv)
  | otherwise = hunt t (Just rest)
  
moveAhead  ::  (Eq a) =>  Maybe [(a,a)]  ->  Maybe [(a,a)]  -> Bool
moveAhead Nothing  xx = False
moveAhead  xx Nothing = False
moveAhead (Just []) xx = True
moveAhead (Just ((uu,vv):rest))  xx 
        | value == (Just vv)  =  (moveAhead (Just rest) xx)
        | value == Nothing  =    (moveAhead (Just rest) xx)
        | otherwise  = False
   where  value = hunt uu xx
   
combineStructures xx yy =
    if moveAhead xx yy == True then (plusStrict xx yy) else Nothing
  
polarizedCNNegation (PCN Pos cn) = (PCN Neg cn)
polarizedCNNegation (PCN Neg cn) = (PCN Pos cn)

-- the definition of  pCNsIn is needed in Sdagleq.hs, but not elsewhere
pCNsIn (CNasTerm (PCN Pos cn))  = (PCN Pos cn)
pCNsIn (CNasTerm (PCN Neg cn))  = (PCN Neg cn)
pCNsIn (TermMaker (PV Pos v) (TermNP All n))  =  pCNsIn n
pCNsIn (TermMaker (PV Pos v) (TermNP Some n))  =  pCNsIn n
pCNsIn (TermMaker (PV Neg v) (TermNP All n))  =  pCNsIn n
pCNsIn (TermMaker (PV Neg v) (TermNP Some n))  =  pCNsIn n 

instance Syn PolCN where
   negation (PCN Pos cn) = (PCN Neg cn)
   negation (PCN Neg cn) = (PCN Pos cn)
   subterms cn = []
   cnsIn (PCN p cn)  = [cn]
   verbsIn (PCN p cn)  = [ ]
   buildTermSub (PCN p cn) (PCN p' cn') = Just [] 
   buildPVSub (PCN p cn) (PCN p' cn') = Just []
   spellOut (PCN p cn) k k' = (PCN p cn)   --- THIS LINE IS QUESTIONABLE.  IT'S NOT NEEDED
   hasNegativeMarker (PCN Pos cn) = False
   hasNegativeMarker (PCN Neg cn) = True
   
instance Syn Term where
   negation (CNasTerm (PCN Pos cn))  = (CNasTerm (PCN Neg cn))
   negation (CNasTerm (PCN Neg cn))  = (CNasTerm (PCN Pos cn))
   negation (TermMaker (PV Pos v) (TermNP All n))  =  TermMaker (PV Neg v) (TermNP Some n) 
   negation (TermMaker (PV Pos v) (TermNP Some n))  =  TermMaker (PV Neg v) (TermNP All n) 
   negation (TermMaker (PV Neg v) (TermNP All n))  =  TermMaker (PV Pos v) (TermNP Some n) 
   negation (TermMaker (PV Neg v) (TermNP Some n))  =  TermMaker (PV Pos v) (TermNP All n) 
   subterms (CNasTerm ter) =  [(CNasTerm ter)]
   subterms (TermMaker pv (TermNP d ter)) = (TermMaker pv (TermNP d ter)):subterms ter
   cnsIn Ter1 = []
   cnsIn Ter2 = []
   cnsIn Ter3 = []
   cnsIn Ter1bar = []
   cnsIn Ter2bar = []
   cnsIn Ter3bar = []
   cnsIn (CNasTerm (PCN p cn)) = [cn]
   cnsIn (TermMaker t n) =    (cnsIn n) 
   hasNegativeMarker   (CNasTerm (PCN Pos cn)) = False
   hasNegativeMarker (CNasTerm (PCN Neg cn))  =  True
   hasNegativeMarker (TermMaker (PV Pos v) (TermNP All n))  =  hasNegativeMarker n
   hasNegativeMarker (TermMaker (PV Pos v) (TermNP Some n))  =  hasNegativeMarker n 
   hasNegativeMarker (TermMaker (PV Neg v) (TermNP All n))  =  hasNegativeMarker n 
   hasNegativeMarker (TermMaker (PV Neg v) (TermNP Some n))  =  hasNegativeMarker n 
   
  
   verbsIn (TermMaker (PV pol ver) np) =  [ver] ++  (verbsIn np)    
   verbsIn _                                            = []
   
   buildTermSub (TermMaker x y) (CNasTerm z) = Nothing
   buildTermSub (CNasTerm (PCN Pos cn))  (CNasTerm dn) = Just [(CNasTerm (PCN Pos cn), CNasTerm dn)]  
   buildTermSub (CNasTerm (PCN Neg cn))  (CNasTerm (PCN Pos dn)) = Just [(CNasTerm (PCN Pos cn), CNasTerm (PCN Neg dn))]  
   buildTermSub (CNasTerm (PCN Neg cn))  (CNasTerm (PCN Neg dn)) = Just [(CNasTerm (PCN Pos cn), CNasTerm (PCN Pos dn))]  
   buildTermSub (CNasTerm zz)(TermMaker xx yy)  = Nothing
   buildTermSub (TermMaker v np1) (TermMaker w np2)  =  buildTermSub np1 np2
   buildTermSub Ter1 t = Just [(Ter1, t)]  
   buildTermSub Ter2 t = Just [(Ter2, t)]
   buildTermSub Ter3 t = Just [(Ter3, t)]
   buildTermSub Ter1bar t = Just [(Ter1, negation t)]  
   buildTermSub Ter2bar t = Just [(Ter2, negation t)]
   buildTermSub Ter3bar t = Just [(Ter3, negation t)]
   buildPVSub (TermMaker xx yy) (CNasTerm zz) = Nothing
   buildPVSub (CNasTerm xx) ter = Just []
   buildPVSub (TermMaker vv (TermNP d t)) (TermMaker ww (TermNP e u))  =  
      if (d == e) then Just [(vv,ww)] else Nothing
   buildPVSub Ter1 t = Just []
   buildPVSub Ter2 t = Just []
   buildPVSub Ter3 t = Just []
   buildPVSub Ter1bar t = Just []
   buildPVSub Ter2bar t = Just []
   buildPVSub Ter3bar t = Just []  
   spellOut (CNasTerm (PCN Pos cn)) list1 list2 = xAsDefaultTerm  $ lookup (CNasTerm (PCN Pos cn)) list1
   spellOut (CNasTerm (PCN Neg cn)) list1 list2 = negation $ xAsDefaultTerm  $ lookup (CNasTerm (PCN Pos cn)) list1
   spellOut (TermMaker t n) list1 list2   =   (TermMaker (rAsDefaultPV $ lookup t list2)   (spellOut n list1 list2))
   spellOut  Ter1 list1 list2 =  xAsDefaultTerm  $ lookup  Ter1 list1
   spellOut  Ter2 list1 list2 =  xAsDefaultTerm  $ lookup  Ter2 list1
   spellOut  Ter3 list1 list2 =  xAsDefaultTerm  $ lookup  Ter3 list1
   spellOut  Ter1bar list1 list2 =  negation $ spellOut  Ter1 list1 list2
   spellOut  Ter2bar list1 list2 =  negation $ spellOut  Ter2 list1 list2
   spellOut  Ter3bar list1 list2 =  negation $ spellOut  Ter3 list1 list2
   
instance Syn NP where
   negation  (TermNP All t)  =  TermNP Some (negation t)  
   negation  (TermNP Some t)  =  TermNP All (negation t) 
   --negation (TermNP Atleast t) = TermNP More (negation t)
   --negation (TermNP More t) = TermNP Atleast (negation t)    
   subterms (TermNP All t)  = subterms t
   cnsIn Everyone = []
   cnsIn Someone = []
   cnsIn (TermNP d t) = cnsIn t
   verbsIn Everyone = []
   verbsIn Someone = []
   verbsIn (TermNP d t) =  verbsIn t 
   buildTermSub (TermNP d t)  (TermNP e u)    = 
      if (d == e) 
      then (buildTermSub t u) 
      else Nothing
   buildPVSub xx yy = Just []   
   spellOut (TermNP d t) list1 list2 =  (TermNP d (spellOut t list1 list2)) 
   hasNegativeMarker (TermNP All t) =  hasNegativeMarker t
   hasNegativeMarker (TermNP Some t) =  hasNegativeMarker t
   hasNegativeMarker (TermNP Atleast t) =  hasNegativeMarker t
   hasNegativeMarker (TermNP More t) =  hasNegativeMarker t
   
instance Syn Sent where
   negation (Sent All t u) = (Sent Some t (negation u)) 
   negation (Sent Some t u) = (Sent All t (negation u)) 
   negation (Sent Atleast t u) = (Sent More u t)
   negation (Sent More t u) = (Sent Atleast u t)  
   subterms (Sent d t u) =   (subterms t) ++ (subterms u)   -- I dropped   at the front    [t,u] ++
   subterms (Sent2 d t u t2 u2) =   (subterms t) ++ (subterms u) ++ (subterms t2) ++ (subterms u2)   -- I dropped [t,u,t2,u2] ++ 
   cnsIn (Sent d t u) = (cnsIn t)  ++  (cnsIn u)    
   cnsIn (Sent2 d t u t2 u2) =    (cnsIn t)  ++  (cnsIn u)  ++ (cnsIn t2)  ++  (cnsIn u2)  
   verbsIn (Sent d t u) = (verbsIn t)  ++  (verbsIn u)
   verbsIn (Sent2 d t u t2 u2) = (verbsIn t)  ++  (verbsIn u) ++(verbsIn t2)  ++  (verbsIn u2)
   buildTermSub (Sent d tt uu) (Sent e vv ww) =
      if (d == e) then (combineStructures (buildTermSub tt vv)  (buildTermSub uu ww)) else Nothing  
   buildTermSub (Sent2 d tt uu tt2 uu2) (Sent2 e vv ww vv2 ww2) =
      if (d == e) 
      then foldl1 combineStructures [(buildTermSub tt vv),  (buildTermSub uu ww),(buildTermSub tt2 vv2),  (buildTermSub uu2 ww2)]
      else Nothing
   buildPVSub (Sent d t uu) (Sent e vv ww) =
      if (d == e) then (plusStrict (buildPVSub t vv)  (buildPVSub uu ww)) else Nothing  
   buildPVSub (Sent2 d tt uu tt2 uu2) (Sent2 e vv ww vv2 ww2)  =
      if (d == e) 
      then foldl1 plusStrict [(buildPVSub tt vv),  (buildPVSub uu ww),(buildPVSub tt2 vv2),  (buildPVSub uu2 ww2)]
      else Nothing
   spellOut (Sent d t u)  list1 list2  =  (Sent d (spellOut t list1 list2)  (spellOut u list1 list2)) 
   spellOut (Sent2 d t u t2 u2)  list1 list2  =  (Sent2 d (spellOut t list1 list2)  (spellOut u list1 list2) (spellOut t2 list1 list2)  (spellOut u2 list1 list2)) 
   hasNegativeMarker (Sent All t u)  =  and [hasNegativeMarker t,  hasNegativeMarker u ]
   hasNegativeMarker (Sent Some t u)  =  and [hasNegativeMarker t , hasNegativeMarker u ]
   hasNegativeMarker (Sent Atleast t u)  =  and [hasNegativeMarker t, hasNegativeMarker u ]
   hasNegativeMarker (Sent More t u)  =  and [hasNegativeMarker t, hasNegativeMarker u ]
        
data Sent = Sent Det Term Term | Sent2 Det Term Term Term Term    
                   deriving (Ord,Eq)
                   
instance Show Sent where
         -- show (Sent d t u)  =  show (d)  ++ " " ++ show(t) ++ " " ++ show(u)  
          show (Sent  d (TermMaker x y) (TermMaker z w) )  =  show (d)  ++ " who " ++ show((TermMaker x y)) ++ " also " ++ show((TermMaker z w))                   
          show (Sent d (TermMaker x y) (CNasTerm pcn) )  =  show (d)  ++ " who " ++ show((TermMaker x y)) ++ " are " ++ show((CNasTerm pcn))  
          show (Sent d (CNasTerm pcn)  (TermMaker x y))  =  show (d)  ++ " " ++ show((CNasTerm pcn)) ++ " " ++ show((TermMaker x y)) 
          show (Sent d (CNasTerm pcn)  (CNasTerm pcn2))  =  show (d)  ++ " " ++ show((CNasTerm pcn)) ++ " are " ++ show((CNasTerm pcn2)) 
          show (Sent2 d x y u v)  =  show (d)  ++ " " ++ show(x) ++ " which are " ++ show(y) ++ " are also " ++  show(u) ++ " which are " ++ show(v) 
          
principalDet (Sent d t t') = d
converse s@(Sent All t u) = (Sent All u t)
           
data NP   =   Everyone | Someone | TermNP Det Term | IntTermNP Det IntersectionTerm
          deriving (Ord,Eq)
          
instance Show NP where
     show (TermNP d t) =  show(d) ++ " " ++ show(t) 
     show (IntTermNP d t) =  show(d) ++ " " ++ show(t) 

data Det  =  All | Some | No | Most | Atleast | More | Contradiction
          deriving  (Ord,Eq)
  
instance Show Det where
     show All = "all"
     show Some = "some"
     show No = "no"
     show Most = "most"
     show Atleast = "at least"
     show More = "more"
     show Contradiction = "contradiction"
                    
  
          
data CN   =  Girls   
                 | Boys 
                 | Dogs | Cats | Skunks | Sneetches | Mammals | Chordates | Animals | Birds | X | Y | Z | W | P | Q | N  --Var CNvariable
          deriving (Eq,Ord) 
          
instance Show CN where
    show Girls = "girls"
    show Boys = "boys"
    show Dogs = "dogs"
    show Cats = "cats"
    show Skunks = "skunks"
    show Sneetches = "sneetches"
    show Mammals = "mammals"
    show Chordates = "chordates"
    show Animals = "animals"
    show Birds = "birds"
    show X = "x"
    show Y = "y"
    show Z = "z"
    show W = "w"
    show P = "p"
    show Q = "q"  
    show N = "n"         

data Polarity =  Pos | Neg
   deriving (Ord, Eq)
   
instance Show Polarity where
   show Pos = ""
   show Neg = "non-"      

data PolCN =  PCN Polarity CN
      deriving (Eq,Ord)
instance Show PolCN   where
    show (PCN a b)  = (show a)++(show b)
                       
cnvariables = [X, Y, Z, W, P, Q, N]          
          
data Term =   CNasTerm PolCN
                   |  TermMaker PV NP    
                   |  Ter1 | Ter2  | Ter3  |  Ter1bar | Ter2bar  | Ter3bar                
                       deriving (Ord,Eq)
instance Show Term where
  show (CNasTerm px) = show px
  show (TermMaker t (TermNP d (TermMaker pv np)))  = show(t) ++ " " ++ show(d) ++ " who " ++ show(pv) ++  " " ++ show(np)
  show (TermMaker t (TermNP d  (CNasTerm px))) = show(t)  ++ " " ++ show(d) ++  " " ++ show(px)
  --show (TermMaker t n) = "(" ++  show(t) ++ " " ++ show(n)++")"  -- this was it!!!
  show Ter1 = "Ter1"
  show Ter2 = "Ter2"
  show Ter3 = "Ter3"
  show Ter1bar = "Ter1-bar"
  show Ter2bar = "Ter2-bar"
  show Ter3bar = "Ter3-bar"  
  
data PV =  PV Polarity V
      deriving (Eq,Ord)
instance Show PV   where
    show (PV a b)  = (show a)++(show b)  

data V   = Loves   | Admires | Helps | Sees | Hates | R | S
          deriving (Eq,Ord) 
          
instance Show V where
    show Loves = "love"
    show Admires = "admire"
    show Helps = "help"
    show Sees = "see"
    show Hates = "hate"
    show R = "r"
    show S = "s"

r = PV Pos R
x = PCN Pos X
y = PCN Pos Y
z = PCN Pos Z
p = PCN Pos P
q = PCN Pos Q
n = PCN Pos N
w = PCN Pos W
non_x = PCN Neg X
non_y = PCN Neg Y
non_z = PCN Neg Z
non_w = PCN Neg W
non_p = PCN Neg P
non_q = PCN Neg Q
non_n = PCN Neg N
skunks = PCN Pos Skunks
mammals = PCN Pos Mammals
animals = PCN Pos Animals
sneetches = PCN Pos Sneetches
dogs = PCN Pos Dogs
birds = PCN Pos Birds
chordates = PCN Pos Chordates
boys = PCN Pos Boys
girls = PCN Pos Girls
cats = PCN Pos Cats
non_skunks = PCN Neg Skunks
non_mammals = PCN Neg Mammals
non_animals = PCN Neg Animals
non_sneetches = PCN Neg Sneetches
non_dogs = PCN Neg Dogs
non_birds = PCN Neg Birds
non_chordates = PCN Neg Chordates
non_boys = PCN Neg Boys
non_girls = PCN Neg Girls
non_cats = PCN Neg Cats
loves = PV Pos Loves
admires = PV Pos Admires
helps = PV Pos Helps
sees = PV Pos Sees
hates = PV Pos Hates
not_loves = PV Neg Loves
not_admires = PV Neg Admires
not_helps = PV Neg Helps
not_sees = PV Neg Sees
not_hates = PV Neg Hates


data IntersectionTerm =   IntersectionTerm PolCN Term  
                   |  IntTer1 | IntTer2  | IntTer3  |  IntTer1bar | IntTer2bar  | IntTer3bar                
                       deriving (Ord,Eq)
instance Show IntersectionTerm where
  show (IntersectionTerm p t) = show(p)  ++ " who " ++ show(t)
  show IntTer1 = "IntTer1"
  show IntTer2 = "IntTer2"
  show IntTer3 = "IntTer3"
  show IntTer1bar = "IntTer1-bar"
  show IntTer2bar = "IntTer2-bar"
  show IntTer3bar = "IntTer3-bar"  



-------------THIS WHOLE FILE SHOULD BE REWORKED IN THE LIGHT OF THE FRONT END! ------------------
          

       
cnlist = [Girls,Boys, Dogs,  Cats, Skunks, Mammals, Animals, Chordates, Birds, X, Y, Z, P, Q]       
verbList = [Loves, Admires,Helps, Hates,Sees, R, S]     
tvVarList = [R,S]        
verblistNotVars = verbList \\ tvVarList  
cnVarList = [X, Y, Z, P, Q]        
cnlistNotVars sList  = cnlist \\ cnVarList  
polarizedCNListNotVars aList = [CNasTerm (PCN Pos w) | w <- cnlistNotVars aList] ++  [CNasTerm (PCN Neg w) | w <- cnlistNotVars aList]  
polarizedTermListNotVars aList = [CNasTerm (PCN Pos w) | w <- cnlistNotVars aList] ++  [CNasTerm (PCN Neg w) | w <- cnlistNotVars aList]   
pairOfCns (Sent d (CNasTerm (PCN Pos n1)) (CNasTerm (PCN Pos n2))) = (n1,n2)

      

s2 = Sent All (CNasTerm x) (CNasTerm y)
t1 = TermMaker sees (TermNP All  (CNasTerm skunks) )
t2 =  TermMaker sees  (TermNP All  (CNasTerm girls))
s = Sent All t3 t2
t3 =  TermMaker sees (TermNP All t1)
t4 =TermMaker  (PV Pos R)  (TermNP All  (CNasTerm  x))
t9 =    TermMaker sees (TermNP All  (CNasTerm sneetches))
t6 = TermMaker (PV Pos R) (TermNP Some t4)
s3 = Sent  All t1 t5
t5 =  (CNasTerm animals)
t7 =  (CNasTerm chordates)
t8 = TermMaker helps (TermNP All  (CNasTerm skunks ))
t10 =  (CNasTerm sneetches)
sAllXY = s2
sAllYZ = Sent All  (CNasTerm y)  (CNasTerm z)  
sAllYX = Sent All  (CNasTerm y)  (CNasTerm x) 
sAllXZ = Sent All  (CNasTerm x)  (CNasTerm z)
sAllXX = Sent All  (CNasTerm x)  (CNasTerm x)
sAntiXY = Sent All  (CNasTerm non_x)  (CNasTerm non_y)  
sAntiYX = Sent All  (CNasTerm non_y)  (CNasTerm non_x)  
sSomeXX = Sent Some  (CNasTerm x)  (CNasTerm x)  
sSomeXY = Sent Some  (CNasTerm x)  (CNasTerm y)  
sSomeYX = Sent Some  (CNasTerm y)   (CNasTerm x) 
sSomeXZ = Sent Some  (CNasTerm x)  (CNasTerm z)  
sZeroX = Sent All (CNasTerm x) (CNasTerm non_x) 
sOneX = Sent All (CNasTerm non_x)  (CNasTerm x) 
sSome = Sent Some  (CNasTerm y)  (CNasTerm z)  
s4 = Sent Some  (CNasTerm dogs) (TermMaker sees (TermNP Some  (CNasTerm skunks) ))
s6 = Sent Some  (CNasTerm dogs) (TermMaker sees (TermNP Some  (CNasTerm skunks) ))
s5 = Sent Some  (CNasTerm sneetches) t2
s7 = Sent All t5 t9
s8 = Sent All  (CNasTerm dogs) t9
s9  =  Sent All t5 t7
s10 = Sent Some t10 t5
s11 = Sent Some  (CNasTerm dogs) (TermMaker sees (TermNP Some  (CNasTerm sneetches)))
s12 = Sent No t10 t10
sentList = [
            (Sent  All  (CNasTerm skunks)   (CNasTerm mammals)), 
            (Sent  Some  (CNasTerm skunks)   (CNasTerm mammals)),   
            (Sent  All  (CNasTerm mammals)  (CNasTerm chordates)),
            s3, s4, s5, s6, s7, s8, s9, s10, s11, s12
            ]


anotherList = 
    [ (Sent  Some  (CNasTerm skunks)   (CNasTerm mammals)),  (Sent  Some  (CNasTerm non_chordates)   (CNasTerm mammals)),
      (Sent  All  (CNasTerm non_chordates)   (CNasTerm dogs)),
     (Sent  Some  (CNasTerm skunks)   (CNasTerm boys)),  (Sent  All  (CNasTerm girls)   (CNasTerm non_mammals))]
             
fourseven = [(Sent All  (CNasTerm non_y)  (CNasTerm p)),  (Sent All  (CNasTerm p)  (CNasTerm q)),
                     (Sent All  (CNasTerm q)  (CNasTerm y)), (Sent All  (CNasTerm y)  (CNasTerm p)), (Sent All  (CNasTerm q)  (CNasTerm z))
                    ] 

smallSentList =   [(Sent  All  (CNasTerm skunks)   (CNasTerm mammals)), 
            (Sent  Some  (CNasTerm skunks)   (CNasTerm mammals)),   
              (Sent  Some  (CNasTerm non_skunks)   (CNasTerm mammals)),
            (Sent  All  (CNasTerm mammals)  (CNasTerm non_chordates)),       (Sent  Some  (CNasTerm boys)  (CNasTerm non_chordates)),
             (Sent  All  (CNasTerm girls)  (CNasTerm non_girls))]
conc =  (Sent  All  t13 t14)

tinySentList =  [(Sent  All  (CNasTerm skunks)   (CNasTerm mammals)), 
                        (Sent  Some    (CNasTerm mammals) (CNasTerm skunks) ),   
                        (Sent  All  (CNasTerm sneetches)   (CNasTerm skunks))]


t11 = TermMaker sees (TermNP All  (CNasTerm skunks) )
t12 =  TermMaker sees  (TermNP All  (CNasTerm mammals))
t13 = TermMaker helps (TermNP All t11)
t14 = TermMaker helps (TermNP All t12)
             
             
             





type Parser a b = [a] -> [(b,[a])]
type PARSER a b = Parser a (ParseTree a b)

epsilonT :: PARSER a b 
epsilonT = succeed Ep

symbolT :: Eq a => a -> PARSER a b
symbolT s = (\ x -> Leaf x) <$$> symbol s

symbol :: Eq a => a -> Parser a a 
symbol c []                 = []
symbol c (x:xs) | c == x    = [(x,xs)]
                | otherwise = [] 

infixl 6 <:>

(<:>) :: Parser a b -> Parser a [b] -> Parser a [b]
(p <:> q) xs = [ (r:rs,zs) | (r,ys)  <- p xs, 
                             (rs,zs) <- q ys ]

(<|>) :: Parser a b -> Parser a b -> Parser a b 
(p1 <|> p2) xs = p1 xs ++ p2 xs 

(<**>) :: Parser a [b] -> Parser a [b] -> Parser a [b]
(p <**> q) xs = [ (r1 ++ r2,zs) | (r1,ys) <- p xs, 
                                 (r2,zs) <- q ys ]
infixl 7 <$$>

(<$$>) :: (a -> b) -> Parser s a -> Parser s b
(f <$$> p) xs = [ (f x,ys) | (x,ys) <- p xs ]

data ParseTree a b =  Ep | Leaf a | Branch b [ParseTree a b] 
                   deriving Eq
                   
instance (Show a, Show b) => Show (ParseTree a b) where
  show Ep            = "[]"
  show (Leaf t)      = show t
  show (Branch l ts) = "[." ++ show l  ++ " " 
                            ++ show ts ++ "]"                   
succeed :: b -> Parser a b 
succeed r xs = [(r,xs)]


collect :: [Parser a b] -> Parser a [b] 
collect []     = succeed []
collect (p:ps) = p <:> collect ps 

parseAs :: b -> [PARSER a b] -> PARSER a b
parseAs label ps = (\ xs -> Branch label xs) <$$> collect ps

sent, tv, cn, det, t, int, intOrT, neg, np :: PARSER String String
cn   =              symbolT "skunks" 
                 <|> symbolT "mammals"  
                 <|> symbolT "chordates" 
                 <|> symbolT "boys" <|> symbolT "girls" <|> symbolT "animals"
                 
tv = symbolT "see" <|> symbolT "love" <|> symbolT "admire"  <|> symbolT "hate"

det  =        symbolT "every"  
           <|> symbolT "some" 
           <|> symbolT "no" 
           <|> symbolT "all"
           <|> symbolT "most"
           
t = parseAs "Term" [cn] 
           <|>  parseAs "Term" [symbolT "non" ,cn]  
           <|> parseAs "Term" [tv, det, intOrT] 
           <|> parseAs "Term" [tv, det, symbolT "who", intOrT]
           
--pcn = parseAs "PCN" [pol, cn]
neg = symbolT "non"

np   =  parseAs "NP" [det,intOrT]
--pv = parseAs "PV" [pol, tv] 

sent =  parseAs "S" [det,intOrT,intOrT]

int = parseAs "Int" [cn,symbolT "who",t]

intOrT = int <|> t

move :: ParseTree String String  -> Term
move (Branch "Term" [Leaf "skunks"]) =  (CNasTerm skunks)
move (Branch "Term" [Leaf "mammals"]) =  (CNasTerm mammals)
move (Branch "Term" [Leaf "animals"]) =  (CNasTerm animals)
move (Branch "Term" [Leaf "chordates"]) =  (CNasTerm chordates)
move (Branch "Term" [Leaf "sneetches"]) =  (CNasTerm sneetches)
move (Branch "Term" [(Leaf "non"), (Leaf "skunks")]) =  (CNasTerm non_skunks)
move (Branch "Term" [(Leaf "non"), Leaf "mammals"]) =  (CNasTerm non_mammals)
move (Branch "Term" [(Leaf "non"), Leaf "animals"]) =  (CNasTerm non_animals)
move (Branch "Term" [(Leaf "non"), Leaf "chordates"]) =  (CNasTerm non_chordates)
move (Branch "Term" [(Leaf "non"), Leaf "sneetches"]) =  (CNasTerm non_sneetches)


move (Branch "Term" [(Leaf "see"), (Leaf "all"), (Leaf "who"), subtree])  
     =    (TermMaker sees   (TermNP All  (move subtree)))
move (Branch "Term" [(Leaf "see"), (Leaf "all"),  subtree])  
     =    (TermMaker sees   (TermNP All  (move subtree)))
move (Branch "Term" [(Leaf "love"), (Leaf "all"), (Leaf "who"), subtree])  
     =    (TermMaker loves   (TermNP All  (move subtree)))
move (Branch "Term" [(Leaf "love"), (Leaf "all"),  subtree])  
     =    (TermMaker loves   (TermNP All  (move subtree))) 
move (Branch "Term" [(Leaf "hate"), (Leaf "all"), (Leaf "who"), subtree])  
     =    (TermMaker hates   (TermNP All  (move subtree)))
move (Branch "Term" [(Leaf "hate"), (Leaf "all"),  subtree])  
     =    (TermMaker hates   (TermNP All  (move subtree)))     
move (Leaf "skunks") =  (CNasTerm skunks)
--move (Leaf ["mammals"]) =  (CNasTerm mammals)
--move (Leaf ["animals"]) =  (CNasTerm animals)

moveS :: ParseTree String String  -> Sent
moveS (Branch "S" [(Leaf "all"), ttree, ttree2])  =   (Sent All (move ttree) (move ttree2)) 
    
readMe  = moveS . fst . head . sent . words

sentParses :: String -> [Sent]
sentParses =
  map (moveS . fst)
  . filter (null . snd)
  . sent
  . words

-----USAGE:      moveS $ (fst.head) $ sent $ words "all see all see all skunks love all mammals"
---- ALSO  move $ (fst . head) $ t $ words "see all see all non skunks" 
--- note how 'non'  worls

split2 :: [t] -> [[[t]]]    ---- split2 takes any list $\ell$ and gives the list of all ways to split $\ell$ into two sublists 
    --- whose concatenation is $\ell$ again.
split2 []          = [[[],[]]]
split2 (x:xs)    =   [[ [], x:xs]]  ++  map (\z -> [x:(z!!0),z!!1]) (split2 xs)

split2' :: [t] -> [([t],[t])]
split2' = \case
  xs@(x : xs') -> ([],xs) : map (first (x :)) (split2' xs')

{-
[]     = [([],[])]
split2' (x:xs) =   [[ [], x:xs]]  ++  map (\z -> [x:(z!!0),z!!1]) (split2 xs)
-}

tF :: [String] -> [Term]
tF quoted    -- this parses terms
  | quoted == []                              = []
  | (quoted!! 0 == "who")   =  tF $ drop 1 quoted
  | (quoted!! 0 == "are")   =  tF $ drop 1 quoted
  |  quoted == ["skunks"]               = [CNasTerm skunks]
  |  quoted == ["mammals"]           = [CNasTerm mammals]
  |  quoted == ["chordates"]               = [CNasTerm chordates]
  |  quoted == ["boys"]                      = [CNasTerm boys]
  |  quoted == ["girls"]                      = [CNasTerm girls]
  |  quoted == ["dogs"]                      = [CNasTerm dogs]
  |  quoted == ["cats"]                      = [CNasTerm cats]
  |  quoted == ["birds"]                      = [CNasTerm birds]
  |  quoted == ["animals"]                      = [CNasTerm animals] 
  |  quoted == ["sneetches"]                      = [CNasTerm sneetches]
  |  quoted == ["non-skunks"]               = [CNasTerm non_skunks]
  |  quoted == ["non-mammals"]           = [CNasTerm non_mammals]
  |  quoted == ["non-chordates"]               = [CNasTerm non_chordates]
  |  quoted == ["non-boys"]                      = [CNasTerm non_boys]
  |  quoted == ["non-girls"]                      = [CNasTerm non_girls]
  |  quoted == ["non-dogs"]                      = [CNasTerm non_dogs]
  |  quoted == ["non-cats"]                      = [CNasTerm non_cats]
  |  quoted == ["non-birds"]                      = [CNasTerm non_birds]
  |  quoted == ["non-animals"]                      = [CNasTerm non_animals]
  |  quoted == ["non-sneetches"]                      = [CNasTerm non_sneetches]  
  |  quoted == ["x"]                      = [CNasTerm x]  
  |  quoted == ["y"]                      = [CNasTerm y]  
  |  quoted == ["z"]                      = [CNasTerm z]  
  |  quoted == ["p"]                      = [CNasTerm p]  
  |  quoted == ["q"]                      = [CNasTerm q]  
  |  quoted == ["non-x"]                      = [CNasTerm non_x]  
  |  quoted == ["non-y"]                      = [CNasTerm non_y]  
  |  quoted == ["non-z"]                      = [CNasTerm non_z]  
  |  quoted == ["non-p"]                      = [CNasTerm non_p]  
  |  quoted == ["non-q"]                      = [CNasTerm non_q]  
  | (quoted!! 0 == "see")   = [(TermMaker sees r) | r <- (npF (drop 1 quoted))]  
  | (quoted!! 0 == "sees")   = [(TermMaker sees r) | r <- (npF (drop 1 quoted))]
  | (quoted!! 0 == "admires")   = [(TermMaker admires r) | r <- (npF (drop 1 quoted))]  
    | (quoted!! 0 == "admire")   = [(TermMaker admires r) | r <- (npF (drop 1 quoted))] 
  | (quoted!! 0 == "loves")   = [(TermMaker loves r) | r <- (npF (drop 1 quoted))]
    | (quoted!! 0 == "love")   = [(TermMaker loves r) | r <- (npF (drop 1 quoted))]
  | (quoted!! 0 == "helps")   = [(TermMaker helps r) | r <- (npF (drop 1 quoted))]  
  | (quoted!! 0 == "help")   = [(TermMaker helps r) | r <- (npF (drop 1 quoted))]  
  | (quoted!! 0 == "hates")   = [(TermMaker hates r) | r <- (npF (drop 1 quoted))]
    | (quoted!! 0 == "hate")   = [(TermMaker hates r) | r <- (npF (drop 1 quoted))]
  | (quoted!! 0 == "doesn't-see")   = [(TermMaker not_sees r) | r <- (npF (drop 1 quoted))]
  | (quoted!! 0 == "doesn't-admire")   = [(TermMaker not_admires r) | r <- (npF (drop 1 quoted))]  
  | (quoted!! 0 == "doesn't-love")   = [(TermMaker not_loves r) | r <- (npF (drop 1 quoted))]
  | (quoted!! 0 == "doesn't-help")   = [(TermMaker not_helps r) | r <- (npF (drop 1 quoted))]  
  | (quoted!! 0 == "doesn't-hate")   = [(TermMaker not_hates r) | r <- (npF (drop 1 quoted))]
  | (quoted!! 0 == "don't-see")   = [(TermMaker not_sees r) | r <- (npF (drop 1 quoted))]
  | (quoted!! 0 == "don't-admire")   = [(TermMaker not_admires r) | r <- (npF (drop 1 quoted))]  
  | (quoted!! 0 == "don't-love")   = [(TermMaker not_loves r) | r <- (npF (drop 1 quoted))]
  | (quoted!! 0 == "don't-help")   = [(TermMaker not_helps r) | r <- (npF (drop 1 quoted))]  
  | (quoted!! 0 == "don't-hate")   = [(TermMaker not_hates r) | r <- (npF (drop 1 quoted))]
  | (quoted!! 0 == "r")   = [(TermMaker r blurt) | blurt <- (npF (drop 1 quoted))]
  | otherwise = []

{--
intTF quoted 
  |  (quoted !! 0 == ["skunks"])              =  [(IntersectionTerm (PCN Pos Skunks)  x) |  x <- (map tF (drop 1 quoted))]
  |  quoted !! 0 == ["mammals"]           = [CNasTerm mammals]
  |  quoted  !! 0== ["chordates"]               = [CNasTerm chordates]
  |  quoted  !! 0== ["boys"]                      = [CNasTerm boys]
  |  quoted !! 0 == ["girls"]                      = [CNasTerm girls]
  |  quoted !! 0 == ["dogs"]                      = [CNasTerm dogs]
  |  quoted !! 0 == ["cats"]                      = [CNasTerm cats]
  |  quoted !! 0 == ["birds"]                      = [CNasTerm birds]
  |  quoted !! 0 == ["animals"]                      = [CNasTerm animals] 
  |  quoted !! 0 == ["sneetches"]                      = [CNasTerm sneetches]
  | otherwise = []
--}

npF x    --- this parses noun phrases
  | x == []                              = []
  | (x!! 0 == "all")         = [(TermNP All w)    |  w <- tF (drop 1 x)]
  | (x!! 0 == "some")         = [(TermNP Some w)    |  w <- tF (drop 1 x)] 
  | (x!! 0 == "no")         = [(TermNP No w)    |  w <- tF (drop 1 x)]
  | (x!! 0 == "most")         = [(TermNP Most w)    |  w <- tF (drop 1 x)] 
  | otherwise = []  
  
readS  input =    --- this parses sentences
   let
      w = words input
      firstWord = head w
      y = tail w
      sp = split2 y
      tr = [ x | x <- (map (map tF) sp), (x!!0) /= [], (x!!1) /= []]
      a =  head $ head $ head tr
      b = head $ head $ tail $ head tr
      output 
         | firstWord == "all"   =  Sent All a b
         | firstWord == "some"   =  Sent Some a b  
         | firstWord == "most"   =  Sent Most a b
         | firstWord == "atleast"  = Sent Atleast a b
         | firstWord == "more"  = Sent More a b
         | firstWord == "no"   =  Sent No a b
         | firstWord == "All"   =  Sent All a b
         | firstWord == "Some"   =  Sent Some a b  
         | firstWord == "Most"   =  Sent Most a b
         | firstWord == "No"   =  Sent No a b
   in output
   
readSs = map readS

toMaybe :: Foldable t => t a -> Maybe a
toMaybe = foldl (maybe Just (const . Just)) Nothing


readS' :: String -> Maybe Sent
readS' input = case words input of
  w0:ws -> do
    q <- lookup (toLower <$> w0)
      [ ( "all"     , All     )
      , ( "some"    , Some    )
      , ( "most"    , Most    )
      , ( "atleast" , Atleast )
      , ( "more"    , More    )
      , ( "no"      , No      )
      ]
    (a,b) <- listToMaybe
      $ split2' ws >>= uncurry zip . (tF *** tF)
    return $ Sent q a b
  _ -> Nothing

-- return either the strings which failed to be parsed,
-- or the full set of parsed sentences.
readSs' :: [String] -> Either [String] [Sent]
readSs' = foldr rS $ Right []
  where
  rS :: String -> Either [String] [Sent] -> Either [String] [Sent]
  rS s es = case readS' s of
    Just s' -> case es of
      Left  bad  -> Left bad
      Right good -> Right $ s' : good
    Nothing   -> case es of
      Left  bad  -> Left $ s : bad
      Right good -> Left [s]


type RuleName = String
data Rule = Rule {rulename :: RuleName, 
  premises :: [Sent], 
  conclusion :: Sent}
  deriving (Show, Eq)
type RuleList = [Rule] 
 
junk = Rule {rulename  = "junk",  premises = readSs ["all x x", "all y y"] , conclusion = readS "all x y"}  
 
anti =   Rule {rulename  = "anti",  premises = readSs ["all x y"] , conclusion = readS "all non-y non-x"}
barbara = Rule {rulename  = "barbara",  premises = readSs ["all x y", "all y z"] , conclusion = readS "all x z"} 
some1 = Rule {rulename  = "some1",  premises = readSs ["some x y"], conclusion = readS "some x x"}
some2 = Rule {rulename  = "some2",  premises = readSs ["some x y"], conclusion = readS "some y x"}
darii =  Rule {rulename  = "darii",  premises = readSs ["all y z", "some x y"],  conclusion = readS "some x z"}
zero =  Rule {rulename  = "zero",  premises = readSs ["all x non-x"], conclusion =readS "all x y"}
one =  Rule {rulename  = "one",  premises = readSs ["all non-x x"], conclusion =readS "all y x"}
axiom =  Rule {rulename  = "axiom",  premises = [], conclusion =readS "all x x"}
exFalso = Rule {rulename  = "X",   premises = readSs ["some x y", "all x non-y"], 
     conclusion = Sent Contradiction (CNasTerm x)  (CNasTerm y) }
sdagger = [anti,barbara,some1, some2, darii,zero,axiom,exFalso]

antiARC = Rule {rulename  = "anti",  premises = [Sent All Ter1 Ter2], conclusion = (Sent All (TermMaker r (TermNP All Ter2)) (TermMaker r (TermNP All Ter1)))}
barbaraARC  = Rule {rulename  = "barbara",  premises = [Sent All Ter1 Ter2, Sent All Ter2 Ter3],   conclusion =(Sent All Ter1 Ter3)}
allARC = Rule {rulename  = "down",  premises = [Sent All Ter1 Ter2, Sent All Ter3 (TermMaker r (TermNP All Ter2)) ], conclusion = (Sent All Ter3 (TermMaker r (TermNP All Ter1)))}





data PTree a = T  a  [PTree a]    
   deriving (Show, Eq)

lineNumberHelp :: [(a, [Int], Int)] ->  [(a, [Int], Int)]  ->  [(a, [Int], Int)]
lineNumberHelp firstseq  secondseq =
     let     
              n = if null firstseq then 0 else (get3 $ head firstseq)
              modify  w = map ( \ (x, listofInts, k) -> (x, (map (\ i -> 1 + n+i) listofInts), k)) w
     in  (firstseq ++ modify secondseq)         
              
------ near of a PTree lists the nodes in depth-first order, along with an extra list for each node.
------ for the node n in the tree it lists the addresses of the children of n in the same tree, again in the 
------ depth-first order of the tree overall.    Getting this right was probably the hardest part of this whole exercise.
------ Note also that what we want in the end is not the depth-first listing of the PTree but rather the 'bottom-up' listing,
------ and these are related by
------     
------                       bottom_up t = reverse (depth_first ( tree_reverse t))
 
near :: (PTree  a) -> [(a, [Int], Int)]
near (T x l) = [(x,s, k+1 )] ++ extrastuff
    where  
                k =  sum r
                --extrastuff :: [(a, [Int], Int)] 
                extrastuff =  foldl lineNumberHelp []  (map near l)
                --q :: [(a, [Int], Int)] 
                q = map head $ map near l               
                r :: [Int]
                r = map get3 q
                s = init( scanl (+) 2 r)
               
tree_reverse (T n t) = T n (map tree_reverse (reverse t))
 
full_reverse ::  [(a, [Int], Int)] -> [(Int, a, [Int])]
full_reverse h = 
   let 
        n = length h
        p = [(i,  reverse( map (\ x -> n  + 1 - x) j )) | (i,j,k) <- h]
        q = reverse p
        w = [1..n]
        mergeMe :: [Int] -> [(a,[Int])] -> [(Int,a,[Int])]
        mergeMe  [] [] = []
        mergeMe (i:wMore)  (pair:pMore) = (i, (fst pair), (snd pair)) : (mergeMe wMore pMore)
   in  mergeMe w q
         



dropList :: [Int]  -> Int -> [Int]
dropList list x = [i  | i <- list, i /= x]
dropM :: M -> Int -> M
dropM m x = M { noun = (noun m), items = (dropList (items m) x) }
dropVb :: Vb -> Int -> Vb
dropVb v x = Vb { verb = (verb v), verb_items = [(i,j) | (i,j) <- verb_items v, i/= x, j/= x]}
dropModel :: Model -> Int -> Model
dropModel m x = Model { universe = (dropList (universe m) x), cnDict = map (\ n -> (dropM n x)) (cnDict m) ,    verbDict = map (\ v -> (dropVb v x))  (verbDict m) }

consecutiveDropList  :: [Int]  -> Int -> [Int]
helpForConsecutiveDrop :: Int -> Int -> Int
helpForConsecutiveDrop k l =   if k < l then k else k -1 
consecutiveDropList list x = [helpForConsecutiveDrop i x  | i <- list, i /= x]
consecutiveDropM m x = M { noun = (noun m), items = (consecutiveDropList (items m) x) }
consecutiveDropVb :: Vb -> Int -> Vb
consecutiveDropVb v x = Vb { verb = (verb v), verb_items = [(helpForConsecutiveDrop i x, helpForConsecutiveDrop j x) | (i,j) <- verb_items v, i/= x, j/= x]}
consecutiveDropModel :: Model -> Int -> Model
consecutiveDropModel m x = Model { universe = (consecutiveDropList (universe m) x), cnDict = map (\ n -> (consecutiveDropM n x)) (cnDict m) ,    verbDict = map (\ v -> (consecutiveDropVb v x))  (verbDict m) }

maybeDrop model x gamma =
     let
         mNew =  consecutiveDropModel model x   --- was dropModel, not consecutiveDropModel
         tvs = map (\ s  -> (semanticsSent s mNew)) gamma
     in 
         if (and tvs) then mNew else model

shorten :: Model -> [Sent] -> Model
shorten model gamma = foldl  (\ m -> (\ x -> maybeDrop m x gamma)) model (universe model)

iterativelyShorten model gamma = if (model == shorten model gamma) then model else (iterativelyShorten (shorten model gamma) gamma)

{--dropALot m gamma = foldl (\acc x -> listU m) (listU m)
--}
data SentencesInModel = SentencesInModel { sentFromModels :: String,  truthvalueOfSent :: [Bool]}
    deriving Show

data M = M { noun  :: CN,  items :: [Int] }
    deriving (Eq, Show) 

data Vb = Vb { verb  :: V,  verb_items :: [(Int,Int)] }
    deriving (Eq,Show)     

type Universe = [Int]
data Model  = Model {universe::Universe, cnDict ::  [M], verbDict :: [Vb]} 
      deriving (Eq,Show)

semanticsTerm :: Term -> Model -> [Int]
semanticsTerm (CNasTerm (PCN Pos cn)) m  =  helper (CNasTerm (PCN Pos cn)) (cnDict m)
semanticsTerm (CNasTerm (PCN Neg cn)) m =    (universe m) \\ semanticsTerm (CNasTerm (PCN Pos cn)) m 
semanticsTerm (TermMaker (PV Pos tv) (TermNP All t)) m  =
    let 
        u = universe m
        tt = semanticsTerm t m
        vv = verbHelper tv (verbDict m)
    in
        [ x | x <- u, and (map (\ y -> implies (y `elem` tt) ((x,y) `elem` vv)) u)] 

semanticsTerm (TermMaker (PV Pos tv) (TermNP Some t)) m  =
    let 
        u = universe m
        tt = semanticsTerm t m
        vv = verbHelper tv (verbDict m)
    in
        [ x | x <- u, or (map (\ y -> (y `elem` tt) && ((x,y) `elem` vv)) u)] 

semanticsTerm (TermMaker (PV Neg tv) (TermNP All t)) m  =
    let 
        u = universe m
        tt = semanticsTerm t m
        vv = verbHelper tv (verbDict m)
    in
        [ x | x <- u, and (map (\ y -> implies (y `elem` tt) (not ((x,y) `elem` vv))   ) u)] 

semanticsTerm (TermMaker (PV Neg tv) (TermNP Some t)) m  =
    let 
        u = universe m
        tt = semanticsTerm t m
        vv = verbHelper tv (verbDict m)
    in
        [ x | x <- u, or (map (\ y ->  (y `elem` tt) && (not ((x,y) `elem` vv))   ) u)] 

helper (CNasTerm (PCN Pos cn))  partialList  
    | null partialList                                  =  []
    | cn == (noun $ head $ partialList)    =  items $ head  partialList
    | otherwise                                         = helper (CNasTerm (PCN Pos cn))  (tail partialList)

implies b c = (not b) ||  c

verbHelper v  vList  
    | null vList                                  =  []
    | v == (verb $ head $ vList)    =  verb_items $ head  vList
    | otherwise                                         = verbHelper v  (tail vList)

semanticsSent :: Sent -> Model -> Bool
semanticsSent (Sent All t1 t2) m  = and ( map (\ x -> x `elem` s2) s1)
     where 
                s1 = semanticsTerm t1 m
                s2 = semanticsTerm t2 m

semanticsSent (Sent Some t1 t2) m  = or (map (\ x -> x `elem` s2) s1)
     where
                s1 = semanticsTerm t1 m
                s2 = semanticsTerm t2 m

semanticsSent (Sent No t1 t2) m =  and ( map (\ x -> not (x `elem` s2)) s1)
     where 
                s1 = semanticsTerm t1 m
                s2 = semanticsTerm t2 m

semanticsSent (Sent Most t1 t2)  m = 
   let   
      s1 = semanticsTerm t1 m
      s2 = semanticsTerm t2 m
      intersection = s1 `intersect` s2
      n = length s1
      k = length intersection
   in
      n < 2 * k  

semanticsSent (Sent Atleast t1 t2)  m = 
   let   
      s1 = semanticsTerm t1 m
      s2 = semanticsTerm t2 m
   in
      s2 <= s1        

semanticsSent (Sent More t1 t2)  m = 
   let   
      s1 = semanticsTerm t1 m
      s2 = semanticsTerm t2 m
   in
      s2 < s1                    

---------   pretty printing of models below

data U = U {name::String, itemsU :: [Int] }
    deriving Show     

transMtoU t  = (U (show(noun t)) (items t))

data Vextra = Vextra { verbextra  :: String,  verb_items_extra :: [(Int,Int)] }
    deriving Show     

transVtoVextra t  = (Vextra (show(verb t)) (verb_items t))

-- a type for fill functions
type Filler = Int -> String -> String

-- a type for describing table columns
data ColDesc t = ColDesc
  { colTitleFill :: Filler
  , colTitle     :: String
  , colValueFill :: Filler
  , colValue     :: t -> String
  }

-- test data
test =
    [ M Cats     [1,2,3],
     M Dogs    [4,5,6],
     M Skunks [1,3,5,6], 
     M Chordates  [ ]
    ]
    
vTest = [Vb Sees [(1,1),(1,4),(3,4),(2,5)]]    

model1 = Model {universe = [1,2,3,4,5,6], cnDict = test, verbDict = vTest}

-- functions that fill a string (s) to a given width (n) by adding pad
-- character (c) to align left, right, or center
fillLeft c n s = s ++ replicate (n - length s) c
fillRight c n s = replicate (n - length s) c ++ s
fillCenter c n s = replicate l c ++ s ++ replicate r c
    where x = n - length s
          l = x `div` 2
          r = x - l

-- functions that fill with spaces
newleft = fillLeft ' '
right = fillRight ' '
center = fillCenter ' '
--showTable :: [ColDesc t] -> [t] -> String


showTable cs ts =
    let header = map colTitle cs
        rows = [[colValue c t | c <- cs] | t <- ts]
        widths = [maximum $ map length col | col <- transpose $ header : rows]
        separator = intercalate "-+-" [replicate width '-' | width <- widths]
        fillCols fill cols = intercalate " | " [fill c width col | (c, width, col) <- zip3 cs widths cols]
    in
        unlines $ fillCols colTitleFill header : separator : map (fillCols colValueFill) rows
   
showModelNounsPlusJustifications m gamma phi = do
  putStrLn ("The universe is the set of numbers in " ++ show(universe m)++".")   
  putStrLn " "
  putStrLn "The nouns are interpreted as follows:"
  putStrLn " "
  showNouns m
  putStrLn " "
  putStrLn "Here is how the assumptions and purported conclusion fare in this model:"
  putStrLn " "
  showSentenceTruthValues m $ gamma++[phi]

showModelNounsVerbsPlusJustifications m gamma phi = do
  putStrLn ("The universe is the set of numbers in " ++ show(universe m)++".")   
  putStrLn " "
  putStrLn "The nouns and verbs are interpreted as follows:"
  putStrLn " "
  showNouns m
  putStrLn " "     
  showVerbs m   
  putStrLn "Here is how the assumptions and purported conclusion fare in this model:"
  putStrLn " "
  showSentenceTruthValues m $ gamma++[phi]

showModelNounsOnly m = do
  putStrLn ("The universe is the set of numbers in " ++ show(universe m)++".")   
  putStrLn " "
  putStrLn "The nouns are interpreted as follows:"
  putStrLn " "
  showNouns m

showModel m = do
  putStrLn ("The universe is the set of numbers in " ++ show(universe m)++".")   
  putStrLn " "
  putStrLn "The nouns are interpreted as follows:"
  putStrLn " "
  showNouns m
  putStrLn "The transitive verbs are interpreted as follows:"
  putStrLn " "     
  showVerbs m     

showNouns m = putStrLn $
  showTable
    [ ColDesc center "Noun"  newleft  name
    , ColDesc center "Interpretation"  newleft (intercalate ", " . map show . itemsU)
    ]
    $ map transMtoU (cnDict m)

showVerbs m = putStrLn $
  showTable
    [ ColDesc center "Verb"  newleft  verbextra
    , ColDesc center "Interpretation"  newleft (intercalate ", " . map show . verb_items_extra)
    ]
    $ map transVtoVextra (verbDict m)

--- showGeneric below is used in showModelPlus             
showGeneric m nameLabel contentLabel recordList = putStrLn $
  showTable
    [ ColDesc center "Term"  newleft  nameLabel
    , ColDesc center "Interpretation" newleft (intercalate ", " . map show . contentLabel)
    ] recordList        

makeSentenceEntry s m = SentencesInModel (show s)  [semanticsSent s m]

showSentenceTruthValues m gamma = putStrLn $
  showTable
    [ ColDesc center "Sentence"  newleft  sentFromModels
    , ColDesc center "Truth Value" newleft (intercalate ", "  . map show .  truthvalueOfSent )
    ] (map (\ x -> makeSentenceEntry x m) (gamma))

showModelPlus mod tList = do
  showModel mod
  putStrLn " "
  putStrLn "Extra information on the relevant terms:"
  putStrLn " "
  let rrrList = map (\ z ->   (U { name = (show z) ,  itemsU =  (semanticsTerm z mod) }) ) tList 
  showGeneric mod name itemsU rrrList

showModelNounsVerbsPlusJustificationsARC :: Model -> [Sent] -> Sent -> [Term] -> IO ()
showModelNounsVerbsPlusJustificationsARC m gamma phi tList = do
  putStrLn ("The universe is the set of numbers in " ++ show(universe m)++".")   
  putStrLn " "
  putStrLn "The nouns and verbs are interpreted as follows:"
  putStrLn " "
  showNouns m
  putStrLn " "     
  showVerbs m   
  putStrLn "Extra information on the relevant terms:"
  putStrLn " "
  let rrrList = map (\ z ->   (U { name = (show z) ,  itemsU =  (semanticsTerm z m) }) ) tList 
  showGeneric m name itemsU rrrList
  putStrLn "Here is how the assumptions and purported conclusion fare in this model:"
  putStrLn " "
  showSentenceTruthValues m (gamma++[phi])

{-
m gamma phi tList
-----------------
show (universe m)
showNouns n:
  showTable
    [ ColDesc center "Noun"  newleft  name
    , ColDesc center "Interpretation"  newleft (intercalate ", " . map show . itemsU)
    ]
    $ map transMtoU (cnDict m)
showVerbs m:
  showTable
    [ ColDesc center "Verb"  newleft  verbextra
    , ColDesc center "Interpretation"  newleft (intercalate ", " . map show . verb_items_extra)
    ]
    $ map transVtoVextra (verbDict m)
showGeneric m name itemsU (...):
  showTable
    [ ColDesc center "Term"  newleft  name
    , ColDesc center "Interpretation"  newleft (intercalate ", " . map show . itemsU)
    ] $ map (\ z -> U { name = show z, itemsU = semanticsTerm z m }) tList
showSentenceTruthValues m $ gamma ++ [phi]:
  showTable
    [ ColDesc center "Sentence"  newleft  sentFromModels
    , ColDesc center "Truth Value" newleft (intercalate ", "  . map show .  truthvalueOfSent )
    ]
    $ map (\ x -> makeSentenceEntry x m) $ gamma ++ [phi]
-}



{-# LANGUAGE PatternGuards #-}


get1 (a,b,c) = a
get2 (a,b,c) = b
get3 (a,b,c) = c

get1Of4 (a,b,c,d) = a
get2Of4 (a,b,c,d) = b
get3Of4(a,b,c,d) = c
get4Of4(a,b,c,d) = d

--firstHelp :: a -> [a] -> [[a]]                          
firstHelp x  []      =  []
firstHelp x (y:ytail)  =  (x,y) : firstHelp x ytail

--secondHelp  :: [a] -> [a] -> [[[a]]]   
secondHelp list ys = map (\ x -> firstHelp x ys) list                           

allFns list1 list2  =  sequence $ (secondHelp list1 list2)
 
lookfor  key ((a,b):abs)
    | key == a          =   b
        
emptyAsDefault :: Maybe [a] -> [a]
emptyAsDefault mx = case mx of
    Nothing -> []
    Just xy -> xy  
zeroAsDefault :: Maybe Int -> Int
zeroAsDefault mx = case mx of
    Nothing -> 0
    Just xy -> xy      
 
findD (Sent d t1 t2) = d    
g1 (Sent d t1 t2)  = t1
g2 (Sent d t1 t2)  = t2   

addAssumptionAsReason :: Sent -> (Sent, String, [Sent])
addAssumptionAsReason s = (s, "A", [])
addReasonsToOriginal :: [Sent] -> [(Sent,String,[Sent])] 
addReasonsToOriginal  = map addAssumptionAsReason

varsInConclusion :: Rule -> [Term] 
varsInConclusion r =  nub [g1 $ conclusion r, g2 $ conclusion r]

premiseExtractPairs :: Rule -> [(Term,Term)]
premiseExtractPairs  r = 
  let  f (Sent d t1 t2)  = (t1, t2) 
  in map f $ premises r
 
varsInPremises :: Rule -> [Term]
varsInPremises  r = concat [[a,b] | (a,b) <- premiseExtractPairs r]
  
  
extras :: Rule -> [Term]  
extras r  = (varsInConclusion r) \\  (varsInPremises  r)

-- I am not sure if 'extras' just above is used.  But the variants below are used.

extracnsInRule r =   nub $ (cnsIn (conclusion r) )  \\  (concatMap cnsIn (premises r))  
extraVerbsInRule r =   nub $ (verbsIn (conclusion r) )  \\  (concatMap verbsIn (premises r))  

fixDuplicates xs = nubBy conclusionsMatch xs
   where conclusionsMatch ys zs = 
                 get1 ys == get1 zs
  
--------------------------- here is where the main part of the code starts

buildPairOfSubs :: Sent -> [Sent] -> [(Sent, Maybe [(Term, Term)], Maybe [(PV, PV)])]
buildPairOfSubs sent sList = [(s, buildTermSub sent s,buildPVSub sent s) | s <- sList, Nothing /= buildTermSub sent s,  Nothing /= buildPVSub sent s ]

ruleToPairOfSubs :: Rule -> [Sent] -> [[(Sent, Maybe [(Term, Term)], Maybe [(PV, PV)])]]
ruleToPairOfSubs rule sList = map (\ x -> buildPairOfSubs x sList) (premises rule)

applicableInstances  :: Rule -> [Sent] -> [([Sent], [(Term, Term)], [(PV, PV)])]
applicableInstances  rule sList  =
   let 
        jj = sequence $ (ruleToPairOfSubs rule sList)
        checkerUnary x = foldl  combineStructures (Just [])  (map get2 x)
        checkerBinary x = foldl  combineStructures (Just [])  (map get3 x)
   in
       [((map get1 x), (emptyAsDefault $ checkerUnary x), (emptyAsDefault $ checkerBinary x)) | x <- jj,  Nothing /= checkerUnary x, Nothing /= checkerBinary x]
  

  
extraReconciliationVerbs rule sList = if extraVerbsInRule rule == [] then (applicableInstances  rule sList) else
    let 
        above = [[((PV Pos x),(PV Pos y))]  |  x <- (extraVerbsInRule rule), y<- verblistNotVars]
    in
        concatMap (\ y ->  (map (\ x -> (get1 x, get2 x , (get3 x ++ y))) (applicableInstances  rule sList ))) above


extraReconciliationCNs rule sList = if extracnsInRule rule == [] then (extraReconciliationVerbs rule sList) else   
    let 
        useThese =   nub $ concatMap cnsIn sList
        firstSet = [CNasTerm (PCN Pos cn1 ) |   cn1 <- (extracnsInRule rule)]
        secondSet =  [CNasTerm (PCN Pos cn2 ) |   cn2 <- useThese]
        firstSetNeg = [CNasTerm (PCN Neg cn1 ) |   cn1 <- (extracnsInRule rule)]
        secondSetNeg =  [CNasTerm (PCN Neg cn2 ) |   cn2 <- useThese]
        tv = or  $ map (hasNegativeMarker . pCNsIn) $ concatMap subterms sList
        extras = if tv then allFns firstSet secondSetNeg else [ ]
        subs = (allFns firstSet secondSet)  ++ extras 
   in
        concatMap (\ y ->  (map (\ x -> (get1 x, (get2 x ++ y) , get3 x)) (extraReconciliationVerbs rule sList ))) subs


 
render rule item = 
   let t = conclusion rule
       u = spellOut t (get2 item) (get3 item)
   in (u, (rulename rule), get1 item)

dropReasons = map get1
       

applyARule sList r  =  nub $ map (\ x -> render r x) (extraReconciliationCNs r sList)   

applyAllRules sListWithReasons rl  = 
  let 
      z = dropReasons sListWithReasons
      a = map (applyARule z) rl
      b = concat a
   in 
      fixDuplicates $ sListWithReasons  ++ b   


type SentRule = (Sent,String)
--data PTree = T (Sent,String)  [PTree]        ---- for development purposes, this declaration was moved to ProofTreeNumbers.hs
--   deriving (Show, Eq)



ll phi stumpset = 
   if (get1 $ (stumpset !! 0)) == phi then (stumpset !! 0) else  (ll phi (tail stumpset))

proofSearch phi stumpset = 
  T ((get1 a), (get2 a))  (map (\ x -> (proofSearch x stumpset)) (get3 a))
  where a = ll phi stumpset
 
    
firstRepeat (x:y:rest) = if x == y then x else  firstRepeat (y:rest)

allDerived :: [Sent] -> [Rule] -> [(Sent, RuleName, [Sent])]
allDerived noReasons rl = allDerivedUnderRepresentations noReasons rl
         

allDerivedUnderRepresentations noReasons rl=   firstRepeat $ fixedPoint addReasons rl
   where addReasons = addReasonsToOriginal  noReasons   
 
fixedPoint withReasons rl = withReasons : map (\ x -> applyAllRules x rl) (fixedPoint withReasons rl)

fullStory noReasonList ruleList = fullStoryUnderRepresentations (readSs noReasonList) ruleList
--- e.g.   fullStory ["all skunks mammals", "some mammals non-chordates"] sdagger

--fullStoryUnderRepresentations :: AssumptionList -> [Rule] -> IO ()
fullStoryUnderRepresentations noReasonList ruleList  = mapM_ print  $ map get1 $ allDerivedUnderRepresentations   noReasonList  ruleList

modify outputList  = map (\ x -> (get1 x, fst (get2 x), snd(get2 x), get3 x)) outputList

--  let stumpset = allDerived [s8,s12] sList
-- let phi = get1 $ stumpset !! 13
findProofByNumber n ch  = mapM_ print $ modify . full_reverse . near . tree_reverse $ proofSearch (get1 (ch !! n)) ch

inconsistency stumpset =
  let 
      q = map get1 stumpset
      --qq = map principalDet q
  in
      dropWhile  (\ s -> Contradiction /=  principalDet s)q 
   
--  relevantChunk is NOT USED!

relevantChunk phi gamma ruleList =       
    let
      addReasons = addReasonsToOriginal  gamma 
      bingo = fixedPoint addReasons ruleList
      firstRepeatOrFind  (x:y:rest)  
           |  phi `elem` (map get1 x)                      =  x
           |  (inconsistency x)  /=   []                       = x
           |  x == y                                                 =  x   
           |  otherwise                                            =  firstRepeatOrFind (y:rest)
   in firstRepeatOrFind bingo     

      
follows phi gamma ruleList = followsUnderRepresentation (readS phi) (readSs gamma) ruleList
     
followsUnderRepresentation phi gamma ruleList = 
   let
      addReasons = addReasonsToOriginal  gamma 
      bingo = fixedPoint addReasons ruleList
      firstRepeatOrFind  (x:y:rest)  
          |  phi `elem` (map get1 x)                      =  do
                           putStrLn " "
                           putStrLn "The sentence follows, and here is a derivation in the given logic from the assumptions:"
                           putStrLn " "
                           mapM_ print $ modify .  full_reverse $ near $ tree_reverse $ proofSearch phi  x
                           putStrLn " "
          |  (inconsistency x)  /=   []                       = do
                           putStrLn " "
                           putStrLn "As shown below, the list of assumptions is inconsistent, so every sentence follows."
                           putStrLn " "
                           mapM_ print $ modify .  full_reverse $ near $ tree_reverse $ proofSearch (head $ (inconsistency x)) x
          |  x == y                                                 =  do   
                           putStrLn " "
                           putStrLn "The given sentence is not provable from the assumptions in the logic."
                           putStrLn " "
          |  otherwise                                            =  firstRepeatOrFind (y:rest)
   in firstRepeatOrFind bingo        
   
---   :set +s  for timing



----  EXTRA STUFF TO TRY TO PRETTY-PRINT THE PROOFS IN 3 NICE COLUMNS
---- SO FAR, NO LUCK!

--import Data.List (transpose, intercalate)


-- a type for records
data K = K { make  :: String
           , model :: String
            , modell :: String
           , years :: [Int] }
    deriving Show




    
    
data SToPrint = SToPrint { lineToPrint  :: Int
           , sentToPrint :: Sent
            , ruleToPrint :: RuleName
           , reasonsToPrint :: [Int] }
    deriving Show    




-- functions that fill with spaces

type Proof       = [(Int,Sent,RuleName,[Int])]
type ProofChunk  = [(Sent,RuleName,[Sent])]
type StopList    = [Term]

oneStepARC :: StopList
           -> ProofChunk
           -> ProofChunk
oneStepARC stopList gammaWithReasons = 
  fixDuplicates $ gammaWithReasons ++
    filter (checkARC stopList . get1)
      ( concatMap
        (applyARule $ dropReasons gammaWithReasons)
        [ antiARC
        , barbaraARC
        , axiom
        ]
      )

checkARC :: StopList
         -> Sent
         -> Bool
checkARC stopList (Sent _ t _) = t `elem` stopList

followsInARC :: [String] -> String -> IO ()
followsInARC gamma phi =
  either
  -- either (\x -> Left ( modelBuildARC stopList x , stopList , map get1 x )) Right
  ( \x -> do
    putStrLn $ unlines
      [ "The given sentence is not provable from the assumptions in ARC."
      , ""
      , "Here is a counter-model:"
      , ""
      ]
    showCounterModel gamma' phi' x
    putStrLn $ unlines
      [ ""
      , "And here is the list of sentences which do follow, and with restrictions:"
      , ""
      ]
    mapM_ (print . get1) x
    putStrLn ""
  )
  ( \p -> do
    putStrLn $ unlines
      [ "The sentence follows from the assumptions in ARC."
      , ""
      , "Here is a derivation:"
      , ""
      ]
    mapM_ print p
    putStrLn ""
  )
  $ followsInARCUnderRepresentations gamma' phi'
  where
  gamma'   = readSs gamma
  phi'     = readS phi
  stopList = mkStopList gamma' phi'

showCounterModel :: [Sent] -> Sent -> ProofChunk -> IO ()
showCounterModel gamma phi x =
  showModelNounsVerbsPlusJustificationsARC
    (modelBuildARC stopList x)
    gamma
    phi
    stopList
  where
  stopList = mkStopList gamma phi

followsInARCUnderRepresentations :: [Sent] -> Sent -> Either ProofChunk Proof
followsInARCUnderRepresentations gamma phi = 
  findFixedPointOrSat (oneStepARC stopList)
    ( \x -> if phi `elem` map get1 x then Just $ numberProof phi x else Nothing
    )
  $ addReasonsToOriginal gamma
  where
  stopList = mkStopList gamma phi

numberProof :: Sent -> ProofChunk -> Proof
numberProof phi = modify . full_reverse . near . tree_reverse . proofSearch phi

justCounterModelARC :: [Sent] -> Sent -> Model
justCounterModelARC gamma phi = 
  modelBuildARC stopList
  $ findFixedPoint (oneStepARC stopList)
  $ addReasonsToOriginal gamma
  where
  stopList = mkStopList gamma phi

findFixedPointOrSat :: Eq a => (a -> a) -> (a -> Maybe b) -> a -> Either a b
findFixedPointOrSat f p = loop
  where
  loop x
    | Just y <- p x = Right y
    | x == f x      = Left  x
    | otherwise     = loop $ f x

findFixedPoint :: Eq a => (a -> a) -> a -> a
findFixedPoint f = either id id . findFixedPointOrSat f (\_ -> Nothing)

mkStopList :: [Sent] -> Sent -> StopList
mkStopList gamma phi = nub $ concatMap subterms $ gamma ++ [phi]

{-
countermod :: [Sent]
           -> Sent
           -> StopList
           -> ProofChunk
           -> IO ()
countermod gamma phi stpList chunk =
  showModelNounsVerbsPlusJustificationsARC m gamma phi stpList    -- !!!! PUT THIS BACK FOR the FULL MODELS
  -- showModelNounsVerbsPlusJustificationsARC mShortened gamma phi stpList    -- !!! PUT THIS BACK FOR SMALLER MODELS
  where
  m = modelBuildARC stpList chunk   -- !!!! USE THIS AND THIS ONLY FOR the FULL MODELS
  -- mShortened = iterativelyShorten m (gamma++[negation phi])   -- !!!! PUT THIS BACK FOR SMALLER MODELS
-}

modelBuildARC :: StopList
              -> ProofChunk
              -> Model
modelBuildARC stopList chunk = Model
  { universe = uni
  , cnDict   = map
               ( \p ->
                 M p $ cnInterpretationFn p
               ) relevantCNs
  , verbDict = map
               ( \transverb ->
                 Vb transverb
                 $ tvInterpretationFn transverb
               ) relVerbs
  }      
  where
  uni         = [ 0 .. length stopList - 1 ]
  sList       = map get1 chunk
  relVerbs    = nub $ concatMap verbsIn sList
  relevantCNs = nub $ concatMap cnsIn sList
  order       = map pairOfTerms sList
  cnInterpretationFn cn =
    [ r
    | r <- uni
    , (stopList !! r , CNasTerm $ PCN Pos cn) `elem` order
    ]
  tvInterpretationFn tv =
    [ (r,s)
    | r <- uni
    , s <- uni
    , (stopList !! r, TermMaker (PV Pos tv) (TermNP All (stopList !! s)))  `elem` order
    ]
  termInterpretationFn t =
    ( t
    , [ r
      | r <- uni
      , (stopList !! r , t) `elem` order
      ]
    )

pairOfTerms :: Sent -> (Term,Term)
pairOfTerms (Sent _ t u) = (t,u)

-- Here is a test of the main example in Chapter 2

tSkunks, tMammals, tChordates, tSkunks2 :: Term
tSkunks    = TermMaker sees (TermNP All  (CNasTerm skunks) )
tMammals   = TermMaker sees  (TermNP All  (CNasTerm mammals))
tChordates = TermMaker sees  (TermNP All  (CNasTerm chordates))
tSkunks2   = TermMaker sees (TermNP All  tSkunks )

testCh2gamma :: [Sent]
testCh2gamma =
  [ Sent All (CNasTerm skunks) (CNasTerm chordates)
  , Sent All tMammals tSkunks2
  , Sent All tSkunks2 (CNasTerm mammals)
  ]

testCh2phi :: Sent
testCh2phi = Sent All tSkunks tChordates

--followsInARCUnderRepresenatations testCh2phi testCh2gamma

tCh2gamma :: [String]
tCh2gamma =
  [ "all skunks chordates"
  , "all see all mammals see all see all skunks"
  , "all see all see all skunks mammals"
  , "all mammals see all chordates"
  ]

tCh2phi :: String
tCh2phi = "all see all skunks see all chordates"

tCh2_run :: IO ()
tCh2_run = followsInARC tCh2gamma tCh2phi

-- followsInARC tCh2phi tCh2gamma

-- The specific mapping to Chapter 2 is
-- skunks --> hawks
---chordates --> birds
-- mammals -> turtles

-- 0  hawks
-- 1 birds
-- 2 see all turtles
-- 3 turtles
-- 4 see all see all hawks
-- 5 see all hawks
-- 6 see all birds



-- here  there
---  0        1
---  1        6
---  2        5
---  3
---  4
---  5
---  6

test2 :: [M]
test2 =
  [ M Chordates [3,4]
  , M Birds     [1,2,5]
  , M Skunks    [2]
  ]

vTest2 :: [Vb]
vTest2 =
  [ Vb Sees  [(1,2),(1,3), (2,1), (2,5), (3,1), (3,3), (3,4), (3,5), (4,3), (4,4), (5,2), (5,3)],        
    Vb Loves [(1,1),(1,2), (1,3), (1,5), (2,1), (3,3), (5,2), (5,5)] ,
    Vb Hates [(2,1),(3,4), (5,1),  (5,2), (5,3), (5,4)] 
  ]

model2 :: Model
model2 = Model
  { universe = [1,2,3,4,5]
  , cnDict   = test2
  , verbDict = vTest2
  }

--- A GOOD TEST IS BELOW
--- followsInARC "all who see all who hate all skunks see all who love all mammals" ["all mammals hate all skunks", "all skunks see all skunks", "all who love all mammals are skunks", "all boys see all who love all skunks", "all who see all boys are mammals"]

-- followsInARC "all who see all who hate all skunks see all who love all mammals" ["all mammals see all skunks", "all skunks see all skunks", "all who love all mammals are skunks", "all boys see all who love all skunks", "all who see all boys are mammals"]

-- followsInARC "all who see all who hate all skunks see all who love all mammals" ["all mammals hate all skunks", "all skunks see all skunks", "all who love all mammals are skunks", "all boys see all who love all skunks", "all who see all boys are mammals", "all who see all boys see all skunks", "all who see all skunks love all skunks"]