--
--  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.Choice
    where

import Control.Concurrent.Session.ExtraClasses
import Control.Concurrent.Session.BaseClasses
import Control.Concurrent.Session.BaseTypes
import Control.Concurrent.Session.List
import Control.Concurrent.Session.State
import Control.Concurrent.Session.Runtime
import Control.Concurrent.MVar
import GHC.Exts

class (TyNum numIdx) => TypeAsIndex tyIdx numIdx generalType | tyIdx -> numIdx, tyIdx -> generalType where
    tyIdxToNum :: tyIdx -> numIdx

instance TypeIndexList (Nil Zero)
instance (TypeIndexList tail, TypeAsIndex tyIdx num generalType, ListLength tail len, TyList tail) =>
    TypeIndexList (Cons tyIdx (Succ len) tail)

listAtTyIdx :: (Choice generalType typeIndexes len, ListLength list len, ListIndexed list len num result, TypeAsIndex tyIdx num generalType) =>
               (List generalType list) -> tyIdx -> result
listAtTyIdx (List generalType list) tyIdx = listAt list (tyIdxToNum tyIdx)

listToChoice :: (Choice generalType typeIndexes len, ListLength list len, TyList list) =>
                list -> List generalType list
listToChoice = List (undefined :: generalType)

class SessionSpecVals list
instance SessionSpecVals (Nil Zero)
instance (SessionSpecVals tail, ListLength tail len) =>
    SessionSpecVals (Cons (SessionSpec s) (Succ len) tail)

instance (Choice generalType typeIndexes len, ListLength list len, SessionSpecVals list) =>
    SpecList generalType list

