{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{- HLINT ignore "Use newtype instead of data" -}
module Data.Delta (
    -- * Synopsis
    -- | Delta encodings.
    --
    -- The type constraint 'Delta'@ delta@ means that the type @delta@
    -- is a delta encoding of the corresponding base type 'Base'@ delta@.
    --
    -- Delta encodings can be transformed into each other using an 'Embedding'.

    -- * Delta encodings
    Delta (..)
    , NoChange (..), Replace (..)
    , DeltaList (..)
    , DeltaSet1 (..)
    , DeltaSet, mkDeltaSet, deltaSetToList, deltaSetFromList

    -- * Embedding of types and delta encodings
    -- $Embedding
    , Embedding
    , module Data.Semigroupoid
    , Embedding' (..), mkEmbedding
    , fromEmbedding, pair, liftUpdates
    , replaceFromApply

    -- * Internal
    , inject, project, Machine (..), idle, pairMachine, fromState,
    ) where

import Prelude

import Control.Exception
    ( SomeException )
import Data.Either
    ( fromRight )
import Data.Kind
    ( Type )
import Data.List.NonEmpty
    ( NonEmpty )
import Data.Semigroupoid
    ( Semigroupoid (..) )
import Data.Set
    ( Set )

import qualified Data.Set as Set

{-------------------------------------------------------------------------------
    Delta encodings
-------------------------------------------------------------------------------}
-- | Type class for delta encodings.
class Delta delta where
    -- | Base type for which @delta@ represents a delta encoding.
    -- This is implemented as a type family, so that we can have
    -- multiple delta encodings for the same base type.
    --
    -- FIXME: Better name for 'Base'? It's sooo generic.
    -- Pier, dock, ground, anchor, site, …
    type Base delta :: Type
    -- | Apply a delta encoding to the base type.
    apply :: delta -> Base delta -> Base delta

-- | Trivial delta encoding for the type @a@ that admits no change at all.
data NoChange a = NoChange
    deriving (NoChange a -> NoChange a -> Bool
(NoChange a -> NoChange a -> Bool)
-> (NoChange a -> NoChange a -> Bool) -> Eq (NoChange a)
forall a. NoChange a -> NoChange a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NoChange a -> NoChange a -> Bool
$c/= :: forall a. NoChange a -> NoChange a -> Bool
== :: NoChange a -> NoChange a -> Bool
$c== :: forall a. NoChange a -> NoChange a -> Bool
Eq, Eq (NoChange a)
Eq (NoChange a)
-> (NoChange a -> NoChange a -> Ordering)
-> (NoChange a -> NoChange a -> Bool)
-> (NoChange a -> NoChange a -> Bool)
-> (NoChange a -> NoChange a -> Bool)
-> (NoChange a -> NoChange a -> Bool)
-> (NoChange a -> NoChange a -> NoChange a)
-> (NoChange a -> NoChange a -> NoChange a)
-> Ord (NoChange a)
NoChange a -> NoChange a -> Bool
NoChange a -> NoChange a -> Ordering
NoChange a -> NoChange a -> NoChange a
forall a. Eq (NoChange a)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. NoChange a -> NoChange a -> Bool
forall a. NoChange a -> NoChange a -> Ordering
forall a. NoChange a -> NoChange a -> NoChange a
min :: NoChange a -> NoChange a -> NoChange a
$cmin :: forall a. NoChange a -> NoChange a -> NoChange a
max :: NoChange a -> NoChange a -> NoChange a
$cmax :: forall a. NoChange a -> NoChange a -> NoChange a
>= :: NoChange a -> NoChange a -> Bool
$c>= :: forall a. NoChange a -> NoChange a -> Bool
> :: NoChange a -> NoChange a -> Bool
$c> :: forall a. NoChange a -> NoChange a -> Bool
<= :: NoChange a -> NoChange a -> Bool
$c<= :: forall a. NoChange a -> NoChange a -> Bool
< :: NoChange a -> NoChange a -> Bool
$c< :: forall a. NoChange a -> NoChange a -> Bool
compare :: NoChange a -> NoChange a -> Ordering
$ccompare :: forall a. NoChange a -> NoChange a -> Ordering
$cp1Ord :: forall a. Eq (NoChange a)
Ord, Int -> NoChange a -> ShowS
[NoChange a] -> ShowS
NoChange a -> String
(Int -> NoChange a -> ShowS)
-> (NoChange a -> String)
-> ([NoChange a] -> ShowS)
-> Show (NoChange a)
forall a. Int -> NoChange a -> ShowS
forall a. [NoChange a] -> ShowS
forall a. NoChange a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NoChange a] -> ShowS
$cshowList :: forall a. [NoChange a] -> ShowS
show :: NoChange a -> String
$cshow :: forall a. NoChange a -> String
showsPrec :: Int -> NoChange a -> ShowS
$cshowsPrec :: forall a. Int -> NoChange a -> ShowS
Show)

