SyllogisticInference.hs

-- There are  "2" versions of a bunch of commands
-- Right now, those are the only ones that are needed.
-- The rest should be dropped at some point.

module SyllogisticInference where

import Data.List
import Control.Monad
import ARC/Syntax2
import ARC/ProofTreeNumbers
import ARC/ExampleSentences
import ARC/ExampleRules
import ARC/FrontEnd
import Data.List (transpose, intercalate)

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)
 
{- not needed, I think 
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, "assumption", [])
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  :: [Sent] ->  Rule ->  [([Sent], [(Term, Term)], [(PV, PV)])]
applicableInstances  sList rule   =
   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  sList rule ) 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  sList  rule))) above
 -- the 'above' above had y  <- verblistNotVars    rather than w


eVerbs rule sList vList = if extraVerbsInRule rule == [] then (applicableInstances  sList rule ) else
    let 
        above = [[((PV Pos x),(PV Pos y))]  |  x <- (extraVerbsInRule rule), y<- vList ]
    in
        concatMap (\ y ->  (map (\ x -> (get1 x, get2 x , (get3 x ++ y))) (applicableInstances  sList  rule))) 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
        
  
extraCNs rule sList cnsToInclude verbsToInclude = if extracnsInRule rule == [] then (eVerbs rule sList verbsToInclude) else   
    let 
        useThese =   cnsToInclude
        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)   

     
applyARule2 sList r exCNs exVerbs  =  nub $ map (\ x -> render r x) (extraCNs r sList exCNs exVerbs)         


applyAllRules2  sListWithReasons rl  exCNs  exVerbs= 
  let 
      z = dropReasons sListWithReasons
      a = map (\ x -> applyARule2 z x exCNs exVerbs) rl
      b = concat a
   in 
      fixDuplicates $ sListWithReasons  ++ b   


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

--allDerived2 :: [Sent] -> [Rule] -> [(Sent, RuleName, [Sent])]
allDerived2 noReasons rl exCNs  exVerbs = allDerivedUnderRepresentations2 noReasons rl exCNs exVerbs
          

allDerivedUnderRepresentations noReasons rl=   firstRepeat $ fixedPoint addReasons rl
   where addReasons = addReasonsToOriginal  noReasons   

allDerivedUnderRepresentations2 noReasons rl exCNs exVerbs =   firstRepeat $ fixedPoint2 addReasons rl exCNs exVerbs
   where addReasons = addReasonsToOriginal  noReasons      
 
fixedPoint withReasons rl = withReasons : map (\ x -> applyAllRules x rl) (fixedPoint withReasons rl)

fixedPoint2 withReasons rl  exCNs  exVerbs = 
    withReasons : map (\ x -> applyAllRules2 x rl  exCNs exVerbs) (fixedPoint2 withReasons rl exCNs  exVerbs)


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     

followsUnderRepresentation phi gamma ruleList = 
   let
      addReasons = addReasonsToOriginal  gamma 
      bingo = fixedPoint2 addReasons ruleList  (cnsIn phi)   (concatMap verbsIn (gamma ++ [phi]))
      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   
         
follows phi gamma ruleList = followsUnderRepresentation (readS phi) (readSs gamma) ruleList

findAProof :: String -> [String] -> [Rule] -> [(Int, Sent, RuleName, [Int])]
findAProof p g ruleList = 
   let
      phi  = readS p
      gamma = readSs g
      addReasons = addReasonsToOriginal  gamma 
      bingo = fixedPoint addReasons ruleList
      firstRepeatOrFind  (x:y:rest)  
          |  phi `elem` (map get1 x)                      =   modify .  full_reverse $ near $ tree_reverse $ proofSearch phi  x
          |  (inconsistency x)  /=   []                       =  []
          |  x == y                                                 =   [] 
          |  otherwise                                            =  firstRepeatOrFind (y:rest)
   in firstRepeatOrFind bingo   


-- based on https://stackoverflow.com/questions/5929377/format-list-output-in-haskell
-- a type for records
data ProofLine = ProofLine { line  :: Int
           , sentence  :: Sent  
           , rule :: RuleName
           , supports :: [Int] }
   deriving Show


-- test data
{- test =
    [ ProofLine 1 (readS "all skunks mammals") "assumption" []
    , ProofLine 2 (readS "all mammals chordates") "assumption"   [1]
    , ProofLine 3 (readS "all skunks chordates") "barbara" [1,2]
    ]
-}

   
displayAProof p g ruleList  =      
   putStrLn $ showTable [ ColDesc center " "  left  (show . line)
                     , ColDesc center " "  left  (show. sentence)
                     , ColDesc center " " left  rule
                     , ColDesc center " "  right (intercalate ", " . map show . supports)
                     ] $ getReadyToDisplay  p g ruleList

getReadyToDisplay  p g ruleList =  map (\k -> ProofLine {line= get1Of4 k, sentence=get2Of4 k, rule = get3Of4 k, supports = get4Of4 k}) $ findAProof p g ruleList 
        
      
 
---   :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)



showT 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