{-# 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) = b -> Ur b
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) = c -> Ur c
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) = b -> Ur b
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) = (a -> Ur a) -> f a -> f (Ur a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Prelude.fmap a -> Ur a
forall a. a -> Ur a
Ur f a
x

instance Prelude.Applicative Ur where
  pure :: forall a. a -> Ur a
pure = a -> Ur a
forall a. a -> Ur a
Ur
  Ur a -> b
f <*> :: forall a b. Ur (a -> b) -> Ur a -> Ur b
<*> Ur a
x = b -> Ur b
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 = Rep (Ur a) p %1 -> Ur a
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))))) = a -> Ur 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 = Ur a %1 -> Rep (Ur a) p
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) = M1
  C
  ('MetaCons "Ur" 'PrefixI 'False)
  (M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (MP1 'Many (K1 R a)))
  p
-> M1
     D
     ('MetaData
        "Ur"
        "Data.Unrestricted.Linear.Internal.Ur"
        "linear-base-0.2.0-inplace"
        'False)
     (M1
        C
        ('MetaCons "Ur" 'PrefixI 'False)
        (M1
           S
           ('MetaSel
              'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
           (MP1 'Many (K1 R a))))
     p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (M1
  S
  ('MetaSel
     'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
  (MP1 'Many (K1 R a))
  p
-> M1
     C
     ('MetaCons "Ur" 'PrefixI 'False)
     (M1
        S
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (MP1 'Many (K1 R a)))
     p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (MP1 'Many (K1 R a) p
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (MP1 'Many (K1 R a))
     p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (K1 R a p -> MP1 'Many (K1 R a) p
forall {k} (b :: k -> *) (c :: k) (a :: Multiplicity).
b c %a -> MP1 a b c
MP1 (a -> K1 R a p
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 = Rep1 Ur p %1 -> Ur p
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))))) = a -> Ur a
forall a. a -> Ur a
Ur a
a

  from1 :: forall p (m :: Multiplicity). Ur p %m -> Rep1 Ur p
from1 Ur p
ur = Ur p %1 -> Rep1 Ur p
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) = M1
  C
  ('MetaCons "Ur" 'PrefixI 'False)
  (M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (MP1 'Many Par1))
  a
-> M1
     D
     ('MetaData
        "Ur"
        "Data.Unrestricted.Linear.Internal.Ur"
        "linear-base-0.2.0-inplace"
        'False)
     (M1
        C
        ('MetaCons "Ur" 'PrefixI 'False)
        (M1
           S
           ('MetaSel
              'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
           (MP1 'Many Par1)))
     a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (M1
  S
  ('MetaSel
     'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
  (MP1 'Many Par1)
  a
-> M1
     C
     ('MetaCons "Ur" 'PrefixI 'False)
     (M1
        S
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (MP1 'Many Par1))
     a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (MP1 'Many Par1 a
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (MP1 'Many Par1)
     a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Par1 a -> MP1 'Many Par1 a
forall {k} (b :: k -> *) (c :: k) (a :: Multiplicity).
b c %a -> MP1 a b c
MP1 (a -> Par1 a
forall p. p -> Par1 p
Par1 a
a))))

type family Any :: Meta