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

module WidgetRattus.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
import Unsafe.Coerce

import Data.Time.Clock
import Data.Time.Calendar.OrdinalDate

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

inputInClock :: InputValue -> Clock -> Bool
inputInClock :: InputValue -> Clock -> Bool
inputInClock (OneInput InputChannelIdentifier
ch a
_) Clock
cl = InputChannelIdentifier -> Clock -> Bool
channelMember InputChannelIdentifier
ch 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

rattusError :: [Char] -> a
rattusError [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
rattusError [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
rattusError [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
rattusError [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@
  -- if @not (ch `channelMember` cl)@.
  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


-- Channels

newtype C a = C {forall a. C a -> InputValue -> IO a
unC :: InputValue -> IO a} 

instance Functor C where
  fmap :: forall a b. (a -> b) -> C a -> C b
fmap a -> b
f (C InputValue -> IO a
g) = (InputValue -> IO b) -> C b
forall a. (InputValue -> IO a) -> C a
C (\InputValue
inp -> (a -> b) -> IO a -> IO b
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (InputValue -> IO a
g InputValue
inp))

instance Applicative C where
  pure :: forall a. a -> C a
pure a
x = (InputValue -> IO a) -> C a
forall a. (InputValue -> IO a) -> C a
C (\ InputValue
_ -> a -> IO a
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)

  C InputValue -> IO (a -> b)
f <*> :: forall a b. C (a -> b) -> C a -> C b
<*> C InputValue -> IO a
g = (InputValue -> IO b) -> C b
forall a. (InputValue -> IO a) -> C a
C (\InputValue
inp -> InputValue -> IO (a -> b)
f InputValue
inp IO (a -> b) -> IO a -> IO b
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> InputValue -> IO a
g InputValue
inp)


instance Monad C where
  return :: forall a. a -> C a
return = a -> C a
forall a. a -> C a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  C InputValue -> IO a
f >>= :: forall a b. C a -> (a -> C b) -> C b
>>= a -> C b
g = (InputValue -> IO b) -> C b
forall a. (InputValue -> IO a) -> C a
C (\InputValue
inp -> InputValue -> IO a
f InputValue
inp IO a -> (a -> IO b) -> IO b
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\ a
x -> C b -> InputValue -> IO b
forall a. C a -> InputValue -> IO a
unC (a -> C b
g a
x) InputValue
inp))

newtype Chan a = Chan InputChannelIdentifier

chan :: C (Chan a)
chan :: forall a. C (Chan a)
chan = (InputValue -> IO (Chan a)) -> C (Chan a)
forall a. (InputValue -> IO a) -> C a
C (\ InputValue
_ -> InputChannelIdentifier -> Chan a
forall a. InputChannelIdentifier -> Chan a
Chan (InputChannelIdentifier -> Chan a)
-> IO InputChannelIdentifier -> IO (Chan a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef InputChannelIdentifier
-> (InputChannelIdentifier
    -> (InputChannelIdentifier, InputChannelIdentifier))
-> IO InputChannelIdentifier
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef InputChannelIdentifier
nextFreshChannel (\ InputChannelIdentifier
x -> (InputChannelIdentifier
x InputChannelIdentifier
-> InputChannelIdentifier -> InputChannelIdentifier
forall a. Num a => a -> a -> a
- InputChannelIdentifier
1, InputChannelIdentifier
x)))

delayC :: O (C a) -> O a
delayC :: forall a. O (C a) -> O a
delayC (Delay Clock
c InputValue -> C a
f) = Clock -> (InputValue -> a) -> O a
forall a. Clock -> (InputValue -> a) -> O a
Delay Clock
c (\ InputValue
inp -> C a -> InputValue -> a
forall a. C a -> InputValue -> a
advC' (InputValue -> C a
f InputValue
inp) InputValue
inp)


{-# NOINLINE advC' #-}
advC' :: C a -> InputValue -> a
advC' :: forall a. C a -> InputValue -> a
advC' (C InputValue -> IO a
c) InputValue
inp =  IO a -> a
forall a. IO a -> a
unsafePerformIO (InputValue -> IO a
c InputValue
inp)

wait :: Chan a -> O a
wait :: forall a. Chan a -> O a
wait (Chan InputChannelIdentifier
ch) = Clock -> (InputValue -> a) -> O a
forall a. Clock -> (InputValue -> a) -> O a
Delay (InputChannelIdentifier -> Clock
singletonClock InputChannelIdentifier
ch) (\(OneInput InputChannelIdentifier
_ a
v) -> a -> a
forall a b. a -> b
unsafeCoerce a
v)

{-# NOINLINE nextFreshChannel #-}
nextFreshChannel :: IORef InputChannelIdentifier
nextFreshChannel :: IORef InputChannelIdentifier
nextFreshChannel = IO (IORef InputChannelIdentifier) -> IORef InputChannelIdentifier
forall a. IO a -> a
unsafePerformIO (InputChannelIdentifier -> IO (IORef InputChannelIdentifier)
forall a. a -> IO (IORef a)
newIORef (-InputChannelIdentifier
1))


-- | @timer n@ produces a delayed computation that ticks every @n@
-- milliseconds. In particular @mkSig (timer n)@ is a signal that
-- produces a new value every #n# milliseconds.
timer :: Int -> O ()
timer :: InputChannelIdentifier -> O ()
timer InputChannelIdentifier
d = Clock -> (InputValue -> ()) -> O ()
forall a. Clock -> (InputValue -> a) -> O a
Delay (InputChannelIdentifier -> Clock
singletonClock (InputChannelIdentifier
d InputChannelIdentifier
-> InputChannelIdentifier -> InputChannelIdentifier
forall a. Ord a => a -> a -> a
`max` InputChannelIdentifier
10)) (\ InputValue
_ -> ())

-- | A strict version of UTCTime
data Time = Time
  { -- | The day component
    Time -> Day
timeDay :: !Day,
    -- | The time component
    Time -> DiffTime
timeDayTime :: !DiffTime
  }
  deriving (Time -> Time -> Bool
(Time -> Time -> Bool) -> (Time -> Time -> Bool) -> Eq Time
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Time -> Time -> Bool
== :: Time -> Time -> Bool
$c/= :: Time -> Time -> Bool
/= :: Time -> Time -> Bool
Eq, Eq Time
Eq Time =>
(Time -> Time -> Ordering)
-> (Time -> Time -> Bool)
-> (Time -> Time -> Bool)
-> (Time -> Time -> Bool)
-> (Time -> Time -> Bool)
-> (Time -> Time -> Time)
-> (Time -> Time -> Time)
-> Ord Time
Time -> Time -> Bool
Time -> Time -> Ordering
Time -> Time -> Time
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Time -> Time -> Ordering
compare :: Time -> Time -> Ordering
$c< :: Time -> Time -> Bool
< :: Time -> Time -> Bool
$c<= :: Time -> Time -> Bool
<= :: Time -> Time -> Bool
$c> :: Time -> Time -> Bool
> :: Time -> Time -> Bool
$c>= :: Time -> Time -> Bool
>= :: Time -> Time -> Bool
$cmax :: Time -> Time -> Time
max :: Time -> Time -> Time
$cmin :: Time -> Time -> Time
min :: Time -> Time -> Time
Ord)

instance Show Time where
  show :: Time -> [Char]
show (Time Day
d DiffTime
t) = UTCTime -> [Char]
forall a. Show a => a -> [Char]
show (Day -> DiffTime -> UTCTime
UTCTime Day
d DiffTime
t)

time :: C Time
time :: C Time
time = (InputValue -> IO Time) -> C Time
forall a. (InputValue -> IO a) -> C a
C ((InputValue -> IO Time) -> C Time)
-> (InputValue -> IO Time) -> C Time
forall a b. (a -> b) -> a -> b
$ \ InputValue
_ ->  do UTCTime Day
d DiffTime
t <- IO UTCTime
getCurrentTime
                      Time -> IO Time
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time -> IO Time) -> Time -> IO Time
forall a b. (a -> b) -> a -> b
$ Day -> DiffTime -> Time
Time Day
d DiffTime
t


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


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