instance Delta (NoChange a) where
    type Base (NoChange a) = a
    apply :: NoChange a -> Base (NoChange a) -> Base (NoChange a)
apply NoChange a
_ Base (NoChange a)
a = Base (NoChange a)
a

-- | Trivial delta encoding for the type @a@ that replaces the value wholesale.
newtype Replace a = Replace a
    deriving (Replace a -> Replace a -> Bool
(Replace a -> Replace a -> Bool)
-> (Replace a -> Replace a -> Bool) -> Eq (Replace a)
forall a. Eq a => Replace a -> Replace a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Replace a -> Replace a -> Bool
$c/= :: forall a. Eq a => Replace a -> Replace a -> Bool
== :: Replace a -> Replace a -> Bool
$c== :: forall a. Eq a => Replace a -> Replace a -> Bool
Eq, Eq (Replace a)
Eq (Replace a)
-> (Replace a -> Replace a -> Ordering)
-> (Replace a -> Replace a -> Bool)
-> (Replace a -> Replace a -> Bool)
-> (Replace a -> Replace a -> Bool)
-> (Replace a -> Replace a -> Bool)
-> (Replace a -> Replace a -> Replace a)
-> (Replace a -> Replace a -> Replace a)
-> Ord (Replace a)
Replace a -> Replace a -> Bool
Replace a -> Replace a -> Ordering
Replace a -> Replace a -> Replace a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Replace a)
forall a. Ord a => Replace a -> Replace a -> Bool
forall a. Ord a => Replace a -> Replace a -> Ordering
forall a. Ord a => Replace a -> Replace a -> Replace a
min :: Replace a -> Replace a -> Replace a
$cmin :: forall a. Ord a => Replace a -> Replace a -> Replace a
max :: Replace a -> Replace a -> Replace a
$cmax :: forall a. Ord a => Replace a -> Replace a -> Replace a
>= :: Replace a -> Replace a -> Bool
$c>= :: forall a. Ord a => Replace a -> Replace a -> Bool
> :: Replace a -> Replace a -> Bool
$c> :: forall a. Ord a => Replace a -> Replace a -> Bool
<= :: Replace a -> Replace a -> Bool
$c<= :: forall a. Ord a => Replace a -> Replace a -> Bool
< :: Replace a -> Replace a -> Bool
$c< :: forall a. Ord a => Replace a -> Replace a -> Bool
compare :: Replace a -> Replace a -> Ordering
$ccompare :: forall a. Ord a => Replace a -> Replace a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Replace a)
Ord, Int -> Replace a -> ShowS
[Replace a] -> ShowS
Replace a -> String
(Int -> Replace a -> ShowS)
-> (Replace a -> String)
-> ([Replace a] -> ShowS)
-> Show (Replace a)
forall a. Show a => Int -> Replace a -> ShowS
forall a. Show a => [Replace a] -> ShowS
forall a. Show a => Replace a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Replace a] -> ShowS
$cshowList :: forall a. Show a => [Replace a] -> ShowS
show :: Replace a -> String
$cshow :: forall a. Show a => Replace a -> String
showsPrec :: Int -> Replace a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Replace a -> ShowS
Show)

instance Delta (Replace a) where
    type Base (Replace a) = a
    apply :: Replace a -> Base (Replace a) -> Base (Replace a)
apply (Replace a
a) Base (Replace a)
_ = a
Base (Replace a)
a

-- | Combine replacements. The first argument takes precedence.
-- In this way, 'apply' becomes a 'Semigroup' morphism.
instance Semigroup (Replace a) where
    Replace a
r <> :: Replace a -> Replace a -> Replace a
<> Replace a
_ = Replace a
r

-- | A delta can be optionally applied.
instance Delta delta => Delta (Maybe delta) where
    type Base (Maybe delta) = Base delta
    apply :: Maybe delta -> Base (Maybe delta) -> Base (Maybe delta)
apply = (Base delta -> Base delta)
-> (delta -> Base delta -> Base delta)
-> Maybe delta
-> Base delta
-> Base delta
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Base delta -> Base delta
forall a. a -> a
id delta -> Base delta -> Base delta
forall delta. Delta delta => delta -> Base delta -> Base delta
apply

