{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module AsyncRattus.InternalPrimitives where

import Prelude hiding (Left, Right)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.IORef
import Control.Concurrent.MVar
import System.IO.Unsafe
import System.Mem.Weak
import Control.Monad

-- An input channel is identified by an integer. The programmer should not know about it.
type InputChannelIdentifier = Int

type Clock = IntSet

singletonClock :: InputChannelIdentifier -> Clock
singletonClock :: InputChannelIdentifier -> Clock
singletonClock = InputChannelIdentifier -> Clock
IntSet.singleton

emptyClock :: Clock
emptyClock :: Clock
emptyClock = Clock
IntSet.empty

clockUnion :: Clock -> Clock -> Clock
clockUnion :: Clock -> Clock -> Clock
clockUnion = Clock -> Clock -> Clock
IntSet.union

channelMember :: InputChannelIdentifier -> Clock -> Bool
channelMember :: InputChannelIdentifier -> Clock -> Bool
channelMember = InputChannelIdentifier -> Clock -> Bool
IntSet.member

data InputValue where
  OneInput :: !InputChannelIdentifier -> !a -> InputValue
  MoreInputs :: !InputChannelIdentifier -> !a -> !InputValue -> InputValue

inputInClock :: InputValue -> Clock -> Bool
inputInClock :: InputValue -> Clock -> Bool
inputInClock (OneInput InputChannelIdentifier
ch a
_) Clock
cl = InputChannelIdentifier -> Clock -> Bool
channelMember InputChannelIdentifier
ch Clock
cl
inputInClock (MoreInputs InputChannelIdentifier
ch a
_ InputValue
more) Clock
cl = InputChannelIdentifier -> Clock -> Bool
channelMember InputChannelIdentifier
ch Clock
cl Bool -> Bool -> Bool
|| InputValue -> Clock -> Bool
inputInClock InputValue
more Clock
cl


-- | The "later" type modality. A value @v@ of type @O 𝜏@ consists of
-- two components: Its clock, denoted @cl(v)@, and a delayed
-- computation that will produce a value of type @𝜏@ as soon as the
-- clock @cl(v)@ ticks. The clock @cl(v)@ is only used for type
-- checking and is not directly accessible, whereas the delayed
-- computation is accessible via 'adv' and 'select'.

data O a = Delay !Clock (InputValue -> a)

-- | The return type of the 'select' primitive.
data Select a b = Fst !a !(O b) | Snd !(O a) !b | Both !a !b

asyncRattusError :: [Char] -> a
asyncRattusError [Char]
pr = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
pr [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": Did you forget to mark this as Async Rattus code?")

-- | This is the constructor for the "later" modality 'O':
--
-- >     Γ ✓θ ⊢ t :: 𝜏
-- > --------------------
-- >  Γ ⊢ delay t :: O 𝜏
--
-- The typing rule requires that its argument @t@ typecheck with an
-- additional tick @✓θ@ of some clock @θ@.
{-# INLINE [1] delay #-}
delay :: a -> O a
delay :: forall a. a -> O a
delay a
_ = [Char] -> O a
forall {a}. [Char] -> a
asyncRattusError [Char]
"delay"

extractClock :: O a -> Clock
extractClock :: forall a. O a -> Clock
extractClock (Delay Clock
cl InputValue -> a
_) = Clock
cl

{-# INLINE [1] adv' #-}
adv' :: O a -> InputValue -> a
adv' :: forall a. O a -> InputValue -> a
adv' (Delay Clock
_ InputValue -> a
f) InputValue
inp = InputValue -> a
f InputValue
inp


-- | This is the eliminator for the "later" modality 'O':
--
-- >   Γ ⊢ t :: O 𝜏     Γ' tick-free
-- > ---------------------------------
-- >     Γ ✓cl(t) Γ' ⊢ adv t :: 𝜏
--
-- It requires that a tick @✓θ@ is in the context whose clock matches
-- exactly the clock of @t@, i.e. @θ = cl(t)@.

{-# INLINE [1] adv #-}
adv :: O a -> a
adv :: forall a. O a -> a
adv O a
_ = [Char] -> a
forall {a}. [Char] -> a
asyncRattusError [Char]
"adv"

-- | If we want to eliminate more than one delayed computation, i.e.\
-- two @s :: O σ@ and @t :: O 𝜏@, we need to use 'select' instead of
-- just 'adv'.
--
-- >   Γ ⊢ s :: O σ     Γ ⊢ t :: O 𝜏     Γ' tick-free
-- > --------------------------------------------------
-- >    Γ ✓cl(s)⊔cl(t) Γ' ⊢ select s t :: Select σ 𝜏
--
-- It requires that we have a tick @✓θ@ in the context whose clock
-- matches the union of the clocks of @s@ and @t@, i.e. @θ =
-- cl(s)⊔cl(t)@. The union of two clocks ticks whenever either of the
-- two clocks ticks, i.e. @cl(s)⊔cl(t)@, whenever @cl(s)@ or @cl(t)@
-- ticks.
--
-- That means there are three possible outcomes, which are reflected
-- in the result type of @select s t@. A value of @Select σ 𝜏@ is
-- either
--
--   * a value of type @σ@ and a delayed computation of type @O 𝜏@, if
--     @cl(s)@ ticks before @cl(t)@,
--
--   * a value of type @𝜏@ and a delayed computation of type @O σ@, if
--     @cl(t)@ ticks before @cl(s)@, or
--
--   * a value of type @σ@ and a value of type @𝜏@, if @cl(s)@ and
--   * @cl(s)@ tick simultaneously.


{-# INLINE [1] select #-}
select :: O a -> O b -> Select a b
select :: forall a b. O a -> O b -> Select a b
select O a
_ O b
_ = [Char] -> Select a b
forall {a}. [Char] -> a
asyncRattusError [Char]
"select"

select' :: O a -> O b -> InputValue -> Select a b
select' :: forall a b. O a -> O b -> InputValue -> Select a b
select' a :: O a
a@(Delay Clock
clA InputValue -> a
inpFA) b :: O b
b@(Delay Clock
clB InputValue -> b
inpFB) InputValue
inp
  = if InputValue -> Clock -> Bool
inputInClock InputValue
inp Clock
clA then
      if InputValue -> Clock -> Bool
inputInClock InputValue
inp Clock
clB then a -> b -> Select a b
forall a b. a -> b -> Select a b
Both (InputValue -> a
inpFA InputValue
inp) (InputValue -> b
inpFB InputValue
inp)
      else a -> O b -> Select a b
forall a b. a -> O b -> Select a b
Fst (InputValue -> a
inpFA InputValue
inp) O b
b
    else O a -> b -> Select a b
forall a b. O a -> b -> Select a b
Snd O a
a (InputValue -> b
inpFB InputValue
inp)



-- | The clock of @never :: O 𝜏@ will never tick, i.e. it will never
-- produce a value of type @𝜏@. With 'never' we can for example
-- implement the constant signal @x ::: never@ of type @Sig a@ for any @x ::
-- a@.
never :: O a
never :: forall a. O a
never = Clock -> (InputValue -> a) -> O a
forall a. Clock -> (InputValue -> a) -> O a
Delay Clock
emptyClock ([Char] -> InputValue -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Trying to adv on the 'never' delayed computation")

-- | A type is @Stable@ if it is a strict type and the later modality
-- @O@ and function types only occur under @Box@.
--
-- For example, these types are stable: @Int@, @Box (a -> b)@, @Box (O
-- Int)@, @Box (Sig a -> Sig b)@.
--
-- But these types are not stable: @[Int]@ (because the list type is
-- not strict), @Int -> Int@, (function type is not stable), @O
-- Int@, @Sig Int@.

class  Stable a  where



-- | The "stable" type modality. A value of type @Box a@ is a
-- time-independent computation that produces a value of type @a@.
-- Use 'box' and 'unbox' to construct and consume 'Box'-types.
data Box a = Box a


-- | This is the constructor for the "stable" modality 'Box':
--
-- >     Γ☐ ⊢ t :: 𝜏
-- > --------------------
-- >  Γ ⊢ box t :: Box 𝜏
--
-- where Γ☐ is obtained from Γ by removing all ticks and all variables
-- @x :: 𝜏@, where 𝜏 is not a stable type.

{-# INLINE [1] box #-}
box :: a -> Box a
box :: forall a. a -> Box a
box a
x = a -> Box a
forall a. a -> Box a
Box a
x


-- | This is the eliminator for the "stable" modality  'Box':
--
-- >   Γ ⊢ t :: Box 𝜏
-- > ------------------
-- >  Γ ⊢ unbox t :: 𝜏
{-# INLINE [1] unbox #-}
unbox :: Box a -> a
unbox :: forall a. Box a -> a
unbox (Box a
d) = a
d


defaultPromote :: Continuous a => a -> Box a
defaultPromote :: forall a. Continuous a => a -> Box a
defaultPromote a
x = IO (Box a) -> Box a
forall a. IO a -> a
unsafePerformIO (IO (Box a) -> Box a) -> IO (Box a) -> Box a
forall a b. (a -> b) -> a -> b
$ 
    do IORef a
r <- a -> IO (IORef a)
forall a. a -> IO (IORef a)
newIORef a
x
       Weak (IORef a)
r' <- IORef a -> IO () -> IO (Weak (IORef a))
forall a. IORef a -> IO () -> IO (Weak (IORef a))
mkWeakIORef IORef a
r (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) 
       IORef [ContinuousData]
-> ([ContinuousData] -> [ContinuousData]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [ContinuousData]
promoteStore (Weak (IORef a) -> ContinuousData
forall a. Continuous a => Weak (IORef a) -> ContinuousData
ContinuousData Weak (IORef a)
r' ContinuousData -> [ContinuousData] -> [ContinuousData]
forall a. a -> [a] -> [a]
:)
       Box a -> IO (Box a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Box a
forall a. a -> Box a
Box (IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$ IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
r))


class Continuous p where
  -- | Computes the same as 'progressInternal' and 'nextProgress'. In
  -- particular @progressAndNext inp v = (progressInternal inp v,
  -- nextProgress (progressInternal inp v))@.
  progressAndNext :: InputValue -> p -> (p , Clock)

  -- | Progresses the continuous value, given the input value from
  -- some channel
  progressInternal :: InputValue -> p -> p
  -- | Computes the set of channels that the continuous value is
  -- depending on. That is if @nextProgress v = cl@ and a new input
  -- @inp@ on channel @ch@ arrives, then @progressInternal inp v = v@.
  nextProgress :: p -> Clock 
  promoteInternal :: p -> Box p
  promoteInternal = p -> Box p
forall a. Continuous a => a -> Box a
defaultPromote

-- For stable types we can circumvent the "promote store".
instance {-# OVERLAPPABLE #-} Stable a => Continuous a where
    progressAndNext :: InputValue -> a -> (a, Clock)
progressAndNext InputValue
_ a
x = (a
x , Clock
emptyClock) 
    progressInternal :: InputValue -> a -> a
progressInternal InputValue
_ a
x = a
x
    nextProgress :: a -> Clock
nextProgress a
_ = Clock
emptyClock
    promoteInternal :: a -> Box a
promoteInternal = a -> Box a
forall a. a -> Box a
Box

data ContinuousData where
   ContinuousData :: Continuous a => !(Weak (IORef a)) -> ContinuousData

-- TODO: The list type needs to be replaced by a more efficient
-- mutable data structure.
{-# NOINLINE promoteStore #-}
promoteStore :: IORef [ContinuousData]
promoteStore :: IORef [ContinuousData]
promoteStore = IO (IORef [ContinuousData]) -> IORef [ContinuousData]
forall a. IO a -> a
unsafePerformIO ([ContinuousData] -> IO (IORef [ContinuousData])
forall a. a -> IO (IORef a)
newIORef [])

{-# NOINLINE progressPromoteStoreMutex #-}
progressPromoteStoreMutex :: MVar ()
progressPromoteStoreMutex :: MVar ()
progressPromoteStoreMutex = IO (MVar ()) -> MVar ()
forall a. IO a -> a
unsafePerformIO (() -> IO (MVar ())
forall a. a -> IO (MVar a)
newMVar ())


-- | Atomic version of 'progressPromoteStore'.

progressPromoteStoreAtomic :: InputValue -> IO ()
progressPromoteStoreAtomic :: InputValue -> IO ()
progressPromoteStoreAtomic InputValue
inp = do
    MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
progressPromoteStoreMutex
    InputValue -> IO ()
progressPromoteStore InputValue
inp
    MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
progressPromoteStoreMutex ()


-- | For promote to work, its argument must be stored in the "promote
-- store", and whenenver an input is received on some channel, all
-- values in the "promote store" must be advanced (using
-- 'progressInternal').

progressPromoteStore :: InputValue -> IO ()
progressPromoteStore :: InputValue -> IO ()
progressPromoteStore InputValue
inp = do 
    [ContinuousData]
xs <- IORef [ContinuousData]
-> ([ContinuousData] -> ([ContinuousData], [ContinuousData]))
-> IO [ContinuousData]
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef [ContinuousData]
promoteStore (\[ContinuousData]
x -> ([],[ContinuousData]
x))
    [ContinuousData]
xs' <- (ContinuousData -> IO Bool)
-> [ContinuousData] -> IO [ContinuousData]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ContinuousData -> IO Bool
run [ContinuousData]
xs
    IORef [ContinuousData]
-> ([ContinuousData] -> ([ContinuousData], ())) -> IO ()
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef [ContinuousData]
promoteStore (\[ContinuousData]
x -> ([ContinuousData]
x [ContinuousData] -> [ContinuousData] -> [ContinuousData]
forall a. [a] -> [a] -> [a]
++ [ContinuousData]
xs',()))
  where run :: ContinuousData -> IO Bool
run (ContinuousData Weak (IORef a)
x) = do
          Maybe (IORef a)
d <- Weak (IORef a) -> IO (Maybe (IORef a))
forall v. Weak v -> IO (Maybe v)
deRefWeak Weak (IORef a)
x
          case Maybe (IORef a)
d of
            Maybe (IORef a)
Nothing -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
            Just IORef a
x -> IORef a -> (a -> a) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef a
x (InputValue -> a -> a
forall p. Continuous p => InputValue -> p -> p
progressInternal InputValue
inp) IO () -> IO Bool -> IO Bool
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

promote :: Continuous a => a -> Box a
promote :: forall a. Continuous a => a -> Box a
promote a
x = a -> Box a
forall a. Continuous a => a -> Box a
promoteInternal a
x

newtype Chan a = Chan InputChannelIdentifier

{-# RULES
  "unbox/box"    forall x. unbox (box x) = x
    #-}


{-# RULES
  "box/unbox"    forall x. box (unbox x) = x
    #-}