-----------------------------------------------------------------------------
-- |
-- 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 LBool -> LBool -> Bool
(LBool -> LBool -> Bool) -> (LBool -> LBool -> Bool) -> Eq LBool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LBool -> LBool -> Bool
$c/= :: LBool -> LBool -> Bool
== :: LBool -> LBool -> Bool
$c== :: LBool -> LBool -> Bool
Eq

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

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

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

-- |
-- @
--   lnot lTrue == lFalse
--   lnot lFalse == lTrue
--   lnot lUndef == lUndef
-- @
{-# INLINE lnot #-}
lnot :: LBool -> LBool
lnot :: LBool -> LBool
lnot LBool
x
  | LBool
x LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
lTrue  = LBool
lFalse
  | LBool
x LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
lFalse = LBool
lTrue
  | Bool
otherwise   = LBool
lUndef

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

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

instance Show LBool where
  show :: LBool -> String
show LBool
x
    | LBool
x LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
lTrue  = String
"lTrue"
    | LBool
x LBool -> LBool -> Bool
forall a. Eq a => a -> a -> Bool
== LBool
lFalse = String
"lFalse"
    | Bool
otherwise   = String
"lUndef"