{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}


-- |

-- Module      : OAlg.Structure.PartiallyOrdered.Definition

-- Description : partial orderings.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- partial orderings..

module OAlg.Structure.PartiallyOrdered.Definition
  ( -- * Partial Ordering

    PartiallyOrdered(..), Empty(..), Full(..)
  )
  where

import OAlg.Prelude

import OAlg.Structure.Oriented.Opposite

--------------------------------------------------------------------------------

-- PartiallyOrdered -


-- | partially ordered types.

--

--  __Properties__ Let @__a__@ be an instance of 'PartiallyOrdered', then holds:

--

--  (1) For all @x@ in @__a__@ holds: @x '<<=' x@.

--

--  (2) For all @x@, @y@ in @__a__@ holds: If @x '<<=' y@ and @y '<<=' x@ then

--  @x '==' y@.

--

--  (3) For all @x@, @y@, @z@ in @__a__@ holds: If @x '<<=' y@ and @y '<<=' z@ then

--  @x '<<=' z@.

class Eq a => PartiallyOrdered a where

  infix 4 <<=
  (<<=) :: a -> a -> Bool

instance PartiallyOrdered x => PartiallyOrdered (Op x) where Op x
x <<= :: Op x -> Op x -> Bool
<<= Op x
y = x
y x -> x -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= x
x

instance PartiallyOrdered Bool where
  <<= :: Bool -> Bool -> Bool
(<<=) = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
(<=)

instance Eq x => PartiallyOrdered [x] where
  [] <<= :: [x] -> [x] -> Bool
<<= [x]
_  = Bool
True
  [x]
_ <<= []  = Bool
False
  (x
x:[x]
xs) <<= (x
y:[x]
ys) = case x
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
y of
    Bool
True  -> [x]
xs [x] -> [x] -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= [x]
ys
    Bool
False -> (x
xx -> [x] -> [x]
forall a. a -> [a] -> [a]
:[x]
xs) [x] -> [x] -> Bool
forall a. PartiallyOrdered a => a -> a -> Bool
<<= [x]
ys

    
--------------------------------------------------------------------------------

-- Empty -


-- | the minimal element of a patrially ordered type..

--

-- __Property__ Let @__a__@ be an instance of 'Empty', then for all @x@ in @__a__@ holds:

-- @empty '<<=' x@.

class PartiallyOrdered a => Empty a where
  empty :: a
  isEmpty :: a -> Bool
  isEmpty a
x = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Empty a => a
empty
  
instance Empty Bool where
  empty :: Bool
empty = Bool
False

instance Eq x => Empty [x] where
  empty :: [x]
empty = []
  isEmpty :: [x] -> Bool
isEmpty [] = Bool
True
  isEmpty [x]
_  = Bool
False
  
--------------------------------------------------------------------------------

-- Full -


-- | the maximal element of a partially ordered type.

--

-- __Property__ Let @__a__@ be an instance of 'Full', then for all @x@ in @__a__@ holds:

-- @x '<<=' full@.

class PartiallyOrdered a => Full a where
  full :: a
  isFull :: a -> Bool
  isFull a
x = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Full a => a
full
  
instance Full Bool where
  full :: Bool
full = Bool
True