symantic-lib/Language/Symantic/Lib/Bool.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Bool'.
   4 module Language.Symantic.Lib.Bool where
   5
   6 import Control.Monad
   7 import Data.Proxy
   8 import Data.Type.Equality ((:~:)(Refl))
   9 import Prelude hiding ((&&), not, (||))
  10 import qualified Data.Bool as Bool
  11 import qualified Data.Text as Text
  12
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling
  16 import Language.Symantic.Interpreting
  17 import Language.Symantic.Transforming
  18 import Language.Symantic.Lib.Lambda
  19 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
  20
  21 -- * Class 'Sym_Bool'
  22 class Sym_Bool term where
  23         bool ::      Bool -> term Bool
  24         not  :: term Bool -> term Bool
  25         (&&) :: term Bool -> term Bool -> term Bool; infixr 3 &&
  26         (||) :: term Bool -> term Bool -> term Bool; infixr 2 ||
  27         xor  :: term Bool -> term Bool -> term Bool; infixr 2 `xor`
  28         xor x y = (x || y) && not (x && y)
  29
  30         default bool :: Trans t term =>        Bool -> t term Bool
  31         default not  :: Trans t term => t term Bool -> t term Bool
  32         default (&&) :: Trans t term => t term Bool -> t term Bool -> t term Bool
  33         default (||) :: Trans t term => t term Bool -> t term Bool -> t term Bool
  34
  35         bool = trans_lift . bool
  36         not  = trans_map1 not
  37         (&&) = trans_map2 (&&)
  38         (||) = trans_map2 (||)
  39
  40 type instance Sym_of_Iface (Proxy Bool) = Sym_Bool
  41 type instance TyConsts_of_Iface (Proxy Bool) = Proxy Bool ': TyConsts_imported_by (Proxy Bool)
  42 type instance TyConsts_imported_by (Proxy Bool) =
  43  [ Proxy Bounded
  44  , Proxy Enum
  45  , Proxy Eq
  46  , Proxy Ord
  47  , Proxy Show
  48  ]
  49
  50 instance Sym_Bool HostI where
  51         bool = HostI
  52         not  = liftM Bool.not
  53         (&&) = liftM2 (Bool.&&)
  54         (||) = liftM2 (Bool.||)
  55 instance Sym_Bool TextI where
  56         bool o = TextI $ \_p _v ->
  57                 Text.pack (show o)
  58         not  = textI1 "not"
  59         (&&) = textI_infix "&&"    (infixR 3)
  60         (||) = textI_infix "||"    (infixR 2)
  61         xor  = textI_infix "`xor`" (infixR 2)
  62 instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
  63         bool b = bool b `DupI` bool b
  64         not  = dupI1 @Sym_Bool not
  65         (&&) = dupI2 @Sym_Bool (&&)
  66         (||) = dupI2 @Sym_Bool (||)
  67         xor  = dupI2 @Sym_Bool xor
  68
  69 instance
  70  ( Read_TyNameR TyName cs rs
  71  , Inj_TyConst cs Bool
  72  ) => Read_TyNameR TyName cs (Proxy Bool ': rs) where
  73         read_TyNameR _cs (TyName "Bool") k = k (ty @Bool)
  74         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  75 instance Show_TyConst cs => Show_TyConst (Proxy Bool ': cs) where
  76         show_TyConst TyConstZ{} = "Bool"
  77         show_TyConst (TyConstS c) = show_TyConst c
  78
  79 instance Proj_TyFamC cs TyFam_MonoElement Bool
  80
  81 instance -- Proj_TyConC
  82  ( Proj_TyConst cs Bool
  83  , Proj_TyConsts cs (TyConsts_imported_by (Proxy Bool))
  84  ) => Proj_TyConC cs (Proxy Bool) where
  85         proj_TyConC _ (TyConst q :$ TyConst c)
  86          | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
  87          , Just Refl <- proj_TyConst c (Proxy @Bool)
  88          = case () of
  89                  _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
  90                    | Just Refl <- proj_TyConst q (Proxy @Enum)    -> Just TyCon
  91                    | Just Refl <- proj_TyConst q (Proxy @Eq)      -> Just TyCon
  92                    | Just Refl <- proj_TyConst q (Proxy @Ord)     -> Just TyCon
  93                    | Just Refl <- proj_TyConst q (Proxy @Show)    -> Just TyCon
  94                  _ -> Nothing
  95         proj_TyConC _c _q = Nothing
  96 data instance TokenT meta (ts::[*]) (Proxy Bool)
  97  = Token_Term_Bool Bool
  98  | Token_Term_Bool_not
  99  | Token_Term_Bool_and
 100  | Token_Term_Bool_or
 101  | Token_Term_Bool_xor
 102 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Bool))
 103 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Bool))
 104
 105 instance -- CompileI
 106  ( Inj_TyConst cs Bool
 107  , Inj_TyConst cs (->)
 108  ) => CompileI cs is (Proxy Bool) where
 109         compileI tok _ctx k =
 110                 case tok of
 111                  Token_Term_Bool b -> k (ty @Bool) $ Term $ \_c -> bool b
 112                  Token_Term_Bool_not -> op1_from not
 113                  Token_Term_Bool_and -> op2_from (&&)
 114                  Token_Term_Bool_or  -> op2_from (||)
 115                  Token_Term_Bool_xor -> op2_from xor
 116                 where
 117                 op1_from
 118                  (op::forall term. Sym_Bool term => term Bool -> term Bool) =
 119                         k (ty @Bool ~> ty @Bool) $ Term $ \_c -> lam op
 120                 op2_from
 121                         (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
 122                         k (ty @Bool ~> ty @Bool ~> ty @Bool) $ Term $ \_c -> lam $ lam . op
 123 instance -- TokenizeT
 124  Inj_Token meta ts Bool =>
 125  TokenizeT meta ts (Proxy Bool) where
 126         tokenizeT _t = mempty
 127          { tokenizers_infix = tokenizeTMod []
 128                  [ tokenize0 "False" infixN5 $  Token_Term_Bool False
 129                  , tokenize0 "True"  infixN5 $  Token_Term_Bool True
 130                  , tokenize0 "not"   infixN5    Token_Term_Bool_not
 131                  , tokenize0 "and"   (infixR 3) Token_Term_Bool_and
 132                  , tokenize0 "or"    (infixR 2) Token_Term_Bool_or
 133                  , tokenize0 "xor"   (infixR 2) Token_Term_Bool_xor
 134                  ]
 135          }
 136 instance Gram_Term_AtomsT meta ts (Proxy Bool) g