{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Universe (
Elem,
In,
Universe (..),
singAll,
Index (..),
IJust (..),
IRight (..),
NEIndex (..),
ISnd (..),
IIdentity (..),
All,
WitAll (..),
NotAll,
Any,
WitAny (..),
None,
Null,
NotNull,
IsJust,
IsNothing,
IsRight,
IsLeft,
decideAny,
decideAll,
genAll,
igenAll,
splitSing,
pickElem,
) where
import Data.Either.Singletons hiding (IsLeft, IsRight)
import Data.Functor.Identity
import Data.Functor.Identity.Singletons
import Data.Kind
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty.Singletons as NE
import Data.List.Singletons hiding (
All,
Any,
Elem,
ElemSym0,
ElemSym1,
ElemSym2,
Null,
)
import Data.Maybe.Singletons hiding (IsJust, IsNothing)
import Data.Singletons
import Data.Singletons.Decide
import Data.Tuple.Singletons
import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import GHC.Generics ((:*:) (..))
import Prelude hiding (all, any)
data WitAny f :: (k ~> Type) -> f k -> Type where
WitAny :: Elem f as a -> p @@ a -> WitAny f p as
data Any f :: Predicate k -> Predicate (f k)
type instance Apply (Any f p) as = WitAny f p as
newtype WitAll f p (as :: f k) = WitAll {forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll :: forall a. Elem f as a -> p @@ a}
data All f :: Predicate k -> Predicate (f k)
type instance Apply (All f p) as = WitAll f p as
instance (Universe f, Decidable p) => Decidable (Any f p) where
decide :: Decide (Any f p)
decide = forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (Any f p)
decideAny @f @_ @p (Decide p -> Decide (Any f p)) -> Decide p -> Decide (Any f p)
forall a b. (a -> b) -> a -> b
$ forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @p
instance (Universe f, Decidable p) => Decidable (All f p) where
decide :: Decide (All f p)
decide = forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (All f p)
decideAll @f @_ @p (Decide p -> Decide (All f p)) -> Decide p -> Decide (All f p)
forall a b. (a -> b) -> a -> b
$ forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @p
instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p)
instance Provable p => Provable (NotNull f ==> Any f p) where
prove :: Prove (NotNull f ==> Any f p)
prove Sing a
_ (WitAny Elem f a a
i Evident @@ a
s) = Elem f a a -> (p @@ a) -> WitAny f p a
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i (forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k ~> *). Provable p => Prove p
prove @p Sing a
Evident @@ a
s)
instance (Universe f, Provable p) => Provable (All f p) where
prove :: Prove (All f p)
prove Sing a
xs = (forall (a :: k). Elem f a a -> p @@ a) -> WitAll f p a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem f a a -> p @@ a) -> WitAll f p a)
-> (forall (a :: k). Elem f a a -> p @@ a) -> WitAll f p a
forall a b. (a -> b) -> a -> b
$ \Elem f a a
i -> forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k ~> *). Provable p => Prove p
prove @p (Elem f a a -> Sing a -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs)
instance Universe f => TFunctor (Any f) where
tmap :: forall (p :: k1 ~> *) (q :: k1 ~> *).
(p --> q) -> Any f p --> Any f q
tmap p --> q
f Sing a
xs (WitAny Elem f a a
i p @@ a
x) = Elem f a a -> (q @@ a) -> WitAny f q a
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i (Sing a -> (p @@ a) -> q @@ a
p --> q
f (Elem f a a -> Sing a -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs) p @@ a
x)
instance Universe f => TFunctor (All f) where
tmap :: forall (p :: k1 ~> *) (q :: k1 ~> *).
(p --> q) -> All f p --> All f q
tmap p --> q
f Sing a
xs All f p @@ a
a = (forall (a :: k1). Elem f a a -> q @@ a) -> WitAll f q a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k1). Elem f a a -> q @@ a) -> WitAll f q a)
-> (forall (a :: k1). Elem f a a -> q @@ a) -> WitAll f q a
forall a b. (a -> b) -> a -> b
$ \Elem f a a
i -> Sing a -> (p @@ a) -> q @@ a
p --> q
f (Elem f a a -> Sing a -> Sing a
forall {k} (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f a a
i Sing a
xs) (WitAll f p a -> forall (a :: k1). Elem f a a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ a
WitAll f p a
a Elem f a a
i)
instance Universe f => DFunctor (All f) where
dmap :: forall (p :: k1 ~> *) (q :: k1 ~> *).
(p -?> q) -> All f p -?> All f q
dmap p -?> q
f Sing a
xs All f p @@ a
a = (forall (a :: k1). Elem f a a -> Sing a -> Decision (q @@ a))
-> Sing a -> Decision (Apply (All f q) a)
forall k (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll (\Elem f a a
i Sing a
x -> Sing a -> (p @@ a) -> Decision (q @@ a)
p -?> q
f Sing a
x (WitAll f p a -> forall (a :: k1). Elem f a a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ a
WitAll f p a
a Elem f a a
i)) Sing a
xs
class FProd f => Universe (f :: Type -> Type) where
idecideAny ::
forall k (p :: k ~> Type) (as :: f k).
() =>
(forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->
(Sing as -> Decision (Any f p @@ as))
idecideAll ::
forall k (p :: k ~> Type) (as :: f k).
() =>
(forall a. Elem f as a -> Sing a -> Decision (p @@ a)) ->
(Sing as -> Decision (All f p @@ as))
allProd ::
forall p g.
() =>
(forall a. Sing a -> p @@ a -> g a) ->
All f p --> TyPred (Prod f g)
prodAll ::
forall p g as.
() =>
(forall a. g a -> p @@ a) ->
Prod f g as ->
All f p @@ as
type Null f = (None f Evident :: Predicate (f k))
type NotNull f = (Any f Evident :: Predicate (f k))
type None f p = (Not (Any f p) :: Predicate (f k))
type NotAll f p = (Not (All f p) :: Predicate (f k))
decideAny ::
forall f k (p :: k ~> Type).
Universe f =>
Decide p ->
Decide (Any f p)
decideAny :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (Any f p)
decideAny Decide p
f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (Any f p) a)
forall k (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
idecideAny ((Sing a -> Decision (Apply p a))
-> Elem f a a -> Sing a -> Decision (Apply p a)
forall a b. a -> b -> a
const Sing a -> Decision (Apply p a)
Decide p
f)
decideAll ::
forall f k (p :: k ~> Type).
Universe f =>
Decide p ->
Decide (All f p)
decideAll :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Decide p -> Decide (All f p)
decideAll Decide p
f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (All f p) a)
forall k (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll ((Sing a -> Decision (Apply p a))
-> Elem f a a -> Sing a -> Decision (Apply p a)
forall a b. a -> b -> a
const Sing a -> Decision (Apply p a)
Decide p
f)
splitSing ::
forall f k (as :: f k).
Universe f =>
Sing as ->
All f (TyPred Sing) @@ as
splitSing :: forall (f :: * -> *) k (as :: f k).
Universe f =>
Sing as -> All f (TyPred Sing) @@ as
splitSing = (forall (a :: k). Sing a -> TyCon Sing @@ a)
-> Prod f Sing as -> Apply (All f (TyCon Sing)) as
forall {k} (p :: Predicate k) (g :: k -> *) (as :: f k).
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
forall (f :: * -> *) {k} (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll Sing a -> Sing a
Sing a -> Apply (TyCon Sing) a
forall (a :: k). Sing a -> TyCon Sing @@ a
forall a. a -> a
id (Prod f Sing as -> WitAll f (TyCon Sing) as)
-> (Sing as -> Prod f Sing as)
-> Sing as
-> WitAll f (TyCon Sing) as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall {k} (as :: f k). Sing as -> Prod f Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
pickElem ::
forall f k (as :: f k) a.
(Universe f, SingI as, SingI a, SDecide k) =>
Decision (Elem f as a)
pickElem :: forall (f :: * -> *) k (as :: f k) (a :: k).
(Universe f, SingI as, SingI a, SDecide k) =>
Decision (Elem f as a)
pickElem =
(WitAny f (TyPred ((:~:) a)) as -> Elem f as a)
-> (Elem f as a -> WitAny f (TyPred ((:~:) a)) as)
-> Decision (WitAny f (TyPred ((:~:) a)) as)
-> Decision (Elem f as a)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision
(\case WitAny Elem f as a
i a :~: a
TyPred ((:~:) a) @@ a
Refl -> Elem f as a
Elem f as a
i)
(\case Elem f as a
i -> Elem f as a
-> (TyPred ((:~:) a) @@ a) -> WitAny f (TyPred ((:~:) a)) as
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f as a
i a :~: a
TyPred ((:~:) a) @@ a
forall {k} (a :: k). a :~: a
Refl)
(Decision (WitAny f (TyPred ((:~:) a)) as)
-> Decision (Elem f as a))
-> (Sing as -> Decision (WitAny f (TyPred ((:~:) a)) as))
-> Sing as
-> Decision (Elem f as a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: f k ~> *). Decidable p => Decide p
decide @(Any f (TyPred ((:~:) a)))
(Sing as -> Decision (Elem f as a))
-> Sing as -> Decision (Elem f as a)
forall a b. (a -> b) -> a -> b
$ Sing as
forall {k} (a :: k). SingI a => Sing a
sing
igenAll ::
forall f k (p :: k ~> Type) (as :: f k).
Universe f =>
(forall a. Elem f as a -> Sing a -> p @@ a) ->
(Sing as -> All f p @@ as)
igenAll :: forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> p @@ a)
-> Sing as -> All f p @@ as
igenAll forall (a :: k). Elem f as a -> Sing a -> p @@ a
f = (forall (a :: k). (:*:) (Elem f as) Sing a -> p @@ a)
-> Prod f (Elem f as :*: Sing) as -> Apply (All f p) as
forall {k} (p :: Predicate k) (g :: k -> *) (as :: f k).
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
forall (f :: * -> *) {k} (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll (\(Elem f as a
i :*: Sing a
x) -> Elem f as a -> Sing a -> p @@ a
forall (a :: k). Elem f as a -> Sing a -> p @@ a
f Elem f as a
i Sing a
x) (Prod f (Elem f as :*: Sing) as -> WitAll f p as)
-> (Sing as -> Prod f (Elem f as :*: Sing) as)
-> Sing as
-> WitAll f p as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k).
Elem f as a -> Sing a -> (:*:) (Elem f as) Sing a)
-> Prod f Sing as -> Prod f (Elem f as :*: Sing) 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 Elem f as a -> Sing a -> (:*:) (Elem f as) Sing a
forall (a :: k). Elem f as a -> Sing a -> (:*:) (Elem f as) Sing a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (Prod f Sing as -> Prod f (Elem f as :*: Sing) as)
-> (Sing as -> Prod f Sing as)
-> Sing as
-> Prod f (Elem f as :*: Sing) as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall {k} (as :: f k). Sing as -> Prod f Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
genAll ::
forall f k (p :: k ~> Type).
Universe f =>
Prove p ->
Prove (All f p)
genAll :: forall (f :: * -> *) k (p :: k ~> *).
Universe f =>
Prove p -> Prove (All f p)
genAll Prove p
f = Prove p -> Prod f Sing a -> Apply (All f p) a
forall {k} (p :: Predicate k) (g :: k -> *) (as :: f k).
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
forall (f :: * -> *) {k} (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll Sing a -> p @@ a
Prove p
f (Prod f Sing a -> WitAll f p a)
-> (Sing a -> Prod f Sing a) -> Sing a -> WitAll f p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod f Sing a
forall {k} (as :: f k). Sing as -> Prod f Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
singAll ::
forall f k (as :: f k).
Universe f =>
Sing as ->
All f Evident @@ as
singAll :: forall (f :: * -> *) k (as :: f k).
Universe f =>
Sing as -> All f Evident @@ as
singAll = (forall (a :: k). Sing a -> Evident @@ a)
-> Prod f Sing as -> Apply (All f Evident) as
forall {k} (p :: Predicate k) (g :: k -> *) (as :: f k).
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
forall (f :: * -> *) {k} (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll Sing a -> Sing a
Sing a -> Apply Evident a
forall (a :: k). Sing a -> Evident @@ a
forall a. a -> a
id (Prod f Sing as -> WitAll f Evident as)
-> (Sing as -> Prod f Sing as) -> Sing as -> WitAll f Evident as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing as -> Prod f Sing as
forall {k} (as :: f k). Sing as -> Prod f Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
type IsJust = (NotNull Maybe :: Predicate (Maybe k))
type IsNothing = (Null Maybe :: Predicate (Maybe k))
type IsRight = (NotNull (Either j) :: Predicate (Either j k))
type IsLeft = (Null (Either j) :: Predicate (Either j k))
instance Universe [] where
idecideAny ::
forall k (p :: k ~> Type) (as :: [k]).
() =>
(forall a. Elem [] as a -> Sing a -> Decision (p @@ a)) ->
Sing as ->
Decision (Any [] p @@ as)
idecideAny :: forall k (p :: k ~> *) (as :: [k]).
(forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any [] p @@ as)
idecideAny forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f = \case
Sing as
SList as
SNil -> Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as))
-> Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny Elem [] '[] a
i p @@ a
_ -> case Elem [] '[] a
i of {}
Sing n1
x `SCons` Sing n2
xs -> case Elem [] as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f Index (n1 : n2) n1
Elem [] as n1
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ Sing n1
x of
Proved p @@ n1
p -> (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a. a -> Decision a
Proved ((Any [] p @@ as) -> Decision (Any [] p @@ as))
-> (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem [] (n1 : n2) n1 -> (p @@ n1) -> WitAny [] p (n1 : n2)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Index (n1 : n2) n1
Elem [] (n1 : n2) n1
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ p @@ n1
p
Disproved Refuted (p @@ n1)
v -> case forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
idecideAny @[] @_ @p (Index (n1 : n2) a -> Sing a -> Decision (Apply p a)
Elem [] as a -> Sing a -> Decision (Apply p a)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f (Index (n1 : n2) a -> Sing a -> Decision (Apply p a))
-> (Index n2 a -> Index (n1 : n2) a)
-> Index n2 a
-> Sing a
-> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> Index (n1 : n2) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS) Sing n2
xs of
Proved (WitAny Elem [] n2 a
i p @@ a
p) -> (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a. a -> Decision a
Proved ((Any [] p @@ as) -> Decision (Any [] p @@ as))
-> (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem [] (n1 : n2) a -> (p @@ a) -> WitAny [] p (n1 : n2)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny (Index n2 a -> Index (n1 : n2) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS Index n2 a
Elem [] n2 a
i) p @@ a
p
Disproved Refuted (Any [] p @@ n2)
vs -> Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as))
-> Refuted (Any [] p @@ as) -> Decision (Any [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny Index (n1 : n2) a
Elem [] (n1 : n2) a
IZ p @@ a
p -> Refuted (p @@ n1)
v p @@ n1
p @@ a
p
WitAny (IS Index bs a
i) p @@ a
p -> Refuted (Any [] p @@ n2)
vs (Elem [] n2 a -> (p @@ a) -> WitAny [] p n2
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Index bs a
Elem [] n2 a
i p @@ a
p)
idecideAll ::
forall k (p :: k ~> Type) (as :: [k]).
() =>
(forall a. Elem [] as a -> Sing a -> Decision (p @@ a)) ->
Sing as ->
Decision (All [] p @@ as)
idecideAll :: forall k (p :: k ~> *) (as :: [k]).
(forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All [] p @@ as)
idecideAll forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f = \case
Sing as
SList as
SNil -> (All [] p @@ as) -> Decision (All [] p @@ as)
forall a. a -> Decision a
Proved ((All [] p @@ as) -> Decision (All [] p @@ as))
-> (All [] p @@ as) -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[]
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[])
-> (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[]
forall a b. (a -> b) -> a -> b
$ \case {}
Sing n1
x `SCons` Sing n2
xs -> case Elem [] as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f Index (n1 : n2) n1
Elem [] as n1
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ Sing n1
x of
Proved p @@ n1
p -> case forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll @[] @_ @p (Index (n1 : n2) a -> Sing a -> Decision (Apply p a)
Elem [] as a -> Sing a -> Decision (Apply p a)
forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)
f (Index (n1 : n2) a -> Sing a -> Decision (Apply p a))
-> (Index n2 a -> Index (n1 : n2) a)
-> Index n2 a
-> Sing a
-> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> Index (n1 : n2) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS) Sing n2
xs of
Proved All [] p @@ n2
a -> (All [] p @@ as) -> Decision (All [] p @@ as)
forall a. a -> Decision a
Proved ((All [] p @@ as) -> Decision (All [] p @@ as))
-> (All [] p @@ as) -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem [] (n1 : n2) a -> p @@ a)
-> WitAll [] p (n1 : n2)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem [] (n1 : n2) a -> p @@ a)
-> WitAll [] p (n1 : n2))
-> (forall (a :: k). Elem [] (n1 : n2) a -> p @@ a)
-> WitAll [] p (n1 : n2)
forall a b. (a -> b) -> a -> b
$ \case
Index (n1 : n2) a
Elem [] (n1 : n2) a
IZ -> p @@ n1
p @@ a
p
IS Index bs a
i -> WitAll [] p n2 -> forall (a :: k). Elem [] n2 a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ n2
WitAll [] p n2
a Index bs a
Elem [] n2 a
i
Disproved Refuted (All [] p @@ n2)
v -> Refuted (All [] p @@ as) -> Decision (All [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All [] p @@ as) -> Decision (All [] p @@ as))
-> Refuted (All [] p @@ as) -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \All [] p @@ as
a -> Refuted (All [] p @@ n2)
v Refuted (All [] p @@ n2) -> Refuted (All [] p @@ n2)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (WitAll [] p (n1 : n2)
-> forall (a :: k). Elem [] (n1 : n2) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ as
WitAll [] p (n1 : n2)
a (Index (n1 : n2) a -> Apply p a)
-> (Index n2 a -> Index (n1 : n2) a) -> Index n2 a -> Apply p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> Index (n1 : n2) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS)
Disproved Refuted (p @@ n1)
v -> Refuted (All [] p @@ as) -> Decision (All [] p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All [] p @@ as) -> Decision (All [] p @@ as))
-> Refuted (All [] p @@ as) -> Decision (All [] p @@ as)
forall a b. (a -> b) -> a -> b
$ \All [] p @@ as
a -> Refuted (p @@ n1)
v Refuted (p @@ n1) -> Refuted (p @@ n1)
forall a b. (a -> b) -> a -> b
$ WitAll [] p (n1 : n2)
-> forall (a :: k). Elem [] (n1 : n2) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ as
WitAll [] p (n1 : n2)
a Index (n1 : n2) n1
Elem [] (n1 : n2) n1
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
allProd ::
forall p g.
() =>
(forall a. Sing a -> p @@ a -> g a) ->
All [] p --> TyPred (Prod [] g)
allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All [] p --> TyPred (Prod [] g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f = Sing a -> Apply (All [] p) a -> Apply (TyCon (Prod [] g)) a
Sing a -> WitAll [] p a -> Prod [] g a
forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as
go
where
go :: Sing as -> WitAll [] p as -> Prod [] g as
go :: forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as
go = \case
Sing as
SList as
SNil -> \WitAll [] p as
_ -> Rec g '[]
Prod [] g as
forall {u} (a :: u -> *). Rec a '[]
RNil
Sing n1
x `SCons` Sing n2
xs -> \WitAll [] p as
a ->
Sing n1 -> (p @@ n1) -> g n1
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n1
x (WitAll [] p as -> forall (a :: k). Elem [] as a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll [] p as
a Index (n1 : n2) n1
Elem [] as n1
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ)
g n1 -> Rec g n2 -> Rec g (n1 : n2)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Sing n2 -> WitAll [] p n2 -> Prod [] g n2
forall (as :: [k]). Sing as -> WitAll [] p as -> Prod [] g as
go Sing n2
xs ((forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (WitAll [] p as -> forall (a :: k). Elem [] as a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll [] p as
a (Index (n1 : n2) a -> Apply p a)
-> (Index n2 a -> Index (n1 : n2) a) -> Index n2 a -> Apply p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> Index (n1 : n2) a
forall {k} (bs :: [k]) (b :: k) (b1 :: k).
Index bs b -> Index (b1 : bs) b
IS))
prodAll ::
forall p g as.
() =>
(forall a. g a -> p @@ a) ->
Prod [] g as ->
All [] p @@ as
prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: [k]).
(forall (a :: k). g a -> p @@ a) -> Prod [] g as -> All [] p @@ as
prodAll forall (a :: k). g a -> p @@ a
f = Prod [] g as -> All [] p @@ as
forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs
go
where
go :: Prod [] g bs -> All [] p @@ bs
go :: forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs
go = \case
Rec g bs
Prod [] g bs
RNil -> (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[]
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[])
-> (forall (a :: k). Elem [] '[] a -> p @@ a) -> WitAll [] p '[]
forall a b. (a -> b) -> a -> b
$ \case {}
g r
x :& Rec g rs
xs -> (forall (a :: k). Elem [] (r : rs) a -> p @@ a)
-> WitAll [] p (r : rs)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem [] (r : rs) a -> p @@ a)
-> WitAll [] p (r : rs))
-> (forall (a :: k). Elem [] (r : rs) a -> p @@ a)
-> WitAll [] p (r : rs)
forall a b. (a -> b) -> a -> b
$ \case
Index (r : rs) a
Elem [] (r : rs) a
IZ -> g r -> p @@ r
forall (a :: k). g a -> p @@ a
f g r
x
IS Index bs a
i -> WitAll [] p rs -> forall (a :: k). Elem [] rs a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll (Prod [] g rs -> All [] p @@ rs
forall (bs :: [k]). Prod [] g bs -> All [] p @@ bs
go Rec g rs
Prod [] g rs
xs) Index bs a
Elem [] rs a
i
instance Universe Maybe where
idecideAny :: forall k (p :: k ~> *) (as :: Maybe k).
(forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any Maybe p @@ as)
idecideAny forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f = \case
Sing as
SMaybe as
SNothing -> Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as))
-> Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ \case WitAny Elem Maybe 'Nothing a
i p @@ a
_ -> case Elem Maybe 'Nothing a
i of {}
SJust Sing n
x -> case Elem Maybe as n -> Sing n -> Decision (p @@ n)
forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f IJust ('Just n) n
Elem Maybe as n
forall {k} (b :: k). IJust ('Just b) b
IJust Sing n
x of
Proved p @@ n
p -> (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a. a -> Decision a
Proved ((Any Maybe p @@ as) -> Decision (Any Maybe p @@ as))
-> (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem Maybe ('Just n) n -> (p @@ n) -> WitAny Maybe p ('Just n)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny IJust ('Just n) n
Elem Maybe ('Just n) n
forall {k} (b :: k). IJust ('Just b) b
IJust p @@ n
p
Disproved Refuted (p @@ n)
v -> Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as))
-> Refuted (Any Maybe p @@ as) -> Decision (Any Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny IJust ('Just n) a
Elem Maybe ('Just n) a
IJust p @@ a
p -> Refuted (p @@ n)
v p @@ n
p @@ a
p
idecideAll :: forall k (p :: k ~> *) (as :: Maybe k).
(forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All Maybe p @@ as)
idecideAll forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f = \case
Sing as
SMaybe as
SNothing -> (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a. a -> Decision a
Proved ((All Maybe p @@ as) -> Decision (All Maybe p @@ as))
-> (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing)
-> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing
forall a b. (a -> b) -> a -> b
$ \case {}
SJust Sing n
x -> case Elem Maybe as n -> Sing n -> Decision (p @@ n)
forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)
f IJust ('Just n) n
Elem Maybe as n
forall {k} (b :: k). IJust ('Just b) b
IJust Sing n
x of
Proved p @@ n
p -> (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a. a -> Decision a
Proved ((All Maybe p @@ as) -> Decision (All Maybe p @@ as))
-> (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem Maybe ('Just n) a -> p @@ a)
-> WitAll Maybe p ('Just n)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Maybe ('Just n) a -> p @@ a)
-> WitAll Maybe p ('Just n))
-> (forall (a :: k). Elem Maybe ('Just n) a -> p @@ a)
-> WitAll Maybe p ('Just n)
forall a b. (a -> b) -> a -> b
$ \case IJust ('Just n) a
Elem Maybe ('Just n) a
IJust -> p @@ n
p @@ a
p
Disproved Refuted (p @@ n)
v -> Refuted (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All Maybe p @@ as) -> Decision (All Maybe p @@ as))
-> Refuted (All Maybe p @@ as) -> Decision (All Maybe p @@ as)
forall a b. (a -> b) -> a -> b
$ \All Maybe p @@ as
a -> Refuted (p @@ n)
v Refuted (p @@ n) -> Refuted (p @@ n)
forall a b. (a -> b) -> a -> b
$ WitAll Maybe p ('Just n)
-> forall (a :: k). Elem Maybe ('Just n) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Maybe p @@ as
WitAll Maybe p ('Just n)
a IJust ('Just n) n
Elem Maybe ('Just n) n
forall {k} (b :: k). IJust ('Just b) b
IJust
allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All Maybe p --> TyPred (Prod Maybe g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f = \case
Sing a
SMaybe a
SNothing -> \All Maybe p @@ a
_ -> PMaybe g 'Nothing
TyPred (Prod Maybe g) @@ a
forall {k} (a :: k -> *). PMaybe a 'Nothing
PNothing
SJust Sing n
x -> \All Maybe p @@ a
a -> g n -> PMaybe g ('Just n)
forall {k} (a :: k -> *) (a1 :: k). a a1 -> PMaybe a ('Just a1)
PJust (Sing n -> (p @@ n) -> g n
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n
x (WitAll Maybe p ('Just n)
-> forall (a :: k). Elem Maybe ('Just n) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Maybe p @@ a
WitAll Maybe p ('Just n)
a IJust ('Just n) n
Elem Maybe ('Just n) n
forall {k} (b :: k). IJust ('Just b) b
IJust))
prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: Maybe k).
(forall (a :: k). g a -> p @@ a)
-> Prod Maybe g as -> All Maybe p @@ as
prodAll forall (a :: k). g a -> p @@ a
f = \case
PMaybe g as
Prod Maybe g as
PNothing -> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing)
-> (forall (a :: k). Elem Maybe 'Nothing a -> p @@ a)
-> WitAll Maybe p 'Nothing
forall a b. (a -> b) -> a -> b
$ \case {}
PJust g a1
x -> (forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a)
-> WitAll Maybe p ('Just a1)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a)
-> WitAll Maybe p ('Just a1))
-> (forall (a :: k). Elem Maybe ('Just a1) a -> p @@ a)
-> WitAll Maybe p ('Just a1)
forall a b. (a -> b) -> a -> b
$ \case IJust ('Just a1) a
Elem Maybe ('Just a1) a
IJust -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x
instance Universe (Either j) where
idecideAny :: forall k (p :: k ~> *) (as :: Either j k).
(forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any (Either j) p @@ as)
idecideAny forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f = \case
SLeft Sing n
_ -> Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as))
-> Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \case WitAny Elem (Either j) ('Left n) a
i p @@ a
_ -> case Elem (Either j) ('Left n) a
i of {}
SRight Sing n
x -> case Elem (Either j) as n -> Sing n -> Decision (p @@ n)
forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f IRight ('Right n) n
Elem (Either j) as n
forall {k} {j} (b :: k). IRight ('Right b) b
IRight Sing n
x of
Proved p @@ n
p -> (Any (Either j) p @@ as) -> Decision (Any (Either j) p @@ as)
forall a. a -> Decision a
Proved ((Any (Either j) p @@ as) -> Decision (Any (Either j) p @@ as))
-> (Any (Either j) p @@ as) -> Decision (Any (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem (Either j) ('Right n) n
-> (p @@ n) -> WitAny (Either j) p ('Right n)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny IRight ('Right n) n
Elem (Either j) ('Right n) n
forall {k} {j} (b :: k). IRight ('Right b) b
IRight p @@ n
p
Disproved Refuted (p @@ n)
v -> Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as))
-> Refuted (Any (Either j) p @@ as)
-> Decision (Any (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny IRight ('Right n) a
Elem (Either j) ('Right n) a
IRight p @@ a
p -> Refuted (p @@ n)
v p @@ n
p @@ a
p
idecideAll :: forall k (p :: k ~> *) (as :: Either j k).
(forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All (Either j) p @@ as)
idecideAll forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f = \case
SLeft Sing n
_ -> (All (Either j) p @@ as) -> Decision (All (Either j) p @@ as)
forall a. a -> Decision a
Proved ((All (Either j) p @@ as) -> Decision (All (Either j) p @@ as))
-> (All (Either j) p @@ as) -> Decision (All (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem (Either j) ('Left n) a -> p @@ a)
-> WitAll (Either j) p ('Left n)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem (Either j) ('Left n) a -> p @@ a)
-> WitAll (Either j) p ('Left n))
-> (forall (a :: k). Elem (Either j) ('Left n) a -> p @@ a)
-> WitAll (Either j) p ('Left n)
forall a b. (a -> b) -> a -> b
$ \case {}
SRight Sing n
x -> case Elem (Either j) as n -> Sing n -> Decision (p @@ n)
forall (a :: k).
Elem (Either j) as a -> Sing a -> Decision (p @@ a)
f IRight ('Right n) n
Elem (Either j) as n
forall {k} {j} (b :: k). IRight ('Right b) b
IRight Sing n
x of
Proved p @@ n
p -> (All (Either j) p @@ as) -> Decision (All (Either j) p @@ as)
forall a. a -> Decision a
Proved ((All (Either j) p @@ as) -> Decision (All (Either j) p @@ as))
-> (All (Either j) p @@ as) -> Decision (All (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a)
-> WitAll (Either j) p ('Right n)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a)
-> WitAll (Either j) p ('Right n))
-> (forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a)
-> WitAll (Either j) p ('Right n)
forall a b. (a -> b) -> a -> b
$ \case IRight ('Right n) a
Elem (Either j) ('Right n) a
IRight -> p @@ n
p @@ a
p
Disproved Refuted (p @@ n)
v -> Refuted (All (Either j) p @@ as)
-> Decision (All (Either j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All (Either j) p @@ as)
-> Decision (All (Either j) p @@ as))
-> Refuted (All (Either j) p @@ as)
-> Decision (All (Either j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \All (Either j) p @@ as
a -> Refuted (p @@ n)
v Refuted (p @@ n) -> Refuted (p @@ n)
forall a b. (a -> b) -> a -> b
$ WitAll (Either j) p ('Right n)
-> forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All (Either j) p @@ as
WitAll (Either j) p ('Right n)
a IRight ('Right n) n
Elem (Either j) ('Right n) n
forall {k} {j} (b :: k). IRight ('Right b) b
IRight
allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All (Either j) p --> TyPred (Prod (Either j) g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f = \case
SLeft Sing n
w -> \All (Either j) p @@ a
_ -> Sing n -> PEither g ('Left n)
forall {j} {k} (e :: j) (a :: k -> *).
Sing e -> PEither a ('Left e)
PLeft Sing n
w
SRight Sing n
x -> \All (Either j) p @@ a
a -> g n -> PEither g ('Right n)
forall {k} {j} (a :: k -> *) (a1 :: k).
a a1 -> PEither a ('Right a1)
PRight (Sing n -> (p @@ n) -> g n
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n
x (WitAll (Either j) p ('Right n)
-> forall (a :: k). Elem (Either j) ('Right n) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All (Either j) p @@ a
WitAll (Either j) p ('Right n)
a IRight ('Right n) n
Elem (Either j) ('Right n) n
forall {k} {j} (b :: k). IRight ('Right b) b
IRight))
prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: Either j k).
(forall (a :: k). g a -> p @@ a)
-> Prod (Either j) g as -> All (Either j) p @@ as
prodAll forall (a :: k). g a -> p @@ a
f = \case
PLeft Sing e
_ -> (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> WitAll (Either j) p ('Left e)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> WitAll (Either j) p ('Left e))
-> (forall (a :: k). Elem (Either j) ('Left e) a -> p @@ a)
-> WitAll (Either j) p ('Left e)
forall a b. (a -> b) -> a -> b
$ \case {}
PRight g a1
x -> (forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a)
-> WitAll (Either j) p ('Right a1)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a)
-> WitAll (Either j) p ('Right a1))
-> (forall (a :: k). Elem (Either j) ('Right a1) a -> p @@ a)
-> WitAll (Either j) p ('Right a1)
forall a b. (a -> b) -> a -> b
$ \case IRight ('Right a1) a
Elem (Either j) ('Right a1) a
IRight -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x
instance Universe NonEmpty where
idecideAny ::
forall k (p :: k ~> Type) (as :: NonEmpty k).
() =>
(forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) ->
Sing as ->
Decision (Any NonEmpty p @@ as)
idecideAny :: forall k (p :: k ~> *) (as :: NonEmpty k).
(forall (a :: k).
Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any NonEmpty p @@ as)
idecideAny forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f (Sing n1
x NE.:%| Sing n2
xs) = case Elem NonEmpty as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f NEIndex (n1 ':| n2) n1
Elem NonEmpty as n1
forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead Sing n1
x of
Proved p @@ n1
p -> (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as)
forall a. a -> Decision a
Proved ((Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as))
-> (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem NonEmpty (n1 ':| n2) n1
-> (p @@ n1) -> WitAny NonEmpty p (n1 ':| n2)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny NEIndex (n1 ':| n2) n1
Elem NonEmpty (n1 ':| n2) n1
forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead p @@ n1
p
Disproved Refuted (p @@ n1)
v -> case forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any f p @@ as)
idecideAny @[] @_ @p (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a)
Elem NonEmpty as a -> Sing a -> Decision (Apply p a)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a))
-> (Index n2 a -> NEIndex (n1 ':| n2) a)
-> Index n2 a
-> Sing a
-> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> NEIndex (n1 ':| n2) a
forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail) Sing n2
xs of
Proved (WitAny Elem [] n2 a
i p @@ a
p) -> (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as)
forall a. a -> Decision a
Proved ((Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as))
-> (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem NonEmpty (n1 ':| n2) a
-> (p @@ a) -> WitAny NonEmpty p (n1 ':| n2)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny (Index n2 a -> NEIndex (n1 ':| n2) a
forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail Index n2 a
Elem [] n2 a
i) p @@ a
p
Disproved Refuted (Any [] p @@ n2)
vs -> Refuted (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any NonEmpty p @@ as) -> Decision (Any NonEmpty p @@ as))
-> Refuted (Any NonEmpty p @@ as)
-> Decision (Any NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ \case
WitAny Elem NonEmpty (n1 ':| n2) a
i p @@ a
p -> case Elem NonEmpty (n1 ':| n2) a
i of
NEIndex (n1 ':| n2) a
Elem NonEmpty (n1 ':| n2) a
NEHead -> Refuted (p @@ n1)
v p @@ n1
p @@ a
p
NETail Index as a
i' -> Refuted (Any [] p @@ n2)
vs (Elem [] n2 a -> (p @@ a) -> WitAny [] p n2
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Index as a
Elem [] n2 a
i' p @@ a
p)
idecideAll ::
forall k (p :: k ~> Type) (as :: NonEmpty k).
() =>
(forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) ->
Sing as ->
Decision (All NonEmpty p @@ as)
idecideAll :: forall k (p :: k ~> *) (as :: NonEmpty k).
(forall (a :: k).
Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All NonEmpty p @@ as)
idecideAll forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f (Sing n1
x NE.:%| Sing n2
xs) = case Elem NonEmpty as n1 -> Sing n1 -> Decision (p @@ n1)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f NEIndex (n1 ':| n2) n1
Elem NonEmpty as n1
forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead Sing n1
x of
Proved p @@ n1
p -> case forall (f :: * -> *) k (p :: k ~> *) (as :: f k).
Universe f =>
(forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All f p @@ as)
idecideAll @[] @_ @p (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a)
Elem NonEmpty as a -> Sing a -> Decision (Apply p a)
forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)
f (NEIndex (n1 ':| n2) a -> Sing a -> Decision (Apply p a))
-> (Index n2 a -> NEIndex (n1 ':| n2) a)
-> Index n2 a
-> Sing a
-> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> NEIndex (n1 ':| n2) a
forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail) Sing n2
xs of
Proved All [] p @@ n2
ps -> (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as)
forall a. a -> Decision a
Proved ((All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as))
-> (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a)
-> WitAll NonEmpty p (n1 ':| n2)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a)
-> WitAll NonEmpty p (n1 ':| n2))
-> (forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a)
-> WitAll NonEmpty p (n1 ':| n2)
forall a b. (a -> b) -> a -> b
$ \case
NEIndex (n1 ':| n2) a
Elem NonEmpty (n1 ':| n2) a
NEHead -> p @@ n1
p @@ a
p
NETail Index as a
i -> WitAll [] p n2 -> forall (a :: k). Elem [] n2 a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All [] p @@ n2
WitAll [] p n2
ps Index as a
Elem [] n2 a
i
Disproved Refuted (All [] p @@ n2)
v -> Refuted (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as))
-> Refuted (All NonEmpty p @@ as)
-> Decision (All NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ \All NonEmpty p @@ as
a -> Refuted (All [] p @@ n2)
v Refuted (All [] p @@ n2) -> Refuted (All [] p @@ n2)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (WitAll NonEmpty p (n1 ':| n2)
-> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ as
WitAll NonEmpty p (n1 ':| n2)
a (NEIndex (n1 ':| n2) a -> Apply p a)
-> (Index n2 a -> NEIndex (n1 ':| n2) a) -> Index n2 a -> Apply p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> NEIndex (n1 ':| n2) a
forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail)
Disproved Refuted (p @@ n1)
v -> Refuted (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All NonEmpty p @@ as) -> Decision (All NonEmpty p @@ as))
-> Refuted (All NonEmpty p @@ as)
-> Decision (All NonEmpty p @@ as)
forall a b. (a -> b) -> a -> b
$ \All NonEmpty p @@ as
a -> Refuted (p @@ n1)
v Refuted (p @@ n1) -> Refuted (p @@ n1)
forall a b. (a -> b) -> a -> b
$ WitAll NonEmpty p (n1 ':| n2)
-> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ as
WitAll NonEmpty p (n1 ':| n2)
a NEIndex (n1 ':| n2) n1
Elem NonEmpty (n1 ':| n2) n1
forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead
allProd ::
forall p g.
() =>
(forall a. Sing a -> p @@ a -> g a) ->
All NonEmpty p --> TyPred (Prod NonEmpty g)
allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All NonEmpty p --> TyPred (Prod NonEmpty g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f (Sing n1
x NE.:%| Sing n2
xs) All NonEmpty p @@ a
a =
Sing n1 -> (p @@ n1) -> g n1
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n1
x (WitAll NonEmpty p (n1 ':| n2)
-> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ a
WitAll NonEmpty p (n1 ':| n2)
a NEIndex (n1 ':| n2) n1
Elem NonEmpty (n1 ':| n2) n1
forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead)
g n1 -> Rec g n2 -> NERec g (n1 ':| n2)
forall {k} (a :: k -> *) (a1 :: k) (as :: [k]).
a a1 -> Rec a as -> NERec a (a1 ':| as)
:&| forall (f :: * -> *) {k} (p :: Predicate k) (g :: k -> *).
Universe f =>
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All f p --> TyPred (Prod f g)
allProd @[] @p Sing a -> (p @@ a) -> g a
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n2
xs ((forall (a :: k). Elem [] n2 a -> p @@ a) -> WitAll [] p n2
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll (WitAll NonEmpty p (n1 ':| n2)
-> forall (a :: k). Elem NonEmpty (n1 ':| n2) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All NonEmpty p @@ a
WitAll NonEmpty p (n1 ':| n2)
a (NEIndex (n1 ':| n2) a -> Apply p a)
-> (Index n2 a -> NEIndex (n1 ':| n2) a) -> Index n2 a -> Apply p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n2 a -> NEIndex (n1 ':| n2) a
forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail))
prodAll ::
forall p g as.
() =>
(forall a. g a -> p @@ a) ->
Prod NonEmpty g as ->
All NonEmpty p @@ as
prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: NonEmpty k).
(forall (a :: k). g a -> p @@ a)
-> Prod NonEmpty g as -> All NonEmpty p @@ as
prodAll forall (a :: k). g a -> p @@ a
f (g a1
x :&| Rec g as
xs) = (forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a)
-> WitAll NonEmpty p (a1 ':| as)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a)
-> WitAll NonEmpty p (a1 ':| as))
-> (forall (a :: k). Elem NonEmpty (a1 ':| as) a -> p @@ a)
-> WitAll NonEmpty p (a1 ':| as)
forall a b. (a -> b) -> a -> b
$ \case
NEIndex (a1 ':| as) a
Elem NonEmpty (a1 ':| as) a
NEHead -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x
NETail Index as a
i -> WitAll [] p as -> forall (a :: k). Elem [] as a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll (forall (f :: * -> *) {k} (p :: Predicate k) (g :: k -> *)
(as :: f k).
Universe f =>
(forall (a :: k). g a -> p @@ a) -> Prod f g as -> All f p @@ as
prodAll @[] @p g a -> p @@ a
forall (a :: k). g a -> p @@ a
f Rec g as
Prod [] g as
xs) Index as a
Elem [] as a
i
instance Universe ((,) j) where
idecideAny :: forall k (p :: k ~> *) (as :: (j, k)).
(forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any ((,) j) p @@ as)
idecideAny forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f (STuple2 Sing n1
_ Sing n2
x) = case Elem ((,) j) as n2 -> Sing n2 -> Decision (p @@ n2)
forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f ISnd '(n1, n2) n2
Elem ((,) j) as n2
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd Sing n2
x of
Proved p @@ n2
p -> (Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as)
forall a. a -> Decision a
Proved ((Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as))
-> (Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem ((,) j) '(n1, n2) n2
-> (p @@ n2) -> WitAny ((,) j) p '(n1, n2)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny ISnd '(n1, n2) n2
Elem ((,) j) '(n1, n2) n2
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd p @@ n2
p
Disproved Refuted (p @@ n2)
v -> Refuted (Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as))
-> Refuted (Any ((,) j) p @@ as) -> Decision (Any ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \case WitAny ISnd '(n1, n2) a
Elem ((,) j) '(n1, n2) a
ISnd p @@ a
p -> Refuted (p @@ n2)
v p @@ n2
p @@ a
p
idecideAll :: forall k (p :: k ~> *) (as :: (j, k)).
(forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All ((,) j) p @@ as)
idecideAll forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f (STuple2 Sing n1
_ Sing n2
x) = case Elem ((,) j) as n2 -> Sing n2 -> Decision (p @@ n2)
forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)
f ISnd '(n1, n2) n2
Elem ((,) j) as n2
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd Sing n2
x of
Proved p @@ n2
p -> (All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as)
forall a. a -> Decision a
Proved ((All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as))
-> (All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a)
-> WitAll ((,) j) p '(n1, n2)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a)
-> WitAll ((,) j) p '(n1, n2))
-> (forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a)
-> WitAll ((,) j) p '(n1, n2)
forall a b. (a -> b) -> a -> b
$ \case ISnd '(n1, n2) a
Elem ((,) j) '(n1, n2) a
ISnd -> p @@ n2
p @@ a
p
Disproved Refuted (p @@ n2)
v -> Refuted (All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as)
forall a. Refuted a -> Decision a
Disproved (Refuted (All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as))
-> Refuted (All ((,) j) p @@ as) -> Decision (All ((,) j) p @@ as)
forall a b. (a -> b) -> a -> b
$ \All ((,) j) p @@ as
a -> Refuted (p @@ n2)
v Refuted (p @@ n2) -> Refuted (p @@ n2)
forall a b. (a -> b) -> a -> b
$ WitAll ((,) j) p '(n1, n2)
-> forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All ((,) j) p @@ as
WitAll ((,) j) p '(n1, n2)
a ISnd '(n1, n2) n2
Elem ((,) j) '(n1, n2) n2
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd
allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All ((,) j) p --> TyPred (Prod ((,) j) g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f (STuple2 Sing n1
w Sing n2
x) All ((,) j) p @@ a
a = Sing n1 -> g n2 -> PTup g '(n1, n2)
forall {j} {k} (w :: j) (a :: k -> *) (a1 :: k).
Sing w -> a a1 -> PTup a '(w, a1)
PTup Sing n1
w (g n2 -> PTup g '(n1, n2)) -> g n2 -> PTup g '(n1, n2)
forall a b. (a -> b) -> a -> b
$ Sing n2 -> (p @@ n2) -> g n2
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n2
x (WitAll ((,) j) p '(n1, n2)
-> forall (a :: k). Elem ((,) j) '(n1, n2) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All ((,) j) p @@ a
WitAll ((,) j) p '(n1, n2)
a ISnd '(n1, n2) n2
Elem ((,) j) '(n1, n2) n2
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd)
prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: (j, k)).
(forall (a :: k). g a -> p @@ a)
-> Prod ((,) j) g as -> All ((,) j) p @@ as
prodAll forall (a :: k). g a -> p @@ a
f (PTup Sing w
_ g a1
x) = (forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a)
-> WitAll ((,) j) p '(w, a1)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a)
-> WitAll ((,) j) p '(w, a1))
-> (forall (a :: k). Elem ((,) j) '(w, a1) a -> p @@ a)
-> WitAll ((,) j) p '(w, a1)
forall a b. (a -> b) -> a -> b
$ \case ISnd '(w, a1) a
Elem ((,) j) '(w, a1) a
ISnd -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x
instance Universe Identity where
idecideAny :: forall k (p :: k ~> *) (as :: Identity k).
(forall (a :: k).
Elem Identity as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (Any Identity p @@ as)
idecideAny forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f (SIdentity Sing n
x) =
(Apply p n -> Any Identity p @@ as)
-> ((Any Identity p @@ as) -> Apply p n)
-> Decision (Apply p n)
-> Decision (Any Identity p @@ as)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision
(Elem Identity ('Identity n) n
-> Apply p n -> WitAny Identity p ('Identity n)
forall {k1} (f :: * -> *) (as :: f k1) (a :: k1) (p :: k1 ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny IIdentity ('Identity n) n
Elem Identity ('Identity n) n
forall {k} (b :: k). IIdentity ('Identity b) b
IId)
(\case WitAny IIdentity ('Identity n) a
Elem Identity ('Identity n) a
IId p @@ a
p -> Apply p n
p @@ a
p)
(Decision (Apply p n) -> Decision (Any Identity p @@ as))
-> Decision (Apply p n) -> Decision (Any Identity p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem Identity as n -> Sing n -> Decision (Apply p n)
forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f IIdentity ('Identity n) n
Elem Identity as n
forall {k} (b :: k). IIdentity ('Identity b) b
IId Sing n
x
idecideAll :: forall k (p :: k ~> *) (as :: Identity k).
(forall (a :: k).
Elem Identity as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (All Identity p @@ as)
idecideAll forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f (SIdentity Sing n
x) =
(Apply p n -> All Identity p @@ as)
-> ((All Identity p @@ as) -> Apply p n)
-> Decision (Apply p n)
-> Decision (All Identity p @@ as)
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision
(\Apply p n
p -> (forall (a :: k). Elem Identity ('Identity n) a -> p @@ a)
-> WitAll Identity p ('Identity n)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Identity ('Identity n) a -> p @@ a)
-> WitAll Identity p ('Identity n))
-> (forall (a :: k). Elem Identity ('Identity n) a -> p @@ a)
-> WitAll Identity p ('Identity n)
forall a b. (a -> b) -> a -> b
$ \case IIdentity ('Identity n) a
Elem Identity ('Identity n) a
IId -> Apply p n
p @@ a
p)
(\All Identity p @@ as
y -> WitAll Identity p ('Identity n)
-> forall (a :: k). Elem Identity ('Identity n) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Identity p @@ as
WitAll Identity p ('Identity n)
y IIdentity ('Identity n) n
Elem Identity ('Identity n) n
forall {k} (b :: k). IIdentity ('Identity b) b
IId)
(Decision (Apply p n) -> Decision (All Identity p @@ as))
-> Decision (Apply p n) -> Decision (All Identity p @@ as)
forall a b. (a -> b) -> a -> b
$ Elem Identity as n -> Sing n -> Decision (Apply p n)
forall (a :: k). Elem Identity as a -> Sing a -> Decision (p @@ a)
f IIdentity ('Identity n) n
Elem Identity as n
forall {k} (b :: k). IIdentity ('Identity b) b
IId Sing n
x
allProd :: forall {k} (p :: Predicate k) (g :: k -> *).
(forall (a :: k). Sing a -> (p @@ a) -> g a)
-> All Identity p --> TyPred (Prod Identity g)
allProd forall (a :: k). Sing a -> (p @@ a) -> g a
f (SIdentity Sing n
x) All Identity p @@ a
a = g n -> PIdentity g ('Identity n)
forall {k} (a :: k -> *) (a1 :: k).
a a1 -> PIdentity a ('Identity a1)
PIdentity (g n -> PIdentity g ('Identity n))
-> g n -> PIdentity g ('Identity n)
forall a b. (a -> b) -> a -> b
$ Sing n -> (p @@ n) -> g n
forall (a :: k). Sing a -> (p @@ a) -> g a
f Sing n
x (WitAll Identity p ('Identity n)
-> forall (a :: k). Elem Identity ('Identity n) a -> p @@ a
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All Identity p @@ a
WitAll Identity p ('Identity n)
a IIdentity ('Identity n) n
Elem Identity ('Identity n) n
forall {k} (b :: k). IIdentity ('Identity b) b
IId)
prodAll :: forall {k} (p :: Predicate k) (g :: k -> *) (as :: Identity k).
(forall (a :: k). g a -> p @@ a)
-> Prod Identity g as -> All Identity p @@ as
prodAll forall (a :: k). g a -> p @@ a
f (PIdentity g a1
x) = (forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a)
-> WitAll Identity p ('Identity a1)
forall k (f :: * -> *) (p :: k ~> *) (as :: f k).
(forall (a :: k). Elem f as a -> p @@ a) -> WitAll f p as
WitAll ((forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a)
-> WitAll Identity p ('Identity a1))
-> (forall (a :: k). Elem Identity ('Identity a1) a -> p @@ a)
-> WitAll Identity p ('Identity a1)
forall a b. (a -> b) -> a -> b
$ \case IIdentity ('Identity a1) a
Elem Identity ('Identity a1) a
IId -> g a1 -> p @@ a1
forall (a :: k). g a -> p @@ a
f g a1
x