-- | A list of deltas can be applied like a single delta.
-- This overloading of 'apply' is very convenient.
--
-- Order is important: The 'head' of the list is applied __last__.
-- This way, we have a morphism to the 'Endo' 'Monoid':
--
-- > apply []         = id
-- > apply (d1 <> d2) = apply d1 . apply d2
instance Delta delta => Delta [delta] where
    type Base [delta] = Base delta
    apply :: [delta] -> Base [delta] -> Base [delta]
apply [delta]
ds Base [delta]
a = (delta -> Base delta -> Base delta)
-> Base delta -> [delta] -> Base delta
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr delta -> Base delta -> Base delta
forall delta. Delta delta => delta -> Base delta -> Base delta
apply Base delta
Base [delta]
a [delta]
ds

-- | For convenience, a nonempty list of deltas
-- can be applied like a list of deltas.
instance Delta delta => Delta (NonEmpty delta) where
    type Base (NonEmpty delta) = Base delta
    apply :: NonEmpty delta -> Base (NonEmpty delta) -> Base (NonEmpty delta)
apply NonEmpty delta
ds Base (NonEmpty delta)
a = (delta -> Base delta -> Base delta)
-> Base delta -> NonEmpty delta -> Base delta
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr delta -> Base delta -> Base delta
forall delta. Delta delta => delta -> Base delta -> Base delta
apply Base delta
Base (NonEmpty delta)
a NonEmpty delta
ds

-- | A pair of deltas represents a delta for a pair.
instance (Delta d1, Delta d2) => Delta (d1,d2) where
    type Base (d1, d2) = (Base d1, Base d2)
    apply :: (d1, d2) -> Base (d1, d2) -> Base (d1, d2)
apply (d1
d1,d2
d2) (a1,a2) = (d1 -> Base d1 -> Base d1
forall delta. Delta delta => delta -> Base delta -> Base delta
apply d1
d1 Base d1
a1, d2 -> Base d2 -> Base d2
forall delta. Delta delta => delta -> Base delta -> Base delta
apply d2
d2 Base d2
a2)

-- | A triple of deltas represents a delta for a triple.
instance (Delta d1, Delta d2, Delta d3) => Delta (d1,d2,d3) where
    type Base (d1,d2,d3) = (Base d1,Base d2,Base d3)
    apply :: (d1, d2, d3) -> Base (d1, d2, d3) -> Base (d1, d2, d3)
apply (d1
d1,d2
d2,d3
d3) (a1,a2,a3) = (d1 -> Base d1 -> Base d1
forall delta. Delta delta => delta -> Base delta -> Base delta
apply d1
d1 Base d1
a1, d2 -> Base d2 -> Base d2
forall delta. Delta delta => delta -> Base delta -> Base delta
apply d2
d2 Base d2
a2, d3 -> Base d3 -> Base d3
forall delta. Delta delta => delta -> Base delta -> Base delta
apply d3
d3 Base d3
a3)

-- | A 4-tuple of deltas represents a delta for a 4-tuple.
instance (Delta d1, Delta d2, Delta d3, Delta d4) => Delta (d1,d2,d3,d4) where
    type Base (d1,d2,d3,d4) = (Base d1,Base d2,Base d3,Base d4)
    apply :: (d1, d2, d3, d4) -> Base (d1, d2, d3, d4) -> Base (d1, d2, d3, d4)
apply (d1
d1,d2
d2,d3
d3,d4
d4) (a1,a2,a3,a4) =
        (d1 -> Base d1 -> Base d1
forall delta. Delta delta => delta -> Base delta -> Base delta
apply d1
d1 Base d1
a1, d2 -> Base d2 -> Base d2
forall delta. Delta delta => delta -> Base delta -> Base delta
apply d2
d2 Base d2
a2, d3 -> Base d3 -> Base d3
forall delta. Delta delta => delta -> Base delta -> Base delta
apply d3
d3 Base d3
a3, d4 -> Base d4 -> Base d4
forall delta. Delta delta => delta -> Base delta -> Base delta
apply d4
d4 Base d4
a4)

