{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Data.Vector.Mutable.Linear.Borrow (
  Vector,
  empty,
  constant,
  fromList,
  fromVector,
  unsafeFromVector,
  fromMutable,
  unsafeFromMutable,
  toVector,
  toList,
  size,
  get,
  unsafeGet,
  set,
  unsafeSet,
  update,
  unsafeUpdate,
  modify,
  head,
  unsafeHead,
  last,
  unsafeLast,
  indicesMut,
  unsafeIndicesMut,
  splitAt,
  swap,
  unsafeSwap,
  copyAt,
  copyAtMut,
  inplace,

  -- * An example algorithm implementations
  qsort,

  -- ** Internal functions
  divide,
) where

import Control.Functor.Linear qualified as Control
import Control.Monad qualified as NonLinear
import Control.Monad.Borrow.Pure.BO
import Control.Monad.Borrow.Pure.BO.Unsafe
import Control.Monad.Borrow.Pure.Clone
import Control.Monad.Borrow.Pure.Copyable
import Control.Monad.Borrow.Pure.Lifetime.Token.Unsafe (
  LinearOnly (..),
  LinearOnlyWitness (..),
 )
import Control.Monad.Borrow.Pure.Utils
import Control.Monad.ST.Strict (ST)
import Control.Syntax.DataFlow qualified as DataFlow
import Data.Function qualified as NonLinear
import Data.Functor.Linear qualified as Data
import Data.IntSet qualified as IntSet
import Data.Unrestricted.Linear qualified as Ur
import Data.Vector qualified as V
import Data.Vector.Mutable (RealWorld)
import Data.Vector.Mutable qualified as MV
import GHC.Exts qualified as GHC
import GHC.IO (unsafePerformIO)
import GHC.Stack (HasCallStack)
import GHC.TypeError
import Prelude.Linear hiding (head, last, splitAt)
import Unsafe.Linear qualified as Unsafe
import Prelude qualified as NonLinear

{- |
Linearly owned mutable vector.
Contrary to those in @linear-base@, our 'Vector' owns every element @linearly@.
This is because Pure Borrow can now treat nested mutability safely, so we must allow mutable values to be stored inside 'Vector'.
This manifests in the type of 'set' - it returns the old value, which MUST NOT drop in favour of the new value.
-}
newtype Vector a = Vector {forall a. Vector a -> MVector RealWorld a
content :: MV.MVector RealWorld a}

empty :: Linearly %1 -> Vector a
{-# NOINLINE empty #-}
empty :: forall a. Linearly %1 -> Vector a
empty =
  (Linearly %1 -> Vector a) -> Linearly %1 -> Vector a
forall a. a -> a
GHC.noinline \Linearly
l ->
    Linearly
l Linearly %1 -> Vector a %1 -> Vector a
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` do
      MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector (IO (MVector RealWorld a) -> MVector RealWorld a
forall a. IO a -> a
unsafePerformIO (IO (MVector RealWorld a) -> MVector RealWorld a)
-> IO (MVector RealWorld a) -> MVector RealWorld a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ Int -> IO (MVector (PrimState IO) a)
forall (m :: * -> *) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
MV.new Int
0)

constant :: Int -> a -> Linearly %1 -> Vector a
{-# NOINLINE constant #-}
constant :: forall a. Int -> a -> Linearly %1 -> Vector a
constant = (Int -> a -> Linearly %1 -> Vector a)
-> Int -> a -> Linearly %1 -> Vector a
forall a. a -> a
GHC.noinline \Int
n a
a Linearly
l ->
  Linearly
l Linearly %1 -> Vector a %1 -> Vector a
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` do
    MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector (MVector RealWorld a -> Vector a)
-> MVector RealWorld a -> Vector a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
      IO (MVector RealWorld a) -> MVector RealWorld a
forall a. IO a -> a
unsafePerformIO (IO (MVector RealWorld a) -> MVector RealWorld a)
-> IO (MVector RealWorld a) -> MVector RealWorld a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
        Int -> a -> IO (MVector (PrimState IO) a)
forall (m :: * -> *) a.
PrimMonad m =>
Int -> a -> m (MVector (PrimState m) a)
MV.replicate Int
n a
a

fromList :: [a] %1 -> Linearly %1 -> Vector a
{-# NOINLINE fromList #-}
fromList :: forall a. [a] %1 -> Linearly %1 -> Vector a
fromList = ([a] %1 -> Linearly %1 -> Vector a)
-> [a] %1 -> Linearly %1 -> Vector a
forall a. a -> a
GHC.noinline (([a] %1 -> Linearly %1 -> Vector a)
 -> [a] %1 -> Linearly %1 -> Vector a)
-> ([a] %1 -> Linearly %1 -> Vector a)
-> [a]
%1 -> Linearly
%1 -> Vector a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ ([a] -> Linearly %1 -> Vector a)
%1 -> [a] %1 -> Linearly %1 -> Vector a
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \[a]
as Linearly
l ->
  Linearly
l Linearly %1 -> Vector a %1 -> Vector a
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` do
    MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector (MVector RealWorld a -> Vector a)
-> MVector RealWorld a -> Vector a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
      IO (MVector RealWorld a) -> MVector RealWorld a
forall a. IO a -> a
unsafePerformIO (IO (MVector RealWorld a) -> MVector RealWorld a)
-> IO (MVector RealWorld a) -> MVector RealWorld a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
        (Vector a -> IO (MVector (PrimState IO) a))
%1 -> Vector a -> IO (MVector (PrimState IO) a)
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear Vector a -> IO (MVector (PrimState IO) a)
forall (m :: * -> *) a.
PrimMonad m =>
Vector a -> m (MVector (PrimState m) a)
V.unsafeThaw (Vector a -> IO (MVector (PrimState IO) a))
-> Vector a -> IO (MVector (PrimState IO) a)
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
          ([a] -> Vector a) %1 -> [a] -> Vector a
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear [a] -> Vector a
forall a. [a] -> Vector a
V.fromList [a]
as

-- | Convert a 'V.Vector' (from @vector@ package) to a 'Vector'.
fromVector :: V.Vector a -> Linearly %1 -> Vector a
{-# NOINLINE fromVector #-}
fromVector :: forall a. Vector a -> Linearly %1 -> Vector a
fromVector = (Vector a -> Linearly %1 -> Vector a)
-> Vector a -> Linearly %1 -> Vector a
forall a. a -> a
GHC.noinline ((Vector a -> Linearly %1 -> Vector a)
 -> Vector a -> Linearly %1 -> Vector a)
-> (Vector a -> Linearly %1 -> Vector a)
-> Vector a
-> Linearly
%1 -> Vector a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ (Vector a -> Linearly %1 -> Vector a)
%1 -> Vector a -> Linearly %1 -> Vector a
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \Vector a
v Linearly
l ->
  Linearly
l Linearly %1 -> Vector a %1 -> Vector a
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` do
    MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector (MVector RealWorld a -> Vector a)
-> MVector RealWorld a -> Vector a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
      IO (MVector RealWorld a) -> MVector RealWorld a
forall a. IO a -> a
unsafePerformIO (IO (MVector RealWorld a) -> MVector RealWorld a)
-> IO (MVector RealWorld a) -> MVector RealWorld a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
        (Vector a -> IO (MVector (PrimState IO) a))
%1 -> Vector a -> IO (MVector (PrimState IO) a)
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear Vector a -> IO (MVector (PrimState IO) a)
forall (m :: * -> *) a.
PrimMonad m =>
Vector a -> m (MVector (PrimState m) a)
V.thaw Vector a
v

-- | /O(n)/. Clone a 'V.MVector' from @vector@ package to a 'Vector'.
fromMutable :: MV.MVector s a %1 -> Linearly %1 -> Vector a
{-# NOINLINE fromMutable #-}
fromMutable :: forall s a. MVector s a %1 -> Linearly %1 -> Vector a
fromMutable = (MVector s a %1 -> Linearly %1 -> Vector a)
-> MVector s a %1 -> Linearly %1 -> Vector a
forall a. a -> a
GHC.noinline ((MVector s a %1 -> Linearly %1 -> Vector a)
 -> MVector s a %1 -> Linearly %1 -> Vector a)
-> (MVector s a %1 -> Linearly %1 -> Vector a)
-> MVector s a
%1 -> Linearly
%1 -> Vector a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ (MVector s a -> Linearly %1 -> Vector a)
%1 -> MVector s a %1 -> Linearly %1 -> Vector a
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \MVector s a
v Linearly
l ->
  Linearly
l Linearly %1 -> Vector a %1 -> Vector a
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` do
    MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector (MVector RealWorld a -> Vector a)
-> MVector RealWorld a -> Vector a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
      IO (MVector RealWorld a) -> MVector RealWorld a
forall a. IO a -> a
unsafePerformIO (IO (MVector RealWorld a) -> MVector RealWorld a)
-> IO (MVector RealWorld a) -> MVector RealWorld a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
        (MVector (PrimState IO) a -> IO (MVector (PrimState IO) a))
%1 -> MVector (PrimState IO) a -> IO (MVector (PrimState IO) a)
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear MVector (PrimState IO) a -> IO (MVector (PrimState IO) a)
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> m (MVector (PrimState m) a)
MV.clone (MVector s a %1 -> MVector (PrimState IO) a
forall a b. a %1 -> b
Unsafe.coerce MVector s a
v)

unsafeFromMutable :: MV.MVector s a %1 -> Linearly %1 -> Vector a
unsafeFromMutable :: forall s a. MVector s a %1 -> Linearly %1 -> Vector a
unsafeFromMutable MVector s a
v Linearly
lin =
  Linearly
lin Linearly %1 -> Vector a %1 -> Vector a
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector (MVector s a %1 -> MVector RealWorld a
forall a b. a %1 -> b
Unsafe.coerce MVector s a
v)

{-
Note [Unrestricted Materialization of Vector]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We impose 'Copyable' on 'toVector' and 'toList' to ensure elements doesn't bare any essentially linear contents inside, but we don't make use of the constraint internally.
Is it a cheating? Maybe. Think hard about it.
-}

-- | /O(1)/. Freezes @'Vector' a@ to @'V.Vector' a@ from @vector@ package, /without/ copying.
toVector ::
  -- See Note [Unrestricted Materialization of Vector].
  (Copyable a) =>
  Vector a %1 -> Ur (V.Vector a)
{-# NOINLINE toVector #-}
toVector :: forall a. Copyable a => Vector a %1 -> Ur (Vector a)
toVector = (Vector a %1 -> Ur (Vector a)) -> Vector a %1 -> Ur (Vector a)
forall a. a -> a
GHC.noinline ((Vector a %1 -> Ur (Vector a)) -> Vector a %1 -> Ur (Vector a))
-> (Vector a %1 -> Ur (Vector a)) -> Vector a %1 -> Ur (Vector a)
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$
  (Vector a -> Ur (Vector a)) %1 -> Vector a %1 -> Ur (Vector a)
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \(Vector MVector RealWorld a
v) -> Vector a -> Ur (Vector a)
forall a. a -> Ur a
Ur (Vector a -> Ur (Vector a)) -> Vector a -> Ur (Vector a)
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ IO (Vector a) -> Vector a
forall a. IO a -> a
unsafePerformIO (IO (Vector a) -> Vector a) -> IO (Vector a) -> Vector a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ MVector (PrimState IO) a -> IO (Vector a)
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> m (Vector a)
V.unsafeFreeze MVector RealWorld a
MVector (PrimState IO) a
v

-- Same applies to 'Copyable' here, as in 'toVector'.
toList ::
  -- See Note [Unrestricted Materialization of Vector].
  (Copyable a) =>
  Vector a %1 -> Ur [a]
{-# INLINE toList #-}
toList :: forall a. Copyable a => Vector a %1 -> Ur [a]
toList = (Vector a -> [a]) -> Ur (Vector a) %1 -> Ur [a]
forall a b. (a -> b) -> Ur a %1 -> Ur b
Ur.lift Vector a -> [a]
forall a. Vector a -> [a]
V.toList (Ur (Vector a) %1 -> Ur [a])
-> (Vector a %1 -> Ur (Vector a)) -> Vector a %1 -> Ur [a]
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. Vector a %1 -> Ur (Vector a)
forall a. Copyable a => Vector a %1 -> Ur (Vector a)
toVector

{- | Unsafely thaws 'V.Vector' (from @vector@ package) to a 'Vector',
reusing the same memory.
This is highly unsafe
-}
unsafeFromVector :: V.Vector a %1 -> Linearly %1 -> Vector a
{-# NOINLINE unsafeFromVector #-}
unsafeFromVector :: forall a. Vector a %1 -> Linearly %1 -> Vector a
unsafeFromVector = (Vector a -> Linearly %1 -> Vector a)
%1 -> Vector a %1 -> Linearly %1 -> Vector a
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \Vector a
v Linearly
l ->
  Linearly
l Linearly %1 -> Vector a %1 -> Vector a
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` Vector a -> Vector a
forall a. a -> a
GHC.noinline do
    MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector (MVector RealWorld a -> Vector a)
-> MVector RealWorld a -> Vector a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
      IO (MVector RealWorld a) -> MVector RealWorld a
forall a. IO a -> a
unsafePerformIO (IO (MVector RealWorld a) -> MVector RealWorld a)
-> IO (MVector RealWorld a) -> MVector RealWorld a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$!
        Vector a -> IO (MVector (PrimState IO) a)
forall (m :: * -> *) a.
PrimMonad m =>
Vector a -> m (MVector (PrimState m) a)
V.unsafeThaw Vector a
v

size :: Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
{-# INLINE size #-}
size :: forall (bk :: BorrowKind) (α :: Lifetime) a.
Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
size =
  Alias ('Borrow bk) α (Vector a) %1 -> Vector a
forall (ak :: AliasKind) (α :: Lifetime) a. Alias ak α a %1 -> a
unsafeUnalias (Alias ('Borrow bk) α (Vector a) %1 -> Vector a)
-> (Vector a %1 -> (Ur Int, Alias ('Borrow bk) α (Vector a)))
-> Alias ('Borrow bk) α (Vector a)
%1 -> (Ur Int, Alias ('Borrow bk) α (Vector a))
forall a b c. (a %1 -> b) -> (b %1 -> c) -> a %1 -> c
>>> (Vector a -> (Ur Int, Alias ('Borrow bk) α (Vector a)))
%1 -> Vector a %1 -> (Ur Int, Alias ('Borrow bk) α (Vector a))
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \(Vector MVector RealWorld a
v) ->
    (Int %1 -> Ur Int
forall a. Movable a => a %1 -> Ur a
move (MVector RealWorld a -> Int
forall s a. MVector s a -> Int
MV.length MVector RealWorld a
v), Vector a -> Alias ('Borrow bk) α (Vector a)
forall (ak :: AliasKind) (α :: Lifetime) a. a -> Alias ak α a
UnsafeAlias (MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector MVector RealWorld a
v))

{- |
@'set' i a v@ sets the @i@-th element of @v@ to @a@, and returns the old value alongside.
Note that @a@ is bound linearly.
-}
set :: (HasCallStack, α >= β) => Int -> a %1 -> Mut α (Vector a) %1 -> BO β (a, Mut α (Vector a))
{-# INLINE set #-}
set :: forall (α :: Lifetime) (β :: Lifetime) a.
(HasCallStack, α >= β) =>
Int -> a %1 -> Mut α (Vector a) %1 -> BO β (a, Mut α (Vector a))
set Int
i a
a Mut α (Vector a)
v = DataFlow.do
  (len, v) <- Mut α (Vector a) %1 -> (Ur Int, Mut α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
size Mut α (Vector a)
v
  case len of
    Ur Int
len ->
      if Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
< Int
0 Bool %1 -> Bool %1 -> Bool
|| Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
>= Int
len
        then String -> Mut α (Vector a) %1 -> a %1 -> BO β (a, Mut α (Vector a))
forall a. HasCallStack => String -> a
error (String
"get: index " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> String
" out of bound: " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> Int -> String
forall a. Show a => a -> String
show Int
len) Mut α (Vector a)
v a
a
        else Int -> a %1 -> Mut α (Vector a) %1 -> BO β (a, Mut α (Vector a))
forall (α :: Lifetime) (β :: Lifetime) a.
(α >= β) =>
Int -> a %1 -> Mut α (Vector a) %1 -> BO β (a, Mut α (Vector a))
unsafeSet Int
i a
a Mut α (Vector a)
v

-- | 'set' without bound check.
unsafeSet :: (α >= β) => Int -> a %1 -> Mut α (Vector a) %1 -> BO β (a, Mut α (Vector a))
unsafeSet :: forall (α :: Lifetime) (β :: Lifetime) a.
(α >= β) =>
Int -> a %1 -> Mut α (Vector a) %1 -> BO β (a, Mut α (Vector a))
unsafeSet = (Int -> a -> Mut α (Vector a) -> BO β (a, Mut α (Vector a)))
%1 -> Int
-> a
%1 -> Mut α (Vector a)
%1 -> BO β (a, Mut α (Vector a))
forall a b c d (p :: Multiplicity) (q :: Multiplicity)
       (r :: Multiplicity) (x :: Multiplicity) (y :: Multiplicity)
       (z :: Multiplicity).
(a %p -> b %q -> c %r -> d) %1 -> a %x -> b %y -> c %z -> d
Unsafe.toLinear3 \Int
i a
a mut :: Mut α (Vector a)
mut@(UnsafeAlias (Vector MVector RealWorld a
v)) -> IO (a, Mut α (Vector a)) %1 -> BO β (a, Mut α (Vector a))
forall a (α :: Lifetime). IO a %1 -> BO α a
unsafeSystemIOToBO do
  old <- MVector (PrimState IO) a -> Int -> IO a
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.unsafeRead MVector RealWorld a
MVector (PrimState IO) a
v Int
i
  MV.unsafeWrite v i a
  NonLinear.pure (old, mut)

-- | 'get' without bounds check.
unsafeGet :: (α >= β) => Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
{-# INLINE unsafeGet #-}
unsafeGet :: forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(α >= β) =>
Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
unsafeGet Int
i =
  (Borrow bk α (Vector a) -> BO β (Borrow bk α a))
%1 -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \Borrow bk α (Vector a)
v ->
    Borrow bk α (Vector a) %1 -> Vector a
forall (ak :: AliasKind) (α :: Lifetime) a. Alias ak α a %1 -> a
unsafeUnalias Borrow bk α (Vector a)
v
      Vector a
-> (Vector a -> BO β (Borrow bk α a)) -> BO β (Borrow bk α a)
forall a b. a -> (a -> b) -> b
NonLinear.& \(Vector MVector RealWorld a
v) ->
        a -> Borrow bk α a
forall (ak :: AliasKind) (α :: Lifetime) a. a -> Alias ak α a
UnsafeAlias
          (a %1 -> Borrow bk α a) %1 -> BO β a %1 -> BO β (Borrow bk α a)
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
Control.<$> IO a %1 -> BO β a
forall a (α :: Lifetime). IO a %1 -> BO α a
unsafeSystemIOToBO (MVector (PrimState IO) a -> Int -> IO a
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.unsafeRead MVector RealWorld a
MVector (PrimState IO) a
v Int
i)

head :: (HasCallStack, α >= β) => Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
{-# INLINE head #-}
head :: forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(HasCallStack, α >= β) =>
Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
head = Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(HasCallStack, α >= β) =>
Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
get Int
0

unsafeHead :: (α >= β) => Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
{-# INLINE unsafeHead #-}
unsafeHead :: forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(α >= β) =>
Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
unsafeHead = Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(α >= β) =>
Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
unsafeGet Int
0

unsafeLast :: (α >= β) => Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
{-# INLINE unsafeLast #-}
unsafeLast :: forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(α >= β) =>
Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
unsafeLast Borrow bk α (Vector a)
v = DataFlow.do
  (len, v) <- Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
size Borrow bk α (Vector a)
v
  case len of
    Ur Int
len -> Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(α >= β) =>
Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
unsafeGet (Int
len Int %1 -> Int %1 -> Int
forall a. AdditiveGroup a => a %1 -> a %1 -> a
- Int
1) Borrow bk α (Vector a)
v

last :: (HasCallStack, α >= β) => Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
{-# INLINE last #-}
last :: forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(HasCallStack, α >= β) =>
Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
last Borrow bk α (Vector a)
v = DataFlow.do
  (len, v) <- Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
size Borrow bk α (Vector a)
v
  case len of
    Ur Int
len
      | Int
len Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
> Int
0 -> Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(α >= β) =>
Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
unsafeGet (Int
len Int %1 -> Int %1 -> Int
forall a. AdditiveGroup a => a %1 -> a %1 -> a
- Int
1) Borrow bk α (Vector a)
v
      | Bool
otherwise -> String -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
forall a. HasCallStack => String -> a
error (String
"last: empty vector") Borrow bk α (Vector a)
v

get ::
  (HasCallStack, α >= β) =>
  Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
{-# INLINE get #-}
get :: forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(HasCallStack, α >= β) =>
Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
get Int
i Borrow bk α (Vector a)
v = DataFlow.do
  (len, v) <- Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
size Borrow bk α (Vector a)
v
  case len of
    Ur Int
len ->
      if Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
< Int
0 Bool %1 -> Bool %1 -> Bool
|| Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
>= Int
len
        then String -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
forall a. HasCallStack => String -> a
error (String
"get: index " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> String
" out of bound: " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> Int -> String
forall a. Show a => a -> String
show Int
len) Borrow bk α (Vector a)
v
        else Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(α >= β) =>
Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
unsafeGet Int
i Borrow bk α (Vector a)
v

unsafeUpdate :: (α >= β) => Int -> (a %1 -> BO β (b, a)) %1 -> Mut α (Vector a) %1 -> BO β (b, Mut α (Vector a))
unsafeUpdate :: forall (α :: Lifetime) (β :: Lifetime) a b.
(α >= β) =>
Int
-> (a %1 -> BO β (b, a))
%1 -> Mut α (Vector a)
%1 -> BO β (b, Mut α (Vector a))
unsafeUpdate Int
i = ((a %1 -> BO β (b, a))
 -> Mut α (Vector a) -> BO β (b, Mut α (Vector a)))
%1 -> (a %1 -> BO β (b, a))
%1 -> Mut α (Vector a)
%1 -> BO β (b, Mut α (Vector a))
forall a b c (p :: Multiplicity) (q :: Multiplicity)
       (x :: Multiplicity) (y :: Multiplicity).
(a %p -> b %q -> c) %1 -> a %x -> b %y -> c
Unsafe.toLinear2 \a %1 -> BO β (b, a)
k (UnsafeAlias Vector a
v) -> Control.do
  a <- IO a %1 -> BO β a
forall a (α :: Lifetime). IO a %1 -> BO α a
unsafeSystemIOToBO (IO a %1 -> BO β a) -> IO a %1 -> BO β a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ MVector (PrimState IO) a -> Int -> IO a
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.unsafeRead (Vector a -> MVector RealWorld a
forall a. Vector a -> MVector RealWorld a
content Vector a
v) Int
i
  (b, a') <- k a
  () <- unsafeSystemIOToBO $ Unsafe.toLinear3 MV.unsafeWrite (content v) i a'
  Control.pure $ (b, UnsafeAlias v)

update :: (α >= β) => Int -> (a %1 -> BO β (b, a)) %1 -> Mut α (Vector a) %1 -> BO β (b, Mut α (Vector a))
update :: forall (α :: Lifetime) (β :: Lifetime) a b.
(α >= β) =>
Int
-> (a %1 -> BO β (b, a))
%1 -> Mut α (Vector a)
%1 -> BO β (b, Mut α (Vector a))
update Int
i a %1 -> BO β (b, a)
k Mut α (Vector a)
v = DataFlow.do
  (len, v) <- Mut α (Vector a) %1 -> (Ur Int, Mut α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
size Mut α (Vector a)
v
  case len of
    Ur Int
len ->
      if Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
< Int
0 Bool %1 -> Bool %1 -> Bool
|| Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
>= Int
len
        then String
-> Mut α (Vector a)
%1 -> (a %1 -> BO β (b, a))
%1 -> BO β (b, Mut α (Vector a))
forall a. HasCallStack => String -> a
error (String
"set: index " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> String
" out of bound: " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> Int -> String
forall a. Show a => a -> String
show Int
len) Mut α (Vector a)
v a %1 -> BO β (b, a)
k
        else Int
-> (a %1 -> BO β (b, a))
%1 -> Mut α (Vector a)
%1 -> BO β (b, Mut α (Vector a))
forall (α :: Lifetime) (β :: Lifetime) a b.
(α >= β) =>
Int
-> (a %1 -> BO β (b, a))
%1 -> Mut α (Vector a)
%1 -> BO β (b, Mut α (Vector a))
unsafeUpdate Int
i a %1 -> BO β (b, a)
k Mut α (Vector a)
v

modify :: (α >= β) => Int -> (a %1 -> a) %1 -> Mut α (Vector a) %1 -> BO β (Mut α (Vector a))
modify :: forall (α :: Lifetime) (β :: Lifetime) a.
(α >= β) =>
Int
-> (a %1 -> a) %1 -> Mut α (Vector a) %1 -> BO β (Mut α (Vector a))
modify Int
i a %1 -> a
f Mut α (Vector a)
v = Control.do
  ((), ma) <- Int
-> (a %1 -> BO β ((), a))
%1 -> Mut α (Vector a)
%1 -> BO β ((), Mut α (Vector a))
forall (α :: Lifetime) (β :: Lifetime) a b.
(α >= β) =>
Int
-> (a %1 -> BO β (b, a))
%1 -> Mut α (Vector a)
%1 -> BO β (b, Mut α (Vector a))
update Int
i (((), a) %1 -> BO β ((), a)
forall a. a %1 -> BO β a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure (((), a) %1 -> BO β ((), a))
-> (a %1 -> ((), a)) %1 -> a %1 -> BO β ((), a)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. ((),) (a %1 -> ((), a)) -> (a %1 -> a) %1 -> a %1 -> ((), a)
forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> a
f) Mut α (Vector a)
v
  Control.pure ma

{- | Get multiple elements at the given indices without bounds and duplication check.
For more safety, use 'indicesMut'.
-}
unsafeIndicesMut :: (α >= β) => Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]
unsafeIndicesMut :: forall (α :: Lifetime) (β :: Lifetime) a.
(α >= β) =>
Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]
unsafeIndicesMut = (Mut α (Vector a) -> [Int] %1 -> BO β [Mut α a])
%1 -> Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \Mut α (Vector a)
v [Int]
is ->
  (Int %1 -> BO β (Mut α a)) -> [Int] %1 -> BO β [Mut α a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a %1 -> f b) -> t a %1 -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a %1 -> f b) -> [a] %1 -> f [b]
Data.traverse
    (\Int
i -> Int %1 -> Ur Int
forall a. Movable a => a %1 -> Ur a
move Int
i Ur Int %1 -> (Ur Int %1 -> BO β (Mut α a)) -> BO β (Mut α a)
forall a b (p :: Multiplicity) (q :: Multiplicity).
a %p -> (a %p -> b) %q -> b
& \(Ur Int
i) -> Int -> Mut α (Vector a) %1 -> BO β (Mut α a)
forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(α >= β) =>
Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
unsafeGet Int
i Mut α (Vector a)
v)
    [Int]
is

indicesMut :: (HasCallStack, α >= β) => Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]
indicesMut :: forall (α :: Lifetime) (β :: Lifetime) a.
(HasCallStack, α >= β) =>
Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]
indicesMut = (Mut α (Vector a) -> [Int] -> BO β [Mut α a])
%1 -> Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]
forall a b c (p :: Multiplicity) (q :: Multiplicity)
       (x :: Multiplicity) (y :: Multiplicity).
(a %p -> b %q -> c) %1 -> a %x -> b %y -> c
Unsafe.toLinear2 \Mut α (Vector a)
v [Int]
is ->
  case Mut α (Vector a) %1 -> (Ur Int, Mut α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
size Mut α (Vector a)
v of
    (Ur Int
len, Mut α (Vector a)
v) ->
      if
        | (Int %1 -> Bool) -> [Int] %1 -> Bool
forall a. (a %1 -> Bool) -> [a] %1 -> Bool
any (\Int
i -> Int %1 -> Ur Int
forall a. Movable a => a %1 -> Ur a
move Int
i Ur Int %1 -> (Ur Int %1 -> Bool) -> Bool
forall a b (p :: Multiplicity) (q :: Multiplicity).
a %p -> (a %p -> b) %q -> b
& \(Ur Int
i) -> Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
< Int
0 Bool %1 -> Bool %1 -> Bool
|| Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
>= Int
len) [Int]
is ->
            String -> Mut α (Vector a) -> BO β [Mut α a]
forall a. HasCallStack => String -> a
error (String
"indicesMut: indices out of bound: " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> [Int] -> String
forall a. Show a => a -> String
show [Int]
is String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> String
" for length " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> Int -> String
forall a. Show a => a -> String
show Int
len) Mut α (Vector a)
v
        | [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
NonLinear.length [Int]
is Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
> IntSet -> Int
IntSet.size ([Int] -> IntSet
IntSet.fromList [Int]
is) ->
            String -> Mut α (Vector a) -> BO β [Mut α a]
forall a. HasCallStack => String -> a
error (String
"indicesMut: duplicate indices: " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> [Int] -> String
forall a. Show a => a -> String
show [Int]
is) Mut α (Vector a)
v
        | Bool
otherwise -> Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]
forall (α :: Lifetime) (β :: Lifetime) a.
(α >= β) =>
Mut α (Vector a) %1 -> [Int] %1 -> BO β [Mut α a]
unsafeIndicesMut Mut α (Vector a)
v [Int]
is

splitAt :: Int %1 -> Borrow bk α (Vector a) %1 -> (Borrow bk α (Vector a), Borrow bk α (Vector a))
{-# INLINE splitAt #-}
splitAt :: forall (bk :: BorrowKind) (α :: Lifetime) a.
Int
%1 -> Borrow bk α (Vector a)
%1 -> (Borrow bk α (Vector a), Borrow bk α (Vector a))
splitAt = (Int
 -> Borrow bk α (Vector a)
 -> (Borrow bk α (Vector a), Borrow bk α (Vector a)))
%1 -> Int
%1 -> Borrow bk α (Vector a)
%1 -> (Borrow bk α (Vector a), Borrow bk α (Vector a))
forall a b c (p :: Multiplicity) (q :: Multiplicity)
       (x :: Multiplicity) (y :: Multiplicity).
(a %p -> b %q -> c) %1 -> a %x -> b %y -> c
Unsafe.toLinear2 \Int
i (UnsafeAlias (Vector MVector RealWorld a
v)) ->
  let (MVector RealWorld a
v1, MVector RealWorld a
v2) = Int
-> MVector RealWorld a
-> (MVector RealWorld a, MVector RealWorld a)
forall s a. Int -> MVector s a -> (MVector s a, MVector s a)
MV.splitAt Int
i MVector RealWorld a
v
   in (Vector a -> Borrow bk α (Vector a)
forall (ak :: AliasKind) (α :: Lifetime) a. a -> Alias ak α a
UnsafeAlias (MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector MVector RealWorld a
v1), Vector a -> Borrow bk α (Vector a)
forall (ak :: AliasKind) (α :: Lifetime) a. a -> Alias ak α a
UnsafeAlias (MVector RealWorld a -> Vector a
forall a. MVector RealWorld a -> Vector a
Vector MVector RealWorld a
v2))

instance LinearOnly (Vector a) where
  linearOnly :: LinearOnlyWitness (Vector a)
linearOnly = LinearOnlyWitness (Vector a)
forall {k} (a :: k). LinearOnlyWitness a
UnsafeLinearOnly
  {-# INLINE linearOnly #-}

instance
  (Unsatisfiable (ShowType (Vector a) :<>: Text " cannot be copied!")) =>
  Copyable (Vector a)
  where
  copy :: forall (bk :: BorrowKind) (α :: Lifetime).
Borrow bk α (Vector a) %1 -> Vector a
copy = Borrow bk α (Vector a) %1 -> Vector a
forall (msg :: ErrorMessage) a. Unsatisfiable msg => a
unsatisfiable

instance (Dupable a) => Clone (Vector a) where
  clone :: forall (α :: Lifetime). Share α (Vector a) %1 -> BO α (Vector a)
clone = (Share α (Vector a) -> BO α (Vector a))
%1 -> Share α (Vector a) %1 -> BO α (Vector a)
forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear \(UnsafeAlias (Vector MVector RealWorld a
v)) -> IO (Vector a) %1 -> BO α (Vector a)
forall a (α :: Lifetime). IO a %1 -> BO α a
unsafeSystemIOToBO do
    let !n :: Int
n = MVector RealWorld a -> Int
forall s a. MVector s a -> Int
MV.length MVector RealWorld a
v
    !new <- Int -> IO (MVector (PrimState IO) a)
forall (m :: * -> *) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
MV.new Int
n
    let go !Int
i = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
NonLinear.when (Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
< Int
n) do
          x <- MVector (PrimState IO) a -> Int -> IO a
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m a
MV.unsafeRead MVector RealWorld a
MVector (PrimState IO) a
v Int
i
          let (!_, !x') = dup x
          MV.unsafeWrite new i x'
          go (i + 1)
    go 0
    NonLinear.pure (Vector new)
  {-# INLINE clone #-}

unsafeSwap :: (α >= β) => Mut α (Vector a) %1 -> Int -> Int -> BO β (Mut α (Vector a))
unsafeSwap :: forall (α :: Lifetime) (β :: Lifetime) a.
(α >= β) =>
Mut α (Vector a) %1 -> Int -> Int -> BO β (Mut α (Vector a))
unsafeSwap = (Mut α (Vector a) -> Int -> Int -> BO β (Mut α (Vector a)))
%1 -> Mut α (Vector a) %1 -> Int -> Int -> BO β (Mut α (Vector a))
forall a b c d (p :: Multiplicity) (q :: Multiplicity)
       (r :: Multiplicity) (x :: Multiplicity) (y :: Multiplicity)
       (z :: Multiplicity).
(a %p -> b %q -> c %r -> d) %1 -> a %x -> b %y -> c %z -> d
Unsafe.toLinear3 \(UnsafeAlias Vector a
v) Int
i Int
j -> Control.do
  () <- IO () %1 -> BO β ()
forall a (α :: Lifetime). IO a %1 -> BO α a
unsafeSystemIOToBO (IO () %1 -> BO β ()) -> IO () %1 -> BO β ()
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ MVector (PrimState IO) a -> Int -> Int -> IO ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> Int -> m ()
MV.unsafeSwap Vector a
v.content Int
i Int
j
  Control.pure $ UnsafeAlias v

swap :: (HasCallStack, α >= β) => Mut α (Vector a) %1 -> Int -> Int -> BO β (Mut α (Vector a))
swap :: forall (α :: Lifetime) (β :: Lifetime) a.
(HasCallStack, α >= β) =>
Mut α (Vector a) %1 -> Int -> Int -> BO β (Mut α (Vector a))
swap Mut α (Vector a)
v Int
i Int
j = DataFlow.do
  (len, v) <- Mut α (Vector a) %1 -> (Ur Int, Mut α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
size Mut α (Vector a)
v
  case len of
    Ur Int
len ->
      if Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
< Int
0 Bool %1 -> Bool %1 -> Bool
|| Int
i Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
>= Int
len Bool %1 -> Bool %1 -> Bool
|| Int
j Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
< Int
0 Bool %1 -> Bool %1 -> Bool
|| Int
j Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
>= Int
len
        then String -> Mut α (Vector a) %1 -> BO β (Mut α (Vector a))
forall a. HasCallStack => String -> a
error (String
"swap: index out of bound: " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> (Int, Int) -> String
forall a. Show a => a -> String
show (Int
i, Int
j) String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> String
" for length " String %1 -> String %1 -> String
forall a. Semigroup a => a %1 -> a %1 -> a
<> Int -> String
forall a. Show a => a -> String
show Int
len) Mut α (Vector a)
v
        else Mut α (Vector a) %1 -> Int -> Int -> BO β (Mut α (Vector a))
forall (α :: Lifetime) (β :: Lifetime) a.
(α >= β) =>
Mut α (Vector a) %1 -> Int -> Int -> BO β (Mut α (Vector a))
unsafeSwap Mut α (Vector a)
v Int
i Int
j

copyAt :: (Copyable a, α >= β) => Int -> Share α (Vector a) -> BO β (Ur a)
copyAt :: forall a (α :: Lifetime) (β :: Lifetime).
(Copyable a, α >= β) =>
Int -> Share α (Vector a) -> BO β (Ur a)
copyAt Int
i Share α (Vector a)
v = Control.do Ur s <- Borrow 'Share α a %1 -> Ur (Borrow 'Share α a)
forall a. Movable a => a %1 -> Ur a
move (Borrow 'Share α a %1 -> Ur (Borrow 'Share α a))
%1 -> BO β (Borrow 'Share α a) %1 -> BO β (Ur (Borrow 'Share α a))
forall (f :: * -> *) a b.
Functor f =>
(a %1 -> b) %1 -> f a %1 -> f b
Control.<$> Int -> Share α (Vector a) %1 -> BO β (Borrow 'Share α a)
forall (α :: Lifetime) (β :: Lifetime) (bk :: BorrowKind) a.
(HasCallStack, α >= β) =>
Int -> Borrow bk α (Vector a) %1 -> BO β (Borrow bk α a)
get Int
i Share α (Vector a)
v; Control.pure $ Ur $ copy s

copyAtMut :: forall a α β. (Copyable a, α >= β) => Int -> Mut α (Vector a) %1 -> BO β (Ur a, Mut α (Vector a))
copyAtMut :: forall a (α :: Lifetime) (β :: Lifetime).
(Copyable a, α >= β) =>
Int -> Mut α (Vector a) %1 -> BO β (Ur a, Mut α (Vector a))
copyAtMut Int
i Mut α (Vector a)
v = BO α (Ur a, Mut α (Vector a)) %1 -> BO β (Ur a, Mut α (Vector a))
forall a b. (a <: b) => a %1 -> b
upcast (BO α (Ur a, Mut α (Vector a)) %1 -> BO β (Ur a, Mut α (Vector a)))
-> BO α (Ur a, Mut α (Vector a))
%1 -> BO β (Ur a, Mut α (Vector a))
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ forall (α :: Lifetime) (α' :: Lifetime) a r.
Mut α a
%1 -> (forall (β :: Lifetime). Share (β /\ α) a -> BO (β /\ α') r)
%1 -> BO α' (r, Mut α a)
sharing @_ @α Mut α (Vector a)
v ((forall (β :: Lifetime).
  Share (β /\ α) (Vector a) -> BO (β /\ α) (Ur a))
 %1 -> BO α (Ur a, Mut α (Vector a)))
%1 -> (forall (β :: Lifetime).
       Share (β /\ α) (Vector a) -> BO (β /\ α) (Ur a))
%1 -> BO α (Ur a, Mut α (Vector a))
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ Int -> Share (β /\ α) (Vector a) -> BO (β /\ α) (Ur a)
forall a (α :: Lifetime) (β :: Lifetime).
(Copyable a, α >= β) =>
Int -> Share α (Vector a) -> BO β (Ur a)
copyAt Int
i

-- | Applies an in-place mutation on 'V.MVector' from @vector@ package.
inplace ::
  (α >= β) =>
  (forall s. V.MVector s a -> ST s ()) %1 ->
  Mut α (Vector a) %1 ->
  BO β (Mut α (Vector a))
{-# INLINE inplace #-}
inplace :: forall (α :: Lifetime) (β :: Lifetime) a.
(α >= β) =>
(forall s. MVector s a -> ST s ())
%1 -> Mut α (Vector a) %1 -> BO β (Mut α (Vector a))
inplace = ((forall s. MVector s a -> ST s ())
 -> Mut α (Vector a) -> BO β (Mut α (Vector a)))
%1 -> (forall s. MVector s a -> ST s ())
%1 -> Mut α (Vector a)
%1 -> BO β (Mut α (Vector a))
forall a b c (p :: Multiplicity) (q :: Multiplicity)
       (x :: Multiplicity) (y :: Multiplicity).
(a %p -> b %q -> c) %1 -> a %x -> b %y -> c
Unsafe.toLinear2 \forall s. MVector s a -> ST s ()
f (UnsafeAlias Vector a
v) -> Control.do
  !() <- ST RealWorld () %1 -> BO β ()
forall s a (α :: Lifetime). ST s a %1 -> BO α a
unsafeSTToBO (ST RealWorld () %1 -> BO β ()) -> ST RealWorld () %1 -> BO β ()
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ MVector RealWorld a -> ST RealWorld ()
forall s. MVector s a -> ST s ()
f (MVector RealWorld a -> ST RealWorld ())
-> MVector RealWorld a -> ST RealWorld ()
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ Vector a -> MVector RealWorld a
forall a. Vector a -> MVector RealWorld a
content (Vector a -> MVector RealWorld a)
-> Vector a -> MVector RealWorld a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ Vector a %1 -> Vector a
forall a b. Coercible a b => a %1 -> b
coerceLin Vector a
v
  Control.pure (UnsafeAlias v)

{- | A simple parallel implementation of quicksort.
It uses a sequential divide-and-conquer when size <8,
and parallel divide-and-conquer with 'parBO' otherwise.

This is meant to be a demonstrative implementation and
not practical - you need a genuine parallel scheduler
to scale this up.
-}
qsort ::
  forall a α β.
  (Ord a, Copyable a, α >= β) =>
  {- | Cost for using parallelism. Halved after each recursive call,
  and stops parallelizing when it reaches 1.
  -}
  Word ->
  Mut α (Vector a) %1 ->
  BO β ()
qsort :: forall a (α :: Lifetime) (β :: Lifetime).
(Ord a, Copyable a, α >= β) =>
Word -> Mut α (Vector a) %1 -> BO β ()
qsort = Word -> Borrow 'Mut α (Vector a) %1 -> BO β ()
go
  where
    go :: Word -> Mut α (Vector a) %1 -> BO β ()
    go :: Word -> Borrow 'Mut α (Vector a) %1 -> BO β ()
go Word
budget Borrow 'Mut α (Vector a)
v = case Borrow 'Mut α (Vector a) %1 -> (Ur Int, Borrow 'Mut α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Borrow bk α (Vector a) %1 -> (Ur Int, Borrow bk α (Vector a))
size Borrow 'Mut α (Vector a)
v of
      (Ur Int
0, Borrow 'Mut α (Vector a)
v) -> () %1 -> BO β ()
forall a. a %1 -> BO β a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure (() %1 -> BO β ()) -> () %1 -> BO β ()
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ Borrow 'Mut α (Vector a) %1 -> ()
forall a. Consumable a => a %1 -> ()
consume Borrow 'Mut α (Vector a)
v
      (Ur Int
1, Borrow 'Mut α (Vector a)
v) -> () %1 -> BO β ()
forall a. a %1 -> BO β a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure (() %1 -> BO β ()) -> () %1 -> BO β ()
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ Borrow 'Mut α (Vector a) %1 -> ()
forall a. Consumable a => a %1 -> ()
consume Borrow 'Mut α (Vector a)
v
      (Ur Int
n, Borrow 'Mut α (Vector a)
v) -> Control.do
        let i :: Int
i = Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`quot` Int
2
        (Ur pivot, v) <- Int
-> Borrow 'Mut α (Vector a)
%1 -> BO β (Ur a, Borrow 'Mut α (Vector a))
forall a (α :: Lifetime) (β :: Lifetime).
(Copyable a, α >= β) =>
Int -> Mut α (Vector a) %1 -> BO β (Ur a, Mut α (Vector a))
copyAtMut Int
i Borrow 'Mut α (Vector a)
v
        (lo, hi) <- divide pivot v 0 n
        let b' = Word
budget Word -> Word -> Word
forall a. Integral a => a -> a -> a
`quot` Word
2
        Control.void $ parIf (b' NonLinear.> 0) (go b' lo) (go b' hi)

parIf :: Bool %1 -> BO α a %1 -> BO α b %1 -> BO α (a, b)
{-# INLINE parIf #-}
parIf :: forall (α :: Lifetime) a b.
Bool %1 -> BO α a %1 -> BO α b %1 -> BO α (a, b)
parIf Bool
p = if Bool
p then BO α a %1 -> BO α b %1 -> BO α (a, b)
forall (α :: Lifetime) a b. BO α a %1 -> BO α b %1 -> BO α (a, b)
parBO else (a %1 -> b %1 -> (a, b))
%1 -> BO α a %1 -> BO α b %1 -> BO α (a, b)
forall a b c.
(a %1 -> b %1 -> c) %1 -> BO α a %1 -> BO α b %1 -> BO α c
forall (f :: * -> *) a b c.
Applicative f =>
(a %1 -> b %1 -> c) %1 -> f a %1 -> f b %1 -> f c
Control.liftA2 (,)

divide ::
  (Ord a, Copyable a, α >= β) =>
  a ->
  Mut α (Vector a) %1 ->
  Int ->
  Int ->
  BO β (Mut α (Vector a), Mut α (Vector a))
divide :: forall a (α :: Lifetime) (β :: Lifetime).
(Ord a, Copyable a, α >= β) =>
a
-> Mut α (Vector a)
%1 -> Int
-> Int
-> BO β (Mut α (Vector a), Mut α (Vector a))
divide a
pivot = Mut α (Vector a)
%1 -> Int -> Int -> BO β (Mut α (Vector a), Mut α (Vector a))
partUp
  where
    partUp :: Mut α (Vector a)
%1 -> Int -> Int -> BO β (Mut α (Vector a), Mut α (Vector a))
partUp Mut α (Vector a)
v Int
l Int
u
      | Int
l Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
< Int
u = Control.do
          (Ur e, v) <- Int -> Mut α (Vector a) %1 -> BO β (Ur a, Mut α (Vector a))
forall a (α :: Lifetime) (β :: Lifetime).
(Copyable a, α >= β) =>
Int -> Mut α (Vector a) %1 -> BO β (Ur a, Mut α (Vector a))
copyAtMut Int
l Mut α (Vector a)
v
          if e < pivot
            then partUp v (l + 1) u
            else partDown v l (u - 1)
      | Bool
otherwise = (Mut α (Vector a), Mut α (Vector a))
%1 -> BO β (Mut α (Vector a), Mut α (Vector a))
forall a. a %1 -> BO β a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure ((Mut α (Vector a), Mut α (Vector a))
 %1 -> BO β (Mut α (Vector a), Mut α (Vector a)))
-> (Mut α (Vector a), Mut α (Vector a))
%1 -> BO β (Mut α (Vector a), Mut α (Vector a))
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ Int
%1 -> Mut α (Vector a) %1 -> (Mut α (Vector a), Mut α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Int
%1 -> Borrow bk α (Vector a)
%1 -> (Borrow bk α (Vector a), Borrow bk α (Vector a))
splitAt Int
l Mut α (Vector a)
v
    partDown :: Mut α (Vector a)
%1 -> Int -> Int -> BO β (Mut α (Vector a), Mut α (Vector a))
partDown Mut α (Vector a)
v Int
l Int
u
      | Int
l Int %1 -> Int %1 -> Bool
forall a. Ord a => a %1 -> a %1 -> Bool
< Int
u = Control.do
          (Ur e, v) <- Int -> Mut α (Vector a) %1 -> BO β (Ur a, Mut α (Vector a))
forall a (α :: Lifetime) (β :: Lifetime).
(Copyable a, α >= β) =>
Int -> Mut α (Vector a) %1 -> BO β (Ur a, Mut α (Vector a))
copyAtMut Int
u Mut α (Vector a)
v
          if pivot < e
            then partDown v l (u - 1)
            else Control.do
              v <- unsafeSwap v l u
              partUp v (l + 1) u
      | Bool
otherwise = (Mut α (Vector a), Mut α (Vector a))
%1 -> BO β (Mut α (Vector a), Mut α (Vector a))
forall a. a %1 -> BO β a
forall (f :: * -> *) a. Applicative f => a %1 -> f a
Control.pure ((Mut α (Vector a), Mut α (Vector a))
 %1 -> BO β (Mut α (Vector a), Mut α (Vector a)))
-> (Mut α (Vector a), Mut α (Vector a))
%1 -> BO β (Mut α (Vector a), Mut α (Vector a))
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ Int
%1 -> Mut α (Vector a) %1 -> (Mut α (Vector a), Mut α (Vector a))
forall (bk :: BorrowKind) (α :: Lifetime) a.
Int
%1 -> Borrow bk α (Vector a)
%1 -> (Borrow bk α (Vector a), Borrow bk α (Vector a))
splitAt Int
l Mut α (Vector a)
v