{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-|
Copyright: © 2021-2023 IOHK, 2024 Cardano Foundation
License: Apache-2.0

Embeddings of delta types.
-}
module Data.Delta.Embedding (
    -- $Embedding
      Embedding
    , Embedding' (..)
    , mkEmbedding
    , fromEmbedding
    , pair
    , liftUpdates
    , replaceFromApply

    -- * Internal
    , inject
    , project
    ) where

import Prelude

import Control.Exception
    ( SomeException
    )
import Data.Delta.Core
    ( Delta (..)
    , Replace (..)
    )
import Data.Delta.Embedding.Internal
    ( Machine (..)
    , fromState
    , pairMachine
    )
import Data.Either
    ( fromRight
    )
import Data.Semigroupoid
    ( Semigroupoid (..)
    )

{-------------------------------------------------------------------------------
    Embedding
-------------------------------------------------------------------------------}
{- $Embedding
#doc:Embedding#

An 'Embedding'@ da db@ embeds one type and its delta type @da@
into another type and its delta type @db@.

For reasons of efficiency, 'Embedding' is an abstract type.
It is constructed using the 'Embedding'' type, which has
three components.

* 'write' embeds values from the type @a = 'Base' da@
    into the type @b = 'Base' db@.
* 'load' attempts to retrieve the value of type @a@
    from the type @b@, but does not necessarily succeed.
* 'update' maps a delta type @da@ to a delta type @db@.
    For this mapping, both the value of type @a@ and a corresponding
    value of type @b@ are provided;
    the delta types @da@ and @db@ are relative to these values.
    In the definition of 'update', we can assume that @Right a = load b@.

The embedding of one type into the other is characterized by the following
properties:

* The embedding is __not necessarily surjective__:
    The type @b@ may contain many values that do not correspond to
    a value of type @a@. Hence, 'load' has an 'Either' result.
    (See Note [EitherSomeException] for the choice of exception type.)
    However, retrieving a written value always succeeds, we have

        prop> load . write = Right

* The embedding is __redundant__:
    The type @b@ may contain multiple values that correspond to
    one and the same @a@.
    This is why the 'update' function expects the type @b@ as argument,
    so that the right deltas can be computed.
    Put differently, we often have

        prop> write a ≠ b   where Right a = load b

* The embedding of a delta __commutes with 'apply'__.
    We have

        > Right (apply da a) = load (apply (update a b da) b)
        >     where Right a = load b

    However, since the embedding is redundant, we often have

        prop> apply (update a (write a) da) (write a) ≠ write (apply da a)
-}

-- | Specification of an embedding of a type @a@ with delta types @da@
-- into the type @b@ with delta type @db@.
-- See [the discussion of @Embedding@](#doc:Embedding)
-- for a more detailed description.
data Embedding' da db where
    Embedding'
        :: (Delta da, Delta db, a ~ Base da, b ~ Base db) =>
        { ()
load   :: b -> Either SomeException a
        , ()
write  :: a -> b
        , ()
update :: a -> b -> da -> db
        } -> Embedding' da db

-- | 'Embedding' with efficient composition 'o'.
-- To construct an embedding, use 'mkEmbedding'.
data Embedding da db = Embedding
    { forall da db. Embedding da db -> Base da -> Machine da db
inject  :: Base da -> Machine da db
    , forall da db.
Embedding da db
-> Base db -> Either SomeException (Base da, Machine da db)
project :: Base db -> Either SomeException (Base da, Machine da db)
    }

-- | Construct 'Embedding' with efficient composition
mkEmbedding :: Embedding' da db -> Embedding da db
mkEmbedding :: forall da db. Embedding' da db -> Embedding da db
mkEmbedding Embedding'{b -> Either SomeException a
load :: ()
load :: b -> Either SomeException a
load,a -> b
write :: ()
write :: a -> b
write,a -> b -> da -> db
update :: ()
update :: a -> b -> da -> db
update} = Embedding
    { inject :: Base da -> Machine da db
inject = b -> Machine da db
start (b -> Machine da db) -> (a -> b) -> a -> Machine da db
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
write
    , project :: Base db -> Either SomeException (Base da, Machine da db)
project = \Base db
b -> (, b -> Machine da db
start b
Base db
b) (a -> (a, Machine da db))
-> Either SomeException a
-> Either SomeException (a, Machine da db)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> Either SomeException a
load b
Base db
b
    }
  where
    start :: b -> Machine da db
