{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}

{- |
This module provides all the safe API of 'BO' monad, including the advanced, low-level combinators that are not meant to be used by most users.
For the conceptual overview, please refer to "Control.Monad.Borrow.Pure", which is the prelude of this package.
-}
module Control.Monad.Borrow.Pure.BO (
  -- $header

  -- * Core 'BO' monad
  BO (),
  execBO,
  runBO,
  runBOLend,
  runBO_,
  sexecBO,
  scope_,
  srunBO,
  srunBO_,
  askLinearly,
  asksLinearly,
  asksLinearlyM,
  evaluateBO,

  -- ** In-place modification with mutable borrows
  modifyBO,
  modifyBO_,
  modifyLinearOnlyBO,
  modifyLinearOnlyBO_,

  -- * Parallel computation
  parBO,

  -- * Borrowing
  Alias,
  AliasKind,
  BorrowKind,
  Borrow,
  Mut,
  Share,
  Lend,
  coerceShare,
  shareCoercion,
  borrowM,
  borrowLinearlyM,
  sharing',
  sharing,
  (<$~),
  sharing_,
  (<$=),
  reborrowing',
  reborrowing,
  (<%~),
  reborrowing_,
  (<%=),
  share,
  reclaim',
  reclaim,
  pureAfter,
  reborrow,
  joinMut,
  joinLend,

  -- *** Lower-level operators
  borrow,
  borrowLinearOnly,

  -- ** Splitting aliases
  DistributesAlias (),
  split,
  GenericDistributesAlias,
  genericSplit,
  splitPair,
  splitEither,

  -- ** Misc Utilities

  -- *** Manual lifetime reassociation
  assocRBO,
  assocLBO,
  assocBOEq,
  assocBorrowL,
  assocBorrowR,
  assocBorrowEq,
  assocLendL,
  assocLendR,
  assocLendEq,

  -- * Re-exports
  module Control.Monad.Borrow.Pure.Lifetime,
  module Control.Monad.Borrow.Pure.Lifetime.Token,
  module Data.Coerce.Directed,
) where

import Control.Functor.Linear qualified as Control
import Control.Monad.Borrow.Pure.BO.Internal
import Control.Monad.Borrow.Pure.Lifetime
import Control.Monad.Borrow.Pure.Lifetime.Token
import Control.Monad.Borrow.Pure.Utils (coerceLin)
import Control.Syntax.DataFlow qualified as DataFlow
import Data.Coerce (Coercible)
import Data.Coerce.Directed
import Data.Type.Coercion (Coercion (..))
import Prelude.Linear

