{-# 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

deProxy :: forall n. FromNat n => Proxy (n::Nat) -> Int
deProxy _ = 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 Type) where
 ConsTransfers ::  x -> Transfers xs -> Transfers (Cons x xs)
 LastTransfer  ::  x -> Transfers (Last x)

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
  

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 

----
---
-- todays developments

---
-- nat singleton

---
-- insatnces to refactor

-- 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 singleton

data WhichNE xs where 
 IsCons :: WhichNE (Cons x xs)
 IsLast :: WhichNE (Last x)

class KnownNE ne where 
 knownNE :: WhichNE ne

instance KnownNE (Last x) where
 knownNE = IsLast
 
instance KnownNE (Cons x xs) where
 knownNE = IsCons
 
---
-- instances to refactor


-- stateful
type family StatefulTransfers (xs :: Nonempty Type) i o = (c :: Constraint) | c -> xs i o where
 StatefulTransfers (Last x) i o = (Stateful x i o)
 StatefulTransfers (Cons x xs) i o = (Stateful x i o,Stateful (Transfers xs) [i] [o])

class StatefulTransfers xs i o => StatefulTransfersConstraint (xs :: Nonempty Type) i o | xs -> i o
instance StatefulTransfers xs i o => StatefulTransfersConstraint xs i o

instance StatefulTransfersConstraint xs i o => Stateful (Transfers xs) [i] [o] where


-- transfer length
class TransfersLength (xs :: Nonempty Type) 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)

-- read and show
instance (Show x) => Show (Transfers (Last x)) where
 show (LastTransfer x) = show x

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

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