{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
-- By Jesse Tov (ccs.neu.edu!tov), November 2007
-- This is a DRAFT.  Later versions at http://www.ccs.neu.edu/home/tov/.
module Session (
  Cap, Chan, Spec, ChanCap,
  Snd, Rcv, (:+:), (:&:), Repeat, Follow, End, (:->:),
  Dual, Append, Evolve,
  Channel(..),
  accept, request, send, recv,
  sel1, sel2, cases, unroll, rollun,
  close,
  with_sel1, with_sel2, with_cases, with_repeat, with_follow,
) where

import Env
import Linear

bot = undefined

data M = M

data Cap t x

newtype Chan t c = Chan c
newtype Spec x c = Spec c

data ChanCap c x = forall t. CC (Chan t c) (Cap t x)

data Snd a
data Rcv a
data End

infixr 5 :+:
infixr 5 :&:
data a :+: b
data a :&: b

data Repeat x
data Follow x

infixr 6 :->:
data a :->: b

class Dual a a' | a -> a', a' -> a where
  dual :: a -> a'
  dual _ = bot

instance Dual (Rcv a) (Snd a)
instance Dual (Snd a) (Rcv a)
instance Dual End     End
instance Dual ()      ()
instance (Dual x x', Dual y y') => Dual (x :+: y)  (x' :&: y')
instance (Dual x x', Dual y y') => Dual (x :&: y)  (x' :+: y')
instance Dual x x' => Dual (Repeat x) (Follow x')
instance Dual x x' => Dual (Follow x) (Repeat x')
instance (Dual x x', Dual y y') => Dual (x :->: y) (x' :->: y')

class Append x y xy | x y -> xy where
  append :: x -> y -> xy
  append _ _ = bot
instance Append (Rcv a) y (Rcv a :->: y)
instance Append (Snd a) y (Snd a :->: y)
instance Append ()      y y
instance Append (x1:+:x2) y ((x1:+:x2) :->: y)
instance Append (x1:&:x2) y ((x1:&:x2) :->: y)
instance Append (Repeat x) y (Repeat x :->: y)
instance Append (Follow x) y (Follow x :->: y)
instance (Append y z yz) =>
         Append (x :->: y) z (x :->: yz)

