module Hackage.Security.Client.Formats (
    -- * Formats
    -- ** Type level
    FormatUn
  , FormatGz
    -- ** Term level
  , Format(..)
  , Formats(..)
    -- * Key membership
  , HasFormat(..)
    -- ** Utility
  , hasFormatAbsurd
  , hasFormatGet
    -- * Map-like operations
  , formatsMap
  , formatsMember
  , formatsLookup
  ) where

import MyPrelude
import Hackage.Security.Util.Stack
import Hackage.Security.Util.TypedEmbedded

{-------------------------------------------------------------------------------
  Formats
-------------------------------------------------------------------------------}

data FormatUn
data FormatGz

-- | Format is a singleton type (reflection type to term level)
--
-- NOTE: In the future we might add further compression formats.
data Format :: * -> * where
  FUn :: Format FormatUn
  FGz :: Format FormatGz

deriving instance Show (Format f)
deriving instance Eq   (Format f)

instance Unify Format where
  unify :: forall typ typ'. Format typ -> Format typ' -> Maybe (typ :=: typ')
unify Format typ
FUn Format typ'
FUn = forall a. a -> Maybe a
Just forall a. a :=: a
Refl
  unify Format typ
FGz Format typ'
FGz = forall a. a -> Maybe a
Just forall a. a :=: a
Refl
  unify Format typ
_   Format typ'
_   = forall a. Maybe a
Nothing

{-------------------------------------------------------------------------------
  Products
-------------------------------------------------------------------------------}

-- | Available formats
--
-- Rather than having a general list here, we enumerate all possibilities.
-- This means we are very precise about what we expect, and we avoid any runtime
-- errors about unexpected format definitions.
--
-- NOTE: If we add additional cases here (for dealing with additional formats)
-- all calls to @error "inaccessible"@ need to be reevaluated.
data Formats :: * -> * -> * where
  FsNone :: Formats () a
  FsUn   :: a -> Formats (FormatUn :- ()) a
  FsGz   :: a -> Formats (FormatGz :- ()) a
  FsUnGz :: a -> a -> Formats (FormatUn :- FormatGz :- ()) a

deriving instance Eq   a => Eq   (Formats fs a)
deriving instance Show a => Show (Formats fs a)

instance Functor (Formats fs) where
  fmap :: forall a b. (a -> b) -> Formats fs a -> Formats fs b
fmap a -> b
g = forall a b fs.
(forall f. Format f -> a -> b) -> Formats fs a -> Formats fs b
formatsMap (\Format f
_format -> a -> b
g)

{-------------------------------------------------------------------------------
  Key membership
-------------------------------------------------------------------------------}

-- | @HasFormat fs f@ is a proof that @f@ is a key in @fs@.
--
-- See 'formatsMember' and 'formatsLookup' for typical usage.
data HasFormat :: * -> * -> * where
  HFZ :: Format f       -> HasFormat (f  :- fs) f
  HFS :: HasFormat fs f -> HasFormat (f' :- fs) f

deriving instance Eq   (HasFormat fs f)
deriving instance Show (HasFormat fs f)

hasFormatAbsurd :: HasFormat () f -> a
hasFormatAbsurd :: forall f a. HasFormat () f -> a
hasFormatAbsurd HasFormat () f
_ = forall a. HasCallStack => String -> a
error String
"inaccessible"

hasFormatGet :: HasFormat fs f -> Format f
hasFormatGet :: forall fs f. HasFormat fs f -> Format f
hasFormatGet (HFZ Format f
f)  = Format f
f
hasFormatGet (HFS HasFormat fs f
hf) = forall fs f. HasFormat fs f -> Format f
hasFormatGet HasFormat fs f
hf

{-------------------------------------------------------------------------------
  Map-like functionality
-------------------------------------------------------------------------------}

formatsMap :: (forall f. Format f -> a -> b) -> Formats fs a -> Formats fs b
formatsMap :: forall a b fs.
(forall f. Format f -> a -> b) -> Formats fs a -> Formats fs b
formatsMap forall f. Format f -> a -> b
_ Formats fs a
FsNone        = forall a. Formats () a
FsNone
formatsMap forall f. Format f -> a -> b
f (FsUn   a
a)    = forall a. a -> Formats (FormatUn :- ()) a
FsUn   (forall f. Format f -> a -> b
f Format FormatUn
FUn a
a)
formatsMap forall f. Format f -> a -> b
f (FsGz   a
a)    = forall a. a -> Formats (FormatGz :- ()) a
FsGz   (forall f. Format f -> a -> b
f Format FormatGz
FGz a
a)
formatsMap forall f. Format f -> a -> b
f (FsUnGz a
a a
a') = forall a. a -> a -> Formats (FormatUn :- (FormatGz :- ())) a
FsUnGz (forall f. Format f -> a -> b
f Format FormatUn
FUn a
a) (forall f. Format f -> a -> b
f Format FormatGz
FGz a
a')

formatsMember :: Format f -> Formats fs a -> Maybe (HasFormat fs f)
formatsMember :: forall f fs a. Format f -> Formats fs a -> Maybe (HasFormat fs f)
formatsMember Format f
_   Formats fs a
FsNone       = forall a. Maybe a
Nothing
formatsMember Format f
FUn (FsUn   a
_  ) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall f fs. Format f -> HasFormat (f :- fs) f
HFZ Format FormatUn
FUn
formatsMember Format f
FUn (FsGz     a
_) = forall a. Maybe a
Nothing
formatsMember Format f
FUn (FsUnGz a
_ a
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall f fs. Format f -> HasFormat (f :- fs) f
HFZ Format FormatUn
FUn
formatsMember Format f
FGz (FsUn   a
_  ) = forall a. Maybe a
Nothing
formatsMember Format f
FGz (FsGz     a
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall f fs. Format f -> HasFormat (f :- fs) f
HFZ Format FormatGz
FGz
formatsMember Format f
FGz (FsUnGz a
_ a
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall fs f f'. HasFormat fs f -> HasFormat (f' :- fs) f
HFS (forall f fs. Format f -> HasFormat (f :- fs) f
HFZ Format FormatGz
FGz)

formatsLookup :: HasFormat fs f -> Formats fs a -> a
formatsLookup :: forall fs f a. HasFormat fs f -> Formats fs a -> a
formatsLookup (HFZ Format f
FUn) (FsUn   a
a  ) = a
a
formatsLookup (HFZ Format f
FUn) (FsUnGz a
a a
_) = a
a
formatsLookup (HFZ Format f
FGz) (FsGz     a
a) = a
a
formatsLookup (HFS HasFormat fs f
hf)  (FsUn   a
_  ) = forall f a. HasFormat () f -> a
hasFormatAbsurd HasFormat fs f
hf
formatsLookup (HFS HasFormat fs f
hf)  (FsGz     a
_) = forall f a. HasFormat () f -> a
hasFormatAbsurd HasFormat fs f
hf
formatsLookup (HFS HasFormat fs f
hf)  (FsUnGz a
_ a
a) = forall fs f a. HasFormat fs f -> Formats fs a -> a
formatsLookup HasFormat fs f
hf (forall a. a -> Formats (FormatGz :- ()) a
FsGz a
a)