{-# 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 = IO (Purify p) -> Purify p
forall a. IO a -> a
unsafePerformIO (IO (Purify p) -> Purify p) -> IO (Purify p) -> Purify p
forall a b. (a -> b) -> a -> b
$ do
    p
p <- a -> IO p
forall p x. Propagator p x => x -> IO p
newConstProp a
x
    Thunk
t1 <- IO Thunk
doneThunk
    Thunk
t2 <- IO Thunk
doneThunk
    Purify p -> IO (Purify p)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (p -> Thunk -> Thunk -> Purify p
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 = IO (Purify p) -> Purify p
forall a. IO a -> a
unsafePerformIO (IO (Purify p) -> Purify p) -> IO (Purify p) -> Purify p
forall a b. (a -> b) -> a -> b
$ do
    p
p <- IO p
forall p x. Propagator p x => IO p
newProp
    Thunk
t1 <- IO [Thunk] -> IO Thunk
thunk (IO [Thunk] -> IO Thunk) -> IO [Thunk] -> IO Thunk
forall a b. (a -> b) -> a -> b
$ p -> IO ()
act p
p IO () -> IO [Thunk] -> IO [Thunk]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Thunk] -> IO [Thunk]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Thunk]
ts1
    Thunk
t2 <- IO [Thunk] -> IO Thunk
thunk (IO [Thunk] -> IO Thunk) -> IO [Thunk] -> IO Thunk
forall a b. (a -> b) -> a -> b
$ p -> IO ()
forall p x. Propagator p x => p -> IO ()
freezeProp p
p IO () -> IO [Thunk] -> IO [Thunk]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Thunk] -> IO [Thunk]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Thunk]
ts2
    Purify p -> IO (Purify p)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (p -> Thunk -> Thunk -> Purify p
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 = [Thunk] -> [Thunk] -> (pb -> IO ()) -> Purify pb
forall p a.
Propagator p a =>
[Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p
new [Purify pa -> Thunk
forall p. Purify p -> Thunk
pre Purify pa
r1] [Purify pa -> Thunk
forall p. Purify p -> Thunk
post Purify pa
r1] ((pb -> IO ()) -> Purify pb) -> (pb -> IO ()) -> Purify pb
forall a b. (a -> b) -> a -> b
$ \pb
p -> do
    pa -> pb -> IO ()
def (Purify pa -> pa
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 = [Thunk] -> [Thunk] -> (pc -> IO ()) -> Purify pc
forall p a.
Propagator p a =>
[Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p
new [Purify pa -> Thunk
forall p. Purify p -> Thunk
pre Purify pa
r1, Purify pb -> Thunk
forall p. Purify p -> Thunk
pre Purify pb
r2] [Purify pa -> Thunk
forall p. Purify p -> Thunk
post Purify pa
r1, Purify pb -> Thunk
forall p. Purify p -> Thunk
post Purify pb
r2] ((pc -> IO ()) -> Purify pc) -> (pc -> IO ()) -> Purify pc
forall a b. (a -> b) -> a -> b
$ \pc
p -> do
    pa -> pb -> pc -> IO ()
def (Purify pa -> pa
forall p. Purify p -> p
prop Purify pa
r1) (Purify pb -> pb
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 = [Thunk] -> [Thunk] -> (pb -> IO ()) -> Purify pb
forall p a.
Propagator p a =>
[Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p
new ((Purify pa -> Thunk) -> [Purify pa] -> [Thunk]
forall a b. (a -> b) -> [a] -> [b]
map Purify pa -> Thunk
forall p. Purify p -> Thunk
pre [Purify pa]
rs) ((Purify pa -> Thunk) -> [Purify pa] -> [Thunk]
forall a b. (a -> b) -> [a] -> [b]
map Purify pa -> Thunk
forall p. Purify p -> Thunk
post [Purify pa]
rs) ((pb -> IO ()) -> Purify pb) -> (pb -> IO ()) -> Purify pb
forall a b. (a -> b) -> a -> b
$ \pb
p -> do
    [pa] -> pb -> IO ()
def ((Purify pa -> pa) -> [Purify pa] -> [pa]
forall a b. (a -> b) -> [a] -> [b]
map Purify pa -> pa
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 = IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$ do
    Thunk -> IO ()
force (Purify pa -> Thunk
forall p. Purify p -> Thunk
pre Purify pa
r)
    Thunk -> IO ()
force (Purify pa -> Thunk
forall p. Purify p -> Thunk
post Purify pa
r)
    pa -> IO a
forall p x. Propagator p x => p -> IO x
readProp (Purify pa -> pa
forall p. Purify p -> p
prop Purify pa
r)