{-# LANGUAGE
    MultiParamTypeClasses,
    FlexibleContexts,
    FlexibleInstances,
    UndecidableInstances,
    ExistentialQuantification,
    TypeSynonymInstances,
    Rank2Types,
    NoMonomorphismRestriction #-}

module Sys(Sys(..)
          ,Sig(..)
          ) where

import CSSM


import Prelude hiding ((.), id)
import Control.Category
import Control.Applicative
import Control.Monad
import Control.Arrow
import Data.Functor.Identity
import Control.Monad.State

-- For Sys's state existential type we need to add some interfaces.
import Struct 
import Data
import Control
import Array



{-

2. Data type
------------

Define a data type to bundle initial state together with update
functions that support the operations above.

The goal is to make this Sys an instance of Category & Arrow.

Unfortunately it's not possible to expose the state type as a
parameter in Sys:

   data Sys s m i o = Sys s ((s, i) -> m (s, o))

Composing 2 of these will have the type

   Sys s1 m b c -> Sys s2 m a b -> Sys (s1,s2) m a b

which will not fit the expected kind for Category: * -> * -> *.  To
hide the non-constant state type we use an existential quantification.
The monad is just a parameter.

To be able to get at the state later (i.e. for abstract evaluation)
some interfaces are exposed.  This takes an extra parameter p to
parameterize over the state primitive type.


-}
  
--- What we want is composition and compilation / evaluation.  Let's
--- just express that directly.  Composition is handled by the
--- standard type classes below, and compilation is handled by this
--- class.


data Sys stx m i o = 
  forall s. (CSSM stx m s i o) => Sys (SSM m s i o)



-- Sys can be composed by composing the update functions and the
-- initial state variables.  This gives rise to Category.  

instance Monad m => Category (Sys stx m) where
  (.) (Sys f) (Sys g) = Sys (cssmSer f g)
  id  = Sys (cssmPure id) 
  
-- Adding also parallel composition and lifting of pure functions
-- gives an Arrow instance.  
  
-- ( Note that arr and first are enough, but we already have (***) so
-- use that to implement first. )
instance Monad m => Arrow (Sys stx m) where
  arr f = Sys (cssmPure f)
  (***) (Sys f) (Sys g) = Sys (cssmPar f g)
  first   a = a *** (arr id)
  second  a = (arr id) *** a
  
  
{- 

Note that these Arrows can not be the Kleisli arrows of a Monad
because of a value to type dependency that prevents composition.

In short, the following types are not isomorphic:

  i -> (Sys () o)
  Sys i o

In the former, the hidden s type can depend on the value of :: i
terms, while in the latter it cannot.

-}


-- Sig are Sys without input.  Applying an Sys to a
-- Sig using (.) produces another Sig.
type Sig stx m o = Sys stx m () o


-- Infinite lists can be converted to Sig by allowing infinite state
-- size.  This defeats the point of having a finite initial state and
-- update equation for abstract evaluation.  However, it's useful for
-- testing Sys with inputs that cannot be represented as a Sig, i.e
-- live input from a DAC.

-- sigInf :: (PrimData p [o], Monad m) => [o] -> Sys p m () o
-- sigInf = Sys $ \(d:ds, ()) -> return (ds, d)






-- Define Functor and Applicative instances for the output of Sys.
-- This is useful for lifting arithmetic to Sys / Sig.
instance Monad m => Functor (Sys stx m i) where
  fmap f op = (arr f) . op
instance Monad m => Applicative (Sys stx m i) where
  pure f = arr $ \_ -> f
  (<*>) f a = fmap (uncurry ($)) (f &&& a)


-- Other queries.
-- stateSize (Sys _ s0) = n where
--  (n, _) = primIndex 0 s0






{- EXAMPLES


-- Sig can be unfolded to infinite lists.  
sigRun :: Sig m a -> [a]
sigRun (Sys update init) = f init where
  f s = (o:os) where
    (s', o) = update (s, ())
    os = f s'


-- Lift sequences represented as functions to Sig.
-- sigFun :: (Num n, PrimData n) => (n -> a) -> Sys () a
sigFun f = (arr f) . ramp




-- Define some well-known linear Sys.
sigOp0 fn = Sys fn 0


-- id = int . dif = dif . int
int = sigOp0 $ \(s, i) -> do { o <- i+s; return (o, o) }
dif = sigOp0 $ \(s, i) -> let o = i-s in (i, o)

z   = sigOp0 $ \(s, i) -> (i, s)

-- Define some well-known signals.
ndirac :: (Num n, PrimData n) => n -> Sig m n
ndirac n0 = Sys update n0 where
  update (n, i) = (n-1, if (n == 0) then 1 else 0)
  
nstep n = int . (ndirac n)
nramp n = int . (nstep n)

dirac = ndirac 0
step  = nstep 0
ramp  = nramp 0   -- [1,2,..]

  -}