start b
b = ((Base da, da) -> (Base db, ()) -> (db, ()))
-> (Base db, ()) -> Machine da db
forall db da s.
Delta db =>
((Base da, da) -> (Base db, s) -> (db, s))
-> (Base db, s) -> Machine da db
fromState (a, da) -> (b, ()) -> (db, ())
(Base da, da) -> (Base db, ()) -> (db, ())
step (b
Base db
b,())
    step :: (a, da) -> (b, ()) -> (db, ())
step (a
a,da
da) (b
b,()
_) = (a -> b -> da -> db
update a
a b
b da
da, ())

-- | Extract 'load', 'write', and 'update' functions
-- from an efficient 'Embedding'.
fromEmbedding :: (Delta da, Delta db) => Embedding da db -> Embedding' da db
fromEmbedding :: forall da db.
(Delta da, Delta db) =>
Embedding da db -> Embedding' da db
fromEmbedding Embedding{Base da -> Machine da db
inject :: forall da db. Embedding da db -> Base da -> Machine da db
inject :: Base da -> Machine da db
inject,Base db -> Either SomeException (Base da, Machine da db)
project :: forall da db.
Embedding da db
-> Base db -> Either SomeException (Base da, Machine da db)
project :: Base db -> Either SomeException (Base da, Machine da db)
project} = Embedding'
    { load :: Base db -> Either SomeException (Base da)
load = ((Base da, Machine da db) -> Base da)
-> Either SomeException (Base da, Machine da db)
-> Either SomeException (Base da)
forall a b.
(a -> b) -> Either SomeException a -> Either SomeException b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Base da, Machine da db) -> Base da
forall a b. (a, b) -> a
fst (Either SomeException (Base da, Machine da db)
 -> Either SomeException (Base da))
-> (Base db -> Either SomeException (Base da, Machine da db))
-> Base db
-> Either SomeException (Base da)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Base db -> Either SomeException (Base da, Machine da db)
project
    , write :: Base da -> Base db
write = Machine da db -> Base db
forall da db. Machine da db -> Base db
state_ (Machine da db -> Base db)
-> (Base da -> Machine da db) -> Base da -> Base db
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Base da -> Machine da db
inject
    , update :: Base da -> Base db -> da -> db
update = \Base da
a Base db
b da
da ->
        let (Base da
_ ,Machine da db
mab) = Either SomeException (Base da, Machine da db)
-> (Base da, Machine da db)
forall {a} {b}. Either a b -> b
from (Base db -> Either SomeException (Base da, Machine da db)
project Base db
b)
            (db
db,Machine da db
_  ) = Machine da db -> (Base da, da) -> (db, Machine da db)
forall da db. Machine da db -> (Base da, da) -> (db, Machine da db)
step_ Machine da db
mab (Base da
a,da
da)
        in  db
db
    }
  where
    from :: Either a b -> b
from = b -> Either a b -> b
forall b a. b -> Either a b -> b
fromRight ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"Embedding: 'load' violates expected laws")

-- | Efficient composition of 'Embedding'
instance Semigroupoid Embedding where
    (Embedding Base j -> Machine j k1
inject2 Base k1 -> Either SomeException (Base j, Machine j k1)
project2) o :: forall j k1 i. Embedding j k1 -> Embedding i j -> Embedding i k1
`o` (Embedding Base i -> Machine i j
inject1 Base j -> Either SomeException (Base i, Machine i j)
project1) =
        Embedding{Base i -> Machine i k1
inject :: Base i -> Machine i k1
inject :: Base i -> Machine i k1
inject,Base k1 -> Either SomeException (Base i, Machine i k1)
project :: Base k1 -> Either SomeException (Base i, Machine i k1)
project :: Base k1 -> Either SomeException (Base i, Machine i k1)
project}
      where
        inject :: Base i -> Machine i k1
