-- Copyright 2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

-- | Provides 'Generic1' derivation of @Representable10@ based on 'Field10'.
--
-- Like with "Data.Functor.Field", we use parametric functions
-- @forall m. f m -> m a@ to identify positions tagged with type @a@ within
-- @f@.  This leads to instances for 'Data.Ten.Representable.Representable10'
-- and 'Data.Ten.Update.Update10'.

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Ten.Field
         ( Field10(..)
         , FieldPaths10(..), GFieldPaths10(..)
         , Constrained10(..)
         ) where

import Control.Monad.Trans.State (state, evalState)
import Data.Coerce (coerce)
import Data.Functor ((<&>))
import Data.Functor.Const (Const(..))
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy(..))
import qualified Data.Text as T
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import GHC.Generics
         ( Generic1(..)
         , (:*:)(..), (:.:)(..)
         , M1(..), Rec1(..), U1(..)
         , Meta(..), S, C, D
         )
import GHC.TypeLits (KnownSymbol, symbolVal)

import Data.GADT.Compare (GEq(..), GCompare(..), GOrdering(..))
import Data.Hashable (Hashable(..))
import Data.Portray (Portray(..), Portrayal(..))
import Data.Portray.Diff (Diff(..), diffVs)
import Data.Wrapped (Wrapped1(..))

import Data.Functor.Field (FieldPaths(..))
import Data.Ten.Ap (Ap10(..))
import Data.Ten.Applicative (Applicative10(..))
import Data.Ten.Entails (Entails(..), Dict1(..))
import Data.Ten.Functor (Functor10(..))
import Data.Ten.Internal
         ( PathComponent(..), dropUnderscore, showsPath, portrayPath
         )