class ProcVals list
instance ProcVals (Nil Zero)
instance (ProcVals tail, ListLength tail len) =>
    ProcVals (Cons (Proc r (SessionSpec s) (SessionSpec s') o o' i i') (Succ len) tail)

instance (Choice generalType typeIndexes len, ListLength list len, ProcVals list) =>
    ProcList generalType list

updateMap :: (TypeAsIndex tyIdx num generalType,
              Choice generalType typeIndexes len,
              ListIndexed typeIndexes len num tyIdx, -- ensure that the tyIdx is actually in the Choice typeIndexes
              ListIndexed list len num value) =>
             tyIdx -> value -> List generalType list -> List generalType list
updateMap tyIdx value (List gt list) = let list' = listReplaceAt list (tyIdxToNum tyIdx) value in List gt list'

infixr 5 ~||~

class SetUpdate generalType list tyIdx value where
    (~||~) :: (tyIdx, value) -> (List generalType list) -> List generalType list

instance (TypeAsIndex tyIdx num generalType,
          Choice generalType typeIndexes len,
          ListIndexed typeIndexes len num tyIdx,
          ListIndexed list len num (SessionSpec s)) =>
    SetUpdate generalType list tyIdx (SessionSpec s) where
        (tyIdx, spec) ~||~ (List gt list) = updateMap tyIdx spec (List gt list)

instance (TypeAsIndex tyIdx num generalType,
          Choice generalType typeIndexes len,
          ListIndexed typeIndexes len num tyIdx,
          ListIndexed list len num (Proc () (SessionSpec s) (SessionSpec s') o o' i i')
         ) =>
    SetUpdate generalType list tyIdx
                  (Proc () (SessionSpec s) (SessionSpec s') o o' i i') where
        (tyIdx, (Proc p)) ~||~ (List gt list) = updateMap tyIdx (Proc p) (List gt list)

class (ListLength list len, SpecList generalType list) => EmptySpecList generalType list len | generalType -> list, list -> len where
    specList :: List generalType list

class (ListLength list len) => EmptyProcList generalType list len | generalType -> list, list -> len where
    procList :: List generalType list

class BuildReductionListLists lstLoop a b | lstLoop a -> b where
    findReductionList :: lstLoop -> a -> b

instance BuildReductionListLists lstLoop (Nil Zero) (Nil Zero) where
    findReductionList _ Nil = nil
instance (BuildReductionList lstLoop (SessionSpec a) lst,
          BuildReductionListLists lstLoop nxt nxt',
          Append lst nxt' result) =>
    BuildReductionListLists lstLoop (Cons (SessionSpec a) (Succ len) nxt) result where
        findReductionList lastSeenLoop lst = append valReductions nxtReductions
            where
              (val, nxt) = decomposeCons lst
              valReductions = findReduction lastSeenLoop val
              nxtReductions = findReductionList lastSeenLoop nxt

-- offer
instance (BuildReductionListLists lstLoop lst lst') =>
    BuildReductionList lstLoop (SessionSpec (OfferT (List t lst))) lst' where
        findReduction lastSeenLoop (OfferS (List ty list)) = findReductionList lastSeenLoop list

-- select
instance (BuildReductionListLists lstLoop lst lst') =>
    BuildReductionList lstLoop (SessionSpec (SelectT (List t lst))) lst' where
        findReduction lastSeenLoop (SelectS (List ty list)) = findReductionList lastSeenLoop list

instance (JustSendsRecvs (List t specsForOffer) (List t listSends) (List t listRecvs),
          DualT (SessionSpec (OfferT (List t specsForOffer)))
                    (SessionSpec (SelectT (List t specsForSelect))),
          ChoiceSpecsProcs specsForOffer procs
         ) =>
    JustSendsRecvs (SessionSpec (OfferT (List t specsForOffer)))
    (SessionSpec (SessChoiceT (List (t,specsForOffer,specsForSelect,procs) listSends)))
    (SessionSpec (SessChoiceT (List (t,specsForSelect,specsForOffer,procs) listRecvs)))

instance (JustSendsRecvs (List t specsForSelect) (List t listSends) (List t listRecvs),
          DualT (SessionSpec (OfferT (List t specsForOffer)))
                    (SessionSpec (SelectT (List t specsForSelect))),
          ChoiceSpecsProcs specsForOffer procs
         ) =>
    JustSendsRecvs (SessionSpec (SelectT (List t specsForSelect)))
    (SessionSpec (SessChoiceT (List (t,specsForSelect,specsForOffer,procs) listSends)))
    (SessionSpec (SessChoiceT (List (t,specsForOffer,specsForSelect,procs) listRecvs)))

instance (JustSendsRecvs list sends recvs) =>
    JustSendsRecvs (List t list) (List t sends) (List t recvs)
instance JustSendsRecvs (Nil Zero) (Nil Zero) (Nil Zero)
instance (JustSendsRecvs ns nsSends nsRecvs,
          JustSendsRecvs (SessionSpec spec) (SessionSpec specSends) (SessionSpec specRecvs)) =>
    JustSendsRecvs (Cons (SessionSpec spec) (Succ n) ns) (Cons (SessionSpec specSends) (Succ n) nsSends) (Cons (SessionSpec specRecvs) (Succ n) nsRecvs)

instance ChoiceSpecsProcs (Nil Zero) (Nil Zero)
instance (ChoiceSpecsProcs specs procs) =>
    ChoiceSpecsProcs
    (Cons (SessionSpec s) (Succ len) specs)
    (Cons (Proc () (SessionSpec s) (SessionSpec s') o o' i i') (Succ len) procs)

instance (ChoiceSpecsProcs specsForOffer procs,
          Choice generalType typeIndexes len,
          ListLength specsForOffer len, ListLength procs len
         ) =>
    ValidOffer generalType procs specsForOffer

instance (DualT (SessionSpec s) (SessionSpec sD),
          DualT (SessionSpec s') (SessionSpec sD')) =>
    DualT (Proc () (SessionSpec s) (SessionSpec s') o o' i i')
    (Proc () (SessionSpec sD) (SessionSpec sD') i i' o o') where
        dual = undefined

instance (DualT
            (Proc () (SessionSpec s) (SessionSpec s') o o' i i')
            (Proc () (SessionSpec sD) (SessionSpec sD') i i' o o'),
          DualT (SessionSpec s) (SessionSpec sD),
          DualT (SessionSpec s') (SessionSpec sD'),
          TypeAsIndex selection num generalType,
          ListLength specsForSelect len,
          Choice generalType typeIndexes len,
          ChoiceSpecsProcs specsForOffer procs,
          ListIndexed typeIndexes len num selection, -- ensure that the selection is actually in the Choice typeIndexes
          DualT specsForOffer specsForSelect,
          SpecList generalType specsForSelect,
          ListIndexed specsForSelect len num (SessionSpec s),
          ListIndexed procs len num (Proc () (SessionSpec sD) (SessionSpec sD') i i' o o')) =>
    ValidSelect generalType specsForSelect procs selection
                (Proc () (SessionSpec s) (SessionSpec s') o o' i i')
                (Proc () (SessionSpec sD) (SessionSpec sD') i i' o o')

findOfferProc :: (ValidOffer generalType procs specsForOffer,
         ValidSelect generalType specsForSelect procs selection
          (Proc () (SessionSpec s) (SessionSpec s') o o' i i')
          (Proc () (SessionSpec sD) (SessionSpec sD') i i' o o'),
         JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
         JustSendsRecvs (SessionSpec sD) (SessionSpec i) (SessionSpec o),
         Choice generalType typeIndexes len,
         ChoiceSpecsProcs specsForOffer procs,
         DualT specsForOffer specsForSelect,
         ListLength specsForSelect len, ListLength specsForOffer len, ListLength procs len,
         ListIndexed typeIndexes len num selection, -- ensure that the selection is actually in the Choice typeIndexes
         ListIndexed procs len num (Proc () (SessionSpec sD) (SessionSpec sD') i i' o o'),
         TypeAsIndex selection num generalType
        ) =>
        generalType -> specsForSelect -> specsForOffer -> procs -> selection ->
          (Proc () (SessionSpec s) (SessionSpec s') o o' i i') ->
          (Proc () (SessionSpec sD) (SessionSpec sD') i i' o o')
findOfferProc generalType specsForSelect specsForOffer procs selection procSel
    = listAt procs num
    where
      num = tyIdxToNum selection

select :: forall generalType specsForSelect specsForOffer s sD o i o' i' s' sD' selection
                 num len typeIndexes specsO specsI procs .
          (ValidOffer generalType procs specsForOffer,
           ValidSelect generalType specsForSelect procs selection
             (Proc () (SessionSpec s) (SessionSpec s') o o' i i')
             (Proc () (SessionSpec sD) (SessionSpec sD') i i' o o'),
           JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
           JustSendsRecvs (SessionSpec sD) (SessionSpec i) (SessionSpec o),
           JustSendsRecvs (SessionSpec s') (SessionSpec o') (SessionSpec i'),
           JustSendsRecvs (SessionSpec sD') (SessionSpec i') (SessionSpec o'),
           ZeroOrMoreSteps (SessionSpec s) (SessionSpec s'),
           ZeroOrMoreSteps (SessionSpec sD) (SessionSpec sD'),
           DualT (SessionSpec s) (SessionSpec sD),
           DualT specsForOffer specsForSelect,
           DualT (SessionSpec s') (SessionSpec sD'),
           TypeAsIndex selection num generalType,
           ListIndexed typeIndexes len num selection, -- ensure that the selection is actually in the Choice typeIndexes
           ListLength specsForOffer len,
           ListLength specsForSelect len,
           ListLength procs len,
           Choice generalType typeIndexes len,
           SpecList generalType specsForSelect,
           SpecList generalType specsForOffer,
           ListIndexed specsForSelect len num (SessionSpec s),
           ListIndexed procs len num (Proc () (SessionSpec sD) (SessionSpec sD') i i' o o'),
           ChoiceSpecsProcs specsForOffer procs,
           JustSendsRecvs (SessionSpec (SelectT (List generalType specsForSelect)))
           (SessionSpec (SessChoiceT (List (generalType, specsForSelect, specsForOffer, procs) specsO)))
           (SessionSpec (SessChoiceT (List (generalType, specsForOffer, specsForSelect, procs) specsI)))
          ) =>
    selection ->
    (Proc () (SessionSpec s) (SessionSpec s') o o' i i') ->
    (SessionState (SessionSpec (SelectT (List generalType specsForSelect)))
     (SessChoiceT (List (generalType, specsForSelect, specsForOffer, procs) specsO))
     (SessChoiceT (List (generalType, specsForOffer, specsForSelect, procs) specsI))) ->
    IO ((), (SessionState (SessionSpec s') o' i'))
select selection proc (SessionState outgoing incoming)
    = do { takeMVar outgoing
         ; cell <- takeMVar incoming
         ; case cell of
             (OffersCell (list :: List generalType procs) procMVar) ->
                 case list of
                   (List (gt :: generalType) (procs :: procs)) ->
                       do { let (offerProc :: Proc () (SessionSpec sD) (SessionSpec sD') i i' o o')
                                    = findOfferProc (undefined :: generalType)
                                                    (undefined :: specsForSelect)
                                                    (undefined :: specsForOffer)
                                                    procs
                                                    selection
                                                    proc
                          ; ((stateSelect, stateOffer) ::
                                 ((SessionState (SessionSpec s) o i),
                                  (SessionState (SessionSpec sD) i o)))
                              <- mkState (undefined :: SessionSpec s)
                          ; let wrapped = wrapProc offerProc stateOffer
                          ; putMVar procMVar wrapped
                          ; case proc of
                              (Proc p) -> p stateSelect
                          }
         }

offer :: forall specsForOffer specsForSelect procs len generalType typeIndexes specsO specsI .
    (ChoiceSpecsProcs specsForOffer procs,
     ListLength procs len,
     ListLength specsForOffer len,
     ListLength specsForSelect len,
     Choice generalType typeIndexes len,
     DualT specsForOffer specsForSelect,
     SpecList generalType specsForOffer,
     SpecList generalType specsForSelect,
     ProcList generalType procs,
     JustSendsRecvs (SessionSpec (OfferT (List generalType specsForOffer)))
     (SessionSpec (SessChoiceT (List (generalType, specsForOffer, specsForSelect, procs) specsO)))
     (SessionSpec (SessChoiceT (List (generalType, specsForSelect, specsForOffer, procs) specsI)))
    ) =>
    (List generalType procs) ->
    (SessionState (SessionSpec (OfferT (List generalType specsForOffer)))
     (SessChoiceT (List (generalType, specsForOffer, specsForSelect, procs) specsO))
     (SessChoiceT (List (generalType, specsForSelect, specsForOffer, procs) specsI))) ->
    IO ((), (SessionState (SessionSpec EndT) EndT EndT))
offer implementations (SessionState outgoing incoming)
    = do { (procMVar :: MVar ProcWrapper) <- newEmptyMVar
         ; putMVar incoming undefined
         ; putMVar outgoing (OffersCell implementations procMVar)
         ; procCell <- takeMVar procMVar
         ; case procCell of
             (PW (cell :: ProcCell () (SessionSpec s) (SessionSpec s') o o' i i')) ->
                 do { (result, stateTrappedPrivate) <- runProc cell
                    ; return (result, undefined)
                    }
         }

runProc :: (ProcCell r (SessionSpec s) (SessionSpec s') o o' i i') ->
           IO (r, (SessionState (SessionSpec s') o' i'))
runProc (ProcCell (Proc p) s) = p s

wrapProc :: (JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
             ZeroOrMoreSteps (SessionSpec s) (SessionSpec s'),
             JustSendsRecvs (SessionSpec s') (SessionSpec o') (SessionSpec i')) =>
            (Proc () (SessionSpec s) (SessionSpec s') o o' i i') ->
            (SessionState (SessionSpec s) o i) ->
            ProcWrapper
wrapProc p s = PW (ProcCell p s)