-- | This is a very very simple prelude, which doesn't depend on anything else
-- in the linear-base library (except possibly "Unsafe.Linear").

{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}

module Prelude.Linear.Internal where

import qualified Prelude as Prelude
import qualified Unsafe.Linear as Unsafe
import Data.Functor.Identity

-- 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.

-- | Beware: @($)@ is not compatible with the standard one because it is
-- higher-order and we don't have multiplicity polymorphism yet.
($) :: (a %1-> b) %1-> a %1-> b
-- XXX: Temporary as `($)` should get its typing rule directly from the type
-- inference mechanism.
$ :: forall a b. (a %1 -> b) %1 -> a %1 -> b
($) a %1 -> b
f a
x = a %1 -> b
f a
x
infixr 0 $

(&) :: a %1-> (a %1-> b) %1-> b
a
x & :: forall a b. a %1 -> (a %1 -> b) %1 -> b
& a %1 -> b
f = a %1 -> b
f a
x
infixl 1 &

id :: a %1-> a
id :: forall a. a %1 -> a
id a
x = a
x

const :: a %1-> b -> a
const :: forall a b. a %1 -> b -> a
const a
x b
_ = a
x

asTypeOf :: a %1-> a -> a
asTypeOf :: forall a. a %1 -> a -> a
asTypeOf = a %1 -> a -> a
forall a b. a %1 -> b -> a
const

-- | @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 %1-> b
seq :: forall a b. a -> b %1 -> b
seq a
x = (b -> b) %1 -> b %1 -> b
forall a b (p :: Multiplicity). (a %p -> b) %1 -> a %1 -> b
Unsafe.toLinear (a -> b -> b
Prelude.seq a
x)

($!) :: (a %1-> b) %1-> a %1-> b
$! :: forall a b. (a %1 -> b) %1 -> a %1 -> b
($!) a %1 -> b
f !a
a = a %1 -> b
f a
a

-- | Beware, 'curry' is not compatible with the standard one because it is
-- higher-order and we don't have multiplicity polymorphism yet.
curry :: ((a, b) %1-> c) %1-> a %1-> b %1-> c
curry :: forall a b c. ((a, b) %1 -> c) %1 -> a %1 -> b %1 -> c
curry (a, b) %1 -> c
f a
x b
y = (a, b) %1 -> c
f (a
x, b
y)

-- | Beware, 'uncurry' is not compatible with the standard one because it is
-- higher-order and we don't have multiplicity polymorphism yet.
uncurry :: (a %1-> b %1-> c) %1-> (a, b) %1-> c
uncurry :: forall a b c. (a %1 -> b %1 -> c) %1 -> (a, b) %1 -> c
uncurry a %1 -> b %1 -> c
f (a
x,b
y) = a %1 -> b %1 -> c
f a
x b
y

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

-- XXX: temporary: with multiplicity polymorphism functions expecting a
-- non-linear arrow would allow a linear arrow passed, so this would be
-- redundant
-- | Convenience operator when a higher-order function expects a non-linear
-- arrow but we have a linear arrow.
forget :: (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 %1-> a
runIdentity' :: forall a. Identity a %1 -> a
runIdentity' (Identity a
x) = a
x