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


-- |
-- 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.Structure.Definition

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

infixr 3 &&
infixr 2 ||
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 Boolean b where
  {-# MINIMAL true, false, not, ((||), (&&) | or, and) #-}
  false :: b 
  true  :: b

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

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

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

  eqvl   :: [b] -> b
  eqvl []     = forall b. Boolean b => b
true
  eqvl (b
a:[b]
as) = forall b. Boolean b => [b] -> b
and [b]
impls where
    impls :: [b]
impls = forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall b. Boolean b => b -> b -> b
(~>)) (forall a b. [a] -> [b] -> [(a, b)]
zip (b
aforall a. a -> [a] -> [a]
:[b]
as) ([b]
asforall 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
(B.||)
  && :: Bool -> Bool -> Bool
(&&)  = Bool -> Bool -> Bool
(B.&&)
  <~> :: Bool -> Bool -> Bool
(<~>) = forall a. Eq a => a -> a -> Bool
(==)

--------------------------------------------------------------------------------
-- Bol -

-- | type representing 'Boolean' structures.
data Bol

type instance Structure Bol x = Boolean x