module Logic.Statement.Laws where

import Logic.Parse (eof, mkInput)
import Logic.Statement (Statement(..))
import Logic.Statement.Parse (stmt)
import Logic.Statement.Serialize (serialize, SerializeFormat(Plain))
import Logic.Graph (bfs, verifyPath, VerifyPathError)

import Data.Either (fromRight, rights)
import Data.Maybe (fromJust, listToMaybe)

data Law = Law
  { lawName :: String
  , lawLhs :: Statement
  , lawRhs :: Statement
  }

instance Eq Law where
  law1 == law2 =
    lawLhs law1 == lawLhs law2
    && lawRhs law1 == lawRhs law2

instance Show Law where
  show law =
    "Law{"
    <> lawName law
    <> ": "
    <> serialize Plain (lawLhs law)
    <> " <=> "
    <> serialize Plain (lawRhs law)
    <> "}"

mkLaw :: String -> String -> String -> Law
mkLaw name lhs rhs = Law name (fromString lhs) (fromString rhs)
  where
    fromString :: String -> Statement
    fromString string = fromRight undefined $ eof stmt $ mkInput string

laws :: [Law]
laws =
  [ mkLaw "dbl_neg"         "A"         "!!A"
  , mkLaw "and_comm"        "(A&B)"     "(B&A)"
  , mkLaw "or_comm"         "(A|B)"     "(B|A)"
  , mkLaw "and_assoc"       "(A&(B&C))" "((A&B)&C)"
  , mkLaw "or_assoc"        "(A|(B|C))" "((A|B)|C)"
  , mkLaw "and_or_distrib"  "(A&(B|C))" "((A&B)|(A&C))"
  , mkLaw "or_and_distrib"  "(A|(B&C))" "((A|B)&(A|C))"
  , mkLaw "and_symm_eq"     "A"         "(A&A)"
  , mkLaw "or_symm_eq"      "A"         "(A|A)"
  , mkLaw "not_and_distrib" "!(A&B)"    "(!A|!B)"
  , mkLaw "not_or_distrib"  "!(A|B)"    "(!A&!B)"
  , mkLaw "implies_or"      "(A->B)"    "(!A|B)"
  , mkLaw "implies_and"     "(A->B)"    "!(A&!B)"
  , mkLaw "or_contr_eq"     "A"         "(A|(B&!B))"
  , mkLaw "and_or_cancel"   "A"         "(A&(A|B))"
  , mkLaw "or_and_cancel"   "A"         "(A|(A&B))"
  , mkLaw "iff_and"         "(A<->B)"   "((A->B)&(B->A))"
  , mkLaw "iff_or"          "(A<->B)"   "((A&B)|(!A&!B))"
  ]

{-
ghci> import Logic.Statement.Eval (bucket, Bucket(Tautology))
ghci> all (== Tautology) $ map (\law -> bucket $ Iff (lawLhs law) (lawRhs law)) laws
True
-}

lookupLaw :: String -> Maybe Law
lookupLaw name = listToMaybe $ filter (\law -> lawName law == name) laws

match
  :: Statement
  -- ^ pattern
  -> Statement
  -- ^ statement to search within
  -> Maybe [(String, Statement)]
  -- ^ mapping from pattern-statement atoms to search-statement parts
