{-# LANGUAGE GADTs #-}

module AsyncRattus.InternalPrimitives where

import Prelude hiding (Left, Right)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet

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

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
  InputValue :: !InputChannelIdentifier -> !a -> InputValue


-- | 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 :: InputValue
inputValue@(InputValue InputChannelIdentifier
chId a
_)
  = if InputChannelIdentifier
chId InputChannelIdentifier -> Clock -> Bool
`channelMember` Clock
clA then
      if InputChannelIdentifier
chId InputChannelIdentifier -> Clock -> Bool
`channelMember` Clock
clB then a -> b -> Select a b
forall a b. a -> b -> Select a b
Both (InputValue -> a
inpFA InputValue
inputValue) (InputValue -> b
inpFB InputValue
inputValue)
      else a -> O b -> Select a b
forall a b. a -> O b -> Select a b
Fst (InputValue -> a
inpFA InputValue
inputValue) 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
inputValue)


-- | 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
IntSet.empty ([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


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


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