-- | Delta encoding for lists where a list of elements is prepended.
data DeltaList a = Append [a]
    deriving (DeltaList a -> DeltaList a -> Bool
(DeltaList a -> DeltaList a -> Bool)
-> (DeltaList a -> DeltaList a -> Bool) -> Eq (DeltaList a)
forall a. Eq a => DeltaList a -> DeltaList a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DeltaList a -> DeltaList a -> Bool
$c/= :: forall a. Eq a => DeltaList a -> DeltaList a -> Bool
== :: DeltaList a -> DeltaList a -> Bool
$c== :: forall a. Eq a => DeltaList a -> DeltaList a -> Bool
Eq, Eq (DeltaList a)
Eq (DeltaList a)
-> (DeltaList a -> DeltaList a -> Ordering)
-> (DeltaList a -> DeltaList a -> Bool)
-> (DeltaList a -> DeltaList a -> Bool)
-> (DeltaList a -> DeltaList a -> Bool)
-> (DeltaList a -> DeltaList a -> Bool)
-> (DeltaList a -> DeltaList a -> DeltaList a)
-> (DeltaList a -> DeltaList a -> DeltaList a)
-> Ord (DeltaList a)
DeltaList a -> DeltaList a -> Bool
DeltaList a -> DeltaList a -> Ordering
DeltaList a -> DeltaList a -> DeltaList a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (DeltaList a)
forall a. Ord a => DeltaList a -> DeltaList a -> Bool
forall a. Ord a => DeltaList a -> DeltaList a -> Ordering
forall a. Ord a => DeltaList a -> DeltaList a -> DeltaList a
min :: DeltaList a -> DeltaList a -> DeltaList a
$cmin :: forall a. Ord a => DeltaList a -> DeltaList a -> DeltaList a
max :: DeltaList a -> DeltaList a -> DeltaList a
$cmax :: forall a. Ord a => DeltaList a -> DeltaList a -> DeltaList a
>= :: DeltaList a -> DeltaList a -> Bool
$c>= :: forall a. Ord a => DeltaList a -> DeltaList a -> Bool
> :: DeltaList a -> DeltaList a -> Bool
$c> :: forall a. Ord a => DeltaList a -> DeltaList a -> Bool
<= :: DeltaList a -> DeltaList a -> Bool
$c<= :: forall a. Ord a => DeltaList a -> DeltaList a -> Bool
< :: DeltaList a -> DeltaList a -> Bool
$c< :: forall a. Ord a => DeltaList a -> DeltaList a -> Bool
compare :: DeltaList a -> DeltaList a -> Ordering
$ccompare :: forall a. Ord a => DeltaList a -> DeltaList a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (DeltaList a)
Ord, Int -> DeltaList a -> ShowS
[DeltaList a] -> ShowS
DeltaList a -> String
(Int -> DeltaList a -> ShowS)
-> (DeltaList a -> String)
-> ([DeltaList a] -> ShowS)
-> Show (DeltaList a)
forall a. Show a => Int -> DeltaList a -> ShowS
forall a. Show a => [DeltaList a] -> ShowS
forall a. Show a => DeltaList a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DeltaList a] -> ShowS
$cshowList :: forall a. Show a => [DeltaList a] -> ShowS
show :: DeltaList a -> String
$cshow :: forall a. Show a => DeltaList a -> String
showsPrec :: Int -> DeltaList a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DeltaList a -> ShowS
Show)

instance Delta (DeltaList a) where
    type Base (DeltaList a) = [a]
    apply :: DeltaList a -> Base (DeltaList a) -> Base (DeltaList a)
