module Hackage.Security.Client.Formats (
FormatUn
, FormatGz
, Format(..)
, Formats(..)
, HasFormat(..)
, hasFormatAbsurd
, hasFormatGet
, formatsMap
, formatsMember
, formatsLookup
) where
import Hackage.Security.Util.Stack
import Hackage.Security.Util.TypedEmbedded
data FormatUn
data FormatGz
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
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)
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
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)