{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveFoldable      #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DeriveTraversable   #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE Safe                #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.Lattice.Levitated
-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus
-- License     :  BSD-3-Clause (see the file LICENSE)
--
-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
--
----------------------------------------------------------------------------
module Algebra.Lattice.Levitated (
    Levitated(..)
  , retractLevitated
  , foldLevitated
  ) where

import Prelude ()
import Prelude.Compat

import Algebra.Lattice
import Algebra.PartialOrd

import Control.DeepSeq       (NFData (..))
import Control.Monad         (ap)
import Data.Data             (Data, Typeable)
import Data.Hashable         (Hashable (..))
import Data.Universe.Class   (Finite (..), Universe (..))
import Data.Universe.Helpers (Natural, Tagged, retag)
import GHC.Generics          (Generic, Generic1)

import qualified Test.QuickCheck as QC

--
-- Levitated
--

-- | Graft a distinct top and bottom onto an otherwise unbounded lattice.
-- The top is the absorbing element for the join, and the bottom is the absorbing
-- element for the meet.
data Levitated a = Bottom
                 | Levitate a
                 | Top
  deriving ( Levitated a -> Levitated a -> Bool
(Levitated a -> Levitated a -> Bool)
-> (Levitated a -> Levitated a -> Bool) -> Eq (Levitated a)
forall a. Eq a => Levitated a -> Levitated a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Levitated a -> Levitated a -> Bool
$c/= :: forall a. Eq a => Levitated a -> Levitated a -> Bool
== :: Levitated a -> Levitated a -> Bool
$c== :: forall a. Eq a => Levitated a -> Levitated a -> Bool
Eq, Eq (Levitated a)
Eq (Levitated a)
-> (Levitated a -> Levitated a -> Ordering)
-> (Levitated a -> Levitated a -> Bool)
-> (Levitated a -> Levitated a -> Bool)
-> (Levitated a -> Levitated a -> Bool)
-> (Levitated a -> Levitated a -> Bool)
-> (Levitated a -> Levitated a -> Levitated a)
-> (Levitated a -> Levitated a -> Levitated a)
-> Ord (Levitated a)
Levitated a -> Levitated a -> Bool
Levitated a -> Levitated a -> Ordering
Levitated a -> Levitated a -> Levitated a
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. Ord a => Eq (Levitated a)
forall a. Ord a => Levitated a -> Levitated a -> Bool
forall a. Ord a => Levitated a -> Levitated a -> Ordering
forall a. Ord a => Levitated a -> Levitated a -> Levitated a
min :: Levitated a -> Levitated a -> Levitated a
$cmin :: forall a. Ord a => Levitated a -> Levitated a -> Levitated a
max :: Levitated a -> Levitated a -> Levitated a
$cmax :: forall a. Ord a => Levitated a -> Levitated a -> Levitated a
>= :: Levitated a -> Levitated a -> Bool
$c>= :: forall a. Ord a => Levitated a -> Levitated a -> Bool
> :: Levitated a -> Levitated a -> Bool
$c> :: forall a. Ord a => Levitated a -> Levitated a -> Bool
<= :: Levitated a -> Levitated a -> Bool
$c<= :: forall a. Ord a => Levitated a -> Levitated a -> Bool
< :: Levitated a -> Levitated a -> Bool
$c< :: forall a. Ord a => Levitated a -> Levitated a -> Bool
compare :: Levitated a -> Levitated a -> Ordering
$ccompare :: forall a. Ord a => Levitated a -> Levitated a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Levitated a)
Ord, Int -> Levitated a -> ShowS
[Levitated a] -> ShowS
Levitated a -> String
(Int -> Levitated a -> ShowS)
-> (Levitated a -> String)
-> ([Levitated a] -> ShowS)
-> Show (Levitated a)
forall a. Show a => Int -> Levitated a -> ShowS
forall a. Show a => [Levitated a] -> ShowS
forall a. Show a => Levitated a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Levitated a] -> ShowS
$cshowList :: forall a. Show a => [Levitated a] -> ShowS
show :: Levitated a -> String
$cshow :: forall a. Show a => Levitated a -> String
showsPrec :: Int -> Levitated a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Levitated a -> ShowS
Show, ReadPrec [Levitated a]
ReadPrec (Levitated a)
Int -> ReadS (Levitated a)
ReadS [Levitated a]
(Int -> ReadS (Levitated a))
-> ReadS [Levitated a]
-> ReadPrec (Levitated a)
-> ReadPrec [Levitated a]
-> Read (Levitated a)
forall a. Read a => ReadPrec [Levitated a]
forall a. Read a => ReadPrec (Levitated a)
forall a. Read a => Int -> ReadS (Levitated a)
forall a. Read a => ReadS [Levitated a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Levitated a]
$creadListPrec :: forall a. Read a => ReadPrec [Levitated a]
readPrec :: ReadPrec (Levitated a)
$creadPrec :: forall a. Read a => ReadPrec (Levitated a)
readList :: ReadS [Levitated a]
$creadList :: forall a. Read a => ReadS [Levitated a]
readsPrec :: Int -> ReadS (Levitated a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Levitated a)
Read, Typeable (Levitated a)
DataType
Constr
Typeable (Levitated a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Levitated a -> c (Levitated a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Levitated a))
-> (Levitated a -> Constr)
-> (Levitated a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Levitated a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Levitated a)))
-> ((forall b. Data b => b -> b) -> Levitated a -> Levitated a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Levitated a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Levitated a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Levitated a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Levitated a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a))
-> Data (Levitated a)
Levitated a -> DataType
Levitated a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Levitated a))
(forall b. Data b => b -> b) -> Levitated a -> Levitated a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Levitated a -> c (Levitated a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Levitated a)
forall a. Data a => Typeable (Levitated a)
forall a. Data a => Levitated a -> DataType
forall a. Data a => Levitated a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Levitated a -> Levitated a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Levitated a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Levitated a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Levitated a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Levitated a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Levitated a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Levitated a -> c (Levitated a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Levitated a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Levitated a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Levitated a -> u
forall u. (forall d. Data d => d -> u) -> Levitated a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Levitated a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Levitated a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Levitated a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Levitated a -> c (Levitated a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Levitated a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Levitated a))
$cTop :: Constr
$cLevitate :: Constr
$cBottom :: Constr
$tLevitated :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
gmapMp :: (forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
gmapM :: (forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Levitated a -> m (Levitated a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Levitated a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Levitated a -> u
gmapQ :: (forall d. Data d => d -> u) -> Levitated a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Levitated a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Levitated a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Levitated a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Levitated a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Levitated a -> r
gmapT :: (forall b. Data b => b -> b) -> Levitated a -> Levitated a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Levitated a -> Levitated a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Levitated a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Levitated a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Levitated a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Levitated a))
dataTypeOf :: Levitated a -> DataType
$cdataTypeOf :: forall a. Data a => Levitated a -> DataType
toConstr :: Levitated a -> Constr
$ctoConstr :: forall a. Data a => Levitated a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Levitated a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Levitated a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Levitated a -> c (Levitated a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Levitated a -> c (Levitated a)
$cp1Data :: forall a. Data a => Typeable (Levitated a)
Data, Typeable, (forall x. Levitated a -> Rep (Levitated a) x)
-> (forall x. Rep (Levitated a) x -> Levitated a)
-> Generic (Levitated a)
forall x. Rep (Levitated a) x -> Levitated a
forall x. Levitated a -> Rep (Levitated a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Levitated a) x -> Levitated a
forall a x. Levitated a -> Rep (Levitated a) x
$cto :: forall a x. Rep (Levitated a) x -> Levitated a
$cfrom :: forall a x. Levitated a -> Rep (Levitated a) x
Generic, a -> Levitated b -> Levitated a
(a -> b) -> Levitated a -> Levitated b
(forall a b. (a -> b) -> Levitated a -> Levitated b)
-> (forall a b. a -> Levitated b -> Levitated a)
-> Functor Levitated
forall a b. a -> Levitated b -> Levitated a
forall a b. (a -> b) -> Levitated a -> Levitated b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Levitated b -> Levitated a
$c<$ :: forall a b. a -> Levitated b -> Levitated a
fmap :: (a -> b) -> Levitated a -> Levitated b
$cfmap :: forall a b. (a -> b) -> Levitated a -> Levitated b
Functor, Levitated a -> Bool
(a -> m) -> Levitated a -> m
(a -> b -> b) -> b -> Levitated a -> b
(forall m. Monoid m => Levitated m -> m)
-> (forall m a. Monoid m => (a -> m) -> Levitated a -> m)
-> (forall m a. Monoid m => (a -> m) -> Levitated a -> m)
-> (forall a b. (a -> b -> b) -> b -> Levitated a -> b)
-> (forall a b. (a -> b -> b) -> b -> Levitated a -> b)
-> (forall b a. (b -> a -> b) -> b -> Levitated a -> b)
-> (forall b a. (b -> a -> b) -> b -> Levitated a -> b)
-> (forall a. (a -> a -> a) -> Levitated a -> a)
-> (forall a. (a -> a -> a) -> Levitated a -> a)
-> (forall a. Levitated a -> [a])
-> (forall a. Levitated a -> Bool)
-> (forall a. Levitated a -> Int)
-> (forall a. Eq a => a -> Levitated a -> Bool)
-> (forall a. Ord a => Levitated a -> a)
-> (forall a. Ord a => Levitated a -> a)
-> (forall a. Num a => Levitated a -> a)
-> (forall a. Num a => Levitated a -> a)
-> Foldable Levitated
forall a. Eq a => a -> Levitated a -> Bool
forall a. Num a => Levitated a -> a
forall a. Ord a => Levitated a -> a
forall m. Monoid m => Levitated m -> m
forall a. Levitated a -> Bool
forall a. Levitated a -> Int
forall a. Levitated a -> [a]
forall a. (a -> a -> a) -> Levitated a -> a
forall m a. Monoid m => (a -> m) -> Levitated a -> m
forall b a. (b -> a -> b) -> b -> Levitated a -> b
forall a b. (a -> b -> b) -> b -> Levitated a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Levitated a -> a
$cproduct :: forall a. Num a => Levitated a -> a
sum :: Levitated a -> a
$csum :: forall a. Num a => Levitated a -> a
minimum :: Levitated a -> a
$cminimum :: forall a. Ord a => Levitated a -> a
maximum :: Levitated a -> a
$cmaximum :: forall a. Ord a => Levitated a -> a
elem :: a -> Levitated a -> Bool
$celem :: forall a. Eq a => a -> Levitated a -> Bool
length :: Levitated a -> Int
$clength :: forall a. Levitated a -> Int
null :: Levitated a -> Bool
$cnull :: forall a. Levitated a -> Bool
toList :: Levitated a -> [a]
$ctoList :: forall a. Levitated a -> [a]
foldl1 :: (a -> a -> a) -> Levitated a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Levitated a -> a
foldr1 :: (a -> a -> a) -> Levitated a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Levitated a -> a
foldl' :: (b -> a -> b) -> b -> Levitated a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Levitated a -> b
foldl :: (b -> a -> b) -> b -> Levitated a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Levitated a -> b
foldr' :: (a -> b -> b) -> b -> Levitated a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Levitated a -> b
foldr :: (a -> b -> b) -> b -> Levitated a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Levitated a -> b
foldMap' :: (a -> m) -> Levitated a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Levitated a -> m
foldMap :: (a -> m) -> Levitated a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Levitated a -> m
fold :: Levitated m -> m
$cfold :: forall m. Monoid m => Levitated m -> m
Foldable, Functor Levitated
Foldable Levitated
Functor Levitated
-> Foldable Levitated
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Levitated a -> f (Levitated b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Levitated (f a) -> f (Levitated a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Levitated a -> m (Levitated b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Levitated (m a) -> m (Levitated a))
-> Traversable Levitated
(a -> f b) -> Levitated a -> f (Levitated b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Levitated (m a) -> m (Levitated a)
forall (f :: * -> *) a.
Applicative f =>
Levitated (f a) -> f (Levitated a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Levitated a -> m (Levitated b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Levitated a -> f (Levitated b)
sequence :: Levitated (m a) -> m (Levitated a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Levitated (m a) -> m (Levitated a)
mapM :: (a -> m b) -> Levitated a -> m (Levitated b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Levitated a -> m (Levitated b)
sequenceA :: Levitated (f a) -> f (Levitated a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Levitated (f a) -> f (Levitated a)
traverse :: (a -> f b) -> Levitated a -> f (Levitated b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Levitated a -> f (Levitated b)
$cp2Traversable :: Foldable Levitated
$cp1Traversable :: Functor Levitated
Traversable
           , (forall a. Levitated a -> Rep1 Levitated a)
-> (forall a. Rep1 Levitated a -> Levitated a)
-> Generic1 Levitated
forall a. Rep1 Levitated a -> Levitated a
forall a. Levitated a -> Rep1 Levitated a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall a. Rep1 Levitated a -> Levitated a
$cfrom1 :: forall a. Levitated a -> Rep1 Levitated a
Generic1
           )

instance Applicative Levitated where
  pure :: a -> Levitated a
pure = a -> Levitated a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: Levitated (a -> b) -> Levitated a -> Levitated b
(<*>) = Levitated (a -> b) -> Levitated a -> Levitated b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Levitated where
  return :: a -> Levitated a
return            = a -> Levitated a
forall a. a -> Levitated a
Levitate
  Levitated a
Top >>= :: Levitated a -> (a -> Levitated b) -> Levitated b
>>= a -> Levitated b
_         = Levitated b
forall a. Levitated a
Top
  Levitated a
Bottom >>= a -> Levitated b
_      = Levitated b
forall a. Levitated a
Bottom
  Levitate a
x >>= a -> Levitated b
f  = a -> Levitated b
f a
x

instance NFData a => NFData (Levitated a) where
  rnf :: Levitated a -> ()
rnf Levitated a
Top          = ()
  rnf Levitated a
Bottom       = ()
  rnf (Levitate a
a) = a -> ()
forall a. NFData a => a -> ()
rnf a
a

instance Hashable a => Hashable (Levitated a)

instance PartialOrd a => PartialOrd (Levitated a) where
  leq :: Levitated a -> Levitated a -> Bool
leq Levitated a
_ Levitated a
Top = Bool
True
  leq Levitated a
Top Levitated a
_ = Bool
False
  leq Levitated a
Bottom Levitated a
_ = Bool
True
  leq Levitated a
_ Levitated a
Bottom = Bool
False
  leq (Levitate a
x) (Levitate a
y) = a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq a
x a
y
  comparable :: Levitated a -> Levitated a -> Bool
comparable Levitated a
Top Levitated a
_ = Bool
True
  comparable Levitated a
_ Levitated a
Top = Bool
True
  comparable Levitated a
Bottom Levitated a
_ = Bool
True
  comparable Levitated a
_ Levitated a
Bottom = Bool
True
  comparable (Levitate a
x) (Levitate a
y) = a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
comparable a
x a
y

instance Lattice a => Lattice (Levitated a) where
    Levitated a
Top        \/ :: Levitated a -> Levitated a -> Levitated a
\/ Levitated a
_          = Levitated a
forall a. Levitated a
Top
    Levitated a
_          \/ Levitated a
Top        = Levitated a
forall a. Levitated a
Top
    Levitate a
x \/ Levitate a
y = a -> Levitated a
forall a. a -> Levitated a
Levitate (a
x a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
y)
    Levitated a
Bottom     \/ Levitated a
lev_y      = Levitated a
lev_y
    Levitated a
lev_x      \/ Levitated a
Bottom     = Levitated a
lev_x

    Levitated a
Top        /\ :: Levitated a -> Levitated a -> Levitated a
/\ Levitated a
lev_y      = Levitated a
lev_y
    Levitated a
lev_x      /\ Levitated a
Top        = Levitated a
lev_x
    Levitate a
x /\ Levitate a
y = a -> Levitated a
forall a. a -> Levitated a
Levitate (a
x a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
y)
    Levitated a
Bottom     /\ Levitated a
_          = Levitated a
forall a. Levitated a
Bottom
    Levitated a
_          /\ Levitated a
Bottom     = Levitated a
forall a. Levitated a
Bottom

instance Lattice a => BoundedJoinSemiLattice (Levitated a) where
    bottom :: Levitated a
bottom = Levitated a
forall a. Levitated a
Bottom

instance Lattice a => BoundedMeetSemiLattice (Levitated a) where
    top :: Levitated a
top = Levitated a
forall a. Levitated a
Top

-- | Interpret @'Levitated' a@ using the 'BoundedLattice' of @a@.
retractLevitated :: (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a) => Levitated a -> a
retractLevitated :: Levitated a -> a
retractLevitated = a -> (a -> a) -> a -> Levitated a -> a
forall b a. b -> (a -> b) -> b -> Levitated a -> b
foldLevitated a
forall a. BoundedJoinSemiLattice a => a
bottom a -> a
forall a. a -> a
id a
forall a. BoundedMeetSemiLattice a => a
top

-- | Fold 'Levitated'.
foldLevitated :: b -> (a -> b) -> b -> Levitated a -> b
foldLevitated :: b -> (a -> b) -> b -> Levitated a -> b
foldLevitated b
b a -> b
_ b
_ Levitated a
Bottom       = b
b
foldLevitated b
_ a -> b
f b
_ (Levitate a
x) = a -> b
f a
x
foldLevitated b
_ a -> b
_ b
t Levitated a
Top          = b
t

instance Universe a => Universe (Levitated a) where
    universe :: [Levitated a]
universe = Levitated a
forall a. Levitated a
Top Levitated a -> [Levitated a] -> [Levitated a]
forall a. a -> [a] -> [a]
: Levitated a
forall a. Levitated a
Bottom Levitated a -> [Levitated a] -> [Levitated a]
forall a. a -> [a] -> [a]
: (a -> Levitated a) -> [a] -> [Levitated a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Levitated a
forall a. a -> Levitated a
Levitate [a]
forall a. Universe a => [a]
universe
instance Finite a => Finite (Levitated a) where
    universeF :: [Levitated a]
universeF = Levitated a
forall a. Levitated a
Top Levitated a -> [Levitated a] -> [Levitated a]
forall a. a -> [a] -> [a]
: Levitated a
forall a. Levitated a
Bottom Levitated a -> [Levitated a] -> [Levitated a]
forall a. a -> [a] -> [a]
: (a -> Levitated a) -> [a] -> [Levitated a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Levitated a
forall a. a -> Levitated a
Levitate [a]
forall a. Finite a => [a]
universeF
    cardinality :: Tagged (Levitated a) Natural
cardinality = (Natural -> Natural)
-> Tagged (Levitated a) Natural -> Tagged (Levitated a) Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+) (Tagged a Natural -> Tagged (Levitated a) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural))

instance QC.Arbitrary a => QC.Arbitrary (Levitated a) where
    arbitrary :: Gen (Levitated a)
arbitrary = [(Int, Gen (Levitated a))] -> Gen (Levitated a)
forall a. [(Int, Gen a)] -> Gen a
QC.frequency
        [ (Int
1, Levitated a -> Gen (Levitated a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Levitated a
forall a. Levitated a
Top)
        , (Int
1, Levitated a -> Gen (Levitated a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Levitated a
forall a. Levitated a
Bottom)
        , (Int
9, a -> Levitated a
forall a. a -> Levitated a
Levitate (a -> Levitated a) -> Gen a -> Gen (Levitated a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
forall a. Arbitrary a => Gen a
QC.arbitrary)
        ]

    shrink :: Levitated a -> [Levitated a]
shrink Levitated a
Top          = []
    shrink Levitated a
Bottom       = []
    shrink (Levitate a
x) = Levitated a
forall a. Levitated a
Top Levitated a -> [Levitated a] -> [Levitated a]
forall a. a -> [a] -> [a]
: Levitated a
forall a. Levitated a
Bottom Levitated a -> [Levitated a] -> [Levitated a]
forall a. a -> [a] -> [a]
: (a -> Levitated a) -> [a] -> [Levitated a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Levitated a
forall a. a -> Levitated a
Levitate (a -> [a]
forall a. Arbitrary a => a -> [a]
QC.shrink a
x)

instance QC.CoArbitrary a => QC.CoArbitrary (Levitated a) where
    coarbitrary :: Levitated a -> Gen b -> Gen b
coarbitrary Levitated a
Top          = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
    coarbitrary Levitated a
Bottom       = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
    coarbitrary (Levitate a
x) = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int) (Gen b -> Gen b) -> (Gen b -> Gen b) -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary a
x

instance QC.Function a => QC.Function (Levitated a) where
    function :: (Levitated a -> b) -> Levitated a :-> b
function = (Levitated a -> Either Bool a)
-> (Either Bool a -> Levitated a)
-> (Levitated a -> b)
-> Levitated a :-> b
forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap Levitated a -> Either Bool a
forall b. Levitated b -> Either Bool b
fromLevitated Either Bool a -> Levitated a
forall a. Either Bool a -> Levitated a
toLevitated where
        fromLevitated :: Levitated b -> Either Bool b
fromLevitated Levitated b
Top          = Bool -> Either Bool b
forall a b. a -> Either a b
Left Bool
True
        fromLevitated Levitated b
Bottom       = Bool -> Either Bool b
forall a b. a -> Either a b
Left Bool
False
        fromLevitated (Levitate b
x) = b -> Either Bool b
forall a b. b -> Either a b
Right b
x

        toLevitated :: Either Bool a -> Levitated a
toLevitated (Left Bool
True)  = Levitated a
forall a. Levitated a
Top
        toLevitated (Left Bool
False) = Levitated a
forall a. Levitated a
Bottom
        toLevitated (Right a
x)    = a -> Levitated a
forall a. a -> Levitated a
Levitate a
x