{-# LANGUAGE TypeOperators, KindSignatures, ScopedTypeVariables, EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}

module FullSession.Base where

class Nat n where
  nat :: n
instance Nat Z where
  nat = Z
instance Nat n => Nat (S n) where
  nat = S nat

data Z = Z deriving Show
data S n = S n deriving Show
data P n = P n

data T = T
data F = F

class EqNat x y b | x y -> b
instance EqNat Z Z T
instance EqNat (S n) Z F
instance EqNat Z (S n) F
instance EqNat n n' b => EqNat (S n) (S n') b

class Sub n n' where 
  sub :: n -> n' -> SubT n n'
  sub_ :: Either n n' -> SubT n n'
instance Sub n n where { sub _ _ = Z; sub_ _ = Z }
instance Sub (S n) n where { sub _ _ = S Z; sub_ _ = S Z }
instance Sub (S (S n)) n where { sub _ _ = S (S Z); sub_ _ = S (S Z) }
instance Sub n (S n) where { sub _ _ = P Z; sub_ _ = P Z }
instance Sub n (S (S n)) where { sub _ _ = P (P Z); sub_ _ = P (P Z) }

type family SubT n n' :: *
type instance SubT n n = Z
type instance SubT (S n) n = S Z
type instance SubT (S (S n)) n = S (S Z)
type instance SubT n (S n) = P Z
type instance SubT n (S (S n)) = P (P Z)

data ss :> s = ss :> s
data Nil = Nil

tinit :: ss :> s -> ss
tinit (ss :> _) = ss

tlast :: ss :> s -> s
tlast (_ :> s) = s

class Length ss l | ss -> l where
  len_ :: ss -> l
instance Length ss l => Length (ss :> s) (S l) where
  len_ ~(ss :> s) = S (len_ ss)
instance Length Nil Z where
  len_ _ = Z

class -- (Length ss l, Sub l (S n), PickupR ss (SubT l (S n)) s) =>
       Pickup ss n s | ss n -> s where
  pickup :: ss -> n -> s
instance (Length ss l, Sub l (S n), PickupR ss (SubT l (S n)) s) 
    => Pickup ss n s where
  pickup ss n = pickupR ss (sub (len_ ss) (S n))

class PickupR ss n s | ss n -> s where
  pickupR :: ss -> n -> s
instance ss ~ (ss':>t) => PickupR ss Z t where
  pickupR (_ :> t) _ = t
instance (PickupR ss' n t, ss ~ (ss':>s')) => PickupR ss (S n) t where
  pickupR (ss' :> _) (S n) = pickupR ss' n

class -- (Length ss l, Sub l (S n), UpdateR ss (SubT l (S n)) t ss') =>
    Update ss n t ss' | ss n t -> ss' where
  update :: ss -> n -> t -> ss'
instance (Length ss l, Sub l (S n), UpdateR ss (SubT l (S n)) t ss') 
 => Update ss n t ss' where
  update ss n t = updateR ss (sub (len_ ss) (S n)) t

class UpdateR ss n t ss' | ss n t -> ss' where
  updateR ::  ss -> n -> t -> ss'
instance UpdateR (ss:>s) Z t (ss:>t) where
  updateR (ss:>_) _ t = ss :> t
instance UpdateR ss n t ss' => UpdateR (ss:>s) (S n) t (ss':>s) where
  updateR (ss:>s) (S n) t = updateR ss n t :> s