{-# 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
  { FLattice a -> forall b. Lattice b => (a -> b) -> b
lowerFLattice :: forall b. Lattice b =>
                                    (a -> b) -> b
  }

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

liftFLattice :: a -> FLattice a
liftFLattice :: a -> FLattice a
liftFLattice a
a = (forall b. Lattice b => (a -> b) -> b) -> FLattice 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 :: FLattice a -> a
retractFLattice FLattice a
a = FLattice a -> (a -> a) -> a
forall a. FLattice a -> forall b. Lattice b => (a -> b) -> b
lowerFLattice FLattice a
a 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 b. Lattice b => (a -> b) -> b) -> FLattice a
forall a. (forall b. Lattice b => (a -> b) -> b) -> FLattice a
FLattice (\a -> b
inj -> (a -> b) -> b
forall b. Lattice b => (a -> b) -> b
f a -> b
inj b -> b -> b
forall a. Lattice a => a -> a -> a
\/ (a -> b) -> b
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 b. Lattice b => (a -> b) -> b) -> FLattice a
forall a. (forall b. Lattice b => (a -> b) -> b) -> FLattice a
FLattice (\a -> b
inj -> (a -> b) -> b
forall b. Lattice b => (a -> b) -> b
f a -> b
inj b -> b -> b
forall a. Lattice a => a -> a -> a
/\ (a -> b) -> b
forall b. Lattice b => (a -> b) -> b
g a -> b
inj)


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

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

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

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

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

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

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

liftFBoundedLattice :: a -> FBoundedLattice a
liftFBoundedLattice :: a -> FBoundedLattice a
liftFBoundedLattice a
a = (forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice 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 :: FBoundedLattice a -> a
retractFBoundedLattice FBoundedLattice a
a = FBoundedLattice a -> (a -> a) -> a
forall a.
FBoundedLattice a -> forall b. BoundedLattice b => (a -> b) -> b
lowerFBoundedLattice FBoundedLattice a
a 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 b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
forall a.
(forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
FBoundedLattice (\a -> b
inj -> (a -> b) -> b
forall b. BoundedLattice b => (a -> b) -> b
f a -> b
inj b -> b -> b
forall a. Lattice a => a -> a -> a
\/ (a -> b) -> b
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 b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
forall a.
(forall b. BoundedLattice b => (a -> b) -> b) -> FBoundedLattice a
FBoundedLattice (\a -> b
inj -> (a -> b) -> b
forall b. BoundedLattice b => (a -> b) -> b
f a -> b
inj b -> b -> b
forall a. Lattice a => a -> a -> a
/\ (a -> b) -> b
forall b. BoundedLattice b => (a -> b) -> b
g a -> b
inj)


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

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

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

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