AllVerbsRelativeClauses.hs

{-# LANGUAGE PatternGuards #-}

module AllVerbsRelativeClauses where


import Data.List
import Control.Monad
import ARC/Syntax2
import ARC/FrontEnd
import ARC/SyllogisticInference
import ARC/ExampleSentences
import ARC/ExampleRules
import ARC/ProofTreeNumbers
import ARC/Models

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

termEval x = semanticsTerm (head $ tF $ words x)

-- allVerbsIn gamma =  nub $ concatMap verbsIn (readSs gamma)

-- tryOneStep  z = applyAllRules z [antiARC, barbaraARC, axiom]

syntaxCheck :: String -> IO()
syntaxCheck x =
  case (inARC (readS  x)) of
     (Just True) -> putStrLn $  "Looks good!"
     (Just False) -> putStrLn $ "Sorry, not in the fragment of this notebook"
     Nothing -> putStrLn $ "Sorry, invalid input"

evaluate :: Model -> String -> Bool
evaluate m s = semanticsSent (readS s) m
{--

allTerms gamma n = nub $ concatMap subterms $  map get1 $ (infiniteSeq gamma (head gamma )) !! n


infinitelyManyModels gamma n =
   showSentenceTruthValues m (readSs gamma)
   where
     r = infiniteSeq gamma (head gamma)
     a =  r!! 2
     t = allTerms gamma n
     m = modelBuildARC t a

--}

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

{--
oldFollowsInARC :: [String] -> String -> IO ()
oldFollowsInARC 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
      [ ""
      , "The model is built using the sentences below, all of which do follow from the assumptions:"
      , ""
      ]
    mapM_ (print . get1) x
    putStrLn ""
  )
  ( \p -> do
    putStrLn $ unlines
      [ "The conclusion follows from the assumptions in ARC."
      , ""
      , "Here is a derivation:"
      ]
    putStrLn $ showTableForProofs [ ColDesc center " "  left  (show . line)
                     , ColDesc center " "  left  (show. sentence)
                     , ColDesc center " " left  rule
                     , ColDesc center " "  right (intercalate ", " . map show . supports)
                     ] $ map (\k -> ProofLine {line= get1Of4 k, sentence=get2Of4 k, rule = get3Of4 k, supports = get4Of4 k})  p
    putStrLn $ unlines ["", "",""]
  )
  $ followsInARCUnderRepresentations gamma' phi'
  where
  gamma'   = readSs gamma
  phi'     = readS phi
  stopList = mkStopList gamma' phi'

  -- last few lines above
    --p  -- NOTE THE LINE BELOW!
    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

--trivialExtension :: [Sent] -> Sent -> [Sent]
--trivialExtension gamma phi =  gamma  ++ (dropReasons $  applyARule [phi] axiom)




mkProofChunk gamma = addReasonsToOriginal $ readSs gamma
mkStopLforInfinite gamma = mkStopL $ readSs gamma

followsInARCUnderRepresentations :: [Sent] -> Sent -> Either ProofChunk Proof
followsInARCUnderRepresentations gamma phi =
  --findFixedPointOrSat (oneStepARC2 stopList (concatMap cnsIn $ readSs $ gamma ++ [phi] ) (concatMap verbsIn $ readSs $ gamma ++ [phi]))
  findFixedPointOrSat (oneStepARC stopList)
    ( \x -> if phi `elem` map get1 x then Just $ numberProof phi x else Nothing
    )
  $ (addReasonsToOriginal $ gamma)   ++  (applyARule [phi] axiom)   --- this did not have the applyARule part!
  where
  stopList = mkStopList gamma phi


 --- revised stuff below

oneStepARC2 stopList gammaWithReasons x y =
  fixDuplicates $ gammaWithReasons ++
    filter (checkARC stopList . get1) (applyAllRules2 gammaWithReasons [antiARC,barbaraARC,axiom] x y)


f gamma phi =
   findFixedPointOrSat
         (\ w -> oneStepARC2 stopList w b c)
         ( \x -> if p `elem` map get1 x then Just $ numberProof p x else Nothing)
         y
   where
         a = readSs $  gamma ++ [phi]
         b = concatMap cnsIn a
         c = concatMap verbsIn a
         y =  mkProofChunk gamma
         p = readS phi
         stopList = mkStopL a



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
      [ ""
      , "The model is built using the sentences below, all of which do follow from the assumptions:"
      , ""
      ]
    mapM_ (print . get1) x
    putStrLn ""
  )
  ( \p -> do
    putStrLn $ unlines
      [ "The conclusion follows from the assumptions in ARC."
      , ""
      , "Here is a derivation:"
      ]
    putStrLn $ showTableForProofs [ ColDesc center " "  left  (show . line)
                     , ColDesc center " "  left  (show. sentence)
                     , ColDesc center " " left  rule
                     , ColDesc center " "  right (intercalate ", " . map show . supports)
                     ] $ map (\k -> ProofLine {line= get1Of4 k, sentence=get2Of4 k, rule = get3Of4 k, supports = get4Of4 k})  p
    putStrLn $ unlines ["", "",""]
  )
  $ (f gamma phi)
  where
  gamma'   = readSs gamma
  phi'     = readS phi
  stopList = mkStopList gamma' phi'

infiniteSeq gamma  phi  =  x
   where
         a = readSs $  gamma ++ [phi]
         b = concatMap cnsIn a
         c = concatMap verbsIn a
         y =  mkProofChunk gamma
         stopList = mkStopL a
         x = y :  map (\ w -> oneStepARC2 stopList w b c ) x


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)

mkStopL :: [Sent]  -> StopList
mkStopL gamma  =
    nub $ concatMap subterms $ gamma

mkStopList :: [Sent] -> Sent -> StopList
mkStopList gamma phi = mkStopL $ 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

--followsInARCUnderRepresentations 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"]


--}