{-# 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
-- 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 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

-- | 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 = 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

-- | 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
forall (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
forall (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
forall (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 = (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

-- | @since 3.0.0
instance Decidable (TyPred WrappedSing)

-- | @since 3.0.0
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

-- | @since 3.0.0
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

-- | @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 -> 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

-- | @since 3.0.0
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

-- | @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 (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

-- | @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 -> 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

-- | @since 3.0.0
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

-- | @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 (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

-- | @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
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

-- | @since 3.0.0
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

-- | @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 (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

-- | @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 ->
      (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

-- | @since 3.0.0
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

-- | @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 (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

-- | @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 -> (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

-- | @since 3.0.0
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

-- | @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 (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

-- | @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) =
    (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

-- | @since 3.0.0
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

-- | @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
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)

-- | 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 = 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

-- | @'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)
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

-- | 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 = 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

-- | 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 -> 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

-- | 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 -> 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

-- | 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 -> a -> Maybe a
forall a. a -> Maybe a
Just a
p
  Disproved Refuted a
_ -> 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 :: 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

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

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

-- | 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 -> 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)

-- | 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 = (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 :: 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