{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoImplicitPrelude #-}
-- TODO: Disabled while we still support GHC 9.2 to enable
-- the import of the empty TypeEq module there.
{-# OPTIONS_GHC -Wno-dodgy-exports -Wno-unused-imports #-}
{-# OPTIONS_HADDOCK hide #-}

-- | This is a very very simple prelude, which doesn't depend on anything else
-- in the linear-base library.
module Prelude.Linear.Internal
  ( module Prelude.Linear.Internal,
    module Prelude.Linear.Internal.TypeEq,
  )
where

import Data.Coerce
import Data.Functor.Identity
import GHC.Exts (TYPE)
import Prelude.Linear.Internal.TypeEq

-- A note on implementation: to avoid silly mistakes, very easy functions are
-- simply reimplemented here. For harder function, we reuse the Prelude
-- definition and make an unsafe cast.

($) :: forall {rep} a (b :: TYPE rep) p q. (a %p -> b) %q -> a %p -> b
$ :: forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
($) a %p -> b
f a
x = a %p -> b
f a
x

infixr 0 $ -- same fixity as base.$

(&) :: forall {rep} a (b :: TYPE rep) p q. a %p -> (a %p -> b) %q -> b
a
x & :: forall a b (p :: Multiplicity) (q :: Multiplicity).
a %p -> (a %p -> b) %q -> b
& a %p -> b
f = a %p -> b
f a
x

infixl 1 & -- same fixity as base.&

id :: a %q -> a
id :: forall a (q :: Multiplicity). a %q -> a
id a
x = a
x

const :: a %q -> b -> a
const :: forall a b (q :: Multiplicity). a %q -> b -> a
const a
x b
_ = a
x

-- | @seq x y@ only forces @x@ to head normal form, therefore is not guaranteed
-- to consume @x@ when the resulting computation is consumed. Therefore, @seq@
-- cannot be linear in it's first argument.
seq :: a -> b %q -> b
seq :: forall a b (q :: Multiplicity). a -> b %q -> b
seq !a
_ b
y = b
y

infixr 0 `seq` -- same fixity as base.seq

($!) :: forall {rep} a (b :: TYPE rep) p q. (a %p -> b) %q -> a %p -> b
$! :: forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
($!) a %p -> b
f !a
a = a %p -> b
f a
a

infixr 0 $! -- same fixity as base.$!

curry :: ((a, b) %p -> c) %q -> a %p -> b %p -> c
curry :: forall a b c (p :: Multiplicity) (q :: Multiplicity).
((a, b) %p -> c) %q -> a %p -> b %p -> c
curry (a, b) %p -> c
f a
x b
y = (a, b) %p -> c
f (a
x, b
y)

uncurry :: (a %p -> b %p -> c) %q -> (a, b) %p -> c
uncurry :: forall a b c (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b %p -> c) %q -> (a, b) %p -> c
uncurry a %p -> b %p -> c
f (a
x, b
y) = a %p -> b %p -> c
f a
x b
y

-- | Beware: @(.)@ is not compatible with the standard one because it is
-- higher-order and we don't have sufficient multiplicity polymorphism yet.
(.) :: forall {rep} b (c :: TYPE rep) a q m n. (b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
b %1 -> c
f . :: forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. a %1 -> b
g = \a
x -> b %1 -> c
f (a %1 -> b
g a
x)

infixr 9 . -- same fixity as base..

-- | Convenience operator when a higher-order function expects a non-linear
-- arrow but we have a linear arrow.
forget :: forall {rep} a (b :: TYPE rep). (a %1 -> b) %1 -> a -> b
forget :: forall a b. (a %1 -> b) %1 -> a -> b
forget a %1 -> b
f a
a = a %1 -> b
f a
a

-- XXX: Temporary, until newtype record projections are linear.
runIdentity' :: Identity a %p -> a
runIdentity' :: forall a (p :: Multiplicity). Identity a %p -> a
runIdentity' (Identity a
x) = a
x

-- | A linear version of 'Data.Coerce.coerce' for types of kind 'Data.Kind.Type'.
lcoerce :: forall a b. (Coercible a b) => a %1 -> b
lcoerce :: forall a b. Coercible a b => a %1 -> b
lcoerce = coerce :: forall a b. Coercible a b => a -> b
coerce ((\a
x -> a
x) :: a %1 -> a)
{-# INLINE CONLIKE lcoerce #-}