class    Modify M n (ChanCap c x) e (ChanCap c x') e' => Evolve n c x e x' e'
instance Modify M n (ChanCap c x) e (ChanCap c x') e' => Evolve n c x e x' e'

class Monad m => Channel m c where
  untyped_new     :: m c
  untyped_send    :: c -> a -> m ()
  untyped_recv    :: c -> m a
  untyped_close   :: c -> m ()

  newSpec     :: m (Spec x c)

  low_accept  :: Spec x c -> m (forall t. (Chan t c, Cap t x))
  low_request :: Dual x x' =>
                 Spec x c -> m (forall t. (Chan t c, Cap t x'))
  
  low_send :: Chan t c -> Cap t (Snd a :->: x) -> a -> m (Cap t x)
  low_recv :: Chan t c -> Cap t (Rcv a :->: x) -> m (Cap t x, a)

  low_sel1 :: Append x1 y x1y =>
              Chan t c -> Cap t ((x1:+:x2) :->: y) -> m (Cap t x1y)
  low_sel2 :: Append x2 y x2y =>
              Chan t c -> Cap t ((x1:+:x2) :->: y) -> m (Cap t x2y)

  low_cases :: (Append x1 y x1y, Append x2 y x2y) =>
               Chan t c -> Cap t ((x1:&:x2) :->: y) ->
               m (Either (Cap t x1y) (Cap t x2y))

  low_unroll :: (Append x (Repeat x) xrx) =>
                Chan t c -> Cap t (Repeat x :->: y) ->
                m (Cap t ((xrx:+:()) :->: y))

  low_rollun :: (Append x (Follow x) xfx) =>
                Chan t c -> Cap t (Follow x :->: y) ->
                m (Cap t ((xfx:&:()) :->: y))

  low_unroll' :: (Append x (Repeat x :->: ()) xrx) =>
                 Chan t c -> Cap t (Repeat x :->: y) ->
                 m (Cap t ((xrx:+:()) :->: y))

  low_rollun' :: (Append x (Follow x :->: ()) xfx) =>
                 Chan t c -> Cap t (Follow x :->: y) ->
                 m (Cap t ((xfx:&:()) :->: y))

  low_close :: Chan t c -> Cap t End -> m ()

  newSpec = untyped_new >>= return . Spec

  low_accept (Spec s) = do
    ch <- untyped_new
    untyped_send s ch
    return (Chan ch, bot)

  low_request (Spec s) = do
    ch <- untyped_recv s
    return (Chan ch, bot)

  low_send (Chan ch) _ a = do
    untyped_send ch a
    return bot

  low_recv (Chan ch) _ = do
    a <- untyped_recv ch
    return (bot, a)

  low_sel1 (Chan ch) _ = do
    untyped_send ch (Left bot)
    return bot

  low_sel2 (Chan ch) _ = do
    untyped_send ch (Right bot)
    return bot

  low_cases (Chan ch) _ = do
    untyped_recv ch

  low_unroll  _ _ = return bot
  low_rollun  _ _ = return bot
  low_unroll' _ _ = return bot
  low_rollun' _ _ = return bot

  low_close (Chan ch) _ = untyped_close ch

makeChanCap :: (LineTrans l m, Extend M (ChanCap c x) e e' n) =>
              (forall t. (Chan t c, Cap t x)) -> l m e e' (LVar n)
makeChanCap pair = newLVar M (CC (fst pair) (snd pair))

accept :: (Channel m c, LineTrans l m,
           Extend M (ChanCap c x) e e' n) =>
          Spec x c -> l m e e' (LVar n)
accept spec =
  liftL (low_accept spec) >>>= makeChanCap

request :: (Channel m c, LineTrans l m,
            Dual x x',
            Extend M (ChanCap c x') e e' n) =>
           Spec x c -> l m e e' (LVar n)
request spec =
  liftL (low_request spec) >>>= makeChanCap

send :: (Channel m c, LineTrans l m,
         Evolve n c (Snd a :->: x) e x e') =>
        LVar n -> a -> l m e e' ()
send ccvar val =
  modifyLVarM_ M ccvar $ \(CC chan cap) ->
    low_send chan cap val >>= return . CC chan

recv :: (Channel m c, LineTrans l m,
         Evolve n c (Rcv a :->: x) e x e') =>
        LVar n -> l m e e' a
recv ccvar =
  modifyLVarM M ccvar $ \(CC chan cap) ->
    low_recv chan cap >>= \(cap, result) ->
    return (CC chan cap, result)

sel1 :: (Channel m c,
         LineTrans l m,
         Append x1 y x1y,
         Evolve n c ((x1:+:x2) :->: y) e x1y e') =>
        LVar n -> l m e e' ()
sel1 ccvar =
  modifyLVarM_ M ccvar $ \(CC chan cap) ->
    low_sel1 chan cap >>= return . CC chan

sel2 :: (Channel m c,
         LineTrans l m,
         Append x2 y x2y,
         Evolve n c ((x1:+:x2) :->: y) e x2y e') =>
        LVar n -> l m e e' ()
sel2 ccvar =
  modifyLVarM_ M ccvar $ \(CC chan cap) ->
    low_sel2 chan cap >>= return . CC chan

cases :: (Channel m c,
          LineTrans l m,
          Append x1 y x1y, Append x2 y x2y,
          Lookup M n e (ChanCap c ((x1:&:x2) :->: y)),
          Replace M n (ChanCap c x1y) e e1,
          Replace M n (ChanCap c x2y) e e2) =>
         LVar n -> l m e (Either e1 e2) ()
cases ccvar =
  readLVar M ccvar           >>>= \(CC chan cap) ->
  liftL (low_cases chan cap) >>>= \choice ->
  case choice of
    Left cap1  -> leftL  (writeLVar M ccvar (CC chan cap1))
    Right cap2 -> rightL (writeLVar M ccvar (CC chan cap2))

unroll :: (Channel m c, LineTrans l m,
           Append x (Repeat x) xrx,
           Evolve n c (Repeat x :->: y) e ((xrx:+:()) :->: y) e') =>
          LVar n -> l m e e' ()
unroll ccvar =
  modifyLVarM_ M ccvar $ \(CC chan cap) ->
    low_unroll chan cap >>= return . CC chan

rollun :: (Channel m c, LineTrans l m,
           Append x (Follow x) xfx,
           Evolve n c (Follow x :->: y) e ((xfx:&:()) :->: y) e') =>
          LVar n -> l m e e' ()
rollun ccvar =
  modifyLVarM_ M ccvar $ \(CC chan cap) ->
    low_rollun chan cap >>= return . CC chan

unroll' :: (Channel m c, LineTrans l m,
            Append x (Repeat x :->: ()) xrx,
            Evolve n c (Repeat x :->: y) e ((xrx:+:()) :->: y) e') =>
           LVar n -> l m e e' ()
unroll' ccvar =
  modifyLVarM_ M ccvar $ \(CC chan cap) ->
    low_unroll' chan cap >>= return . CC chan

rollun' :: (Channel m c, LineTrans l m,
            Append x (Follow x :->: ()) xfx,
            Evolve n c (Follow x :->: y) e ((xfx:&:()) :->: y) e') =>
           LVar n -> l m e e' ()
rollun' ccvar =
  modifyLVarM_ M ccvar $ \(CC chan cap) ->
    low_rollun' chan cap >>= return . CC chan

close :: (Channel m c, LineTrans l m,
          Use M n e e' (ChanCap c End)) =>
         LVar n -> l m e e' ()
close ccvar =
  takeLVar M ccvar >>>= \(CC chan cap) ->
  liftL (low_close chan cap)

parenthesize ::
    (Channel m c, LineTrans l m,
     Evolve n c (x:->:y) e   (x:->:()) e1,
     Evolve n c ()       e1' y         e') =>
    LVar n -> l m e1 e1' a -> l m e e' a
parenthesize ccvar f =
  let get1 :: Cap t (x:->:y) -> Cap t (x:->:())
      get2 :: Cap t (x:->:y) -> Cap t y
      get1 _ = bot
      get2 _ = bot in
  readLVar M ccvar >>>= \(CC chan cap) ->
  writeLVar M ccvar (CC chan (get1 cap)) >>>
  f >>>= \res ->
  writeLVar M ccvar (CC chan (get2 cap)) >>>
  unitL res

with_sel1 :: (Channel m c, LineTrans l m,
              Evolve n c (x :->: y) e (x :->: ()) e0,
              Append x1 () x1,
              Evolve n c ((x1:+:x2) :->: ()) e0 x1 e1,
              Evolve n c () e1' y e') =>
             LVar n -> l m e1 e1' a -> l m e e' a
with_sel1 ccvar f = parenthesize ccvar (sel1 ccvar >>> f)

with_sel2 :: (Channel m c, LineTrans l m,
              Evolve n c (x :->: y) e (x :->: ()) e0,
              Append x2 () x2,
              Evolve n c ((x1:+:x2) :->: ()) e0 x2 e2,
              Evolve n c () e2' y e') =>
             LVar n -> l m e2 e2' a -> l m e e' a
with_sel2 ccvar f = parenthesize ccvar (sel2 ccvar >>> f)

with_cases :: (Channel m c, LineTrans l m,
               Evolve n c (x :->: y) e (x :->: ()) e0,
               Append x1 () x1,
               Append x2 () x2,
               Evolve n c ((x1:&:x2) :->: ()) e0 x1 e11,
               Evolve n c ((x1:&:x2) :->: ()) e0 x2 e12,
               Evolve n c () e2 y e') =>
              LVar n -> l m e11 e2 a -> l m e12 e2 a -> l m e e' a
with_cases ccvar f g =
  parenthesize ccvar (cases ccvar >>> eitherL f g)

with_repeat ::
    (Channel m c, LineTrans l m,
     Append x (Repeat x :->: ()) xrx,
     Evolve n c (Repeat x :->: y) e'' ((xrx:+:()) :->: y) e''',
     Evolve n c ((xrx:+:()) :->: y) e''' ((xrx:+:()) :->: ()) e0,
     Append xrx () xrx,
     Evolve n c ((xrx:+:()) :->: ()) e0 xrx e1,
     Evolve n c () e1' y e,
     Evolve n c ((xrx:+:()) :->: ()) e0 () e2,
     Evolve n c () e2 y e') =>
    LVar n -> a -> (a -> l m e e'' (Either (l m e1 e1' a) b)) -> l m e e' b
with_repeat ccvar state0 body =
  loop state0 where
    loop acc =
      body acc >>>= \choice ->
      unroll' ccvar >>>
      case choice of
        Left next -> with_sel1 ccvar next >>>= loop
        Right res -> with_sel2 ccvar (unitL res)

with_follow ::
    (Channel m c, LineTrans l m,
     Evolve n c (Follow x :->: y) e (Follow x :->: ()) e0,
     Append x (Follow x :->: ()) xfx,
     Evolve n c (Follow x :->: ()) e0 ((xfx:&:()) :->: ()) e0',
     Evolve n c ((xfx:&:()) :->: ()) e0' ((xfx:&:()) :->: ()) e0',
     Append xfx () xfx,
     Evolve n c ((xfx:&:()) :->: ()) e0' xfx e1,
     Evolve n c ((xfx:&:()) :->: ()) e0' ()  e2,
     Evolve n c () e2 () e2,
     Evolve n c () e2 y e') =>
    LVar n -> a -> (a -> l m e1 e0 a) -> l m e e' a
with_follow ccvar state0 body =
  parenthesize ccvar (loop state0) where
    loop acc =
      rollun' ccvar >>>
      with_cases ccvar
        (body acc >>>= loop)
        (unitL acc)

with_follow' ::
    (Channel m c, LineTrans l m,
     Evolve n c (Follow x :->: y) e
                (Follow x :->: ()) e0,
     Append x (Follow x :->: ()) xfx,
     Evolve n c (Follow x :->: ()) e0 ((xfx:&:()) :->: ()) e0',
     Append xfx () xfx,
     Evolve n c ((xfx:&:()) :->: ()) e0' xfx e1,
     Evolve n c ((xfx:&:()) :->: ()) e0' ()  e2,
     Evolve n c () e2 y e') =>
    LVar n -> a ->
    (a -> l m e1 e0 a) ->
    l m e e' a
with_follow' ccvar state0 body =
  parenthesize ccvar (loop state0) where
    loop acc =
      rollun' ccvar >>>
      cases ccvar >>>
      eitherL
        (body acc >>>= loop)
        (unitL acc)