module Control.Computation.Resourceful (

    -- * Computations

    module Control.Computation,

    -- * Resourceful computations

    type (~>),
    type Resourceful,
    type Blank,
    type (**),
    type (-:),

    -- * Resources

    Resource (anchor),
    type Anchor (Anchor),

    -- * Attributes

    type Attr,
    unsafeToAttr,
    type Property (Property),
    (^>),
    (>^),
    (^^>),
    (>^^),
    unsafeToProperty,
    ResourceFunction (get),

    -- * Resource values

    type ResourceValue (annotate),
    type Annotator,

    -- * Atomic resources

    type AtomicResource,
    unsafeToResourceConv,
    fromResourceConv,
    toUnitResource,
    fromUnitResource,
    toPairResource,
    fromPairResource

) where

{-FIXME:
    Make this module work well with Safe Haskell, which possibly includes moving
    the two unsafe functions into a separate module.
-}

-- Prelude

import Prelude hiding (id, (.), curry, uncurry)

-- Control

import Control.Category
import Control.Arrow
import Control.Computation
import Control.Applicative

-- Data

import Data.Monoid
import Data.Traversable

-- System

import System.IO.Unsafe

-- Fixities

infixr 0 ~>
infixr 7 **
infixr 1 -:
infixr 1 ^>
infixr 1 >^
infixr 1 ^^>
infixr 1 >^^

-- * Resourceful computations

newtype a ~> b = Resourceful (a -> b) deriving (Category, Arrow, ArrowChoice)

type Resourceful = (~>)

data Blank = Blank { fromBlank :: Shredder }
{-NOTE:
    We have to use data instead of newtype, since otherwise the user could
    trigger the I/O via seq.
-}

newtype a ** b = ResourcefulPair { stdPair :: (a, b) }

newtype a -: b = ResourcefulFunction { stdFunction :: a -> b }

instance Computation Resourceful where

    type Unit Resourceful = Blank

    type Pair Resourceful = (**)

    type Function Resourceful = (-:)

    type DropResult Resourceful a = ResourceValue a

    Resourceful fun1 ### Resourceful fun2 = Resourceful $ stdPair         >>>
                                                          fun1 ### fun2   >>>
                                                          ResourcefulPair

    assocLeft = Resourceful $ stdPair                >>>
                              mapSnd stdPair         >>>
                              assocLeft              >>>
                              mapFst ResourcefulPair >>>
                              ResourcefulPair

    assocRight = Resourceful $ stdPair                >>>
                               mapFst stdPair         >>>
                               assocRight             >>>
                               mapSnd ResourcefulPair >>>
                               ResourcefulPair

    padFst = Resourceful $ const (Blank mempty) &&& id >>>
                           ResourcefulPair

    padSnd = Resourceful $ id &&& const (Blank mempty) >>>
                           ResourcefulPair

    dropFst = Resourceful $ stdPair                >>>
                            mapFst fromBlank       >>>
                            uncurry insertShredder

    dropSnd = Resourceful $ stdPair                       >>>
                            mapSnd fromBlank              >>>
                            uncurry (flip insertShredder)

    swap = Resourceful $ stdPair         >>>
                         swap            >>>
                         ResourcefulPair

    curry (Resourceful fun) = Resourceful $ curry (ResourcefulPair >>> fun) >>>
                                            ResourcefulFunction

    apply = Resourceful $ stdPair            >>>
                          mapFst stdFunction >>>
                          apply

-- * Connection to pure computations

instance Connected Pure Resourceful where

    data (Pure ==> Resourceful) a = Up {
                                        shredder :: Shredder,
                                        value    :: a
                                    }

    newtype (Pure <== Resourceful) b = Down { fromDown :: Shredder -> b }

    inject val = Down $ \ shredder -> Up shredder val

    extract = Resourceful fun where

        fun (Up shredder (Down toVal)) = toVal shredder

