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 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 FUn FUn = (typ :=: typ) -> Maybe (typ :=: typ)
forall a. a -> Maybe a
Just typ :=: typ
forall a. a :=: a
Refl
  unify FGz FGz = (typ :=: typ) -> Maybe (typ :=: typ)
forall a. a -> Maybe a
Just typ :=: typ
forall a. a :=: a
Refl
  unify _   _   = 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 g :: 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 :: 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 _ = String -> a
forall a. HasCallStack => String -> a
error "inaccessible"

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