{-# 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 (Ur a) = a

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

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

instance Prelude.Functor Ur where
  fmap f (Ur a) = Ur (f a)

instance Prelude.Foldable Ur where
  foldMap f (Ur x) = f x

instance Prelude.Traversable Ur where
  sequenceA (Ur x) = Prelude.fmap Ur x

instance Prelude.Applicative Ur where
  pure = Ur
  Ur f <*> Ur x = Ur (f x)

instance Prelude.Monad Ur where
  Ur a >>= f = f 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 rur = to' rur
    where
      to' :: Rep (Ur a) p %1 -> Ur a
      to' (M1 (M1 (M1 (MP1 (K1 a))))) = Ur a

  from ur = from' ur
    where
      from' :: Ur a %1 -> Rep (Ur a) p
      from' (Ur a) = M1 (M1 (M1 (MP1 (K1 a))))

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

  to1 rur = to1' rur
    where
      to1' :: Rep1 Ur a %1 -> Ur a
      to1' (M1 (M1 (M1 (MP1 (Par1 a))))) = Ur a

  from1 ur = from1' ur
    where
      from1' :: Ur a %1 -> Rep1 Ur a
      from1' (Ur a) = M1 (M1 (M1 (MP1 (Par1 a))))

type family Any :: Meta