--
--  Control.Concurrent.Session :: Session Types for Haskell
--  Copyright (C) 2007  Matthew Sackman (matthew@wellquite.org)
--
--  This library is free software; you can redistribute it and/or
--  modify it under the terms of the GNU Lesser General Public
--  License as published by the Free Software Foundation; either
--  version 2.1 of the License, or (at your option) any later version.
--
--  This library 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
--  Lesser General Public License for more details.
--
--  You should have received a copy of the GNU Lesser General Public
--  License along with this library; if not, write to the Free Software
--  Foundation, Inc., 59 Temple Place, Suite 330, Boston,
--  MA  02111-1307  USA
--
{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}

module Control.Concurrent.Session.List
    where

data List :: * -> * -> * where
                List :: t -> l -> List t l
instance (Show l) => Show (List t l) where
    show (List _ l) = "List : " ++ (show l)

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

instance Show Nil where
    show Nil = "Nil"
instance (Show n, Show t) => Show (Cons t n) where
    show lst = "Cons " ++ (show val) ++ " (" ++ (show nxt) ++ ")"
        where
          (val, nxt) = decomposeCons lst

class ListLength list length | list -> length where
    listLength :: list -> length
instance ListLength Nil Zero where
    listLength Nil = Zero
instance (ListLength n len) => ListLength (Cons t n) (Succ len) where
    listLength lst = Succ (listLength (snd (decomposeCons lst)))

data Zero = Zero
data Succ n = Succ n

class TyNum a
instance TyNum Zero
instance (TyNum n) => TyNum (Succ n)

nil :: Nil
nil = Nil

cons :: (ListLength n l) => t -> n -> (Cons t n)
cons t n = Cons t n

decomposeCons :: (Cons val nxt) -> (val, nxt)
decomposeCons (Cons val nxt) = (val, nxt)

class Add m n s | m n -> s where
    addTy :: m -> n -> s
instance Add Zero Zero Zero where
    addTy Zero Zero = Zero
instance (TyNum m) => Add (Succ m) Zero (Succ m) where
    addTy (Succ p) Zero = (Succ p)
instance (TyNum n) => Add Zero (Succ n) (Succ n) where
    addTy Zero (Succ p) = (Succ p)
instance (TyNum m, TyNum n, TyNum s, Add m n s) => Add (Succ m) (Succ n) (Succ (Succ s)) where
    addTy (Succ m) (Succ n) = Succ . Succ $ addTy m n

class Append lstA lstB lstC | lstA lstB -> lstC where
    append :: lstA -> lstB -> lstC
instance Append Nil lstB lstB where
    append _ b = b
instance (ListLength lstB length, Add (Succ len) length (Succ len'),
          Append next lstB next', ListLength next len, ListLength next' len') =>
    Append (Cons val next) lstB (Cons val next') where
        append lst b = cons val (append nxt b)
            where
              (val, nxt) = decomposeCons lst

class (TyNum a, TyNum b) => UpperBoundedBy a b
instance (TyNum b) => UpperBoundedBy Zero b
instance (UpperBoundedBy a b) => UpperBoundedBy (Succ a) (Succ b)

class (ListLength list length, UpperBoundedBy idx length) =>
    ListIndexed list length idx result | list idx -> result, list -> length where
        listAt :: list -> idx -> result
        listReplaceAt :: list -> idx -> result -> list

instance (TyNum len, ListLength tail len) => ListIndexed (Cons valTy tail) (Succ len) Zero valTy where
    listAt lst Zero = let (val, nxt) = decomposeCons lst in val
    listReplaceAt lst Zero val = let (valOld, nxt) = decomposeCons lst in cons val nxt
          
instance (ListLength tail len, ListIndexed tail len idx valTy) =>
    ListIndexed (Cons valTy' tail) (Succ len) (Succ idx) valTy where
        listAt lst (Succ idx) = let (val, nxt) = decomposeCons lst in listAt nxt idx
        listReplaceAt lst (Succ idx) valNew = let (val, nxt) = decomposeCons lst
                                                  nxtNew = listReplaceAt nxt idx valNew
                                              in cons val nxtNew

class TyList a
instance TyList Nil
instance (TyList tail, ListLength tail l) => TyList (Cons v tail)