{-# 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 Linear (
  LVar,
  Line(..),
  (>>>), pureL_,
  newLVar, deleteLVar, readLVar, writeLVar,
  takeLVar, modifyLVar, modifyLVar_,
  newLList, addLList, caseLList, elimLList,
  LVars, lvars,
  LineTrans(..),
  arrL_, io, forkIOinL, 
  modifyLVarM, modifyLVarM_,
  Linear, runLinear,
  LinearT, runLinearT,
) where

import Control.Concurrent (ThreadId, forkIO)
import Control.Monad.Trans
import Data.IORef

import Control.Monad.Fix

import Env as Env

-- Linear Variables:

newtype LVar n = LVar (Key n)

instance Show n => Show (Key n) where
  showsPrec d _
    = showParen (d > 10)
        (("LVar " ++) . shows (undefined::n))

-- The Line computation class:

class Line l where
  pureL    :: (forall t. Env t e -> (Env t e', a)) ->
              l e e' a
  leftL    :: l e e1 a -> l e (Either e1 e2) a
  rightL   :: l e e2 a -> l e (Either e1 e2) a
  eitherL  :: l e1 e a -> l e2 e a -> l (Either e1 e2) e a
  unitL    :: a -> l e e a
  (>>>=)   :: l e e' a -> (a -> l e' e'' b) -> l e e'' b

(>>>) :: Line l => l e e' a -> l e' e'' b -> l e e'' b
f >>> g = f >>>= const g

infixl 1 >>>=, >>>

pureL_     :: Line l => (forall t. Env t e -> Env t e') -> l e e' ()
pureL_ f    = pureL (\e -> (f e, ()))

newLVar     :: (Line l, Extend m v e e' n) => m -> v -> l e e' (LVar n)
deleteLVar  :: (Line l, Remove m n e e') => m -> LVar n -> l e e' ()
readLVar    :: (Line l, Lookup m n e v) => m -> LVar n -> l e e v
writeLVar   :: (Line l, Replace m n v e e') => m -> LVar n -> v ->
               l e e' ()
takeLVar    :: (Line l, Use m n e e' v) => m -> LVar n -> l e e' v
modifyLVar  :: (Line l, Modify m n v e v' e') => m -> LVar n ->
               (v -> (v', a)) -> l e e' a
modifyLVar_ :: (Line l, Modify m n v e v' e') => m -> LVar n ->
               (v -> v') -> l e e' ()

newLVar m v = pureL (\e -> let (e', n) = extend m v e in (e', LVar n))
deleteLVar  m (LVar n)   = pureL_ (remove m n)
readLVar    m (LVar n)   = pureL (\e -> (e, Env.lookup m n e))
writeLVar   m (LVar n) v = pureL_ (replace m n v)
takeLVar    m (LVar n)   = pureL (use m n)
modifyLVar  m (LVar n) f = pureL (modify m n f)
modifyLVar_ m (LVar n) f = pureL_ (modify_ m n f)

-- List operations
newLList  :: (Line l, Extend2 ListMark List e e' n) =>
             l e e' (LVar n)
newLList = pureL (\e -> let (e', n) = introList e in (e', LVar n))

caseLList :: (Line l, CdrList nl e m a na ea) =>
             LVar nl -> (LVar na -> l ea e' r) -> l e e' r -> l e e' r
caseLList (LVar k) f g = pureL (\e ->
  case cdrList k e of
    Left (e', k) -> (leftEnv e', k)
    Right e'     -> (rightEnv e', undefined)) >>>= \k ->
  eitherL (f (LVar k)) g

elimLList :: (Line l, ElimList nl e m a na ea e0) =>
             LVar nl -> (LVar na -> l ea e' r) -> l e0 e' r -> l e e' r
elimLList (LVar k) f g = pureL (\e ->
  case elimList k e of
    Left (e', k) -> (leftEnv e', k)
    Right e'     -> (rightEnv e', undefined)) >>>= \k ->
  eitherL (f (LVar k)) g

addLList :: (Line l, ConsList na nl e m a e') =>
            LVar na -> LVar nl -> l e e' ()
addLList (LVar na) (LVar nl) = pureL_ (consList na nl)

-- LVar lists
newtype LVars a = LVars a

class MakeLVars acc res | res -> acc where
  lvars' :: acc -> res

instance MakeLVars (LVars acc) (LVars acc) where
  lvars' = id

instance MakeLVars (LVars (Key n, acc)) res =>
         MakeLVars (LVars acc) (LVar n -> res) where
  lvars' (LVars acc) (LVar key) = lvars' (LVars (key, acc))

lvars :: MakeLVars (LVars ()) b => b
lvars  = lvars' (LVars ())

-- The LineTrans class

class (Monad m, Line (l m)) => LineTrans l m where
  arrL       :: (forall t. Env t e -> m (Env t e', a)) -> l m e e' a
  liftL      :: m a -> l m e e a
  unsafeRunL :: Partition ks e e1 e2 =>
                LVars ks -> l m e1 Empty a -> l m e e2 (m a)

arrL_  :: LineTrans l m =>
          (forall t. Env t e -> m (Env t e')) ->
          l m e e' ()
arrL_ f = arrL (\e -> f e >>= \e' -> return (e', ()))

io :: (LineTrans l m, MonadIO m) => IO a -> l m e e a
io  = liftL . liftIO

forkIOinL :: (LineTrans l IO, Partition ks e e1 e2) =>
             LVars ks -> l IO e1 Empty () -> l IO e e2 ThreadId
forkIOinL ks thunk =
  unsafeRunL ks thunk >>>= \action ->
  io (forkIO action)

modifyLVarM :: (LineTrans l m0, Modify m n v e v' e') =>
               m -> LVar n -> (v -> m0 (v', a)) -> l m0 e e' a
modifyLVarM_ :: (LineTrans l m0, Modify m n v e v' e') =>
                m -> LVar n -> (v -> m0 v') -> l m0 e e' ()

modifyLVarM m (LVar n) f  = arrL (modifyM m n f)
modifyLVarM_ m (LVar n) f = arrL_ (modifyM_ m n f)

-- Implementations:

-- Functional:
newtype Linear e e' a = Linear {
  unLinear :: e -> (e', a)
}

instance Line Linear where
  pureL f = Linear (outEnv f)
  eitherL (Linear f) (Linear g) = Linear $ outEnv $ \e ->
    case eitherEnv e of
      Left e ->  inEnv f e
      Right e -> inEnv g e
  leftL (Linear f) = Linear $ outEnv $ \e ->
    let (e', a) = inEnv f e in (leftEnv e', a)
  rightL (Linear f) = Linear $ outEnv $ \e ->
    let (e', a) = inEnv f e in (rightEnv e', a)
  unitL a = Linear (\e -> (e, a))
  Linear f >>>= g = Linear (\e -> let (e', a) = f e in unLinear (g a) e')

instance Monad (Linear e e) where
  (>>=)  = (>>>=)
  return = unitL

runLinear :: Linear Empty Empty a -> a
runLinear (Linear f) = snd (f Empty)
                                      
-- Transformer:

newtype LinearT m e e' a = LinearT {
  unLinearT :: e -> m (e', a)
}

instance Monad m => Line (LinearT m) where
  pureL f = LinearT (return . outEnv f)
  eitherL (LinearT f) (LinearT g) = LinearT $ outEnvM $ \e ->
    case eitherEnv e of
      Left e ->  inEnvM f e
      Right e -> inEnvM g e
  leftL (LinearT f) = LinearT $ outEnvM $ \e -> do
    (e', a) <- inEnvM f e
    return (leftEnv e', a)
  rightL (LinearT f) = LinearT $ outEnvM $ \e -> do
    (e', a) <- inEnvM f e
    return (rightEnv e', a)
  unitL a = LinearT (\e -> return (e, a))
  LinearT f >>>= g = LinearT (\e -> f e >>= \(e', a) -> unLinearT (g a) e')

instance Monad m => Monad (LinearT m e e) where
  (>>=)  = (>>>=)
  return = unitL

instance Monad m => LineTrans LinearT m where
  liftL f = LinearT (\e -> f >>= \a -> return (e, a))
  arrL f  = LinearT (outEnvM f)
  unsafeRunL (LVars ks) (LinearT f)
          = LinearT (return . peelEnvM ks (inEnvM f))

runLinearT :: Monad m => LinearT m Empty Empty a -> m a
runLinearT (LinearT f) = f Empty >>= return . snd

-- sample
data M = M

maybeGetLine = catch (fmap Just getLine) (const $ return Nothing)

readLList m lst =
  io maybeGetLine >>>= \s ->
  case s of
    Nothing -> unitL ()
    Just s  ->
      newLVar m s >>>= \var ->
      addLList var lst >>>
      readLList m lst

printLList m lst = elimLList lst
  (\v -> takeLVar m v   >>>=
         io . putStrLn  >>>
         printLList m lst)
  (unitL ())

a :: IO ()
a = runLinearT $
  newLList          >>>= \lst ->
  readLList M lst   >>>
  forkIOinL (lvars lst)
    (printLList M lst) >>>
  unitL ()