{-# LANGUAGE GADTs               #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE TypeOperators       #-}



--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi.Mutable
-- Copyright   :  (c) 2020 James Koppel
-- License     :  BSD3
--
-- Experimental module for mutable terms.
--
--------------------------------------------------------------------------------

module Data.Comp.Multi.Mutable (
    Label
  , Mut
  , HMut
  , Cell(..)

  , MutCxt
  , MutTerm
  ) where


import Control.Monad
import Control.Monad.IO.Class

import Data.IORef

import Data.Comp.Multi.Term
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.HTraversable

newtype Mut a = Mut { Mut a -> IO a
runMut :: IO a }
  deriving ( a -> Mut b -> Mut a
(a -> b) -> Mut a -> Mut b
(forall a b. (a -> b) -> Mut a -> Mut b)
-> (forall a b. a -> Mut b -> Mut a) -> Functor Mut
forall a b. a -> Mut b -> Mut a
forall a b. (a -> b) -> Mut a -> Mut b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Mut b -> Mut a
$c<$ :: forall a b. a -> Mut b -> Mut a
fmap :: (a -> b) -> Mut a -> Mut b
$cfmap :: forall a b. (a -> b) -> Mut a -> Mut b
Functor, Functor Mut
a -> Mut a
Functor Mut =>
(forall a. a -> Mut a)
-> (forall a b. Mut (a -> b) -> Mut a -> Mut b)
-> (forall a b c. (a -> b -> c) -> Mut a -> Mut b -> Mut c)
-> (forall a b. Mut a -> Mut b -> Mut b)
-> (forall a b. Mut a -> Mut b -> Mut a)
-> Applicative Mut
Mut a -> Mut b -> Mut b
Mut a -> Mut b -> Mut a
Mut (a -> b) -> Mut a -> Mut b
(a -> b -> c) -> Mut a -> Mut b -> Mut c
forall a. a -> Mut a
forall a b. Mut a -> Mut b -> Mut a
forall a b. Mut a -> Mut b -> Mut b
forall a b. Mut (a -> b) -> Mut a -> Mut b
forall a b c. (a -> b -> c) -> Mut a -> Mut b -> Mut c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Mut a -> Mut b -> Mut a
$c<* :: forall a b. Mut a -> Mut b -> Mut a
*> :: Mut a -> Mut b -> Mut b
$c*> :: forall a b. Mut a -> Mut b -> Mut b
liftA2 :: (a -> b -> c) -> Mut a -> Mut b -> Mut c
$cliftA2 :: forall a b c. (a -> b -> c) -> Mut a -> Mut b -> Mut c
<*> :: Mut (a -> b) -> Mut a -> Mut b
$c<*> :: forall a b. Mut (a -> b) -> Mut a -> Mut b
pure :: a -> Mut a
$cpure :: forall a. a -> Mut a
$cp1Applicative :: Functor Mut
Applicative, Applicative Mut
a -> Mut a
Applicative Mut =>
(forall a b. Mut a -> (a -> Mut b) -> Mut b)
-> (forall a b. Mut a -> Mut b -> Mut b)
-> (forall a. a -> Mut a)
-> Monad Mut
Mut a -> (a -> Mut b) -> Mut b
Mut a -> Mut b -> Mut b
forall a. a -> Mut a
forall a b. Mut a -> Mut b -> Mut b
forall a b. Mut a -> (a -> Mut b) -> Mut b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Mut a
$creturn :: forall a. a -> Mut a
>> :: Mut a -> Mut b -> Mut b
$c>> :: forall a b. Mut a -> Mut b -> Mut b
>>= :: Mut a -> (a -> Mut b) -> Mut b
$c>>= :: forall a b. Mut a -> (a -> Mut b) -> Mut b
$cp1Monad :: Applicative Mut
Monad )

instance MonadIO Mut where
  liftIO :: IO a -> Mut a
liftIO = IO a -> Mut a
forall a. IO a -> Mut a
Mut

type HMut = HMonad Mut

newtype HIORef g l = HIORef { HIORef g l -> IORef (g l)
unHIORef :: IORef (g l)}

type Label = Int
data Cell f g i = Cell { Cell f g i -> IORef (Maybe (E g))
parent :: IORef (Maybe (E g))
                       , Cell f g i -> f (HIORef g) i
elt    :: f (HIORef g) i
                       --, label  :: Label
                       }

type MutCxt h f = Cxt h (Cell f)
type MutTerm f = MutCxt NoHole f (K ())

ref :: (MonadIO m) => a -> m (IORef a)
ref :: a -> m (IORef a)
ref = IO (IORef a) -> m (IORef a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef a) -> m (IORef a))
-> (a -> IO (IORef a)) -> a -> m (IORef a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IO (IORef a)
forall a. a -> IO (IORef a)
newIORef

deref :: (MonadIO m) => IORef a -> m a
deref :: IORef a -> m a
deref = IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> (IORef a -> IO a) -> IORef a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef a -> IO a
forall a. IORef a -> IO a
readIORef

hderef :: (MonadIO m) => HIORef g i -> m (g i)
hderef :: HIORef g i -> m (g i)
hderef = IORef (g i) -> m (g i)
forall (m :: * -> *) a. MonadIO m => IORef a -> m a
deref (IORef (g i) -> m (g i))
-> (HIORef g i -> IORef (g i)) -> HIORef g i -> m (g i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HIORef g i -> IORef (g i)
forall (g :: * -> *) l. HIORef g l -> IORef (g l)
unHIORef

refify :: (MonadIO m, HTraversable f) => f e i -> m (f (HIORef e) i)
refify :: f e i -> m (f (HIORef e) i)
refify = NatM m e (HIORef e) -> NatM m (f e) (f (HIORef e))
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse ((IORef (e i) -> HIORef e i) -> m (IORef (e i)) -> m (HIORef e i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IORef (e i) -> HIORef e i
forall (g :: * -> *) l. IORef (g l) -> HIORef g l
HIORef (m (IORef (e i)) -> m (HIORef e i))
-> (e i -> m (IORef (e i))) -> e i -> m (HIORef e i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e i -> m (IORef (e i))
forall (m :: * -> *) a. MonadIO m => a -> m (IORef a)
ref)

(=:) :: (MonadIO m) => IORef a -> a -> m ()
=: :: IORef a -> a -> m ()
(=:) r :: IORef a
r x :: a
x = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
r a
x

isNothing :: Maybe a -> Bool
isNothing :: Maybe a -> Bool
isNothing Nothing = Bool
True
isNothing _ = Bool
False

htraverseMut :: (MonadIO m, HTraversable f) => NatM m a b -> f (HIORef a) i -> m (f b i)
htraverseMut :: NatM m a b -> f (HIORef a) i -> m (f b i)
htraverseMut f :: NatM m a b
f = NatM m (HIORef a) b -> NatM m (f (HIORef a)) (f b)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse (a i -> m (b i)
NatM m a b
f (a i -> m (b i))
-> (HIORef a i -> m (a i)) -> HIORef a i -> m (b i)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< HIORef a i -> m (a i)
forall (m :: * -> *) (g :: * -> *) i.
MonadIO m =>
HIORef g i -> m (g i)
hderef)

setChildren :: (HTraversable f) => MutTerm f i -> Mut ()
setChildren :: MutTerm f i -> Mut ()
setChildren t :: MutTerm f i
t@(Term (Cell {elt :: forall (f :: (* -> *) -> * -> *) (g :: * -> *) i.
Cell f g i -> f (HIORef g) i
elt=f (HIORef (Cxt NoHole (Cell f) (K ()))) i
elt})) = do
  NatM Mut (Cxt NoHole (Cell f) (K ())) (K ())
-> f (HIORef (Cxt NoHole (Cell f) (K ()))) i -> Mut (f (K ()) i)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) (a :: * -> *)
       (b :: * -> *) i.
(MonadIO m, HTraversable f) =>
NatM m a b -> f (HIORef a) i -> m (f b i)
htraverseMut (\(Term (Cell {parent=parPtr})) -> do Maybe (E (Cxt NoHole (Cell f) (K ())))
curPar <- IORef (Maybe (E (Cxt NoHole (Cell f) (K ()))))
-> Mut (Maybe (E (Cxt NoHole (Cell f) (K ()))))
forall (m :: * -> *) a. MonadIO m => IORef a -> m a
deref IORef (Maybe (E (Cxt NoHole (Cell f) (K ()))))
parPtr
                                                   --  assert (isNothing curPar) (return ())
                                                     IORef (Maybe (E (Cxt NoHole (Cell f) (K ()))))
parPtr IORef (Maybe (E (Cxt NoHole (Cell f) (K ()))))
-> Maybe (E (Cxt NoHole (Cell f) (K ()))) -> Mut ()
forall (m :: * -> *) a. MonadIO m => IORef a -> a -> m ()
=: E (Cxt NoHole (Cell f) (K ()))
-> Maybe (E (Cxt NoHole (Cell f) (K ())))
forall a. a -> Maybe a
Just (MutTerm f i -> E (Cxt NoHole (Cell f) (K ()))
forall (f :: * -> *) i. f i -> E f
E MutTerm f i
t)
                                                     K () i -> Mut (K () i)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> K () i
forall a i. a -> K a i
K ()))
    f (HIORef (Cxt NoHole (Cell f) (K ()))) i
elt
  () -> Mut ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()


mkCell' :: (HTraversable f) => f (HIORef (MutTerm f)) i -> Mut (MutTerm f i)
mkCell' :: f (HIORef (MutTerm f)) i -> Mut (MutTerm f i)
mkCell' t :: f (HIORef (MutTerm f)) i
t = do
  IORef (Maybe (E (MutTerm f)))
parPtr <- Maybe (E (MutTerm f)) -> Mut (IORef (Maybe (E (MutTerm f))))
forall (m :: * -> *) a. MonadIO m => a -> m (IORef a)
ref Maybe (E (MutTerm f))
forall a. Maybe a
Nothing
  let cell :: MutTerm f i
cell = Cell f (MutTerm f) i -> MutTerm f i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (Cell f (MutTerm f) i -> MutTerm f i)
-> Cell f (MutTerm f) i -> MutTerm f i
forall a b. (a -> b) -> a -> b
$ Cell :: forall (f :: (* -> *) -> * -> *) (g :: * -> *) i.
IORef (Maybe (E g)) -> f (HIORef g) i -> Cell f g i
Cell { elt :: f (HIORef (MutTerm f)) i
elt=f (HIORef (MutTerm f)) i
t, parent :: IORef (Maybe (E (MutTerm f)))
parent=IORef (Maybe (E (MutTerm f)))
parPtr }
  MutTerm f i -> Mut ()
forall (f :: (* -> *) -> * -> *) i.
HTraversable f =>
MutTerm f i -> Mut ()
setChildren MutTerm f i
cell
  MutTerm f i -> Mut (MutTerm f i)
forall (m :: * -> *) a. Monad m => a -> m a
return MutTerm f i
cell

mkCell :: (HTraversable f) => f (MutTerm f) i -> Mut (MutTerm f i)
mkCell :: f (MutTerm f) i -> Mut (MutTerm f i)
mkCell = f (HIORef (MutTerm f)) i -> Mut (MutTerm f i)
forall (f :: (* -> *) -> * -> *) i.
HTraversable f =>
f (HIORef (MutTerm f)) i -> Mut (MutTerm f i)
mkCell' (f (HIORef (MutTerm f)) i -> Mut (MutTerm f i))
-> (f (MutTerm f) i -> Mut (f (HIORef (MutTerm f)) i))
-> f (MutTerm f) i
-> Mut (MutTerm f i)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< f (MutTerm f) i -> Mut (f (HIORef (MutTerm f)) i)
forall (m :: * -> *) (f :: (* -> *) -> * -> *) (e :: * -> *) i.
(MonadIO m, HTraversable f) =>
f e i -> m (f (HIORef e) i)
refify