module Control.Concurrent.Session.List
( Nil ()
, Cons ()
, TyListLength (..)
, nil
, cons
, modifyCons
, tyHead
, tyTail
, TyList ()
, TyListIndex (..)
, TyListUpdateVar (..)
, TyListTake (..)
, TyListDrop (..)
, TyListAppend (..)
, TyListReverse (..)
, TyListElem (..)
) where
import Control.Concurrent.Session.Number
data Nil :: * where
Nil :: Nil
data Cons :: * -> * -> * where
Cons :: t -> n -> Cons t n
class TyListLength list length | list -> length where
tyListLength :: list -> length
instance TyListLength Nil (D0 E) where
tyListLength Nil = (D0 E)
instance (TyListLength n len, Succ len len') => TyListLength (Cons t n) len' where
tyListLength (Cons _ nxt) = tySucc . tyListLength $ nxt
instance Show Nil where
show Nil = "Nil"
instance (TyListLength n l, Succ l l', Show n, Show t) => Show (Cons t n) where
show (Cons val nxt) = "Cons " ++ (show val) ++ " (" ++ (show nxt) ++ ")"
nil :: Nil
nil = Nil
cons :: (TyList n) => t -> n -> (Cons t n)
cons t n = Cons t n
modifyCons :: (TyList n1, TyList n2) => (t1 -> t2) -> (n1 -> n2) -> (Cons t1 n1) -> (Cons t2 n2)
modifyCons f g (Cons t n) = cons (f t) (g n)
class TyList l
instance TyList Nil
instance (TyList nxt) => TyList (Cons val nxt)
tyHead :: (Cons t n) -> t
tyHead (Cons t _) = t
tyTail :: (TyList n) => (Cons t n) -> n
tyTail (Cons _ n) = n
class TyListIndex lst idx res | lst idx -> res where
tyListIndex :: lst -> idx -> res
tyListUpdate :: lst -> idx -> res -> lst
instance TyListIndex (Cons res nxt) (D0 E) res where
tyListIndex (Cons val _) _ = val
tyListUpdate (Cons _ nxt) _ val = (Cons val nxt)
instance ( TyListIndex nxt idx' res
, Pred idx idx'
, SmallerThan idx' len
, TyListLength nxt len) =>
TyListIndex (Cons val nxt) idx res where
tyListIndex (Cons _ nxt) idx = tyListIndex nxt (tyPred idx)
tyListUpdate (Cons val nxt) idx val'
= Cons val (tyListUpdate nxt (tyPred idx) val')
class TyListUpdateVar lst1 idx val lst2 | lst1 idx val -> lst2 where
tyListUpdateVar :: lst1 -> idx -> val -> lst2
instance ( TyListTake idx lst1 prefix
, TyListDrop idxP lst1 suffix
, Succ idx idxP
, TyListAppend prefix (Cons val suffix) lst2
) =>
TyListUpdateVar lst1 idx val lst2 where
tyListUpdateVar lst1 idx val
= tyListAppend prefix (Cons val suffix)
where
prefix = tyListTake idx lst1
idxP = tySucc idx
suffix = tyListDrop idxP lst1
class TyListAppend a b c | a b -> c where
tyListAppend :: a -> b -> c
instance TyListAppend Nil b b where
tyListAppend _ b = b
instance (TyListAppend nxt b nxt') =>
TyListAppend (Cons val nxt) b (Cons val nxt') where
tyListAppend (Cons val nxt) b
= Cons val $ tyListAppend nxt b
class TyListDrop cnt lst res | cnt lst -> res where
tyListDrop :: cnt -> lst -> res
instance TyListDrop (D0 E) (Cons val nxt) (Cons val nxt) where
tyListDrop _ lst = lst
instance TyListDrop cnt Nil Nil where
tyListDrop _ lst = lst
instance ( TyListDrop cnt' nxt lst
, Pred cnt cnt'
) =>
TyListDrop cnt (Cons val nxt) lst where
tyListDrop cnt (Cons _ nxt) = tyListDrop (tyPred cnt) nxt
class TyListTake cnt lst res | cnt lst -> res where
tyListTake :: cnt -> lst -> res
instance TyListTake (D0 E) Nil Nil where
tyListTake _ _ = nil
instance TyListTake (D0 E) (Cons val nxt) Nil where
tyListTake _ _ = nil
instance ( TyListTake cnt' nxt nxt'
, Pred (D1 r) cnt'
) =>
TyListTake (D1 r) (Cons val nxt) (Cons val nxt') where
tyListTake cnt (Cons val nxt)
= Cons val (tyListTake (tyPred cnt) nxt)
instance ( TyListTake cnt' nxt nxt'
, Pred (D2 r) cnt'
) =>
TyListTake (D2 r) (Cons val nxt) (Cons val nxt') where
tyListTake cnt (Cons val nxt)
= Cons val (tyListTake (tyPred cnt) nxt)
instance ( TyListTake cnt' nxt nxt'
, Pred (D3 r) cnt'
) =>
TyListTake (D3 r) (Cons val nxt) (Cons val nxt') where
tyListTake cnt (Cons val nxt)
= Cons val (tyListTake (tyPred cnt) nxt)
instance ( TyListTake cnt' nxt nxt'
, Pred (D4 r) cnt'
) =>
TyListTake (D4 r) (Cons val nxt) (Cons val nxt') where
tyListTake cnt (Cons val nxt)
= Cons val (tyListTake (tyPred cnt) nxt)
instance ( TyListTake cnt' nxt nxt'
, Pred (D5 r) cnt'
) =>
TyListTake (D5 r) (Cons val nxt) (Cons val nxt') where
tyListTake cnt (Cons val nxt)
= Cons val (tyListTake (tyPred cnt) nxt)
instance ( TyListTake cnt' nxt nxt'
, Pred (D6 r) cnt'
) =>
TyListTake (D6 r) (Cons val nxt) (Cons val nxt') where
tyListTake cnt (Cons val nxt)
= Cons val (tyListTake (tyPred cnt) nxt)
instance ( TyListTake cnt' nxt nxt'
, Pred (D7 r) cnt'
) =>
TyListTake (D7 r) (Cons val nxt) (Cons val nxt') where
tyListTake cnt (Cons val nxt)
= Cons val (tyListTake (tyPred cnt) nxt)
instance ( TyListTake cnt' nxt nxt'
, Pred (D8 r) cnt'
) =>
TyListTake (D8 r) (Cons val nxt) (Cons val nxt') where
tyListTake cnt (Cons val nxt)
= Cons val (tyListTake (tyPred cnt) nxt)
instance ( TyListTake cnt' nxt nxt'
, Pred (D9 r) cnt'
) =>
TyListTake (D9 r) (Cons val nxt) (Cons val nxt') where
tyListTake cnt (Cons val nxt)
= Cons val (tyListTake (tyPred cnt) nxt)
class TyListElem lst val idx | lst val -> idx where
tyListElem :: (Monad m) => lst -> val -> m idx
instance (TyListElem' lst (D0 E) val idx) =>
TyListElem lst val idx where
tyListElem lst val = tyListElem' lst (D0 E) val
class TyListElem' lst acc val idx | lst acc val -> idx where
tyListElem' :: (Monad m) => lst -> acc -> val -> m idx
instance TyListElem' Nil acc val idx where
tyListElem' _ _ _ = fail "TyListElem not found in list"
instance TyListElem' (Cons val nxt) idx val idx where
tyListElem' _ idx _ = return idx
instance ( Succ acc acc'
, TyListElem' nxt acc' val idx
) =>
TyListElem' (Cons val' nxt) acc val idx where
tyListElem' (Cons _ nxt) acc val = tyListElem' nxt (tySucc acc) val
class TyListReverse m n | m -> n, n -> m where
tyListReverse :: m -> n
instance (TyListReverse' m Nil n) => TyListReverse m n where
tyListReverse lst = tyListReverse' lst nil
class TyListReverse' m a n | m a -> n where
tyListReverse' :: m -> a -> n
instance TyListReverse' Nil acc acc where
tyListReverse' _ = id
instance (TyListReverse' nxt (Cons v acc) n, TyList acc) =>
TyListReverse' (Cons v nxt) acc n where
tyListReverse' (Cons v nxt) acc = tyListReverse' nxt (cons v acc)