{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Predicate (
Predicate,
Wit (..),
TyPred,
Evident,
EqualTo,
BoolPred,
Impossible,
In,
PMap,
type Not,
decideNot,
Prove,
type (-->),
type (-->#),
Provable (..),
Disprovable,
disprove,
ProvableTC,
proveTC,
TFunctor (..),
compImpl,
Decide,
type (-?>),
type (-?>#),
Decidable (..),
DecidableTC,
decideTC,
DFunctor (..),
Decision (..),
flipDecision,
mapDecision,
elimDisproof,
forgetDisproof,
forgetProof,
isProved,
isDisproved,
mapRefuted,
) where
import Data.Either.Singletons
import Data.Function.Singletons
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 (ElemSym1)
import Data.Maybe
import Data.Maybe.Singletons
import Data.Singletons
import Data.Singletons.Decide
import Data.Tuple.Singletons
import Data.Type.Functor.Product
import Data.Void
type Predicate k = k ~> Type
type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)
data Evident :: Predicate k
type instance Apply Evident a = Sing a
type Impossible = (Not Evident :: Predicate k)
type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)
type BoolPred (p :: k ~> Bool) = (PMap p (EqualTo 'True) :: Predicate k)
type PMap (f :: k ~> j) (p :: Predicate j) = (p .@#@$$$ f :: Predicate k)
newtype Wit p a = Wit {forall {k1} (p :: k1 ~> *) (a :: k1). Wit p a -> p @@ a
getWit :: p @@ a}
type Decide p = forall a. Sing a -> Decision (p @@ a)
type p -?> q = forall a. Sing a -> p @@ a -> Decision (q @@ a)
type (p -?># q) h = forall a. Sing a -> p @@ a -> h (Decision (q @@ a))
type Prove p = forall a. Sing a -> p @@ a
type p --> q = forall a. Sing a -> p @@ a -> q @@ a
type (p --># q) h = forall a. Sing a -> p @@ a -> h (q @@ a)
infixr 1 -?>
infixr 1 -?>#
infixr 1 -->
infixr 1 -->#
class Decidable p where
decide :: Decide p
default decide :: Provable p => Decide p
decide = Apply p a -> Decision (Apply p a)
forall a. a -> Decision a
Proved (Apply p a -> Decision (Apply p a))
-> (Sing a -> Apply p a) -> Sing a -> Decision (Apply p a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k1 ~> *). Provable p => Prove p
prove @p
class Provable p where
prove :: Prove p
type Disprovable p = Provable (Not p)
disprove :: forall p. Disprovable p => Prove (Not p)
disprove :: forall {k1} (p :: Predicate k1). Disprovable p => Prove (Not p)
disprove = forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k1 ~> *). Provable p => Prove p
prove @(Not p)
type DecidableTC p = Decidable (TyPred p)
decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)
decideTC :: forall {k1} (t :: k1 -> *) (a :: k1).
DecidableTC t =>
Sing a -> Decision (t a)
decideTC = forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k1 ~> *). Decidable p => Decide p
decide @(TyPred t)
type ProvableTC p = Provable (TyPred p)
proveTC :: forall t a. ProvableTC t => Sing a -> t a
proveTC :: forall {k1} (t :: k1 -> *) (a :: k1). ProvableTC t => Sing a -> t a
proveTC = forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k1 ~> *). Provable p => Prove p
prove @(TyPred t)
class DFunctor f where
dmap :: forall p q. (p -?> q) -> (f p -?> f q)
class TFunctor f where
tmap :: forall p q. (p --> q) -> (f p --> f q)
instance (SDecide k, SingI (a :: k)) => Decidable (EqualTo a) where
decide :: Decide (EqualTo a)
decide = (Sing a
forall {k} (a :: k). SingI a => Sing a
sing Sing a -> Sing a -> Decision (a :~: a)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~)
instance Decidable Evident
instance Provable Evident where
prove :: Prove Evident
prove = Sing a -> Sing a
Sing a -> Apply Evident a
forall a. a -> a
id
instance Decidable (TyPred WrappedSing)
instance Provable (TyPred WrappedSing) where
prove :: Prove (TyPred WrappedSing)
prove = Sing a -> Apply (TyPred WrappedSing) a
Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing
instance Provable p => Provable (TyPred (Rec (Wit p))) where
prove :: Prove (TyPred (Rec (Wit p)))
prove = (forall (a :: u). Sing a -> Wit p a)
-> Prod [] Sing a -> Prod [] (Wit p) a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: u ~> *). Provable p => Prove p
prove @p) (Prod [] Sing a -> Rec (Wit p) a)
-> (SList a -> Prod [] Sing a) -> SList a -> Rec (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod [] Sing a
SList a -> Prod [] Sing a
forall {k} (as :: [k]). Sing as -> Prod [] Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (Rec (Wit p))) where
decide :: Decide (TyPred (Rec (Wit p)))
decide = \case
Sing a
SList a
SNil -> Rec (Wit p) '[] -> Decision (Rec (Wit p) '[])
forall a. a -> Decision a
Proved Rec (Wit p) '[]
forall {u} (a :: u -> *). Rec a '[]
RNil
Sing n1
x `SCons` Sing n2
xs -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: u ~> *). Decidable p => Decide p
decide @p Sing n1
x of
Proved p @@ n1
p -> case Sing n2 -> Decision (Rec (Wit p) n2)
forall {k1} (t :: k1 -> *) (a :: k1).
DecidableTC t =>
Sing a -> Decision (t a)
decideTC Sing n2
xs of
Proved Rec (Wit p) n2
ps -> (TyPred (Rec (Wit p)) @@ a) -> Decision (TyPred (Rec (Wit p)) @@ a)
forall a. a -> Decision a
Proved ((TyPred (Rec (Wit p)) @@ a)
-> Decision (TyPred (Rec (Wit p)) @@ a))
-> (TyPred (Rec (Wit p)) @@ a)
-> Decision (TyPred (Rec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ (p @@ n1) -> Wit p n1
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit p @@ n1
p Wit p n1 -> Rec (Wit p) n2 -> Rec (Wit p) (n1 : n2)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec (Wit p) n2
ps
Disproved Refuted (Rec (Wit p) n2)
vs -> Refuted (TyPred (Rec (Wit p)) @@ a)
-> Decision (TyPred (Rec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (TyPred (Rec (Wit p)) @@ a)
-> Decision (TyPred (Rec (Wit p)) @@ a))
-> Refuted (TyPred (Rec (Wit p)) @@ a)
-> Decision (TyPred (Rec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
Wit p r
_ :& Rec (Wit p) rs
ps -> Refuted (Rec (Wit p) n2)
vs Rec (Wit p) n2
Rec (Wit p) rs
ps
Disproved Refuted (p @@ n1)
v -> Refuted (TyPred (Rec (Wit p)) @@ a)
-> Decision (TyPred (Rec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (TyPred (Rec (Wit p)) @@ a)
-> Decision (TyPred (Rec (Wit p)) @@ a))
-> Refuted (TyPred (Rec (Wit p)) @@ a)
-> Decision (TyPred (Rec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
Wit p @@ r
p :& Rec (Wit p) rs
_ -> Refuted (p @@ n1)
v p @@ n1
p @@ r
p
instance Provable (TyPred (Rec WrappedSing)) where
prove :: Prove (TyPred (Rec WrappedSing))
prove = (forall (a :: u). Sing a -> WrappedSing a)
-> Prod [] Sing a -> Prod [] WrappedSing a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd Sing a -> WrappedSing a
forall (a :: u). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (Prod [] Sing a -> Rec WrappedSing a)
-> (SList a -> Prod [] Sing a) -> SList a -> Rec WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod [] Sing a
SList a -> Prod [] Sing a
forall {k} (as :: [k]). Sing as -> Prod [] Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (Rec WrappedSing))
instance Provable p => Provable (TyPred (PMaybe (Wit p))) where
prove :: Prove (TyPred (PMaybe (Wit p)))
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod Maybe Sing a -> Prod Maybe (Wit p) a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k ~> *). Provable p => Prove p
prove @p) (Prod Maybe Sing a -> PMaybe (Wit p) a)
-> (SMaybe a -> Prod Maybe Sing a) -> SMaybe a -> PMaybe (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod Maybe Sing a
SMaybe a -> Prod Maybe Sing a
forall {k} (as :: Maybe k). Sing as -> Prod Maybe Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (PMaybe (Wit p))) where
decide :: Decide (TyPred (PMaybe (Wit p)))
decide = \case
Sing a
SMaybe a
SNothing -> PMaybe (Wit p) 'Nothing -> Decision (PMaybe (Wit p) 'Nothing)
forall a. a -> Decision a
Proved PMaybe (Wit p) 'Nothing
forall {k} (a :: k -> *). PMaybe a 'Nothing
PNothing
SJust Sing n
x ->
(Apply p n -> PMaybe (Wit p) ('Just n))
-> (PMaybe (Wit p) ('Just n) -> Apply p n)
-> Decision (Apply p n)
-> Decision (PMaybe (Wit p) ('Just n))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Wit p n -> PMaybe (Wit p) ('Just n)
forall {k} (a :: k -> *) (a1 :: k). a a1 -> PMaybe a ('Just a1)
PJust (Wit p n -> PMaybe (Wit p) ('Just n))
-> (Apply p n -> Wit p n) -> Apply p n -> PMaybe (Wit p) ('Just n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Apply p n -> Wit p n
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PJust (Wit p @@ a1
p) -> Apply p n
p @@ a1
p)
(Decision (Apply p n) -> Decision (TyPred (PMaybe (Wit p)) @@ a))
-> (Sing n -> Decision (Apply p n))
-> Sing n
-> Decision (TyPred (PMaybe (Wit p)) @@ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @p
(Sing n -> Decision (TyPred (PMaybe (Wit p)) @@ a))
-> Sing n -> Decision (TyPred (PMaybe (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n
x
instance Provable (TyPred (PMaybe WrappedSing)) where
prove :: Prove (TyPred (PMaybe WrappedSing))
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod Maybe Sing a -> Prod Maybe WrappedSing a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd Sing a -> WrappedSing a
forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (Prod Maybe Sing a -> PMaybe WrappedSing a)
-> (SMaybe a -> Prod Maybe Sing a)
-> SMaybe a
-> PMaybe WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod Maybe Sing a
SMaybe a -> Prod Maybe Sing a
forall {k} (as :: Maybe k). Sing as -> Prod Maybe Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (PMaybe WrappedSing))
instance Provable p => Provable (TyPred (NERec (Wit p))) where
prove :: Prove (TyPred (NERec (Wit p)))
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod NonEmpty Sing a -> Prod NonEmpty (Wit p) a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k ~> *). Provable p => Prove p
prove @p) (Prod NonEmpty Sing a -> NERec (Wit p) a)
-> (SNonEmpty a -> Prod NonEmpty Sing a)
-> SNonEmpty a
-> NERec (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod NonEmpty Sing a
SNonEmpty a -> Prod NonEmpty Sing a
forall {k} (as :: NonEmpty k). Sing as -> Prod NonEmpty Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (NERec (Wit p))) where
decide :: Decide (TyPred (NERec (Wit p)))
decide = \case
Sing n1
x NE.:%| Sing n2
xs -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @p Sing n1
x of
Proved p @@ n1
p -> case Sing n2 -> Decision (Rec (Wit p) n2)
forall {k1} (t :: k1 -> *) (a :: k1).
DecidableTC t =>
Sing a -> Decision (t a)
decideTC Sing n2
xs of
Proved Rec (Wit p) n2
ps -> (TyPred (NERec (Wit p)) @@ a)
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a. a -> Decision a
Proved ((TyPred (NERec (Wit p)) @@ a)
-> Decision (TyPred (NERec (Wit p)) @@ a))
-> (TyPred (NERec (Wit p)) @@ a)
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ (p @@ n1) -> Wit p n1
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit p @@ n1
p Wit p n1 -> Rec (Wit p) n2 -> NERec (Wit p) (n1 ':| n2)
forall {k} (a :: k -> *) (a1 :: k) (as :: [k]).
a a1 -> Rec a as -> NERec a (a1 ':| as)
:&| Rec (Wit p) n2
ps
Disproved Refuted (Rec (Wit p) n2)
vs -> Refuted (TyPred (NERec (Wit p)) @@ a)
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (TyPred (NERec (Wit p)) @@ a)
-> Decision (TyPred (NERec (Wit p)) @@ a))
-> Refuted (TyPred (NERec (Wit p)) @@ a)
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
Wit p a1
_ :&| Rec (Wit p) as
ps -> Refuted (Rec (Wit p) n2)
vs Rec (Wit p) n2
Rec (Wit p) as
ps
Disproved Refuted (p @@ n1)
v -> Refuted (TyPred (NERec (Wit p)) @@ a)
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (TyPred (NERec (Wit p)) @@ a)
-> Decision (TyPred (NERec (Wit p)) @@ a))
-> Refuted (TyPred (NERec (Wit p)) @@ a)
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
Wit p @@ a1
p :&| Rec (Wit p) as
_ -> Refuted (p @@ n1)
v p @@ n1
p @@ a1
p
instance Provable (TyPred (NERec WrappedSing)) where
prove :: Prove (TyPred (NERec WrappedSing))
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod NonEmpty Sing a -> Prod NonEmpty WrappedSing a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd Sing a -> WrappedSing a
forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (Prod NonEmpty Sing a -> NERec WrappedSing a)
-> (SNonEmpty a -> Prod NonEmpty Sing a)
-> SNonEmpty a
-> NERec WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod NonEmpty Sing a
SNonEmpty a -> Prod NonEmpty Sing a
forall {k} (as :: NonEmpty k). Sing as -> Prod NonEmpty Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (NERec WrappedSing))
instance Provable p => Provable (TyPred (PIdentity (Wit p))) where
prove :: Prove (TyPred (PIdentity (Wit p)))
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod Identity Sing a -> Prod Identity (Wit p) a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k ~> *). Provable p => Prove p
prove @p) (Prod Identity Sing a -> PIdentity (Wit p) a)
-> (SIdentity a -> Prod Identity Sing a)
-> SIdentity a
-> PIdentity (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod Identity Sing a
SIdentity a -> Prod Identity Sing a
forall {k} (as :: Identity k). Sing as -> Prod Identity Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (PIdentity (Wit p))) where
decide :: Decide (TyPred (PIdentity (Wit p)))
decide = \case
SIdentity Sing n
x ->
(Apply p n -> PIdentity (Wit p) ('Identity n))
-> (PIdentity (Wit p) ('Identity n) -> Apply p n)
-> Decision (Apply p n)
-> Decision (PIdentity (Wit p) ('Identity n))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Wit p n -> PIdentity (Wit p) ('Identity n)
forall {k} (a :: k -> *) (a1 :: k).
a a1 -> PIdentity a ('Identity a1)
PIdentity (Wit p n -> PIdentity (Wit p) ('Identity n))
-> (Apply p n -> Wit p n)
-> Apply p n
-> PIdentity (Wit p) ('Identity n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Apply p n -> Wit p n
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PIdentity (Wit p @@ a1
p) -> Apply p n
p @@ a1
p)
(Decision (Apply p n)
-> Decision (TyPred (PIdentity (Wit p)) @@ a))
-> (Sing n -> Decision (Apply p n))
-> Sing n
-> Decision (TyPred (PIdentity (Wit p)) @@ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @p
(Sing n -> Decision (TyPred (PIdentity (Wit p)) @@ a))
-> Sing n -> Decision (TyPred (PIdentity (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n
x
instance Provable (TyPred (PIdentity WrappedSing)) where
prove :: Prove (TyPred (PIdentity WrappedSing))
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod Identity Sing a -> Prod Identity WrappedSing a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd Sing a -> WrappedSing a
forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (Prod Identity Sing a -> PIdentity WrappedSing a)
-> (SIdentity a -> Prod Identity Sing a)
-> SIdentity a
-> PIdentity WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod Identity Sing a
SIdentity a -> Prod Identity Sing a
forall {k} (as :: Identity k). Sing as -> Prod Identity Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (PIdentity WrappedSing))
instance Provable p => Provable (TyPred (PEither (Wit p))) where
prove :: Prove (TyPred (PEither (Wit p)))
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod (Either j) Sing a -> Prod (Either j) (Wit p) a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k ~> *). Provable p => Prove p
prove @p) (Prod (Either j) Sing a -> PEither (Wit p) a)
-> (SEither a -> Prod (Either j) Sing a)
-> SEither a
-> PEither (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod (Either j) Sing a
SEither a -> Prod (Either j) Sing a
forall {k} (as :: Either j k). Sing as -> Prod (Either j) Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (PEither (Wit p))) where
decide :: Decide (TyPred (PEither (Wit p)))
decide = \case
SLeft Sing n
x -> (TyPred (PEither (Wit p)) @@ a)
-> Decision (TyPred (PEither (Wit p)) @@ a)
forall a. a -> Decision a
Proved ((TyPred (PEither (Wit p)) @@ a)
-> Decision (TyPred (PEither (Wit p)) @@ a))
-> (TyPred (PEither (Wit p)) @@ a)
-> Decision (TyPred (PEither (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n -> PEither (Wit p) ('Left n)
forall {j} {k} (e :: j) (a :: k -> *).
Sing e -> PEither a ('Left e)
PLeft Sing n
x
SRight Sing n
y ->
(Apply p n -> PEither (Wit p) ('Right n))
-> (PEither (Wit p) ('Right n) -> Apply p n)
-> Decision (Apply p n)
-> Decision (PEither (Wit p) ('Right n))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Wit p n -> PEither (Wit p) ('Right n)
forall {k} {j} (a :: k -> *) (a1 :: k).
a a1 -> PEither a ('Right a1)
PRight (Wit p n -> PEither (Wit p) ('Right n))
-> (Apply p n -> Wit p n)
-> Apply p n
-> PEither (Wit p) ('Right n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Apply p n -> Wit p n
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PRight (Wit p @@ a1
p) -> Apply p n
p @@ a1
p)
(Decision (Apply p n) -> Decision (TyPred (PEither (Wit p)) @@ a))
-> (Sing n -> Decision (Apply p n))
-> Sing n
-> Decision (TyPred (PEither (Wit p)) @@ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @p
(Sing n -> Decision (TyPred (PEither (Wit p)) @@ a))
-> Sing n -> Decision (TyPred (PEither (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n
y
instance Provable (TyPred (PEither WrappedSing)) where
prove :: Prove (TyPred (PEither WrappedSing))
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod (Either j) Sing a -> Prod (Either j) WrappedSing a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd Sing a -> WrappedSing a
forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (Prod (Either j) Sing a -> PEither WrappedSing a)
-> (SEither a -> Prod (Either j) Sing a)
-> SEither a
-> PEither WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod (Either j) Sing a
SEither a -> Prod (Either j) Sing a
forall {k} (as :: Either j k). Sing as -> Prod (Either j) Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (PEither WrappedSing))
instance Provable p => Provable (TyPred (PTup (Wit p))) where
prove :: Prove (TyPred (PTup (Wit p)))
prove = (forall (a :: k). Sing a -> Wit p a)
-> Prod ((,) j) Sing a -> Prod ((,) j) (Wit p) a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd ((p @@ a) -> Wit p a
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit ((p @@ a) -> Wit p a) -> (Sing a -> p @@ a) -> Sing a -> Wit p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: k ~> *). Provable p => Prove p
prove @p) (Prod ((,) j) Sing a -> PTup (Wit p) a)
-> (STuple2 a -> Prod ((,) j) Sing a)
-> STuple2 a
-> PTup (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod ((,) j) Sing a
STuple2 a -> Prod ((,) j) Sing a
forall {k} (as :: (j, k)). Sing as -> Prod ((,) j) Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable p => Decidable (TyPred (PTup (Wit p))) where
decide :: Decide (TyPred (PTup (Wit p)))
decide (STuple2 Sing n1
x Sing n2
y) =
(Apply p n2 -> PTup (Wit p) '(n1, n2))
-> (PTup (Wit p) '(n1, n2) -> Apply p n2)
-> Decision (Apply p n2)
-> Decision (PTup (Wit p) '(n1, n2))
forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (Sing n1 -> Wit p n2 -> PTup (Wit p) '(n1, n2)
forall {j} {k} (w :: j) (a :: k -> *) (a1 :: k).
Sing w -> a a1 -> PTup a '(w, a1)
PTup Sing n1
x (Wit p n2 -> PTup (Wit p) '(n1, n2))
-> (Apply p n2 -> Wit p n2) -> Apply p n2 -> PTup (Wit p) '(n1, n2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Apply p n2 -> Wit p n2
forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PTup Sing w
_ (Wit p @@ a1
p) -> Apply p n2
p @@ a1
p)
(Decision (Apply p n2)
-> Decision (Apply (TyPred (PTup (Wit p))) a))
-> (Sing n2 -> Decision (Apply p n2))
-> Sing n2
-> Decision (Apply (TyPred (PTup (Wit p))) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @p
(Sing n2 -> Decision (Apply (TyPred (PTup (Wit p))) a))
-> Sing n2 -> Decision (Apply (TyPred (PTup (Wit p))) a)
forall a b. (a -> b) -> a -> b
$ Sing n2
y
instance Provable (TyPred (PTup WrappedSing)) where
prove :: Prove (TyPred (PTup WrappedSing))
prove = (forall (a :: k). Sing a -> WrappedSing a)
-> Prod ((,) j) Sing a -> Prod ((,) j) WrappedSing a
forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd Sing a -> WrappedSing a
forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (Prod ((,) j) Sing a -> PTup WrappedSing a)
-> (STuple2 a -> Prod ((,) j) Sing a)
-> STuple2 a
-> PTup WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Prod ((,) j) Sing a
STuple2 a -> Prod ((,) j) Sing a
forall {k} (as :: (j, k)). Sing as -> Prod ((,) j) Sing as
forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
instance Decidable (TyPred (PTup WrappedSing))
instance (Decidable p, SingI f) => Decidable (PMap f p) where
decide :: Decide (PMap f p)
decide = forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: j ~> *). Decidable p => Decide p
decide @p (Sing (Apply f a) -> Decision (p @@ Apply f a))
-> (Sing a -> Sing (Apply f a))
-> Sing a
-> Decision (p @@ Apply f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SLambda f -> forall (t :: k1). 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 p, SingI f) => Provable (PMap f p) where
prove :: Prove (PMap f p)
prove = forall {k1} (p :: k1 ~> *). Provable p => Prove p
forall (p :: j ~> *). Provable p => Prove p
prove @p (Sing (Apply f a) -> p @@ Apply f a)
-> (Sing a -> Sing (Apply f a)) -> Sing a -> p @@ Apply f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SLambda f -> forall (t :: k1). 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)
compImpl ::
forall p q r.
() =>
p --> q ->
q --> r ->
p --> r
compImpl :: forall {k1} (p :: k1 ~> *) (q :: k1 ~> *) (r :: k1 ~> *).
(p --> q) -> (q --> r) -> p --> r
compImpl p --> q
f q --> r
g Sing a
s = Sing a -> Apply q a -> Apply r a
q --> r
g Sing a
s (Apply q a -> Apply r a)
-> (Apply p a -> Apply q a) -> Apply p a -> Apply r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Apply p a -> Apply q a
p --> q
f Sing a
s
data Not :: Predicate k -> Predicate k
type instance Apply (Not p) a = Refuted (p @@ a)
instance Decidable p => Decidable (Not p) where
decide :: Decide (Not p)
decide (Sing a
x :: Sing a) = forall {k1} (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
forall (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
decideNot @p @a (forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing a
x)
instance Provable (Not Impossible) where
prove :: Prove (Not Impossible)
prove Sing a
x Sing a -> Void
v = Void -> Void
forall a. Void -> a
absurd (Void -> Void) -> Void -> Void
forall a b. (a -> b) -> a -> b
$ Sing a -> Void
v Sing a
x
decideNot ::
forall p a.
() =>
Decision (p @@ a) ->
Decision (Not p @@ a)
decideNot :: forall {k1} (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
decideNot = Decision (Apply p a) -> Decision (Apply (Not p) a)
Decision (Apply p a) -> Decision (Refuted (Apply p a))
forall a. Decision a -> Decision (Refuted a)
flipDecision
flipDecision ::
Decision a ->
Decision (Refuted a)
flipDecision :: forall a. Decision a -> Decision (Refuted a)
flipDecision = \case
Proved a
p -> Refuted (Refuted a) -> Decision (Refuted a)
forall a. Refuted a -> Decision a
Disproved (Refuted a -> Refuted a
forall a b. (a -> b) -> a -> b
$ a
p)
Disproved Refuted a
v -> Refuted a -> Decision (Refuted a)
forall a. a -> Decision a
Proved Refuted a
v
mapDecision ::
(a -> b) ->
(b -> a) ->
Decision a ->
Decision b
mapDecision :: forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision a -> b
f b -> a
g = \case
Proved a
p -> b -> Decision b
forall a. a -> Decision a
Proved (b -> Decision b) -> b -> Decision b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
p
Disproved Refuted a
v -> Refuted b -> Decision b
forall a. Refuted a -> Decision a
Disproved (Refuted b -> Decision b) -> Refuted b -> Decision b
forall a b. (a -> b) -> a -> b
$ (b -> a) -> Refuted a -> Refuted b
forall a b. (a -> b) -> Refuted b -> Refuted a
mapRefuted b -> a
g Refuted a
v
forgetDisproof ::
Decision a ->
Maybe a
forgetDisproof :: forall a. Decision a -> Maybe a
forgetDisproof = \case
Proved a
p -> a -> Maybe a
forall a. a -> Maybe a
Just a
p
Disproved Refuted a
_ -> Maybe a
forall a. Maybe a
Nothing
forgetProof ::
Decision a ->
Maybe (Refuted a)
forgetProof :: forall a. Decision a -> Maybe (Refuted a)
forgetProof = Decision (Refuted a) -> Maybe (Refuted a)
forall a. Decision a -> Maybe a
forgetDisproof (Decision (Refuted a) -> Maybe (Refuted a))
-> (Decision a -> Decision (Refuted a))
-> Decision a
-> Maybe (Refuted a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decision a -> Decision (Refuted a)
forall a. Decision a -> Decision (Refuted a)
flipDecision
isProved :: Decision a -> Bool
isProved :: forall a. Decision a -> Bool
isProved = Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (Maybe a -> Bool) -> (Decision a -> Maybe a) -> Decision a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decision a -> Maybe a
forall a. Decision a -> Maybe a
forgetDisproof
isDisproved :: Decision a -> Bool
isDisproved :: forall a. Decision a -> Bool
isDisproved = Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe a -> Bool) -> (Decision a -> Maybe a) -> Decision a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decision a -> Maybe a
forall a. Decision a -> Maybe a
forgetDisproof
elimDisproof ::
Decision a ->
Refuted (Refuted a) ->
a
elimDisproof :: forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof = \case
Proved a
p -> a -> Refuted (Refuted a) -> a
forall a b. a -> b -> a
const a
p
Disproved Refuted a
v -> Void -> a
forall a. Void -> a
absurd (Void -> a)
-> (Refuted (Refuted a) -> Void) -> Refuted (Refuted a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Refuted (Refuted a) -> Refuted (Refuted a)
forall a b. (a -> b) -> a -> b
$ Refuted a
v)
mapRefuted ::
(a -> b) ->
Refuted b ->
Refuted a
mapRefuted :: forall a b. (a -> b) -> Refuted b -> Refuted a
mapRefuted = (Refuted b -> (a -> b) -> Refuted a)
-> (a -> b) -> Refuted b -> Refuted a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Refuted b -> (a -> b) -> Refuted a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
instance (SDecide k, SingI (as :: [k])) => Decidable (In [] as) where
decide :: forall a. Sing a -> Decision (Index as a)
decide :: forall (a :: k). Sing a -> Decision (Index as a)
decide Sing a
x = Sing as -> Decision (Index as a)
forall (bs :: [k]). Sing bs -> Decision (Index bs a)
go (forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as)
where
go :: Sing bs -> Decision (Index bs a)
go :: forall (bs :: [k]). Sing bs -> Decision (Index bs a)
go = \case
Sing bs
SList bs
SNil -> Refuted (Index bs a) -> Decision (Index bs a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Index bs a) -> Decision (Index bs a))
-> Refuted (Index bs a) -> Decision (Index bs a)
forall a b. (a -> b) -> a -> b
$ \case {}
Sing n1
y `SCons` Sing n2
ys -> case Sing a
x Sing a -> Sing n1 -> Decision (a :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
Proved a :~: n1
Refl -> Index bs a -> Decision (Index bs a)
forall a. a -> Decision a
Proved Index bs a
Index (a : n2) a
forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
Disproved Refuted (a :~: n1)
v -> case Sing n2 -> Decision (Index n2 a)
forall (bs :: [k]). Sing bs -> Decision (Index bs a)
go Sing n2
ys of
Proved Index n2 a
i -> Index bs a -> Decision (Index bs a)
forall a. a -> Decision a
Proved (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
i)
Disproved Refuted (Index n2 a)
u -> Refuted (Index bs a) -> Decision (Index bs a)
forall a. Refuted a -> Decision a
Disproved (Refuted (Index bs a) -> Decision (Index bs a))
-> Refuted (Index bs a) -> Decision (Index bs a)
forall a b. (a -> b) -> a -> b
$ \case
Index bs a
IZ -> Refuted (a :~: n1)
v a :~: a
a :~: n1
forall {k} (a :: k). a :~: a
Refl
IS Index bs a
i -> Refuted (Index n2 a)
u Index n2 a
Index bs a
i
instance (SDecide k, SingI (as :: Maybe k)) => Decidable (In Maybe as) where
decide :: Decide (In Maybe as)
decide Sing a
x = case forall (a :: Maybe k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
Sing as
SMaybe as
SNothing -> Refuted (In Maybe as @@ a) -> Decision (In Maybe as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (In Maybe as @@ a) -> Decision (In Maybe as @@ a))
-> Refuted (In Maybe as @@ a) -> Decision (In Maybe as @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
SJust Sing n
y -> case Sing a
x Sing a -> Sing n -> Decision (a :~: n)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
Proved a :~: n
Refl -> IJust ('Just a) a -> Decision (IJust ('Just a) a)
forall a. a -> Decision a
Proved IJust ('Just a) a
forall {k} (b :: k). IJust ('Just b) b
IJust
Disproved Refuted (a :~: n)
v -> Refuted (In Maybe as @@ a) -> Decision (In Maybe as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (In Maybe as @@ a) -> Decision (In Maybe as @@ a))
-> Refuted (In Maybe as @@ a) -> Decision (In Maybe as @@ a)
forall a b. (a -> b) -> a -> b
$ \case IJust ('Just n) a
In Maybe as @@ a
IJust -> Refuted (a :~: n)
v a :~: a
a :~: n
forall {k} (a :: k). a :~: a
Refl
instance (SDecide k, SingI (as :: Either j k)) => Decidable (In (Either j) as) where
decide :: Decide (In (Either j) as)
decide Sing a
x = case forall (a :: Either j k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
SLeft Sing n
_ -> Refuted (In (Either j) as @@ a) -> Decision (In (Either j) as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (In (Either j) as @@ a)
-> Decision (In (Either j) as @@ a))
-> Refuted (In (Either j) as @@ a)
-> Decision (In (Either j) as @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
SRight Sing n
y -> case Sing a
x Sing a -> Sing n -> Decision (a :~: n)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
Proved a :~: n
Refl -> IRight ('Right a) a -> Decision (IRight ('Right a) a)
forall a. a -> Decision a
Proved IRight ('Right a) a
forall {k} {j} (b :: k). IRight ('Right b) b
IRight
Disproved Refuted (a :~: n)
v -> Refuted (In (Either j) as @@ a) -> Decision (In (Either j) as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (In (Either j) as @@ a)
-> Decision (In (Either j) as @@ a))
-> Refuted (In (Either j) as @@ a)
-> Decision (In (Either j) as @@ a)
forall a b. (a -> b) -> a -> b
$ \case IRight ('Right n) a
In (Either j) as @@ a
IRight -> Refuted (a :~: n)
v a :~: a
a :~: n
forall {k} (a :: k). a :~: a
Refl
instance (SDecide k, SingI (as :: NonEmpty k)) => Decidable (In NonEmpty as) where
decide :: Decide (In NonEmpty as)
decide Sing a
x = case forall (a :: NonEmpty k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @as of
Sing n1
y NE.:%| (Sing n2
Sing :: Sing bs) -> case Sing a
x Sing a -> Sing n1 -> Decision (a :~: n1)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
Proved a :~: n1
Refl -> NEIndex (a ':| n2) a -> Decision (NEIndex (a ':| n2) a)
forall a. a -> Decision a
Proved NEIndex (a ':| n2) a
forall {k} (b :: k) (as :: [k]). NEIndex (b ':| as) b
NEHead
Disproved Refuted (a :~: n1)
v -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
forall (p :: k ~> *). Decidable p => Decide p
decide @(In [] bs) Sing a
x of
Proved In [] n2 @@ a
i -> (In NonEmpty as @@ a) -> Decision (In NonEmpty as @@ a)
forall a. a -> Decision a
Proved ((In NonEmpty as @@ a) -> Decision (In NonEmpty as @@ a))
-> (In NonEmpty as @@ a) -> Decision (In NonEmpty as @@ a)
forall a b. (a -> b) -> a -> b
$ 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
In [] n2 @@ a
i
Disproved Refuted (In [] n2 @@ a)
u -> Refuted (In NonEmpty as @@ a) -> Decision (In NonEmpty as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (In NonEmpty as @@ a) -> Decision (In NonEmpty as @@ a))
-> Refuted (In NonEmpty as @@ a) -> Decision (In NonEmpty as @@ a)
forall a b. (a -> b) -> a -> b
$ \case
NEIndex (n1 ':| n2) a
In NonEmpty as @@ a
NEHead -> Refuted (a :~: n1)
v a :~: a
a :~: n1
forall {k} (a :: k). a :~: a
Refl
NETail Index as a
i -> Refuted (In [] n2 @@ a)
u Index as a
In [] n2 @@ a
i
instance (SDecide k, SingI (as :: (j, k))) => Decidable (In ((,) j) as) where
decide :: Decide (In ((,) j) as)
decide Sing a
x = case forall {k} (a :: k). SingI a => Sing a
forall (a :: (j, k)). SingI a => Sing a
sing @as of
STuple2 Sing n1
_ Sing n2
y -> case Sing a
x Sing a -> Sing n2 -> Decision (a :~: n2)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n2
y of
Proved a :~: n2
Refl -> ISnd '(n1, a) a -> Decision (ISnd '(n1, a) a)
forall a. a -> Decision a
Proved ISnd '(n1, a) a
forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd
Disproved Refuted (a :~: n2)
v -> Refuted (In ((,) j) as @@ a) -> Decision (In ((,) j) as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (In ((,) j) as @@ a) -> Decision (In ((,) j) as @@ a))
-> Refuted (In ((,) j) as @@ a) -> Decision (In ((,) j) as @@ a)
forall a b. (a -> b) -> a -> b
$ \case ISnd '(n1, n2) a
In ((,) j) as @@ a
ISnd -> Refuted (a :~: n2)
v a :~: a
a :~: n2
forall {k} (a :: k). a :~: a
Refl
instance (SDecide k, SingI (as :: Identity k)) => Decidable (In Identity as) where
decide :: Decide (In Identity as)
decide Sing a
x = case forall {k} (a :: k). SingI a => Sing a
forall (a :: Identity k). SingI a => Sing a
sing @as of
SIdentity Sing n
y -> case Sing a
x Sing a -> Sing n -> Decision (a :~: n)
forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
Proved a :~: n
Refl -> IIdentity ('Identity a) a -> Decision (IIdentity ('Identity a) a)
forall a. a -> Decision a
Proved IIdentity ('Identity a) a
forall {k} (b :: k). IIdentity ('Identity b) b
IId
Disproved Refuted (a :~: n)
v -> Refuted (In Identity as @@ a) -> Decision (In Identity as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (In Identity as @@ a) -> Decision (In Identity as @@ a))
-> Refuted (In Identity as @@ a) -> Decision (In Identity as @@ a)
forall a b. (a -> b) -> a -> b
$ \case IIdentity ('Identity n) a
In Identity as @@ a
IId -> Refuted (a :~: n)
v a :~: a
a :~: n
forall {k} (a :: k). a :~: a
Refl