{-# LANGUAGE CPP #-}

module Algebra.Heyting
  ( -- * Heyting algebras
    HeytingAlgebra (..)
  , implies
  , (<=>)
  , iff
  , iff'
  , toBoolean
    -- * Boolean algebras
  , BooleanAlgebra
  )
  where


import           Prelude hiding (not)
import qualified Prelude

import           Control.Applicative    (Const (..))
import           Data.Functor.Identity  (Identity (..))
import           Data.Hashable          (Hashable)
import           Data.Proxy             (Proxy (..))
import           Data.Semigroup         ( All (..)
                                        , Any (..)
                                        , Endo (..)
                                        )
import           Data.Tagged            (Tagged (..))
import           Data.Universe.Class    (Finite, universe)
import qualified Data.Map as M
import           Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Lazy as HM
import qualified Data.HashSet      as HS

import           Algebra.Lattice ( BoundedJoinSemiLattice (..)
                                 , BoundedMeetSemiLattice (..)
                                 , BoundedLattice
                                 , Meet (..)
                                 , bottom
                                 , top
                                 , (/\)
                                 , (\/)
                                 )
import           Algebra.Lattice.Dropped    (Dropped (..))
import           Algebra.Lattice.Lifted     (Lifted (..))
import           Algebra.Lattice.Levitated  (Levitated)
import qualified Algebra.Lattice.Levitated as L
import           Algebra.Lattice.Ordered    (Ordered (..))
import           Algebra.Lattice.Op         (Op (..))
import           Algebra.PartialOrd         (leq)

-- 
-- Heyting algebras
--

-- |
-- Heyting algebra is a bounded semi-lattice with implication which should
-- satisfy the following law:
--
-- prop> x ∧ a ≤ b ⇔ x ≤ (a ⇒ b)
--
-- We also require that a Heyting algebra is a distributive lattice, which
-- means any of the two equivalent conditions holds:
--
-- prop> a ∧ (b ∨ c) = a ∧ b ∨ a ∧ c
-- prop> a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c)
--
-- This means @a ⇒ b@ is an
-- [exponential object](https://ncatlab.org/nlab/show/exponential%2Bobject),
-- which makes any Heyting algebra
-- a [cartesian
-- closed category](https://ncatlab.org/nlab/show/cartesian%2Bclosed%2Bcategory).
-- This means that Curry isomorphism holds (which takes a form of an actual
-- equality):
--
-- prop> a ⇒ (b ⇒ c) = (a ∧ b) ⇒ c
--
-- Some other useful properties of Heyting algebras:
-- 
-- prop> (a ⇒ b) ∧ a ≤ b
-- prop> b ≤ a ⇒ a ∧ b
-- prop> a ≤ b  iff a ⇒ b = ⊤
-- prop> b ≤ b' then a ⇒ b ≤ a ⇒ b'
-- prop> a'≤ a  then a' ⇒ b ≤ a ⇒ b
-- prop> not (a ∧ b) = not (a ∨ b)
-- prop> not (a ∨ b) = not a ∧ not b
class BoundedLattice a => HeytingAlgebra a where
  -- |
  -- Default implementation: @a ==> b = not a \/ b@, it requires @not@ to
  -- satisfy Boolean axioms, which will make it into a Boolean algebra.
  --
  -- Fixity is less than fixity of both @'\/'@ and @'/\'@.
  (==>) :: a -> a -> a
  (==>) a b = not a \/ b

  -- |
  -- Default implementation: @not a = a '==>' 'bottom'@
  --
  -- It is useful for optimisation reasons.
  not :: a -> a
  not a = a ==> bottom

  {-# MINIMAL (==>) | not #-}

infixr 4 ==>

-- |
-- @'implies'@ is an alias for @'==>'@
implies :: HeytingAlgebra a => a -> a -> a
implies = (==>)

(<=>) :: HeytingAlgebra a => a -> a -> a
a <=> b = (a ==> b) /\ (b ==> a)

-- |
-- @'iff'@ is an alias for @'<=>'@
iff :: HeytingAlgebra a => a -> a -> a
iff = (<=>)

iff' :: (Eq a, HeytingAlgebra a) => a -> a -> Bool
iff' a b = Meet top `leq` Meet (iff a b)
  
-- |
-- Every Heyting algebra contains a Boolean algebra. @'toBoolean'@ maps onto it;
-- moreover it is a monad (Heyting algebra is a category as every poset is) which
-- preserves finite infima.
toBoolean :: HeytingAlgebra a => a -> a
toBoolean = not . not

instance HeytingAlgebra Bool where
  not = Prelude.not

instance HeytingAlgebra All where
  All a ==> All b = All (a ==> b)
  not (All a)     = All (not a)

instance HeytingAlgebra Any where
  Any a ==> Any b = Any (a ==> b)
  not (Any a)     = Any (not a)

instance HeytingAlgebra () where
  _ ==> _ = ()

instance HeytingAlgebra (Proxy a) where
  _ ==> _ = Proxy

instance HeytingAlgebra a => HeytingAlgebra (Tagged t a) where
  Tagged a ==> Tagged b = Tagged (a ==> b)

instance HeytingAlgebra b => HeytingAlgebra (a -> b) where
  f ==> g = \a -> f a ==> g a

#if MIN_VERSION_base(4,8,0)
instance HeytingAlgebra a => HeytingAlgebra (Identity a) where
  (Identity a) ==> (Identity b) = Identity (a ==> b)
#endif

instance HeytingAlgebra a => HeytingAlgebra (Const a b) where
  (Const a) ==> (Const b) = Const (a ==> b)

instance HeytingAlgebra a => HeytingAlgebra (Endo a) where
  (Endo f) ==> (Endo g) = Endo (f ==> g)

instance (HeytingAlgebra a, HeytingAlgebra b) => HeytingAlgebra (a, b) where
  (a0, b0) ==> (a1, b1) = (a0 ==> a1, b0 ==> b1)

--
-- Dropped, Lifted, Levitated, Ordered
--

-- |
-- Subdirectly irreducible Heyting algebra.
instance (Eq a, HeytingAlgebra a) => HeytingAlgebra (Dropped a) where
  (Drop a) ==> (Drop b) | Meet a `leq` Meet b = Top
                        | otherwise           = Drop (a ==> b)
  Top      ==> a        = a
  _        ==> Top      = Top

instance HeytingAlgebra a => HeytingAlgebra (Lifted a) where
  (Lift a) ==> (Lift b) = Lift (a ==> b)
  Bottom   ==> _        = Lift top
  _        ==> Bottom   = Bottom

instance (Eq a, HeytingAlgebra a) => HeytingAlgebra (Levitated a) where
  (L.Levitate a) ==> (L.Levitate b) | Meet a `leq` Meet b = L.Top
                                    | otherwise           = L.Levitate (a ==> b)
  L.Top          ==> a              = a
  _              ==> L.Top          = L.Top
  L.Bottom       ==> _              = L.Top
  _              ==> L.Bottom       = L.Bottom

instance (Ord a, Bounded a) => HeytingAlgebra (Ordered a) where
  Ordered a ==> Ordered b | a <= b    = top
                          | otherwise = Ordered b

--
-- containers
--

-- |
-- Power set: the canonical example of a Boolean algebra
instance (Ord a, Finite a) => HeytingAlgebra (Set a) where
  not a = Set.fromList universe `Set.difference` a

instance (Eq a, Finite a, Hashable a) => HeytingAlgebra (HS.HashSet a) where
  not a = HS.fromList universe `HS.difference` a

-- |
-- It is not a boolean algebra (even if values are).
instance (Ord k, Finite k, HeytingAlgebra v) => HeytingAlgebra (M.Map k v) where
  -- _xx__
  -- __yy_
  -- T_iTT where i = x ==> y; T = top; _ missing (or removed key)
#if __GLASOW_HASKELL__ >= 804
  a ==> b =
    Merge.merge
      Merge.dropMissing                    -- drop if an element is missing in @b@
      (Merge.mapMissing (\_ _ -> top))     -- put @top@ if an element is missing in @a@
      (Merge.zipWithMatched (\_ -> (==>))) -- merge  matching elements with @==>@
      a b

    \/ M.fromList [(k, top) | k <- universe, not (M.member k a), not (M.member k b) ] 
                            -- for elements which are not in a, nor in b add
                            -- a @top@ key
#else
  a ==> b =
    M.intersectionWith (==>) a b
      `M.union` M.map (const top) (M.difference b a)
      `M.union` M.fromList [(k, top) | k <- universe, not (M.member k a), not (M.member k b)]
#endif

instance (Eq k, Finite k, Hashable k, HeytingAlgebra v) => HeytingAlgebra (HM.HashMap k v) where
  a ==> b = HM.intersectionWith (==>) a b
    `HM.union` HM.map (const top) (HM.difference b a)
    `HM.union` HM.fromList [(k, top) | k <- universe, not (HM.member k a), not (HM.member k b)]

-- 
-- Boolean algebras
--
-- They are defined in the same module, to avoid module dependency: @Op a@ is
-- a Boolean algebra (thus Heyting algebra in the first place), whenever @a@ is
-- a Boolean algebra.
--

-- |
-- Boolean algebra is a Heyting algebra which negation satisfies the law of
-- excluded middle, i.e. either of the following:
--
-- prop> not . not == not
--
-- or
--
-- prop> x ∨ not x == top
--
-- Another characterisation of Boolean algebras is as
-- [complemented](https://en.wikipedia.org/wiki/Complemented_lattice)
-- [distributive lattices](https://ncatlab.org/nlab/show/distributive+lattice)
-- where the complement satisfies the following three properties:
--
-- prop> (not a) ∧ a == bottom and (not a) ∨ a == top -- excluded middle law
-- prop> not (not a) == a                             -- involution law
-- prop> a ≤ b ⇒ not b ≤ not a                        -- order-reversing
class HeytingAlgebra a => BooleanAlgebra a

--
-- Instances
--

instance BooleanAlgebra Bool

instance BooleanAlgebra All

instance BooleanAlgebra Any

instance BooleanAlgebra ()

instance BooleanAlgebra (Proxy a)

instance BooleanAlgebra a => BooleanAlgebra (Tagged t a)

instance BooleanAlgebra b => BooleanAlgebra (a -> b)

#if MIN_VERSION_base(4,8,0)
instance BooleanAlgebra a => BooleanAlgebra (Identity a)
#endif

instance BooleanAlgebra a => BooleanAlgebra (Const a b)

instance BooleanAlgebra a => BooleanAlgebra (Endo a)

instance (BooleanAlgebra a, BooleanAlgebra b) => BooleanAlgebra (a, b)

--
-- containers
--

instance (Ord a, Finite a) => BooleanAlgebra (Set a)


--
-- Op
--

-- | Whenever @a@ is a Boolean Algebra, @Op a@ is a Boolean algebra as well,
-- which in particular means that it is a Heyting algebra in the first place.
--
instance BooleanAlgebra a => HeytingAlgebra (Op a) where
  (Op a) ==> (Op b) = Op (not a /\ b)

-- | Every boolean algebra is isomorphic to power set @P(X)@ of some set @X@;
-- then `not :: Op (P(X)) -> P(X)` is a lattice isomorphism, thus `Op (P(X))` is
-- a boolean algebra, since @P(X)@ is.
instance BooleanAlgebra a => BooleanAlgebra (Op a)