{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Predicate.Param (
ParamPred,
IsTC,
EqBy,
FlipPP,
ConstPP,
PPMap,
PPMapV,
InP,
AnyMatch,
TyPP,
Found,
NotFound,
Selectable,
select,
Searchable,
search,
inPNotNull,
notNullInP,
SelectableTC,
selectTC,
SearchableTC,
searchTC,
OrP,
AndP,
) where
import Data.Kind
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.Sigma
import Data.Tuple.Singletons
import Data.Type.Functor.Product
import Data.Type.Predicate
import Data.Type.Predicate.Logic
import Data.Type.Universe
type ParamPred k v = k -> Predicate v
data Found :: ParamPred k v -> Predicate k
type instance Apply (Found (p :: ParamPred k v)) a = Σ v (p a)
type NotFound (p :: ParamPred k v) = (Not (Found p) :: Predicate k)
data FlipPP :: ParamPred v k -> ParamPred k v
type instance Apply (FlipPP p x) y = p y @@ x
data ConstPP :: Predicate v -> ParamPred k v
type instance Apply (ConstPP p k) v = p @@ v
data EqBy :: (v ~> k) -> ParamPred k v
type instance Apply (EqBy f x) y = x :~: (f @@ y)
type IsTC t = EqBy (TyCon1 t)
data TyPP :: (k -> v -> Type) -> ParamPred k v
type instance Apply (TyPP t k) v = t k v
data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v
type instance Apply (PPMap f p x) y = p (f @@ x) @@ y
data PPMapV :: (u ~> v) -> ParamPred k u -> ParamPred k v
type instance Apply (PPMapV f p x) y = p x @@ (f @@ y)
instance (Decidable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Decidable (Found (PPMap f p)) where
decide :: Decide (Found (PPMap f p))
decide =
(Sigma v (p (Apply f a)) -> Sigma v (PPMap f p a))
-> (Sigma v (PPMap f p a) -> Sigma v (p (Apply f a)))
-> Decision (Sigma v (p (Apply f a)))
-> Decision (Sigma v (PPMap f p a))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision
(\case Sing fst
i :&: p (Apply f a) @@ fst
p -> Sing fst
i Sing fst -> (PPMap f p a @@ fst) -> Sigma v (PPMap f p a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: p (Apply f a) @@ fst
PPMap f p a @@ fst
p)
(\case Sing fst
i :&: PPMap f p a @@ fst
p -> Sing fst
i Sing fst -> (p (Apply f a) @@ fst) -> Sigma v (p (Apply f a))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: p (Apply f a) @@ fst
PPMap f p a @@ fst
p)
(Decision (Sigma v (p (Apply f a)))
-> Decision (Sigma v (PPMap f p a)))
-> (Sing a -> Decision (Sigma v (p (Apply f a))))
-> Sing a
-> Decision (Sigma v (PPMap f p a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: j ~> *). Decidable p => Decide p
decide @(Found p)
(Sing (Apply f a) -> Decision (Sigma v (p (Apply f a))))
-> (Sing a -> Sing (Apply f a))
-> Sing a
-> Decision (Sigma v (p (Apply f a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SLambda f -> forall (t :: k). Sing t -> Sing (f @@ t)
forall k1 k2 (f :: k1 ~> k2).
SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing (Sing f
forall {k} (a :: k). SingI a => Sing a
sing :: Sing f)
instance (Provable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Provable (Found (PPMap f p)) where
prove :: Prove (Found (PPMap f p))
prove (Sing a
x :: Sing a) = case forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: j ~> *). Provable p => Prove p
prove @(Found p) ((Sing f
forall {k} (a :: k). SingI a => Sing a
sing :: Sing f) Sing f -> Sing a -> Sing (Apply f a)
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ Sing a
x) of
Sing fst
i :&: p (Apply f a) @@ fst
p -> Sing fst
i Sing fst -> (PPMap f p a @@ fst) -> Sigma v (PPMap f p a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: p (Apply f a) @@ fst
PPMap f p a @@ fst
p
type Searchable p = Decidable (Found p)
type Selectable p = Provable (Found p)
search ::
forall p.
Searchable p =>
Decide (Found p)
search :: forall {k1} {v} (p :: ParamPred k1 v).
Searchable p =>
Decide (Found p)
search = forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k1 ~> *). Decidable p => Decide p
decide @(Found p)
select ::
forall p.
Selectable p =>
Prove (Found p)
select :: forall {k1} {v} (p :: ParamPred k1 v).
Selectable p =>
Prove (Found p)
select = forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k1 ~> *). Provable p => Prove p
prove @(Found p)
type SearchableTC t = Decidable (Found (TyPP t))
type SelectableTC t = Provable (Found (TyPP t))
searchTC ::
forall t.
SearchableTC t =>
Decide (Found (TyPP t))
searchTC :: forall {k1} {v} (t :: k1 -> v -> *).
SearchableTC t =>
Decide (Found (TyPP t))
searchTC = forall {k1} {v} (p :: ParamPred k1 v).
Searchable p =>
Decide (Found p)
forall (p :: ParamPred k1 v). Searchable p => Decide (Found p)
search @(TyPP t)
selectTC ::
forall t.
SelectableTC t =>
Prove (Found (TyPP t))
selectTC :: forall {k1} {v} (t :: k1 -> v -> *).
SelectableTC t =>
Prove (Found (TyPP t))
selectTC = forall {k1} {v} (p :: ParamPred k1 v).
Selectable p =>
Prove (Found p)
forall (p :: ParamPred k1 v). Selectable p => Prove (Found p)
select @(TyPP t)
type InP f = (ElemSym1 f :: ParamPred (f k) k)
notNullInP :: NotNull f --> Found (InP f)
notNullInP :: forall {k} (f :: * -> *) (a :: f k).
Sing a -> (NotNull f @@ a) -> Found (InP f) @@ a
notNullInP Sing a
_ (WitAny Elem f a a1
i Evident @@ a1
s) = Sing a1
Evident @@ a1
s Sing a1 -> (ElemSym1 f a @@ a1) -> Sigma k (ElemSym1 f a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: Elem f a a1
ElemSym1 f a @@ a1
i
inPNotNull :: Found (InP f) --> NotNull f
inPNotNull :: forall {v} (f :: * -> *) (a :: f v).
Sing a -> (Found (InP f) @@ a) -> NotNull f @@ a
inPNotNull Sing a
_ (Sing fst
s :&: ElemSym1 f a @@ fst
i) = Elem f a fst -> (Evident @@ fst) -> WitAny f Evident a
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f a fst
ElemSym1 f a @@ fst
i Sing fst
Evident @@ fst
s
instance Universe f => Decidable (Found (InP f)) where
decide :: Decide (Found (InP f))
decide =
(WitAny f Evident a -> Sigma v (ElemSym1 f a))
-> (Sigma v (ElemSym1 f a) -> WitAny f Evident a)
-> Decision (WitAny f Evident a)
-> Decision (Sigma v (ElemSym1 f a))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision
(\case WitAny Elem f a a1
i Evident @@ a1
s -> Sing a1
Evident @@ a1
s Sing a1 -> (ElemSym1 f a @@ a1) -> Sigma v (ElemSym1 f a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: Elem f a a1
ElemSym1 f a @@ a1
i)
(\case Sing fst
s :&: ElemSym1 f a @@ fst
i -> Elem f a fst -> (Evident @@ fst) -> WitAny f Evident a
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f a fst
ElemSym1 f a @@ fst
i Sing fst
Evident @@ fst
s)
(Decision (WitAny f Evident a)
-> Decision (Sigma v (ElemSym1 f a)))
-> (Sing a -> Decision (WitAny f Evident a))
-> Sing a
-> Decision (Sigma v (ElemSym1 f a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: f v ~> *). Decidable p => Decide p
decide @(NotNull f)
instance Decidable (NotNull f ==> Found (InP f))
instance Provable (NotNull f ==> Found (InP f)) where
prove :: Prove (NotNull f ==> Found (InP f))
prove = Sing a -> Apply (NotNull f ==> Found (InP f)) a
Sing a -> (NotNull f @@ a) -> Found (InP f) @@ a
forall {k} (f :: * -> *) (a :: f k).
Sing a -> (NotNull f @@ a) -> Found (InP f) @@ a
notNullInP
instance Decidable (Found (InP f) ==> NotNull f)
instance Provable (Found (InP f) ==> NotNull f) where
prove :: Prove (Found (InP f) ==> NotNull f)
prove = Sing a -> Apply (Found (InP f) ==> NotNull f) a
Sing a -> (Found (InP f) @@ a) -> NotNull f @@ a
forall {v} (f :: * -> *) (a :: f v).
Sing a -> (Found (InP f) @@ a) -> NotNull f @@ a
inPNotNull
data AnyMatch f :: ParamPred k v -> ParamPred (f k) v
type instance Apply (AnyMatch f p as) a = Any f (FlipPP p a) @@ as
instance (Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p)) where
decide :: Decide (Found (AnyMatch f p))
decide =
(WitAny f (Found p) a -> Sigma v (AnyMatch f p a))
-> (Sigma v (AnyMatch f p a) -> WitAny f (Found p) a)
-> Decision (WitAny f (Found p) a)
-> Decision (Sigma v (AnyMatch f p a))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision
(\case WitAny Elem f a a1
i (Sing fst
x :&: p a1 @@ fst
p) -> Sing fst
x Sing fst -> (AnyMatch f p a @@ fst) -> Sigma v (AnyMatch f p a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: Elem f a a1 -> (FlipPP p fst @@ a1) -> WitAny f (FlipPP p fst) a
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f a a1
i FlipPP p fst @@ a1
p a1 @@ fst
p)
(\case Sing fst
x :&: WitAny Elem f a a1
i FlipPP p fst @@ a1
p -> Elem f a a1 -> (Found p @@ a1) -> WitAny f (Found p) a
forall {k} (f :: * -> *) (b :: f k) (a1 :: k) (a :: k ~> *).
Elem f b a1 -> (a @@ a1) -> WitAny f a b
WitAny Elem f a a1
i (Sing fst
x Sing fst -> (p a1 @@ fst) -> Sigma v (p a1)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: FlipPP p fst @@ a1
p a1 @@ fst
p))
(Decision (WitAny f (Found p) a)
-> Decision (Sigma v (AnyMatch f p a)))
-> (Sing a -> Decision (WitAny f (Found p) a))
-> Sing a
-> Decision (Sigma v (AnyMatch f p 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 (Found p))
data OrP :: ParamPred k v -> ParamPred k v -> ParamPred k v
type instance Apply (OrP p q x) y = (p x ||| q x) @@ y
data AndP :: ParamPred k v -> ParamPred k u -> ParamPred k (v, u)
type instance Apply (AndP p q x) '(y, z) = (p x @@ y, q x @@ z)
instance (Searchable p, Searchable q) => Decidable (Found (OrP p q)) where
decide :: Decide (Found (OrP p q))
decide Sing a
x = case forall {k1} {v} (p :: ParamPred k1 v).
Searchable p =>
Decide (Found p)
forall (p :: ParamPred k1 v). Searchable p => Decide (Found p)
search @p Sing a
x of
Proved (Sing fst
s :&: p a @@ fst
p) -> (Found (OrP p q) @@ a) -> Decision (Found (OrP p q) @@ a)
forall a. a -> Decision a
Proved ((Found (OrP p q) @@ a) -> Decision (Found (OrP p q) @@ a))
-> (Found (OrP p q) @@ a) -> Decision (Found (OrP p q) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing fst
s Sing fst -> (OrP p q a @@ fst) -> Sigma v (OrP p q a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: (p a @@ fst) -> Either (p a @@ fst) (Apply (q a) fst)
forall a b. a -> Either a b
Left p a @@ fst
p
Disproved Refuted (Found p @@ a)
vp -> case forall {k1} {v} (p :: ParamPred k1 v).
Searchable p =>
Decide (Found p)
forall (p :: ParamPred k1 v). Searchable p => Decide (Found p)
search @q Sing a
x of
Proved (Sing fst
s :&: q a @@ fst
q) -> (Found (OrP p q) @@ a) -> Decision (Found (OrP p q) @@ a)
forall a. a -> Decision a
Proved ((Found (OrP p q) @@ a) -> Decision (Found (OrP p q) @@ a))
-> (Found (OrP p q) @@ a) -> Decision (Found (OrP p q) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing fst
s Sing fst -> (OrP p q a @@ fst) -> Sigma v (OrP p q a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: (q a @@ fst) -> Either (Apply (p a) fst) (q a @@ fst)
forall a b. b -> Either a b
Right q a @@ fst
q
Disproved Refuted (Found q @@ a)
vq -> Refuted (Found (OrP p q) @@ a) -> Decision (Found (OrP p q) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Found (OrP p q) @@ a) -> Decision (Found (OrP p q) @@ a))
-> Refuted (Found (OrP p q) @@ a)
-> Decision (Found (OrP p q) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
Sing fst
s :&: Left Apply (p a) fst
p -> Refuted (Found p @@ a)
vp (Sing fst
s Sing fst -> Apply (p a) fst -> Sigma v (p a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: Apply (p a) fst
p)
Sing fst
s :&: Right Apply (q a) fst
q -> Refuted (Found q @@ a)
vq (Sing fst
s Sing fst -> Apply (q a) fst -> Sigma v (q a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: Apply (q a) fst
q)
instance (Searchable p, Searchable q) => Decidable (Found (AndP p q)) where
decide :: Decide (Found (AndP p q))
decide Sing a
x = case forall {k1} {v} (p :: ParamPred k1 v).
Searchable p =>
Decide (Found p)
forall (p :: ParamPred k1 v). Searchable p => Decide (Found p)
search @p Sing a
x of
Proved (Sing fst
s :&: p a @@ fst
p) -> case forall {k1} {v} (p :: ParamPred k1 v).
Searchable p =>
Decide (Found p)
forall (p :: ParamPred k1 u). Searchable p => Decide (Found p)
search @q Sing a
x of
Proved (Sing fst
t :&: q a @@ fst
q) -> (Found (AndP p q) @@ a) -> Decision (Found (AndP p q) @@ a)
forall a. a -> Decision a
Proved ((Found (AndP p q) @@ a) -> Decision (Found (AndP p q) @@ a))
-> (Found (AndP p q) @@ a) -> Decision (Found (AndP p q) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing fst -> Sing fst -> STuple2 '(fst, fst)
forall a b (n1 :: a) (n2 :: b).
Sing n1 -> Sing n2 -> STuple2 '(n1, n2)
STuple2 Sing fst
s Sing fst
t Sing '(fst, fst)
-> (AndP p q a @@ '(fst, fst)) -> Sigma (v, u) (AndP p q a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: (p a @@ fst
p, q a @@ fst
q)
Disproved Refuted (Found q @@ a)
vq -> Refuted (Found (AndP p q) @@ a) -> Decision (Found (AndP p q) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Found (AndP p q) @@ a)
-> Decision (Found (AndP p q) @@ a))
-> Refuted (Found (AndP p q) @@ a)
-> Decision (Found (AndP p q) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
STuple2 Sing n1
_ Sing n2
t :&: (Apply (p a) n1
_, Apply (q a) n2
q) -> Refuted (Found q @@ a)
vq Refuted (Found q @@ a) -> Refuted (Found q @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n2
t Sing n2 -> Apply (q a) n2 -> Sigma u (q a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: Apply (q a) n2
q
Disproved Refuted (Found p @@ a)
vp -> Refuted (Found (AndP p q) @@ a) -> Decision (Found (AndP p q) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Found (AndP p q) @@ a)
-> Decision (Found (AndP p q) @@ a))
-> Refuted (Found (AndP p q) @@ a)
-> Decision (Found (AndP p q) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
STuple2 Sing n1
s Sing n2
_ :&: (Apply (p a) n1
p, Apply (q a) n2
_) -> Refuted (Found p @@ a)
vp Refuted (Found p @@ a) -> Refuted (Found p @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n1
s Sing n1 -> Apply (p a) n1 -> Sigma v (p a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: Apply (p a) n1
p
instance (Selectable p, Selectable q) => Provable (Found (AndP p q)) where
prove :: Prove (Found (AndP p q))
prove Sing a
x = case forall {k1} {v} (p :: ParamPred k1 v).
Selectable p =>
Prove (Found p)
forall (p :: ParamPred k1 v). Selectable p => Prove (Found p)
select @p Sing a
x of
Sing fst
s :&: p a @@ fst
p -> case forall {k1} {v} (p :: ParamPred k1 v).
Selectable p =>
Prove (Found p)
forall (p :: ParamPred k1 u). Selectable p => Prove (Found p)
select @q Sing a
x of
Sing fst
t :&: q a @@ fst
q -> Sing fst -> Sing fst -> STuple2 '(fst, fst)
forall a b (n1 :: a) (n2 :: b).
Sing n1 -> Sing n2 -> STuple2 '(n1, n2)
STuple2 Sing fst
s Sing fst
t Sing '(fst, fst)
-> (AndP p q a @@ '(fst, fst)) -> Sigma (v, u) (AndP p q a)
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: (p a @@ fst
p, q a @@ fst
q)