{-# 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.Functor.Identity
import           Data.Kind
import           Data.List.NonEmpty                    (NonEmpty(..))
import           Data.Maybe
import           Data.Singletons
import           Data.Singletons.Decide
import           Data.Singletons.Prelude hiding        (Not, ElemSym1)
import           Data.Singletons.Prelude.Identity
import           Data.Type.Functor.Product
import           Data.Void
import qualified Data.Singletons.Prelude.List.NonEmpty 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 { 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 = 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
. Provable p => Prove p
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 :: Prove (Not p)
disprove = Provable (Not p) => Prove (Not p)
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 :: Sing a -> Decision (t a)
decideTC = Decidable (TyPred t) => Decide (TyPred t)
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 :: Sing a -> t a
proveTC = Provable (TyPred t) => Prove (TyPred t)
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 :: Sing a -> Decision (EqualTo a @@ a)
decide = (Sing a
forall k (a :: k). SingI a => Sing a
sing Sing a -> Sing a -> Decision (a :~: a)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~)

instance Decidable Evident
instance Provable Evident where
    prove :: Sing a -> Evident @@ a
prove = Sing a -> Evident @@ a
forall a. a -> a
id

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

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

-- | @since 3.0.0
instance Provable (TyPred (Rec WrappedSing)) where
    prove :: Sing a -> TyPred (Rec WrappedSing) @@ a
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 forall (a :: u). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (Rec Sing a -> Rec WrappedSing a)
-> (SList a -> Rec Sing a) -> SList a -> Rec WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SList a -> Rec Sing a
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 :: Sing a -> TyPred (PMaybe (Wit p)) @@ a
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
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (PMaybe Sing a -> PMaybe (Wit p) a)
-> (SMaybe a -> PMaybe Sing a) -> SMaybe a -> PMaybe (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMaybe a -> PMaybe Sing a
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 :: Sing a -> Decision (TyPred (PMaybe (Wit p)) @@ a)
decide = \case
      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 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 :: p @@ a1
p) -> Apply p n
p @@ a1
p)
                (Decision (Apply p n) -> Decision (PMaybe (Wit p) ('Just n)))
-> (Sing n -> Decision (Apply p n))
-> Sing n
-> Decision (PMaybe (Wit p) ('Just n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decidable p => Decide p
forall k1 (p :: k1 ~> *). 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

-- | @since 3.0.0
instance Provable (TyPred (PMaybe WrappedSing)) where
    prove :: Sing a -> TyPred (PMaybe WrappedSing) @@ a
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 forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (PMaybe Sing a -> PMaybe WrappedSing a)
-> (SMaybe a -> PMaybe Sing a) -> SMaybe a -> PMaybe WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMaybe a -> PMaybe Sing a
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 :: Sing a -> TyPred (NERec (Wit p)) @@ a
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
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (NERec Sing a -> NERec (Wit p) a)
-> (SNonEmpty a -> NERec Sing a) -> SNonEmpty a -> NERec (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNonEmpty a -> NERec Sing a
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 :: Sing a -> Decision (TyPred (NERec (Wit p)) @@ a)
decide = \case
      x NE.:%| xs -> case Sing n1 -> Decision (p @@ n1)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing n1
x of
        Proved p :: 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 ps :: Rec (Wit p) n2
ps -> NERec (Wit p) (n1 ':| n2) -> Decision (TyPred (NERec (Wit p)) @@ a)
forall a. a -> Decision a
Proved (NERec (Wit p) (n1 ':| n2)
 -> Decision (TyPred (NERec (Wit p)) @@ a))
-> NERec (Wit p) (n1 ':| n2)
-> 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 vs :: Refuted (Rec (Wit p) n2)
vs -> Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (NERec (Wit p) (n1 ':| n2))
 -> Decision (TyPred (NERec (Wit p)) @@ a))
-> Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
            _ :&| ps :: Rec (Wit p) as
ps -> Refuted (Rec (Wit p) n2)
vs Rec (Wit p) n2
Rec (Wit p) as
ps
        Disproved v :: Refuted (p @@ n1)
v -> Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (NERec (Wit p) (n1 ':| n2))
 -> Decision (TyPred (NERec (Wit p)) @@ a))
-> Refuted (NERec (Wit p) (n1 ':| n2))
-> Decision (TyPred (NERec (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ \case
          Wit p :&| _ -> Refuted (p @@ n1)
v p @@ n1
p @@ a1
p

-- | @since 3.0.0
instance Provable (TyPred (NERec WrappedSing)) where
    prove :: Sing a -> TyPred (NERec WrappedSing) @@ a
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 forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (NERec Sing a -> NERec WrappedSing a)
-> (SNonEmpty a -> NERec Sing a)
-> SNonEmpty a
-> NERec WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNonEmpty a -> NERec Sing a
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 :: Sing a -> TyPred (PIdentity (Wit p)) @@ a
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
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (PIdentity Sing a -> PIdentity (Wit p) a)
-> (SIdentity a -> PIdentity Sing a)
-> SIdentity a
-> PIdentity (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIdentity a -> PIdentity Sing a
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 :: Sing a -> Decision (TyPred (PIdentity (Wit p)) @@ a)
decide = \case
      SIdentity 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 :: p @@ a1
p) -> Apply p n
p @@ a1
p)
                   (Decision (Apply p n)
 -> Decision (PIdentity (Wit p) ('Identity n)))
-> (Sing n -> Decision (Apply p n))
-> Sing n
-> Decision (PIdentity (Wit p) ('Identity n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decidable p => Decide p
forall k1 (p :: k1 ~> *). 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

-- | @since 3.0.0
instance Provable (TyPred (PIdentity WrappedSing)) where
    prove :: Sing a -> TyPred (PIdentity WrappedSing) @@ a
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 forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (PIdentity Sing a -> PIdentity WrappedSing a)
-> (SIdentity a -> PIdentity Sing a)
-> SIdentity a
-> PIdentity WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SIdentity a -> PIdentity Sing a
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 :: Sing a -> TyPred (PEither (Wit p)) @@ a
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
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (PEither Sing a -> PEither (Wit p) a)
-> (SEither a -> PEither Sing a) -> SEither a -> PEither (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEither a -> PEither Sing a
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 :: Sing a -> Decision (TyPred (PEither (Wit p)) @@ a)
decide = \case
      SLeft  x -> PEither (Wit p) ('Left n)
-> Decision (TyPred (PEither (Wit p)) @@ a)
forall a. a -> Decision a
Proved (PEither (Wit p) ('Left n)
 -> Decision (TyPred (PEither (Wit p)) @@ a))
-> PEither (Wit p) ('Left n)
-> 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 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 :: p @@ a1
p) -> Apply p n
p @@ a1
p)
                (Decision (Apply p n) -> Decision (PEither (Wit p) ('Right n)))
-> (Sing n -> Decision (Apply p n))
-> Sing n
-> Decision (PEither (Wit p) ('Right n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decidable p => Decide p
forall k1 (p :: k1 ~> *). 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

-- | @since 3.0.0
instance Provable (TyPred (PEither WrappedSing)) where
    prove :: Sing a -> TyPred (PEither WrappedSing) @@ a
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 forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (PEither Sing a -> PEither WrappedSing a)
-> (SEither a -> PEither Sing a)
-> SEither a
-> PEither WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEither a -> PEither Sing a
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 :: Sing a -> TyPred (PTup (Wit p)) @@ a
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
. Provable p => Prove p
forall k1 (p :: k1 ~> *). Provable p => Prove p
prove @p) (PTup Sing a -> PTup (Wit p) a)
-> (STuple2 a -> PTup Sing a) -> STuple2 a -> PTup (Wit p) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STuple2 a -> PTup Sing a
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 :: Sing a -> Decision (TyPred (PTup (Wit p)) @@ a)
decide (STuple2 x 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 _ (Wit p :: p @@ a1
p) -> Apply p n2
p @@ a1
p)
                         (Decision (Apply p n2) -> Decision (PTup (Wit p) '(n1, n2)))
-> (Sing n2 -> Decision (Apply p n2))
-> Sing n2
-> Decision (PTup (Wit p) '(n1, n2))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Decidable p => Decide p
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p
                         (Sing n2 -> Decision (TyPred (PTup (Wit p)) @@ a))
-> Sing n2 -> Decision (TyPred (PTup (Wit p)) @@ a)
forall a b. (a -> b) -> a -> b
$ Sing n2
y

-- | @since 3.0.0
instance Provable (TyPred (PTup WrappedSing)) where
    prove :: Sing a -> TyPred (PTup WrappedSing) @@ a
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 forall (a :: k). Sing a -> WrappedSing a
forall k (a :: k). Sing a -> WrappedSing a
WrapSing (PTup Sing a -> PTup WrappedSing a)
-> (STuple2 a -> PTup Sing a) -> STuple2 a -> PTup WrappedSing a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STuple2 a -> PTup Sing a
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 :: Sing a -> Decision (PMap f p @@ a)
decide = Decidable p => Decide p
forall k1 (p :: k1 ~> *). 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 :: Sing a -> PMap f p @@ a
prove = Provable p => Prove p
forall k1 (p :: k1 ~> *). 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)

-- | Compose two implications.
compImpl
    :: forall p q r. ()
    => p --> q
    -> q --> r
    -> p --> r
compImpl :: (p --> q) -> (q --> r) -> p --> r
compImpl f :: p --> q
f g :: q --> r
g s :: Sing a
s = Sing a -> (q @@ a) -> Apply r a
q --> r
g Sing a
s ((q @@ a) -> Apply r a)
-> (Apply p a -> q @@ a) -> Apply p a -> Apply r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> Apply p a -> q @@ a
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 :: Sing a -> Decision (Not p @@ a)
decide (x :: Sing a) = Decision (p @@ a) -> Decision (Not p @@ a)
forall k1 (p :: k1 ~> *) (a :: k1).
Decision (p @@ a) -> Decision (Not p @@ a)
decideNot @p @a (Sing a -> Decision (p @@ a)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @p Sing a
x)

instance Provable (Not Impossible) where
    prove :: Sing a -> Not Impossible @@ a
prove x :: Sing a
x v :: 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

-- | Decide @'Not' p@ based on decisions of @p@.
decideNot
    :: forall p a. ()
    => Decision (p @@ a)
    -> Decision (Not p @@ a)
decideNot :: Decision (p @@ a) -> Decision (Not p @@ a)
decideNot = Decision (p @@ a) -> Decision (Not p @@ a)
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 :: Decision a -> Decision (Refuted a)
flipDecision = \case
    Proved    p :: 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 v :: Refuted a
v -> Refuted a -> Decision (Refuted a)
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 :: (a -> b) -> (b -> a) -> Decision a -> Decision b
mapDecision f :: a -> b
f g :: b -> a
g = \case
    Proved    p :: 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 v :: 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

-- | 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 :: Decision a -> Maybe a
forgetDisproof = \case
    Proved    p :: a
p -> a -> Maybe a
forall a. a -> Maybe a
Just a
p
    Disproved _ -> Maybe 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 :: 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

-- | Boolean test if a 'Decision' is 'Proved'.
--
-- @since 0.1.1.0
isProved :: Decision a -> Bool
isProved :: 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

-- | Boolean test if a 'Decision' is 'Disproved'.
--
-- @since 0.1.1.0
isDisproved :: Decision a -> Bool
isDisproved :: 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

-- | 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 :: Decision a -> Refuted (Refuted a) -> a
elimDisproof = \case
    Proved    p :: a
p -> a -> Refuted (Refuted a) -> a
forall a b. a -> b -> a
const a
p
    Disproved v :: 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)

-- | Change the target of a 'Refuted' with a contravariant mapping
-- function.
--
-- @since 0.1.2.0
mapRefuted
    :: (a -> b)
    -> Refuted b
    -> Refuted a
mapRefuted :: (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
(.)

-- | @'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 :: Sing a -> Decision (Index as a)
decide x :: Sing a
x = Sing as -> Decision (Index as a)
forall (bs :: [k]). Sing bs -> Decision (Index bs a)
go (SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as)
      where
        go :: Sing bs -> Decision (Index bs a)
        go :: Sing bs -> Decision (Index bs a)
go = \case
          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 {}
          y `SCons` ys -> case Sing a
x Sing a -> Sing n1 -> Decision (a :~: n1)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
            Proved Refl -> Index (a : n2) a -> Decision (Index (a : n2) a)
forall a. a -> Decision a
Proved Index (a : n2) a
forall k (b :: k) (as :: [k]). Index (b : as) b
IZ
            Disproved v :: 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 i :: Index n2 a
i    -> Index (n1 : n2) a -> Decision (Index (n1 : n2) 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 u :: 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
                IZ   -> Refuted (a :~: n1)
v a :~: n1
forall k (a :: k). a :~: a
Refl
                IS i :: 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 :: Sing a -> Decision (In Maybe as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
      SNothing -> Refuted (IJust 'Nothing a) -> Decision (In Maybe as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IJust 'Nothing a) -> Decision (In Maybe as @@ a))
-> Refuted (IJust 'Nothing a) -> Decision (In Maybe as @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
      SJust y  -> case Sing a
x Sing a -> Sing n -> Decision (a :~: n)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
        Proved 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 v :: Refuted (a :~: n)
v -> Refuted (IJust ('Just n) a) -> Decision (In Maybe as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IJust ('Just n) a) -> Decision (In Maybe as @@ a))
-> Refuted (IJust ('Just n) a) -> Decision (In Maybe as @@ a)
forall a b. (a -> b) -> a -> b
$ \case IJust -> Refuted (a :~: n)
v a :~: n
forall k (a :: k). a :~: a
Refl

instance (SDecide k, SingI (as :: Either j k)) => Decidable (In (Either j) as) where
    decide :: Sing a -> Decision (In (Either j) as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
      SLeft _  -> Refuted (IRight ('Left n) a) -> Decision (In (Either j) as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IRight ('Left n) a) -> Decision (In (Either j) as @@ a))
-> Refuted (IRight ('Left n) a) -> Decision (In (Either j) as @@ a)
forall a b. (a -> b) -> a -> b
$ \case {}
      SRight y -> case Sing a
x Sing a -> Sing n -> Decision (a :~: n)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
        Proved 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 v :: Refuted (a :~: n)
v -> Refuted (IRight ('Right n) a) -> Decision (In (Either j) as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IRight ('Right n) a) -> Decision (In (Either j) as @@ a))
-> Refuted (IRight ('Right n) a)
-> Decision (In (Either j) as @@ a)
forall a b. (a -> b) -> a -> b
$ \case IRight -> Refuted (a :~: n)
v a :~: n
forall k (a :: k). a :~: a
Refl

instance (SDecide k, SingI (as :: NonEmpty k)) => Decidable (In NonEmpty as) where
    decide :: Sing a -> Decision (In NonEmpty as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
      y NE.:%| (Sing :: Sing bs) -> case Sing a
x Sing a -> Sing n1 -> Decision (a :~: n1)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n1
y of
        Proved 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 v :: Refuted (a :~: n1)
v -> case Sing a -> Decision (In [] n2 @@ a)
forall k1 (p :: k1 ~> *). Decidable p => Decide p
decide @(In [] bs) Sing a
x of
          Proved i :: In [] n2 @@ a
i    -> NEIndex (n1 ':| n2) a -> Decision (In NonEmpty as @@ a)
forall a. a -> Decision a
Proved (NEIndex (n1 ':| n2) a -> Decision (In NonEmpty as @@ a))
-> NEIndex (n1 ':| n2) 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 u :: Refuted (In [] n2 @@ a)
u -> Refuted (NEIndex (n1 ':| n2) a) -> Decision (In NonEmpty as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (NEIndex (n1 ':| n2) a) -> Decision (In NonEmpty as @@ a))
-> Refuted (NEIndex (n1 ':| n2) a)
-> Decision (In NonEmpty as @@ a)
forall a b. (a -> b) -> a -> b
$ \case
            NEHead   -> Refuted (a :~: n1)
v a :~: n1
forall k (a :: k). a :~: a
Refl
            NETail i :: 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 :: Sing a -> Decision (In ((,) j) as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
      STuple2 _ y -> case Sing a
x Sing a -> Sing n2 -> Decision (a :~: n2)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n2
y of
        Proved 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 v :: Refuted (a :~: n2)
v -> Refuted (ISnd '(n1, n2) a) -> Decision (In ((,) j) as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (ISnd '(n1, n2) a) -> Decision (In ((,) j) as @@ a))
-> Refuted (ISnd '(n1, n2) a) -> Decision (In ((,) j) as @@ a)
forall a b. (a -> b) -> a -> b
$ \case ISnd -> Refuted (a :~: n2)
v a :~: n2
forall k (a :: k). a :~: a
Refl

instance (SDecide k, SingI (as :: Identity k)) => Decidable (In Identity as) where
    decide :: Sing a -> Decision (In Identity as @@ a)
decide x :: Sing a
x = case SingI as => Sing as
forall k (a :: k). SingI a => Sing a
sing @as of
      SIdentity y -> case Sing a
x Sing a -> Sing n -> Decision (a :~: n)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
y of
        Proved 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 v :: Refuted (a :~: n)
v -> Refuted (IIdentity ('Identity n) a)
-> Decision (In Identity as @@ a)
forall a. Refuted a -> Decision a
Disproved (Refuted (IIdentity ('Identity n) a)
 -> Decision (In Identity as @@ a))
-> Refuted (IIdentity ('Identity n) a)
-> Decision (In Identity as @@ a)
forall a b. (a -> b) -> a -> b
$ \case IId -> Refuted (a :~: n)
v a :~: n
forall k (a :: k). a :~: a
Refl