{-# OPTIONS_HADDOCK not-home #-}

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

-- |
--
-- This module provides the 'R' data type, which wraps an imperative propagator (e.g. "Data.Recursive.Propagator.Naive") in a pure and (if done right) safe data structure.
--
-- The result of 'getR' is always a solution of the given equations, but for it
-- to be deterministic (and hence for this API to be safe), the following
-- should hold:
--
-- * The @a@ in @R a@ should be partially orderd ('Data.POrder.POrder')
-- * That partial order must respect equality on @a@
-- * It must have a bottom element 'Data.POrder.bottom' ('Data.POrder.Bottom').
-- * The function passed to 'defR1', 'defR2' etc. must be a monotonic function
--   between these partial orders.
--
-- If this does not hold, then the result of 'getR' may not be deterministic.
--
-- Termination depends on whether a soluiton can be found iteratively. This is
-- guaranteed if all partial orders involved satisfy the Ascending Chain Condition.

module Data.Recursive.R.Internal
    ( R
    , getR, getRDual
    , mkR, defR1, defR2, defRList
    )
where

import System.IO.Unsafe
import Control.Monad.ST
import Data.Monoid
import Data.Coerce

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

-- | A value of type @R a@ is a @a@, but defined using only specific operations
-- (which you will find in the corresponding module, e.g.
-- "Data.Recursive.Bool"), which allow recursive definitions.
--
-- You can use 'getR' to extract the value.
--
-- 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 R a = R (Prop a) Thunk

-- | Any value of type @a@ is also a value of type @r a@.
mkR :: HasPropagator a => a -> R a
mkR :: forall a. HasPropagator a => a -> R a
mkR a
x = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
    Prop a
p <- forall p x. Propagator p x => x -> IO p
newConstProp a
x
    Thunk
t <- IO Thunk
doneThunk
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Prop a -> Thunk -> R a
R Prop a
p Thunk
t)

newR :: HasPropagator a => (Prop a -> IO [Thunk]) -> R a
newR :: forall a. HasPropagator a => (Prop a -> IO [Thunk]) -> R a
newR Prop a -> IO [Thunk]
act = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
    Prop a
p <- forall p x. Propagator p x => IO p
newProp
    Thunk
t <- IO [Thunk] -> IO Thunk
thunk (Prop a -> IO [Thunk]
act Prop a
p)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Prop a -> Thunk -> R a
R Prop a
p Thunk
t)

-- | Defines a value of type @R b@ to be a function of the values of @R a@.
--
-- The action passed it should declare that relation to the underlying propagator.
--
-- The @Prop a@ propagator must only be used for reading values _from_.
defR1 :: (HasPropagator a, HasPropagator b) =>
    (Prop a -> Prop b -> IO ()) ->
    R a -> R b
defR1 :: forall a b.
(HasPropagator a, HasPropagator b) =>
(Prop a -> Prop b -> IO ()) -> R a -> R b
defR1 Prop a -> Prop b -> IO ()
def R a
r1 = forall a. HasPropagator a => (Prop a -> IO [Thunk]) -> R a
newR forall a b. (a -> b) -> a -> b
$ \Prop b
p -> do
    let R Prop a
p1 Thunk
t1 = R a
r1
    Prop a -> Prop b -> IO ()
def Prop a
p1 Prop b
p
    forall (f :: * -> *) a. Applicative f => a -> f a
pure [Thunk
t1]

-- | Defines a value of type @R c@ to be a function of the values of @R a@ and @R b@.
--
-- The action passed it should declare that relation to the underlying propagator.
--
-- The @Prop a@ and @Prop b@ propagators must only be used for reading values _from_.
defR2 :: (HasPropagator a, HasPropagator b, HasPropagator c) =>
    (Prop a -> Prop b -> Prop c -> IO ()) ->
    R a -> R b -> R c
defR2 :: forall a b c.
(HasPropagator a, HasPropagator b, HasPropagator c) =>
(Prop a -> Prop b -> Prop c -> IO ()) -> R a -> R b -> R c
defR2 Prop a -> Prop b -> Prop c -> IO ()
def R a
r1 R b
r2 = forall a. HasPropagator a => (Prop a -> IO [Thunk]) -> R a
newR forall a b. (a -> b) -> a -> b
$ \Prop c
p -> do
    let R Prop a
p1 Thunk
t1 = R a
r1
    let R Prop b
p2 Thunk
t2 = R b
r2
    Prop a -> Prop b -> Prop c -> IO ()
def Prop a
p1 Prop b
p2 Prop c
p
    forall (f :: * -> *) a. Applicative f => a -> f a
pure [Thunk
t1, Thunk
t2]

-- | Defines a value of type @R b@ to be a function of the values of a list of @R a@ values.
--
-- The action passed it should declare that relation to the underlying propagator.
--
-- The @Prop a@ propagators must only be used for reading values _from_.
defRList :: (HasPropagator a, HasPropagator b) =>
    ([Prop a] -> Prop b -> IO ()) ->
    [R a] -> R b
defRList :: forall a b.
(HasPropagator a, HasPropagator b) =>
([Prop a] -> Prop b -> IO ()) -> [R a] -> R b
defRList [Prop a] -> Prop b -> IO ()
def [R a]
rs = forall a. HasPropagator a => (Prop a -> IO [Thunk]) -> R a
newR forall a b. (a -> b) -> a -> b
$ \Prop b
p -> do
    [Prop a] -> Prop b -> IO ()
def [ Prop a
p' | R Prop a
p' Thunk
_ <- [R a]
rs] Prop b
p
    forall (f :: * -> *) a. Applicative f => a -> f a
pure [ Thunk
t | R Prop a
_ Thunk
t <- [R a]
rs]

-- | Extract the value from a @R a@. This must not be used when _defining_ that value.
getR :: HasPropagator a => R a -> a
getR :: forall a. HasPropagator a => R a -> a
getR (R Prop a
p Thunk
t) = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
    Thunk -> IO ()
force Thunk
t
    forall p x. Propagator p x => p -> IO x
readProp Prop a
p

-- | Convenience variant of 'getR' to also remove the 'Dual' newtype wrapper, mostly for use with "Data.Recursive.DualBool".
getRDual :: HasPropagator (Dual a) => R (Dual a) -> a
getRDual :: forall a. HasPropagator (Dual a) => R (Dual a) -> a
getRDual = forall a. Dual a -> a
getDual forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasPropagator a => R a -> a
getR