ARCwithDown.hs

{-# LANGUAGE PatternGuards #-}

module AllVerbsRelativeClausesPrime where

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

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)
        [ downARC
        , 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

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