{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Bool'. 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 () -- * Class 'Sym_Bool' 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 (||) -- Interpreting 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 -- Transforming instance (Sym_Lambda term, Sym_Bool term) => Sym_Bool (BetaT term) where xor = trans2 xor -- Typing instance ClassInstancesFor Bool where proveConstraintFor _ (TyApp _ (TyConst _ _ q) c) | Just HRefl <- proj_ConstKiTy @_ @Bool c = 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 -- Compiling 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 ] -- ** 'Type's tyBool :: Source src => LenInj vs => Type src vs Bool tyBool = tyConst @(K Bool) @Bool -- ** 'Term's 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