{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DefaultSignatures   #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE InstanceSigs        #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeInType          #-}
{-# LANGUAGE TypeOperators       #-}

-- |
-- Module      : Data.Type.Predicate
-- Copyright   : (c) Justin Le 2018
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Combinators for working with type-level predicates, along with
-- typeclasses for canonical proofs and deciding functions.
--
module Data.Type.Predicate (
    -- * Predicates
    Predicate, Wit(..)
    -- ** Construct Predicates
  , TyPred, Evident, EqualTo, BoolPred, Impossible, In
    -- ** Manipulate predicates
  , PMap, type Not, decideNot
    -- * Provable Predicates
  , Prove, type (-->), type (-->#)
  , Provable(..)
  , Disprovable, disprove
  , ProvableTC, proveTC
  , TFunctor(..)
  , compImpl
    -- * Decidable Predicates
  , Decide, type (-?>), type (-?>#)
  , Decidable(..)
  , DecidableTC, decideTC
  , DFunctor(..)
  -- * Manipulate Decisions
  , 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           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
import qualified Data.List.NonEmpty.Singletons    as NE

-- | A type-level predicate in Haskell.  We say that the predicate @P ::
-- 'Predicate' k@ is true/satisfied by input @x :: k@ if there exists
-- a value of type @P \@\@ x@, and that it false/disproved if such a value
-- cannot exist. (Where '@@' is 'Apply', the singleton library's type-level
-- function application for mathcable functions).  In some contexts, this
-- is also known as a dependently typed "view".
--
-- See 'Provable' and 'Decidable' for more information on how to use, prove
-- and decide these predicates.
--
-- The kind @k ~> 'Type'@ is the kind of "matchable" type-level functions
-- in Haskell.  They are type-level functions that are encoded as dummy
-- type constructors ("defunctionalization symbols") that can be decidedly
-- "matched" on for things like typeclass instances.
--
-- There are two ways to define your own predicates:
--
--     1. Using the predicate combinators and predicate transformers in
--     this library and the /singletons/ library, which let you construct
--     pre-made predicates and sometimes create predicates from other
--     predicates.
--
--     2. Manually creating a data type that acts as a matchable predicate.
--
-- For an example of the latter, we can create the "not p" predicate, which
-- takes a predicate @p@ as input and returns the negation of the
-- predicate:
--
-- @
-- -- First, create the data type with the kind signature you want
-- data Not :: Predicate k -> Predicate k
--
-- -- Then, write the 'Apply' instance, to specify the type of the
-- -- witnesses of that predicate
-- instance 'Apply' (Not p) a = (p '@@' a) -> 'Void'
-- @
--
-- See the source of "Data.Type.Predicate" and "Data.Type.Predicate.Logic"
-- for simple examples of hand-made predicates.  For example, we have the
-- always-true predicate 'Evident':
--
-- @
-- data Evident :: 'Predicate' k
-- instance Apply Evident a = 'Sing' a
-- @
--
-- And the "and" predicate combinator:
--
-- @
-- data (&&&) :: Predicate k -> Predicate k -> Predicate k
-- instance Apply (p &&& q) a = (p '@@' a, q '@@' a)
-- @
--
-- Typically it is recommended to create predicates from the supplied
-- predicate combinators ('TyPred' can be used for any type constructor to
-- turn it into a predicate, for instance) whenever possible.
type Predicate k = k ~> Type

-- | Convert a normal '->' type constructor into a 'Predicate'.
--
-- @
-- 'TyPred' :: (k -> 'Type') -> 'Predicate' k
-- @
type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)

-- | The always-true predicate.
--
-- @
-- 'Evident' :: 'Predicate' k
-- @
data Evident :: Predicate k
type instance Apply Evident a = Sing a

-- | The always-false predicate
--
-- Could also be defined as @'ConstSym1' Void@, but this defintion gives
-- us a free 'Decidable' instance.
--
-- @
-- 'Impossible' :: 'Predicate' k
-- @
type Impossible = (Not Evident :: Predicate k)

-- | @'EqualTo' a@ is a predicate that the input is equal to @a@.
--
-- @
-- 'EqualTo' :: k -> 'Predicate' k
-- @
type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)

-- | Convert a tradtional @k ~> 'Bool'@ predicate into a 'Predicate'.
--
-- @
-- 'BoolPred' :: (k ~> Bool) -> Predicate k
-- @
type BoolPred (p :: k ~> Bool) = (PMap p (EqualTo 'True) :: Predicate k)

-- | Pre-compose a function to a predicate
--
-- @
-- 'PMap' :: (k ~> j) -> 'Predicate' j -> Predicate k
-- @
type PMap (f :: k ~> j) (p :: Predicate j) = (p .@#@$$$ f :: Predicate k)

-- | A @'Wit' p a@ is a value of type @p \@\@ a@ --- that is, it is a proof
-- or witness that @p@ is satisfied for @a@.
--
-- It essentially turns a @k ~> 'Type'@ ("matchable" @'Predicate' k@) /back
-- into/ a @k -> 'Type'@ predicate.
newtype Wit p a = Wit { forall {k1} (p :: k1 ~> *) (a :: k1). Wit p a -> p @@ a
getWit :: p @@ a }

-- | A decision function for predicate @p@.  See 'Decidable' for more
-- information.
type Decide p = forall a. Sing a -> Decision (p @@ a)

-- | Like implication '-->', but knowing @p \@\@ a@ can only let us decidably
-- prove @q @@ a@ is true or false.
type p -?> q = forall a. Sing a -> p @@ a -> Decision (q @@ a)

-- | Like '-?>', but only in a specific context @h@.
type (p -?># q) h = forall a. Sing a -> p @@ a -> h (Decision (q @@ a))

-- | A proving function for predicate @p@; in some contexts, also called
-- a "view function".  See 'Provable' for more information.
type Prove p = forall a. Sing a -> p @@ a

-- | We say that @p@ implies @q@ (@p '-->' q@) if, given @p @@ a@, we can
-- always prove @q \@\@ a@.
type p --> q = forall a. Sing a -> p @@ a -> q @@ a

-- | This is implication '-->#', but only in a specific context @h@.
type (p --># q) h = forall a. Sing a -> p @@ a -> h (q @@ a)

infixr 1 -?>
infixr 1 -?>#
infixr 1 -->
infixr 1 -->#

-- | A typeclass for decidable predicates.
--
-- A predicate is decidable if, given any input @a@, you can either prove
-- or disprove @p \@\@ a@.  A @'Decision' (p \@\@ a)@ is a data type
-- that has a branch @p \@\@ a@ and @'Refuted' (p \@\@ a)@.
--
-- This typeclass associates a canonical decision function for every
-- decidable predicate.
--
-- It confers two main advatnages:
--
--     1. The decision function for every predicate is available via the
--     same name
--
--     2. We can write 'Decidable' instances for polymorphic predicate
--     transformers (predicates parameterized on other predicates) easily,
--     by refering to 'Decidable' instances of the transformed predicates.
class Decidable p where
    -- | The canonical decision function for predicate @p@.
    --
    -- Note that 'decide' is ambiguously typed, so you /always/ need to call by
    -- specifying the predicate you want to prove using TypeApplications
    -- syntax:
    --
    -- @
    -- 'decide' \@MyPredicate
    -- @
    --
    -- See 'decideTC' and 'DecidableTC' for a version that isn't ambiguously
    -- typed, but only works when @p@ is a type constructor.
    decide :: Decide p

    default decide :: Provable p => Decide p
    decide = forall a. a -> Decision a
Proved forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @p

-- | A typeclass for provable predicates (constructivist tautologies).  In
-- some context, these are also known as "views".
--
-- A predicate is provable if, given any input @a@, you can generate
-- a proof of @p \@\@ a@.  Essentially, it means that a predicate is "always
-- true".
--
-- We can call a type a view if, for any input @a@, there is /some/
-- constructor of @p \@\@ a@ that can we can use to "categorize" @a@.
--
-- This typeclass associates a canonical proof function for every provable
-- predicate, or a canonical view function for any view.
--
-- It confers two main advatnages:
--
--     1. The proof function/view for every predicate/view is available via
--     the same name
--
--     2. We can write 'Provable' instances for polymorphic predicate
--     transformers (predicates parameterized on other predicates) easily,
--     by refering to 'Provable' instances of the transformed predicates.
class Provable p where
    -- | The canonical proving function for predicate @p@ (or a canonical
    -- view function for view @p@).
    --
    -- Note that 'prove' is ambiguously typed, so you /always/ need to call
    -- by specifying the predicate you want to prove using TypeApplications
    -- syntax:
    --
    -- @
    -- 'prove' \@MyPredicate
    -- @
    --
    -- See 'proveTC' and 'ProvableTC' for a version that isn't ambiguously
    -- typed, but only works when @p@ is a type constructor.
    prove :: Prove p

-- | @'Disprovable' p@ is a constraint that @p@ can be disproven.
type Disprovable p = Provable (Not p)

-- | The deciding/disproving function for @'Disprovable' p@.
--
-- Must be called by applying the 'Predicate' to disprove:
--
-- @
-- 'disprove' \@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
prove @(Not p)

-- | If @T :: k -> 'Type'@ is a type constructor, then @'DecidableTC' T@ is
-- a constraint that @T@ is "decidable", in that you have a canonical
-- function:
--
-- @
-- 'decideTC' :: 'Sing' a -> 'Decision' (T a)
-- @
--
-- Is essentially 'Decidable', except with /type constructors/ @k ->
-- 'Type'@ instead of matchable type-level functions (that are @k ~>
-- 'Type'@).  Useful because 'decideTC' doesn't require anything fancy like
-- TypeApplications to use.
--
-- Also is in this library for compatiblity with "traditional" predicates
-- that are GADT type constructors.
--
-- @since 0.1.1.0
type DecidableTC p = Decidable (TyPred p)

-- | The canonical deciding function for @'DecidableTC' t@.
--
-- Note that because @t@ must be an injective type constructor, you can use
-- this without explicit type applications; the instance of 'DecidableTC'
-- can be inferred from the result type.
--
-- @since 0.1.1.0
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
decide @(TyPred t)

-- | If @T :: k -> 'Type'@ is a type constructor, then @'ProvableTC' T@ is
-- a constraint that @T@ is "decidable", in that you have a canonical
-- function:
--
-- @
-- 'proveTC' :: 'Sing' a -> T a
-- @
--
-- Is essentially 'Provable', except with /type constructors/ @k -> 'Type'@
-- instead of matchable type-level functions (that are @k ~> 'Type'@).
-- Useful because 'proveTC' doesn't require anything fancy like
-- TypeApplications to use.
--
-- Also is in this library for compatiblity with "traditional" predicates
-- that are GADT type constructors.
--
-- @since 0.1.1.0
type ProvableTC  p = Provable  (TyPred p)

-- | The canonical proving function for @'DecidableTC' t@.
--
-- Note that because @t@ must be an injective type constructor, you can use
-- this without explicit type applications; the instance of 'ProvableTC'
-- can be inferred from the result type.
--
-- @since 0.1.1.0
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
prove @(TyPred t)

-- | Implicatons @p '-?>' q@ can be lifted "through" a 'DFunctor' into an
-- @f p '-?>' f q@.
class DFunctor f where
    dmap :: forall p q. (p -?> q) -> (f p -?> f q)

-- | Implicatons @p '-->' q@ can be lifted "through" a 'TFunctor' into an
-- @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 = (forall {k} (a :: k). SingI a => Sing a
sing 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 = forall a. a -> a
id

-- | @since 3.0.0
instance Decidable (TyPred WrappedSing)
-- | @since 3.0.0
instance Provable (TyPred WrappedSing) where
    prove :: Prove (TyPred WrappedSing)
prove = forall k (a :: k). Sing a -> WrappedSing a
WrapSing


-- | @since 3.0.0
instance Provable p => Provable (TyPred (Rec (Wit p))) where
    prove :: Prove (TyPred (Rec (Wit p)))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable p => Decidable (TyPred (Rec (Wit p))) where
    decide :: Decide (TyPred (Rec (Wit p)))
decide = \case
      Sing a
SList a
SNil         -> forall a. a -> Decision a
Proved forall {u} (a :: u -> *). Rec a '[]
RNil
      Sing n1
x `SCons` Sing n2
xs -> case forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing n1
x of
        Proved p @@ n1
p -> case forall {k1} (t :: k1 -> *) (a :: k1).
DecidableTC t =>
Sing a -> Decision (t a)
decideTC Sing n2
xs of
          Proved Rec (Wit p) n2
ps -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit p @@ n1
p 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 -> forall a. Refuted a -> Decision a
Disproved 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) rs
ps
        Disproved Refuted (p @@ n1)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
          Wit p @@ r
p :& Rec (Wit p) rs
_ -> Refuted (p @@ n1)
v p @@ r
p

-- | @since 3.0.0
instance Provable (TyPred (Rec WrappedSing)) where
    prove :: Prove (TyPred (Rec WrappedSing))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall k (a :: k). Sing a -> WrappedSing a
WrapSing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable (TyPred (Rec WrappedSing))

-- | @since 3.0.0
instance Provable p => Provable (TyPred (PMaybe (Wit p))) where
    prove :: Prove (TyPred (PMaybe (Wit p)))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable p => Decidable (TyPred (PMaybe (Wit p))) where
    decide :: Decide (TyPred (PMaybe (Wit p)))
decide = \case
      Sing a
SMaybe a
SNothing -> forall a. a -> Decision a
Proved forall {k} (a :: k -> *). PMaybe a 'Nothing
PNothing
      SJust Sing n
x  -> forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (forall {k} (a :: k -> *) (a1 :: k). a a1 -> PMaybe a ('Just a1)
PJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PJust (Wit p @@ a1
p) -> p @@ a1
p)
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @p
                forall a b. (a -> b) -> a -> b
$ Sing n
x

-- | @since 3.0.0
instance Provable (TyPred (PMaybe WrappedSing)) where
    prove :: Prove (TyPred (PMaybe WrappedSing))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall k (a :: k). Sing a -> WrappedSing a
WrapSing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable (TyPred (PMaybe WrappedSing))

-- | @since 3.0.0
instance Provable p => Provable (TyPred (NERec (Wit p))) where
    prove :: Prove (TyPred (NERec (Wit p)))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
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
decide @p Sing n1
x of
        Proved p @@ n1
p -> case forall {k1} (t :: k1 -> *) (a :: k1).
DecidableTC t =>
Sing a -> Decision (t a)
decideTC Sing n2
xs of
          Proved Rec (Wit p) n2
ps -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit p @@ n1
p 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 -> forall a. Refuted a -> Decision a
Disproved 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) as
ps
        Disproved Refuted (p @@ n1)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
          Wit p @@ a1
p :&| Rec (Wit p) as
_ -> Refuted (p @@ n1)
v p @@ a1
p

-- | @since 3.0.0
instance Provable (TyPred (NERec WrappedSing)) where
    prove :: Prove (TyPred (NERec WrappedSing))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall k (a :: k). Sing a -> WrappedSing a
WrapSing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable (TyPred (NERec WrappedSing))

-- | @since 3.0.0
instance Provable p => Provable (TyPred (PIdentity (Wit p))) where
    prove :: Prove (TyPred (PIdentity (Wit p)))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable p => Decidable (TyPred (PIdentity (Wit p))) where
    decide :: Decide (TyPred (PIdentity (Wit p)))
decide = \case
      SIdentity Sing n
x -> forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (forall {k} (a :: k -> *) (a1 :: k).
a a1 -> PIdentity a ('Identity a1)
PIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PIdentity (Wit p @@ a1
p) -> p @@ a1
p)
                   forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @p
                   forall a b. (a -> b) -> a -> b
$ Sing n
x

-- | @since 3.0.0
instance Provable (TyPred (PIdentity WrappedSing)) where
    prove :: Prove (TyPred (PIdentity WrappedSing))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall k (a :: k). Sing a -> WrappedSing a
WrapSing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable (TyPred (PIdentity WrappedSing))

-- | @since 3.0.0
instance Provable p => Provable (TyPred (PEither (Wit p))) where
    prove :: Prove (TyPred (PEither (Wit p)))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable p => Decidable (TyPred (PEither (Wit p))) where
    decide :: Decide (TyPred (PEither (Wit p)))
decide = \case
      SLeft  Sing n
x -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {j} {k} (e :: j) (a :: k -> *).
Sing e -> PEither a ('Left e)
PLeft Sing n
x
      SRight Sing n
y -> forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (forall {k} {j} (a :: k -> *) (a1 :: k).
a a1 -> PEither a ('Right a1)
PRight forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PRight (Wit p @@ a1
p) -> p @@ a1
p)
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @p
                forall a b. (a -> b) -> a -> b
$ Sing n
y

-- | @since 3.0.0
instance Provable (TyPred (PEither WrappedSing)) where
    prove :: Prove (TyPred (PEither WrappedSing))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall k (a :: k). Sing a -> WrappedSing a
WrapSing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable (TyPred (PEither WrappedSing))

-- | @since 3.0.0
instance Provable p => Provable (TyPred (PTup (Wit p))) where
    prove :: Prove (TyPred (PTup (Wit p)))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd (forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Provable p => Prove p
prove @p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
instance Decidable p => Decidable (TyPred (PTup (Wit p))) where
    decide :: Decide (TyPred (PTup (Wit p)))
decide (STuple2 Sing n1
x Sing n2
y) = forall a b. (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision (forall {j} {k} (w :: j) (a :: k -> *) (a1 :: k).
Sing w -> a a1 -> PTup a '(w, a1)
PTup Sing n1
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *) (a :: k1). (p @@ a) -> Wit p a
Wit) (\case PTup Sing w
_ (Wit p @@ a1
p) -> p @@ a1
p)
                         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} (p :: k1 ~> *). Decidable p => Decide p
decide @p
                         forall a b. (a -> b) -> a -> b
$ Sing n2
y

-- | @since 3.0.0
instance Provable (TyPred (PTup WrappedSing)) where
    prove :: Prove (TyPred (PTup WrappedSing))
prove = forall {k} (f :: * -> *) (g :: k -> *) (h :: k -> *) (as :: f k).
FProd f =>
(forall (a :: k). g a -> h a) -> Prod f g as -> Prod f h as
mapProd forall k (a :: k). Sing a -> WrappedSing a
WrapSing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) {k} (as :: f k).
FProd f =>
Sing as -> Prod f Sing as
singProd
-- | @since 3.0.0
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
decide @p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k1 k2 (f :: k1 ~> k2).
SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing (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
prove @p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k1 k2 (f :: k1 ~> k2).
SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
applySing (forall {k} (a :: k). SingI a => Sing a
sing :: Sing f)

-- | Compose two implications.
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 = q --> r
g Sing a
s forall b c a. (b -> c) -> (a -> b) -> a -> c
. p --> q
f Sing a
s

-- | @'Not' p@ is the predicate that @p@ is not true.
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)
decideNot @p @a (forall {k1} (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 = forall a. Void -> a
absurd forall a b. (a -> b) -> a -> b
$ Sing a -> Void
v Sing a
x

-- | Decide @'Not' p@ based on decisions of @p@.
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 = forall a. Decision a -> Decision (Refuted a)
flipDecision

-- | Flip the contents of a decision.  Turn a proof of @a@ into a disproof
-- of not-@a@.
--
-- Note that this is not reversible in general in constructivist logic  See
-- 'Data.Type.Predicate.Logic.doubleNegation' for a situation where it is.
--
-- @since 0.1.1.0
flipDecision
    :: Decision a
    -> Decision (Refuted a)
flipDecision :: forall a. Decision a -> Decision (Refuted a)
flipDecision = \case
    Proved    a
p -> forall a. Refuted a -> Decision a
Disproved (forall a b. (a -> b) -> a -> b
$ a
p)
    Disproved Refuted a
v -> forall a. a -> Decision a
Proved Refuted a
v

-- | Map over the value inside a 'Decision'.
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 -> forall a. a -> Decision a
Proved    forall a b. (a -> b) -> a -> b
$ a -> b
f a
p
    Disproved Refuted a
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> Refuted b -> Refuted a
mapRefuted b -> a
g Refuted a
v

-- | Converts a 'Decision' to a 'Maybe'.  Drop the witness of disproof of
-- @a@, returning 'Just' if 'Proved' (with the proof) and 'Nothing' if
-- 'Disproved'.
--
-- @since 0.1.1.0
forgetDisproof
    :: Decision a
    -> Maybe a
forgetDisproof :: forall a. Decision a -> Maybe a
forgetDisproof = \case
    Proved    a
p -> forall a. a -> Maybe a
Just a
p
    Disproved Refuted a
_ -> forall a. Maybe a
Nothing

-- | Drop the witness of proof of @a@, returning 'Nothing' if 'Proved' and
-- 'Just' if 'Disproved' (with the disproof).
--
-- @since 0.1.1.0
forgetProof
    :: Decision a
    -> Maybe (Refuted a)
forgetProof :: forall a. Decision a -> Maybe (Refuted a)
forgetProof = forall a. Decision a -> Maybe a
forgetDisproof forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Decision a -> Decision (Refuted a)
flipDecision

-- | Boolean test if a 'Decision' is 'Proved'.
--
-- @since 0.1.1.0
isProved :: Decision a -> Bool
isProved :: forall a. Decision a -> Bool
isProved = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Decision a -> Maybe a
forgetDisproof

-- | Boolean test if a 'Decision' is 'Disproved'.
--
-- @since 0.1.1.0
isDisproved :: Decision a -> Bool
isDisproved :: forall a. Decision a -> Bool
isDisproved = forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Decision a -> Maybe a
forgetDisproof

-- | Helper function for a common pattern of eliminating the disproved
-- branch of 'Decision' to certaintify the proof.
--
-- @since 0.1.2.0
elimDisproof
    :: Decision a
    -> Refuted (Refuted a)
    -> a
elimDisproof :: forall a. Decision a -> Refuted (Refuted a) -> a
elimDisproof = \case
    Proved    a
p -> forall a b. a -> b -> a
const a
p
    Disproved Refuted a
v -> forall a. Void -> a
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> a -> b
$ Refuted a
v)

-- | Change the target of a 'Refuted' with a contravariant mapping
-- function.
--
-- @since 0.1.2.0
mapRefuted
    :: (a -> b)
    -> Refuted b
    -> Refuted a
mapRefuted :: forall a b. (a -> b) -> Refuted b -> Refuted a
mapRefuted = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)

-- | @'In' f as@ is a predicate that a given input @a@ is a member of
-- collection @as@.
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 = forall (bs :: [k]). Sing bs -> Decision (Index bs a)
go (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         -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
          Sing n1
y `SCons` Sing n2
ys -> case Sing a
x forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
            Proved a :~: n1
Refl -> forall a. a -> Decision a
Proved forall {k} (b :: k) (as :: [k]). Index (b : as) b
IZ
            Disproved Refuted (a :~: n1)
v -> case forall (bs :: [k]). Sing bs -> Decision (Index bs a)
go Sing n2
ys of
              Proved Index n2 a
i    -> forall a. a -> Decision a
Proved (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 -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
                Index bs a
IZ   -> Refuted (a :~: n1)
v forall {k} (a :: k). a :~: a
Refl
                IS Index bs a
i -> Refuted (Index n2 a)
u 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 {k} (a :: k). SingI a => Sing a
sing @as of
      Sing as
SMaybe as
SNothing -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
      SJust Sing n
y  -> case Sing a
x forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
        Proved a :~: n
Refl -> forall a. a -> Decision a
Proved forall {k} (b :: k). IJust ('Just b) b
IJust
        Disproved Refuted (a :~: n)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case IJust ('Just n) a
In Maybe as @@ a
IJust -> Refuted (a :~: n)
v 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 {k} (a :: k). SingI a => Sing a
sing @as of
      SLeft Sing n
_  -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case {}
      SRight Sing n
y -> case Sing a
x forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
        Proved a :~: n
Refl -> forall a. a -> Decision a
Proved forall {k} {j} (b :: k). IRight ('Right b) b
IRight
        Disproved Refuted (a :~: n)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case IRight ('Right n) a
In (Either j) as @@ a
IRight -> Refuted (a :~: n)
v 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 {k} (a :: k). SingI a => Sing a
sing @as of
      Sing n1
y NE.:%| (Sing n2
Sing :: Sing bs) -> case Sing a
x forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
        Proved a :~: n1
Refl -> forall a. a -> Decision a
Proved 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
decide @(In [] bs) Sing a
x of
          Proved In [] n2 @@ a
i    -> forall a. a -> Decision a
Proved forall a b. (a -> b) -> a -> b
$ forall {k} (as :: [k]) (b :: k) (b1 :: k).
Index as b -> NEIndex (b1 ':| as) b
NETail In [] n2 @@ a
i
          Disproved Refuted (In [] n2 @@ a)
u -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case
            NEIndex (n1 ':| n2) a
In NonEmpty as @@ a
NEHead   -> Refuted (a :~: n1)
v forall {k} (a :: k). a :~: a
Refl
            NETail Index as a
i -> Refuted (In [] n2 @@ a)
u Index as 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
sing @as of
      STuple2 Sing n1
_ Sing n2
y -> case Sing a
x forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n2
y of
        Proved a :~: n2
Refl -> forall a. a -> Decision a
Proved forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
ISnd
        Disproved Refuted (a :~: n2)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case ISnd '(n1, n2) a
In ((,) j) as @@ a
ISnd -> Refuted (a :~: n2)
v 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
sing @as of
      SIdentity Sing n
y -> case Sing a
x forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
        Proved a :~: n
Refl -> forall a. a -> Decision a
Proved forall {k} (b :: k). IIdentity ('Identity b) b
IId
        Disproved Refuted (a :~: n)
v -> forall a. Refuted a -> Decision a
Disproved forall a b. (a -> b) -> a -> b
$ \case IIdentity ('Identity n) a
In Identity as @@ a
IId -> Refuted (a :~: n)
v forall {k} (a :: k). a :~: a
Refl