apply (Append [a]
xs) Base (DeltaList a)
ys = [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
Base (DeltaList a)
ys

-- | Delta encoding for 'Set' where a single element is deleted or added.
data DeltaSet1 a = Insert a | Delete a
    deriving (DeltaSet1 a -> DeltaSet1 a -> Bool
(DeltaSet1 a -> DeltaSet1 a -> Bool)
-> (DeltaSet1 a -> DeltaSet1 a -> Bool) -> Eq (DeltaSet1 a)
forall a. Eq a => DeltaSet1 a -> DeltaSet1 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DeltaSet1 a -> DeltaSet1 a -> Bool
$c/= :: forall a. Eq a => DeltaSet1 a -> DeltaSet1 a -> Bool
== :: DeltaSet1 a -> DeltaSet1 a -> Bool
$c== :: forall a. Eq a => DeltaSet1 a -> DeltaSet1 a -> Bool
Eq, Eq (DeltaSet1 a)
Eq (DeltaSet1 a)
-> (DeltaSet1 a -> DeltaSet1 a -> Ordering)
-> (DeltaSet1 a -> DeltaSet1 a -> Bool)
-> (DeltaSet1 a -> DeltaSet1 a -> Bool)
-> (DeltaSet1 a -> DeltaSet1 a -> Bool)
-> (DeltaSet1 a -> DeltaSet1 a -> Bool)
-> (DeltaSet1 a -> DeltaSet1 a -> DeltaSet1 a)
-> (DeltaSet1 a -> DeltaSet1 a -> DeltaSet1 a)
-> Ord (DeltaSet1 a)
DeltaSet1 a -> DeltaSet1 a -> Bool
DeltaSet1 a -> DeltaSet1 a -> Ordering
DeltaSet1 a -> DeltaSet1 a -> DeltaSet1 a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (DeltaSet1 a)
forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> Bool
forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> Ordering
forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> DeltaSet1 a
min :: DeltaSet1 a -> DeltaSet1 a -> DeltaSet1 a
$cmin :: forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> DeltaSet1 a
max :: DeltaSet1 a -> DeltaSet1 a -> DeltaSet1 a
$cmax :: forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> DeltaSet1 a
>= :: DeltaSet1 a -> DeltaSet1 a -> Bool
$c>= :: forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> Bool
> :: DeltaSet1 a -> DeltaSet1 a -> Bool
$c> :: forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> Bool
<= :: DeltaSet1 a -> DeltaSet1 a -> Bool
$c<= :: forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> Bool
< :: DeltaSet1 a -> DeltaSet1 a -> Bool
$c< :: forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> Bool
compare :: DeltaSet1 a -> DeltaSet1 a -> Ordering
$ccompare :: forall a. Ord a => DeltaSet1 a -> DeltaSet1 a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (DeltaSet1 a)
Ord, Int -> DeltaSet1 a -> ShowS
[DeltaSet1 a] -> ShowS
DeltaSet1 a -> String
(Int -> DeltaSet1 a -> ShowS)
-> (DeltaSet1 a -> String)
-> ([DeltaSet1 a] -> ShowS)
-> Show (DeltaSet1 a)
forall a. Show a => Int -> DeltaSet1 a -> ShowS
forall a. Show a => [DeltaSet1 a] -> ShowS
forall a. Show a => DeltaSet1 a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DeltaSet1 a] -> ShowS
$cshowList :: forall a. Show a => [DeltaSet1 a] -> ShowS
show :: DeltaSet1 a -> String
$cshow :: forall a. Show a => DeltaSet1 a -> String
showsPrec :: Int -> DeltaSet1 a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DeltaSet1 a -> ShowS
Show)

instance Ord a => Delta (DeltaSet1 a) where
    type Base (DeltaSet1 a) = Set a
    apply :: DeltaSet1 a -> Base (DeltaSet1 a) -> Base (DeltaSet1 a)
apply (Insert a
a) = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
a
    apply (Delete a
a) = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.delete a
a

-- | Delta encoding for a 'Set' where
-- collections of elements are inserted or deleted.
data DeltaSet a = DeltaSet
    { DeltaSet a -> Set a
inserts :: Set a
    , DeltaSet a -> Set a
deletes :: Set a
    } deriving (DeltaSet a -> DeltaSet a -> Bool
(DeltaSet a -> DeltaSet a -> Bool)
-> (DeltaSet a -> DeltaSet a -> Bool) -> Eq (DeltaSet a)
forall a. Eq a => DeltaSet a -> DeltaSet a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DeltaSet a -> DeltaSet a -> Bool
$c/= :: forall a. Eq a => DeltaSet a -> DeltaSet a -> Bool
== :: DeltaSet a -> DeltaSet a -> Bool
$c== :: forall a. Eq a => DeltaSet a -> DeltaSet a -> Bool
Eq)
-- INVARIANT: The two sets are always disjoint.

instance Ord a => Delta (DeltaSet a) where
    type Base (DeltaSet a) = Set a
    apply :: DeltaSet a -> Base (DeltaSet a) -> Base (DeltaSet a)
apply (DeltaSet Set a
i Set a
d) Base (DeltaSet a)
x = Set a
i Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Set a
Base (DeltaSet a)
x Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
d)

-- | Delta to get from the second argument to the first argument.
mkDeltaSet :: Ord a => Set a -> Set a -> DeltaSet a
mkDeltaSet :: Set a -> Set a -> DeltaSet a
mkDeltaSet Set a
new Set a
old =
    Set a -> Set a -> DeltaSet a
forall a. Set a -> Set a -> DeltaSet a
DeltaSet (Set a
new Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
old) (Set a
old Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
new)