match = aux []
  where
    aux
      :: [(String, Statement)]
      -> Statement
      -> Statement
      -> Maybe [(String, Statement)]
    aux mapping (Atom key) s = add mapping (key, s)
    aux mapping (Not p) (Not s) = aux mapping p s
    aux mapping (And     p1 p2) (And     s1 s2) = binary mapping (p1, s1) (p2, s2)
    aux mapping (Or      p1 p2) (Or      s1 s2) = binary mapping (p1, s1) (p2, s2)
    aux mapping (Implies p1 p2) (Implies s1 s2) = binary mapping (p1, s1) (p2, s2)
    aux mapping (Iff     p1 p2) (Iff     s1 s2) = binary mapping (p1, s1) (p2, s2)
    aux mapping pattern s = Nothing

    add
      :: [(String, Statement)]
      -> (String, Statement)
      -> Maybe [(String, Statement)]
    add mapping entry@(key, s') =
      case lookup key mapping of
        Nothing -> Just (entry:mapping)
        Just existing
          | existing == s' -> Just mapping
          | otherwise -> Nothing

    binary
      :: [(String, Statement)]
      -> (Statement, Statement)
      -> (Statement, Statement)
      -> Maybe [(String, Statement)]
    binary mapping (p1, s1) (p2, s2) = do
      mapping' <- aux mapping p1 s1
      aux mapping' p2 s2

{-
ghci> f x = fromRight undefined $ eof stmt $ mkInput x
ghci> match (f "(A&B)") (f "(p&(q|r))")
Just [("B",Or (Atom "q") (Atom "r")),("A",Atom "p")]
ghci> match (f "((A&B)|A)") (f "(p&(q|r))")
Nothing
ghci> match (f "((A&B)|A)") (f "((p&(q|r))|p)")
Just [("B",Or (Atom "q") (Atom "r")),("A",Atom "p")]
ghci> match (f "((A&B)|A)") (f "((p&(q|r))|q)")
Nothing
ghci> l = fromJust $ lookupLaw "and_or_distrib"
ghci> l
Law {lawName = "and_or_distrib", lawLhs = And (Atom "A") (Or (Atom "B") (Atom "C")), lawRhs = Or (And (Atom "A") (Atom "B")) (And (Atom "A") (Atom "C"))}
ghci> match (lawLhs l) (f "(p&(q|r))")
Just [("C",Atom "r"),("B",Atom "q"),("A",Atom "p")]
-}

data SwapError
  = IndeterminateSwap
  -- ^ An atom in p2 doesn't exist in p1.
  -- Strictly: an atom in p2 doesn't exist in the result from `match`
  -- (matters only if `match` is implemented incorrectly).
  -- Theoretically if for atoms we used terms of a type instead of strings, we
  -- could avoid needing this error, but I think we still wouldn't be able
  -- to return a mapping from atom-type-1 to atom-type-2 in a type safe way.
  | NonMatchingPattern
  deriving Show

swap :: Statement -> Statement -> Statement -> Either SwapError Statement
swap p1 p2 s = do
  mapping <- maybe (Left NonMatchingPattern) Right $ match p1 s
  maybe (Left IndeterminateSwap) Right $ aux mapping p2
  where
    aux :: [(String, Statement)] -> Statement -> Maybe Statement
    aux mapping (Atom key) = lookup key mapping
    aux mapping (Not p) = Not <$> aux mapping p
    aux mapping (And     p1 p2) = And     <$> aux mapping p1 <*> aux mapping p2
    aux mapping (Or      p1 p2) = Or      <$> aux mapping p1 <*> aux mapping p2
    aux mapping (Implies p1 p2) = Implies <$> aux mapping p1 <*> aux mapping p2
    aux mapping (Iff     p1 p2) = Iff     <$> aux mapping p1 <*> aux mapping p2

{-
ghci> f x = fromRight undefined $ eof stmt $ mkInput x
ghci> l = fromJust $ lookupLaw "and_or_distrib"
ghci> l
Law {lawName = "and_or_distrib", lawLhs = And (Atom "A") (Or (Atom "B") (Atom "C")), lawRhs = Or (And (Atom "A") (Atom "B")) (And (Atom "A") (Atom "C"))}
ghci> 
ghci> match (f "(A&B)") (f "(p&(q|r))")
Just [("B",Or (Atom "q") (Atom "r")),("A",Atom "p")]
ghci> swap (f "(A&B)") (f "A") (f "(p&(q|r))")
Right (Atom "p")
ghci> swap (f "(A&B)") (f "B") (f "(p&(q|r))")
Right (Or (Atom "q") (Atom "r"))
ghci> swap (f "(A&B)") (f "C") (f "(p&(q|r))")
Left Indeterminate
ghci> swap (f "((A&B)->C)") (f "A") (f "(p&(q|r))")
Left NonMatchingPattern
ghci> 
ghci> x = f "(p&(q|r))"
ghci> x
And (Atom "p") (Or (Atom "q") (Atom "r"))
ghci> serialize Plain x
"(p&(q|r))"
ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawLhs l) x
"(p&(q|r))"
ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawRhs l) x
"((p&q)|(p&r))"
ghci> 
ghci> x = f "(p&(!q|r))"
ghci> serialize Plain x
"(p&(!q|r))"
ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawLhs l) x
"(p&(!q|r))"
ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawRhs l) x
"((p&!q)|(p&r))"
-}

