{-# Language DataKinds ,AllowAmbiguousTypes,FunctionalDependencies, RankNTypes,TypeOperators ,ScopedTypeVariables, TypeFamilies , TypeFamilyDependencies , KindSignatures , GADTs , TypeApplications ,  FlexibleInstances , StandaloneDeriving , MultiParamTypeClasses , FlexibleContexts , UndecidableInstances , ConstraintKinds #-}

import Data.Proxy
import Data.Kind

class Stateful s i o | s -> i , s -> o where
 stateFunction :: s -> i -> (s,o)
 
---
-- Lag

data Lag = Lag Double Double deriving (Read,Show)

instance Stateful Lag Double Double where
 stateFunction (Lag la b) i = (Lag la o,o) 
  where
   o = b * x + i * y
   x = la ** 0.01
   y = (1-x)
   
egLag :: Lag 
egLag = Lag 0.5 0

---
-- Extend

data Extend = Extend Lag deriving (Read,Show)

instance Stateful Extend Double Double where
 stateFunction (Extend l) i = (Extend l',o)
  where
   (l',x) = stateFunction l i
   o = 2*i-x

egExtend :: Extend 
egExtend = Extend $ Lag 0.5 0


---
-- Nat

data Nat = S Nat | Z

-- Type-level addition
type family Plus (x :: Nat) (y :: Nat) :: Nat where
  Plus Z y = y
  Plus (S x) y = S (Plus x y)

proxyPlus :: Proxy (n::Nat) -> Proxy (m::Nat) -> Proxy(Plus n m)
proxyPlus _ _ = Proxy

-- Value-level conversion for Nat
class FromNat (n :: Nat) where
  fromNat :: Int

instance FromNat Z where
  fromNat = 0

instance FromNat n => FromNat (S n) where
  fromNat = 1 + fromNat @n
  
---
-- Nonempty

data Nonempty a = Cons a (Nonempty a) | Last a

type family Length (xs :: Nonempty Type) :: Nat where
 Length ('Last x) = (S Z)
 Length ('Cons x xs) =  S (Length xs)
 
---
-- Transfers

data Transfers (xs :: Nonempty *) where
 ConsTransfers ::  x -> Transfers xs -> Transfers (Cons x xs)
 LastTransfer  ::  x -> Transfers (Last x)

instance (Stateful x i o,Stateful (Transfers xs) [i] [o]) => Stateful (Transfers (Cons x xs)) [i] [o] where
 stateFunction (ConsTransfers x xs) (i:is) = let ((x',o),(xs',os)) = (stateFunction x i,stateFunction xs is) in (ConsTransfers x' xs',(:) o os)

instance Stateful x i o => Stateful (Transfers (Last x)) [i] [o] where
 stateFunction (LastTransfer x) [i] = let (x',o) = stateFunction x i in (LastTransfer x',[o])

deProxy :: forall n. FromNat n => Proxy (n::Nat) -> Int
deProxy _ = fromNat @n

class TransfersLength (xs :: Nonempty *) where
 transfersLength :: Transfers xs -> Proxy (Length xs)

instance TransfersLength (Last a) where
 transfersLength _ = Proxy @(S Z)

instance TransfersLength xs => TransfersLength (Cons x xs) where
 transfersLength (ConsTransfers _ xs) = proxyPlus (Proxy @(S Z)) (transfersLength xs)

transfers :: (TransfersLength xs,FromNat n,n~(Length xs),Stateful (Transfers xs) [i] [o]) => Transfers xs -> i -> (Transfers xs,[o])
transfers ts i = stateFunction ts (replicate l i)
 where
  l = deProxy $ transfersLength ts
  
type Disp x = (Read x,Show x)

instance (Disp x) => Show (Transfers (Last x)) where
 show (LastTransfer x) = show x

-- readsPrec :: String -> [(a, String)]
instance (Disp x) => Read (Transfers (Last x)) where
 readsPrec n str = let [(a,b)] = readsPrec n str in [(LastTransfer a,b)]

instance (Disp x,Disp (Transfers xs)) => Show (Transfers (Cons x xs)) where
 show (ConsTransfers x xs) = show (x,xs)
   
instance (Disp x,Disp (Transfers xs)) => Read (Transfers (Cons x xs)) where
 readsPrec n str = let [((x,xs),b)] = readsPrec n str in [(ConsTransfers x xs,b)]

egTransfers :: Transfers (Cons Lag (Last Extend))
egTransfers = ConsTransfers egLag (LastTransfer egExtend)

test :: IO ()
test = do
 let f = egTransfers
 let (f',o) = transfers f 1
 print f
 print f'
 print o
 
main = test