inject Base i
a =
            let mab :: Machine i j
mab = Base i -> Machine i j
inject1 Base i
a
                mbc :: Machine j k1
mbc = Base j -> Machine j k1
inject2 (Machine i j -> Base j
forall da db. Machine da db -> Base db
state_ Machine i j
mab)
            in  Machine j k1
mbc Machine j k1 -> Machine i j -> Machine i k1
forall j k1 i. Machine j k1 -> Machine i j -> Machine i k1
forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
`o` Machine i j
mab
        project :: Base k1 -> Either SomeException (Base i, Machine i k1)
project Base k1
c = do
            (Base j
b, Machine j k1
mbc) <- Base k1 -> Either SomeException (Base j, Machine j k1)
project2 Base k1
c
            (Base i
a, Machine i j
mab) <- Base j -> Either SomeException (Base i, Machine i j)
project1 Base j
b
            (Base i, Machine i k1)
-> Either SomeException (Base i, Machine i k1)
forall a. a -> Either SomeException a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Base i
a, Machine j k1
mbc Machine j k1 -> Machine i j -> Machine i k1
forall j k1 i. Machine j k1 -> Machine i j -> Machine i k1
forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
`o` Machine i j
mab)

-- | A pair of 'Embedding's gives an embedding of pairs.
pair :: Embedding da1 db1 -> Embedding da2 db2 -> Embedding (da1,da2) (db1,db2)
pair :: forall da1 db1 da2 db2.
Embedding da1 db1
-> Embedding da2 db2 -> Embedding (da1, da2) (db1, db2)
pair (Embedding Base da1 -> Machine da1 db1
inject1 Base db1 -> Either SomeException (Base da1, Machine da1 db1)
project1) (Embedding Base da2 -> Machine da2 db2
inject2 Base db2 -> Either SomeException (Base da2, Machine da2 db2)
project2) =
    Embedding{(Base da1, Base da2) -> Machine (da1, da2) (db1, db2)
Base (da1, da2) -> Machine (da1, da2) (db1, db2)
inject :: Base (da1, da2) -> Machine (da1, da2) (db1, db2)
inject :: (Base da1, Base da2) -> Machine (da1, da2) (db1, db2)
inject,(Base db1, Base db2)
-> Either
     SomeException ((Base da1, Base da2), Machine (da1, da2) (db1, db2))
Base (db1, db2)
-> Either
     SomeException (Base (da1, da2), Machine (da1, da2) (db1, db2))
project :: Base (db1, db2)
-> Either
     SomeException (Base (da1, da2), Machine (da1, da2) (db1, db2))
project :: (Base db1, Base db2)
-> Either
     SomeException ((Base da1, Base da2), Machine (da1, da2) (db1, db2))
project}
  where
    inject :: (Base da1, Base da2) -> Machine (da1, da2) (db1, db2)
inject (Base da1
a1,Base da2
a2) = Machine da1 db1 -> Machine da2 db2 -> Machine (da1, da2) (db1, db2)
forall da1 db1 da2 db2.
Machine da1 db1 -> Machine da2 db2 -> Machine (da1, da2) (db1, db2)
pairMachine (Base da1 -> Machine da1 db1
inject1 Base da1
a1) (Base da2 -> Machine da2 db2
inject2 Base da2
a2)
    project :: (Base db1, Base db2)
-> Either
     SomeException ((Base da1, Base da2), Machine (da1, da2) (db1, db2))
project (Base db1
b1,Base db2
b2) = do
        (Base da1
a1, Machine da1 db1
m1) <- Base db1 -> Either SomeException (Base da1, Machine da1 db1)
project1 Base db1
b1
        (Base da2
a2, Machine da2 db2
m2) <- Base db2 -> Either SomeException (Base da2, Machine da2 db2)
project2 Base db2
b2
        ((Base da1, Base da2), Machine (da1, da2) (db1, db2))
-> Either
     SomeException ((Base da1, Base da2), Machine (da1, da2) (db1, db2))
