{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DefaultSignatures #-}


-- |
-- Module      : OAlg.Data.Boolean.Definition
-- Description : definition of boolean structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- boolean structure for multivalent logic. 
module OAlg.Data.Boolean.Definition
  ( -- * Boolean
    Boolean(..)

    -- * Bool
  , B.Bool(..), B.otherwise

    -- * Structure
  -- , Bol
  )
  where

import Prelude as P hiding (not,(||),(&&),or,and)
import qualified Data.Bool as B

import OAlg.Data.Logical

--------------------------------------------------------------------------------
-- Boolean -

infixr 1 ~>, <~>

-- | types with a 'Boolean' structure, allowing multivalent logic.
--
--   __Note__ Every 'Enum' type which is also 'Bounded' has a natural implementation
--   as @'false' = 'minBound'@, @'true' = 'maxBound'@, @('||') = 'max'@, @('&&') = 'min'@
--   (as there are min and max bounds the operator ('||') and @('&&')@ should be
--    implemented with a lazy variant of 'min' and 'max') and
--    @'not' b = 'toEnum' ('fromEnum' 'maxBound' '-' 'fromEnum' t)@.
class Logical b => Boolean b where
  {-# MINIMAL true, false, not #-}
  false :: b 
  true  :: b

  not   :: b -> b
  
  or    :: [b] -> b
  or []     = b
forall b. Boolean b => b
false
  or (b
a:[b]
as) = b
a b -> b -> b
forall a. Logical a => a -> a -> a
|| [b] -> b
forall b. Boolean b => [b] -> b
or [b]
as
  
  and   :: [b] -> b
  and []     = b
forall b. Boolean b => b
true
  and (b
a:[b]
as) = b
a b -> b -> b
forall a. Logical a => a -> a -> a
&& [b] -> b
forall b. Boolean b => [b] -> b
and [b]
as

  
  (~>) :: b -> b -> b
  b
a ~> b
b = b -> b
forall b. Boolean b => b -> b
not b
a b -> b -> b
forall a. Logical a => a -> a -> a
|| b
b

  (<~>) :: b -> b -> b
  b
a <~> b
b = (b
a b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
b) b -> b -> b
forall a. Logical a => a -> a -> a
&& (b
b b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
a)

  eqvl   :: [b] -> b
  eqvl []     = b
forall b. Boolean b => b
true
  eqvl (b
a:[b]
as) = [b] -> b
forall b. Boolean b => [b] -> b
and [b]
impls where
    impls :: [b]
impls = ((b, b) -> b) -> [(b, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((b -> b -> b) -> (b, b) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry b -> b -> b
forall b. Boolean b => b -> b -> b
(~>)) ([b] -> [b] -> [(b, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip (b
ab -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
as) ([b]
as[b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++[b
a]))

instance Boolean Bool where
  false :: Bool
false = Bool
False  
  true :: Bool
true  = Bool
True
  not :: Bool -> Bool
not   = Bool -> Bool
B.not
  <~> :: Bool -> Bool -> Bool
(<~>) = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==)