{-# LANGUAGE TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators,
             GADTs, ScopedTypeVariables, DeriveDataTypeable, UndecidableInstances,
             DataKinds, PolyKinds, StandaloneKindSignatures #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Bool.Singletons
-- Copyright   :  (C) 2013-2014 Richard Eisenberg, Jan Stolarek
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Ryan Scott
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Defines functions and datatypes relating to the singleton for 'Bool',
-- including singled versions of all the definitions in @Data.Bool@.
--
-- Because many of these definitions are produced by Template Haskell,
-- it is not possible to create proper Haddock documentation. Please look
-- up the corresponding operation in @Data.Bool@. Also, please excuse
-- the apparent repeated variable names. This is due to an interaction
-- between Template Haskell and Haddock.
--
----------------------------------------------------------------------------

module Data.Bool.Singletons (
  -- * The 'Bool' singleton
  Sing, SBool(..),

  -- * Conditionals
  If, sIf,

  -- * Singletons from @Data.Bool@
  Not, sNot, type (&&), type (||), (%&&), (%||),

  -- | The following are derived from the function 'bool' in @Data.Bool@. The extra
  -- underscore is to avoid name clashes with the type 'Bool'.
  bool_, Bool_, sBool_, Otherwise, sOtherwise,

  -- * Defunctionalization symbols
  TrueSym0, FalseSym0,

  IfSym0, IfSym1, IfSym2, IfSym3,
  NotSym0, NotSym1,
  type (&&@#@$), type (&&@#@$$), type (&&@#@$$$),
  type (||@#@$), type (||@#@$$), type (||@#@$$$),
  Bool_Sym0, Bool_Sym1, Bool_Sym2, Bool_Sym3,
  OtherwiseSym0
  ) where

import Data.Singletons
import Data.Singletons.Base.Instances
import Data.Singletons.TH
import Data.Type.Bool ( If, type (&&), type (||), Not )

$(singletons [d|
  bool_ :: a -> a -> Bool -> a
  bool_ fls _tru False = fls
  bool_ _fls tru True  = tru
 |])

$(singletonsOnly [d|
  otherwise               :: Bool
  otherwise               =  True
  |])

-- | Conjunction of singletons
(%&&) :: Sing a -> Sing b -> Sing (a && b)
Sing a
SBool a
SFalse %&& :: forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a && b)
%&& Sing b
_ = Sing (a && b)
SBool 'False
SFalse
Sing a
SBool a
STrue  %&& Sing b
a = Sing b
Sing (a && b)
a
infixr 3 %&&
$(genDefunSymbols [''(&&)])
instance SingI (&&@#@$) where
  sing :: Sing (&&@#@$)
sing = SingFunction2 (&&@#@$) -> Sing (&&@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a && b)
SingFunction2 (&&@#@$)
(%&&)
instance SingI x => SingI ((&&@#@$$) x) where
  sing :: Sing ((&&@#@$$) x)
sing = SingFunction1 ((&&@#@$$) x) -> Sing ((&&@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (forall (a :: Bool). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x Sing x -> Sing t -> Sing (x && t)
forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a && b)
%&&)

-- | Disjunction of singletons
(%||) :: Sing a -> Sing b -> Sing (a || b)
Sing a
SBool a
SFalse %|| :: forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a || b)
%|| Sing b
a = Sing b
Sing (a || b)
a
Sing a
SBool a
STrue  %|| Sing b
_ = Sing (a || b)
SBool 'True
STrue
infixr 2 %||
$(genDefunSymbols [''(||)])
instance SingI (||@#@$) where
  sing :: Sing (||@#@$)
sing = SingFunction2 (||@#@$) -> Sing (||@#@$)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a || b)
SingFunction2 (||@#@$)
(%||)
instance SingI x => SingI ((||@#@$$) x) where
  sing :: Sing ((||@#@$$) x)
sing = SingFunction1 ((||@#@$$) x) -> Sing ((||@#@$$) x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (forall (a :: Bool). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x Sing x -> Sing t -> Sing (x || t)
forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a || b)
%||)

-- | Negation of a singleton
sNot :: Sing a -> Sing (Not a)
sNot :: forall (a :: Bool). Sing a -> Sing (Not a)
sNot Sing a
SBool a
SFalse = Sing (Not a)
SBool 'True
STrue
sNot Sing a
SBool a
STrue  = Sing (Not a)
SBool 'False
SFalse
$(genDefunSymbols [''Not])
instance SingI NotSym0 where
  sing :: Sing NotSym0
sing = SingFunction1 NotSym0 -> Sing NotSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 forall (a :: Bool). Sing a -> Sing (Not a)
SingFunction1 NotSym0
sNot

-- | Conditional over singletons
sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf :: forall {k} (a :: Bool) (b :: k) (c :: k).
Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf Sing a
SBool a
STrue Sing b
b Sing c
_ = Sing b
Sing (If a b c)
b
sIf Sing a
SBool a
SFalse Sing b
_ Sing c
c = Sing c
Sing (If a b c)
c
$(genDefunSymbols [''If])
instance SingI IfSym0 where
  sing :: Sing IfSym0
sing = SingFunction3 IfSym0 -> Sing IfSym0
forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))).
SingFunction3 f -> Sing f
singFun3 SingFunction3 IfSym0
forall {k} (a :: Bool) (b :: k) (c :: k).
Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf
instance SingI c => SingI (IfSym1 c) where
  sing :: Sing (IfSym1 c)
sing = SingFunction2 (IfSym1 c) -> Sing (IfSym1 c)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 (SingFunction2 (IfSym1 c) -> Sing (IfSym1 c))
-> SingFunction2 (IfSym1 c) -> Sing (IfSym1 c)
forall a b. (a -> b) -> a -> b
$ Sing c -> Sing t1 -> Sing t2 -> Sing (If c t1 t2)
forall {k} (a :: Bool) (b :: k) (c :: k).
Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf (forall (a :: Bool). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @c)
instance (SingI c, SingI t) => SingI (IfSym2 c t) where
  sing :: Sing (IfSym2 c t)
sing = SingFunction1 (IfSym2 c t) -> Sing (IfSym2 c t)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (IfSym2 c t) -> Sing (IfSym2 c t))
-> SingFunction1 (IfSym2 c t) -> Sing (IfSym2 c t)
forall a b. (a -> b) -> a -> b
$ Sing c -> Sing t -> Sing t -> Sing (If c t t)
forall {k} (a :: Bool) (b :: k) (c :: k).
Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf (forall (a :: Bool). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @c) (forall (a :: k). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @t)
instance SingI1 IfSym1 where
  liftSing :: forall (x :: Bool). Sing x -> Sing (IfSym1 x)
liftSing Sing x
s = SingFunction2 (IfSym1 x) -> Sing (IfSym1 x)
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 (SingFunction2 (IfSym1 x) -> Sing (IfSym1 x))
-> SingFunction2 (IfSym1 x) -> Sing (IfSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t1 -> Sing t2 -> Sing (If x t1 t2)
forall {k} (a :: Bool) (b :: k) (c :: k).
Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf Sing x
s
instance SingI c => SingI1 (IfSym2 c) where
  liftSing :: forall (x :: k1). Sing x -> Sing (IfSym2 c x)
liftSing Sing x
s = SingFunction1 (IfSym2 c x) -> Sing (IfSym2 c x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (IfSym2 c x) -> Sing (IfSym2 c x))
-> SingFunction1 (IfSym2 c x) -> Sing (IfSym2 c x)
forall a b. (a -> b) -> a -> b
$ Sing c -> Sing x -> Sing t -> Sing (If c x t)
forall {k} (a :: Bool) (b :: k) (c :: k).
Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf (forall (a :: Bool). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @c) Sing x
s
instance SingI2 IfSym2 where
  liftSing2 :: forall (x :: Bool) (y :: k2). Sing x -> Sing y -> Sing (IfSym2 x y)
liftSing2 Sing x
s1 Sing y
s2 = SingFunction1 (IfSym2 x y) -> Sing (IfSym2 x y)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (IfSym2 x y) -> Sing (IfSym2 x y))
-> SingFunction1 (IfSym2 x y) -> Sing (IfSym2 x y)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing y -> Sing t -> Sing (If x y t)
forall {k} (a :: Bool) (b :: k) (c :: k).
Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf Sing x
s1 Sing y
s2