{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes      #-}
{-# LANGUAGE Safe            #-}

----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.Lattice.Free
-- License     :  BSD-3-Clause (see the file LICENSE)
--
-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
--
----------------------------------------------------------------------------

module Algebra.Lattice.Free.Final (
   -- * Free Lattice
    FLattice,
    liftFLattice,
    lowerFLattice,
    retractFLattice,
   -- * Free BoundedLattice
    FBoundedLattice,
    liftFBoundedLattice,
    lowerFBoundedLattice,
    retractFBoundedLattice,
    ) where

import Prelude ()
import Prelude.Compat

import Algebra.Lattice

import Data.Universe.Class (Finite (..), Universe (..))

-------------------------------------------------------------------------------
-- Lattice
-------------------------------------------------------------------------------

newtype FLattice a = FLattice
  { forall a. FLattice a -> forall b. Lattice b => (a -> b) -> b
lowerFLattice :: forall b. Lattice b =>
                                    (a -> b) -> b
  }

instance Functor FLattice where
  fmap :: forall a b. (a -> b) -> FLattice a -> FLattice b
fmap a -> b
f (FLattice forall b. Lattice b => (a -> b) -> b
g) = forall a. (forall b. Lattice b => (a -> b) -> b) -> FLattice a
FLattice (\b -> b
inj -> forall b. Lattice b => (a -> b) -> b
g (b -> b
inj forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f))
  a
a <$ :: forall a b. a -> FLattice b -> FLattice a
<$ FLattice forall b. Lattice b => (b -> b) -> b
f = forall a. (forall b. Lattice b => (a -> b) -> b) -> FLattice a
FLattice (\a -> b
inj -> forall b. Lattice b => (b -> b) -> b
f (forall a b. a -> b -> a
const (a -> b
inj a
a)))

liftFLattice :: a -> FLattice a
liftFLattice :: forall a. a -> FLattice a
liftFLattice a
a = forall a. (forall b. Lattice b => (a -> b) -> b) -> FLattice a
FLattice (\a -> b
inj -> a -> b
inj a
a)

retractFLattice :: Lattice a => FLattice a -> a
retractFLattice :: forall a. Lattice a => FLattice a -> a
retractFLattice FLattice a
a = forall a. FLattice a -> forall b. Lattice b => (a -> b) -> b
lowerFLattice FLattice a
a forall a. a -> a
id

instance Lattice (FLattice a) where
  FLattice forall b. Lattice b => (a -> b) -> b
f \/ :: FLattice a -> FLattice a -> FLattice a
\/ FLattice forall b. Lattice b => (a -> b) -> b
g = forall a. (forall b. Lattice b => (a -> b) -> b) -> FLattice a
FLattice (\a -> b
inj -> forall b. Lattice b => (a -> b) -> b
f a -> b
inj forall a. Lattice a => a -> a -> a
\/ forall b. Lattice b => (a -> b) -> b
g a -> b
inj)
  FLattice forall b. Lattice b => (a -> b) -> b
f /\ :: FLattice a -> FLattice a -> FLattice a
/\ FLattice forall b. Lattice b => (a -> b) -> b
g = forall a. (forall b. Lattice b => (a -> b) -> b) -> FLattice a
FLattice (\a -> b
inj -> forall b. Lattice b => (a -> b) -> b
f a -> b
inj forall a. Lattice a => a -> a -> a
/\ forall b. Lattice b => (a -> b) -> b
g a -> b
inj)


instance BoundedJoinSemiLattice a =>
         BoundedJoinSemiLattice (FLattice a) where
  bottom :: FLattice a
bottom = forall a. (forall b. Lattice b => (a -> b) -> b) -> FLattice a
FLattice (\a -> b
inj -> a -> b
inj forall a. BoundedJoinSemiLattice a => a
bottom)

instance BoundedMeetSemiLattice a =>
         BoundedMeetSemiLattice (FLattice a) where
  top :: FLattice a
top = forall a. (forall b. Lattice b => (a -> b) -> b) -> FLattice a
FLattice (\a -> b
inj -> a -> b
inj forall a. BoundedMeetSemiLattice a => a
top)

instance Universe a => Universe (FLattice a) where
  universe :: [FLattice a]
universe = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> FLattice a
liftFLattice forall a. Universe a => [a]
universe

instance Finite a => Finite (FLattice a) where
  universeF :: [FLattice a]
universeF = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> FLattice a
liftFLattice forall a. Finite a => [a]
universeF

-------------------------------------------------------------------------------
-- BoundedLattice
-------------------------------------------------------------------------------

newtype FBoundedLattice a = FBoundedLattice
  { forall a.
FBoundedLattice a -> forall b. BoundedLattice b => (a -> b) -> b
lowerFBoundedLattice :: forall b. BoundedLattice b =>
                                    (a -> b) -> b
  }

instance Functor FBoundedLattice where
  fmap :: forall a b. (a -> b) -> FBoundedLattice a -> FBoundedLattice b
fmap a -> b
f (FBoundedLattice forall b. BoundedLattice b => (a -> b) -> b
g) = forall a.
(forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
FBoundedLattice (\b -> b
inj -> forall b. BoundedLattice b => (a -> b) -> b
g (b -> b
inj forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f))
  a
a <$ :: forall a b. a -> FBoundedLattice b -> FBoundedLattice a
<$ FBoundedLattice forall b. BoundedLattice b => (b -> b) -> b
f = forall a.
(forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
FBoundedLattice (\a -> b
inj -> forall b. BoundedLattice b => (b -> b) -> b
f (forall a b. a -> b -> a
const (a -> b
inj a
a)))

liftFBoundedLattice :: a -> FBoundedLattice a
liftFBoundedLattice :: forall a. a -> FBoundedLattice a
liftFBoundedLattice a
a = forall a.
(forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
FBoundedLattice (\a -> b
inj -> a -> b
inj a
a)

retractFBoundedLattice :: BoundedLattice a => FBoundedLattice a -> a
retractFBoundedLattice :: forall a. BoundedLattice a => FBoundedLattice a -> a
retractFBoundedLattice FBoundedLattice a
a = forall a.
FBoundedLattice a -> forall b. BoundedLattice b => (a -> b) -> b
lowerFBoundedLattice FBoundedLattice a
a forall a. a -> a
id

instance Lattice (FBoundedLattice a) where
  FBoundedLattice forall b. BoundedLattice b => (a -> b) -> b
f \/ :: FBoundedLattice a -> FBoundedLattice a -> FBoundedLattice a
\/ FBoundedLattice forall b. BoundedLattice b => (a -> b) -> b
g = forall a.
(forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
FBoundedLattice (\a -> b
inj -> forall b. BoundedLattice b => (a -> b) -> b
f a -> b
inj forall a. Lattice a => a -> a -> a
\/ forall b. BoundedLattice b => (a -> b) -> b
g a -> b
inj)
  FBoundedLattice forall b. BoundedLattice b => (a -> b) -> b
f /\ :: FBoundedLattice a -> FBoundedLattice a -> FBoundedLattice a
/\ FBoundedLattice forall b. BoundedLattice b => (a -> b) -> b
g = forall a.
(forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
FBoundedLattice (\a -> b
inj -> forall b. BoundedLattice b => (a -> b) -> b
f a -> b
inj forall a. Lattice a => a -> a -> a
/\ forall b. BoundedLattice b => (a -> b) -> b
g a -> b
inj)


instance BoundedJoinSemiLattice (FBoundedLattice a) where
  bottom :: FBoundedLattice a
bottom = forall a.
(forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
FBoundedLattice (\a -> b
_ -> forall a. BoundedJoinSemiLattice a => a
bottom)

instance BoundedMeetSemiLattice (FBoundedLattice a) where
  top :: FBoundedLattice a
top = forall a.
(forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
FBoundedLattice (\a -> b
_ -> forall a. BoundedMeetSemiLattice a => a
top)

instance Universe a => Universe (FBoundedLattice a) where
  universe :: [FBoundedLattice a]
universe = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> FBoundedLattice a
liftFBoundedLattice forall a. Universe a => [a]
universe

instance Finite a => Finite (FBoundedLattice a) where
  universeF :: [FBoundedLattice a]
universeF = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> FBoundedLattice a
liftFBoundedLattice forall a. Finite a => [a]
universeF