{- |
Runs a 'BO' computation and returns the result of postprocessing 'After' the lifetime has ended.

See also: 'runBOLend' and 'runBO_'.
-}
runBO :: forall a. Linearly %1 -> (forall α. BO α (After α a)) %1 -> a
{-# INLINE runBO #-}
runBO :: forall a.
Linearly %1 -> (forall (α :: Lifetime). BO α (After α a)) %1 -> a
runBO Linearly
lin forall (α :: Lifetime). BO α (After α a)
bo =
  case Linearly %1 -> SomeNow
newLifetime Linearly
lin of
    MkSomeNow (Now (Al i)
now :: Now α) -> DataFlow.do
      (now, f) <- forall (α :: Lifetime) a. BO α a %1 -> Now α %1 -> (Now α, a)
execBO @α @(After α a) BO (Al i) (After (Al i) a)
forall (α :: Lifetime). BO α (After α a)
bo Now (Al i)
now
      case endLifetime now of
        Ur EndToken (Al i)
end -> forall (α :: Lifetime) r. EndToken α -> After α r %1 -> r
withEnd @α EndToken (Al i)
end After (Al i) a
f

-- | A variant of 'runBO' that returns the original rsource retained by the 'Lend'er
runBOLend :: Linearly %1 -> (forall α. BO α (Lend α a)) %1 -> a
{-# INLINE runBOLend #-}
runBOLend :: forall a.
Linearly %1 -> (forall (α :: Lifetime). BO α (Lend α a)) %1 -> a
runBOLend Linearly
lin forall (α :: Lifetime). BO α (Lend α a)
bo = Linearly %1 -> (forall (α :: Lifetime). BO α (After α a)) %1 -> a
forall a.
Linearly %1 -> (forall (α :: Lifetime). BO α (After α a)) %1 -> a
runBO Linearly
lin Control.do
  lend <- BO α (Lend α a)
forall (α :: Lifetime). BO α (Lend α a)
bo
  Control.pure (reclaim' lend)

-- | A variant of 'runBO' that returns the direct value of 'BO' computation.
runBO_ :: Linearly %1 -> (forall α. BO α a) %1 -> a
{-# INLINE runBO_ #-}
runBO_ :: forall a. Linearly %1 -> (forall (α :: Lifetime). BO α a) %1 -> a
runBO_ Linearly
lin forall (α :: Lifetime). BO α a
bo = Linearly %1 -> (forall (α :: Lifetime). BO α (After α a)) %1 -> a
forall a.
Linearly %1 -> (forall (α :: Lifetime). BO α (After α a)) %1 -> a
runBO Linearly
lin Control.do
  a <- BO α a
forall (α :: Lifetime). BO α a
bo
  pureAfter a

-- | Flipped version of 'sexecBO'.
scope_ :: Now α %1 -> BO (α /\ β) a %1 -> BO β (Now α, a)
{-# INLINE scope_ #-}
scope_ :: forall (α :: Lifetime) (β :: Lifetime) a.
Now α %1 -> BO (α /\ β) a %1 -> BO β (Now α, a)
scope_ = (BO (α /\ β) a %1 -> Now α %1 -> BO β (Now α, a))
-> Now α %1 -> BO (α /\ β) a %1 -> BO β (Now α, a)
forall a (p :: Multiplicity) b (q :: Multiplicity) c
       (r :: Multiplicity).
(a %p -> b %q -> c) %r -> b %q -> a %p -> c
flip BO (α /\ β) a %1 -> Now α %1 -> BO β (Now α, a)
forall (α :: Lifetime) (β :: Lifetime) a.
BO (α /\ β) a %1 -> Now α %1 -> BO β (Now α, a)
sexecBO

-- | A variant of 'borrow' that obtains 'Linearly' viar 'LinearOnly'.
borrowLinearOnly :: forall α a. (LinearOnly a) => a %1 -> (Mut α a, Lend α a)
borrowLinearOnly :: forall (α :: Lifetime) a.
LinearOnly a =>
a %1 -> (Mut α a, Lend α a)
borrowLinearOnly !a
a = case a %1 -> (Linearly, a)
forall a. LinearOnly a => a %1 -> (Linearly, a)
withLinearly a
a of
  (!Linearly
lin, !a
a) -> a %1 -> Linearly %1 -> (Mut α a, Lend α a)
forall (α :: Lifetime) a.
a %1 -> Linearly %1 -> (Mut α a, Lend α a)
borrow a
a Linearly
lin

{- | A variant of 'sharing'' that discards the final result of the computation.
There is also a flipped infix version '(<$=)'.

See also: 'sharing'. For 'Mut'able borrows, see 'reborrowing_'.
-}
sharing_ ::
  forall α α' a r.
  (Consumable r) =>
  Mut α a %1 ->
  (forall β. Share (β /\ α) a -> BO (β /\ α') r) %1 ->
  BO α' (Mut α a)
{-# INLINE sharing_ #-}
sharing_ :: forall (α :: Lifetime) (α' :: Lifetime) a r.
Consumable r =>
Mut α a
%1 -> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> BO α' (Mut α a)
sharing_ Mut α a
v forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r
k = (r %1 -> Mut α a %1 -> Mut α a) -> (r, Mut α a) %1 -> Mut α a
forall a (p :: Multiplicity) b c (q :: Multiplicity).
(a %p -> b %p -> c) %q -> (a, b) %p -> c
uncurry r %1 -> Mut α a %1 -> Mut α a
forall a b. Consumable a => a %1 -> b %1 -> b
lseq ((r, Mut α a) %1 -> Mut α a)
%1 -> BO α' (r, Mut α a) %1 -> BO α' (Mut α a)
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
Control.<$> Mut α a
%1 -> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
forall (α :: Lifetime) (α' :: Lifetime) a r.
Mut α a
%1 -> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
sharing Mut α a
v Share (β /\ α) a -> BO (β /\ α') r
forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r
k

-- | Flipped infix version of 'sharing_', smoewhat analgous to '(Control.<$>)' and @(<%=)@ in @lens@ package.
(<$=) ::
  (forall β. Share (β /\ α) a -> BO (β /\ α') ()) %1 ->
  Mut α a %1 ->
  BO α' (Mut α a)
{-# INLINE (<$=) #-}
<$= :: forall (α :: Lifetime) a (α' :: Lifetime).
(forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') ())
%1 -> Mut α a %1 -> BO α' (Mut α a)
(<$=) = (Alias ('Borrow 'Mut) α a
 %1 -> (forall (β :: Lifetime).
        Alias ('Borrow 'Share) (β ':/\ α) a -> BO (β ':/\ α') ())
 %1 -> BO α' (Alias ('Borrow 'Mut) α a))
-> (forall (β :: Lifetime).
    Alias ('Borrow 'Share) (β ':/\ α) a -> BO (β ':/\ α') ())
%1 -> Alias ('Borrow 'Mut) α a
%1 -> BO α' (Alias ('Borrow 'Mut) α a)
forall a (p :: Multiplicity) b (q :: Multiplicity) c
       (r :: Multiplicity).
(a %p -> b %q -> c) %r -> b %q -> a %p -> c
flip Alias ('Borrow 'Mut) α a
%1 -> (forall (β :: Lifetime).
       Alias ('Borrow 'Share) (β ':/\ α) a -> BO (β ':/\ α') ())
%1 -> BO α' (Alias ('Borrow 'Mut) α a)
forall (α :: Lifetime) (α' :: Lifetime) a r.
Consumable r =>
Mut α a
%1 -> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> BO α' (Mut α a)
sharing_

{- | A variant of 'sharing'' that returns the direct value of the computation on the shared borrow.
There is also a flipped infix version '(<$~)'.

See also: 'sharing_'. For 'Mut'able borrows, see 'reborrowing'.
-}
sharing ::
  forall α α' a r.
  Mut α a %1 ->
  (forall β. Share (β /\ α) a -> BO (β /\ α') r) %1 ->
  BO α' (r, Mut α a)
{-# INLINE sharing #-}
sharing :: forall (α :: Lifetime) (α' :: Lifetime) a r.
Mut α a
%1 -> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
sharing Mut α a
v forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r
k = Mut α a
%1 -> (forall (β :: Lifetime).
       Share (β /\ α) a -> BO (β /\ α') (After β r))
%1 -> BO α' (r, Mut α a)
forall (α :: Lifetime) a (α' :: Lifetime) r.
Mut α a
%1 -> (forall (β :: Lifetime).
       Share (β /\ α) a -> BO (β /\ α') (After β r))
%1 -> BO α' (r, Mut α a)
sharing' Mut α a
v (\Share (β /\ α) a
mut -> r %1 -> After β r
forall a. a %1 -> After β a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure (r %1 -> After β r)
%1 -> BO (β /\ α') r %1 -> BO (β /\ α') (After β r)
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
Control.<$> Share (β /\ α) a -> BO (β /\ α') r
forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r
k Share (β /\ α) a
mut)

-- | Flipped infix version of 'sharing', smoewhat analgous to '(Control.<$>)' and @(<%~)@ in @lens@ package.
(<$~) ::
  (forall β. Share (β /\ α) a -> BO (β /\ α') r) %1 ->
  Mut α a %1 ->
  BO α' (r, Mut α a)
{-# INLINE (<$~) #-}
<$~ :: forall (α :: Lifetime) a (α' :: Lifetime) r.
(forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> Mut α a %1 -> BO α' (r, Mut α a)
(<$~) = (Mut α a
 %1 -> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
 %1 -> BO α' (r, Mut α a))
-> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> Mut α a
%1 -> BO α' (r, Mut α a)
forall a (p :: Multiplicity) b (q :: Multiplicity) c
       (r :: Multiplicity).
(a %p -> b %q -> c) %r -> b %q -> a %p -> c
flip Mut α a
%1 -> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
forall (α :: Lifetime) (α' :: Lifetime) a r.
Mut α a
%1 -> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
sharing

infix 4 <$~

{- | Executes an operation on 'Share'd borrow in sub lifetime.
You may need @-XImpredicativeTypes@ extension to use this function.

See also: 'sharing' and 'sharing_'. For 'Mut'able borrows, see 'reborrowing''.
-}
sharing' ::
  Mut α a %1 ->
  (forall β. Share (β /\ α) a -> BO (β /\ α') (After β r)) %1 ->
  BO α' (r, Mut α a)
{-# INLINE sharing' #-}
sharing' :: forall (α :: Lifetime) a (α' :: Lifetime) r.
Mut α a
%1 -> (forall (β :: Lifetime).
       Share (β /\ α) a -> BO (β /\ α') (After β r))
%1 -> BO α' (r, Mut α a)
sharing' Mut α a
v forall (β :: Lifetime).
Share (β /\ α) a -> BO (β /\ α') (After β r)
k = DataFlow.do
  (forall (α :: Lifetime). BO (α /\ α') (After α (r, Mut α a)))
%1 -> BO α' (r, Mut α a)
forall (β :: Lifetime) a.
(forall (α :: Lifetime). BO (α /\ β) (After α a)) %1 -> BO β a
srunBO DataFlow.do
    (v, lend) <- Mut α a %1 -> (Mut (α /\ α) a, Lend (α /\ α) (Mut α a))
forall (β :: Lifetime) (α :: Lifetime) a.
(α >= β) =>
Mut α a %1 -> (Mut β a, Lend β (Mut α a))
reborrow Mut α a
v
    share v & \(Ur Share (α /\ α) a
v) -> Control.do
      Share (α /\ α) a -> BO (α /\ α') (After α r)
forall (β :: Lifetime).
Share (β /\ α) a -> BO (β /\ α') (After β r)
k Share (α /\ α) a
v BO (α /\ α') (After α r)
%1 -> (After α r %1 -> After α (r, Mut α a))
%1 -> BO (α /\ α') (After α (r, Mut α a))
forall (f :: * -> *) a b.
Functor f =>
f a %1 -> (a %1 -> b) %1 -> f b
Control.<&> \After α r
v -> (,) (r %1 -> Mut α a %1 -> (r, Mut α a))
%1 -> After α r %1 -> After α (Mut α a %1 -> (r, Mut α a))
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
Control.<$> After α r
v After α (Mut α a %1 -> (r, Mut α a))
%1 -> After α (Mut α a) %1 -> After α (r, Mut α a)
forall a b. After α (a %1 -> b) %1 -> After α a %1 -> After α b
forall (f :: * -> *) a b.
Applicative f =>
f (a %1 -> b) %1 -> f a %1 -> f b
Control.<*> After (α /\ α) (Mut α a) %1 -> After α (Mut α a)
forall a b. (a <: b) => a %1 -> b
upcast (Lend (α /\ α) (Mut α a) %1 -> After (α /\ α) (Mut α a)
forall (α :: Lifetime) a. Lend α a %1 -> After α a
reclaim' Lend (α /\ α) (Mut α a)
lend)

{- | Executes an operation on 'Mut'able borrow in sub lifetime.
You may need @-XImpredicativeTypes@ extension to use this function.

See also: 'reborrowing', and 'reborrowing_'. For 'Share'd borrows, see 'sharing', 'sharing'', and 'sharing_'.
-}
reborrowing' ::
  Mut α a %1 ->
  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') (After β r)) %1 ->
  BO α' (r, Mut α a)
reborrowing' :: forall (α :: Lifetime) a (α' :: Lifetime) r.
Mut α a
%1 -> (forall (β :: Lifetime).
       Mut (β /\ α) a %1 -> BO (β /\ α') (After β r))
%1 -> BO α' (r, Mut α a)
reborrowing' Mut α a
v forall (β :: Lifetime).
Mut (β /\ α) a %1 -> BO (β /\ α') (After β r)
k = (forall (α :: Lifetime). BO (α /\ α') (After α (r, Mut α a)))
%1 -> BO α' (r, Mut α a)
forall (β :: Lifetime) a.
(forall (α :: Lifetime). BO (α /\ β) (After α a)) %1 -> BO β a
srunBO DataFlow.do
  (v, lend) <- Mut α a %1 -> (Mut (α /\ α) a, Lend (α /\ α) (Mut α a))
forall (β :: Lifetime) (α :: Lifetime) a.
(α >= β) =>
Mut α a %1 -> (Mut β a, Lend β (Mut α a))
reborrow Mut α a
v
  Control.do
    v <- k v
    Control.pure $ (,) Control.<$> v Control.<*> upcast (reclaim' lend)

{- | A variant of 'reborrowing'' that returns the direct value of the operation on the reborrowed mutable borrow.
There is also a flipped infix version '(<%~)'.

See also: 'reborrowing_' and 'sharing'.
-}
reborrowing ::
  Mut α a %1 ->
  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') r) %1 ->
  BO α' (r, Mut α a)
reborrowing :: forall (α :: Lifetime) a (α' :: Lifetime) r.
Mut α a
%1 -> (forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
reborrowing Mut α a
mutα forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r
k = Mut α a
%1 -> (forall (β :: Lifetime).
       Mut (β /\ α) a %1 -> BO (β /\ α') (After β r))
%1 -> BO α' (r, Mut α a)
forall (α :: Lifetime) a (α' :: Lifetime) r.
Mut α a
%1 -> (forall (β :: Lifetime).
       Mut (β /\ α) a %1 -> BO (β /\ α') (After β r))
%1 -> BO α' (r, Mut α a)
reborrowing' Mut α a
mutα (\Mut (β /\ α) a
mut -> r %1 -> After β r
forall a. a %1 -> After β a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure (r %1 -> After β r)
%1 -> BO (β /\ α') r %1 -> BO (β /\ α') (After β r)
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
Control.<$> Mut (β /\ α) a %1 -> BO (β /\ α') r
forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r
k Mut (β /\ α) a
mut)

-- | Flipped infix version of 'reborrowing', smoewhat analgous to '(Control.<$>)' and @(<%~)@ in @lens@ package.
(<%~) ::
  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') r) %1 ->
  Mut α a %1 ->
  BO α' (r, Mut α a)
{-# INLINE (<%~) #-}
<%~ :: forall (α :: Lifetime) a (α' :: Lifetime) r.
(forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r)
%1 -> Mut α a %1 -> BO α' (r, Mut α a)
(<%~) = (Mut α a
 %1 -> (forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r)
 %1 -> BO α' (r, Mut α a))
-> (forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r)
%1 -> Mut α a
%1 -> BO α' (r, Mut α a)
forall a (p :: Multiplicity) b (q :: Multiplicity) c
       (r :: Multiplicity).
(a %p -> b %q -> c) %r -> b %q -> a %p -> c
flip Mut α a
%1 -> (forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
forall (α :: Lifetime) a (α' :: Lifetime) r.
Mut α a
%1 -> (forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
reborrowing

infix 4 <%~

{- |
A variant of 'reborrowing'' that discards the final result of the computation.
There is also a flipped infix version '(<%=)'.

See also: 'reborrowing' and 'sharing_'.
-}
reborrowing_ ::
  (Consumable r) =>
  Mut α a %1 ->
  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') r) %1 ->
  BO α' (Mut α a)
reborrowing_ :: forall r (α :: Lifetime) a (α' :: Lifetime).
Consumable r =>
Mut α a
%1 -> (forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r)
%1 -> BO α' (Mut α a)
reborrowing_ Mut α a
mutα forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r
k = Mut α a
%1 -> (forall (β :: Lifetime).
       Mut (β /\ α) a %1 -> BO (β /\ α') ())
%1 -> BO α' ((), Mut α a)
forall (α :: Lifetime) a (α' :: Lifetime) r.
Mut α a
%1 -> (forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
reborrowing Mut α a
mutα ((r %1 -> ()) %1 -> BO (β /\ α') r %1 -> BO (β /\ α') ()
forall a b. (a %1 -> b) %1 -> BO (β /\ α') a %1 -> BO (β /\ α') b
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
Control.fmap r %1 -> ()
forall a. Consumable a => a %1 -> ()
consume (BO (β /\ α') r %1 -> BO (β /\ α') ())
-> (Mut (β /\ α) a %1 -> BO (β /\ α') r)
%1 -> Mut (β /\ α) a
%1 -> BO (β /\ α') ()
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. Mut (β /\ α) a %1 -> BO (β /\ α') r
forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r
k) BO α' ((), Mut α a)
%1 -> (((), Mut α a) %1 -> Mut α a) %1 -> BO α' (Mut α a)
forall (f :: * -> *) a b.
Functor f =>
f a %1 -> (a %1 -> b) %1 -> f b
Control.<&> \((), Mut α a
a) -> Mut α a
a

-- | Flipped infix version of 'reborrowing_', smoewhat analgous to '(Control.<$>)' and @(<%=)@ in @lens@ package.
(<%=) ::
  (forall β. Mut (β /\ α) a %1 -> BO (β /\ α') ()) %1 ->
  Mut α a %1 ->
  BO α' (Mut α a)
{-# INLINE (<%=) #-}
<%= :: forall (α :: Lifetime) a (α' :: Lifetime).
(forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') ())
%1 -> Mut α a %1 -> BO α' (Mut α a)
(<%=) = (Alias ('Borrow 'Mut) α a
 %1 -> (forall (β :: Lifetime).
        Alias ('Borrow 'Mut) (β ':/\ α) a %1 -> BO (β ':/\ α') ())
 %1 -> BO α' (Alias ('Borrow 'Mut) α a))
-> (forall (β :: Lifetime).
    Alias ('Borrow 'Mut) (β ':/\ α) a %1 -> BO (β ':/\ α') ())
%1 -> Alias ('Borrow 'Mut) α a
%1 -> BO α' (Alias ('Borrow 'Mut) α a)
forall a (p :: Multiplicity) b (q :: Multiplicity) c
       (r :: Multiplicity).
(a %p -> b %q -> c) %r -> b %q -> a %p -> c
flip Alias ('Borrow 'Mut) α a
%1 -> (forall (β :: Lifetime).
       Alias ('Borrow 'Mut) (β ':/\ α) a %1 -> BO (β ':/\ α') ())
%1 -> BO α' (Alias ('Borrow 'Mut) α a)
forall r (α :: Lifetime) a (α' :: Lifetime).
Consumable r =>
Mut α a
%1 -> (forall (β :: Lifetime). Mut (β /\ α) a %1 -> BO (β /\ α') r)
%1 -> BO α' (Mut α a)
reborrowing_

infix 4 <%=

-- | Modifies linear resources in-place, together with results.
modifyBO ::
  a %1 ->
  Linearly %1 ->
  (forall α. Mut α a %1 -> BO α r) %1 ->
  (r, a)
modifyBO :: forall a r.
a
%1 -> Linearly
%1 -> (forall (α :: Lifetime). Mut α a %1 -> BO α r)
%1 -> (r, a)
modifyBO a
v Linearly
lin forall (α :: Lifetime). Mut α a %1 -> BO α r
k = DataFlow.do
  (lin, lin') <- Linearly %1 -> (Linearly, Linearly)
forall a. Dupable a => a %1 -> (a, a)
dup Linearly
lin
  runBO lin Control.do
    let %1 !(mut, lend) = borrow v lin'
    r <- k mut
    Control.pure $ (r,) Control.<$> reclaim' lend

-- | Modifies linear resources in-place, without results.
modifyBO_ ::
  a %1 ->
  Linearly %1 ->
  (forall α. Mut α a %1 -> BO α ()) %1 ->
  a
modifyBO_ :: forall a.
a
%1 -> Linearly
%1 -> (forall (α :: Lifetime). Mut α a %1 -> BO α ())
%1 -> a
modifyBO_ a
v Linearly
lin forall (α :: Lifetime). Mut α a %1 -> BO α ()
k = DataFlow.do
  (lin, lin') <- Linearly %1 -> (Linearly, Linearly)
forall a. Dupable a => a %1 -> (a, a)
dup Linearly
lin
  runBO lin Control.do
    let %1 !(mut, lend) = borrow v lin'
    k mut
    Control.pure $ reclaim' lend

-- | Modifies linear resources in-place, together with results.
modifyLinearOnlyBO ::
  (LinearOnly a) =>
  a %1 ->
  (forall α. Mut α a %1 -> BO α r) %1 ->
  (r, a)
modifyLinearOnlyBO :: forall a r.
LinearOnly a =>
a %1 -> (forall (α :: Lifetime). Mut α a %1 -> BO α r) %1 -> (r, a)
modifyLinearOnlyBO a
v forall (α :: Lifetime). Mut α a %1 -> BO α r
k = DataFlow.do
  (lin, v) <- a %1 -> (Linearly, a)
forall a. LinearOnly a => a %1 -> (Linearly, a)
withLinearly a
v
  runBO lin Control.do
    let %1 !(mut, lend) = borrowLinearOnly v
    !r <- k mut
    Control.pure $ (r,) Control.<$> reclaim' lend

-- | Modifies linear resources in-place, together with results.
modifyLinearOnlyBO_ ::
  (LinearOnly a) =>
  a %1 ->
  (forall α. Mut α a %1 -> BO α ()) %1 ->
  a
modifyLinearOnlyBO_ :: forall a.
LinearOnly a =>
a %1 -> (forall (α :: Lifetime). Mut α a %1 -> BO α ()) %1 -> a
modifyLinearOnlyBO_ a
v forall (α :: Lifetime). Mut α a %1 -> BO α ()
k = DataFlow.do
  (lin, v) <- a %1 -> (Linearly, a)
forall a. LinearOnly a => a %1 -> (Linearly, a)
withLinearly a
v
  runBO lin Control.do
    let %1 !(mut, lend) = borrowLinearOnly v
    k mut
    Control.pure (reclaim' lend)

asksLinearly :: (Linearly %1 -> r) %1 -> BO α r
{-# INLINE asksLinearly #-}
asksLinearly :: forall r (α :: Lifetime). (Linearly %1 -> r) %1 -> BO α r
asksLinearly Linearly %1 -> r
k = (Linearly %1 -> BO α r) %1 -> BO α r
forall (α :: Lifetime) r. (Linearly %1 -> BO α r) %1 -> BO α r
asksLinearlyM ((Linearly %1 -> BO α r) %1 -> BO α r)
-> (Linearly %1 -> BO α r) %1 -> BO α r
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ r %1 -> BO α r
forall a. a %1 -> BO α a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure (r %1 -> BO α r) -> (Linearly %1 -> r) %1 -> Linearly %1 -> BO α r
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. Linearly %1 -> r
k

pureAfter :: ((End α) => a) %1 -> BO α (After α a)
{-# INLINE pureAfter #-}
pureAfter :: forall (α :: Lifetime) a. (End α => a) %1 -> BO α (After α a)
pureAfter End α => a
a = After α a %1 -> BO α (After α a)
forall a. a %1 -> BO α a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure ((End α => a) -> After α a
forall (α :: Lifetime) a. (End α => a) -> After α a
After a
End α => a
a)

coerceShare :: forall b α a. (Coercible a b) => Share α a %1 -> Share α b
{-# INLINE coerceShare #-}
coerceShare :: forall b (α :: Lifetime) a.
Coercible a b =>
Share α a %1 -> Share α b
coerceShare = Share α a %1 -> Share α b
forall a b. Coercible a b => a %1 -> b
coerceLin

shareCoercion :: forall a b α. (Coercible a b) => Coercion (Share α a) (Share α b)
{-# INLINE shareCoercion #-}
shareCoercion :: forall a b (α :: Lifetime).
Coercible a b =>
Coercion (Share α a) (Share α b)
shareCoercion = Coercion (Share α a) (Share α b)
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

{- |
Borrow a resource linearly for the same lifetime as the ambient 'BO' computation.
Returns the pair of the mutable borrow to the resource, and 'Lend'er to be invoked later to 'reclaim' the resource at the 'End' of the lifetime.

See also 'borrowLinearlyM'.

If you want to borrow a resource indepdendent of the ambient lifetime, you can use 'borrow' instead.
-}
borrowM :: a %1 -> BO α (Mut α a, Lend α a)
{-# INLINE borrowM #-}
borrowM :: forall a (α :: Lifetime). a %1 -> BO α (Mut α a, Lend α a)
borrowM !a
a = (Linearly %1 -> (Mut α a, Lend α a)) %1 -> BO α (Mut α a, Lend α a)
forall r (α :: Lifetime). (Linearly %1 -> r) %1 -> BO α r
asksLinearly \Linearly
lin -> a %1 -> Linearly %1 -> (Mut α a, Lend α a)
forall (α :: Lifetime) a.
a %1 -> Linearly %1 -> (Mut α a, Lend α a)
borrow a
a Linearly
lin

-- | A variant of 'borrowM' that does linear allocation first.
borrowLinearlyM :: (Linearly %1 -> a) %1 -> BO α (Mut α a, Lend α a)
{-# INLINE borrowLinearlyM #-}
borrowLinearlyM :: forall a (α :: Lifetime).
(Linearly %1 -> a) %1 -> BO α (Mut α a, Lend α a)
borrowLinearlyM Linearly %1 -> a
k = (Linearly %1 -> BO α (Mut α a, Lend α a))
%1 -> BO α (Mut α a, Lend α a)
forall (α :: Lifetime) r. (Linearly %1 -> BO α r) %1 -> BO α r
asksLinearlyM ((Linearly %1 -> BO α (Mut α a, Lend α a))
 %1 -> BO α (Mut α a, Lend α a))
-> (Linearly %1 -> BO α (Mut α a, Lend α a))
%1 -> BO α (Mut α a, Lend α a)
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ a %1 -> BO α (Mut α a, Lend α a)
forall a (α :: Lifetime). a %1 -> BO α (Mut α a, Lend α a)
borrowM (a %1 -> BO α (Mut α a, Lend α a))
-> (Linearly %1 -> a) %1 -> Linearly %1 -> BO α (Mut α a, Lend α a)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. Linearly %1 -> a
k

-- | Runs a 'BO' computation within the ephemeral sublifetime and returns the result.
srunBO :: (forall α. BO (α /\ β) (After α a)) %1 -> BO β a
{-# INLINE srunBO #-}
srunBO :: forall (β :: Lifetime) a.
(forall (α :: Lifetime). BO (α /\ β) (After α a)) %1 -> BO β a
srunBO forall (α :: Lifetime). BO (α /\ β) (After α a)
bo = (Linearly %1 -> BO β a) %1 -> BO β a
forall (α :: Lifetime) r. (Linearly %1 -> BO α r) %1 -> BO α r
asksLinearlyM \Linearly
lin ->
  Linearly
%1 -> (forall (ι :: Nat). Now (Al ι) %1 -> BO β a) %1 -> BO β a
forall a.
Linearly %1 -> (forall (ι :: Nat). Now (Al ι) %1 -> a) %1 -> a
newLifetime' Linearly
lin \Now (Al ι)
now -> Control.do
    (now, f) <- BO (Al ι /\ β) (After (Al ι) a)
%1 -> Now (Al ι) %1 -> BO β (Now (Al ι), After (Al ι) a)
forall (α :: Lifetime) (β :: Lifetime) a.
BO (α /\ β) a %1 -> Now α %1 -> BO β (Now α, a)
sexecBO BO (Al ι /\ β) (After (Al ι) a)
forall (α :: Lifetime). BO (α /\ β) (After α a)
bo Now (Al ι)
now
    Ur end <- Control.pure (endLifetime now)
    Control.pure (withEnd end f)

-- | A variant of 'srunBO' that returns the direct value of 'BO' computation.
srunBO_ :: (forall α. BO (α /\ β) a) %1 -> BO β a
{-# INLINE srunBO_ #-}
srunBO_ :: forall (β :: Lifetime) a.
(forall (α :: Lifetime). BO (α /\ β) a) %1 -> BO β a
srunBO_ forall (α :: Lifetime). BO (α /\ β) a
k = (forall (α :: Lifetime). BO (α /\ β) (After α a)) %1 -> BO β a
forall (β :: Lifetime) a.
(forall (α :: Lifetime). BO (α /\ β) (After α a)) %1 -> BO β a
srunBO Control.do a <- BO (α /\ β) a
forall (α :: Lifetime). BO (α /\ β) a
k; Control.pure $ After a