Language/Symantic/Compiling/Bool.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Bool'.
   4 module Language.Symantic.Compiling.Bool where
   5
   6 import Control.Monad
   7 import qualified Data.Bool as Bool
   8 import Data.Monoid
   9 import Data.Proxy
  10 import Data.Text (Text)
  11 import qualified Data.Text as Text
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Prelude hiding ((&&), not, (||))
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling.Term
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  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
  26         (||) :: term Bool -> term Bool -> term Bool
  27         xor  :: term Bool -> term Bool -> term Bool
  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 infixr 2 ||
  41 infixr 2 `xor`
  42 infixr 3 &&
  43
  44 type instance Sym_of_Iface (Proxy Bool) = Sym_Bool
  45 type instance Consts_of_Iface (Proxy Bool) = Proxy Bool ': Consts_imported_by Bool
  46 type instance Consts_imported_by Bool =
  47  [ Proxy Bounded
  48  , Proxy Enum
  49  , Proxy Eq
  50  , Proxy Ord
  51  , Proxy Show
  52  ]
  53
  54 instance Sym_Bool HostI where
  55         bool = HostI
  56         not  = liftM Bool.not
  57         (&&) = liftM2 (Bool.&&)
  58         (||) = liftM2 (Bool.||)
  59 instance Sym_Bool TextI where
  60         bool a = TextI $ \_p _v ->
  61                 Text.pack (show a)
  62         not (TextI x) =
  63                 TextI $ \p v ->
  64                         let p' = Precedence 9 in
  65                         paren p p' $ "not " <> x p' v
  66         (&&) = textI_infix "&&"    (Precedence 6)
  67         (||) = textI_infix "||"    (Precedence 5)
  68         xor  = textI_infix "`xor`" (Precedence 5)
  69 instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
  70         bool x = bool x `DupI` bool x
  71         not  = dupI1 (Proxy @Sym_Bool) not
  72         (&&) = dupI2 (Proxy @Sym_Bool) (&&)
  73         (||) = dupI2 (Proxy @Sym_Bool) (||)
  74         xor  = dupI2 (Proxy @Sym_Bool) xor
  75
  76 instance
  77  ( Read_TypeNameR Text cs rs
  78  , Inj_Const cs Bool
  79  ) => Read_TypeNameR Text cs (Proxy Bool ': rs) where
  80         read_typenameR _cs "Bool" k = k (ty @Bool)
  81         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  82 instance Show_Const cs => Show_Const (Proxy Bool ': cs) where
  83         show_const ConstZ{} = "Bool"
  84         show_const (ConstS c) = show_const c
  85
  86 instance -- Proj_ConC
  87  ( Proj_Const cs Bool
  88  , Proj_Consts cs (Consts_imported_by Bool)
  89  ) => Proj_ConC cs (Proxy Bool) where
  90         proj_conC _ (TyConst q :$ TyConst c)
  91          | Just Refl <- eq_skind (kind_of_const c) SKiType
  92          , Just Refl <- proj_const c (Proxy::Proxy Bool)
  93          = case () of
  94                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Con
  95                    | Just Refl <- proj_const q (Proxy::Proxy Enum)    -> Just Con
  96                    | Just Refl <- proj_const q (Proxy::Proxy Eq)      -> Just Con
  97                    | Just Refl <- proj_const q (Proxy::Proxy Ord)     -> Just Con
  98                    | Just Refl <- proj_const q (Proxy::Proxy Show)    -> Just Con
  99                  _ -> Nothing
 100         proj_conC _c _q = Nothing
 101 data instance TokenT meta (ts::[*]) (Proxy Bool)
 102  = Token_Term_Bool Bool
 103  | Token_Term_Bool_not
 104  | Token_Term_Bool_and
 105  | Token_Term_Bool_or
 106  | Token_Term_Bool_xor
 107 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Bool))
 108 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Bool))
 109 instance -- CompileI
 110  ( Inj_Const (Consts_of_Ifaces is) Bool
 111  , Inj_Const (Consts_of_Ifaces is) (->)
 112  ) => CompileI is (Proxy Bool) where
 113         compileI tok _ctx k =
 114                 case tok of
 115                  Token_Term_Bool b -> k (ty @Bool) $ TermO $ \_c -> bool b
 116                  Token_Term_Bool_not -> op1_from not
 117                  Token_Term_Bool_and -> op2_from (&&)
 118                  Token_Term_Bool_or  -> op2_from (||)
 119                  Token_Term_Bool_xor -> op2_from xor
 120                 where
 121                 op1_from
 122                  (op::forall term. Sym_Bool term => term Bool -> term Bool) =
 123                         k (ty @Bool ~> ty @Bool) $ TermO $ \_c -> lam op
 124                 op2_from
 125                         (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
 126                         k (ty @Bool ~> ty @Bool ~> ty @Bool) $ TermO $ \_c -> lam $ lam . op