-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.LBool
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
-- 
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Lifted boolean type.
-- 
-----------------------------------------------------------------------------
module ToySolver.Data.LBool
  ( LBool
  , lTrue
  , lFalse
  , lUndef
  , lnot
  , liftBool
  , unliftBool
  ) where

import Data.Int

-- | Lifted Bool type. It has three values 'lTrue', 'lFalse', 'lUndef'.
newtype LBool = LBool Int8 deriving Eq

-- | lifted true value
{-# INLINE lTrue #-}
lTrue :: LBool
lTrue = LBool 1

-- | lifted false value
{-# INLINE lFalse #-}
lFalse :: LBool
lFalse = LBool (-1)

-- | undefined truth value
{-# INLINE lUndef #-}
lUndef :: LBool
lUndef = LBool 0

-- |
-- @
--   lnot lTrue == lFalse
--   lnot lFalse == lTrue
--   lnot lUndef == lUndef
-- @
{-# INLINE lnot #-}
lnot :: LBool -> LBool
lnot x
  | x == lTrue  = lFalse
  | x == lFalse = lTrue
  | otherwise   = lUndef

-- |
-- @
--   liftBool True == lTrue
--   liftBool False == lFalse
-- @
{-# INLINE liftBool #-}
liftBool :: Bool -> LBool
liftBool True  = lTrue
liftBool False = lFalse

-- |
-- @
--   unliftBool lTrue == Just True
--   unliftBool lFalse == Just False
--   unliftBool lUndef == Nothing
-- @
{-# INLINE unliftBool #-}
unliftBool :: LBool -> Maybe Bool
unliftBool x
  | x == lTrue  = Just True
  | x == lFalse = Just False
  | otherwise   = Nothing

instance Show LBool where
  show x
    | x == lTrue  = "lTrue"
    | x == lFalse = "lFalse"
    | otherwise   = "lUndef"