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)

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

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

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 LawsGraphEdge = LawsGraphEdge
  { lgeLaw :: Law
  , lgeReverse :: Bool
  , lgeIndex :: Integer
  }

instance Show LawsGraphEdge where
  show edge =
    "LawsGraphEdge{"
    <> (if lgeReverse edge then "< " else "> ")
    <> lawName (lgeLaw edge)
    <> " "
    <> show (lgeIndex edge)
    <> "}"

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

getLawsGraphEdges :: Statement -> [(LawsGraphEdge, Statement)]
getLawsGraphEdges s = concat $ rights $ map aux laws
  -- ^ `rights` here because we can't apply
  -- e.g. or_contr_eq forwards without inventing B
  where
    aux :: Law -> Either ReplaceError [(LawsGraphEdge, Statement)]
    aux law = do
      forward <- direction law lawLhs lawRhs False
      reverse <- direction law lawRhs lawLhs True
      return $ forward ++ reverse

    direction
      :: Law
      -> (Law -> Statement)
      -> (Law -> Statement)
      -> Bool
      -> Either ReplaceError [(LawsGraphEdge, Statement)]
    direction law mkPattern1 mkPattern2 isReverse = do
      replaceds <- replace (mkPattern1 law) (mkPattern2 law) s
      return $
        (flip map) (zip [0..] replaceds) $ \(index, s') ->
          let
            edge = LawsGraphEdge
              { lgeLaw = law
              , lgeReverse = isReverse
              , lgeIndex = index
              }
          in (edge, s')

{-
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
-}