{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

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

Internal representation of 'Embedding'
in terms of state machines.
-}
module Data.Delta.Embedding.Internal (
      Machine (..)
    , idle
    , pairMachine
    , fromState
    ) where

import Prelude

import Data.Delta.Core
    ( Delta (..)
    )
import Data.Semigroupoid
    ( Semigroupoid (..)
    )

{-------------------------------------------------------------------------------
    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
    { forall da db. Machine da db -> Base db
state_ :: !(Base db)
    , forall da 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 :: forall j k1 i. 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 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)

-- | Identity machine starting from a base type.
idle :: Delta da => Base da -> Machine da da
idle :: forall da. Delta da => 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's.
pairMachine
    :: Machine da1 db1 -> Machine da2 db2 -> Machine (da1,da2) (db1,db2)
pairMachine :: forall da1 db1 da2 db2.
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
$ \((Base da1
a1,Base da2
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 :: 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 (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))