-- | Flatten a 'DeltaSet' to a list of 'DeltaSet1'.
--
-- In the result list, the set of @a@ appearing as 'Insert'@ a@
-- is /disjoint/ from the set of @a@ appearing as 'Delete'@ a@.
deltaSetToList :: DeltaSet a -> [DeltaSet1 a]
deltaSetToList :: DeltaSet a -> [DeltaSet1 a]
deltaSetToList DeltaSet{Set a
inserts :: Set a
inserts :: forall a. DeltaSet a -> Set a
inserts,Set a
deletes :: Set a
deletes :: forall a. DeltaSet a -> Set a
deletes} =
    (a -> DeltaSet1 a) -> [a] -> [DeltaSet1 a]
forall a b. (a -> b) -> [a] -> [b]
map a -> DeltaSet1 a
forall a. a -> DeltaSet1 a
Insert (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
inserts) [DeltaSet1 a] -> [DeltaSet1 a] -> [DeltaSet1 a]
forall a. Semigroup a => a -> a -> a
<> (a -> DeltaSet1 a) -> [a] -> [DeltaSet1 a]
forall a b. (a -> b) -> [a] -> [b]
map a -> DeltaSet1 a
forall a. a -> DeltaSet1 a
Delete (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
deletes)

-- | Collect insertions or deletions of elements into a 'DeltaSet'.
--
-- To save space, combinations of 'Insert' and 'Delete'
-- for the same element are simplified when possible.
-- These simplifications always preserve the property
--
-- > apply (deltaSetFromList ds) = apply ds
deltaSetFromList :: Ord a => [DeltaSet1 a] -> DeltaSet a
deltaSetFromList :: [DeltaSet1 a] -> DeltaSet a
deltaSetFromList = (DeltaSet1 a -> DeltaSet a -> DeltaSet a)
-> DeltaSet a -> [DeltaSet1 a] -> DeltaSet a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr DeltaSet1 a -> DeltaSet a -> DeltaSet a
forall a. Ord a => DeltaSet1 a -> DeltaSet a -> DeltaSet a
step DeltaSet a
forall a. DeltaSet a
empty
  where
    empty :: DeltaSet a
empty = Set a -> Set a -> DeltaSet a
forall a. Set a -> Set a -> DeltaSet a
DeltaSet Set a
forall a. Set a
Set.empty Set a
forall a. Set a
Set.empty
    step :: DeltaSet1 a -> DeltaSet a -> DeltaSet a
step (Insert a
a) (DeltaSet Set a
i Set a
d) = Set a -> Set a -> DeltaSet a
forall a. Set a -> Set a -> DeltaSet a
DeltaSet (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
a Set a
i) (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.delete a
a Set a
d)
    step (Delete a
a) (DeltaSet Set a
i Set a
d) = Set a -> Set a -> DeltaSet a
forall a. Set a -> Set a -> DeltaSet a
DeltaSet (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.delete a
a Set a
i) (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
a Set a
d)

{- Note [DeltaSet1 Cancellations]

The following cancellation laws hold:

  apply [Insert a, Delete a] = apply (Insert a)
  apply [Insert a, Insert a] = apply (Insert a)
  apply [Delete a, Insert a] = apply (Delete a)
  apply [Delete a, Delete a] = apply (Delete a)

-}

-- | 'apply' distributes over '(<>)'.
instance Ord a => Semigroup (DeltaSet a) where
    (DeltaSet Set a
i1 Set a
d1) <> :: DeltaSet a -> DeltaSet a -> DeltaSet a
<> (DeltaSet Set a
i2 Set a
d2) = Set a -> Set a -> DeltaSet a
forall a. Set a -> Set a -> DeltaSet a
DeltaSet
        (Set a
i1 Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Set a
i2 Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
d1))
        (Set a
d1 Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Set a
d2 Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
i1))
        -- This takes into account [DeltaSet1 Cancellations]

instance Ord a => Monoid (DeltaSet a) where
    mempty :: DeltaSet a
mempty = Set a -> Set a -> DeltaSet a
forall a. Set a -> Set a -> DeltaSet a
DeltaSet Set a
forall a. Set a
Set.empty Set a
forall a. Set a
Set.empty

