Add IsIn and IsSubAPI constraints
This commit is contained in:
parent
09c8464a5a
commit
e9b281f3cc
1 changed files with 50 additions and 5 deletions
|
@ -17,23 +17,30 @@ import Servant.API.Alternative ( type (:<|>) )
|
|||
|
||||
-- * API predicates
|
||||
|
||||
-- | Flatten API into a list of endpoints.
|
||||
type family Endpoints api where
|
||||
Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
|
||||
Endpoints (e :> a) = MapSub e (Endpoints a)
|
||||
Endpoints a = '[a]
|
||||
|
||||
-- ** Lax inclusion
|
||||
|
||||
-- | You may use this type family to tell the type checker that your custom
|
||||
-- type may be skipped as part of a link. This is useful for things like
|
||||
-- 'QueryParam' that are optional in a URI and do not affect them if they are
|
||||
-- @'QueryParam'@ that are optional in a URI and do not affect them if they are
|
||||
-- omitted.
|
||||
--
|
||||
-- >>> data CustomThing
|
||||
-- >>> type instance IsElem' e (CustomThing :> s) = IsElem e s
|
||||
--
|
||||
-- Note that 'IsElem' is called, which will mutually recurse back to `IsElem'`
|
||||
-- Note that @'IsElem'@ is called, which will mutually recurse back to @'IsElem''@
|
||||
-- if it exhausts all other options again.
|
||||
--
|
||||
-- Once you have written a HasLink instance for CustomThing you are ready to
|
||||
-- go.
|
||||
-- Once you have written a @HasLink@ instance for @CustomThing@ you are ready to go.
|
||||
type family IsElem' a s :: Constraint
|
||||
|
||||
-- | Closed type family, check if @endpoint@ is within @api@.
|
||||
-- Uses @'IsElem''@.
|
||||
-- Uses @'IsElem''@ if it exhausts all other options.
|
||||
type family IsElem endpoint api :: Constraint where
|
||||
IsElem e (sa :<|> sb) = Or (IsElem e sa) (IsElem e sb)
|
||||
IsElem (e :> sa) (e :> sb) = IsElem sa sb
|
||||
|
@ -51,10 +58,48 @@ type family IsElem endpoint api :: Constraint where
|
|||
IsElem e e = ()
|
||||
IsElem e a = IsElem' e a
|
||||
|
||||
-- | Check whether @sub@ is a sub API of @api@.
|
||||
type family IsSubAPI sub api :: Constraint where
|
||||
IsSubAPI sub api = AllIsElem (Endpoints sub) api
|
||||
|
||||
-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsElem'@).
|
||||
type family AllIsElem xs api :: Constraint where
|
||||
AllIsElem '[] api = ()
|
||||
AllIsElem (x ': xs) api = (IsElem x api, AllIsElem xs api)
|
||||
|
||||
-- ** Strict inclusion
|
||||
|
||||
-- | Closed type family, check if @endpoint@ is exactly within @api@.
|
||||
-- We aren't sure what affects how an endpoint is built up, so we require an
|
||||
-- exact match.
|
||||
type family IsIn (endpoint :: *) (api :: *) :: Constraint where
|
||||
IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)
|
||||
IsIn (e :> sa) (e :> sb) = IsIn sa sb
|
||||
IsIn e e = ()
|
||||
|
||||
-- | Check whether @sub@ is a sub API of @api@.
|
||||
type family IsStrictSubAPI sub api :: Constraint where
|
||||
IsStrictSubAPI sub api = AllIsIn (Endpoints sub) api
|
||||
|
||||
-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
|
||||
type family AllIsIn xs api :: Constraint where
|
||||
AllIsIn '[] api = ()
|
||||
AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api)
|
||||
|
||||
-- * Helpers
|
||||
|
||||
-- ** Lists
|
||||
|
||||
-- | Apply @(e :>)@ to every API in @xs@.
|
||||
type family MapSub e xs where
|
||||
MapSub e '[] = '[]
|
||||
MapSub e (x ': xs) = (e :> x) ': MapSub e xs
|
||||
|
||||
-- | Append two type-level lists.
|
||||
type family AppendList xs ys where
|
||||
AppendList '[] ys = ys
|
||||
AppendList (x ': xs) ys = x ': AppendList xs ys
|
||||
|
||||
type family IsSubList a b :: Constraint where
|
||||
IsSubList '[] b = ()
|
||||
IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y
|
||||
|
|
Loading…
Reference in a new issue