--
--  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 ChoiceTests where

import Control.Concurrent.Session

-- A calc example --
data CalcOp = Add
            | Subtract
            | Negate
            | Quit
              deriving (Show, Eq, Ord, Enum, Bounded)

data CalcOpAdd = CalcOpAdd
data CalcOpSubtract = CalcOpSubtract
data CalcOpNegate = CalcOpNegate
data CalcOpQuit = CalcOpQuit

instance TypeAsIndex CalcOpQuit (Succ (Succ (Succ Zero))) CalcOp where
    tyIdxToNum = const (Succ (Succ (Succ Zero)))
instance TypeAsIndex CalcOpSubtract (Succ (Succ Zero)) CalcOp where
    tyIdxToNum = const (Succ (Succ Zero))
instance TypeAsIndex CalcOpNegate (Succ Zero) CalcOp where
    tyIdxToNum = const (Succ Zero)
instance TypeAsIndex CalcOpAdd Zero CalcOp where
    tyIdxToNum = const Zero

instance Choice CalcOp (Cons CalcOpAdd
                        (Cons CalcOpNegate
                         (Cons CalcOpSubtract
                          (Cons CalcOpQuit
                           Nil))))
    (Succ (Succ (Succ (Succ Zero)))) where
        typeIndexes = List (undefined :: CalcOp)
                              (cons CalcOpAdd $
                               cons CalcOpNegate $
                               cons CalcOpSubtract $
                               cons CalcOpQuit nil)

instance EmptySpecList CalcOp (Cons (SessionSpec a)
                               (Cons (SessionSpec b)
                                (Cons (SessionSpec c)
                                 (Cons (SessionSpec d)
                                  Nil))))
    (Succ (Succ (Succ (Succ Zero)))) where
        specList = List (undefined :: CalcOp)
                   (cons undefined
                    (cons undefined
                     (cons undefined
                      (cons undefined
                       nil))))

type P r s o i s' o' i' = Proc r (SessionSpec s) (SessionSpec s') o o' i i'

instance
    EmptyProcList CalcOp (Cons (P r s1 o1 i1 s1' o1' i1')
                          (Cons (P r s2 o2 i2 s2' o2' i2')
                           (Cons (P r s3 o3 i3 s3' o3' i3')
                            (Cons (P r s4 o4 i4 s4' o4' i4')
                             Nil))))
    (Succ (Succ (Succ (Succ Zero)))) where
        procList = List (undefined :: CalcOp)
                   (cons undefined
                    (cons undefined
                     (cons undefined
                      (cons undefined
                       nil))))