import Data.Ten.Traversable (Traversable10, fsequenceA10)
import {-# SOURCE #-} Data.Ten.Update (Update10, EqualityTable(..), equalityTable)

-- | A 'Data.Ten.Representable.Rep10' type as a parametric accessor function.
newtype Field10 f a = Field10 { Field10 f a -> forall (m :: k -> *). f m -> m a
getField10 :: forall m. f m -> m a }

instance Update10 f => TestEquality (Field10 f) where
  testEquality :: Field10 f a -> Field10 f b -> Maybe (a :~: b)
testEquality (Field10 forall (m :: k -> *). f m -> m a
f) (Field10 forall (m :: k -> *). f m -> m b
g) = case f (EqualityTable f) -> EqualityTable f a
forall (m :: k -> *). f m -> m a
f f (EqualityTable f)
forall k1 (f :: (k1 -> *) -> *). Update10 f => f (EqualityTable f)
equalityTable of
    EqualityTable f (Maybe :.: (:~:) a)
tbl -> (:.:) Maybe ((:~:) a) b -> Maybe (a :~: b)
forall k2 (f :: k2 -> *) k1 (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1 (f (Maybe :.: (:~:) a) -> (:.:) Maybe ((:~:) a) b
forall (m :: k -> *). f m -> m b
g f (Maybe :.: (:~:) a)
tbl)

instance Update10 f => GEq (Field10 f) where
  geq :: Field10 f a -> Field10 f b -> Maybe (a :~: b)
geq = Field10 f a -> Field10 f b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality

instance (Traversable10 f, Applicative10 f, Update10 f)
      => GCompare (Field10 f) where
  gcompare :: Field10 f a -> Field10 f b -> GOrdering a b
gcompare Field10 f a
x Field10 f b
y = case Field10 f a -> Field10 f b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq Field10 f a
x Field10 f b
y of
    Just a :~: b
Refl -> GOrdering a b
forall k (a :: k). GOrdering a a
GEQ
    Maybe (a :~: b)
Nothing ->
      if Const Int a -> Int
forall a k (b :: k). Const a b -> a
getConst (Field10 f a -> f (Const Int) -> Const Int a
forall k (f :: (k -> *) -> *) (a :: k).
Field10 f a -> forall (m :: k -> *). f m -> m a
getField10 Field10 f a
x f (Const Int)
forall k (f :: (k -> *) -> *).
(Traversable10 f, Applicative10 f) =>
f (Const Int)
fieldNumbers) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<
           Const Int b -> Int
forall a k (b :: k). Const a b -> a
getConst (Field10 f b -> f (Const Int) -> Const Int b
forall k (f :: (k -> *) -> *) (a :: k).
Field10 f a -> forall (m :: k -> *). f m -> m a
getField10 Field10 f b
y f (Const Int)
forall k (f :: (k -> *) -> *).
(Traversable10 f, Applicative10 f) =>
f (Const Int)
fieldNumbers)
        then GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GLT
        else GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GGT

fieldNumbers :: (Traversable10 f, Applicative10 f) => f (Const Int)
fieldNumbers :: f (Const Int)
fieldNumbers =
  (State Int (f (Const Int)) -> Int -> f (Const Int))
-> Int -> State Int (f (Const Int)) -> f (Const Int)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State Int (f (Const Int)) -> Int -> f (Const Int)
forall s a. State s a -> s -> a
evalState Int
0 (State Int (f (Const Int)) -> f (Const Int))
-> State Int (f (Const Int)) -> f (Const Int)
forall a b. (a -> b) -> a -> b
$
  f (StateT Int Identity :.: Const Int) -> State Int (f (Const Int))
forall k (m :: * -> *) (f :: (k -> *) -> *) (n :: k -> *).
(Applicative m, Traversable10 f) =>
f (m :.: n) -> m (f n)
fsequenceA10 ((forall (a :: k). (:.:) (StateT Int Identity) (Const Int) a)
-> f (StateT Int Identity :.: Const Int)
forall k (f :: (k -> *) -> *) (m :: k -> *).
Applicative10 f =>
(forall (a :: k). m a) -> f m
pure10 ((forall (a :: k). (:.:) (StateT Int Identity) (Const Int) a)
 -> f (StateT Int Identity :.: Const Int))
-> (forall (a :: k). (:.:) (StateT Int Identity) (Const Int) a)
-> f (StateT Int Identity :.: Const Int)
forall a b. (a -> b) -> a -> b
$ StateT Int Identity (Const Int a)
-> (:.:) (StateT Int Identity) (Const Int) a
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (StateT Int Identity (Const Int a)
 -> (:.:) (StateT Int Identity) (Const Int) a)
-> StateT Int Identity (Const Int a)
-> (:.:) (StateT Int Identity) (Const Int) a
forall a b. (a -> b) -> a -> b
$ (Int -> (Const Int a, Int)) -> StateT Int Identity (Const Int a)
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state ((Int -> (Const Int a, Int)) -> StateT Int Identity (Const Int a))
-> (Int -> (Const Int a, Int)) -> StateT Int Identity (Const Int a)
forall a b. (a -> b) -> a -> b
$ \Int
i -> (Int -> Const Int a
forall k a (b :: k). a -> Const a b
Const Int
i, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))

instance (Traversable10 f, Applicative10 f) => Eq (Field10 f a) where
  Field10 forall (m :: k -> *). f m -> m a
x == :: Field10 f a -> Field10 f a -> Bool
== Field10 forall (m :: k -> *). f m -> m a
y = f (Const Int) -> Const Int a
forall (m :: k -> *). f m -> m a
x f (Const Int)
forall k (f :: (k -> *) -> *).
(Traversable10 f, Applicative10 f) =>
f (Const Int)
fieldNumbers Const Int a -> Const Int a -> Bool
forall a. Eq a => a -> a -> Bool
== f (Const Int) -> Const Int a
forall (m :: k -> *). f m -> m a
y f (Const Int)
forall k (f :: (k -> *) -> *).
(Traversable10 f, Applicative10 f) =>
f (Const Int)
fieldNumbers

instance (Traversable10 f, Applicative10 f) => Ord (Field10 f a) where
  Field10 forall (m :: k -> *). f m -> m a
x compare :: Field10 f a -> Field10 f a -> Ordering
`compare` Field10 forall (m :: k -> *). f m -> m a
y = f (Const Int) -> Const Int a
forall (m :: k -> *). f m -> m a
x f (Const Int)
forall k (f :: (k -> *) -> *).
(Traversable10 f, Applicative10 f) =>
f (Const Int)
fieldNumbers Const Int a -> Const Int a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` f (Const Int) -> Const Int a
forall (m :: k -> *). f m -> m a
y f (Const Int)
forall k (f :: (k -> *) -> *).
(Traversable10 f, Applicative10 f) =>
f (Const Int)
fieldNumbers

instance (Traversable10 f, Applicative10 f) => Hashable (Field10 f a) where
  hashWithSalt :: Int -> Field10 f a -> Int
hashWithSalt Int
salt (Field10 forall (m :: k -> *). f m -> m a
x) = Int -> Const Int a -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (Const Int a -> Int) -> Const Int a -> Int
forall a b. (a -> b) -> a -> b
$ f (Const Int) -> Const Int a
forall (m :: k -> *). f m -> m a
x f (Const Int)
forall k (f :: (k -> *) -> *).
(Traversable10 f, Applicative10 f) =>
f (Const Int)
fieldNumbers

instance FieldPaths10 f => Show (Field10 f a) where
  showsPrec :: Int -> Field10 f a -> ShowS
showsPrec Int
p (Field10 forall (m :: k -> *). f m -> m a
f) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"Field10 " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [PathComponent] -> ShowS
showsPath Int
11 (Const [PathComponent] a -> [PathComponent]
coerce (Const [PathComponent] a -> [PathComponent])
-> Const [PathComponent] a -> [PathComponent]
forall a b. (a -> b) -> a -> b
$ f (Const [PathComponent]) -> Const [PathComponent] a
forall (m :: k -> *). f m -> m a
f f (Const [PathComponent])
forall k (rec :: (k -> *) -> *).
FieldPaths10 rec =>
rec (Const [PathComponent])
fieldPaths10)

instance FieldPaths10 f => Portray (Field10 f a) where
  portray :: Field10 f a -> Portrayal
portray (Field10 forall (m :: k -> *). f m -> m a
f) =
    Portrayal -> [Portrayal] -> Portrayal
Apply (Ident -> Portrayal
Name Ident
"Field10") [[PathComponent] -> Portrayal
portrayPath ([PathComponent] -> Portrayal) -> [PathComponent] -> Portrayal
forall a b. (a -> b) -> a -> b
$ Const [PathComponent] a -> [PathComponent]
coerce (Const [PathComponent] a -> [PathComponent])
-> Const [PathComponent] a -> [PathComponent]
forall a b. (a -> b) -> a -> b
$ f (Const [PathComponent]) -> Const [PathComponent] a
forall (m :: k -> *). f m -> m a
f f (Const [PathComponent])
forall k (rec :: (k -> *) -> *).
FieldPaths10 rec =>
rec (Const [PathComponent])
fieldPaths10]

instance (Traversable10 f, Applicative10 f, FieldPaths10 f)
      => Diff (Field10 f a) where
  diff :: Field10 f a -> Field10 f a -> Maybe Portrayal
diff Field10 f a
f Field10 f a
g
    | Field10 f a
f Field10 f a -> Field10 f a -> Bool
forall a. Eq a => a -> a -> Bool
== Field10 f a
g    = Maybe Portrayal
forall a. Maybe a
Nothing
    | Bool
otherwise = Portrayal -> Maybe Portrayal
forall a. a -> Maybe a
Just (Portrayal -> Maybe Portrayal) -> Portrayal -> Maybe Portrayal
forall a b. (a -> b) -> a -> b
$ Field10 f a -> Portrayal
forall a. Portray a => a -> Portrayal
portray Field10 f a
f Portrayal -> Portrayal -> Portrayal
`diffVs` Field10 f a -> Portrayal
forall a. Portray a => a -> Portrayal
portray Field10 f a
g

-- | Provides a path of field selectors / lenses identifying each "field".
class FieldPaths10 (rec :: (k -> Type) -> Type) where
  fieldPaths10 :: rec (Const [PathComponent])

instance (Generic1 rec, GFieldPaths10 (Rep1 rec))
      => FieldPaths10 (Wrapped1 Generic1 rec) where
  fieldPaths10 :: Wrapped1 Generic1 rec (Const [PathComponent])
fieldPaths10 = rec (Const [PathComponent])
-> Wrapped1 Generic1 rec (Const [PathComponent])
forall k (c :: (k -> *) -> Constraint) (f :: k -> *) (a :: k).
f a -> Wrapped1 c f a
Wrapped1 (rec (Const [PathComponent])
 -> Wrapped1 Generic1 rec (Const [PathComponent]))
-> (Rep1 rec (Const [PathComponent])
    -> rec (Const [PathComponent]))
-> Rep1 rec (Const [PathComponent])
-> Wrapped1 Generic1 rec (Const [PathComponent])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep1 rec (Const [PathComponent]) -> rec (Const [PathComponent])
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 rec (Const [PathComponent])
 -> Wrapped1 Generic1 rec (Const [PathComponent]))
-> Rep1 rec (Const [PathComponent])
-> Wrapped1 Generic1 rec (Const [PathComponent])
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). [PathComponent] -> Const [PathComponent] a)
-> Rep1 rec (Const [PathComponent])
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GFieldPaths10 rec =>
(forall (a :: k). [PathComponent] -> r a) -> rec r
gfieldPaths10 forall (a :: k). [PathComponent] -> Const [PathComponent] a
forall k a (b :: k). a -> Const a b
Const
  {-# INLINE fieldPaths10 #-}

-- | 'Generic1' implementation of 'FieldPaths10'.
class GFieldPaths10 (rec :: (k -> Type) -> Type) where
  gfieldPaths10 :: (forall a. [PathComponent] -> r a) -> rec r

instance GFieldPaths10 U1 where
  gfieldPaths10 :: (forall (a :: k). [PathComponent] -> r a) -> U1 r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
_ = U1 r
forall k (p :: k). U1 p
U1
  {-# INLINE gfieldPaths10 #-}

instance FieldPaths10 (Ap10 a) where
  fieldPaths10 :: Ap10 a (Const [PathComponent])
fieldPaths10 = Const [PathComponent] a -> Ap10 a (Const [PathComponent])
forall k (a :: k) (f :: k -> *). f a -> Ap10 a f
Ap10 ([PathComponent] -> Const [PathComponent] a
forall k a (b :: k). a -> Const a b
Const [])
  {-# INLINE fieldPaths10 #-}

instance (Functor10 rec, FieldPaths10 rec) => GFieldPaths10 (Rec1 rec) where
  gfieldPaths10 :: (forall (a :: k). [PathComponent] -> r a) -> Rec1 rec r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r = rec r -> Rec1 rec r
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (rec r -> Rec1 rec r) -> rec r -> Rec1 rec r
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Const [PathComponent] a -> r a)
-> rec (Const [PathComponent]) -> rec r
forall k (f :: (k -> *) -> *) (m :: k -> *) (n :: k -> *).
Functor10 f =>
(forall (a :: k). m a -> n a) -> f m -> f n
fmap10 ([PathComponent] -> r a
forall (a :: k). [PathComponent] -> r a
r ([PathComponent] -> r a)
-> (Const [PathComponent] a -> [PathComponent])
-> Const [PathComponent] a
-> r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const [PathComponent] a -> [PathComponent]
forall a k (b :: k). Const a b -> a
getConst) rec (Const [PathComponent])
forall k (rec :: (k -> *) -> *).
FieldPaths10 rec =>
rec (Const [PathComponent])
fieldPaths10
  {-# INLINE gfieldPaths10 #-}

instance GFieldPaths10 rec => GFieldPaths10 (M1 C i rec) where
  gfieldPaths10 :: (forall (a :: k). [PathComponent] -> r a) -> M1 C i rec r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r = rec r -> M1 C i rec r
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (rec r -> M1 C i rec r) -> rec r -> M1 C i rec r
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). [PathComponent] -> r a) -> rec r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GFieldPaths10 rec =>
(forall (a :: k). [PathComponent] -> r a) -> rec r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r
  {-# INLINE gfieldPaths10 #-}

-- Non-newtype constructors: wait until we get to the fields to assign a path
-- component.
instance GFieldPaths10 rec => GFieldPaths10 (M1 D ('MetaData n m p 'False) rec) where
  gfieldPaths10 :: (forall (a :: k). [PathComponent] -> r a)
-> M1 D ('MetaData n m p 'False) rec r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r = rec r -> M1 D ('MetaData n m p 'False) rec r
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (rec r -> M1 D ('MetaData n m p 'False) rec r)
-> rec r -> M1 D ('MetaData n m p 'False) rec r
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). [PathComponent] -> r a) -> rec r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GFieldPaths10 rec =>
(forall (a :: k). [PathComponent] -> r a) -> rec r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r
  {-# INLINE gfieldPaths10 #-}

-- Newtype constructors: immediately decide to use 'NewtypeIso'.
instance GFieldPaths10 rec
      => GFieldPaths10 (M1 D ('MetaData n m p 'True) (M1 C i (M1 S j rec))) where
  gfieldPaths10 :: (forall (a :: k). [PathComponent] -> r a)
-> M1 D ('MetaData n m p 'True) (M1 C i (M1 S j rec)) r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r = M1 C i (M1 S j rec) r
-> M1 D ('MetaData n m p 'True) (M1 C i (M1 S j rec)) r
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (M1 C i (M1 S j rec) r
 -> M1 D ('MetaData n m p 'True) (M1 C i (M1 S j rec)) r)
-> (rec r -> M1 C i (M1 S j rec) r)
-> rec r
-> M1 D ('MetaData n m p 'True) (M1 C i (M1 S j rec)) r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 S j rec r -> M1 C i (M1 S j rec) r
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (M1 S j rec r -> M1 C i (M1 S j rec) r)
-> (rec r -> M1 S j rec r) -> rec r -> M1 C i (M1 S j rec) r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. rec r -> M1 S j rec r
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (rec r -> M1 D ('MetaData n m p 'True) (M1 C i (M1 S j rec)) r)
-> rec r -> M1 D ('MetaData n m p 'True) (M1 C i (M1 S j rec)) r
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). [PathComponent] -> r a) -> rec r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GFieldPaths10 rec =>
(forall (a :: k). [PathComponent] -> r a) -> rec r
gfieldPaths10 ([PathComponent] -> r a
forall (a :: k). [PathComponent] -> r a
r ([PathComponent] -> r a)
-> ([PathComponent] -> [PathComponent]) -> [PathComponent] -> r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PathComponent
NewtypeIsoPathComponent -> [PathComponent] -> [PathComponent]
forall a. a -> [a] -> [a]
:))
  {-# INLINE gfieldPaths10 #-}

instance (KnownSymbol sym, GFieldPaths10 rec)
      => GFieldPaths10 (M1 S ('MetaSel ('Just sym) b c d) rec) where
  gfieldPaths10 :: (forall (a :: k). [PathComponent] -> r a)
-> M1 S ('MetaSel ('Just sym) b c d) rec r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r = rec r -> M1 S ('MetaSel ('Just sym) b c d) rec r
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (rec r -> M1 S ('MetaSel ('Just sym) b c d) rec r)
-> rec r -> M1 S ('MetaSel ('Just sym) b c d) rec r
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). [PathComponent] -> r a) -> rec r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GFieldPaths10 rec =>
(forall (a :: k). [PathComponent] -> r a) -> rec r
gfieldPaths10 ((forall (a :: k). [PathComponent] -> r a) -> rec r)
-> (forall (a :: k). [PathComponent] -> r a) -> rec r
forall a b. (a -> b) -> a -> b
$
    [PathComponent] -> r a
forall (a :: k). [PathComponent] -> r a
r ([PathComponent] -> r a)
-> ([PathComponent] -> [PathComponent]) -> [PathComponent] -> r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Text -> PathComponent
NamedField (String -> Text
T.pack String
nm) (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ ShowS
dropUnderscore String
nm) PathComponent -> [PathComponent] -> [PathComponent]
forall a. a -> [a] -> [a]
:)
   where
    nm :: String
nm = Proxy sym -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal @sym Proxy sym
forall k (t :: k). Proxy t
Proxy
  {-# INLINE gfieldPaths10 #-}

instance (GFieldPaths10 f, GFieldPaths10 g) => GFieldPaths10 (f :*: g) where
  gfieldPaths10 :: (forall (a :: k). [PathComponent] -> r a) -> (:*:) f g r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r = (forall (a :: k). [PathComponent] -> r a) -> f r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GFieldPaths10 rec =>
(forall (a :: k). [PathComponent] -> r a) -> rec r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r f r -> g r -> (:*:) f g r
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (forall (a :: k). [PathComponent] -> r a) -> g r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GFieldPaths10 rec =>
(forall (a :: k). [PathComponent] -> r a) -> rec r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r
  {-# INLINE gfieldPaths10 #-}

instance (Functor f, FieldPaths f, GFieldPaths10 g)
      => GFieldPaths10 (f :.: g) where
  gfieldPaths10 :: (forall (a :: k). [PathComponent] -> r a) -> (:.:) f g r
gfieldPaths10 forall (a :: k). [PathComponent] -> r a
r = f (g r) -> (:.:) f g r
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f (g r) -> (:.:) f g r) -> f (g r) -> (:.:) f g r
forall a b. (a -> b) -> a -> b
$
    f [PathComponent]
forall (f :: * -> *). FieldPaths f => f [PathComponent]
fieldPaths f [PathComponent] -> ([PathComponent] -> g r) -> f (g r)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \[PathComponent]
outer ->
    (forall (a :: k). [PathComponent] -> r a) -> g r
forall k (rec :: (k -> *) -> *) (r :: k -> *).
GFieldPaths10 rec =>
(forall (a :: k). [PathComponent] -> r a) -> rec r
gfieldPaths10 ((forall (a :: k). [PathComponent] -> r a) -> g r)
-> (forall (a :: k). [PathComponent] -> r a) -> g r
forall a b. (a -> b) -> a -> b
$ \[PathComponent]
inner ->
    [PathComponent] -> r a
forall (a :: k). [PathComponent] -> r a
r ([PathComponent] -> r a) -> [PathComponent] -> r a
forall a b. (a -> b) -> a -> b
$ [PathComponent]
outer [PathComponent] -> [PathComponent] -> [PathComponent]
forall a. [a] -> [a] -> [a]
++ [PathComponent]
inner
  {-# INLINE gfieldPaths10 #-}

-- | @Constrained10 c f@ means that in @f m@, all applications of @m@
-- are to types @x@ that satisfy constraint @c@.
class Constrained10 (c :: k -> Constraint) (f :: (k -> Type) -> Type) where
  -- | Recover instances of @c@ to accompany each @m@ element in @f@.
  constrained10 :: f (Dict1 c)

instance c a => Constrained10 c (Ap10 a) where
  constrained10 :: Ap10 a (Dict1 c)
constrained10 = Dict1 c a -> Ap10 a (Dict1 c)
forall k (a :: k) (f :: k -> *). f a -> Ap10 a f
Ap10 Dict1 c a
forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a
Dict1

instance (Generic1 f, Constrained10 c (Rep1 f))
      => Constrained10 c (Wrapped1 Generic1 f) where
  constrained10 :: Wrapped1 Generic1 f (Dict1 c)
constrained10 = f (Dict1 c) -> Wrapped1 Generic1 f (Dict1 c)
forall k (c :: (k -> *) -> Constraint) (f :: k -> *) (a :: k).
f a -> Wrapped1 c f a
Wrapped1 (f (Dict1 c) -> Wrapped1 Generic1 f (Dict1 c))
-> f (Dict1 c) -> Wrapped1 Generic1 f (Dict1 c)
forall a b. (a -> b) -> a -> b
$ Rep1 f (Dict1 c) -> f (Dict1 c)
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 Rep1 f (Dict1 c)
forall k (c :: k -> Constraint) (f :: (k -> *) -> *).
Constrained10 c f =>
f (Dict1 c)
constrained10

instance Constrained10 c U1 where
  constrained10 :: U1 (Dict1 c)
constrained10 = U1 (Dict1 c)
forall k (p :: k). U1 p
U1

deriving instance Constrained10 c f => Constrained10 c (Rec1 f)
deriving instance Constrained10 c f => Constrained10 c (M1 i c1 f)

instance (Constrained10 c f, Constrained10 c g)
      => Constrained10 c (f :*: g) where
  constrained10 :: (:*:) f g (Dict1 c)
constrained10 = f (Dict1 c)
forall k (c :: k -> Constraint) (f :: (k -> *) -> *).
Constrained10 c f =>
f (Dict1 c)
constrained10 f (Dict1 c) -> g (Dict1 c) -> (:*:) f g (Dict1 c)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g (Dict1 c)
forall k (c :: k -> Constraint) (f :: (k -> *) -> *).
Constrained10 c f =>
f (Dict1 c)
constrained10

instance (Applicative f, Constrained10 c g) => Constrained10 c (f :.: g) where
  constrained10 :: (:.:) f g (Dict1 c)
constrained10 = f (g (Dict1 c)) -> (:.:) f g (Dict1 c)
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (g (Dict1 c) -> f (g (Dict1 c))
forall (f :: * -> *) a. Applicative f => a -> f a
pure g (Dict1 c)
forall k (c :: k -> Constraint) (f :: (k -> *) -> *).
Constrained10 c f =>
f (Dict1 c)
constrained10)

instance (Constrained10 c f, Applicative10 f) => Entails (Field10 f) c where
  entailment :: Field10 f a -> Dict1 c a
entailment (Field10 forall (m :: k -> *). f m -> m a
f) = f (Dict1 c) -> Dict1 c a
forall (m :: k -> *). f m -> m a
f f (Dict1 c)
forall k (c :: k -> Constraint) (f :: (k -> *) -> *).
Constrained10 c f =>
f (Dict1 c)
constrained10