AllVerbsRelativeClausesLM.hs

module AllVerbsRelativeClausesLM where

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


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

allVerbsIn gamma =  nub $ concatMap verbsIn (readSs gamma)

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

oneStepARC gammaWithReasons  stopList =
   let
        z = dropReasons gammaWithReasons
        a = map (applyARule z)  [antiARC, barbaraARC,axiom]  -- was antiARC
        b = concat a
   in
        fixDuplicates $ gammaWithReasons ++ [ s | s <- b, checkARC stopList (get1 s)]


filterAfterApply stopList x = [ s | s <- x, checkARC stopList s]
checkARC stopList (Sent d t u) = (t `elem` stopList)

fixedPointARC gammaWithReasons  stopList =  gammaWithReasons : map (\ x -> oneStepARC x stopList )(fixedPointARC gammaWithReasons  stopList)

followsInARC phi gamma  = followsInARCUnderRepresenatations (readS phi) (readSs gamma)
followsInARCUnderRepresenatations phi gamma =
   let
      ruleList = [axiom,barbaraARC,antiARC]
      stopList = nub $ concatMap subterms (gamma ++ [phi])
      withReasons = addReasonsToOriginal gamma  -- this was the original line; don't lose it!
      h = applyARule (gamma ++ [phi]) axiom -- new
      withReason  = withReasons ++ h
      oneStepARC setWithReasons   =
        let
            z = dropReasons setWithReasons
            a = map (applyARule z)  ruleList
            b = concat a
        in
             fixDuplicates $ setWithReasons ++ [ s | s <- b, checkARC stopList (get1 s)]
      fixedPointARC  =  withReason : map oneStepARC fixedPointARC    --- withReason had been withReasons !! note
      firstRepeatOrFind  (x:y:rest)
          |  phi `elem` (map get1 x)                      =  do
                           putStrLn " "
                           putStrLn "The sentence follows, and here is a derivation in ARC from the assumptions:"
                           putStrLn " "
                           mapM_ print $ modify .  full_reverse $ near $ tree_reverse $ proofSearch phi  x
                           putStrLn " "
          |  x == y                                                 =  do
                           {
                           putStrLn "The given sentence is not provable from the assumptions in ARC.";
                           putStrLn "  ";
                           -- mapM_ print $ x ; --  !!
                           putStrLn "Here is a counter-model:";
                           countermod gamma phi stopList x;
                           }
          |  otherwise                                            =  firstRepeatOrFind (y:rest)
   in firstRepeatOrFind fixedPointARC


justCounterModelARC p g =
   let
      phi = readS p
      gamma = readSs g
      ruleList = [axiom,barbaraARC,antiARC]
      stopList = nub $ concatMap subterms (gamma ++ [phi])
      withReasons = addReasonsToOriginal gamma
      oneStepARC setWithReasons   =
        let
            z = dropReasons setWithReasons
            a = map (applyARule z)  ruleList
            b = concat a
        in
             fixDuplicates $ setWithReasons ++ [ s | s <- b, checkARC stopList (get1 s)]
      fixedPointARC  =  withReasons : map oneStepARC fixedPointARC
      firstRepeatOrFind  (x:y:rest)
          |  x == y                                                 =   modelBuildARC stopList x  -- countermod gamma phi stopList x
          |  otherwise                                            =  firstRepeatOrFind (y:rest)
   in firstRepeatOrFind fixedPointARC



fullStoryARC phi gamma  = fullStoryARCUnderRepresenatations (readS phi) (readSs gamma)
fullStoryARCUnderRepresenatations phi gamma =
   let
      ruleList = [axiom,barbaraARC,antiARC]
      stopList = nub $ concatMap subterms (gamma ++ [phi])
      withReasons = addReasonsToOriginal gamma
      oneStepARC setWithReasons   =
        let
            z = dropReasons setWithReasons
            a = map (applyARule z)  ruleList
            b = concat a
        in
             fixDuplicates $ setWithReasons ++ [ s | s <- b, checkARC stopList (get1 s)]
      fixedPointARC  =  withReasons : map oneStepARC fixedPointARC
      firstRepeatOrFind  (x:y:rest)
          |  phi `elem` (map get1 x)                      =  do
                           putStrLn " "
                           putStrLn "The sentence follows, and here is a derivation in ARC from the assumptions:"
                           putStrLn " "
                           mapM_ print $ modify .  full_reverse $ near $ tree_reverse $ proofSearch phi  x
                           putStrLn " "
          |  x == y                                                 =  do
                           {
                           putStrLn "The given sentence is not provable from the assumptions in ARC.";
                           putStrLn "  ";
                           putStrLn "Here is the list of sentences which do follow, and with restrictions:";
                           mapM_ print $  map get1  x
                           }
          |  otherwise                                            =  firstRepeatOrFind (y:rest)
   in firstRepeatOrFind fixedPointARC



countermod gamma phi stpList chunk =
   let
       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

   in
       showModelNounsVerbsPlusJustificationsARC m gamma phi stpList    -- !!!! PUT THIS BACK FOR the FULL MODELS
       -- showModelNounsVerbsPlusJustificationsARC mShortened gamma phi stpList    -- !!! PUT THIS BACK FOR SMALLER MODELS

modelBuildARC stpList chunk =
   let
        k:: Int
        k = length stpList
        uni = [0..k-1]
        sList = map get1 chunk
        relVerbs = nub $ concatMap  verbsIn sList
        relevantCNs =  nub $ concatMap cnsIn sList
        withNumbers = zip stpList uni
        order = map pairOfTerms sList
        cnInterpretationFn cn =  [  r | r<- uni,  ((stpList !! r), (CNasTerm  (PCN Pos cn) )) `elem` order]
        tvInterpretationFn tv =  [(r,s) | r<-uni, s<-uni, ((stpList!! r), (TermMaker (PV Pos tv) (TermNP All (stpList!! s))))  `elem` order]
        termInterpretationFn t = (t, [r | r<-uni, ((stpList !! r),t) `elem` order])
        m = Model  {universe =  uni, cnDict = [ (M p (cnInterpretationFn p)) | p <- relevantCNs],
                     verbDict = [ (Vb transverb (tvInterpretationFn transverb)) | transverb <- relVerbs] }
   in
        m -- showModelPlus m stpList





pairOfTerms (Sent d t u) = (t,u)

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"


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

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 All (CNasTerm skunks) (CNasTerm chordates)),
   (Sent All tMammals tSkunks2),
   (Sent All tSkunks2 (CNasTerm mammals))]
testCh2phi = (Sent All tSkunks tChordates)

--followsInARCUnderRepresenatations testCh2phi testCh2gamma

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 =  "all see all skunks see all chordates"

-- 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 Chordates     [3,4],
     M Birds    [1,2,5],
     M Skunks [2]
    ]
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 {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"]


conclusion1 = "all who see all who hate all skunks see all who love all mammals"
assumptions1 =     ["all mammals hate all skunks",
                                 "all skunks see all skunks",
                                 "all who love all mammals are skunks",
                                 "all birds see all who love all skunks",
                                 "all who see all birds are mammals"]


assumptions2 = ["all mammals hate all skunks",
                            "all skunks see all skunks",
                            "all who love all mammals are skunks",
                            "all birds see all who love all skunks",
                             "all who see all birds are mammals",
                             "all who see all birds see all skunks",
                             "all who see all skunks love all skunks"]