{-# 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
(SequenceException -> SequenceException -> Bool)
-> (SequenceException -> SequenceException -> Bool)
-> Eq SequenceException
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SequenceException -> SequenceException -> Bool
== :: SequenceException -> SequenceException -> Bool
$c/= :: SequenceException -> SequenceException -> Bool
/= :: SequenceException -> SequenceException -> Bool
Eq,Int -> SequenceException -> ShowS
[SequenceException] -> ShowS
SequenceException -> String
(Int -> SequenceException -> ShowS)
-> (SequenceException -> String)
-> ([SequenceException] -> ShowS)
-> Show SequenceException
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SequenceException -> ShowS
showsPrec :: Int -> SequenceException -> ShowS
$cshow :: SequenceException -> String
show :: SequenceException -> String
$cshowList :: [SequenceException] -> ShowS
showList :: [SequenceException] -> ShowS
Show)

instance Exception SequenceException where
  toException :: SequenceException -> SomeException
toException   = SequenceException -> SomeException
forall e. Exception e => e -> SomeException
oalgExceptionToException
  fromException :: SomeException -> Maybe SequenceException
fromException = SomeException -> Maybe SequenceException
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 = [(i, x)] -> Graph i x
forall i x. [(i, x)] -> Graph i x
Graph ([(i, x)] -> Graph i x) -> [(i, x)] -> Graph i x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((x, i) -> (i, x)) -> [(x, i)] -> [(i, x)]
forall a b. (a -> b) -> [a] -> [b]
map (\(x
x,i
i) -> (i
i,x
x)) ([(x, i)] -> [(i, x)]) -> [(x, i)] -> [(i, x)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ p i -> s x -> [(x, i)]
forall (p :: * -> *). p i -> s x -> [(x, i)]
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 = ((i, x) -> (x, i)) -> [(i, x)] -> [(x, i)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i
i,x
x) -> (x
x,i
i)) [(i, x)]
xs' where Graph [(i, x)]
xs' = p i -> s x -> Graph i x
forall (p :: * -> *). p i -> s x -> Graph i x
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 = Graph i x -> i -> Maybe x
forall i x. Ord i => Graph i x -> i -> Maybe x
gphLookup (Maybe i -> s x -> Graph i x
forall (p :: * -> *). p i -> s x -> Graph i x
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Graph i x
graph (i -> Maybe i
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 = Proxy N -> s x -> [(x, N)]
forall (p :: * -> *). p N -> s x -> [(x, N)]
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> [(x, i)]
list (Proxy N
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 = (i -> Maybe x) -> Set i -> s x
forall (s :: * -> *) i x.
ConstructableSequence s i x =>
(i -> Maybe x) -> Set i -> s x
sequence (s x
xss x -> i -> Maybe x
forall (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 = (i -> Maybe x) -> Set i -> s x
forall (s :: * -> *) i x.
ConstructableSequence s i x =>
(i -> Maybe x) -> Set i -> s x
sequence ((s x
xjss x -> j -> Maybe x
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
??)(j -> Maybe x) -> (i -> j) -> i -> Maybe x
forall y z x. (y -> z) -> (x -> y) -> x -> z
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 p i -> s x -> [(x, i)]
forall (p :: * -> *). p i -> s x -> [(x, i)]
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 s x -> i -> Maybe x
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
?? i
i of
  Just x
x -> x
x
  Maybe x
Nothing -> SequenceException -> x
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 = [i] -> Set i
forall x. [x] -> Set x
Set ([i] -> Set i) -> [i] -> Set i
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((i, x) -> i) -> [(i, x)] -> [i]
forall a b. (a -> b) -> [a] -> [b]
map (i, x) -> i
forall a b. (a, b) -> a
fst ([(i, x)] -> [i]) -> [(i, x)] -> [i]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Graph i x -> [(i, x)]
forall i x. Graph i x -> [(i, x)]
gphxs (Graph i x -> [(i, x)]) -> Graph i x -> [(i, x)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ p i -> s x -> Graph i x
forall (p :: * -> *). p i -> s x -> Graph i x
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 = Set i -> Span i
forall x. Set x -> Span x
setSpan (Set i -> Span i) -> (s x -> Set i) -> s x -> Span i
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. p i -> s x -> Set i
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 = [x] -> Set x
forall x. [x] -> Set x
Set ([x] -> Set x) -> [x] -> Set x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ([x] -> x) -> [[x]] -> [x]
forall a b. (a -> b) -> [a] -> [b]
map [x] -> x
forall a. HasCallStack => [a] -> a
head ([[x]] -> [x]) -> [[x]] -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [x] -> [[x]]
forall a. Eq a => [a] -> [[a]]
group ([x] -> [[x]]) -> [x] -> [[x]]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [x] -> [x]
forall a. Ord a => [a] -> [a]
sort ([x] -> [x]) -> [x] -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((i, x) -> x) -> [(i, x)] -> [x]
forall a b. (a -> b) -> [a] -> [b]
map (i, x) -> x
forall a b. (a, b) -> b
snd ([(i, x)] -> [x]) -> [(i, x)] -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Graph i x -> [(i, x)]
forall i x. Graph i x -> [(i, x)]
gphxs (Graph i x -> [(i, x)]) -> Graph i x -> [(i, x)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ p i -> s x -> Graph i x
forall (p :: * -> *). p i -> s x -> Graph i x
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 = [(r, x)] -> Graph r x
forall i x. [(i, x)] -> Graph i x
Graph ([r
forall r. Semiring r => r
rZero..] [r] -> [x] -> [(r, x)]
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)
  = (Maybe x -> x) -> [Maybe x] -> [x]
forall a b. (a -> b) -> [a] -> [b]
map Maybe x -> x
forall a. HasCallStack => Maybe a -> a
fromJust
  ([Maybe x] -> [x]) -> [Maybe x] -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Maybe x -> Bool) -> [Maybe x] -> [Maybe x]
forall a. (a -> Bool) -> [a] -> [a]
filter Maybe x -> Bool
forall a. Maybe a -> Bool
isJust
  ([Maybe x] -> [Maybe x]) -> [Maybe x] -> [Maybe x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (i -> Maybe x) -> [i] -> [Maybe x]
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 = (r -> Maybe x) -> Set r -> [x]
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 [x] -> [r] -> [(x, r)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [r
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 = (r -> Maybe x) -> Set r -> Set x
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
_ = Graph i x -> Graph i x
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 = (i -> Maybe x) -> Set i -> Graph i x
forall i x. (i -> Maybe x) -> Set i -> Graph i x
gphSqc