instance Link (Pure ==> Resourceful) where

    type Source (Pure ==> Resourceful) = Pure

    type Target (Pure ==> Resourceful) = Resourceful

    linkMap comp = Resourceful fun where

        fun (Up shredder val) = Up shredder (comp val)

    unitInside = Resourceful fun where

        fun (Blank shredder) = Up shredder ()

    pairInside = Resourceful $ stdPair >>> fun where

        fun (Up shredder1 val1, Up shredder2 val2) = Up (shredder1 <> shredder2)
                                                        (val1, val2)

instance Link (Pure <== Resourceful) where

    type Source (Pure <== Resourceful) = Resourceful

    type Target (Pure <== Resourceful) = Pure

    linkMap (Resourceful fun) = comp where

        comp (Down toVal) = Down (toVal >>> fun)

    unitInside _ = Down Blank

    pairInside (Down toVal1, Down toVal2) = Down toVal' where

        toVal' shredder = ResourcefulPair (toVal1 shredder, toVal2 shredder)

-- * Resources

class ResourceFunction a => Resource a where

    anchor :: Anchor a

data Anchor a = forall h . Anchor (a ~> AtomicResource h)
                                  (AtomicResource h ~> a)

instance Resource (AtomicResource h) where

    anchor = Anchor id id

instance Resource Blank where

    anchor = Anchor toUnitResource fromUnitResource