{-------------------------------------------------------------------------------
    Embedding
-------------------------------------------------------------------------------}
{- $Embedding

An 'Embedding'@ da db@ embeds one type and its delta encoding @da@
into another type and its delta encoding @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 bd@.
* 'load' attempts to retrieve the value of type @a@
    from the type @b@, but does not necessarily succeed.
* 'update' maps a delta encoding @da@ to a delta encoding @db@.
    For this mapping, the value of type @a@ and a corresponding
    value of type @b@ are provided;
    the delta encodings of types @da@ and @db@ are
    relative to these values.

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

* The embedding need __not__ be __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

        > 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 delta encoding can be computed.
    Put differently, we often have

        > write a ≠ b   where Right a = load b

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

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

    However, since the embedding is redundant, we often have

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

-- | Specification of an embedding of a type @a@ with delta encoding @da@
-- into the type @b@ with delta encoding @db@.
-- See [the discussion of @Embedding@](#g:3) 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
    { Embedding da db -> Base da -> Machine da db
inject  :: Base da -> Machine 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 :: Embedding' da db -> Embedding da db
mkEmbedding Embedding'{b -> Either SomeException a
load :: b -> Either SomeException a
load :: ()
load,a -> b
write :: a -> b
write :: ()
write,a -> b -> da -> db
update :: a -> b -> da -> db
update :: ()
update} = Embedding :: forall da db.
(Base da -> Machine da db)
-> (Base db -> Either SomeException (Base da, Machine da db))
-> Embedding da db
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 :: Embedding da db -> Embedding' da db
fromEmbedding Embedding{Base da -> Machine da db
inject :: Base da -> Machine da db
inject :: forall da db. Embedding da db -> Base da -> Machine da db
inject,Base db -> Either SomeException (Base da, Machine da db)
project :: 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} = Embedding' :: forall da db a b.
(Delta da, Delta db, a ~ Base da, b ~ Base db) =>
(b -> Either SomeException a)
-> (a -> b) -> (a -> b -> da -> db) -> Embedding' da db
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 (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 (String -> b
forall a. HasCallStack => String -> a
error String
"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 :: 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 :: forall da db.
(Base da -> Machine da db)
-> (Base db -> Either SomeException (Base da, Machine da db))
-> Embedding da db
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 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 (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 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 :: 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 :: forall da db.
(Base da -> Machine da db)
-> (Base db -> Either SomeException (Base da, Machine da db))
-> Embedding da db
Embedding{(Base da1, Base da2) -> Machine (da1, da2) (db1, db2)
Base (da1, da2) -> Machine (da1, da2) (db1, db2)
inject :: (Base da1, Base da2) -> Machine (da1, da2) (db1, db2)
inject :: Base (da1, 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, Base db2)
-> Either
     SomeException ((Base da1, Base da2), Machine (da1, da2) (db1, db2))
project :: Base (db1, db2)
-> Either
     SomeException (Base (da1, 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 (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'.
liftUpdates
    :: Delta da
    => Embedding da db
    -> [da] -- ^ List of deltas to apply. 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 :: Embedding da db -> [da] -> Base da -> (Base db, [db])
liftUpdates Embedding{Base da -> Machine da db
inject :: Base da -> Machine da db
inject :: forall da db. Embedding da db -> 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 encoding.
replaceFromApply :: (Delta da, a ~ Base da) => Embedding' da (Replace a)
replaceFromApply :: Embedding' da (Replace a)
replaceFromApply = Embedding' :: forall da db a b.
(Delta da, Delta db, a ~ Base da, b ~ Base db) =>
(b -> Either SomeException a)
-> (a -> b) -> (a -> b -> da -> db) -> Embedding' da db
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 encoding 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
-}

{-------------------------------------------------------------------------------
    Machine (state machines) with efficient composition
-------------------------------------------------------------------------------}
-- | Strict pair.
-- If a value of this type is in WHNF, so are the two components.
-- data StrictPair a b = !a :*: !b
-- infixr 1 :*:

-- | A state machine that maps deltas to deltas.
-- This machine always carries a state of type 'Base'@ db@ around.
data Machine da db = Machine
    { Machine da db -> Base db
state_ :: !(Base db)
    , Machine da db -> (Base da, da) -> (db, Machine da db)
step_  :: (Base da, da) -> (db, Machine da db)
    }

-- | Composition of 'Machine'
instance Semigroupoid Machine where
    (Machine Base k1
c (Base j, j) -> (k1, Machine j k1)
fbc) o :: Machine j k1 -> Machine i j -> Machine i k1
`o` (Machine Base j
b (Base i, i) -> (j, Machine i j)
fab) = Base k1 -> ((Base i, i) -> (k1, Machine i k1)) -> Machine i k1
forall da db.
Base db -> ((Base da, da) -> (db, Machine da db)) -> Machine da db
Machine Base k1
c (((Base i, i) -> (k1, Machine i k1)) -> Machine i k1)
-> ((Base i, i) -> (k1, Machine i k1)) -> Machine i k1
forall a b. (a -> b) -> a -> b
$ \(Base i, i)
ada ->
        case (Base i, i) -> (j, Machine i j)
fab (Base i, i)
ada of
            (j
db, Machine i j
mab) -> case (Base j, j) -> (k1, Machine j k1)
fbc (Base j
b,j
db) of
                (k1
dc, Machine j k1
mbc) -> (k1
dc, Machine j k1
mbc 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)

-- | Identity machine starting from a base type.
idle :: Delta da => Base da -> Machine da da
idle :: Base da -> Machine da da
idle Base da
a0 = Base da -> ((Base da, da) -> (da, Machine da da)) -> Machine da da
forall da db.
Base db -> ((Base da, da) -> (db, Machine da db)) -> Machine da db
Machine Base da
a0 (((Base da, da) -> (da, Machine da da)) -> Machine da da)
-> ((Base da, da) -> (da, Machine da da)) -> Machine da da
forall a b. (a -> b) -> a -> b
$ \(Base da
a1,da
da) -> let a2 :: Base da
a2 = da -> Base da -> Base da
forall delta. Delta delta => delta -> Base delta -> Base delta
apply da
da Base da
a1 in (da
da, Base da -> Machine da da
forall da. Delta da => Base da -> Machine da da
idle Base da
a2)

-- | Pair two 'Machine'.
pairMachine
    :: Machine da1 db1 -> Machine da2 db2 -> Machine (da1,da2) (db1,db2)
pairMachine :: Machine da1 db1 -> Machine da2 db2 -> Machine (da1, da2) (db1, db2)
pairMachine (Machine Base db1
s1 (Base da1, da1) -> (db1, Machine da1 db1)
step1) (Machine Base db2
s2 (Base da2, da2) -> (db2, Machine da2 db2)
step2) =
    Base (db1, db2)
-> ((Base (da1, da2), (da1, da2))
    -> ((db1, db2), Machine (da1, da2) (db1, db2)))
-> Machine (da1, da2) (db1, db2)
forall da db.
Base db -> ((Base da, da) -> (db, Machine da db)) -> Machine da db
Machine (Base db1
s1,Base db2
s2) (((Base (da1, da2), (da1, da2))
  -> ((db1, db2), Machine (da1, da2) (db1, db2)))
 -> Machine (da1, da2) (db1, db2))
-> ((Base (da1, da2), (da1, da2))
    -> ((db1, db2), Machine (da1, da2) (db1, db2)))
-> Machine (da1, da2) (db1, db2)
forall a b. (a -> b) -> a -> b
$ \((a1,a2), (da1
da1,da2
da2)) ->
        let (db1
db1, Machine da1 db1
m1) = (Base da1, da1) -> (db1, Machine da1 db1)
step1 (Base da1
a1,da1
da1)
            (db2
db2, Machine da2 db2
m2) = (Base da2, da2) -> (db2, Machine da2 db2)
step2 (Base da2
a2,da2
da2)
        in  ((db1
db1,db2
db2), 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)

-- | Create a 'Machine' from a specific state 's',
-- and the built-in state 'Base'@ db@.
fromState
    :: Delta db
    => ((Base da, da) -> (Base db, s) -> (db, s))
    -> (Base db, s)
    -> Machine da db
fromState :: ((Base da, da) -> (Base db, s) -> (db, s))
-> (Base db, s) -> Machine da db
fromState (Base da, da) -> (Base db, s) -> (db, s)
step (Base db
b,s
s0) = Base db -> ((Base da, da) -> (db, Machine da db)) -> Machine da db
forall da db.
Base db -> ((Base da, da) -> (db, Machine da db)) -> Machine da db
Machine Base db
b (((Base da, da) -> (db, Machine da db)) -> Machine da db)
-> ((Base da, da) -> (db, Machine da db)) -> Machine da db
forall a b. (a -> b) -> a -> b
$ \(Base da, da)
ada ->
    case (Base da, da) -> (Base db, s) -> (db, s)
step (Base da, da)
ada (Base db
b,s
s0) of
        (db
db,s
s1) -> (db
db, ((Base da, da) -> (Base db, s) -> (db, s))
-> (Base db, s) -> Machine da db
forall db da s.
Delta db =>
((Base da, da) -> (Base db, s) -> (db, s))
-> (Base db, s) -> Machine da db
fromState (Base da, da) -> (Base db, s) -> (db, s)
step (db -> Base db -> Base db
forall delta. Delta delta => delta -> Base delta -> Base delta
apply db
db Base db
b,s
s1))