{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Symantic for 'Bool'. module Language.Symantic.Lib.Bool where import Control.Monad import Data.Proxy import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding ((&&), not, (||)) import qualified Data.Bool as Bool import qualified Data.Text as Text import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling import Language.Symantic.Interpreting import Language.Symantic.Transforming import Language.Symantic.Lib.Lambda import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..)) -- * Class '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 :: Trans t term => Bool -> t term Bool default not :: Trans t term => t term Bool -> t term Bool default (&&) :: Trans t term => t term Bool -> t term Bool -> t term Bool default (||) :: Trans t term => t term Bool -> t term Bool -> t term Bool bool = trans_lift . bool not = trans_map1 not (&&) = trans_map2 (&&) (||) = trans_map2 (||) type instance Sym_of_Iface (Proxy Bool) = Sym_Bool type instance TyConsts_of_Iface (Proxy Bool) = Proxy Bool ': TyConsts_imported_by (Proxy Bool) type instance TyConsts_imported_by (Proxy Bool) = [ Proxy Bounded , Proxy Enum , Proxy Eq , Proxy Ord , Proxy Show ] instance Sym_Bool HostI where bool = HostI not = liftM Bool.not (&&) = liftM2 (Bool.&&) (||) = liftM2 (Bool.||) instance Sym_Bool TextI where bool o = TextI $ \_p _v -> Text.pack (show o) not = textI1 "not" (&&) = textI_infix "&&" (infixR 3) (||) = textI_infix "||" (infixR 2) xor = textI_infix "`xor`" (infixR 2) instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where bool b = bool b `DupI` bool b not = dupI1 @Sym_Bool not (&&) = dupI2 @Sym_Bool (&&) (||) = dupI2 @Sym_Bool (||) xor = dupI2 @Sym_Bool xor instance ( Read_TyNameR TyName cs rs , Inj_TyConst cs Bool ) => Read_TyNameR TyName cs (Proxy Bool ': rs) where read_TyNameR _cs (TyName "Bool") k = k (ty @Bool) read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k instance Show_TyConst cs => Show_TyConst (Proxy Bool ': cs) where show_TyConst TyConstZ{} = "Bool" show_TyConst (TyConstS c) = show_TyConst c instance Proj_TyFamC cs TyFam_MonoElement Bool instance -- Proj_TyConC ( Proj_TyConst cs Bool , Proj_TyConsts cs (TyConsts_imported_by (Proxy Bool)) ) => Proj_TyConC cs (Proxy Bool) where proj_TyConC _ (TyConst q :$ TyConst c) | Just Refl <- eq_skind (kind_of_TyConst c) SKiType , Just Refl <- proj_TyConst c (Proxy @Bool) = case () of _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon _ -> Nothing proj_TyConC _c _q = Nothing data instance TokenT meta (ts::[*]) (Proxy Bool) = Token_Term_Bool Bool | Token_Term_Bool_not | Token_Term_Bool_and | Token_Term_Bool_or | Token_Term_Bool_xor deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Bool)) deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Bool)) instance -- CompileI ( Inj_TyConst cs Bool , Inj_TyConst cs (->) ) => CompileI cs is (Proxy Bool) where compileI tok _ctx k = case tok of Token_Term_Bool b -> k (ty @Bool) $ Term $ \_c -> bool b Token_Term_Bool_not -> op1_from not Token_Term_Bool_and -> op2_from (&&) Token_Term_Bool_or -> op2_from (||) Token_Term_Bool_xor -> op2_from xor where op1_from (op::forall term. Sym_Bool term => term Bool -> term Bool) = k (ty @Bool ~> ty @Bool) $ Term $ \_c -> lam op op2_from (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) = k (ty @Bool ~> ty @Bool ~> ty @Bool) $ Term $ \_c -> lam $ lam . op instance -- TokenizeT Inj_Token meta ts Bool => TokenizeT meta ts (Proxy Bool) where tokenizeT _t = mempty { tokenizers_infix = tokenizeTMod [] [ tokenize0 "False" infixN5 $ Token_Term_Bool False , tokenize0 "True" infixN5 $ Token_Term_Bool True , tokenize0 "not" infixN5 Token_Term_Bool_not , tokenize0 "and" (infixR 3) Token_Term_Bool_and , tokenize0 "or" (infixR 2) Token_Term_Bool_or , tokenize0 "xor" (infixR 2) Token_Term_Bool_xor ] } instance Gram_Term_AtomsT meta ts (Proxy Bool) g