{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_HADDOCK hide #-}

module Data.Unrestricted.Linear.Internal.Dupable
  ( Dupable (..),
    genericDupR,
    dup,
    dup3,
    dup4,
    dup5,
    dup6,
    dup7,
    GDupable,
  )
where

import Data.List.NonEmpty (NonEmpty)
import Data.Replicator.Linear.Internal (Replicator (..))
import qualified Data.Replicator.Linear.Internal as Replicator
import Data.Replicator.Linear.Internal.ReplicationStream (ReplicationStream (..))
import qualified Data.Replicator.Linear.Internal.ReplicationStream as ReplicationStream
import qualified Data.Semigroup as Semigroup
import Data.Unrestricted.Linear.Internal.Consumable
import Data.Unrestricted.Linear.Internal.Ur (Ur)
import GHC.Tuple (Solo (..))
import GHC.Types (Multiplicity (..))
import Prelude.Linear.Generically
import Prelude.Linear.Internal
import qualified Unsafe.Linear as Unsafe
import qualified Prelude

-- | The laws of 'Dupable' are dual to those of 'Monoid':
--
-- * 1. @first consume (dup2 a) ≃ a ≃ second consume (dup2 a)@ ('dup2' neutrality)
-- * 2. @first dup2 (dup2 a) ≃ (second dup2 (dup2 a))@ ('dup2' associativity)
--
-- where the @(≃)@ sign represents equality up to type isomorphism.
--
-- * 3. @dup2 = Replicator.elim (,) . dupR@ (coherence between 'dup2' and 'dupR')
-- * 4. @consume = Replicator.elim () . dupR@ (coherence between 'consume' and 'dupR')
--
-- * 5. @Replicator.extract . dupR = id@ ('dupR' identity)
-- * 6. @dupR . dupR = (Replicator.map dupR) . dupR@ ('dupR' interchange)
--
-- (Laws 1-2 and 5-6 are equivalent)
--
-- Implementation of 'Dupable' for 'Data.Unrestricted.Movable' types should
-- be done with @deriving via 'Data.Unrestricted.AsMovable'@.
--
-- Implementation of 'Dupable' for other types can be done with
-- @deriving via 'Generically'@. Note that at present this mechanism
-- can have performance problems for recursive parameterized types.
-- Specifically, the methods will not specialize to underlying 'Dupable'
-- instances. See [this GHC issue](https://gitlab.haskell.org/ghc/ghc/-/issues/21131).
class Consumable a => Dupable a where
  {-# MINIMAL dupR | dup2 #-}

  -- | Creates a 'Replicator' for the given @a@.
  --
  -- You usually want to define this method using 'Replicator'\'s
  -- 'Data.Functor.Linear.Applicative' instance. For instance, here is an
  -- implementation of @'Dupable' [a]@:
  --
  -- > instance Dupable a => Dupable [a] where
  -- >   dupR [] = pure []
  -- >   dupR (a : as) = (:) <$> dupR a <*> dupR as
  dupR :: a %1 -> Replicator a
  dupR a
x = forall a. ReplicationStream a -> Replicator a
Streamed forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ forall s a.
s
-> (s %1 -> a)
-> (s %1 -> (s, s))
-> (s %1 -> ())
-> ReplicationStream a
ReplicationStream a
x forall a (q :: Multiplicity). a %q -> a
id forall a. Dupable a => a %1 -> (a, a)
dup2 forall a. Consumable a => a %1 -> ()
consume

  -- | Creates two @a@s from a @'Dupable' a@, in a linear fashion.
  dup2 :: a %1 -> (a, a)
  dup2 a
x = forall (n :: Nat) a b f.
(Elim (NatToPeano n) a b, IsFunN a b f,
 f ~ FunN (NatToPeano n) a b, n ~ Arity b f) =>
f %1 -> Replicator a %1 -> b
Replicator.elim (,) (forall a. Dupable a => a %1 -> Replicator a
dupR a
x)

-- | Creates 3 @a@s from a @'Dupable' a@, in a linear fashion.
dup3 :: Dupable a => a %1 -> (a, a, a)
dup3 :: forall a. Dupable a => a %1 -> (a, a, a)
dup3 a
x = forall (n :: Nat) a b f.
(Elim (NatToPeano n) a b, IsFunN a b f,
 f ~ FunN (NatToPeano n) a b, n ~ Arity b f) =>
f %1 -> Replicator a %1 -> b
Replicator.elim (,,) (forall a. Dupable a => a %1 -> Replicator a
dupR a
x)

-- | Creates 4 @a@s from a @'Dupable' a@, in a linear fashion.
dup4 :: Dupable a => a %1 -> (a, a, a, a)
dup4 :: forall a. Dupable a => a %1 -> (a, a, a, a)
dup4 a
x = forall (n :: Nat) a b f.
(Elim (NatToPeano n) a b, IsFunN a b f,
 f ~ FunN (NatToPeano n) a b, n ~ Arity b f) =>
f %1 -> Replicator a %1 -> b
Replicator.elim (,,,) (forall a. Dupable a => a %1 -> Replicator a
dupR a
x)

-- | Creates 5 @a@s from a @'Dupable' a@, in a linear fashion.
dup5 :: Dupable a => a %1 -> (a, a, a, a, a)
dup5 :: forall a. Dupable a => a %1 -> (a, a, a, a, a)
dup5 a
x = forall (n :: Nat) a b f.
(Elim (NatToPeano n) a b, IsFunN a b f,
 f ~ FunN (NatToPeano n) a b, n ~ Arity b f) =>
f %1 -> Replicator a %1 -> b
Replicator.elim (,,,,) (forall a. Dupable a => a %1 -> Replicator a
dupR a
x)

-- | Creates 6 @a@s from a @'Dupable' a@, in a linear fashion.
dup6 :: Dupable a => a %1 -> (a, a, a, a, a, a)
dup6 :: forall a. Dupable a => a %1 -> (a, a, a, a, a, a)
dup6 a
x = forall (n :: Nat) a b f.
(Elim (NatToPeano n) a b, IsFunN a b f,
 f ~ FunN (NatToPeano n) a b, n ~ Arity b f) =>
f %1 -> Replicator a %1 -> b
Replicator.elim (,,,,,) (forall a. Dupable a => a %1 -> Replicator a
dupR a
x)

-- | Creates 7 @a@s from a @'Dupable' a@, in a linear fashion.
dup7 :: Dupable a => a %1 -> (a, a, a, a, a, a, a)
dup7 :: forall a. Dupable a => a %1 -> (a, a, a, a, a, a, a)
dup7 a
x = forall (n :: Nat) a b f.
(Elim (NatToPeano n) a b, IsFunN a b f,
 f ~ FunN (NatToPeano n) a b, n ~ Arity b f) =>
f %1 -> Replicator a %1 -> b
Replicator.elim (,,,,,,) (forall a. Dupable a => a %1 -> Replicator a
dupR a
x)

-- | Creates two @a@s from a @'Dupable' a@. Same function as 'dup2'.
dup :: Dupable a => a %1 -> (a, a)
dup :: forall a. Dupable a => a %1 -> (a, a)
dup = forall a. Dupable a => a %1 -> (a, a)
dup2

------------
-- Instances
------------

instance Dupable (ReplicationStream a) where
  dupR :: ReplicationStream a %1 -> Replicator (ReplicationStream a)
dupR = forall a. ReplicationStream a -> Replicator a
Streamed forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall a.
ReplicationStream a %1 -> ReplicationStream (ReplicationStream a)
ReplicationStream.duplicate

instance Dupable (Replicator a) where
  dupR :: Replicator a %1 -> Replicator (Replicator a)
dupR = forall a. Replicator a %1 -> Replicator (Replicator a)
Replicator.duplicate

deriving via
  Generically Prelude.Bool
  instance
    Dupable Prelude.Bool

deriving via
  Generically Prelude.Int
  instance
    Dupable Prelude.Int

deriving via
  Generically Prelude.Word
  instance
    Dupable Prelude.Word

deriving via
  Generically Prelude.Ordering
  instance
    Dupable Prelude.Ordering

deriving via
  Generically Prelude.Char
  instance
    Dupable Prelude.Char

deriving via
  Generically Prelude.Double
  instance
    Dupable Prelude.Double

deriving via
  Generically Prelude.Float
  instance
    Dupable Prelude.Float

deriving via
  Generically (Prelude.Maybe a)
  instance
    Dupable a => Dupable (Prelude.Maybe a)

deriving via
  Generically (Prelude.Either a b)
  instance
    (Dupable a, Dupable b) => Dupable (Prelude.Either a b)

-- This instance is written manually because I (David Feuer) haven't
-- been able to find a way to get the generic version to specialize
-- to a particular underlying Dupable. The recursion leads to the
-- whole thing being a loop breaker and I don't know how to fix that.
instance Dupable a => Dupable [a] where
  dupR :: [a] %1 -> Replicator [a]
dupR = [a] %1 -> Replicator [a]
go
    where
      go :: [a] %1 -> Replicator [a]
      go :: [a] %1 -> Replicator [a]
go [] = forall a. a -> Replicator a
Replicator.pure []
      go (a
x : [a]
xs) = forall a b c.
(a %1 -> b %1 -> c)
-> Replicator a %1 -> Replicator b %1 -> Replicator c
Replicator.liftA2 (:) (forall a. Dupable a => a %1 -> Replicator a
dupR a
x) ([a] %1 -> Replicator [a]
go [a]
xs)

deriving via
  Generically (NonEmpty a)
  instance
    Dupable a => Dupable (NonEmpty a)

deriving via
  Generically (Ur a)
  instance
    Dupable (Ur a)

deriving via
  Generically ()
  instance
    Dupable ()

deriving via
  Generically (Solo a)
  instance
    Dupable a => Dupable (Solo a)

deriving via
  Generically (a, b)
  instance
    (Dupable a, Dupable b) => Dupable (a, b)

deriving via
  Generically (a, b, c)
  instance
    (Dupable a, Dupable b, Dupable c) => Dupable (a, b, c)

deriving via
  Generically (a, b, c, d)
  instance
    (Dupable a, Dupable b, Dupable c, Dupable d) => Dupable (a, b, c, d)

deriving via
  Generically (a, b, c, d, e)
  instance
    (Dupable a, Dupable b, Dupable c, Dupable d, Dupable e) => Dupable (a, b, c, d, e)

deriving newtype instance Dupable a => Dupable (Semigroup.Sum a)

deriving newtype instance Dupable a => Dupable (Semigroup.Product a)

deriving newtype instance Dupable Semigroup.All

deriving newtype instance Dupable Semigroup.Any

-------------------
-- Generic deriving
-------------------

instance (Generic a, GDupable (Rep a)) => Dupable (Generically a) where
  dupR :: Generically a %1 -> Replicator (Generically a)
dupR (Generically a
x) = forall a b. Coercible a b => a %1 -> b
lcoerce (forall a b. (a %1 -> b) -> Replicator a %1 -> Replicator b
Replicator.map (forall a p (m :: Multiplicity). Generic a => Rep a p %m -> a
to :: Rep a x %1 -> a) (forall (f :: * -> *) a. GDupable f => f a %1 -> Replicator (f a)
gdupR (forall a p (m :: Multiplicity). Generic a => a %m -> Rep a p
from a
x)))

genericDupR :: (Generic a, GDupable (Rep a)) => a %1 -> Replicator a
genericDupR :: forall a. (Generic a, GDupable (Rep a)) => a %1 -> Replicator a
genericDupR a
x = forall a b. (a %1 -> b) -> Replicator a %1 -> Replicator b
Replicator.map forall a p (m :: Multiplicity). Generic a => Rep a p %m -> a
to (forall (f :: * -> *) a. GDupable f => f a %1 -> Replicator (f a)
gdupR (forall a p (m :: Multiplicity). Generic a => a %m -> Rep a p
from a
x))

class GConsumable f => GDupable f where
  gdupR :: f a %1 -> Replicator (f a)

instance GDupable f => GDupable (M1 i c f) where
  gdupR :: forall a. M1 i c f a %1 -> Replicator (M1 i c f a)
gdupR (M1 f a
x) = forall a b. Coercible a b => a %1 -> b
lcoerce (forall (f :: * -> *) a. GDupable f => f a %1 -> Replicator (f a)
gdupR f a
x)
  {-# INLINE gdupR #-}

instance (GDupable f, GDupable g) => GDupable (f :*: g) where
  gdupR :: forall a. (:*:) f g a %1 -> Replicator ((:*:) f g a)
gdupR (f a
x :*: g a
y) = forall a b c.
(a %1 -> b %1 -> c)
-> Replicator a %1 -> Replicator b %1 -> Replicator c
Replicator.liftA2 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (forall (f :: * -> *) a. GDupable f => f a %1 -> Replicator (f a)
gdupR f a
x) (forall (f :: * -> *) a. GDupable f => f a %1 -> Replicator (f a)
gdupR g a
y)
  {-# INLINE gdupR #-}

instance (GDupable f, GDupable g) => GDupable (f :+: g) where
  gdupR :: forall a. (:+:) f g a %1 -> Replicator ((:+:) f g a)
gdupR (L1 f a
x) = forall a b. (a %1 -> b) -> Replicator a %1 -> Replicator b
Replicator.map forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall (f :: * -> *) a. GDupable f => f a %1 -> Replicator (f a)
gdupR f a
x)
  gdupR (R1 g a
y) = forall a b. (a %1 -> b) -> Replicator a %1 -> Replicator b
Replicator.map forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall (f :: * -> *) a. GDupable f => f a %1 -> Replicator (f a)
gdupR g a
y)
  {-# INLINE gdupR #-}

instance Dupable c => GDupable (K1 i c) where
  gdupR :: forall a. K1 i c a %1 -> Replicator (K1 i c a)
gdupR = forall a b. Coercible a b => a %1 -> b
lcoerce (forall a. Dupable a => a %1 -> Replicator a
dupR @c)
  {-# INLINE gdupR #-}

instance GDupable U1 where
  gdupR :: forall a. U1 a %1 -> Replicator (U1 a)
gdupR U1 a
U1 = forall a. a -> Replicator a
Replicator.pure forall k (p :: k). U1 p
U1
  {-# INLINE gdupR #-}

instance GDupable V1 where
  gdupR :: forall a. V1 a %1 -> Replicator (V1 a)
gdupR = \case {}
  {-# INLINE gdupR #-}

instance GDupable (MP1 'Many f) where
  gdupR :: forall a. MP1 'Many f a %1 -> Replicator (MP1 'Many f a)
gdupR (MP1 f a
x) = forall a. a -> Replicator a
Replicator.pure (forall {k} (b :: k -> *) (c :: k) (a :: Multiplicity).
b c %a -> MP1 a b c
MP1 f a
x)
  {-# INLINE gdupR #-}

instance GDupable f => GDupable (MP1 'One f) where
  gdupR :: forall a. MP1 'One f a %1 -> Replicator (MP1 'One f a)
gdupR (MP1 f a
x) = forall a b. (a %1 -> b) -> Replicator a %1 -> Replicator b
Replicator.map forall {k} (b :: k -> *) (c :: k) (a :: Multiplicity).
b c %a -> MP1 a b c
MP1 (forall (f :: * -> *) a. GDupable f => f a %1 -> Replicator (f a)
gdupR f a
x)
  {-# INLINE gdupR #-}

instance GDupable UChar where
  gdupR :: forall a. UChar a %1 -> Replicator (UChar a)
gdupR = forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear forall a. a -> Replicator a
Replicator.pure

instance GDupable UDouble where
  gdupR :: forall a. UDouble a %1 -> Replicator (UDouble a)
gdupR = forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear forall a. a -> Replicator a
Replicator.pure

instance GDupable UFloat where
  gdupR :: forall a. UFloat a %1 -> Replicator (UFloat a)
gdupR = forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear forall a. a -> Replicator a
Replicator.pure

instance GDupable UInt where
  gdupR :: forall a. UInt a %1 -> Replicator (UInt a)
gdupR = forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear forall a. a -> Replicator a
Replicator.pure

instance GDupable UWord where
  gdupR :: forall a. UWord a %1 -> Replicator (UWord a)
gdupR = forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear forall a. a -> Replicator a
Replicator.pure