{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Data.Type.Functor.Product (
FProd(..), Shape
, PureProd(..), pureShape
, PureProdC(..), ReifyConstraintProd(..)
, AllConstrainedProd
, indexProd, mapProd, foldMapProd, hmap, zipProd
, imapProd, itraverseProd, ifoldMapProd
, generateProd, generateProdA
, selectProd, indices
, eqProd, compareProd
, indexSing, singShape
, foldMapSing, ifoldMapSing
, Rec(..), Index(..), withPureProdList
, PMaybe(..), IJust(..)
, PEither(..), IRight(..)
, NERec(..), NEIndex(..), withPureProdNE
, PTup(..), ISnd(..)
, PIdentity(..), IIdentity(..)
, sameIndexVal, sameNEIndexVal
, rElemIndex, indexRElem, toCoRec
, SIndex(..), SIJust(..), SIRight(..), SNEIndex(..), SISnd(..), SIIdentity(..)
, ElemSym0, ElemSym1, ElemSym2
, ProdSym0, ProdSym1, ProdSym2
) where
import Control.Applicative
import Data.Functor.Classes
import Data.Functor.Identity
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
import Data.Maybe
import Data.Semigroup
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.Prelude hiding (Elem, ElemSym0, ElemSym1, ElemSym2)
import Data.Singletons.Prelude.Foldable hiding (Elem, ElemSym0, ElemSym1, ElemSym2)
import Data.Singletons.Prelude.Identity
import Data.Vinyl hiding ((:~:))
import Data.Vinyl.CoRec
import GHC.Generics ((:*:)(..))
import Lens.Micro hiding ((%~))
import Lens.Micro.Extras
import Unsafe.Coerce
import qualified Data.Singletons.Prelude.List.NonEmpty as NE
import qualified Data.Text as T
import qualified Data.Vinyl.Functor as V
import qualified Data.Vinyl.TypeLevel as V
fmapIdent :: Fmap IdSym0 as :~: as
fmapIdent :: Fmap IdSym0 as :~: as
fmapIdent = (Any :~: Any) -> Fmap IdSym0 as :~: as
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl
type Shape f = (Prod f Proxy :: f k -> Type)
class (PFunctor f, SFunctor f, PFoldable f, SFoldable f) => FProd (f :: Type -> Type) where
type Elem f = (i :: f k -> k -> Type) | i -> f
type Prod f = (p :: (k -> Type) -> f k -> Type) | p -> f
singProd :: Sing as -> Prod f Sing as
prodSing :: Prod f Sing as -> Sing as
withIndices
:: Prod f g as
-> Prod f (Elem f as :*: g) as
traverseProd
:: forall g h as m. Applicative m
=> (forall a. g a -> m (h a))
-> Prod f g as
-> m (Prod f h as)
traverseProd = case Fmap IdSym0 as :~: as
forall (f0 :: * -> *) b0 (as :: f0 b0). Fmap IdSym0 as :~: as
fmapIdent @as of
Refl -> Sing IdSym0
-> (forall (a :: k). g a -> m (h (IdSym0 @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap IdSym0 as))
forall (f :: * -> *) a0 k (m :: * -> *) (ff :: a0 ~> k)
(g :: a0 -> *) (h :: k -> *) (as :: f a0).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse (SingI IdSym0 => Sing IdSym0
forall k (a :: k). SingI a => Sing a
sing @IdSym0)
zipWithProd
:: (forall a. g a -> h a -> j a)
-> Prod f g as
-> Prod f h as
-> Prod f j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f xs :: Prod f g as
xs ys :: Prod f h as
ys = (forall (a :: k). Elem f as a -> g a -> j a)
-> Prod f g as -> Prod f j as
forall k (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd (\i :: Elem f as a
i x :: g a
x -> g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x (Elem f as a -> Prod f h as -> h a
forall k (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
indexProd Elem f as a
i Prod f h as
ys)) Prod f g as
xs
htraverse
:: Applicative m
=> Sing ff
-> (forall a. g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
ixProd
:: Elem f as a
-> Lens' (Prod f g as) (g a)
toRec :: Prod f g as -> Rec g (ToList as)
withPureProd
:: Prod f g as
-> (PureProd f as => r)
-> r
class PureProd f as where
pureProd :: (forall a. g a) -> Prod f g as
class PureProdC f c as where
pureProdC :: (forall a. c a => g a) -> Prod f g as
class ReifyConstraintProd f c g as where
reifyConstraintProd :: Prod f g as -> Prod f (Dict c V.:. g) as
data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type
data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a
type instance Apply (ElemSym0 f) as = ElemSym1 f as
type instance Apply (ElemSym1 f as) a = Elem f as a
data ProdSym0 (f :: Type -> Type) :: (k -> Type) ~> f k ~> Type
data ProdSym1 (f :: Type -> Type) :: (k -> Type) -> f k ~> Type
type ProdSym2 (f :: Type -> Type) (g :: k -> Type) (as :: f k) = Prod f g as
type instance Apply (ProdSym0 f) g = ProdSym1 f g
type instance Apply (ProdSym1 f g) as = Prod f g as
type AllConstrainedProd c as = V.AllConstrained c (ToList as)
pureShape :: PureProd f as => Shape f as
pureShape :: Shape f as
pureShape = (forall (a :: k). Proxy a) -> Shape f as
forall k (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
pureProd forall (a :: k). Proxy a
forall k (t :: k). Proxy t
Proxy
indices :: (FProd f, PureProd f as) => Prod f (Elem f as) as
indices :: Prod f (Elem f as) as
indices = (forall (a :: k). Elem f as a -> Proxy a -> Elem f as a)
-> Prod f Proxy as -> Prod f (Elem f as) as
forall k (f :: * -> *) (as :: f k) (g :: k -> *) (h :: k -> *).
FProd f =>
(forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd forall (a :: k). Elem f as a -> Proxy a -> Elem f as a
forall a b. a -> b -> a
const Prod f Proxy as
forall k (f :: * -> *) (as :: f k). PureProd f as => Shape f as
pureShape
singShape
:: FProd f
=> Sing as
-> Shape f as
singShape :: Sing as -> Shape f as
singShape = (forall (a :: k). Sing a -> Proxy a)
-> Prod f Sing as -> Shape f as
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (Proxy a -> Sing a -> Proxy a
forall a b. a -> b -> a
const Proxy a
forall k (t :: k). Proxy t
Proxy) (Prod f Sing as -> Shape f as)
-> (Sing as -> Prod f Sing as) -> Sing as -> Shape f as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
mapProd
:: FProd f
=> (forall a. g a -> h a)
-> Prod f g as
-> Prod f h as
mapProd :: (forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd f :: forall (a :: k). g a -> h a
f = Identity (Prod f h as) -> Prod f h as
forall a. Identity a -> a
runIdentity (Identity (Prod f h as) -> Prod f h as)
-> (Prod f g as -> Identity (Prod f h as))
-> Prod f g as
-> Prod f h as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). g a -> Identity (h a))
-> Prod f g as -> Identity (Prod f h as)
forall (f :: * -> *) k (g :: k -> *) (h :: k -> *) (as :: f k)
(m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd (h a -> Identity (h a)
forall a. a -> Identity a
Identity (h a -> Identity (h a)) -> (g a -> h a) -> g a -> Identity (h a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> h a
forall (a :: k). g a -> h a
f)
zipProd
:: FProd f
=> Prod f g as
-> Prod f h as
-> Prod f (g :*: h) as
zipProd :: Prod f g as -> Prod f h as -> Prod f (g :*: h) as
zipProd = (forall (a :: k). g a -> h a -> (:*:) g h a)
-> Prod f g as -> Prod f h as -> Prod f (g :*: h) as
forall (f :: * -> *) k (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd forall (a :: k). g a -> h a -> (:*:) g h a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)
hmap
:: FProd f
=> Sing ff
-> (forall a. g a -> h (ff @@ a))
-> Prod f g as
-> Prod f h (Fmap ff as)
hmap :: Sing ff
-> (forall (a :: a0). g a -> h (ff @@ a))
-> Prod f g as
-> Prod f h (Fmap ff as)
hmap ff :: Sing ff
ff f :: forall (a :: a0). g a -> h (ff @@ a)
f = Identity (Prod f h (Fmap ff as)) -> Prod f h (Fmap ff as)
forall a. Identity a -> a
runIdentity (Identity (Prod f h (Fmap ff as)) -> Prod f h (Fmap ff as))
-> (Prod f g as -> Identity (Prod f h (Fmap ff as)))
-> Prod f g as
-> Prod f h (Fmap ff as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing ff
-> (forall (a :: a0). g a -> Identity (h (ff @@ a)))
-> Prod f g as
-> Identity (Prod f h (Fmap ff as))
forall (f :: * -> *) a0 k (m :: * -> *) (ff :: a0 ~> k)
(g :: a0 -> *) (h :: k -> *) (as :: f a0).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse Sing ff
ff (h (Apply ff a) -> Identity (h (Apply ff a))
forall a. a -> Identity a
Identity (h (Apply ff a) -> Identity (h (Apply ff a)))
-> (g a -> h (Apply ff a)) -> g a -> Identity (h (Apply ff a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> h (Apply ff a)
forall (a :: a0). g a -> h (ff @@ a)
f)
imapProd
:: FProd f
=> (forall a. Elem f as a -> g a -> h a)
-> Prod f g as
-> Prod f h as
imapProd :: (forall (a :: k). Elem f as a -> g a -> h a)
-> Prod f g as -> Prod f h as
imapProd f :: forall (a :: k). Elem f as a -> g a -> h a
f = (forall (a :: k). (:*:) (Elem f as) g a -> h a)
-> Prod f (Elem f as :*: g) as -> Prod f h as
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (\(i :*: x) -> Elem f as a -> g a -> h a
forall (a :: k). Elem f as a -> g a -> h a
f Elem f as a
i g a
x) (Prod f (Elem f as :*: g) as -> Prod f h as)
-> (Prod f g as -> Prod f (Elem f as :*: g) as)
-> Prod f g as
-> Prod f h as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prod f g as -> Prod f (Elem f as :*: g) as
forall (f :: * -> *) k (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices
indexSing
:: forall f as a. FProd f
=> Elem f as a
-> Sing as
-> Sing a
indexSing :: Elem f as a -> Sing as -> Sing a
indexSing i :: Elem f as a
i = Elem f as a -> Prod f Sing as -> Sing a
forall k (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
indexProd Elem f as a
i (Prod f Sing as -> Sing a)
-> (Sing as -> Prod f Sing as) -> Sing as -> Sing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
indexProd
:: FProd f
=> Elem f as a
-> Prod f g as
-> g a
indexProd :: Elem f as a -> Prod f g as -> g a
indexProd i :: Elem f as a
i = Getting (g a) (Prod f g as) (g a) -> Prod f g as -> g a
forall a s. Getting a s a -> s -> a
view (Elem f as a -> Lens' (Prod f g as) (g a)
forall (f :: * -> *) k (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Lens' (Prod f g as) (g a)
ixProd Elem f as a
i)
itraverseProd
:: (FProd f, Applicative m)
=> (forall a. Elem f as a -> g a -> m (h a))
-> Prod f g as
-> m (Prod f h as)
itraverseProd :: (forall (a :: k). Elem f as a -> g a -> m (h a))
-> Prod f g as -> m (Prod f h as)
itraverseProd f :: forall (a :: k). Elem f as a -> g a -> m (h a)
f = (forall (a :: k). (:*:) (Elem f as) g a -> m (h a))
-> Prod f (Elem f as :*: g) as -> m (Prod f h as)
forall (f :: * -> *) k (g :: k -> *) (h :: k -> *) (as :: f k)
(m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd (\(i :*: x) -> Elem f as a -> g a -> m (h a)
forall (a :: k). Elem f as a -> g a -> m (h a)
f Elem f as a
i g a
x) (Prod f (Elem f as :*: g) as -> m (Prod f h as))
-> (Prod f g as -> Prod f (Elem f as :*: g) as)
-> Prod f g as
-> m (Prod f h as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prod f g as -> Prod f (Elem f as :*: g) as
forall (f :: * -> *) k (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices
ifoldMapProd
:: (FProd f, Monoid m)
=> (forall a. Elem f as a -> g a -> m)
-> Prod f g as
-> m
ifoldMapProd :: (forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd f :: forall (a :: k). Elem f as a -> g a -> m
f = Const m (Prod f Any as) -> m
forall a k (b :: k). Const a b -> a
getConst (Const m (Prod f Any as) -> m)
-> (Prod f g as -> Const m (Prod f Any as)) -> Prod f g as -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). Elem f as a -> g a -> Const m (Any a))
-> Prod f g as -> Const m (Prod f Any as)
forall k (f :: * -> *) (m :: * -> *) (as :: f k) (g :: k -> *)
(h :: k -> *).
(FProd f, Applicative m) =>
(forall (a :: k). Elem f as a -> g a -> m (h a))
-> Prod f g as -> m (Prod f h as)
itraverseProd (\i :: Elem f as a
i -> m -> Const m (Any a)
forall k a (b :: k). a -> Const a b
Const (m -> Const m (Any a)) -> (g a -> m) -> g a -> Const m (Any a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elem f as a -> g a -> m
forall (a :: k). Elem f as a -> g a -> m
f Elem f as a
i)
foldMapProd
:: (FProd f, Monoid m)
=> (forall a. g a -> m)
-> Prod f g as
-> m
foldMapProd :: (forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd f :: forall (a :: k). g a -> m
f = (forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
forall k (f :: * -> *) m (as :: f k) (g :: k -> *).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd ((g a -> m) -> Elem f as a -> g a -> m
forall a b. a -> b -> a
const g a -> m
forall (a :: k). g a -> m
f)
ifoldMapSing
:: forall f k (as :: f k) m. (FProd f, Monoid m)
=> (forall a. Elem f as a -> Sing a -> m)
-> Sing as
-> m
ifoldMapSing :: (forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
ifoldMapSing f :: forall (a :: k). Elem f as a -> Sing a -> m
f = (forall (a :: k). Elem f as a -> Sing a -> m)
-> Prod f Sing as -> m
forall k (f :: * -> *) m (as :: f k) (g :: k -> *).
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> g a -> m) -> Prod f g as -> m
ifoldMapProd forall (a :: k). Elem f as a -> Sing a -> m
f (Prod f Sing as -> m)
-> (Sing as -> Prod f Sing as) -> Sing as -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
foldMapSing
:: forall f k (as :: f k) m. (FProd f, Monoid m)
=> (forall (a :: k). Sing a -> m)
-> Sing as
-> m
foldMapSing :: (forall (a :: k). Sing a -> m) -> Sing as -> m
foldMapSing f :: forall (a :: k). Sing a -> m
f = (forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
forall (f :: * -> *) k (as :: f k) m.
(FProd f, Monoid m) =>
(forall (a :: k). Elem f as a -> Sing a -> m) -> Sing as -> m
ifoldMapSing ((Sing a -> m) -> Elem f as a -> Sing a -> m
forall a b. a -> b -> a
const Sing a -> m
forall (a :: k). Sing a -> m
f)
selectProd
:: FProd f
=> Prod f (Elem f as) bs
-> Prod f g as
-> Prod f g bs
selectProd :: Prod f (Elem f as) bs -> Prod f g as -> Prod f g bs
selectProd is :: Prod f (Elem f as) bs
is xs :: Prod f g as
xs = (forall (a :: k). Elem f as a -> g a)
-> Prod f (Elem f as) bs -> Prod f g bs
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (Elem f as a -> Prod f g as -> g a
forall k (f :: * -> *) (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Prod f g as -> g a
`indexProd` Prod f g as
xs) Prod f (Elem f as) bs
is
eqProd
:: (FProd f, ReifyConstraintProd f Eq g as)
=> Prod f g as
-> Prod f g as
-> Bool
eqProd :: Prod f g as -> Prod f g as -> Bool
eqProd xs :: Prod f g as
xs = All -> Bool
getAll
(All -> Bool) -> (Prod f g as -> All) -> Prod f g as -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). Const All a -> All)
-> Prod f (Const All) as -> All
forall k (f :: * -> *) m (g :: k -> *) (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd forall (a :: k). Const All a -> All
forall a k (b :: k). Const a b -> a
getConst
(Prod f (Const All) as -> All)
-> (Prod f g as -> Prod f (Const All) as) -> Prod f g as -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). (:.) (Dict Eq) g a -> g a -> Const All a)
-> Prod f (Dict Eq :. g) as -> Prod f g as -> Prod f (Const All) as
forall (f :: * -> *) k (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd (\(V.Compose (Dict x)) y :: g a
y -> All -> Const All a
forall k a (b :: k). a -> Const a b
Const (Bool -> All
All (g a
x g a -> g a -> Bool
forall a. Eq a => a -> a -> Bool
== g a
y)))
(Prod f g as -> Prod f (Dict Eq :. g) as
forall k (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Eq Prod f g as
xs)
compareProd
:: (FProd f, ReifyConstraintProd f Ord g as)
=> Prod f g as
-> Prod f g as
-> Ordering
compareProd :: Prod f g as -> Prod f g as -> Ordering
compareProd xs :: Prod f g as
xs = (forall (a :: k). Const Ordering a -> Ordering)
-> Prod f (Const Ordering) as -> Ordering
forall k (f :: * -> *) m (g :: k -> *) (as :: f k).
(FProd f, Monoid m) =>
(forall (a :: k). g a -> m) -> Prod f g as -> m
foldMapProd forall (a :: k). Const Ordering a -> Ordering
forall a k (b :: k). Const a b -> a
getConst
(Prod f (Const Ordering) as -> Ordering)
-> (Prod f g as -> Prod f (Const Ordering) as)
-> Prod f g as
-> Ordering
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). (:.) (Dict Ord) g a -> g a -> Const Ordering a)
-> Prod f (Dict Ord :. g) as
-> Prod f g as
-> Prod f (Const Ordering) as
forall (f :: * -> *) k (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd (\(V.Compose (Dict x)) y :: g a
y -> Ordering -> Const Ordering a
forall k a (b :: k). a -> Const a b
Const (g a -> g a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare g a
x g a
y))
(Prod f g as -> Prod f (Dict Ord :. g) as
forall k (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Ord Prod f g as
xs)
generateProd
:: (FProd f, PureProd f as)
=> (forall a. Elem f as a -> g a)
-> Prod f g as
generateProd :: (forall (a :: k). Elem f as a -> g a) -> Prod f g as
generateProd f :: forall (a :: k). Elem f as a -> g a
f = (forall (a :: k). Elem f as a -> g a)
-> Prod f (Elem f as) as -> Prod f g as
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall (a :: k). Elem f as a -> g a
f Prod f (Elem f as) as
forall k (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices
generateProdA
:: (FProd f, PureProd f as, Applicative m)
=> (forall a. Elem f as a -> m (g a))
-> m (Prod f g as)
generateProdA :: (forall (a :: k). Elem f as a -> m (g a)) -> m (Prod f g as)
generateProdA f :: forall (a :: k). Elem f as a -> m (g a)
f = (forall (a :: k). Elem f as a -> m (g a))
-> Prod f (Elem f as) as -> m (Prod f g as)
forall (f :: * -> *) k (g :: k -> *) (h :: k -> *) (as :: f k)
(m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd forall (a :: k). Elem f as a -> m (g a)
f Prod f (Elem f as) as
forall k (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices
data Index :: [k] -> k -> Type where
IZ :: Index (a ': as) a
IS :: Index bs a -> Index (b ': bs) a
deriving instance Show (Index as a)
deriving instance Eq (Index as a)
deriving instance Ord (Index as a)
data SIndex as a :: Index as a -> Type where
SIZ :: SIndex (a ': as) a 'IZ
SIS :: SIndex bs a i -> SIndex (b ': bs) a ('IS i)
deriving instance Show (SIndex as a i)
type instance Sing = SIndex as a :: Index as a -> Type
instance SingI 'IZ where
sing :: Sing 'IZ
sing = Sing 'IZ
forall k (a :: k) (as :: [k]). SIndex (a : as) a 'IZ
SIZ
instance SingI i => SingI ('IS i) where
sing :: Sing ('IS i)
sing = SIndex bs a i -> SIndex (b : bs) a ('IS i)
forall k (bs :: [k]) (a :: k) (i :: Index bs a) (b :: k).
SIndex bs a i -> SIndex (b : bs) a ('IS i)
SIS SIndex bs a i
forall k (a :: k). SingI a => Sing a
sing
instance SingKind (Index as a) where
type Demote (Index as a) = Index as a
fromSing :: Sing a -> Demote (Index as a)
fromSing = \case
SIZ -> Demote (Index as a)
forall k (a :: k) (as :: [k]). Index (a : as) a
IZ
SIS j -> Index bs a -> Index (b : bs) a
forall k (bs :: [k]) (a :: k) (b :: k).
Index bs a -> Index (b : bs) a
IS (Sing i -> Demote (Index bs a)
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing i
SIndex bs a i
j)
toSing :: Demote (Index as a) -> SomeSing (Index as a)
toSing i :: Demote (Index as a)
i = Index as a
-> (forall (i :: Index as a).
SIndex as a i -> SomeSing (Index as a))
-> SomeSing (Index as a)
forall k (bs :: [k]) (b :: k) r.
Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
go Demote (Index as a)
Index as a
i forall k (a :: k). Sing a -> SomeSing k
forall (i :: Index as a). SIndex as a i -> SomeSing (Index as a)
SomeSing
where
go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r
go :: Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
go = \case
IZ -> ((SIndex bs b 'IZ -> r) -> SIndex bs b 'IZ -> r
forall a b. (a -> b) -> a -> b
$ SIndex bs b 'IZ
forall k (a :: k) (as :: [k]). SIndex (a : as) a 'IZ
SIZ)
IS j :: Index bs b
j -> \f :: forall (i :: Index bs b). SIndex bs b i -> r
f -> Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
forall k (bs :: [k]) (b :: k) r.
Index bs b -> (forall (i :: Index bs b). SIndex bs b i -> r) -> r
go Index bs b
j (SIndex bs b ('IS i) -> r
forall (i :: Index bs b). SIndex bs b i -> r
f (SIndex bs b ('IS i) -> r)
-> (SIndex bs b i -> SIndex bs b ('IS i)) -> SIndex bs b i -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIndex bs b i -> SIndex bs b ('IS i)
forall k (bs :: [k]) (a :: k) (i :: Index bs a) (b :: k).
SIndex bs a i -> SIndex (b : bs) a ('IS i)
SIS)
instance SDecide (Index as a) where
%~ :: Sing a -> Sing b -> Decision (a :~: b)
(%~) = \case
SIZ -> \case
SIZ -> (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
SIS _ -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
SIS i' -> \case
SIZ -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
SIS j' -> case Sing i
SIndex bs a i
i' Sing i -> Sing i -> Decision (i :~: i)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing i
SIndex bs a i
j' of
Proved Refl -> (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
Disproved v :: Refuted (i :~: i)
v -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case Refl -> Refuted (i :~: i)
v i :~: i
forall k (a :: k). a :~: a
Refl
instance FProd [] where
type Elem [] = Index
type Prod [] = Rec
singProd :: Sing as -> Prod [] Sing as
singProd = \case
SNil -> Prod [] Sing as
forall u (a :: u -> *). Rec a '[]
RNil
x `SCons` xs -> Sing n1
x Sing n1 -> Rec Sing n2 -> Rec Sing (n1 : n2)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing n2 -> Prod [] Sing n2
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd Sing n2
xs
prodSing :: Prod [] Sing as -> Sing as
prodSing = \case
RNil -> Sing as
forall a0. SList '[]
SNil
x :& xs -> Sing r
x Sing r -> Sing rs -> SList (r : rs)
forall a0 (n1 :: a0) (n2 :: [a0]).
Sing n1 -> Sing n2 -> SList (n1 : n2)
`SCons` Prod [] Sing rs -> Sing rs
forall (f :: * -> *) k (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing rs
Prod [] Sing rs
xs
traverseProd
:: forall g h m as. Applicative m
=> (forall a. g a -> m (h a))
-> Prod [] g as
-> m (Prod [] h as)
traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod [] g as -> m (Prod [] h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f = Prod [] g as -> m (Prod [] h as)
forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go
where
go :: Prod [] g bs -> m (Prod [] h bs)
go :: Prod [] g bs -> m (Prod [] h bs)
go = \case
RNil -> Rec h '[] -> m (Rec h '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec h '[]
forall u (a :: u -> *). Rec a '[]
RNil
x :& xs -> h r -> Rec h rs -> Rec h (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) (h r -> Rec h rs -> Rec h (r : rs))
-> m (h r) -> m (Rec h rs -> Rec h (r : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g r -> m (h r)
forall (a :: k). g a -> m (h a)
f g r
x m (Rec h rs -> Rec h (r : rs))
-> m (Rec h rs) -> m (Rec h (r : rs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Prod [] g rs -> m (Prod [] h rs)
forall (bs :: [k]). Prod [] g bs -> m (Prod [] h bs)
go Rec g rs
Prod [] g rs
xs
zipWithProd
:: forall g h j as. ()
=> (forall a. g a -> h a -> j a)
-> Prod [] g as
-> Prod [] h as
-> Prod [] j as
zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod [] g as -> Prod [] h as -> Prod [] j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f = Prod [] g as -> Prod [] h as -> Prod [] j as
forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go
where
go :: Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go :: Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go = \case
RNil -> \case
RNil -> Prod [] j bs
forall u (a :: u -> *). Rec a '[]
RNil
x :& xs -> \case
y :& ys -> g r -> h r -> j r
forall (a :: k). g a -> h a -> j a
f g r
x h r
h r
y j r -> Rec j rs -> Rec j (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Prod [] g rs -> Prod [] h rs -> Prod [] j rs
forall (bs :: [k]). Prod [] g bs -> Prod [] h bs -> Prod [] j bs
go Rec g rs
Prod [] g rs
xs Rec h rs
Prod [] h rs
ys
htraverse
:: forall ff g h as m. Applicative m
=> Sing ff
-> (forall a. g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
htraverse _ f :: forall (a :: a0). g a -> m (h (ff @@ a))
f = Prod [] g as -> m (Prod [] h (Fmap ff as))
forall (bs :: [a0]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go
where
go :: Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go :: Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go = \case
RNil -> Rec h '[] -> m (Rec h '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec h '[]
forall u (a :: u -> *). Rec a '[]
RNil
x :& xs -> h (Apply ff r)
-> Rec h (Fmap_6989586621680022960 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621680022960 ff rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
(:&) (h (Apply ff r)
-> Rec h (Fmap_6989586621680022960 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621680022960 ff rs))
-> m (h (Apply ff r))
-> m (Rec h (Fmap_6989586621680022960 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621680022960 ff rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g r -> m (h (Apply ff r))
forall (a :: a0). g a -> m (h (ff @@ a))
f g r
x m (Rec h (Fmap_6989586621680022960 ff rs)
-> Rec h (Apply ff r : Fmap_6989586621680022960 ff rs))
-> m (Rec h (Fmap_6989586621680022960 ff rs))
-> m (Rec h (Apply ff r : Fmap_6989586621680022960 ff rs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Prod [] g rs -> m (Prod [] h (Fmap ff rs))
forall (bs :: [a0]). Prod [] g bs -> m (Prod [] h (Fmap ff bs))
go Rec g rs
Prod [] g rs
xs
withIndices :: Prod [] g as -> Prod [] (Elem [] as :*: g) as
withIndices = \case
RNil -> Prod [] (Elem [] as :*: g) as
forall u (a :: u -> *). Rec a '[]
RNil
x :& xs -> (Index (r : rs) r
forall k (a :: k) (as :: [k]). Index (a : as) a
IZ Index (r : rs) r -> g r -> (:*:) (Index (r : rs)) g r
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g r
x) (:*:) (Index (r : rs)) g r
-> Rec (Index (r : rs) :*: g) rs
-> Rec (Index (r : rs) :*: g) (r : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& (forall (a :: k).
(:*:) (Index rs) g a -> (:*:) (Index (r : rs)) g a)
-> Prod [] (Index rs :*: g) rs -> Prod [] (Index (r : rs) :*: g) rs
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (\(i :*: y) -> Index rs a -> Index (r : rs) a
forall k (bs :: [k]) (a :: k) (b :: k).
Index bs a -> Index (b : bs) a
IS Index rs a
i Index (r : rs) a -> g a -> (:*:) (Index (r : rs)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (Prod [] g rs -> Prod [] (Elem [] rs :*: g) rs
forall (f :: * -> *) k (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices Rec g rs
Prod [] g rs
xs)
ixProd
:: forall g as a. ()
=> Elem [] as a
-> Lens' (Prod [] g as) (g a)
ixProd :: Elem [] as a -> Lens' (Prod [] g as) (g a)
ixProd i0 :: Elem [] as a
i0 (g a -> f (g a)
f :: g a -> h (g a)) = Elem [] as a -> Prod [] g as -> f (Prod [] g as)
forall (bs :: [k]).
Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go Elem [] as a
i0
where
go :: Elem [] bs a -> Prod [] g bs -> h (Prod [] g bs)
go :: Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go = \case
IZ -> \case
x :& xs -> (g a -> Rec g rs -> Rec g (a : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g rs
xs) (g a -> Rec g (a : rs)) -> f (g a) -> f (Rec g (a : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g r
x
IS i -> \case
x :& xs -> (g r
x g r -> Rec g bs -> Rec g (r : bs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:&) (Rec g bs -> Rec g (r : bs)) -> f (Rec g bs) -> f (Rec g (r : bs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
forall (bs :: [k]).
Elem [] bs a -> Prod [] g bs -> f (Prod [] g bs)
go Index bs a
Elem [] bs a
i Rec g rs
Prod [] g bs
xs
toRec :: Prod [] g as -> Rec g (ToList as)
toRec = Prod [] g as -> Rec g (ToList as)
forall a. a -> a
id
withPureProd :: Prod [] g as -> (PureProd [] as => r) -> r
withPureProd = Prod [] g as -> (PureProd [] as => r) -> r
forall k (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList
withPureProdList
:: Rec f as
-> ((RecApplicative as, PureProd [] as) => r)
-> r
withPureProdList :: Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList = \case
RNil -> ((RecApplicative as, PureProd [] as) => r) -> r
forall a. a -> a
id
_ :& xs :: Rec f rs
xs -> Rec f rs -> ((RecApplicative rs, PureProd [] rs) => r) -> r
forall k (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList Rec f rs
xs
instance RecApplicative as => PureProd [] as where
pureProd :: (forall (a :: k). g a) -> Prod [] g as
pureProd = (forall (a :: k). g a) -> Prod [] g as
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure
instance RPureConstrained c as => PureProdC [] c as where
pureProdC :: (forall (a :: k). c a => g a) -> Prod [] g as
pureProdC = forall (ts :: [k]) (f :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). c a => f a) -> Rec f ts
forall u (c :: u -> Constraint) (ts :: [u]) (f :: u -> *).
RPureConstrained c ts =>
(forall (a :: u). c a => f a) -> Rec f ts
rpureConstrained @c
instance ReifyConstraint c f as => ReifyConstraintProd [] c f as where
reifyConstraintProd :: Prod [] f as -> Prod [] (Dict c :. f) as
reifyConstraintProd = forall u (c :: * -> Constraint) (f :: u -> *) (rs :: [u]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
forall (f :: k -> *) (rs :: [k]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
reifyConstraint @c
data IJust :: Maybe k -> k -> Type where
IJust :: IJust ('Just a) a
deriving instance Show (IJust as a)
deriving instance Read (IJust ('Just a) a)
deriving instance Eq (IJust as a)
deriving instance Ord (IJust as a)
data SIJust as a :: IJust as a -> Type where
SIJust :: SIJust ('Just a) a 'IJust
deriving instance Show (SIJust as a i)
type instance Sing = SIJust as a :: IJust as a -> Type
instance SingI 'IJust where
sing :: Sing 'IJust
sing = Sing 'IJust
forall k (a :: k). SIJust ('Just a) a 'IJust
SIJust
instance SingKind (IJust as a) where
type Demote (IJust as a) = IJust as a
fromSing :: Sing a -> Demote (IJust as a)
fromSing SIJust = Demote (IJust as a)
forall k (a :: k). IJust ('Just a) a
IJust
toSing :: Demote (IJust as a) -> SomeSing (IJust as a)
toSing IJust = Sing 'IJust -> SomeSing (IJust as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IJust
forall k (a :: k). SIJust ('Just a) a 'IJust
SIJust
instance SDecide (IJust as a) where
SIJust %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ SIJust = (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
data PMaybe :: (k -> Type) -> Maybe k -> Type where
PNothing :: PMaybe f 'Nothing
PJust :: f a -> PMaybe f ('Just a)
instance ReifyConstraintProd Maybe Show f as => Show (PMaybe f as) where
showsPrec :: Int -> PMaybe f as -> ShowS
showsPrec d :: Int
d xs :: PMaybe f as
xs = case Prod Maybe f as -> Prod Maybe (Dict Show :. f) as
forall k (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Show PMaybe f as
Prod Maybe f as
xs of
PNothing -> String -> ShowS
showString "PNothing"
PJust (V.Compose (Dict x)) -> (Int -> f a -> ShowS) -> String -> Int -> f a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec "PJust" Int
d f a
x
instance ReifyConstraintProd Maybe Eq f as => Eq (PMaybe f as) where
== :: PMaybe f as -> PMaybe f as -> Bool
(==) = PMaybe f as -> PMaybe f as -> Bool
forall k (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Eq g as) =>
Prod f g as -> Prod f g as -> Bool
eqProd
instance (ReifyConstraintProd Maybe Eq f as, ReifyConstraintProd Maybe Ord f as) => Ord (PMaybe f as) where
compare :: PMaybe f as -> PMaybe f as -> Ordering
compare = PMaybe f as -> PMaybe f as -> Ordering
forall k (f :: * -> *) (g :: k -> *) (as :: f k).
(FProd f, ReifyConstraintProd f Ord g as) =>
Prod f g as -> Prod f g as -> Ordering
compareProd
instance FProd Maybe where
type instance Elem Maybe = IJust
type instance Prod Maybe = PMaybe
singProd :: Sing as -> Prod Maybe Sing as
singProd = \case
SNothing -> Prod Maybe Sing as
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
SJust x -> Sing n -> PMaybe Sing ('Just n)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust Sing n
x
prodSing :: Prod Maybe Sing as -> Sing as
prodSing = \case
PNothing -> Sing as
forall a0. SMaybe 'Nothing
SNothing
PJust x -> Sing a -> SMaybe ('Just a)
forall a0 (n :: a0). Sing n -> SMaybe ('Just n)
SJust Sing a
x
withIndices :: Prod Maybe g as -> Prod Maybe (Elem Maybe as :*: g) as
withIndices = \case
PNothing -> Prod Maybe (Elem Maybe as :*: g) as
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust x -> (:*:) (IJust ('Just a)) g a
-> PMaybe (IJust ('Just a) :*: g) ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (IJust ('Just a) a
forall k (a :: k). IJust ('Just a) a
IJust IJust ('Just a) a -> g a -> (:*:) (IJust ('Just a)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod Maybe g as -> m (Prod Maybe h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f = \case
PNothing -> PMaybe h 'Nothing -> m (PMaybe h 'Nothing)
forall (f :: * -> *) a. Applicative f => a -> f a
pure PMaybe h 'Nothing
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust x -> h a -> PMaybe h ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (h a -> PMaybe h ('Just a)) -> m (h a) -> m (PMaybe h ('Just a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x
zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod Maybe g as -> Prod Maybe h as -> Prod Maybe j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f = \case
PNothing -> \case
PNothing -> Prod Maybe j as
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust x -> \case
PJust y -> j a -> PMaybe j ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y)
htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod Maybe g as
-> m (Prod Maybe h (Fmap ff as))
htraverse _ f :: forall (a :: a0). g a -> m (h (ff @@ a))
f = \case
PNothing -> PMaybe h 'Nothing -> m (PMaybe h 'Nothing)
forall (f :: * -> *) a. Applicative f => a -> f a
pure PMaybe h 'Nothing
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
PJust x -> h (Apply ff a) -> PMaybe h ('Just (Apply ff a))
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (h (Apply ff a) -> PMaybe h ('Just (Apply ff a)))
-> m (h (Apply ff a)) -> m (PMaybe h ('Just (Apply ff a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a0). g a -> m (h (ff @@ a))
f g a
x
ixProd :: Elem Maybe as a -> Lens' (Prod Maybe g as) (g a)
ixProd = \case
IJust -> \f :: g a -> f (g a)
f -> \case
PJust x -> g a -> PMaybe g ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (g a -> PMaybe g ('Just a)) -> f (g a) -> f (PMaybe g ('Just a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g a
x
toRec :: Prod Maybe g as -> Rec g (ToList as)
toRec = \case
PNothing -> Rec g (ToList as)
forall u (a :: u -> *). Rec a '[]
RNil
PJust x -> g a
x g a -> Rec g '[] -> Rec g '[a]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
forall u (a :: u -> *). Rec a '[]
RNil
withPureProd :: Prod Maybe g as -> (PureProd Maybe as => r) -> r
withPureProd = \case
PNothing -> (PureProd Maybe as => r) -> r
forall a. a -> a
id
PJust _ -> (PureProd Maybe as => r) -> r
forall a. a -> a
id
instance PureProd Maybe 'Nothing where
pureProd :: (forall (a :: k). g a) -> Prod Maybe g 'Nothing
pureProd _ = Prod Maybe g 'Nothing
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
instance PureProd Maybe ('Just a) where
pureProd :: (forall (a :: k). g a) -> Prod Maybe g ('Just a)
pureProd x :: forall (a :: k). g a
x = g a -> PMaybe g ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust g a
forall (a :: k). g a
x
instance PureProdC Maybe c 'Nothing where
pureProdC :: (forall (a :: k). c a => g a) -> Prod Maybe g 'Nothing
pureProdC _ = Prod Maybe g 'Nothing
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
instance c a => PureProdC Maybe c ('Just a) where
pureProdC :: (forall (a :: a). c a => g a) -> Prod Maybe g ('Just a)
pureProdC x :: forall (a :: a). c a => g a
x = g a -> PMaybe g ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust g a
forall (a :: a). c a => g a
x
instance ReifyConstraintProd Maybe c g 'Nothing where
reifyConstraintProd :: Prod Maybe g 'Nothing -> Prod Maybe (Dict c :. g) 'Nothing
reifyConstraintProd PNothing = Prod Maybe (Dict c :. g) 'Nothing
forall k (f :: k -> *). PMaybe f 'Nothing
PNothing
instance c (g a) => ReifyConstraintProd Maybe c g ('Just a) where
reifyConstraintProd :: Prod Maybe g ('Just a) -> Prod Maybe (Dict c :. g) ('Just a)
reifyConstraintProd (PJust x) = Compose (Dict c) g a -> PMaybe (Dict c :. g) ('Just a)
forall a (f :: a -> *) (a :: a). f a -> PMaybe f ('Just a)
PJust (Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x))
data IRight :: Either j k -> k -> Type where
IRight :: IRight ('Right a) a
deriving instance Show (IRight as a)
deriving instance Read (IRight ('Right a) a)
deriving instance Eq (IRight as a)
deriving instance Ord (IRight as a)
data SIRight as a :: IRight as a -> Type where
SIRight :: SIRight ('Right a) a 'IRight
deriving instance Show (SIRight as a i)
type instance Sing = SIRight as a :: IRight as a -> Type
instance SingI 'IRight where
sing :: Sing 'IRight
sing = Sing 'IRight
forall k j (a :: k). SIRight ('Right a) a 'IRight
SIRight
instance SingKind (IRight as a) where
type Demote (IRight as a) = IRight as a
fromSing :: Sing a -> Demote (IRight as a)
fromSing SIRight = Demote (IRight as a)
forall k j (a :: k). IRight ('Right a) a
IRight
toSing :: Demote (IRight as a) -> SomeSing (IRight as a)
toSing IRight = Sing 'IRight -> SomeSing (IRight as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IRight
forall k j (a :: k). SIRight ('Right a) a 'IRight
SIRight
instance SDecide (IRight as a) where
SIRight %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ SIRight = (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
data PEither :: (k -> Type) -> Either j k -> Type where
PLeft :: Sing e -> PEither f ('Left e)
PRight :: f a -> PEither f ('Right a)
instance (SShow j, ReifyConstraintProd (Either j) Show f as) => Show (PEither f as) where
showsPrec :: Int -> PEither f as -> ShowS
showsPrec d :: Int
d xs :: PEither f as
xs = case Prod (Either j) f as -> Prod (Either j) (Dict Show :. f) as
forall k (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @Show PEither f as
Prod (Either j) f as
xs of
PLeft e -> (Int -> Sing e -> ShowS) -> String -> Int -> Sing e -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> Sing e -> ShowS
forall a a (t2 :: a).
(Integral a, SShow a) =>
a -> Sing t2 -> ShowS
go "PLeft" Int
d Sing e
e
PRight (V.Compose (Dict x)) -> (Int -> f a -> ShowS) -> String -> Int -> f a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec "PRight" Int
d f a
x
where
go :: a -> Sing t2 -> ShowS
go (a -> Demote Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral->FromSing i) x :: Sing t2
x (String -> Text
T.pack->FromSing str) = Text -> String
T.unpack (Text -> String)
-> (SSymbol (ShowsPrec a t2 a) -> Text)
-> SSymbol (ShowsPrec a t2 a)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SSymbol (ShowsPrec a t2 a) -> Text
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (SSymbol (ShowsPrec a t2 a) -> String)
-> SSymbol (ShowsPrec a t2 a) -> String
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing t2
-> Sing a
-> Sing (Apply (Apply (Apply ShowsPrecSym0 a) t2) a)
forall a (t1 :: Nat) (t2 :: a) (t3 :: Symbol).
SShow a =>
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)
sShowsPrec Sing a
i Sing t2
x Sing a
str
go _ _ _ = String
forall a. HasCallStack => a
undefined
instance FProd (Either j) where
type instance Elem (Either j) = IRight
type instance Prod (Either j) = PEither
singProd :: Sing as -> Prod (Either j) Sing as
singProd = \case
SLeft e -> Sing n -> PEither Sing ('Left n)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing n
e
SRight x -> Sing n -> PEither Sing ('Right n)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight Sing n
x
prodSing :: Prod (Either j) Sing as -> Sing as
prodSing = \case
PLeft e -> Sing e -> SEither ('Left e)
forall b0 a0 (n :: a0). Sing n -> SEither ('Left n)
SLeft Sing e
e
PRight x -> Sing a -> SEither ('Right a)
forall a0 b0 (n :: b0). Sing n -> SEither ('Right n)
SRight Sing a
x
withIndices :: Prod (Either j) g as
-> Prod (Either j) (Elem (Either j) as :*: g) as
withIndices = \case
PLeft e -> Sing e -> PEither (IRight ('Left e) :*: g) ('Left e)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing e
e
PRight x -> (:*:) (IRight ('Right a)) g a
-> PEither (IRight ('Right a) :*: g) ('Right a)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight (IRight ('Right a) a
forall k j (a :: k). IRight ('Right a) a
IRight IRight ('Right a) a -> g a -> (:*:) (IRight ('Right a)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod (Either j) g as -> m (Prod (Either j) h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f = \case
PLeft e -> PEither h ('Left e) -> m (PEither h ('Left e))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sing e -> PEither h ('Left e)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing e
e)
PRight x -> h a -> PEither h ('Right a)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight (h a -> PEither h ('Right a))
-> m (h a) -> m (PEither h ('Right a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x
zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod (Either j) g as
-> Prod (Either j) h as
-> Prod (Either j) j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f = \case
PLeft e -> \case
PLeft _ -> Sing e -> PEither j ('Left e)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing e
e
PRight x -> \case
PRight y -> j a -> PEither j ('Right a)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y)
htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod (Either j) g as
-> m (Prod (Either j) h (Fmap ff as))
htraverse _ f :: forall (a :: a0). g a -> m (h (ff @@ a))
f = \case
PLeft e -> PEither h ('Left e) -> m (PEither h ('Left e))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sing e -> PEither h ('Left e)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing e
e)
PRight x -> h (Apply ff a) -> PEither h ('Right (Apply ff a))
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight (h (Apply ff a) -> PEither h ('Right (Apply ff a)))
-> m (h (Apply ff a)) -> m (PEither h ('Right (Apply ff a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a0). g a -> m (h (ff @@ a))
f g a
x
ixProd :: Elem (Either j) as a -> Lens' (Prod (Either j) g as) (g a)
ixProd = \case
IRight -> \f :: g a -> f (g a)
f -> \case
PRight x -> g a -> PEither g ('Right a)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight (g a -> PEither g ('Right a))
-> f (g a) -> f (PEither g ('Right a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g a
x
toRec :: Prod (Either j) g as -> Rec g (ToList as)
toRec = \case
PLeft _ -> Rec g (ToList as)
forall u (a :: u -> *). Rec a '[]
RNil
PRight x -> g a
x g a -> Rec g '[] -> Rec g '[a]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
forall u (a :: u -> *). Rec a '[]
RNil
withPureProd :: Prod (Either j) g as -> (PureProd (Either j) as => r) -> r
withPureProd = \case
PLeft Sing -> (PureProd (Either j) as => r) -> r
forall a. a -> a
id
PRight _ -> (PureProd (Either j) as => r) -> r
forall a. a -> a
id
instance SingI e => PureProd (Either j) ('Left e) where
pureProd :: (forall (a :: k). g a) -> Prod (Either j) g ('Left e)
pureProd _ = Sing e -> PEither g ('Left e)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing e
forall k (a :: k). SingI a => Sing a
sing
instance PureProd (Either j) ('Right a) where
pureProd :: (forall (a :: k). g a) -> Prod (Either j) g ('Right a)
pureProd x :: forall (a :: k). g a
x = g a -> PEither g ('Right a)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight g a
forall (a :: k). g a
x
instance SingI e => PureProdC (Either j) c ('Left e) where
pureProdC :: (forall (a :: k). c a => g a) -> Prod (Either j) g ('Left e)
pureProdC _ = (Sing e -> PEither g ('Left e)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing e
forall k (a :: k). SingI a => Sing a
sing)
instance c a => PureProdC (Either j) c ('Right a) where
pureProdC :: (forall (a :: b). c a => g a) -> Prod (Either j) g ('Right a)
pureProdC x :: forall (a :: b). c a => g a
x = g a -> PEither g ('Right a)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight g a
forall (a :: b). c a => g a
x
instance ReifyConstraintProd (Either j) c g ('Left e) where
reifyConstraintProd :: Prod (Either j) g ('Left e)
-> Prod (Either j) (Dict c :. g) ('Left e)
reifyConstraintProd (PLeft e) = Sing e -> PEither (Dict c :. g) ('Left e)
forall j k (e :: j) (f :: k -> *). Sing e -> PEither f ('Left e)
PLeft Sing e
Sing e
e
instance c (g a) => ReifyConstraintProd (Either j) c g ('Right a) where
reifyConstraintProd :: Prod (Either j) g ('Right a)
-> Prod (Either j) (Dict c :. g) ('Right a)
reifyConstraintProd (PRight x) = Compose (Dict c) g a -> PEither (Dict c :. g) ('Right a)
forall b j (f :: b -> *) (a :: b). f a -> PEither f ('Right a)
PRight (Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x))
data NEIndex :: NonEmpty k -> k -> Type where
NEHead :: NEIndex (a ':| as) a
NETail :: Index as a -> NEIndex (b ':| as) a
deriving instance Show (NEIndex as a)
deriving instance Eq (NEIndex as a)
deriving instance Ord (NEIndex as a)
data SNEIndex as a :: NEIndex as a -> Type where
SNEHead :: SNEIndex (a ':| as) a 'NEHead
SNETail :: SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)
deriving instance Show (SNEIndex as a i)
type instance Sing = SNEIndex as a :: NEIndex as a -> Type
instance SingI 'NEHead where
sing :: Sing 'NEHead
sing = Sing 'NEHead
forall k (a :: k) (as :: [k]). SNEIndex (a ':| as) a 'NEHead
SNEHead
instance SingI i => SingI ('NETail i) where
sing :: Sing ('NETail i)
sing = SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)
forall k (as :: [k]) (a :: k) (i :: Index as a) (b :: k).
SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)
SNETail SIndex as a i
forall k (a :: k). SingI a => Sing a
sing
instance SingKind (NEIndex as a) where
type Demote (NEIndex as a) = NEIndex as a
fromSing :: Sing a -> Demote (NEIndex as a)
fromSing = \case
SNEHead -> Demote (NEIndex as a)
forall k (a :: k) (as :: [k]). NEIndex (a ':| as) a
NEHead
SNETail i -> Index as a -> Demote (NEIndex as a)
forall k (as :: [k]) (a :: k) (b :: k).
Index as a -> NEIndex (b ':| as) a
NETail (Index as a -> Demote (NEIndex as a))
-> Index as a -> Demote (NEIndex as a)
forall a b. (a -> b) -> a -> b
$ Sing i -> Demote (Index as a)
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing i
SIndex as a i
i
toSing :: Demote (NEIndex as a) -> SomeSing (NEIndex as a)
toSing = \case
NEHead -> Sing 'NEHead -> SomeSing (NEIndex as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'NEHead
forall k (a :: k) (as :: [k]). SNEIndex (a ':| as) a 'NEHead
SNEHead
NETail i -> Demote (Index as a)
-> (forall (a :: Index as a). Sing a -> SomeSing (NEIndex as a))
-> SomeSing (NEIndex as a)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote (Index as a)
Index as a
i ((forall (a :: Index as a). Sing a -> SomeSing (NEIndex as a))
-> SomeSing (NEIndex as a))
-> (forall (a :: Index as a). Sing a -> SomeSing (NEIndex as a))
-> SomeSing (NEIndex as a)
forall a b. (a -> b) -> a -> b
$ SNEIndex (b ':| as) a ('NETail a)
-> SomeSing (NEIndex (b ':| as) a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing (SNEIndex (b ':| as) a ('NETail a)
-> SomeSing (NEIndex (b ':| as) a))
-> (SIndex as a a -> SNEIndex (b ':| as) a ('NETail a))
-> SIndex as a a
-> SomeSing (NEIndex (b ':| as) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIndex as a a -> SNEIndex (b ':| as) a ('NETail a)
forall k (as :: [k]) (a :: k) (i :: Index as a) (b :: k).
SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)
SNETail
instance SDecide (NEIndex as a) where
%~ :: Sing a -> Sing b -> Decision (a :~: b)
(%~) = \case
SNEHead -> \case
SNEHead -> (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
SNETail _ -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
SNETail i -> \case
SNEHead -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case {}
SNETail j -> case Sing i
SIndex as a i
i Sing i -> Sing i -> Decision (i :~: i)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing i
SIndex as a i
j of
Proved Refl -> (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
Disproved v :: Refuted (i :~: i)
v -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (Refuted (a :~: b) -> Decision (a :~: b))
-> Refuted (a :~: b) -> Decision (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case Refl -> Refuted (i :~: i)
v i :~: i
forall k (a :: k). a :~: a
Refl
data NERec :: (k -> Type) -> NonEmpty k -> Type where
(:&|) :: f a -> Rec f as -> NERec f (a ':| as)
infixr 5 :&|
deriving instance (Show (f a), RMap as, ReifyConstraint Show f as, RecordToList as) => Show (NERec f (a ':| as))
deriving instance (Eq (f a), Eq (Rec f as)) => Eq (NERec f (a ':| as))
deriving instance (Ord (f a), Ord (Rec f as)) => Ord (NERec f (a ':| as))
instance FProd NonEmpty where
type instance Elem NonEmpty = NEIndex
type instance Prod NonEmpty = NERec
singProd :: Sing as -> Prod NonEmpty Sing as
singProd (x NE.:%| xs) = Sing n1
x Sing n1 -> Rec Sing n2 -> NERec Sing (n1 ':| n2)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| Sing n2 -> Prod [] Sing n2
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd Sing n2
xs
prodSing :: Prod NonEmpty Sing as -> Sing as
prodSing (x :&| xs) = Sing a
x Sing a -> Sing as -> SNonEmpty (a ':| as)
forall a0 (n1 :: a0) (n2 :: [a0]).
Sing n1 -> Sing n2 -> SNonEmpty (n1 ':| n2)
NE.:%| Prod [] Sing as -> Sing as
forall (f :: * -> *) k (as :: f k).
FProd f =>
Prod f Sing as -> Sing as
prodSing Rec Sing as
Prod [] Sing as
xs
withIndices :: Prod NonEmpty g as -> Prod NonEmpty (Elem NonEmpty as :*: g) as
withIndices (x :&| xs) =
(NEIndex (a ':| as) a
forall k (a :: k) (as :: [k]). NEIndex (a ':| as) a
NEHead NEIndex (a ':| as) a -> g a -> (:*:) (NEIndex (a ':| as)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
(:*:) (NEIndex (a ':| as)) g a
-> Rec (NEIndex (a ':| as) :*: g) as
-> NERec (NEIndex (a ':| as) :*: g) (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| (forall (a :: k).
(:*:) (Index as) g a -> (:*:) (NEIndex (a ':| as)) g a)
-> Prod [] (Index as :*: g) as
-> Prod [] (NEIndex (a ':| as) :*: g) as
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (\(i :*: y) -> Index as a -> NEIndex (a ':| as) a
forall k (as :: [k]) (a :: k) (b :: k).
Index as a -> NEIndex (b ':| as) a
NETail Index as a
i NEIndex (a ':| as) a -> g a -> (:*:) (NEIndex (a ':| as)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
y) (Prod [] g as -> Prod [] (Elem [] as :*: g) as
forall (f :: * -> *) k (g :: k -> *) (as :: f k).
FProd f =>
Prod f g as -> Prod f (Elem f as :*: g) as
withIndices Rec g as
Prod [] g as
xs)
traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod NonEmpty g as -> m (Prod NonEmpty h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f (x :&| xs) =
h a -> Rec h as -> NERec h (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
(:&|) (h a -> Rec h as -> NERec h (a ':| as))
-> m (h a) -> m (Rec h as -> NERec h (a ':| as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x m (Rec h as -> NERec h (a ':| as))
-> m (Rec h as) -> m (NERec h (a ':| as))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (a :: k). g a -> m (h a))
-> Prod [] g as -> m (Prod [] h as)
forall (f :: * -> *) k (g :: k -> *) (h :: k -> *) (as :: f k)
(m :: * -> *).
(FProd f, Applicative m) =>
(forall (a :: k). g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
traverseProd forall (a :: k). g a -> m (h a)
f Rec g as
Prod [] g as
xs
zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod NonEmpty g as -> Prod NonEmpty h as -> Prod NonEmpty j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f (x :&| xs) (y :&| ys) = g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y j a -> Rec j as -> NERec j (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| (forall (a :: k). g a -> h a -> j a)
-> Prod [] g as -> Prod [] h as -> Prod [] j as
forall (f :: * -> *) k (g :: k -> *) (h :: k -> *) (j :: k -> *)
(as :: f k).
FProd f =>
(forall (a :: k). g a -> h a -> j a)
-> Prod f g as -> Prod f h as -> Prod f j as
zipWithProd forall (a :: k). g a -> h a -> j a
f Rec g as
Prod [] g as
xs Rec h as
Prod [] h as
ys
htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod NonEmpty g as
-> m (Prod NonEmpty h (Fmap ff as))
htraverse ff :: Sing ff
ff f :: forall (a :: a0). g a -> m (h (ff @@ a))
f (x :&| xs) =
h (Apply ff a)
-> Rec h (Fmap_6989586621680022960 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
(:&|) (h (Apply ff a)
-> Rec h (Fmap_6989586621680022960 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as))
-> m (h (Apply ff a))
-> m (Rec h (Fmap_6989586621680022960 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a0). g a -> m (h (ff @@ a))
f g a
x m (Rec h (Fmap_6989586621680022960 ff as)
-> NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as))
-> m (Rec h (Fmap_6989586621680022960 ff as))
-> m (NERec h (Apply ff a ':| Fmap_6989586621680022960 ff as))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod [] g as
-> m (Prod [] h (Fmap ff as))
forall (f :: * -> *) a0 k (m :: * -> *) (ff :: a0 ~> k)
(g :: a0 -> *) (h :: k -> *) (as :: f a0).
(FProd f, Applicative m) =>
Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod f g as
-> m (Prod f h (Fmap ff as))
htraverse Sing ff
ff forall (a :: a0). g a -> m (h (ff @@ a))
f Rec g as
Prod [] g as
xs
ixProd :: Elem NonEmpty as a -> Lens' (Prod NonEmpty g as) (g a)
ixProd = \case
NEHead -> \f :: g a -> f (g a)
f -> \case
x :&| xs -> (g a -> Rec g as -> NERec g (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| Rec g as
xs) (g a -> NERec g (a ':| as)) -> f (g a) -> f (NERec g (a ':| as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g a
x
NETail i -> \f :: g a -> f (g a)
f -> \case
x :&| xs -> (g a
x g a -> Rec g as -> NERec g (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&|) (Rec g as -> NERec g (a ':| as))
-> f (Rec g as) -> f (NERec g (a ':| as))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elem [] as a
-> (g a -> f (g a)) -> Prod [] g as -> f (Prod [] g as)
forall (f :: * -> *) k (as :: f k) (a :: k) (g :: k -> *).
FProd f =>
Elem f as a -> Lens' (Prod f g as) (g a)
ixProd Index as a
Elem [] as a
i g a -> f (g a)
f Rec g as
Prod [] g as
xs
toRec :: Prod NonEmpty g as -> Rec g (ToList as)
toRec (x :&| xs) = g a
x g a -> Rec g as -> Rec g (a : as)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g as
xs
withPureProd :: Prod NonEmpty g as -> (PureProd NonEmpty as => r) -> r
withPureProd (x :&| xs) = g a
-> Rec g as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
forall k (f :: k -> *) (a :: k) (as :: [k]) r.
f a
-> Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
withPureProdNE g a
x Rec g as
xs
withPureProdNE
:: f a
-> Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
withPureProdNE :: f a
-> Rec f as
-> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r)
-> r
withPureProdNE _ xs :: Rec f as
xs = Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
forall k (f :: k -> *) (as :: [k]) r.
Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r
withPureProdList Rec f as
xs
instance RecApplicative as => PureProd NonEmpty (a ':| as) where
pureProd :: (forall (a :: k). g a) -> Prod NonEmpty g (a ':| as)
pureProd x :: forall (a :: k). g a
x = g a
forall (a :: k). g a
x g a -> Rec g as -> NERec g (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| (forall (a :: k). g a) -> Prod [] g as
forall k (f :: * -> *) (as :: f k) (g :: k -> *).
PureProd f as =>
(forall (a :: k). g a) -> Prod f g as
pureProd forall (a :: k). g a
x
instance (c a, RPureConstrained c as) => PureProdC NonEmpty c (a ':| as) where
pureProdC :: (forall (a :: a). c a => g a) -> Prod NonEmpty g (a ':| as)
pureProdC x :: forall (a :: a). c a => g a
x = g a
forall (a :: a). c a => g a
x g a -> Rec g as -> NERec g (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| (forall (a :: a). c a => g a) -> Prod [] g as
forall k (f :: * -> *) (c :: k -> Constraint) (as :: f k)
(g :: k -> *).
PureProdC f c as =>
(forall (a :: k). c a => g a) -> Prod f g as
pureProdC @_ @c forall (a :: a). c a => g a
x
instance (c (g a), ReifyConstraint c g as) => ReifyConstraintProd NonEmpty c g (a ':| as) where
reifyConstraintProd :: Prod NonEmpty g (a ':| as)
-> Prod NonEmpty (Dict c :. g) (a ':| as)
reifyConstraintProd (x :&| xs) = Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)
Compose (Dict c) g a
-> Rec (Dict c :. g) as -> NERec (Dict c :. g) (a ':| as)
forall a (f :: a -> *) (a :: a) (as :: [a]).
f a -> Rec f as -> NERec f (a ':| as)
:&| Prod [] g as -> Prod [] (Dict c :. g) as
forall k (f :: * -> *) (c :: * -> Constraint) (g :: k -> *)
(as :: f k).
ReifyConstraintProd f c g as =>
Prod f g as -> Prod f (Dict c :. g) as
reifyConstraintProd @_ @c Rec g as
Prod [] g as
xs
sameIndexVal
:: Index as a
-> Index as b
-> Maybe (a :~: b)
sameIndexVal :: Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal = \case
IZ -> \case
IZ -> (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
IS _ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
IS i :: Index bs a
i -> \case
IZ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
IS j :: Index bs b
j -> Index bs a -> Index bs b -> Maybe (a :~: b)
forall k (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal Index bs a
i Index bs b
Index bs b
j Maybe (a :~: b) -> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case Refl -> a :~: b
forall k (a :: k). a :~: a
Refl
sameNEIndexVal
:: NEIndex as a
-> NEIndex as b
-> Maybe (a :~: b)
sameNEIndexVal :: NEIndex as a -> NEIndex as b -> Maybe (a :~: b)
sameNEIndexVal = \case
NEHead -> \case
NEHead -> (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
NETail _ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
NETail i :: Index as a
i -> \case
NEHead -> Maybe (a :~: b)
forall a. Maybe a
Nothing
NETail j :: Index as b
j -> Index as a -> Index as b -> Maybe (a :~: b)
forall k (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal Index as a
i Index as b
Index as b
j Maybe (a :~: b) -> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case Refl -> a :~: b
forall k (a :: k). a :~: a
Refl
data ISnd :: (j, k) -> k -> Type where
ISnd :: ISnd '(a, b) b
deriving instance Show (ISnd as a)
deriving instance Read (ISnd '(a, b) b)
deriving instance Eq (ISnd as a)
deriving instance Ord (ISnd as a)
data SISnd as a :: ISnd as a -> Type where
SISnd :: SISnd '(a, b) b 'ISnd
deriving instance Show (SISnd as a i)
type instance Sing = SISnd as a :: ISnd as a -> Type
instance SingI 'ISnd where
sing :: Sing 'ISnd
sing = Sing 'ISnd
forall j k (a :: j) (b :: k). SISnd '(a, b) b 'ISnd
SISnd
instance SingKind (ISnd as a) where
type Demote (ISnd as a) = ISnd as a
fromSing :: Sing a -> Demote (ISnd as a)
fromSing SISnd = Demote (ISnd as a)
forall j k (a :: j) (b :: k). ISnd '(a, b) b
ISnd
toSing :: Demote (ISnd as a) -> SomeSing (ISnd as a)
toSing ISnd = Sing 'ISnd -> SomeSing (ISnd as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'ISnd
forall j k (a :: j) (b :: k). SISnd '(a, b) b 'ISnd
SISnd
instance SDecide (ISnd as a) where
SISnd %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ SISnd = (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
data PTup :: (k -> Type) -> (j, k) -> Type where
PTup :: Sing w -> f a -> PTup f '(w, a)
deriving instance (Show (Sing w), Show (f a)) => Show (PTup f '(w, a))
deriving instance (Read (Sing w), Read (f a)) => Read (PTup f '(w, a))
deriving instance (Eq (Sing w), Eq (f a)) => Eq (PTup f '(w, a))
deriving instance (Ord (Sing w), Ord (f a)) => Ord (PTup f '(w, a))
instance FProd ((,) j) where
type instance Elem ((,) j) = ISnd
type instance Prod ((,) j) = PTup
singProd :: Sing as -> Prod ((,) j) Sing as
singProd (STuple2 w x) = Sing n1 -> Sing n2 -> PTup Sing '(n1, n2)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing n1
w Sing n2
x
prodSing :: Prod ((,) j) Sing as -> Sing as
prodSing (PTup w x) = Sing w -> Sing a -> STuple2 '(w, a)
forall a0 b0 (n1 :: a0) (n2 :: b0).
Sing n1 -> Sing n2 -> STuple2 '(n1, n2)
STuple2 Sing w
w Sing a
x
withIndices :: Prod ((,) j) g as -> Prod ((,) j) (Elem ((,) j) as :*: g) as
withIndices (PTup w x) = Sing w
-> (:*:) (ISnd '(w, a)) g a -> PTup (ISnd '(w, a) :*: g) '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
w (ISnd '(w, a) a
forall j k (a :: j) (b :: k). ISnd '(a, b) b
ISnd ISnd '(w, a) a -> g a -> (:*:) (ISnd '(w, a)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod ((,) j) g as -> m (Prod ((,) j) h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f (PTup w x) = Sing w -> h a -> PTup h '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
w (h a -> PTup h '(w, a)) -> m (h a) -> m (PTup h '(w, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x
zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod ((,) j) g as -> Prod ((,) j) h as -> Prod ((,) j) j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f (PTup w x) (PTup _ y) = Sing w -> j a -> PTup j '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
w (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y)
htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod ((,) j) g as
-> m (Prod ((,) j) h (Fmap ff as))
htraverse _ f :: forall (a :: a0). g a -> m (h (ff @@ a))
f (PTup w x) = Sing w -> h (Apply ff a) -> PTup h '(w, Apply ff a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
w (h (Apply ff a) -> PTup h '(w, Apply ff a))
-> m (h (Apply ff a)) -> m (PTup h '(w, Apply ff a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a0). g a -> m (h (ff @@ a))
f g a
x
ixProd :: Elem ((,) j) as a -> Lens' (Prod ((,) j) g as) (g a)
ixProd ISnd f :: g a -> f (g a)
f (PTup w x) = Sing a -> g a -> PTup g '(a, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing a
Sing w
w (g a -> PTup g '(a, a)) -> f (g a) -> f (PTup g '(a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g a
x
toRec :: Prod ((,) j) g as -> Rec g (ToList as)
toRec (PTup _ x) = g a
x g a -> Rec g '[] -> Rec g '[a]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
forall u (a :: u -> *). Rec a '[]
RNil
withPureProd :: Prod ((,) j) g as -> (PureProd ((,) j) as => r) -> r
withPureProd (PTup Sing _) x :: PureProd ((,) j) as => r
x = r
PureProd ((,) j) as => r
x
instance SingI w => PureProd ((,) j) '(w, a) where
pureProd :: (forall (a :: k). g a) -> Prod ((,) j) g '(w, a)
pureProd x :: forall (a :: k). g a
x = Sing w -> g a -> PTup g '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
forall k (a :: k). SingI a => Sing a
sing g a
forall (a :: k). g a
x
instance (SingI w, c a) => PureProdC ((,) j) c '(w, a) where
pureProdC :: (forall (a :: k). c a => g a) -> Prod ((,) j) g '(w, a)
pureProdC x :: forall (a :: k). c a => g a
x = Sing w -> g a -> PTup g '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
forall k (a :: k). SingI a => Sing a
sing g a
forall (a :: k). c a => g a
x
instance c (g a) => ReifyConstraintProd ((,) j) c g '(w, a) where
reifyConstraintProd :: Prod ((,) j) g '(w, a) -> Prod ((,) j) (Dict c :. g) '(w, a)
reifyConstraintProd (PTup w x) = Sing w -> Compose (Dict c) g a -> PTup (Dict c :. g) '(w, a)
forall j k (w :: j) (f :: k -> *) (a :: k).
Sing w -> f a -> PTup f '(w, a)
PTup Sing w
Sing w
w (Compose (Dict c) g a -> Prod ((,) j) (Dict c :. g) '(w, a))
-> Compose (Dict c) g a -> Prod ((,) j) (Dict c :. g) '(w, a)
forall a b. (a -> b) -> a -> b
$ Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)
data IIdentity :: Identity k -> k -> Type where
IId :: IIdentity ('Identity x) x
deriving instance Show (IIdentity as a)
deriving instance Read (IIdentity ('Identity a) a)
deriving instance Eq (IIdentity as a)
deriving instance Ord (IIdentity as a)
data SIIdentity as a :: IIdentity as a -> Type where
SIId :: SIIdentity ('Identity a) a 'IId
deriving instance Show (SIIdentity as a i)
type instance Sing = SIIdentity as a :: IIdentity as a -> Type
instance SingI 'IId where
sing :: Sing 'IId
sing = Sing 'IId
forall k (a :: k). SIIdentity ('Identity a) a 'IId
SIId
instance SingKind (IIdentity as a) where
type Demote (IIdentity as a) = IIdentity as a
fromSing :: Sing a -> Demote (IIdentity as a)
fromSing SIId = Demote (IIdentity as a)
forall k (x :: k). IIdentity ('Identity x) x
IId
toSing :: Demote (IIdentity as a) -> SomeSing (IIdentity as a)
toSing IId = Sing 'IId -> SomeSing (IIdentity as a)
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'IId
forall k (a :: k). SIIdentity ('Identity a) a 'IId
SIId
instance SDecide (IIdentity as a) where
SIId %~ :: Sing a -> Sing b -> Decision (a :~: b)
%~ SIId = (a :~: a) -> Decision (a :~: a)
forall a. a -> Decision a
Proved a :~: a
forall k (a :: k). a :~: a
Refl
data PIdentity :: (k -> Type) -> Identity k -> Type where
PIdentity :: f a -> PIdentity f ('Identity a)
deriving instance Show (f a) => Show (PIdentity f ('Identity a))
deriving instance Read (f a) => Read (PIdentity f ('Identity a))
deriving instance Eq (f a) => Eq (PIdentity f ('Identity a))
deriving instance Ord (f a) => Ord (PIdentity f ('Identity a))
instance FProd Identity where
type Elem Identity = IIdentity
type Prod Identity = PIdentity
singProd :: Sing as -> Prod Identity Sing as
singProd (SIdentity x) = Sing n -> PIdentity Sing ('Identity n)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity Sing n
x
prodSing :: Prod Identity Sing as -> Sing as
prodSing (PIdentity x) = Sing a -> SIdentity ('Identity a)
forall a0 (n :: a0). Sing n -> SIdentity ('Identity n)
SIdentity Sing a
x
withIndices :: Prod Identity g as -> Prod Identity (Elem Identity as :*: g) as
withIndices (PIdentity x) = (:*:) (IIdentity ('Identity a)) g a
-> PIdentity (IIdentity ('Identity a) :*: g) ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (IIdentity ('Identity a) a
forall k (x :: k). IIdentity ('Identity x) x
IId IIdentity ('Identity a) a
-> g a -> (:*:) (IIdentity ('Identity a)) g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
x)
traverseProd :: (forall (a :: k). g a -> m (h a))
-> Prod Identity g as -> m (Prod Identity h as)
traverseProd f :: forall (a :: k). g a -> m (h a)
f (PIdentity x) = h a -> PIdentity h ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (h a -> PIdentity h ('Identity a))
-> m (h a) -> m (PIdentity h ('Identity a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h a)
forall (a :: k). g a -> m (h a)
f g a
x
zipWithProd :: (forall (a :: k). g a -> h a -> j a)
-> Prod Identity g as -> Prod Identity h as -> Prod Identity j as
zipWithProd f :: forall (a :: k). g a -> h a -> j a
f (PIdentity x) (PIdentity y) = j a -> PIdentity j ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (g a -> h a -> j a
forall (a :: k). g a -> h a -> j a
f g a
x h a
h a
y)
htraverse :: Sing ff
-> (forall (a :: a0). g a -> m (h (ff @@ a)))
-> Prod Identity g as
-> m (Prod Identity h (Fmap ff as))
htraverse _ f :: forall (a :: a0). g a -> m (h (ff @@ a))
f (PIdentity x) = h (Apply ff a) -> PIdentity h ('Identity (Apply ff a))
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (h (Apply ff a) -> PIdentity h ('Identity (Apply ff a)))
-> m (h (Apply ff a)) -> m (PIdentity h ('Identity (Apply ff a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> m (h (Apply ff a))
forall (a :: a0). g a -> m (h (ff @@ a))
f g a
x
ixProd :: Elem Identity as a -> Lens' (Prod Identity g as) (g a)
ixProd IId f :: g a -> f (g a)
f (PIdentity x) = g a -> PIdentity g ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (g a -> PIdentity g ('Identity a))
-> f (g a) -> f (PIdentity g ('Identity a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a -> f (g a)
f g a
g a
x
toRec :: Prod Identity g as -> Rec g (ToList as)
toRec (PIdentity x) = g a
x g a -> Rec g '[] -> Rec g '[a]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec g '[]
forall u (a :: u -> *). Rec a '[]
RNil
withPureProd :: Prod Identity g as -> (PureProd Identity as => r) -> r
withPureProd (PIdentity _) x :: PureProd Identity as => r
x = r
PureProd Identity as => r
x
instance PureProd Identity ('Identity a) where
pureProd :: (forall (a :: k). g a) -> Prod Identity g ('Identity a)
pureProd x :: forall (a :: k). g a
x = g a -> PIdentity g ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity g a
forall (a :: k). g a
x
instance c a => PureProdC Identity c ('Identity a) where
pureProdC :: (forall (a :: a). c a => g a) -> Prod Identity g ('Identity a)
pureProdC x :: forall (a :: a). c a => g a
x = g a -> PIdentity g ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity g a
forall (a :: a). c a => g a
x
instance c (g a) => ReifyConstraintProd Identity c g ('Identity a) where
reifyConstraintProd :: Prod Identity g ('Identity a)
-> Prod Identity (Dict c :. g) ('Identity a)
reifyConstraintProd (PIdentity x) = Compose (Dict c) g a -> Prod Identity (Dict c :. g) ('Identity a)
forall a (f :: a -> *) (a :: a). f a -> PIdentity f ('Identity a)
PIdentity (Compose (Dict c) g a -> Prod Identity (Dict c :. g) ('Identity a))
-> Compose (Dict c) g a
-> Prod Identity (Dict c :. g) ('Identity a)
forall a b. (a -> b) -> a -> b
$ Dict c (g a) -> Compose (Dict c) g a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (g a -> Dict c (g a)
forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict g a
x)
rElemIndex
:: forall r rs i. (RElem r rs i, PureProd [] rs)
=> Index rs r
rElemIndex :: Index rs r
rElemIndex = Rec (Index rs) rs -> Index rs r
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
(rs :: [k]) (rs' :: [k]) (i :: Nat) (f :: k -> *).
(RecElem record r r' rs rs' i, RecElemFCtx record f, r ~ r') =>
record f rs -> f r
rgetC Rec (Index rs) rs
forall k (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices
toCoRec
:: forall as a f. (RecApplicative as, FoldRec as as)
=> Index as a
-> f a
-> CoRec f as
toCoRec :: Index as a -> f a -> CoRec f as
toCoRec = \case
IZ -> f a -> CoRec f as
forall k (a1 :: k) (b :: [k]) (a :: k -> *).
RElem a1 b (RIndex a1 b) =>
a a1 -> CoRec a b
CoRec
IS i :: Index bs a
i -> \x :: f a
x -> Maybe (CoRec f as) -> CoRec f as
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (CoRec f as) -> CoRec f as)
-> (Rec (Maybe :. f) as -> Maybe (CoRec f as))
-> Rec (Maybe :. f) as
-> CoRec f as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Maybe :. f) as -> Maybe (CoRec f as)
forall k (ts :: [k]) (f :: k -> *).
FoldRec ts ts =>
Rec (Maybe :. f) ts -> Maybe (CoRec f ts)
firstField (Rec (Maybe :. f) as -> CoRec f as)
-> Rec (Maybe :. f) as -> CoRec f as
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Index (b : bs) a -> (:.) Maybe f a)
-> Prod [] (Index (b : bs)) (b : bs)
-> Prod [] (Maybe :. f) (b : bs)
forall k (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (Index bs a -> f a -> Index (b : bs) a -> Compose Maybe f a
forall (bs :: [k]) (b :: k) (c :: k).
Index bs a -> f a -> Index (b : bs) c -> Compose Maybe f c
go Index bs a
i f a
x) Prod [] (Index (b : bs)) (b : bs)
forall k (f :: * -> *) (as :: f k).
(FProd f, PureProd f as) =>
Prod f (Elem f as) as
indices
where
go :: Index bs a -> f a -> Index (b ': bs) c -> V.Compose Maybe f c
go :: Index bs a -> f a -> Index (b : bs) c -> Compose Maybe f c
go i :: Index bs a
i x :: f a
x j :: Index (b : bs) c
j = case Index (b : bs) a -> Index (b : bs) c -> Maybe (a :~: c)
forall k (as :: [k]) (a :: k) (b :: k).
Index as a -> Index as b -> Maybe (a :~: b)
sameIndexVal (Index bs a -> Index (b : bs) a
forall k (bs :: [k]) (a :: k) (b :: k).
Index bs a -> Index (b : bs) a
IS Index bs a
i) Index (b : bs) c
j of
Just Refl -> Maybe (f a) -> Compose Maybe f a
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose (f a -> Maybe (f a)
forall a. a -> Maybe a
Just f a
x)
Nothing -> Maybe (f c) -> Compose Maybe f c
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
V.Compose Maybe (f c)
forall a. Maybe a
Nothing
indexRElem
:: (SDecide k, SingI (a :: k), RecApplicative as, FoldRec as as)
=> Index as a
-> (RElem a as (V.RIndex a as) => r)
-> r
indexRElem :: Index as a -> (RElem a as (RIndex a as) => r) -> r
indexRElem i :: Index as a
i = case Index as a -> Sing a -> CoRec Sing as
forall k (as :: [k]) (a :: k) (f :: k -> *).
(RecApplicative as, FoldRec as as) =>
Index as a -> f a -> CoRec f as
toCoRec Index as a
i Sing a
x of
CoRec y :: Sing a1
y -> case Sing a
x Sing a -> Sing a1 -> Decision (a :~: a1)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a1
y of
Proved Refl -> (RElem a as (RIndex a as) => r) -> r
forall a. a -> a
id
Disproved _ -> String -> (RElem a as (RIndex a as) => r) -> r
forall a. String -> a
errorWithoutStackTrace "why :|"
where
x :: Sing a
x = Sing a
forall k (a :: k). SingI a => Sing a
sing