{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module : Control.Env.Hierarchical.Internal
-- Description:
-- License: BSD-3
-- Maintainer: autotaker@gmail.com
-- Stability: experimental
module Control.Env.Hierarchical.Internal
  ( Environment (..),
    Extends (..),
    Root (..),
    Field (..),
    Trans (..),
    SomeInterface (SomeInterface),
    Has,
    Has1,
    getL,
    ifaceL,
    runIF,
    rootL,
    extendsL,
  )
where

import Data.Kind (Type)
import Data.Type.Bool (If)
import GHC.TypeLits
  ( ErrorMessage (ShowType, Text, (:<>:)),
    TypeError,
  )
import Lens.Micro (Lens')
import Lens.Micro.Mtl (view)
import RIO (RIO, runRIO)

class Environment env where
  -- | @Super env@ represents the inheritance relation between environments.
  --
  -- * If @env@ owns a field of the form @'Extends' T@, then @T@ is the super environment.
  -- * If @env@ owns no field of the form @'Extends' T@, then 'Root' is the super environment.
  -- * Every @env@ must have at most one field of the form @Extends T@ because multiple inheritance is not supported.
  type Super env

  -- | interfaces that are fields of the environment
  type Fields1 env :: [Type -> Type]

  -- | fields of the environment
  type Fields env :: [Type]

  -- | Lens to super environment
  superL :: Lens' env (Super env)
  {-# INLINE superL #-}
  default superL :: Field (Extends (Super env)) env => Lens' env (Super env)
  superL = (Extends (Super env) -> f (Extends (Super env))) -> env -> f env
forall a env. Field a env => Lens' env a
fieldL ((Extends (Super env) -> f (Extends (Super env))) -> env -> f env)
-> ((Super env -> f (Super env))
    -> Extends (Super env) -> f (Extends (Super env)))
-> (Super env -> f (Super env))
-> env
-> f env
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Super env -> f (Super env))
-> Extends (Super env) -> f (Extends (Super env))
forall x. Lens' (Extends x) x
extendsL

-- | Root environment that does not have any fields.
data Root = Root

-- | Wrapper that represents the super environment.
newtype Extends env = Extends env

{-# INLINE extendsL #-}
extendsL :: Lens' (Extends x) x
extendsL :: (x -> f x) -> Extends x -> f (Extends x)
extendsL x -> f x
f (Extends x
x) = (x -> Extends x) -> f x -> f (Extends x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> Extends x
forall env. env -> Extends env
Extends (x -> f x
f x
x)

rootL :: Lens' x Root
rootL :: (Root -> f Root) -> x -> f x
rootL Root -> f Root
f x
x = x
x x -> f Root -> f x
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Root -> f Root
f Root
Root

instance Environment Root where
  type Super Root = TypeError ('Text "No super environment for Root")
  type Fields1 Root = '[]
  type Fields Root = '[]
  superL :: (Super Root -> f (Super Root)) -> Root -> f Root
superL = (Super Root -> f (Super Root)) -> Root -> f Root
forall a. HasCallStack => a
undefined

-- | direct field of @env@
class Field a env where
  fieldL :: Lens' env a

instance Field env env where
  fieldL :: (env -> f env) -> env -> f env
fieldL = (env -> f env) -> env -> f env
forall a. a -> a
id

-- Addr s t = '[v1, ... vn]
-- s = v1 <: v2 <: ... <: vn = t
-- s = env1 <: env2 <: env3 = Target s '[env2, env3]
-- s = env1 <: env2 = Target s '[env2]
-- s = env1 = Target s '[]
-- Trans env1 [env1]
class Trans s (l :: [Type]) where
  type Target s l
  transL :: Lens' s (Target s l)

instance Trans s '[] where
  type Target s '[] = s
  transL :: (Target s '[] -> f (Target s '[])) -> s -> f s
transL = (Target s '[] -> f (Target s '[])) -> s -> f s
forall a. a -> a
id

instance (Environment s, Super s ~ t, Trans t l) => Trans s (t : l) where
  type Target s (t : l) = Target t l
  transL :: (Target s (t : l) -> f (Target s (t : l))) -> s -> f s
transL = (t -> f t) -> s -> f s
forall env. Environment env => Lens' env (Super env)
superL ((t -> f t) -> s -> f s)
-> ((Target t l -> f (Target t l)) -> t -> f t)
-> (Target t l -> f (Target t l))
-> s
-> f s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trans t l => Lens' t (Target t l)
forall s (l :: [*]). Trans s l => Lens' s (Target s l)
transL @t @l

-- env1 <: env2 <: env3
-- Addr env1 env3 = [env2, env3]
-- Addr env2 env3 = [env3]
-- Addr env3 env3 = []
type family Addr a :: [Type] where
  Addr Root = '[]
  Addr a = Super a ': Addr (Super a)

type family Member (f :: k) (l :: [k]) :: Bool where
  Member f '[] = 'False
  Member f (f : l) = 'True
  Member f (g : l) = Member f l

-- X <- Env1, FindEnv X Env1 [Env2,Root] => []
-- X <- Env2, FindEnv X Env1 [Env2,Root] => [Env2]
type family FindEnv (f :: Type) env (envs :: [Type]) :: [Type] where
  FindEnv f env (env' ': envs) = If (Member f (Fields env)) '[] (env' : FindEnv f env' envs)
  FindEnv f env '[] = TypeError ('Text "No environment has " ':<>: 'ShowType f)

type family FindEnv1 (f :: Type -> Type) env (envs :: [Type]) :: [Type] where
  FindEnv1 f env (env' ': envs) = If (Member f (Fields1 env)) '[] (env' : FindEnv1 f env' envs)
  FindEnv1 f env '[] = TypeError ('Text "No environment has " ':<>: 'ShowType f)

data SomeInterface f env where
  SomeInterface :: Lens' env' (f env') -> Lens' env env' -> SomeInterface f env

type HasAux a env route = (Trans env route, Field a (Target env route))

type Has1Aux f env route = (Trans env route, Field (f (Target env route)) (Target env route))

-- | Type constraint meaning @env@ contains @a@ as a (including ancestors') field.
--
-- An environment @env@ contains unique value for each type @T@ that satisfies
-- @Has T env@. If you want to depends on multiple values of the same type,
-- please distinguish them by using newtype.
type family Has a env where
  Has a env = HasAux a env (FindEnv a env (Addr env))

-- | Type constraint meaning @env@ contains @f env'@ for some ancestor @env'@
type family Has1 f env where
  Has1 f env = Has1Aux f env (FindEnv1 f env (Addr env))

-- | Lens to extract @a@ from @env@
getL :: forall a env. Has a env => Lens' env a
getL :: Lens' env a
getL = Trans env (FindEnv a env (Addr env)) =>
Lens' env (Target env (FindEnv a env (Addr env)))
forall s (l :: [*]). Trans s l => Lens' s (Target s l)
transL @env @(FindEnv a env (Addr env)) ((Target env (FindEnv a env (Addr env))
  -> f (Target env (FindEnv a env (Addr env))))
 -> env -> f env)
-> ((a -> f a)
    -> Target env (FindEnv a env (Addr env))
    -> f (Target env (FindEnv a env (Addr env))))
-> (a -> f a)
-> env
-> f env
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a)
-> Target env (FindEnv a env (Addr env))
-> f (Target env (FindEnv a env (Addr env)))
forall a env. Field a env => Lens' env a
fieldL

ifaceL :: forall f env. Has1 f env => SomeInterface f env
ifaceL :: SomeInterface f env
ifaceL =
  Lens'
  (Target env (FindEnv1 f env (Addr env)))
  (f (Target env (FindEnv1 f env (Addr env))))
-> Lens' env (Target env (FindEnv1 f env (Addr env)))
-> SomeInterface f env
forall env' (f :: * -> *) env.
Lens' env' (f env') -> Lens' env env' -> SomeInterface f env
SomeInterface
    (forall env.
Field (f (Target env (FindEnv1 f env (Addr env)))) env =>
Lens' env (f (Target env (FindEnv1 f env (Addr env))))
forall a env. Field a env => Lens' env a
fieldL @(f (Target env (FindEnv1 f env (Addr env)))))
    (Trans env (FindEnv1 f env (Addr env)) =>
Lens' env (Target env (FindEnv1 f env (Addr env)))
forall s (l :: [*]). Trans s l => Lens' s (Target s l)
transL @env @(FindEnv1 f env (Addr env)))

-- | Run action that depends on an interface @f@.
-- The action must be polymorphic to @env'@,
-- because it will run in some ancestor environment, which may be different from @env@,
runIF :: forall f env a. Has1 f env => (forall env'. f env' -> RIO env' a) -> RIO env a
runIF :: (forall env'. f env' -> RIO env' a) -> RIO env a
runIF forall env'. f env' -> RIO env' a
body =
  case forall env. Has1 f env => SomeInterface f env
forall (f :: * -> *) env. Has1 f env => SomeInterface f env
ifaceL @f of
    SomeInterface Lens' env' (f env')
_ifaceL Lens' env env'
_superL -> do
      f env'
iface <- Getting (f env') env (f env') -> RIO env (f env')
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Getting (f env') env (f env') -> RIO env (f env'))
-> Getting (f env') env (f env') -> RIO env (f env')
forall a b. (a -> b) -> a -> b
$ (env' -> Const (f env') env') -> env -> Const (f env') env
Lens' env env'
_superL ((env' -> Const (f env') env') -> env -> Const (f env') env)
-> ((f env' -> Const (f env') (f env'))
    -> env' -> Const (f env') env')
-> Getting (f env') env (f env')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f env' -> Const (f env') (f env')) -> env' -> Const (f env') env'
Lens' env' (f env')
_ifaceL
      env'
env <- Getting env' env env' -> RIO env env'
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting env' env env'
Lens' env env'
_superL
      env' -> RIO env' a -> RIO env a
forall (m :: * -> *) env a. MonadIO m => env -> RIO env a -> m a
runRIO env'
env (f env' -> RIO env' a
forall env'. f env' -> RIO env' a
body f env'
iface)