module Algebra.Heyting.Layered
  ( Layered (..)
  , layer
  ) where

import           Prelude

import           Algebra.Lattice ( BoundedJoinSemiLattice (..)
                                 , BoundedMeetSemiLattice (..)
                                 , Lattice (..)
                                 )

import           Algebra.Heyting ( Heyting (..) )

-- |
-- Layer one Heyting algebra on top of the other.  Note: this is not
-- a categorical sum.
data Layered a b
  = Lower a
  | Upper b
  deriving (Int -> Layered a b -> ShowS
[Layered a b] -> ShowS
Layered a b -> String
(Int -> Layered a b -> ShowS)
-> (Layered a b -> String)
-> ([Layered a b] -> ShowS)
-> Show (Layered a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> Layered a b -> ShowS
forall a b. (Show a, Show b) => [Layered a b] -> ShowS
forall a b. (Show a, Show b) => Layered a b -> String
showList :: [Layered a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [Layered a b] -> ShowS
show :: Layered a b -> String
$cshow :: forall a b. (Show a, Show b) => Layered a b -> String
showsPrec :: Int -> Layered a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> Layered a b -> ShowS
Show, Layered a b -> Layered a b -> Bool
(Layered a b -> Layered a b -> Bool)
-> (Layered a b -> Layered a b -> Bool) -> Eq (Layered a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => Layered a b -> Layered a b -> Bool
/= :: Layered a b -> Layered a b -> Bool
$c/= :: forall a b. (Eq a, Eq b) => Layered a b -> Layered a b -> Bool
== :: Layered a b -> Layered a b -> Bool
$c== :: forall a b. (Eq a, Eq b) => Layered a b -> Layered a b -> Bool
Eq, Eq (Layered a b)
Eq (Layered a b)
-> (Layered a b -> Layered a b -> Ordering)
-> (Layered a b -> Layered a b -> Bool)
-> (Layered a b -> Layered a b -> Bool)
-> (Layered a b -> Layered a b -> Bool)
-> (Layered a b -> Layered a b -> Bool)
-> (Layered a b -> Layered a b -> Layered a b)
-> (Layered a b -> Layered a b -> Layered a b)
-> Ord (Layered a b)
Layered a b -> Layered a b -> Bool
Layered a b -> Layered a b -> Ordering
Layered a b -> Layered a b -> Layered a b
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a b. (Ord a, Ord b) => Eq (Layered a b)
forall a b. (Ord a, Ord b) => Layered a b -> Layered a b -> Bool
forall a b.
(Ord a, Ord b) =>
Layered a b -> Layered a b -> Ordering
forall a b.
(Ord a, Ord b) =>
Layered a b -> Layered a b -> Layered a b
min :: Layered a b -> Layered a b -> Layered a b
$cmin :: forall a b.
(Ord a, Ord b) =>
Layered a b -> Layered a b -> Layered a b
max :: Layered a b -> Layered a b -> Layered a b
$cmax :: forall a b.
(Ord a, Ord b) =>
Layered a b -> Layered a b -> Layered a b
>= :: Layered a b -> Layered a b -> Bool
$c>= :: forall a b. (Ord a, Ord b) => Layered a b -> Layered a b -> Bool
> :: Layered a b -> Layered a b -> Bool
$c> :: forall a b. (Ord a, Ord b) => Layered a b -> Layered a b -> Bool
<= :: Layered a b -> Layered a b -> Bool
$c<= :: forall a b. (Ord a, Ord b) => Layered a b -> Layered a b -> Bool
< :: Layered a b -> Layered a b -> Bool
$c< :: forall a b. (Ord a, Ord b) => Layered a b -> Layered a b -> Bool
compare :: Layered a b -> Layered a b -> Ordering
$ccompare :: forall a b.
(Ord a, Ord b) =>
Layered a b -> Layered a b -> Ordering
$cp1Ord :: forall a b. (Ord a, Ord b) => Eq (Layered a b)
Ord)

instance ( Lattice a
         , Lattice b
         ) => Lattice (Layered a b) where
  l :: Layered a b
l@Lower{} /\ :: Layered a b -> Layered a b -> Layered a b
/\ Upper b
_   = Layered a b
l
  Upper b
_   /\ l :: Layered a b
l@Lower{} = Layered a b
l
  Lower a
l   /\ Lower a
l'  = a -> Layered a b
forall a b. a -> Layered a b
Lower (a -> Layered a b) -> a -> Layered a b
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
l'
  Upper b
u   /\ Upper b
u'  = b -> Layered a b
forall a b. b -> Layered a b
Upper (b -> Layered a b) -> b -> Layered a b
forall a b. (a -> b) -> a -> b
$ b
u b -> b -> b
forall a. Lattice a => a -> a -> a
/\ b
u'

  Lower a
_   \/ :: Layered a b -> Layered a b -> Layered a b
\/ u :: Layered a b
u@Upper{} = Layered a b
u
  u :: Layered a b
u@Upper{} \/ Lower a
_   = Layered a b
u
  Lower a
l   \/ Lower a
l'  = a -> Layered a b
forall a b. a -> Layered a b
Lower (a -> Layered a b) -> a -> Layered a b
forall a b. (a -> b) -> a -> b
$ a
l a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
l'
  Upper b
u   \/ Upper b
u'  = b -> Layered a b
forall a b. b -> Layered a b
Upper (b -> Layered a b) -> b -> Layered a b
forall a b. (a -> b) -> a -> b
$ b
u b -> b -> b
forall a. Lattice a => a -> a -> a
\/ b
u'

instance (BoundedJoinSemiLattice a, Lattice b) => BoundedJoinSemiLattice (Layered a b) where
  bottom :: Layered a b
bottom = a -> Layered a b
forall a b. a -> Layered a b
Lower a
forall a. BoundedJoinSemiLattice a => a
bottom

instance (Lattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (Layered a b) where
  top :: Layered a b
top = b -> Layered a b
forall a b. b -> Layered a b
Upper b
forall a. BoundedMeetSemiLattice a => a
top

instance ( Heyting a
         , Heyting b
         , Eq a
         ) => Heyting (Layered a b) where
  Lower a
_   ==> :: Layered a b -> Layered a b -> Layered a b
==> Upper b
_      = b -> Layered a b
forall a b. b -> Layered a b
Upper b
forall a. BoundedMeetSemiLattice a => a
top
  Upper b
_   ==> l :: Layered a b
l@Lower{}    = Layered a b
l
  Upper b
u   ==> Upper b
u'     = b -> Layered a b
forall a b. b -> Layered a b
Upper (b -> Layered a b) -> b -> Layered a b
forall a b. (a -> b) -> a -> b
$ b
u b -> b -> b
forall a. Heyting a => a -> a -> a
==> b
u'
  Lower a
l   ==> Lower a
l'     = case a
l a -> a -> a
forall a. Heyting a => a -> a -> a
==> a
l' of
    a
ll' | a
ll' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. BoundedMeetSemiLattice a => a
top -> b -> Layered a b
forall a b. b -> Layered a b
Upper b
forall a. BoundedMeetSemiLattice a => a
top
        | Bool
otherwise  -> a -> Layered a b
forall a b. a -> Layered a b
Lower a
ll'

layer :: (a -> c) -> (b -> c) -> Layered a b -> c
layer :: (a -> c) -> (b -> c) -> Layered a b -> c
layer a -> c
f b -> c
_ (Lower a
a) = a -> c
f a
a
layer a -> c
_ b -> c
g (Upper b
b) = b -> c
g b
b