{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-- |
-- Module      : OAlg.Entity.Sequence.Definition
-- Description : basic definitions for sequences as mappings of an index to an entity
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- basic definitions for sequences as mappings of an index to an entity.
module OAlg.Entity.Sequence.Definition
  ( -- * Sequence
    Sequence(..), listN, (?), isEmpty, span, support, image

    -- * Constructable
  , ConstructableSequence(..)
  , sqcIndexMap

    -- * Exception
  , SequenceException(..)
  ) where

import Data.Proxy
import Data.List (head,zip,sort,group,map,filter)

import OAlg.Prelude
import OAlg.Structure.Ring
import OAlg.Structure.Number

import OAlg.Entity.Sequence.Set
import OAlg.Entity.Sequence.Graph

--------------------------------------------------------------------------------
-- SequenceException -

-- | sequence exceptions which are sub exceptions from 'SomeOAlgException'.
data SequenceException
  = IndexOutOfSupport
  deriving (SequenceException -> SequenceException -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SequenceException -> SequenceException -> Bool
$c/= :: SequenceException -> SequenceException -> Bool
== :: SequenceException -> SequenceException -> Bool
$c== :: SequenceException -> SequenceException -> Bool
Eq,Int -> SequenceException -> ShowS
[SequenceException] -> ShowS
SequenceException -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SequenceException] -> ShowS
$cshowList :: [SequenceException] -> ShowS
show :: SequenceException -> String
$cshow :: SequenceException -> String
showsPrec :: Int -> SequenceException -> ShowS
$cshowsPrec :: Int -> SequenceException -> ShowS
Show)

instance Exception SequenceException where
  toException :: SequenceException -> SomeException
toException   = forall e. Exception e => e -> SomeException
oalgExceptionToException
  fromException :: SomeException -> Maybe SequenceException
fromException = forall e. Exception e => SomeException -> Maybe e
oalgExceptionFromException

--------------------------------------------------------------------------------
-- Sequence -