data ReplaceError
  = IndeterminateReplace
  deriving Show

replace :: Statement -> Statement -> Statement -> Either ReplaceError [Statement]
replace p1 p2 = firstLeft . aux
  where
    aux :: Statement -> [Either ReplaceError Statement]
    aux s =
      case swap p1 p2 s of
        Left IndeterminateSwap -> [Left IndeterminateReplace]
        -- ^ terminate here because in `replace` we stop at the first Left
        Left NonMatchingPattern -> deeper s
        Right s' -> (Right s'):(deeper s)

    deeper :: Statement -> [Either ReplaceError Statement]
    deeper (Atom key) = []
    deeper (Not s) = do
      e <- aux s
      return $ Not <$> e
    deeper (And     s1 s2) = binary And     s1 s2
    deeper (Or      s1 s2) = binary Or      s1 s2
    deeper (Implies s1 s2) = binary Implies s1 s2
    deeper (Iff     s1 s2) = binary Iff     s1 s2

    binary constructor s1 s2 =
      [constructor <$> e1 <*> (Right s2) | e1 <- aux s1] ++
      [constructor <$> (Right s1) <*> e2 | e2 <- aux s2]

firstLeft :: [Either a b] -> Either a [b]
firstLeft [] = Right []
firstLeft ((Left a):_) = Left a
firstLeft ((Right b):xs) = (b:) <$> firstLeft xs

data Direction
  = Forward
  | Reverse
  deriving (Eq, Show)

data LawsGraphEdge = LawsGraphEdge
  { lgeDirection :: Direction
  , lgeIndex :: Integer
  , lgeLaw :: Law
  } deriving Eq

instance Show LawsGraphEdge where
  show edge =
    "LawsGraphEdge{"
    <> (
      case lgeDirection edge of
        Forward -> "> "
        Reverse -> "< "
    )
    <> lawName (lgeLaw edge)
    <> " "
    <> show (lgeIndex edge)
    <> "}"

bfsLaws :: Statement -> Statement -> Maybe [LawsGraphEdge]
bfsLaws = bfs getLawsGraphEdges

