logic/Logic/Statement/Serialize.hs

module Logic.Statement.Serialize where

import Logic.Statement (Statement(..), atoms)
import Logic.Statement.Eval (enumerate, eval, implies)

import Data.List (intercalate)
import Data.Either (fromRight)

data TokenString = TokenString
  { tsCanEval :: CanEval
  , tsLevel :: Int
  , tsString :: String
  } deriving (Show, Eq)

data CanEval
  = Filler
  | CanEval
  deriving (Show, Eq)

data TokenValue = TokenValue
  { tvLevel :: Int
  , tvValue :: Value
  } deriving (Show, Eq)

data Value
  = NoValue
  | Value Bool
  deriving (Show, Eq)

data SerializeFormat
  = Plain
  | Latex
--  | PrefixPlain
  deriving (Show, Eq)

serialize :: SerializeFormat -> Statement -> String
serialize fmt s = concat $ map tsString $ serializeStrings fmt s

serializeStrings :: SerializeFormat -> Statement -> [TokenString]
serializeStrings fmt = aux 0
  where
    aux :: Int -> Statement -> [TokenString]
    aux =
      case fmt of
        Plain -> serializeStringsPlain
        Latex -> serializeStringsLatex

-- Internal function
serializeStringsPlain :: Int -> Statement -> [TokenString]
serializeStringsPlain level = aux
  where
    f = serializeStringsPlain
    level' = level + 1

    aux (Atom key)      = [TokenString CanEval level key]
    aux (Not s)         = [TokenString CanEval level "!"] ++ f level' s
    aux (And s1 s2)     = connective level "&"   (f level' s1) (f level' s2)
    aux (Or s1 s2)      = connective level "|"   (f level' s1) (f level' s2)
    aux (Implies s1 s2) = connective level "->"  (f level' s1) (f level' s2)
    aux (Iff s1 s2)     = connective level "<->" (f level' s1) (f level' s2)

-- Internal function
serializeStringsLatex :: Int -> Statement -> [TokenString]
serializeStringsLatex level = aux
  where
    f = serializeStringsLatex
    level' = level + 1

    aux (Atom key)      = [TokenString CanEval level key]
    aux (Not s)         = [TokenString CanEval level "\\neg "] ++ f level' s
    aux (And s1 s2)     = connective level "\\land "           (f level' s1) (f level' s2)
    aux (Or s1 s2)      = connective level "\\lor "            (f level' s1) (f level' s2)
    aux (Implies s1 s2) = connective level "\\to "             (f level' s1) (f level' s2)
    aux (Iff s1 s2)     = connective level "\\leftrightarrow " (f level' s1) (f level' s2)

-- Internal function
connective :: Int -> String -> [TokenString] -> [TokenString] -> [TokenString]
connective level middle tokens1 tokens2 =
  [TokenString Filler level "("]
  ++ tokens1
  ++ [TokenString CanEval level middle]
  ++ tokens2
  ++ [TokenString Filler level ")"]

-- Using infix convention with brackets
serializeValues :: [(String, Bool)] -> Statement -> Either String [TokenValue]
serializeValues ass = fmap snd . aux 0
  where
    aux :: Int -> Statement -> Either String (Bool, [TokenValue])
    aux level s@(Atom key) = do
      bool <- eval ass s
      return (bool, [TokenValue level $ Value bool])
    aux level (Not s) = do
      (bool, tokens) <- aux (level + 1) s
      return (not bool, [TokenValue level $ Value $ not bool] ++ tokens)
    aux level (And s1 s2)     = connective level (&&) s1 s2
    aux level (Or s1 s2)      = connective level (||) s1 s2
    aux level (Implies s1 s2) = connective level implies s1 s2
    aux level (Iff s1 s2)     = connective level (==) s1 s2

    connective
      :: Int
      -> (Bool -> Bool -> Bool)
      -> Statement
      -> Statement
      -> Either String (Bool, [TokenValue])
    connective level f s1 s2 = do
      (bool1, tokens1) <- aux (level + 1) s1
      (bool2, tokens2) <- aux (level + 1) s2
      let bracket = [TokenValue level NoValue]
      let bool = f bool1 bool2
      return (bool, bracket ++ tokens1 ++ [TokenValue level $ Value bool] ++ tokens2 ++ bracket)

serializeLatexTruthTable :: Statement -> String
serializeLatexTruthTable s = open <> header <> "\\hline\n" <> body <> close
  where
    open :: String
    open = "\\begin{tabular}{" <> replicate (length $ atoms s) 'c' <> "||" <> spec <> "}\n"

    close :: String
    close = "\\end{tabular}\n"

    spec :: String
    spec
      | length serial == 0 = undefined
      | length serial == 1 = "c"
      | isMain (head serial) = "c|" <> replicate (length serial - 1) 'c'
      | isMain (serial !! (length serial - 1)) = replicate (length serial - 1) 'c' <> "|c"
      | otherwise = concat $ map (\token -> if isMain token then "|c|" else "c") serial

    isMain :: TokenString -> Bool
    isMain (TokenString CanEval level string) = level == 0
    isMain _ = False

    serial :: [TokenString]
    serial = serializeStrings Latex s

    header :: String
    header =
      intercalate " & " (map dollars $ atoms s) <>
      " & " <>
      intercalate " & " (map dollars $ map tsString serial) <>
      " \\\\\n"

    dollars :: String -> String
    dollars string = "$" <> string <> "$"

    body :: String
    body = concat $ map line $ enumerate $ atoms s

    line :: [(String, Bool)] -> String
    line ass =
      intercalate " & " (bools ass) <>
      " & " <>
      intercalate " & " (cells ass) <>
      "\\\\\n"

    bools :: [(String, Bool)] -> [String]
    bools ass = [if bool then "1" else "0" | (key, bool) <- ass]

    cells :: [(String, Bool)] -> [String]
    cells ass = map cell $ fromRight undefined $ serializeValues ass s

    cell :: TokenValue -> String
    cell (TokenValue level value) =
      case value of
        NoValue -> ""
        Value bool -> mkBold level $ if bool then "1" else "0"

    mkBold :: Int -> String -> String
    mkBold level string
      | level == 0 = "\\textbf " <> string
      | otherwise = string