タブローの方法

tableau.hs

{-# LANGUAGE FlexibleContexts #-}

import qualified Text.Parsec as P
import Text.Parsec.String (Parser)
import Data.List (intercalate)
import Control.Applicative
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.Map as M

main = do
  s <- getLine
  let res = parse s
  case res of
    Left err -> print err
    Right  e -> do
      putStrLn $ "parse succeeded: " ++ show e
      putStrLn $ showResult $ tableau True e

infixl 3 :/\, :\/
infixr 2 ==>

data Expr
  = Var String
  | Not Expr
  | Expr :/\ Expr
  | Expr :\/ Expr
  deriving Show

(==>) :: Expr -> Expr -> Expr
a ==> b = Not a :\/ b

showResult :: Maybe String -> String
showResult Nothing = "False"
showResult (Just a) = "True: " ++ a

showEnv :: M.Map String Bool -> String
showEnv m = intercalate ", "
  $ map (\(k,b) -> k ++ ":" ++ showBool b)
  $ M.toList m
  where
    showBool = show

(*|>) :: (Alternative m, MonadReader Bool m) => m a -> m a -> m a
m *|> n = do
  b <- ask
  if b then m *> n else m <|> n
(|*>) :: (Alternative m, MonadReader Bool m) => m a -> m a -> m a
m |*> n = do
  b <- ask
  if b then m <|> n else m *> n

tableau :: Bool -> Expr -> Maybe String
tableau b e = showEnv . snd <$> ((f e `runStateT` M.empty) `runReaderT` b)
  where
    -- M.Map String Bool ってもっとマシにできそう...
    f :: Expr -> StateT (M.Map String Bool) (ReaderT Bool Maybe) ()
    f (Var a) = check a
    f (Not e) = local not $ f e
    f (e1 :/\ e2) = f e1 *|> f e2
    f (e1 :\/ e2) = f e1 |*> f e2

check :: String -> StateT (M.Map String Bool) (ReaderT Bool Maybe) ()
check n = do
  mp <- get
  b <- ask
  case M.lookup n mp of
    Just  b' | b /= b' -> mzero
    Just   _ -> return ()
    _ -> put $ M.insert n b mp


parse = P.parse (expr <* P.eof) "expression"

token :: Parser a -> Parser a
token p = p <* P.spaces

symbolic :: Char -> Parser Char
symbolic = token . P.char

symbol :: String -> Parser String
symbol = token . P.string

name :: Parser String
name = token $ some P.letter

factor :: Parser Expr
factor = P.between (symbolic '(') (symbolic ')') expr
  <|> (Not <$ symbolic '~' <*> factor)
  <|> (Var <$> name)

manyFromTo :: Int -> Int -> Parser a -> Parser [a]
manyFromTo from to p
  | from <= 0 = f to
  | otherwise = (:) <$> p <*> manyFromTo (from-1) (to-1) p
  where
    f i
      | i <= 0 = return []
      | otherwise = do
        m <- optional p
        case m of
          Nothing -> return []
          Just  a -> (a :) <$> f (i-1)

exprAnd :: Parser Expr
exprAnd = P.chainl1 factor
  $ (:/\) <$ (symbol "/\\" <|> token (manyFromTo 1 2 (P.char '&')))

exprOr :: Parser Expr
exprOr = P.chainl1 exprAnd
  $ (:\/) <$ (symbol "\\/" <|> token (manyFromTo 1 2 (P.char '|')))

expr :: Parser Expr
expr = P.chainr1 exprOr $ (==>) <$ symbol "->"