{-# LANGUAGE CPP #-}
module Algebra.Heyting
  ( HeytingAlgebra (..)
  , iff
  , iff'
  , toBoolean

    -- * Properties
    --
    -- $properties
  , prop_BoundedMeetSemiLattice
  , prop_BoundedJoinSemiLattice
  , prop_HeytingAlgebra
  , prop_implies
  )
  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
#if __GLASGOW_HASKELL__ >= 822
import qualified Data.Map.Merge.Lazy as Merge
#endif
import qualified Data.Set as S
import qualified Data.HashMap.Lazy as HM
import qualified Data.HashSet      as HS

import Algebra.Lattice ( BoundedJoinSemiLattice (..)
                       , BoundedMeetSemiLattice (..)
                       , BoundedLattice
                       , Meet (..)
                       , Join (..)
                       , (/\)
                       , (\/)
                       )
import Algebra.Lattice.Dropped (Dropped (..))
import Algebra.Lattice.Lifted (Lifted (..))
import Algebra.Lattice.Levitated (Levitated)
import qualified Algebra.Lattice.Levitated as L
import Algebra.PartialOrd (leq)
#ifdef EXPORT_PROPERTIES
import Test.QuickCheck hiding ((==>))
import qualified Test.QuickCheck as QC
#endif

-- |
-- Heyting algebra is a bounded semi-lattice with implication which should
-- satisfy the following law:
--
-- prop> x ∧ a ≤ b ⇔ x ≤ (a ⇒ b)
--
-- 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).
--
-- Some 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
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.
  (==>) :: 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 #-}

-- |
-- Less than fixity of both @'\/'@ and @'/\'@.
infixr 4 ==>

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

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

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

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
--

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

--
-- containers
--

-- |
-- Power set: the cannoical example of a Boolean algebra
instance (Ord a, Finite a) => HeytingAlgebra (S.Set a) where
  not a = S.fromList universe `S.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__ >= 822
  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)]

--
-- $properties
--
-- /Properties are exported only if @export-properties@ cabal flag is defined./
#ifdef EXPORT_PROPERTIES

-- |
-- Verfifies bounded meet semilattice laws.
prop_BoundedMeetSemiLattice :: (BoundedMeetSemiLattice a, Eq a, Show a)
                            => a -> a -> a -> Property
prop_BoundedMeetSemiLattice a b c =
       counterexample "meet associativity" ((a /\ (b /\ c)) === ((a /\ b) /\ c))
  .&&. counterexample "meet commutativity" ((a /\ b) === (b /\ a))
  .&&. counterexample "meet idempotent" ((a /\ a) === a)
  .&&. counterexample "meet identity" ((top /\ a) === a)
  .&&. counterexample "meet order" (Meet (a /\ b) `leq` Meet a)

-- |
-- Verfifies bounded join semilattice laws.
prop_BoundedJoinSemiLattice :: (BoundedJoinSemiLattice a, Eq a, Show a) => a -> a -> a -> Property
prop_BoundedJoinSemiLattice a b c =
       counterexample "join associativity" ((a \/ (b \/ c)) === ((a \/ b) \/ c))
  .&&. counterexample "join commutativity" ((a \/ b) === (b \/ a))
  .&&. counterexample "join idempotent" ((a \/ a) === a)
  .&&. counterexample "join identity" ((bottom \/ a) === a)
  .&&. counterexample "join order" (Join a `leq` Join (a \/ b))

-- |
-- Verifies the Heyting algebra law for @==>@:
-- for all @a@: @_ /\ a@ is left adjoint to  @a ==>@
prop_implies :: (HeytingAlgebra a, Eq a, Show a)
             => a -> a -> a -> Property
prop_implies x a b =
  counterexample ("Failed: x ≤ (a ⇒ b) then x ∧ a ≤ b\n\ta ⇒ b = " ++ show (a ==> b))
    (Meet x `leq` Meet (a ==> b) QC.==> (Meet (x /\ a) `leq` Meet b))
  .&&.
  counterexample ("Failed: x ∧ a ≤ b then x ≤ (a ⇒ b)\n\ta ⇒ b = " ++ show (a ==> b))
    (Meet (x /\ a) `leq` Meet b QC.==> (Meet x `leq` Meet (a ==> b)))


-- |
-- Usefull for testing valid instances of @'HeytingAlgebra'@ type class. It
-- validates:
--
-- * bounded lattice laws
-- * @'prop_implies'@
prop_HeytingAlgebra :: (HeytingAlgebra a, Eq a, Show a)
                    => a -> a -> a -> Property
prop_HeytingAlgebra a b c = 
       prop_BoundedJoinSemiLattice a b c
  .&&. prop_BoundedMeetSemiLattice a b c
  .&&. prop_implies a b c
#endif