content: {-# LANGUAGE UndecidableInstances #-}
  {-# OPTIONS_HADDOCK not-home #-}
  
  -- | This module is intended for internal use only, and may change without
  -- warning in subsequent releases.
  module Optics.Internal.Generic.TypeLevel
    ( -- * Pathing
      PathTree(..)
    , Path(..)
    -- ** Names
    , GetFieldPaths
    , GetNamePath
    -- ** Positions
    , GetPositionPaths
    , GetPositionPath
    -- * Misc
    , HideReps
    , AnyHasPath
    , NoGenericError
    ) where
  
  import Data.Kind
  import Data.Type.Bool
  import Data.Type.Equality
  import GHC.Generics
  import GHC.TypeLits
  
  import Optics.Internal.Optic.TypeLevel
  
  -- | A map that allows reaching a specific field in a generic representation of
  -- a data type. Computed up front by generic optics for early error reporting
  -- and efficient data traversal.
  data PathTree e
    = PathNode (PathTree e) (PathTree e)
    | PathLeaf (Either e [Path])
  
  data Path = PathLeft | PathRight
  
  ----------------------------------------
  -- Paths to a field
  
  -- | Compute paths to a field with a specific name.
  type family GetFieldPaths s (name :: Symbol) g :: PathTree Symbol where
    GetFieldPaths s name (M1 D _ g)  = GetFieldPaths s name g
    GetFieldPaths s name (g1 :+: g2) = PathNode (GetFieldPaths s name g1)
                                                (GetFieldPaths s name g2)
    GetFieldPaths s name (M1 C _ g)  = PathLeaf (GetNamePath name g '[])
  
    GetFieldPaths s name V1 = TypeError (Text "Type " :<>: QuoteType s :<>:
                                         Text " has no data constructors")
  
  -- | Compute path to a constructor in a sum or a field in a product with a
  -- specific name.
  type family GetNamePath (name :: Symbol) g (acc :: [Path]) :: Either Symbol [Path] where
    GetNamePath name (M1 D _ g) acc = GetNamePath name g acc
  
    -- Find path to a constructor in a sum type.
    GetNamePath name (M1 C (MetaCons name _ _) _) acc = Right (Reverse acc '[])
    GetNamePath name (g1 :+: g2) acc = FirstRight (GetNamePath name g1 (PathLeft  : acc))
                                                  (GetNamePath name g2 (PathRight : acc))
  
    -- Find path to a field in a product type.
    GetNamePath name (M1 S (MetaSel (Just name) _ _ _) _) acc = Right (Reverse acc '[])
    GetNamePath name (g1 :*: g2) acc = FirstRight (GetNamePath name g1 (PathLeft  : acc))
                                                  (GetNamePath name g2 (PathRight : acc))
  
    GetNamePath name _ _ = Left name
  
  ----------------------------------------
  -- Paths to a position
  
  -- | Compute paths to a field at a specific position.
  type family GetPositionPaths s (pos :: Nat) g :: PathTree (Nat, Nat) where
    GetPositionPaths s pos (M1 D _ g)  = GetPositionPaths s pos g
    GetPositionPaths s pos (g1 :+: g2) = PathNode (GetPositionPaths s pos g1)
                                                  (GetPositionPaths s pos g2)
    GetPositionPaths s pos (M1 C _ g)  = PathLeaf (GetPositionPath pos g 0 '[])
  
    GetPositionPaths s pos V1 = TypeError (Text "Type " :<>: QuoteType s :<>:
                                           Text " has no data constructors")
  
  -- | Compute path to a constructor in a sum or a field in a product at a
  -- specific position.
  type family GetPositionPath (pos :: Nat) g (k :: Nat) (acc :: [Path])
    :: Either (Nat, Nat) [Path] where
    GetPositionPath pos (M1 D _ g) k acc = GetPositionPath pos g k acc
  
    -- Find field at a position in a sum type.
    GetPositionPath pos (M1 C _ _) k acc =
      If (pos == k + 1) (Right (Reverse acc '[])) (Left '(pos, k + 1))
    GetPositionPath pos (g1 :+: g2) k acc =
      ContinueWhenLeft (GetPositionPath pos g1 k (PathLeft : acc)) g2 acc
  
    -- Find field at a position in a product type.
    GetPositionPath pos (M1 S _ _) k acc =
      If (pos == k + 1) (Right (Reverse acc '[])) (Left '(pos, k + 1))
    GetPositionPath pos (g1 :*: g2) k acc =
      ContinueWhenLeft (GetPositionPath pos g1 k (PathLeft : acc)) g2 acc
  
    -- The second element is the number of fields in the data constructor.
    GetPositionPath pos _ k _ = Left '(pos, k)
  
  -- | If the left branch had the position we're looking for, return it. Otherwise
  -- continue with the right branch.
  type family ContinueWhenLeft (r :: Either (Nat, Nat) [Path]) g acc
    :: Either (Nat, Nat) [Path] where
    ContinueWhenLeft (Right path) _ _ = Right path
    ContinueWhenLeft (Left '(pos, k)) g acc = GetPositionPath pos g k (PathRight : acc)
  
  ----------------------------------------
  -- Misc
  
  data Void1 a
  -- | Generate bogus equality constraints that attempt to unify generic
  -- representations with this type in case there is an error such as missing
  -- field, constructor etc. so these huge types don't leak into error messages.
  type family HideReps (g :: Type -> Type) (h :: Type -> Type) :: Constraint where
    HideReps g h = (g ~ Void1, h ~ Void1)
  
  -- | Check if any leaf in the tree has a '[Path]'.
  type family AnyHasPath (path :: PathTree e) :: Bool where
    AnyHasPath (PathNode path1 path2) = AnyHasPath path1 || AnyHasPath path2
    AnyHasPath (PathLeaf (Right _))  = True
    AnyHasPath (PathLeaf (Left _ ))  = False
  
  type family NoGenericError t where
    NoGenericError t = TypeError
      (Text "Type " :<>: QuoteType t :<>:
       Text " doesn't have a Generic instance")
  