module Language.Symantic.Lib.Bool where
import Control.Monad
import Prelude hiding ((&&), not, (||))
import qualified Data.Bool as Bool
import qualified Data.Text as Text
import Language.Symantic
import Language.Symantic.Lib.Function ()
type instance Sym Bool = Sym_Bool
class Sym_Bool term where
bool :: Bool -> term Bool
not :: term Bool -> term Bool
(&&) :: term Bool -> term Bool -> term Bool; infixr 3 &&
(||) :: term Bool -> term Bool -> term Bool; infixr 2 ||
xor :: term Bool -> term Bool -> term Bool; infixr 2 `xor`
xor x y = (x || y) && not (x && y)
default bool :: Sym_Bool (UnT term) => Trans term => Bool -> term Bool
default not :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool
default (&&) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool
default (||) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool
bool = trans . bool
not = trans1 not
(&&) = trans2 (&&)
(||) = trans2 (||)
instance Sym_Bool Eval where
bool = Eval
not = liftM Bool.not
(&&) = liftM2 (Bool.&&)
(||) = liftM2 (Bool.||)
instance Sym_Bool View where
bool o = View $ \_p _v -> Text.pack (show o)
not = view1 "not"
(&&) = viewInfix "&&" (infixR 3)
(||) = viewInfix "||" (infixR 2)
xor = viewInfix "`xor`" (infixR 2)
instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (Dup r1 r2) where
bool b = bool b `Dup` bool b
not = dup1 @Sym_Bool not
(&&) = dup2 @Sym_Bool (&&)
(||) = dup2 @Sym_Bool (||)
xor = dup2 @Sym_Bool xor
instance (Sym_Lambda term, Sym_Bool term) => Sym_Bool (BetaT term) where
xor = trans2 xor
instance NameTyOf Bool where
nameTyOf _c = ["Bool"] `Mod` "Bool"
instance ClassInstancesFor Bool where
proveConstraintFor _ (TyConst _ _ q :@ b)
| Just HRefl <- proj_ConstKiTy @_ @Bool b
= case () of
_ | Just Refl <- proj_Const @Bounded q -> Just Dict
| Just Refl <- proj_Const @Enum q -> Just Dict
| Just Refl <- proj_Const @Eq q -> Just Dict
| Just Refl <- proj_Const @Ord q -> Just Dict
| Just Refl <- proj_Const @Show q -> Just Dict
_ -> Nothing
proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Bool
instance Gram_Term_AtomsFor src ss g Bool
instance (Source src, SymInj ss Bool) => ModuleFor src ss Bool where
moduleFor = ["Bool"] `moduleWhere`
[ "False" := teBool False
, "True" := teBool True
, "not" := teBool_not
, "and" `withInfixR` 3 := teBool_and
, "or" `withInfixR` 2 := teBool_or
, "xor" `withInfixR` 2 := teBool_xor
]
tyBool :: Source src => LenInj vs => Type src vs Bool
tyBool = tyConst @(K Bool) @Bool
teBool :: Source src => SymInj ss Bool => Bool -> Term src ss ts '[] (() #> Bool)
teBool b = Term noConstraint tyBool $ teSym @Bool $ bool b
teBool_not :: TermDef Bool '[] (() #> (Bool -> Bool))
teBool_not = Term noConstraint (tyBool ~> tyBool) $ teSym @Bool $ lam1 not
teBool_and, teBool_or, teBool_xor :: TermDef Bool '[] (() #> (Bool -> Bool -> Bool))
teBool_and = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (&&)
teBool_or = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (||)
teBool_xor = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 xor