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 :: Format typ -> Format typ' -> Maybe (typ :=: typ')
unify Format typ
FUn Format typ'
FUn = (typ :=: typ) -> Maybe (typ :=: typ)
forall a. a -> Maybe a
Just typ :=: typ
forall a. a :=: a
Refl
  unify Format typ
FGz Format typ'
FGz = (typ :=: typ) -> Maybe (typ :=: typ)
forall a. a -> Maybe a
Just typ :=: typ
forall a. a :=: a
Refl
  unify Format typ
_   Format typ'
_   = Maybe (typ :=: 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 unexpect 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 :: (a -> b) -> Formats fs a -> Formats fs b
fmap a -> b
g = (forall f. Format f -> a -> b) -> Formats fs a -> Formats fs b
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 :: HasFormat () f -> a
hasFormatAbsurd HasFormat () f
_ = String -> a
forall a. HasCallStack => String -> a
error String
"inaccessible"

hasFormatGet :: HasFormat fs f -> Format f
hasFormatGet :: HasFormat fs f -> Format f
hasFormatGet (HFZ Format f
f)  = Format f
f
hasFormatGet (HFS HasFormat fs f
hf) = HasFormat fs f -> Format f
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 f. Format f -> a -> b) -> Formats fs a -> Formats fs b
formatsMap forall f. Format f -> a -> b
_ Formats fs a
FsNone        = Formats fs b
forall a. Formats () a
FsNone
formatsMap forall f. Format f -> a -> b
f (FsUn   a
a)    = b -> Formats (FormatUn :- ()) b
forall a. a -> Formats (FormatUn :- ()) a
FsUn   (Format FormatUn -> a -> b
forall f. Format f -> a -> b
f Format FormatUn
FUn a
a)
formatsMap forall f. Format f -> a -> b
f (FsGz   a
a)    = b -> Formats (FormatGz :- ()) b
forall a. a -> Formats (FormatGz :- ()) a
FsGz   (Format FormatGz -> a -> b
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') = b -> b -> Formats (FormatUn :- (FormatGz :- ())) b
forall a. a -> a -> Formats (FormatUn :- (FormatGz :- ())) a
FsUnGz (Format FormatUn -> a -> b
forall f. Format f -> a -> b
f Format FormatUn
FUn a
a) (Format FormatGz -> a -> b
forall f. Format f -> a -> b
f Format FormatGz
FGz a
a')

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

formatsLookup :: HasFormat fs f -> Formats fs a -> a
formatsLookup :: 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
_  ) = HasFormat () f -> a
forall f a. HasFormat () f -> a
hasFormatAbsurd HasFormat fs f
HasFormat () f
hf
formatsLookup (HFS HasFormat fs f
hf)  (FsGz     a
_) = HasFormat () f -> a
forall f a. HasFormat () f -> a
hasFormatAbsurd HasFormat fs f
HasFormat () f
hf
formatsLookup (HFS HasFormat fs f
hf)  (FsUnGz a
_ a
a) = HasFormat fs f -> Formats fs a -> a
forall fs f a. HasFormat fs f -> Formats fs a -> a
formatsLookup HasFormat fs f
hf (a -> Formats (FormatGz :- ()) a
forall a. a -> Formats (FormatGz :- ()) a
FsGz a
a)