{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Predicate.Quantification (
Any, WitAny(..), None, anyImpossible
, decideAny, idecideAny, decideNone, idecideNone
, entailAny, ientailAny, entailAnyF, ientailAnyF
, All, WitAll(..), NotAll
, decideAll, idecideAll
, entailAll, ientailAll, entailAllF, ientailAllF
, decideEntailAll, idecideEntailAll
, allToAny
, allNotNone, noneAllNot
, anyNotNotAll, notAllAnyNot
) where
import Data.Kind
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Type.Universe
idecideNone
:: forall f k (p :: k ~> Type) (as :: f k). Universe f
=> (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
-> (Sing as -> Decision (None f p @@ as))
idecideNone :: (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a))
-> Sing as -> Decision (None f p @@ as)
idecideNone f :: forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)
f xs :: Sing as
xs = forall (a :: f k).
Decision (Any f p @@ a) -> Decision (None f p @@ a)
forall k1 (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
decideNot @(Any f p) (Decision (Any f p @@ as) -> Decision (None f p @@ as))
-> Decision (Any f p @@ as) -> Decision (None f p @@ as)
forall a b. (a -> b) -> a -> b
$ (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 forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)
f Sing as
xs
decideNone
:: forall f k (p :: k ~> Type). Universe f
=> Decide p
-> Decide (None f p)
decideNone :: Decide p -> Decide (None f p)
decideNone f :: Decide p
f = (forall (a :: k). Elem f a a -> Sing a -> Decision (p @@ a))
-> Sing a -> Decision (Apply (None f p) a)
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 (None f p @@ as)
idecideNone ((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)
ientailAny
:: forall f p q as. (Universe f, SingI as)
=> (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)
-> Any f p @@ as
-> Any f q @@ as
ientailAny :: (forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a)
-> (Any f p @@ as) -> Any f q @@ as
ientailAny f :: forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a
f (WitAny i x) = Elem f as a -> (q @@ a) -> WitAny f q as
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f as a
i (Elem f as a -> Sing a -> (p @@ a) -> q @@ a
forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a
f Elem f as a
i (Elem f as a -> Sing as -> Sing a
forall k (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f as a
i Sing as
forall k (a :: k). SingI a => Sing a
sing) p @@ a
x)
entailAny
:: forall f p q. Universe f
=> (p --> q)
-> (Any f p --> Any f q)
entailAny :: (p --> q) -> Any f p --> Any f q
entailAny = forall (p :: k ~> *) (q :: k ~> *).
TFunctor (Any f) =>
(p --> q) -> Any f p --> Any f q
forall k1 k1 (f :: (k1 ~> *) -> k1 ~> *) (p :: k1 ~> *)
(q :: k1 ~> *).
TFunctor f =>
(p --> q) -> f p --> f q
tmap @(Any f)
ientailAll
:: forall f p q as. (Universe f, SingI as)
=> (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)
-> All f p @@ as
-> All f q @@ as
ientailAll :: (forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a)
-> (All f p @@ as) -> All f q @@ as
ientailAll f :: forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a
f a :: All f p @@ as
a = (forall (a :: k). Elem f as a -> q @@ a) -> All f q @@ 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 f as a -> q @@ a) -> All f q @@ as)
-> (forall (a :: k). Elem f as a -> q @@ a) -> All f q @@ as
forall a b. (a -> b) -> a -> b
$ \i :: Elem f as a
i -> Elem f as a -> Sing a -> (p @@ a) -> q @@ a
forall (a :: k). Elem f as a -> Sing a -> (p @@ a) -> q @@ a
f Elem f as a
i (Elem f as a -> Sing as -> Sing a
forall k (f :: * -> *) (as :: f k) (a :: k).
FProd f =>
Elem f as a -> Sing as -> Sing a
indexSing Elem f as a
i Sing as
forall k (a :: k). SingI a => Sing a
sing) (WitAll f p as -> Elem f as a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ as
WitAll f p as
a Elem f as a
i)
entailAll
:: forall f p q. Universe f
=> (p --> q)
-> (All f p --> All f q)
entailAll :: (p --> q) -> All f p --> All f q
entailAll = forall (p :: k ~> *) (q :: k ~> *).
TFunctor (All f) =>
(p --> q) -> All f p --> All f q
forall k1 k1 (f :: (k1 ~> *) -> k1 ~> *) (p :: k1 ~> *)
(q :: k1 ~> *).
TFunctor f =>
(p --> q) -> f p --> f q
tmap @(All f)
ientailAnyF
:: forall f p q as h. Functor h
=> (forall a. Elem f as a -> p @@ a -> h (q @@ a))
-> Any f p @@ as
-> h (Any f q @@ as)
ientailAnyF :: (forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (Any f p @@ as) -> h (Any f q @@ as)
ientailAnyF f :: forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a)
f = \case WitAny i x -> Elem f as a -> (q @@ a) -> WitAny f q as
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f as a
i ((q @@ a) -> WitAny f q as) -> h (q @@ a) -> h (WitAny f q as)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elem f as a -> (p @@ a) -> h (q @@ a)
forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a)
f Elem f as a
i p @@ a
x
entailAnyF
:: forall f p q h. (Universe f, Functor h)
=> (p --># q) h
-> (Any f p --># Any f q) h
entailAnyF :: (-->#) p q h -> (-->#) (Any f p) (Any f q) h
entailAnyF f :: (-->#) p q h
f x :: Sing a
x a :: Any f p @@ a
a = Sing a -> (SingI a => h (WitAny f q a)) -> h (WitAny f q a)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
x ((SingI a => h (WitAny f q a)) -> h (Apply (Any f q) a))
-> (SingI a => h (WitAny f q a)) -> h (Apply (Any f q) a)
forall a b. (a -> b) -> a -> b
$
(forall (a :: k). Elem f a a -> (p @@ a) -> h (q @@ a))
-> (Any f p @@ a) -> h (Apply (Any f q) a)
forall k (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
(as :: f k) (h :: * -> *).
Functor h =>
(forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (Any f p @@ as) -> h (Any f q @@ as)
ientailAnyF @f @p @q (\i :: Elem f a a
i -> Sing a -> (p @@ a) -> h (q @@ a)
(-->#) p q h
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
x)) Any f p @@ a
a
ientailAllF
:: forall f p q as h. (Universe f, Applicative h, SingI as)
=> (forall a. Elem f as a -> p @@ a -> h (q @@ a))
-> All f p @@ as
-> h (All f q @@ as)
ientailAllF :: (forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (All f p @@ as) -> h (All f q @@ as)
ientailAllF f :: forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a)
f a :: All f p @@ as
a = (Prod f (Wit q) as -> WitAll f q as)
-> h (Prod f (Wit q) as) -> h (WitAll f q as)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall (a :: k). Wit q a -> q @@ a)
-> Prod f (Wit q) as -> All f q @@ 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 forall (a :: k). Wit q a -> q @@ a
forall k1 (p :: k1 ~> *) (a :: k1). Wit p a -> p @@ a
getWit)
(h (Prod f (Wit q) as) -> h (WitAll f q as))
-> (Prod f Sing as -> h (Prod f (Wit q) as))
-> Prod f Sing as
-> h (WitAll f q as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). Elem f as a -> Sing a -> h (Wit q a))
-> Prod f Sing as -> h (Prod f (Wit q) 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 _ -> forall (a :: k). (q @@ a) -> Wit q a
forall k1 (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit @q ((q @@ a) -> Wit q a) -> h (q @@ a) -> h (Wit q a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Elem f as a -> (p @@ a) -> h (q @@ a)
forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a)
f Elem f as a
i (WitAll f p as -> Elem f as a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ as
WitAll f p as
a Elem f as a
i))
(Prod f Sing as -> h (All f q @@ as))
-> Prod f Sing as -> h (All f q @@ as)
forall a b. (a -> b) -> a -> b
$ Sing as -> Prod f Sing as
forall (f :: * -> *) k (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd (SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as)
entailAllF
:: forall f p q h. (Universe f, Applicative h)
=> (p --># q) h
-> (All f p --># All f q) h
entailAllF :: (-->#) p q h -> (-->#) (All f p) (All f q) h
entailAllF f :: (-->#) p q h
f x :: Sing a
x a :: All f p @@ a
a = Sing a -> (SingI a => h (WitAll f q a)) -> h (WitAll f q a)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
x ((SingI a => h (WitAll f q a)) -> h (Apply (All f q) a))
-> (SingI a => h (WitAll f q a)) -> h (Apply (All f q) a)
forall a b. (a -> b) -> a -> b
$
(forall (a :: k). Elem f a a -> (p @@ a) -> h (q @@ a))
-> (All f p @@ a) -> h (Apply (All f q) a)
forall k (f :: * -> *) (p :: Predicate k) (q :: Predicate k)
(as :: f k) (h :: * -> *).
(Universe f, Applicative h, SingI as) =>
(forall (a :: k). Elem f as a -> (p @@ a) -> h (q @@ a))
-> (All f p @@ as) -> h (All f q @@ as)
ientailAllF @f @p @q (\i :: Elem f a a
i -> Sing a -> (p @@ a) -> h (q @@ a)
(-->#) p q h
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
x)) All f p @@ a
a
idecideEntailAll
:: forall f p q as. (Universe f, SingI as)
=> (forall a. Elem f as a -> p @@ a -> Decision (q @@ a))
-> All f p @@ as
-> Decision (All f q @@ as)
idecideEntailAll :: (forall (a :: k). Elem f as a -> (p @@ a) -> Decision (q @@ a))
-> (All f p @@ as) -> Decision (All f q @@ as)
idecideEntailAll f :: forall (a :: k). Elem f as a -> (p @@ a) -> Decision (q @@ a)
f a :: All f p @@ as
a = (forall (a :: k). Elem f as a -> Sing a -> Decision (q @@ a))
-> Sing as -> Decision (All f q @@ 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 (\i :: Elem f as a
i _ -> Elem f as a -> (p @@ a) -> Decision (q @@ a)
forall (a :: k). Elem f as a -> (p @@ a) -> Decision (q @@ a)
f Elem f as a
i (WitAll f p as -> Elem f as a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f p @@ as
WitAll f p as
a Elem f as a
i)) Sing as
forall k (a :: k). SingI a => Sing a
sing
decideEntailAll
:: forall f p q. Universe f
=> p -?> q
-> All f p -?> All f q
decideEntailAll :: (p -?> q) -> All f p -?> All f q
decideEntailAll = forall (p :: k ~> *) (q :: k ~> *).
DFunctor (All f) =>
(p -?> q) -> All f p -?> All f q
forall k1 k1 (f :: (k1 ~> *) -> k1 ~> *) (p :: k1 ~> *)
(q :: k1 ~> *).
DFunctor f =>
(p -?> q) -> f p -?> f q
dmap @(All f)
anyImpossible :: Universe f => Any f Impossible --> Impossible
anyImpossible :: Any f Impossible --> Impossible
anyImpossible _ (WitAny i p) = Impossible @@ a
Sing a -> Void
p (Sing a -> Void) -> (Sing a -> Sing a) -> Sing a -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
anyNotNotAll :: Any f (Not p) --> NotAll f p
anyNotNotAll :: Sing a -> (Any f (Not p) @@ a) -> NotAll f p @@ a
anyNotNotAll _ (WitAny i v) a :: WitAll f p a
a = Not p @@ a
Refuted (p @@ a)
v Refuted (p @@ a) -> Refuted (p @@ a)
forall a b. (a -> b) -> a -> b
$ WitAll f p a -> Elem f a a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll f p a
a Elem f a a
i
notAllAnyNot
:: forall f p. (Universe f, Decidable p)
=> NotAll f p --> Any f (Not p)
notAllAnyNot :: NotAll f p --> Any f (Not p)
notAllAnyNot xs :: Sing a
xs vAll :: NotAll f p @@ a
vAll = Decision (WitAny f (Not p) a)
-> Refuted (Refuted (WitAny f (Not p) a)) -> WitAny f (Not p) a
forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof (Sing a -> Decision (Apply (Any f (Not p)) a)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @(Any f (Not p)) Sing a
xs) (Refuted (Refuted (WitAny f (Not p) a)) -> Apply (Any f (Not p)) a)
-> Refuted (Refuted (WitAny f (Not p) a))
-> Apply (Any f (Not p)) a
forall a b. (a -> b) -> a -> b
$ \vAny :: Refuted (WitAny f (Not p) a)
vAny ->
NotAll f p @@ a
WitAll f p a -> Void
vAll (WitAll f p a -> Void) -> WitAll f p a -> Void
forall a b. (a -> b) -> a -> b
$ (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
$ \i :: Elem f a a
i ->
Decision (Apply p a) -> Refuted (Refuted (Apply p a)) -> Apply p a
forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof (Sing a -> Decision (Apply p a)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @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)) (Refuted (Refuted (Apply p a)) -> Apply p a)
-> Refuted (Refuted (Apply p a)) -> Apply p a
forall a b. (a -> b) -> a -> b
$ \vP :: Refuted (Apply p a)
vP ->
Refuted (WitAny f (Not p) a)
vAny Refuted (WitAny f (Not p) a) -> Refuted (WitAny f (Not p) a)
forall a b. (a -> b) -> a -> b
$ Elem f a a -> (Not p @@ a) -> WitAny f (Not p) a
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i Not p @@ a
Refuted (Apply p a)
vP
allNotNone :: All f (Not p) --> None f p
allNotNone :: Sing a -> (All f (Not p) @@ a) -> None f p @@ a
allNotNone _ a :: All f (Not p) @@ a
a (WitAny i :: Elem f a a
i v :: p @@ a
v) = WitAll f (Not p) a -> Elem f a a -> Refuted (p @@ a)
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll All f (Not p) @@ a
WitAll f (Not p) a
a Elem f a a
i p @@ a
v
noneAllNot
:: forall f p. (Universe f, Decidable p)
=> None f p --> All f (Not p)
noneAllNot :: None f p --> All f (Not p)
noneAllNot xs :: Sing a
xs vAny :: None f p @@ a
vAny = Decision (WitAll f (Not p) a)
-> Refuted (Refuted (WitAll f (Not p) a)) -> WitAll f (Not p) a
forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof (Sing a -> Decision (Apply (All f (Not p)) a)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @(All f (Not p)) Sing a
xs) (Refuted (Refuted (WitAll f (Not p) a)) -> Apply (All f (Not p)) a)
-> Refuted (Refuted (WitAll f (Not p) a))
-> Apply (All f (Not p)) a
forall a b. (a -> b) -> a -> b
$ \vAll :: Refuted (WitAll f (Not p) a)
vAll ->
Refuted (WitAll f (Not p) a)
vAll Refuted (WitAll f (Not p) a) -> Refuted (WitAll f (Not p) a)
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). Elem f a a -> Not p @@ a) -> WitAll f (Not 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 -> Not p @@ a) -> WitAll f (Not p) a)
-> (forall (a :: k). Elem f a a -> Not p @@ a)
-> WitAll f (Not p) a
forall a b. (a -> b) -> a -> b
$ \i :: Elem f a a
i p :: Apply p a
p -> None f p @@ a
WitAny f p a -> Void
vAny (WitAny f p a -> Void) -> WitAny f p a -> Void
forall a b. (a -> b) -> a -> b
$ Elem f a a -> Apply p a -> WitAny f p a
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i Apply p a
p
allToAny :: (All f p &&& NotNull f) --> Any f p
allToAny :: Sing a -> ((All f p &&& NotNull f) @@ a) -> Any f p @@ a
allToAny _ (a, WitAny i _) = Elem f a a -> (p @@ a) -> WitAny f p a
forall k (f :: * -> *) (as :: f k) (a :: k) (p :: k ~> *).
Elem f as a -> (p @@ a) -> WitAny f p as
WitAny Elem f a a
i ((p @@ a) -> Any f p @@ a) -> (p @@ a) -> Any f p @@ a
forall a b. (a -> b) -> a -> b
$ WitAll f p a -> Elem f a a -> p @@ a
forall k (p :: k ~> *) (f :: * -> *) (as :: f k).
WitAll f p as -> forall (a :: k). Elem f as a -> p @@ a
runWitAll WitAll f p a
a Elem f a a
i