instance (Resource a, Resource b) => Resource (a ** b) where

    anchor = case (anchor, anchor) of
        (Anchor toAtomic1 fromAtomic1, Anchor toAtomic2 fromAtomic2)
            -> Anchor (toAtomic1 ### toAtomic2 >>> toPairResource)
                      (fromPairResource >>> fromAtomic1 ### fromAtomic2)

-- * Attributes

type Attr a v = Property a a v

unsafeToAttr :: (h -> IO v) -> Attr (AtomicResource h) v
unsafeToAttr attrIOFun = unsafeToProperty $ \ hdl -> do
    val <- attrIOFun hdl
    return (val, hdl)

newtype Property a b v = Property (forall h . (v -> (b ~> AtomicResource h)) ->
                                              (a ~> AtomicResource h))

instance Functor (Property a b) where

    fmap fun (Property contPassing) = prop where

        prop = Property (\ cont -> contPassing (cont . fun))

(^>) :: (a -> b) -> Property b c v -> Property a c v
fun ^> prop = arr fun ^^> prop

(>^) :: Property a b v -> (b -> c) -> Property a c v
prop >^ fun = prop >^^ arr fun

(^^>) :: (a ~> b) -> Property b c v -> Property a c v
comp ^^> Property contPassing = prop where

    prop = Property (\ cont -> comp >>> contPassing cont)

(>^^) :: Property a b v -> (b ~> c) -> Property a c v
Property contPassing >^^ comp = prop where

    prop = Property (\ cont -> contPassing ((comp >>>) . cont))

unsafeToProperty :: (h -> IO (v, k))
                 -> Property (AtomicResource h) (AtomicResource k) v
unsafeToProperty propIOFun = prop where

    prop = Property (\ valDependent -> unsafeToResourceConv (\ hdl -> do
        (val, hdl') <- propIOFun hdl
        fromResourceConv (valDependent val) hdl'))

class ResourceFunction r where

    get :: Property a b v -> (v -> (b ~> r)) -> (a ~> r)

instance ResourceFunction (AtomicResource h) where

    get = resourceGet

instance ResourceFunction Blank where

    get = resourceGet

instance (Resource a, Resource b) => ResourceFunction (a ** b) where

    get = resourceGet

instance ResourceFunction b => ResourceFunction (a -: b) where

    get prop valDependent = Resourceful (ResourcefulFunction . ctxFun) where

        ctxFun res ctx = fun res where

            Resourceful fun = get prop $
                              \ val -> valDependent val              >>>
                                       arr (stdFunction >>> ($ ctx))

resourceGet :: Resource r => Property a b v -> (v -> (b ~> r)) -> (a ~> r)
resourceGet (Property contPassing) valDependent = case anchor of
    Anchor toAtomic fromAtomic -> result where

        result = contPassing (valDependent >>> (>>> toAtomic)) >>> fromAtomic

-- * Resource values

class ResourceValue a where

    annotate :: a -> Annotator a
    annotate = pure

newtype Annotator a = Annotator { fromAnnotator :: Shredder -> a }
                      deriving (Functor, Applicative)

{-NOTE:
    Here we define instances for all Prelude types that are unrelated to I/O.
-}

instance ResourceValue (AtomicResource h) where

    annotate = withShredder >>> Annotator where

        withShredder (AtomicResource gen) shredder = AtomicResource gen' where

            gen' = fromShredder shredder *> gen

instance ResourceValue Blank where

    annotate = withShredder >>> Annotator where

        withShredder (Blank shredder) shredder' = Blank (shredder' <> shredder)

instance ResourceValue a => ResourceValue (a ** b) where

    annotate = withShredder >>> Annotator where

        withShredder pair shredder = ResourcefulPair $
                                     (insertShredder shredder val1, val2) where

            (val1, val2) = stdPair pair

instance ResourceValue b => ResourceValue (a -: b) where

    annotate = withShredder >>> Annotator where

        withShredder fun shredder = ResourcefulFunction $
                                    stdFunction fun         >>>
                                    insertShredder shredder

instance ResourceValue ((Pure ==> Resourceful) a) where

    annotate = withShredder >>> Annotator where

        withShredder (Up shredder val) shredder' = Up (shredder' <> shredder)
                                                      val

instance ResourceValue Bool

instance ResourceValue a => ResourceValue (Maybe a) where

    annotate = traverse annotate

instance (ResourceValue a, ResourceValue b) => ResourceValue (Either a b) where

    annotate (Left  val1) = Left  <$> annotate val1
    annotate (Right val2) = Right <$> annotate val2

instance ResourceValue Ordering

instance ResourceValue Char

instance ResourceValue Int

instance ResourceValue Integer

instance ResourceValue Float

instance ResourceValue Double

instance ResourceValue Rational

instance ResourceValue a => ResourceValue [a] where

    annotate = traverse annotate

instance ResourceValue ()

instance (ResourceValue a, ResourceValue b) => ResourceValue (a, b) where

    annotate (val1, val2) = (,) <$> annotate val1 <*> annotate val2

instance (ResourceValue a, ResourceValue b, ResourceValue c) =>
         ResourceValue (a, b, c) where

    annotate (val1, val2, val3) = (,,) <$> annotate val1
                                       <*> annotate val2
                                       <*> annotate val3

instance (ResourceValue a, ResourceValue b, ResourceValue c, ResourceValue d) =>
         ResourceValue (a, b, c, d) where

    annotate (val1, val2, val3, val4) = (,,,) <$> annotate val1
                                              <*> annotate val2
                                              <*> annotate val3
                                              <*> annotate val4

instance (ResourceValue a,
          ResourceValue b,
          ResourceValue c,
          ResourceValue d,
          ResourceValue e) =>
         ResourceValue (a, b, c, d, e) where

    annotate (val1, val2, val3, val4, val5) = (,,,,) <$> annotate val1
                                                     <*> annotate val2
                                                     <*> annotate val3
                                                     <*> annotate val4
                                                     <*> annotate val5

instance (ResourceValue a,
          ResourceValue b,
          ResourceValue c,
          ResourceValue d,
          ResourceValue e,
          ResourceValue f) =>
         ResourceValue (a, b, c, d, e, f) where

    annotate (val1, val2, val3, val4, val5, val6) = (,,,,,) <$> annotate val1
                                                            <*> annotate val2
                                                            <*> annotate val3
                                                            <*> annotate val4
                                                            <*> annotate val5
                                                            <*> annotate val6

instance (ResourceValue a, ResourceValue b) => ResourceValue (a -> b)
{-NOTE:
    This instance declaration is correct, because we have this non-standard
    definition of (->) in the Resourceful category, where α -> β for a resource
    type R corresponds to ∀ Q . α Q → β Q. This is independent of R, and for
    every r : Q → R, the morphism (α -> β) r is just the identity.
-}

insertShredder :: ResourceValue a => Shredder -> a -> a
insertShredder = flip (fromAnnotator . annotate)

-- * Atomic resources

data AtomicResource h = AtomicResource (Gen h)
{-NOTE:
    Note that we have to use data instead of newtype, since otherwise the user
    could trigger the I/O via seq.
-}

{-# NOINLINE unsafeToResourceConv #-}
unsafeToResourceConv :: (h -> IO k) -> (AtomicResource h ~> AtomicResource k)
unsafeToResourceConv ioFun = Resourceful fun where

    fun (AtomicResource gen) = AtomicResource $
                               unsafePerformIO $
                               case gen of Gen hdl -> Gen <$> ioFun hdl

{-NOTE:

    Regarding unsafePerformIO:

      • We hope that putting the application of unsafePerformIO into a where
        clause does not cause harm due to inlining or such.

      • We have not disabled common subexpression elimination for this module,
        as we do not see how CSE could cause harm in connection with our use of
        unsafePerformIO. However if we were to add another function that uses
        unsafePerformIO, we should check whether this is still safe.

    Regarding Gen being no monad:

      • It looks like Gen could be a monad. Then we could just implement a
        conversion from IO to Gen and implement unsafeToResourceConv in terms of
        (>>=) of the Gen monad. However, the second argument of (>>=) would be a
        generator that does not refer to the initial resource set, but to the
        one that is left by the first argument. This is in contradiction with
        the idea that generators generate resources from the initial resource
        set. (However, we do not have the approach anymore that Gen refers to
        some “initial” resource set, but that every Gen value refers to some
        specific resource set.)
-}

fromResourceConv :: (AtomicResource h ~> AtomicResource k) -> (h -> IO k)
fromResourceConv (Resourceful fun) hdl = io where

    io = do
             AtomicResource (Gen hdl') <- return $
                                          fun (AtomicResource (pure hdl))
             return hdl'

toUnitResource :: Blank ~> AtomicResource ()
toUnitResource = Resourceful fun where

    fun (Blank shredder) = AtomicResource (fromShredder shredder)

fromUnitResource :: AtomicResource () ~> Blank
fromUnitResource = Resourceful fun where

    fun (AtomicResource gen) = Blank (toShredder gen)

toPairResource :: AtomicResource h ** AtomicResource k ~> AtomicResource (h, k)
toPairResource = Resourceful $ stdPair >>> fun where

    fun (AtomicResource gen1, AtomicResource gen2) = AtomicResource $
                                                     (,) <$> gen1 <*> gen2

fromPairResource :: AtomicResource (h, k) ~> AtomicResource h ** AtomicResource k
fromPairResource = Resourceful $ fun >>> ResourcefulPair where

    fun (AtomicResource gen) = (AtomicResource gen1, AtomicResource gen2) where

        gen1 = fst <$> gen

        gen2 = snd <$> gen

-- * Generators

data Gen h = Gen h
{-NOTE:
    A value of type Gen h denotes a morphism in the resource category from some
    Q to h. The Q is not visible in the type, but every value of type Gen h has
    an associated Q. The implementation of this module has to make sure that Gen
    is only used in type-safe ways regarding the Qs.
-}

instance Functor Gen where

    fmap fun (Gen hdl) = Gen (fun hdl)

instance Applicative Gen where

    pure = Gen

    Gen fun <*> Gen arg = Gen (fun arg)

data Shredder = Shredder

toShredder :: Gen () -> Shredder
toShredder (Gen _) = Shredder

fromShredder :: Shredder -> Gen ()
fromShredder Shredder = Gen ()

instance Monoid Shredder where

    mempty = Shredder

    Shredder `mappend` Shredder = Shredder