module Polysemy.Hasql.Interpreter.AtomicState where

import Conc (interpretLockReentrant)
import Hasql.Connection (Connection)
import Polysemy.Db.Data.InitDbError (InitDbError)
import Polysemy.Db.Interpreter.AtomicState (interpretAtomicStateStore, interpretAtomicStatesStore)
import Sqel.Data.QuerySchema (emptyQuerySchema)
import Sqel.Data.TableSchema (TableSchema)

import Polysemy.Hasql.Effect.Database (ConnectionSource)
import Polysemy.Hasql.Effect.DbTable (DbTable)
import Polysemy.Hasql.Interpreter.Store (interpretQStoreDb, interpretQStores)

-- |Interpret 'AtomicState' as a singleton table.
--
-- Given an action that produces an initial value, every state action reads the value from the database and writes it
-- back.
interpretAtomicStateDb ::
  Members [DbTable d !! e, Error InitDbError, Mask, Resource, Race, Embed IO] r =>
  TableSchema d ->
  Sem r d ->
  InterpreterFor (AtomicState d !! e) r
interpretAtomicStateDb :: forall d e (r :: EffectRow).
Members
  '[DbTable d !! e, Error InitDbError, Mask, Resource, Race,
    Embed IO]
  r =>
TableSchema d -> Sem r d -> InterpreterFor (AtomicState d !! e) r
interpretAtomicStateDb TableSchema d
table Sem r d
initial =
  forall (r :: EffectRow).
Members '[Resource, Race, Mask, Embed IO] r =>
InterpreterFor Lock r
interpretLockReentrant forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (k2 :: k1) (e :: (* -> *) -> * -> *) (r :: EffectRow)
       a.
Sem (Tagged k2 e : r) a -> Sem (e : r) a
untag forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall (f :: * -> *) q d e (r :: EffectRow).
(ResultShape d (f d), Member (DbTable d !! e) r) =>
TableSchema d
-> QuerySchema q d -> InterpreterFor (QStore f q d !! e) r
interpretQStoreDb @Maybe TableSchema d
table forall {k} (a :: k). QuerySchema () a
emptyQuerySchema forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall {k} (tag :: k) d err (r :: EffectRow).
Members '[QStore Maybe () d !! err, Lock @@ tag] r =>
Sem (Stop err : r) d -> InterpreterFor (AtomicState d !! err) r
interpretAtomicStateStore (forall (index :: Nat) (inserted :: EffectRow) (head :: EffectRow)
       (oldTail :: EffectRow) (tail :: EffectRow) (old :: EffectRow)
       (full :: EffectRow) a.
(ListOfLength index head, WhenStuck index InsertAtUnprovidedIndex,
 old ~ Append head oldTail, tail ~ Append inserted oldTail,
 full ~ Append head tail,
 InsertAtIndex index head tail oldTail full inserted) =>
Sem old a -> Sem full a
insertAt @0 Sem r d
initial) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall (index :: Nat) (inserted :: EffectRow) (head :: EffectRow)
       (oldTail :: EffectRow) (tail :: EffectRow) (old :: EffectRow)
       (full :: EffectRow) a.
(ListOfLength index head, WhenStuck index InsertAtUnprovidedIndex,
 old ~ Append head oldTail, tail ~ Append inserted oldTail,
 full ~ Append head tail,
 InsertAtIndex index head tail oldTail full inserted) =>
Sem old a -> Sem full a
insertAt @1

interpretAtomicStatesDb ::
  Members [Error InitDbError, Mask, Resource, Race, Embed IO] r =>
  Members [Scoped ConnectionSource (DbTable d !! err), DbTable d !! err, Log, Embed IO] r =>
  TableSchema d ->
  Sem r d ->
  InterpretersFor [AtomicState d !! err, Scoped Connection (AtomicState d !! err) !! err] r
interpretAtomicStatesDb :: forall (r :: EffectRow) d err.
(Members '[Error InitDbError, Mask, Resource, Race, Embed IO] r,
 Members
   '[Scoped ConnectionSource (DbTable d !! err), DbTable d !! err,
     Log, Embed IO]
   r) =>
TableSchema d
-> Sem r d
-> InterpretersFor
     '[AtomicState d !! err,
       Scoped Connection (AtomicState d !! err) !! err]
     r
interpretAtomicStatesDb TableSchema d
table Sem r d
initial =
  forall (r :: EffectRow).
Members '[Resource, Race, Mask, Embed IO] r =>
InterpreterFor Lock r
interpretLockReentrant forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (k2 :: k1) (e :: (* -> *) -> * -> *) (r :: EffectRow)
       a.
Sem (Tagged k2 e : r) a -> Sem (e : r) a
untag forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall (f :: * -> *) err q d (r :: EffectRow).
(ResultShape d (f d),
 Members
   '[Scoped ConnectionSource (DbTable d !! err), DbTable d !! err,
     Log, Embed IO]
   r) =>
TableSchema d
-> QuerySchema q d
-> InterpretersFor
     '[QStore f q d !! err,
       Scoped Connection (QStore f q d !! err) !! err]
     r
interpretQStores @Maybe TableSchema d
table forall {k} (a :: k). QuerySchema () a
emptyQuerySchema forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall {k} (tag :: k) param d err (r :: EffectRow).
Members
  '[QStore Maybe () d !! err,
    Scoped param (QStore Maybe () d !! err) !! err, Lock @@ tag]
  r =>
Sem (Stop err : r) d
-> InterpretersFor
     '[AtomicState d !! err, Scoped param (AtomicState d !! err) !! err]
     r
interpretAtomicStatesStore (forall (index :: Nat) (inserted :: EffectRow) (head :: EffectRow)
       (oldTail :: EffectRow) (tail :: EffectRow) (old :: EffectRow)
       (full :: EffectRow) a.
(ListOfLength index head, WhenStuck index InsertAtUnprovidedIndex,
 old ~ Append head oldTail, tail ~ Append inserted oldTail,
 full ~ Append head tail,
 InsertAtIndex index head tail oldTail full inserted) =>
Sem old a -> Sem full a
insertAt @0 Sem r d
initial) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall (index :: Nat) (inserted :: EffectRow) (head :: EffectRow)
       (oldTail :: EffectRow) (tail :: EffectRow) (old :: EffectRow)
       (full :: EffectRow) a.
(ListOfLength index head, WhenStuck index InsertAtUnprovidedIndex,
 old ~ Append head oldTail, tail ~ Append inserted oldTail,
 full ~ Append head tail,
 InsertAtIndex index head tail oldTail full inserted) =>
Sem old a -> Sem full a
insertAt @2