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