{-# OPTIONS_HADDOCK not-home #-}

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

-- |
--
-- This module provides the 'Purify' data type, which wraps a imperative propagator
-- (for example "Data.Propagator.Naive") in a pure data structure.
--
-- It provides functions to declare the inputs to these propagators, which are unsafe on their own, but can be instantiated and wrapped to form safe APIs, e.g. "Data.Recursive.Bool".
--
-- This module is labeled as Internal because its safety depends on the behaviour of the
-- underlying propagator implementation. The assumptions is that
--
-- * The defining function passed to `def1` etc. declare a functional relation
--   between the input propagators and the output propagator.
-- * Defining functions do not (observably) affect their input propagators.
-- * Once all the functions passed to `def1` of a propagator and its
--   dependencies have run, `readProp` will return a correct value, i.e. one
--   that satisfies the functional relations.
-- * The order in which the defining functions are executed does not affect the
--   result.
-- * Termination depends on the termination of the underlying propagator
--
module Data.Propagator.Purify
    ( Purify
    , get
    , mk, def1, def2, defList
    )
where

import System.IO.Unsafe

import Data.Propagator.Class
import System.IO.RecThunk

-- | A value of type @Purify p@ is a propagator @p@, gether with a (lazy)
-- action to define it.
--
-- You can use 'get' to extract the value from the propagator.
--
-- Do not use the extracted value in the definition of that value, this will
-- loop just like a recursive definition with plain values would!
data Purify p = Purify
        { forall p. Purify p -> p
prop :: p
        , forall p. Purify p -> Thunk
pre :: Thunk
        , forall p. Purify p -> Thunk
post :: Thunk
        }

-- | Any value of type @a@ is also a value of type @Purify p@ if @p@ is a propagator for @a@.
mk :: Propagator p a => a -> Purify p
mk :: forall p a. Propagator p a => a -> Purify p
mk a
x = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
    p
p <- forall p x. Propagator p x => x -> IO p
newConstProp a
x
    Thunk
t1 <- IO Thunk
doneThunk
    Thunk
t2 <- IO Thunk
doneThunk
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall p. p -> Thunk -> Thunk -> Purify p
Purify p
p Thunk
t1 Thunk
t2)

new :: Propagator p a => [Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p
new :: forall p a.
Propagator p a =>
[Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p
new [Thunk]
ts1 [Thunk]
ts2 p -> IO ()
act = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
    p
p <- forall p x. Propagator p x => IO p
newProp
    Thunk
t1 <- IO [Thunk] -> IO Thunk
thunk forall a b. (a -> b) -> a -> b
$ p -> IO ()
act p
p forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Thunk]
ts1
    Thunk
t2 <- IO [Thunk] -> IO Thunk
thunk forall a b. (a -> b) -> a -> b
$ forall p x. Propagator p x => p -> IO ()
freezeProp p
p forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Thunk]
ts2
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall p. p -> Thunk -> Thunk -> Purify p
Purify p
p Thunk
t1 Thunk
t2)

-- | Defines a value of type @Purify b@ to be a function of the values of @Purify a@.
--
-- The action passed should declare that relation to the underlying propagator.
--
-- The @Prop a@ propagator must only be used for reading values /from/.
def1 :: (Propagator pa a, Propagator pb b) =>
    (pa -> pb -> IO ()) ->
    Purify pa -> Purify pb
def1 :: forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
def1 pa -> pb -> IO ()
def Purify pa
r1 = forall p a.
Propagator p a =>
[Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p
new [forall p. Purify p -> Thunk
pre Purify pa
r1] [forall p. Purify p -> Thunk
post Purify pa
r1] forall a b. (a -> b) -> a -> b
$ \pb
p -> do
    pa -> pb -> IO ()
def (forall p. Purify p -> p
prop Purify pa
r1) pb
p

-- | Defines a value of type @Purify c@ to be a function of the values of @Purify a@ and @Purify b@.
--
-- The action passed should declare that relation to the underlying propagator.
--
-- The @Prop a@ and @Prop b@ propagators must only be used for reading values /from/.
def2 :: (Propagator pa a, Propagator pb b, Propagator pc c) =>
    (pa -> pb -> pc -> IO ()) ->
    Purify pa -> Purify pb -> Purify pc
def2 :: forall pa a pb b pc c.
(Propagator pa a, Propagator pb b, Propagator pc c) =>
(pa -> pb -> pc -> IO ()) -> Purify pa -> Purify pb -> Purify pc
def2 pa -> pb -> pc -> IO ()
def Purify pa
r1 Purify pb
r2 = forall p a.
Propagator p a =>
[Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p
new [forall p. Purify p -> Thunk
pre Purify pa
r1, forall p. Purify p -> Thunk
pre Purify pb
r2] [forall p. Purify p -> Thunk
post Purify pa
r1, forall p. Purify p -> Thunk
post Purify pb
r2] forall a b. (a -> b) -> a -> b
$ \pc
p -> do
    pa -> pb -> pc -> IO ()
def (forall p. Purify p -> p
prop Purify pa
r1) (forall p. Purify p -> p
prop Purify pb
r2) pc
p

-- | Defines a value of type @Purify b@ to be a function of the values of a list of @Purify a@ values.
--
-- The action passed should declare that relation to the underlying propagator.
--
-- The @Prop a@ propagators must only be used for reading values /from/.
defList :: (Propagator pa a, Propagator pb b) =>
    ([pa] -> pb -> IO ()) ->
    [Purify pa] -> Purify pb
defList :: forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
([pa] -> pb -> IO ()) -> [Purify pa] -> Purify pb
defList [pa] -> pb -> IO ()
def [Purify pa]
rs = forall p a.
Propagator p a =>
[Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p
new (forall a b. (a -> b) -> [a] -> [b]
map forall p. Purify p -> Thunk
pre [Purify pa]
rs) (forall a b. (a -> b) -> [a] -> [b]
map forall p. Purify p -> Thunk
post [Purify pa]
rs) forall a b. (a -> b) -> a -> b
$ \pb
p -> do
    [pa] -> pb -> IO ()
def (forall a b. (a -> b) -> [a] -> [b]
map forall p. Purify p -> p
prop [Purify pa]
rs) pb
p

-- | Extract the value from a @Purify a@. This must not be used when /defining/ that value.
get :: Propagator pa a => Purify pa -> a
get :: forall pa a. Propagator pa a => Purify pa -> a
get Purify pa
r = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
    Thunk -> IO ()
force (forall p. Purify p -> Thunk
pre Purify pa
r)
    Thunk -> IO ()
force (forall p. Purify p -> Thunk
post Purify pa
r)
    forall p x. Propagator p x => p -> IO x
readProp (forall p. Purify p -> p
prop Purify pa
r)