-- | sequences as mappings of an index.
--
--  __Definition__ Let @__s__@, @__i__@, @__x__@ be an instance of 'Sequence' and @xs@ be
--  in @__s__ __x__@, then we call @xs@ __/finite/__ if and only if the evaluation of
--  @'lengthN' xs@ terminates and will not end up in an exception.
--
--  __Property__ Let @__s__@, @__i__@, @__x__@ be an instance of 'Sequence', then holds:
--
-- (1) For all @xs@ in @__s__ __x__@ holds:
--
--     (1) 'graph' is constant in its first parameter.
--
--     (2) If @xs@ is finite, then @'lengthN' xs '==' 'lengthN' ('graph' p xs)@ for any
--     @p@.
--
-- (2) For all @xs@ in @__s__ __x__@ holds:
--
--     (1) 'list' is constant in its first parameter.
--
--     (2) For all @..(x,i)':'(x,j)..@ in @xs@ holds: @i '<' j@.
--
--     (3) If @xs@ is finite, then @'lengthN' xs '==' 'lengthN' ('list' p xs)@ for any
--     @p@.
--
-- (3) Let @xs@ be in @__s__ __x__@ and @i@ in @__i__@, then holds:
-- there exists an @x@ in @__x__@ with @xs '?' i@ matches @'Just' x@ if and only if there
-- exists an @(i',x)@ in @'graph' (Just i) xs@ such that @i '==' i'@.
--
-- __Note__ The first parameter of 'graph' - respectively 'list' - serves only as a /proxy/
-- and as such it is only relevant on the type level.
class (LengthN (s x), Ord i) => Sequence s i x where
  {-# MINIMAL graph | list #-}

  -- | the associated graph of a sequence
  graph :: p i -> s x -> Graph i x
  graph p i
p s x
xs = forall i x. [(i, x)] -> Graph i x
Graph forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(x
x,i
i) -> (i
i,x
x)) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> [(x, i)]
list p i
p s x
xs

  -- | the associated list of its items together with there index.
  list :: p i -> s x -> [(x,i)]
  list p i
p s x
xs = forall a b. (a -> b) -> [a] -> [b]
map (\(i
i,x
x) -> (x
x,i
i)) [(i, x)]
xs' where Graph [(i, x)]
xs' = forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Graph i x
graph p i
p s x
xs

  -- | the @i@-th item.
  (??) :: s x -> i -> Maybe x
  s x
xs ?? i
i = forall i x. Ord i => Graph i x -> i -> Maybe x
gphLookup (forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Graph i x
graph (forall a. a -> Maybe a
Just i
i) s x
xs) i
i

--------------------------------------------------------------------------------
-- listN -

-- | the indexed list of the sequence.
listN :: Sequence s N x => s x -> [(x,N)]
listN :: forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN = forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> [(x, i)]
list (forall {k} (t :: k). Proxy t
Proxy :: Proxy N)

--------------------------------------------------------------------------------
-- ConstructableSequence -

-- | constructable sequences.
class (Entity x, Entity i, Sequence s i x) => ConstructableSequence s i x where

  -- | constructs a sequence.
  sequence :: (i -> Maybe x) -> Set i -> s x

  infixl 7 <&
  -- | restricts a sequence.
  (<&) :: s x -> Set i -> s x
  (<&) s x
xs Set i
is = forall (s :: * -> *) i x.
ConstructableSequence s i x =>
(i -> Maybe x) -> Set i -> s x
sequence (s x
xsforall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
??) Set i
is

--------------------------------------------------------------------------------
-- sqcIndexmap -

-- | mapping the indices according to the given set.
sqcIndexMap :: (ConstructableSequence s i x, Sequence s j x)
  => Set i -> (i -> j) -> s x -> s x
sqcIndexMap :: forall (s :: * -> *) i x j.
(ConstructableSequence s i x, Sequence s j x) =>
Set i -> (i -> j) -> s x -> s x
sqcIndexMap Set i
is i -> j
f s x
xjs = forall (s :: * -> *) i x.
ConstructableSequence s i x =>
(i -> Maybe x) -> Set i -> s x
sequence ((s x
xjsforall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
??)forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
.i -> j
f) Set i
is


--------------------------------------------------------------------------------
-- isEmpty -

-- | checks for being empty.
isEmpty :: Sequence s i x => p i -> s x -> Bool
isEmpty :: forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Bool
isEmpty p i
p s x
xs = case forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> [(x, i)]
list p i
p s x
xs of
  [] -> Bool
True
  [(x, i)]
_  -> Bool
False

--------------------------------------------------------------------------------
-- (?) -

-- | the @i@-th element of the sequence.
--
--  __Property__ Let @xs@ be in @__s__ __x__@ and @i@ in @__i__@ for a instance of
--  @'Sequence' __s__ __i__ __x__@, then holds: If @i@ is in the 'support' of @xs@ then
--  @xs '?' i@ is the @i@-th item of @xs@, else its evaluation will end up by throwing a
--  'IndexOutOfSupport'-exception.
(?) :: Sequence s i x => s x -> i -> x
s x
xs ? :: forall (s :: * -> *) i x. Sequence s i x => s x -> i -> x
? i
i = case s x
xs forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
?? i
i of
  Just x
x -> x
x
  Maybe x
Nothing -> forall a e. Exception e => e -> a
throw SequenceException
IndexOutOfSupport
  
--------------------------------------------------------------------------------
-- support -

-- | the support of a sequence, i.e. all the indices which are not mapped to 'Nothing'.
support :: Sequence s i x => p i -> s x -> Set i
support :: forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Set i
support p i
p s x
xs = forall x. [x] -> Set x
Set forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. Graph i x -> [(i, x)]
gphxs forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Graph i x
graph p i
p s x
xs

--------------------------------------------------------------------------------
-- span -

-- | the span of a sequence.
span :: Sequence s i x => p i -> s x -> Span i
span :: forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Span i
span p i
p = forall x. Set x -> Span x
setSpan forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Set i
support p i
p 

--------------------------------------------------------------------------------
-- image -

-- | the image of a sequence, i.e. all the entities are hit by the mapping.
image :: (Sequence s i x, Ord x) => p i -> s x -> Set x
image :: forall (s :: * -> *) i x (p :: * -> *).
(Sequence s i x, Ord x) =>
p i -> s x -> Set x
image p i
p s x
xs = forall x. [x] -> Set x
Set forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. [a] -> a
head forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Eq a => [a] -> [[a]]
group forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Ord a => [a] -> [a]
sort forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall i x. Graph i x -> [(i, x)]
gphxs forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Graph i x
graph p i
p s x
xs

--------------------------------------------------------------------------------
-- [] - Sequence -

instance (Integral r, Enum r) => Sequence [] r x where
  graph :: forall (p :: * -> *). p r -> [x] -> Graph r x
graph p r
_ [x]
xs = forall i x. [(i, x)] -> Graph i x
Graph ([forall r. Semiring r => r
rZero..] forall a b. [a] -> [b] -> [(a, b)]
`zip` [x]
xs)

--------------------------------------------------------------------------------
-- lstSqc -

-- | @'lstSqc' f is@ maps the index set @is@ according to @f@ and strips out all 'Nothing'
--   items.
lstSqc :: (i -> Maybe x) -> Set i -> [x]
lstSqc :: forall i x. (i -> Maybe x) -> Set i -> [x]
lstSqc i -> Maybe x
mx (Set [i]
is)
  = forall a b. (a -> b) -> [a] -> [b]
map forall a. HasCallStack => Maybe a -> a
fromJust
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter forall a. Maybe a -> Bool
isJust
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map i -> Maybe x
mx [i]
is

--------------------------------------------------------------------------------
-- [] - ConstructableSequence -

instance (Integral r, Enum r, Entity x) => ConstructableSequence [] r x where
  sequence :: (r -> Maybe x) -> Set r -> [x]
sequence = forall i x. (i -> Maybe x) -> Set i -> [x]
lstSqc

--------------------------------------------------------------------------------
-- Set - ConstructableSequence -

instance (Integral r, Enum r) => Sequence Set r x where
  list :: forall (p :: * -> *). p r -> Set x -> [(x, r)]
list p r
_ (Set [x]
xs) = [x]
xs forall a b. [a] -> [b] -> [(a, b)]
`zip` [forall r. Semiring r => r
rZero .. ]
  
instance (Integral r, Enum r, Entity x, Ord x) => ConstructableSequence Set r x where
  sequence :: (r -> Maybe x) -> Set r -> Set x
sequence = forall x i. Ord x => (i -> Maybe x) -> Set i -> Set x
setSqc

--------------------------------------------------------------------------------
-- Graph - ConstructableSequence -

instance Ord i => Sequence (Graph i) i x where
  graph :: forall (p :: * -> *). p i -> Graph i x -> Graph i x
graph p i
_ = forall x. x -> x
id

instance (Entity x, Entity i, Ord i) => ConstructableSequence (Graph i) i x where
  sequence :: (i -> Maybe x) -> Set i -> Graph i x
sequence = forall i x. (i -> Maybe x) -> Set i -> Graph i x
gphSqc