getLawsGraphEdges :: Statement -> [(Statement, LawsGraphEdge)]
getLawsGraphEdges s = concat $ rights $ map aux laws
  -- ^ `rights` here because we can't apply
  -- e.g. or_contr_eq forwards without inventing B
  -- and the `Left` case is `Left IndeterminateReplace`
  where
    aux :: Law -> Either ReplaceError [(Statement, LawsGraphEdge)]
    aux law = do
      forward <- edges Forward law
      reverse <- edges Reverse law
      return $ forward ++ reverse

    replaceds :: Direction -> Law -> Either ReplaceError [Statement]
    replaceds direction law =
      let
        (pattern1, pattern2) =
          case direction of
            Forward -> (lawLhs law, lawRhs law)
            Reverse -> (lawRhs law, lawLhs law)
      in replace pattern1 pattern2 s

    mkEdges :: Direction -> Law -> [Statement] -> [(Statement, LawsGraphEdge)]
    mkEdges direction law statements = do
      (index, s') <- zip [0..] statements
      return (s', LawsGraphEdge direction index law)

    edges :: Direction -> Law -> Either ReplaceError [(Statement, LawsGraphEdge)]
    edges direction law = mkEdges direction law <$> replaceds direction law

{-
ghci> fromString x = fromRight undefined $ eof stmt $ mkInput x
ghci> niceEdges = map (\edge -> (if lgeReverse edge then "< " else "> ") <> lawName (lgeLaw edge) <> " " <> show (lgeIndex edge))
ghci> 
ghci> niceEdges <$> bfsLaws (fromString "(p|!q)") (fromString "(p|!q)")
Just []
ghci> niceEdges <$> bfsLaws (fromString "!!(p|!q)") (fromString "(p|!q)")
Just ["> dbl_neg 0"]
ghci> niceEdges <$> bfsLaws (fromString "(!!p|!q)") (fromString "(p|!q)")
Just ["> dbl_neg 1"]
ghci> niceEdges <$> bfsLaws (fromString "(p|!!!q)") (fromString "(p|!q)")
Just ["> dbl_neg 2"]
ghci> niceEdges <$> bfsLaws (fromString "(p|p)") (fromString "p")
Just ["> or_symm_eq 0"]
ghci> niceEdges <$> bfsLaws (fromString "p") (fromString "(p|p)")
Just ["< or_symm_eq 0"]
ghci> 
ghci> niceEdges <$> bfsLaws (fromString "!(!p&(q|q))") (fromString "(p|!q)")
Just ["> dbl_neg 1","> or_symm_eq 5","< not_and_distrib 0"]
ghci> niceEdges <$> bfsLaws (fromString "!(!(p&p)&(q|q))") (fromString "(p|!q)")
Just ["> dbl_neg 1","> and_symm_eq 3","> or_symm_eq 7","< not_and_distrib 0"]
ghci> 
ghci> import Data.Time.POSIX (getPOSIXTime)
ghci> time f = getPOSIXTime >>= \t0 -> f >> getPOSIXTime >>= \t1 -> return $ t1 - t0
ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "p") (fromString "p")
Just []
0.000087114s
ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!p") (fromString "p")
Just ["> dbl_neg 0"]
0.000201159s
ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!p") (fromString "p")
Just ["> dbl_neg 0","> dbl_neg 0"]
0.000444047s
ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!p") (fromString "p")
Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
0.001260947s
ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!p") (fromString "p")
Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
0.021864298s
ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!!!p") (fromString "p")
Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
3.244101767s
ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!!!!!p") (fromString "p")
Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
3066.211460539s
-}

data LawsGraphPath = LawsGraphPath
  { lgpStart :: Statement
  , lgpGoal :: Statement
  , lgpEdges :: [LawsGraphEdge]
  } deriving Show

verifyLawsPath
  :: LawsGraphPath
  -> Either (VerifyPathError Statement LawsGraphEdge) [Statement]
verifyLawsPath path =
  verifyPath getLawsGraphEdges (lgpGoal path) (lgpStart path) (lgpEdges path)

lawsPathExample1 :: LawsGraphPath
lawsPathExample1 = LawsGraphPath start goal edges
  where
    start = Implies (Atom "p") (Atom "q")
    goal = Implies (Not (Atom "q")) (Not (Atom "p"))
    edges =
      [ LawsGraphEdge Forward 1 $ law "dbl_neg"
      , LawsGraphEdge Forward 0 $ law "implies_and"
      , LawsGraphEdge Forward 0 $ law "and_comm"
      , LawsGraphEdge Reverse 0 $ law "implies_and"
      ]
    law = fromJust . lookupLaw

{-
ghci> import Logic.Statement.Serialize (serialize, SerializeFormat(..))
ghci> map (serialize Plain) <$> verifyLawsPath lawsPathExample1
Right ["(p->q)","(!!p->q)","!(!!p&!q)","!(!q&!!p)","(!q->!p)"]
-}