{-
    List.hs
        Copyright 2008 Matthew Sackman <matthew@wellquite.org>

    This file is part of Session Types for Haskell.

    Session Types for Haskell is free software: you can redistribute it
    and/or modify it under the terms of the GNU General Public License
    as published by the Free Software Foundation, either version 3 of
    the License, or (at your option) any later version.

    Session Types for Haskell is distributed in the hope that it will
    be useful, but WITHOUT ANY WARRANTY; without even the implied
    warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
    See the GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with Session Types for Haskell.
    If not, see <http://www.gnu.org/licenses/>.
-}

{-# LANGUAGE KindSignatures, GADTs, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, OverlappingInstances #-}

-- | Heterogeneous lists. This has been done many times, in many
-- different ways. Explicit constructors are hidden deliberately.

module Control.Concurrent.Session.List where

import Control.Concurrent.Session.Number

data Nil :: * where
            Nil :: Nil
data Cons :: * -> * -> * where
             Cons :: t -> n -> Cons t n

-- | Find the length of a list.
class ListLength list length | list -> length where
    listLength :: list -> length
instance ListLength Nil (D0 E) where
    listLength Nil = (D0 E)
instance (ListLength n len, Succ len len') => ListLength (Cons t n) len' where
    listLength (Cons _ nxt) = tySucc . listLength $ nxt

instance Show Nil where
    show Nil = "Nil"

instance (ListLength 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

class TyList l
instance TyList Nil
instance (TyList nxt) => TyList (Cons val nxt)

-- | Index or update a list
class Elem lst idx res | lst idx -> res where
    tyListElem :: lst -> idx -> res
    tyListUpdate :: lst -> idx -> res -> lst

instance Elem (Cons res nxt) (D0 E) res where
    tyListElem (Cons val _) _ = val
    tyListUpdate (Cons _ nxt) _ val = (Cons val nxt)

instance ( Elem nxt idx' res
         , Pred idx idx'
         , SmallerThan idx' len
         , ListLength nxt len) =>
    Elem (Cons val nxt) idx res where
        tyListElem (Cons _ nxt) idx = tyListElem nxt (tyPred idx)
        tyListUpdate (Cons val nxt) idx val'
            = Cons val (tyListUpdate nxt (tyPred idx) val')