{-# LANGUAGE CPP                      #-}
{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE FlexibleInstances        #-}

{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE UndecidableSuperClasses  #-}

{-|
This module collects utilities for manipulating @servant@ API types. The
functionality in this module is for advanced usage.

The code samples in this module use the following type synonym:

> type SampleAPI = "hello" :> Get '[JSON] Int
>             :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool

-}
module Servant.API.TypeLevel (
    -- $setup
    -- * API predicates
    Endpoints,
    -- ** Lax inclusion
    IsElem',
    IsElem,
    IsSubAPI,
    AllIsElem,
    -- ** Strict inclusion
    IsIn,
    IsStrictSubAPI,
    AllIsIn,
    -- * Helpers
    -- ** Lists
    MapSub,
    AppendList,
    IsSubList,
    Elem,
    ElemGo,
    -- ** Logic
    Or,
    And,
    -- ** Fragment
    FragmentUnique,
    AtMostOneFragment
    ) where


import           GHC.Exts
                 (Constraint)
import           Data.Kind
                 (Type)
import           Servant.API.Alternative
                 (type (:<|>))
import           Servant.API.Capture
                 (Capture, CaptureAll)
import           Servant.API.Fragment
import           Servant.API.Header
                 (Header, Header')
import           Servant.API.QueryParam
                 (QueryFlag, QueryParam, QueryParams)
import           Servant.API.ReqBody
                 (ReqBody)
import           Servant.API.NamedRoutes
                 (NamedRoutes)
import           Servant.API.Generic
                 (ToServantApi)
import           Servant.API.Sub
                 (type (:>))
import           Servant.API.Verbs
                 (Verb)
import           Servant.API.UVerb
                 (UVerb)
import           GHC.TypeLits
                 (ErrorMessage (..), TypeError)



-- * API predicates

-- | Flatten API into a list of endpoints.
--
-- >>> Refl :: Endpoints SampleAPI :~: '["hello" :> Verb 'GET 200 '[JSON] Int, "bye" :> (Capture "name" String :> Verb 'POST 200 '[JSON, PlainText] Bool)]
-- Refl
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
-- omitted.
--
-- >>> data CustomThing
-- >>> type instance IsElem' e (CustomThing :> s) = IsElem e s
--
-- 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.
type family IsElem' a s :: Constraint

-- | Closed type family, check if @endpoint@ is within @api@.
-- Uses @'IsElem''@ if it exhausts all other options.
--
-- >>> ok (Proxy :: Proxy (IsElem ("hello" :> Get '[JSON] Int) SampleAPI))
-- OK
--
-- >>> ok (Proxy :: Proxy (IsElem ("bye" :> Get '[JSON] Int) SampleAPI))
-- ...
-- ... Could not ...
-- ...
--
-- An endpoint is considered within an api even if it is missing combinators
-- that don't affect the URL:
--
-- >>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
-- OK
--
-- >>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (ReqBody '[JSON] Bool :> Get '[JSON] Int)))
-- OK
--
-- *N.B.:* @IsElem a b@ can be seen as capturing the notion of whether the URL
-- represented by @a@ would match the URL represented by @b@, *not* whether a
-- request represented by @a@ matches the endpoints serving @b@ (for the
-- latter, use 'IsIn').
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
  IsElem sa (Header sym x :> sb)          = IsElem sa sb
  IsElem sa (Header' mods sym x :> sb)    = IsElem sa sb
  IsElem sa (ReqBody y x :> sb)           = IsElem sa sb
  IsElem (CaptureAll z y :> sa) (CaptureAll x y :> sb)
                                          = IsElem sa sb
  IsElem (Capture z y :> sa) (Capture x y :> sb)
                                          = IsElem sa sb
  IsElem sa (QueryParam x y :> sb)        = IsElem sa sb
  IsElem sa (QueryParams x y :> sb)       = IsElem sa sb
  IsElem sa (QueryFlag x :> sb)           = IsElem sa sb
  IsElem sa (Fragment x :> sb)            = IsElem sa sb
  IsElem (Verb m s ct typ) (Verb m s ct' typ)
                                          = IsSubList ct ct'
  IsElem e e                              = ()
  IsElem e (NamedRoutes rs)               = IsElem e (ToServantApi rs)
  IsElem e a                              = IsElem' e a

-- | Check whether @sub@ is a sub-API of @api@.
--
-- >>> ok (Proxy :: Proxy (IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int)))
-- OK
--
-- >>> ok (Proxy :: Proxy (IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI))
-- ...
-- ... Could not ...
-- ...
--
-- This uses @IsElem@ for checking; thus the note there applies here.
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@.
--
-- >>> ok (Proxy :: Proxy (IsIn ("hello" :> Get '[JSON] Int) SampleAPI))
-- OK
--
-- Unlike 'IsElem', this requires an *exact* match.
--
-- >>> ok (Proxy :: Proxy (IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
-- ...
-- ... Could not ...
-- ...
type family IsIn (endpoint :: Type) (api :: Type) :: Constraint where
  IsIn e (sa :<|> sb)                = Or (IsIn e sa) (IsIn e sb)
  IsIn (e :> sa) (e :> sb)           = IsIn sa sb
  IsIn e e                           = ()
  IsIn e (NamedRoutes record)        = IsIn e (ToServantApi record)

-- | Check whether @sub@ is a sub API of @api@.
--
-- Like 'IsSubAPI', but uses 'IsIn' rather than 'IsElem'.
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'@).
--
-- >>> ok (Proxy :: Proxy (AllIsIn (Endpoints SampleAPI) SampleAPI))
-- OK
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

-- | Check that a value is an element of a list:
--
-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
-- OK
--
-- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
-- ...
-- ... [Char]...'[Int, Bool...
-- ...
type Elem e es = ElemGo e es es

-- 'orig' is used to store original list for better error messages
type family ElemGo e es orig :: Constraint where
  ElemGo x (x ': xs) orig = ()
  ElemGo y (x ': xs) orig = ElemGo y xs orig
  -- Note [Custom Errors]
  ElemGo x '[] orig       = TypeError ('ShowType x
                                 ':<>: 'Text " expected in list "
                                 ':<>: 'ShowType orig)

-- ** Logic

-- | If either 'a' or 'b' produce an empty constraint, produce an empty constraint.
type family Or (a :: Constraint) (b :: Constraint) :: Constraint where
    -- This works because of:
    -- https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/CoincidentOverlap
  Or () b       = ()
  Or a ()       = ()

-- | If both 'a' or 'b' produce an empty constraint, produce an empty constraint.
type family And (a :: Constraint) (b :: Constraint) :: Constraint where
  And () ()     = ()

{- Note [Custom Errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We might try to factor these our more cleanly, but the type synonyms and type
families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048).
-}

-- ** Fragment

-- | If there is more than one fragment in an API endpoint,
-- a compile-time error is raised.
--
-- >>> type FailAPI = Fragment Bool :> Fragment Int :> Get '[JSON] NoContent
-- >>> instance AtMostOneFragment FailAPI
-- ...
-- ...Only one Fragment allowed per endpoint in api...
-- ...
class FragmentUnique api => AtMostOneFragment api

instance AtMostOneFragment (Verb m s ct typ)

instance AtMostOneFragment (UVerb m cts as)

instance AtMostOneFragment (Fragment a)

type family FragmentUnique api :: Constraint where
  FragmentUnique (sa :<|> sb)       = And (FragmentUnique sa) (FragmentUnique sb)
  FragmentUnique (Fragment a :> sa) = FragmentNotIn sa (Fragment a :> sa)
  FragmentUnique (x :> sa)          = FragmentUnique sa
  FragmentUnique (Fragment a)       = ()
  FragmentUnique x                  = ()

type family FragmentNotIn api orig :: Constraint where
  FragmentNotIn (sa :<|> sb)       orig =
    And (FragmentNotIn sa orig) (FragmentNotIn sb orig)
  FragmentNotIn (Fragment c :> sa) orig = TypeError (NotUniqueFragmentInApi orig)
  FragmentNotIn (x :> sa)          orig = FragmentNotIn sa orig
  FragmentNotIn (Fragment c)       orig = TypeError (NotUniqueFragmentInApi orig)
  FragmentNotIn x                  orig = ()

type NotUniqueFragmentInApi api =
    'Text "Only one Fragment allowed per endpoint in api ‘"
    ':<>: 'ShowType api
    ':<>: 'Text "’."

-- $setup
--
-- The doctests in this module are run with following preamble:
--
-- >>> :set -XPolyKinds
-- >>> :set -XGADTs
-- >>> :set -XTypeSynonymInstances -XFlexibleInstances
-- >>> import Data.Proxy
-- >>> import Data.Type.Equality
-- >>> import Servant.API
-- >>> data OK ctx where OK :: ctx => OK ctx
-- >>> instance Show (OK ctx) where show _ = "OK"
-- >>> let ok :: ctx => Proxy ctx -> OK ctx; ok _ = OK
-- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
-- >>> type FailAPI = Fragment Bool :> Fragment Int :> Get '[JSON] NoContent
-- >>> let sampleAPI = Proxy :: Proxy SampleAPI