forall a. a -> Either SomeException a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Base da1
a1,Base da2
a2), Machine da1 db1 -> Machine da2 db2 -> Machine (da1, da2) (db1, db2)
forall da1 db1 da2 db2.
Machine da1 db1 -> Machine da2 db2 -> Machine (da1, da2) (db1, db2)
pairMachine Machine da1 db1
m1 Machine da2 db2
m2)

-- | Lift a sequence of updates through an 'Embedding'.
--
-- >   (b, dbs) = liftUpdates (mkEmbedding embedding') das a
-- > implies
-- >   load embedding' b = Right (apply das a)
-- >   b = apply dbs (write embedding' a)
liftUpdates
    :: Delta da
    => Embedding da db
    -> [da]
    -- ^ List of deltas to apply.
    -- The deltas are applied right-to-left; the 'head' is applied __last__.
    -> Base da
    -- ^ Base value to apply the deltas to.
    -> (Base db, [db])
    -- ^ (Final base value, updates that were applied ('head' is __last__)).
liftUpdates :: forall da db.
Delta da =>
Embedding da db -> [da] -> Base da -> (Base db, [db])
liftUpdates Embedding{Base da -> Machine da db
inject :: forall da db. Embedding da db -> Base da -> Machine da db
inject :: Base da -> Machine da db
inject} [da]
das0 Base da
a0 =
    let (Base db
b,[db]
dbs) = Machine da db -> Base da -> [da] -> (Base db, [db])
forall {delta} {a}.
Delta delta =>
Machine delta a -> Base delta -> [delta] -> (Base a, [a])
go (Base da -> Machine da db
inject Base da
a0) Base da
a0 ([da] -> [da]
forall a. [a] -> [a]
reverse [da]
das0) in (Base db
b, [db] -> [db]
forall a. [a] -> [a]
reverse [db]
dbs)
  where
    go :: Machine delta a -> Base delta -> [delta] -> (Base a, [a])
go Machine delta a
machine1 Base delta
_  [] = (Machine delta a -> Base a
forall da db. Machine da db -> Base db
state_ Machine delta a
machine1, [])
    go Machine delta a
machine1 !Base delta
a (delta
da:[delta]
das) = (Base a
b,a
dba -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
dbs)
      where
        (Base a
b ,[a]
dbs) = Machine delta a -> Base delta -> [delta] -> (Base a, [a])
go Machine delta a
machine2 (delta -> Base delta -> Base delta
forall delta. Delta delta => delta -> Base delta -> Base delta
apply delta
da Base delta
a) [delta]
das
        (a
db,Machine delta a
machine2) = Machine delta a -> (Base delta, delta) -> (a, Machine delta a)
forall da db. Machine da db -> (Base da, da) -> (db, Machine da db)
step_ Machine delta a
machine1 (Base delta
a,delta
da)

-- | Having an 'apply' function is equivalent to the existence
-- of a canonical embedding into the trivial 'Replace' delta type.
replaceFromApply :: (Delta da, a ~ Base da) => Embedding' da (Replace a)
replaceFromApply :: forall da a. (Delta da, a ~ Base da) => Embedding' da (Replace a)
replaceFromApply = Embedding'
    { load :: a -> Either SomeException a
load = a -> Either SomeException a
forall a b. b -> Either a b
Right
    , write :: a -> a
write = a -> a
forall a. a -> a
id
    , update :: a -> a -> da -> Replace a
update = \a
_ a
a da
da -> a -> Replace a
forall a. a -> Replace a
Replace (da -> Base da -> Base da
forall delta. Delta delta => delta -> Base delta -> Base delta
apply da
da a
Base da
a)
    }

{-
-- | Use the 'update' function of an 'Embedding' to convert
-- one delta type to another.
--
-- This function assumes that the 'Embedding' argument satisfies
-- @load = Just@ and @write = id@.
applyWithEmbedding
    :: (Delta db, a ~ Base db)
    => Embedding da db -> (da -> a -> a)
applyWithEmbedding e delta1 a = apply (update e a delta1) a
-}