{-# LANGUAGE Trustworthy #-}
-- | Boolean functions.
--
-- Type families are defined in "Data.Type.Bool" module in @base@ package.
-- Term implementation use 'SBool' from @singleton-bool@ package.
--
module SBool.DeFun (
    -- * Logical and
    LAnd, LAndSym, LAndSym1,
    land, landSym, landSym1,
    -- * Logical or
    LOr, LOrSym, LOrSym1,
    lor, lorSym, lorSym1,
    -- * Logical not
    Not, NotSym,
    not, notSym,
) where

import Data.Singletons.Bool (SBool (..), sboolAnd, sboolNot, sboolOr)

import DeFun.Bool
import DeFun.Core

-------------------------------------------------------------------------------
-- LAnd
-------------------------------------------------------------------------------

land :: SBool x -> SBool y -> SBool (LAnd x y)
land :: forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LAnd x y)
land = forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LAnd x y)
sboolAnd

landSym1 :: SBool x -> Lam SBool SBool (LAndSym1 x)
landSym1 :: forall (x :: Bool). SBool x -> Lam SBool SBool (LAndSym1 x)
landSym1 SBool x
x = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LAnd x y)
land SBool x
x)

landSym :: Lam2 SBool SBool SBool LAndSym
landSym :: Lam2 SBool SBool SBool LAndSym
landSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall (x :: Bool). SBool x -> Lam SBool SBool (LAndSym1 x)
landSym1

-------------------------------------------------------------------------------
-- LOr
-------------------------------------------------------------------------------

lor :: SBool x -> SBool y -> SBool (LOr x y)
lor :: forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LOr x y)
lor = forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LOr x y)
sboolOr

lorSym1 :: SBool x -> Lam SBool SBool (LOrSym1 x)
lorSym1 :: forall (x :: Bool). SBool x -> Lam SBool SBool (LOrSym1 x)
lorSym1 SBool x
x = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall (x :: Bool) (y :: Bool).
SBool x -> SBool y -> SBool (LOr x y)
lor SBool x
x)

lorSym :: Lam2 SBool SBool SBool LOrSym
lorSym :: Lam2 SBool SBool SBool LOrSym
lorSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall (x :: Bool). SBool x -> Lam SBool SBool (LOrSym1 x)
lorSym1

-------------------------------------------------------------------------------
-- Not
-------------------------------------------------------------------------------

not :: SBool x -> SBool (Not x)
not :: forall (x :: Bool). SBool x -> SBool (Not x)
not = forall (x :: Bool). SBool x -> SBool (Not x)
sboolNot

notSym :: Lam SBool SBool NotSym
notSym :: Lam SBool SBool NotSym
notSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall (x :: Bool). SBool x -> SBool (Not x)
not