{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
-- for GHC.Types
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK hide #-}

module Data.Unrestricted.Linear.Internal.Ur
  ( Ur (..),
    unur,
    lift,
    lift2,
  )
where

import qualified GHC.Generics as GHCGen
import GHC.Types (Multiplicity (..))
import Generics.Linear
import Prelude.Linear.GenericUtil
import qualified Prelude

-- | @Ur a@ represents unrestricted values of type @a@ in a linear
-- context. The key idea is that because the contructor holds @a@ with a
-- regular arrow, a function that uses @Ur a@ linearly can use @a@
-- however it likes.
--
-- > someLinear :: Ur a %1-> (a,a)
-- > someLinear (Ur a) = (a,a)
data Ur a where
  Ur :: a -> Ur a

deriving instance GHCGen.Generic (Ur a)

deriving instance GHCGen.Generic1 Ur

-- | Get an @a@ out of an @Ur a@. If you call this function on a
-- linearly bound @Ur a@, then the @a@ you get out has to be used
-- linearly, for example:
--
-- > restricted :: Ur a %1-> b
-- > restricted x = f (unur x)
-- >   where
-- >     -- f __must__ be linear
-- >     f :: a %1-> b
-- >     f x = ...
unur :: Ur a %1 -> a
unur :: forall a. Ur a %1 -> a
unur (Ur a
a) = a
a

-- | Lifts a function on a linear @Ur a@.
lift :: (a -> b) -> Ur a %1 -> Ur b
lift :: forall a b. (a -> b) -> Ur a %1 -> Ur b
lift a -> b
f (Ur a
a) = forall a. a -> Ur a
Ur (a -> b
f a
a)

-- | Lifts a function to work on two linear @Ur a@.
lift2 :: (a -> b -> c) -> Ur a %1 -> Ur b %1 -> Ur c
lift2 :: forall a b c. (a -> b -> c) -> Ur a %1 -> Ur b %1 -> Ur c
lift2 a -> b -> c
f (Ur a
a) (Ur b
b) = forall a. a -> Ur a
Ur (a -> b -> c
f a
a b
b)

instance Prelude.Functor Ur where
  fmap :: forall a b. (a -> b) -> Ur a -> Ur b
fmap a -> b
f (Ur a
a) = forall a. a -> Ur a
Ur (a -> b
f a
a)

instance Prelude.Foldable Ur where
  foldMap :: forall m a. Monoid m => (a -> m) -> Ur a -> m
foldMap a -> m
f (Ur a
x) = a -> m
f a
x

instance Prelude.Traversable Ur where
  sequenceA :: forall (f :: * -> *) a. Applicative f => Ur (f a) -> f (Ur a)
sequenceA (Ur f a
x) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Prelude.fmap forall a. a -> Ur a
Ur f a
x

instance Prelude.Applicative Ur where
  pure :: forall a. a -> Ur a
pure = forall a. a -> Ur a
Ur
  Ur a -> b
f <*> :: forall a b. Ur (a -> b) -> Ur a -> Ur b
<*> Ur a
x = forall a. a -> Ur a
Ur (a -> b
f a
x)

instance Prelude.Monad Ur where
  Ur a
a >>= :: forall a b. Ur a -> (a -> Ur b) -> Ur b
>>= a -> Ur b
f = a -> Ur b
f a
a

-- -------------------
-- Generic and Generic1 instances

instance Generic (Ur a) where
  type
    Rep (Ur a) =
      FixupMetaData
        (Ur a)
        ( D1
            Any
            ( C1
                Any
                ( S1
                    Any
                    (MP1 'Many (Rec0 a))
                )
            )
        )
  to :: forall p (m :: Multiplicity). Rep (Ur a) p %m -> Ur a
to Rep (Ur a) p
rur = forall a p. Rep (Ur a) p %1 -> Ur a
to' Rep (Ur a) p
rur
    where
      to' :: Rep (Ur a) p %1 -> Ur a
      to' :: forall a p. Rep (Ur a) p %1 -> Ur a
to' (M1 (M1 (M1 (MP1 (K1 a
a))))) = forall a. a -> Ur a
Ur a
a

  from :: forall p (m :: Multiplicity). Ur a %m -> Rep (Ur a) p
from Ur a
ur = forall a p. Ur a %1 -> Rep (Ur a) p
from' Ur a
ur
    where
      from' :: Ur a %1 -> Rep (Ur a) p
      from' :: forall a p. Ur a %1 -> Rep (Ur a) p
from' (Ur a
a) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall {k} (b :: k -> *) (c :: k) (a :: Multiplicity).
b c %a -> MP1 a b c
MP1 (forall k i c (p :: k). c -> K1 i c p
K1 a
a))))

instance Generic1 Ur where
  type
    Rep1 Ur =
      FixupMetaData1
        Ur
        ( D1
            Any
            ( C1
                Any
                ( S1
                    Any
                    (MP1 'Many Par1)
                )
            )
        )

  to1 :: forall p (m :: Multiplicity). Rep1 Ur p %m -> Ur p
to1 Rep1 Ur p
rur = forall a. Rep1 Ur a %1 -> Ur a
to1' Rep1 Ur p
rur
    where
      to1' :: Rep1 Ur a %1 -> Ur a
      to1' :: forall a. Rep1 Ur a %1 -> Ur a
to1' (M1 (M1 (M1 (MP1 (Par1 a
a))))) = forall a. a -> Ur a
Ur a
a

  from1 :: forall p (m :: Multiplicity). Ur p %m -> Rep1 Ur p
from1 Ur p
ur = forall a. Ur a %1 -> Rep1 Ur a
from1' Ur p
ur
    where
      from1' :: Ur a %1 -> Rep1 Ur a
      from1' :: forall a. Ur a %1 -> Rep1 Ur a
from1' (Ur a
a) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall {k} (b :: k -> *) (c :: k) (a :: Multiplicity).
b c %a -> MP1 a b c
MP1 (forall p. p -> Par1 p
Par1 a
a))))

type family Any :: Meta