-- For the Route pattern
{-# LANGUAGE PatternSynonyms #-}
-- For the Route pattern
{-# LANGUAGE ViewPatterns #-}

module Webc.Data where

import Data.Kind (Constraint, Type)
import Data.Maybe (Maybe (..))
import Symantic.Derive (Derivable (..), Derived)
import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))

-- * Type 'Route'

{- | Pattern-matchable combinators (initial algebra) for routes.
 This is an extensible data-type indexed by
 the symantic classes (final algebra).
-}
data family
  Route
    (route :: (Type -> Type) -> Constraint) ::
    (Type -> Type) -> (Type -> Type)

type instance Derived (Route route repr) = repr

-- ** Type 'SomeRoute'

{- | Some 'Route' existentialized over
 the actual indexing symantic class.
 Useful for the initial algebra of symantic combinators
 containing at least one 'Route'.
-}
data SomeRoute repr a
  = forall route.
    ( Derivable (Route route repr)
    , Typeable route
    ) =>
    SomeRoute (Route route repr a)

{- | Convenient utility to pattern-match a 'SomeRoute'.
 and bring its constraints in scope.
-}
pattern Route :: Typeable route => Route route repr a -> SomeRoute repr a
pattern Route x <- (unSomeRoute -> Just x)

{- | @(unSomeRoute x :: 'Maybe' ('Route' route repr a))@
 extract the data-constructor from the given 'SomeRoute'
 iif. it belongs to the @('Route' route repr a)@ data-instance.
-}
unSomeRoute ::
  forall route repr a.
  Typeable route =>
  SomeRoute repr a ->
  Maybe (Route route repr a)
unSomeRoute (SomeRoute (x :: Route x repr a)) =
  case typeRep @route `eqTypeRep` typeRep @x of
    Just HRefl -> Just x
    Nothing -> Nothing

type instance Derived (SomeRoute repr) = repr
instance Derivable (SomeRoute repr) where
  derive (SomeRoute x) = derive x