{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE UnboxedTuples #-}

module Bluefin.Internal.Prim where

import Bluefin.Internal
  ( Eff,
    Effects,
    Handle,
    HandleD (MkHandleD),
    OneWayCoercibleHandle,
    effIO,
    makeOp,
    unsafeProvideIO,
    (:&),
    type (<:),
  )
import Bluefin.Internal.OneWayCoercible
  ( OneWayCoercible (..),
    unsafeOneWayCoercible,
  )
import Control.Monad.Primitive qualified as P
import Data.Kind (Type)
import GHC.Exts (State#)
import Unsafe.Coerce (unsafeCoerce)

type Prim :: Effects -> Effects -> Type
data Prim e1 e2 = UnsafeMkPrim
  deriving (HandleD (Prim e1)
(forall (e :: Effects) (es :: Effects).
 (e <: es) =>
 OneWayCoercible (Prim e1 e) (Prim e1 es)) =>
HandleD (Prim e1) -> Handle (Prim e1)
forall (e1 :: Effects). HandleD (Prim e1)
forall (e :: Effects) (es :: Effects).
(e <: es) =>
OneWayCoercible (Prim e1 e) (Prim e1 es)
forall (e1 :: Effects) (e :: Effects) (es :: Effects).
(e <: es) =>
OneWayCoercible (Prim e1 e) (Prim e1 es)
forall (h :: Effects -> *).
(forall (e :: Effects) (es :: Effects).
 (e <: es) =>
 OneWayCoercible (h e) (h es)) =>
HandleD h -> Handle h
$chandleImpl :: forall (e1 :: Effects). HandleD (Prim e1)
handleImpl :: HandleD (Prim e1)
Handle) via OneWayCoercibleHandle (Prim e1)

type role Prim nominal nominal

data PrimStateEff (es :: Effects)

instance (e2 <: es) => OneWayCoercible (Prim e1 e2) (Prim e1 es) where
  oneWayCoercibleImpl :: OneWayCoercibleD (Prim e1 e2) (Prim e1 es)
oneWayCoercibleImpl = OneWayCoercibleD (Prim e1 e2) (Prim e1 es)
forall {k} (a :: k) (b :: k). OneWayCoercibleD a b
unsafeOneWayCoercible

runPrim ::
  (forall e. Prim e e -> Eff (e :& es) r) ->
  -- | ͘
  Eff es r
runPrim :: forall (es :: Effects) r.
(forall (e :: Effects). Prim e e -> Eff (e :& es) r) -> Eff es r
runPrim forall (e :: Effects). Prim e e -> Eff (e :& es) r
k = Eff (es :& es) r -> Eff es r
forall (e :: Effects) r. Eff (e :& e) r -> Eff e r
makeOp (Prim es es -> Eff (es :& es) r
forall (e :: Effects). Prim e e -> Eff (e :& es) r
k Prim es es
forall (e1 :: Effects) (e2 :: Effects). Prim e1 e2
UnsafeMkPrim)

type StateM s a = State# s -> (# State# s, a #)

unsafeCoerceStateM :: forall s1 s2 a. StateM s1 a -> StateM s2 a
unsafeCoerceStateM :: forall s1 s2 a. StateM s1 a -> StateM s2 a
unsafeCoerceStateM = StateM s1 a -> StateM s2 a
forall a b. a -> b
unsafeCoerce

primitive ::
  forall e1 e2 es a.
  (e2 <: es) =>
  Prim e1 e2 ->
  (State# (PrimStateEff e1) -> (# State# (PrimStateEff e1), a #)) ->
  -- | ͘
  Eff es a
primitive :: forall (e1 :: Effects) (e2 :: Effects) (es :: Effects) a.
(e2 <: es) =>
Prim e1 e2
-> (State# (PrimStateEff e1) -> (# State# (PrimStateEff e1), a #))
-> Eff es a
primitive Prim e1 e2
UnsafeMkPrim State# (PrimStateEff e1) -> (# State# (PrimStateEff e1), a #)
k = (forall (e :: Effects). IOE e -> Eff (e :& es) a) -> Eff es a
forall (es :: Effects) a.
(forall (e :: Effects). IOE e -> Eff (e :& es) a) -> Eff es a
unsafeProvideIO ((forall (e :: Effects). IOE e -> Eff (e :& es) a) -> Eff es a)
-> (forall (e :: Effects). IOE e -> Eff (e :& es) a) -> Eff es a
forall a b. (a -> b) -> a -> b
$ \IOE e
io ->
  IOE e -> IO a -> Eff (e :& es) a
forall (e :: Effects) (es :: Effects) a.
(e <: es) =>
IOE e -> IO a -> Eff es a
effIO
    IOE e
io
    (forall (m :: * -> *) a.
PrimMonad m =>
(State# (PrimState m) -> (# State# (PrimState m), a #)) -> m a
P.primitive @IO (forall s1 s2 a. StateM s1 a -> StateM s2 a
unsafeCoerceStateM @(PrimStateEff e1) @P.RealWorld State# (PrimStateEff e1) -> (# State# (PrimStateEff e1), a #)
k))