{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# 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
    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 Data.Kind (Type)
import GHC.Exts (Constraint)
import GHC.TypeLits (ErrorMessage (..), TypeError)

import Servant.API.Alternative (type (:<|>))
import Servant.API.Capture (Capture, CaptureAll)
import Servant.API.Fragment
import Servant.API.Generic (ToServantApi)
import Servant.API.Header (Header, Header')
import Servant.API.NamedRoutes (NamedRoutes)
import Servant.API.QueryParam (QueryFlag, QueryParam, QueryParams)
import Servant.API.ReqBody (ReqBody)
import Servant.API.Sub (type (:>))
import Servant.API.UVerb (UVerb)
import Servant.API.Verbs (Verb)

-- * 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
