Language/Symantic/Compiling/Bool.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 -- | Symantic for 'Bool'.
  14 module Language.Symantic.Compiling.Bool where
  15
  16 import Control.Monad
  17 import qualified Data.Bool as Bool
  18 import Data.Monoid
  19 import Data.Proxy
  20 import Data.String (IsString)
  21 import Data.Text (Text)
  22 import Data.Type.Equality ((:~:)(Refl))
  23 import qualified Data.Text as Text
  24 import Prelude hiding ((&&), not, (||))
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Interpreting
  29 import Language.Symantic.Transforming.Trans
  30
  31 -- * Class 'Sym_Bool'
  32 class Sym_Bool term where
  33         bool ::      Bool -> term Bool
  34         not  :: term Bool -> term Bool
  35         (&&) :: term Bool -> term Bool -> term Bool
  36         (||) :: term Bool -> term Bool -> term Bool
  37         xor  :: term Bool -> term Bool -> term Bool
  38         xor x y = (x || y) && not (x && y)
  39
  40         default bool :: Trans t term =>        Bool -> t term Bool
  41         default not  :: Trans t term => t term Bool -> t term Bool
  42         default (&&) :: Trans t term => t term Bool -> t term Bool -> t term Bool
  43         default (||) :: Trans t term => t term Bool -> t term Bool -> t term Bool
  44
  45         bool = trans_lift . bool
  46         not  = trans_map1 not
  47         (&&) = trans_map2 (&&)
  48         (||) = trans_map2 (||)
  49
  50 infixr 2 ||
  51 infixr 2 `xor`
  52 infixr 3 &&
  53
  54 type instance Sym_of_Iface (Proxy Bool) = Sym_Bool
  55 type instance Consts_of_Iface (Proxy Bool) = Proxy Bool ': Consts_imported_by Bool
  56 type instance Consts_imported_by Bool =
  57  [ Proxy Bounded
  58  , Proxy Enum
  59  , Proxy Eq
  60  , Proxy Ord
  61  ]
  62
  63 instance Sym_Bool HostI where
  64         bool = HostI
  65         not  = liftM Bool.not
  66         (&&) = liftM2 (Bool.&&)
  67         (||) = liftM2 (Bool.||)
  68 instance Sym_Bool TextI where
  69         bool a = TextI $ \_p _v ->
  70                 Text.pack (show a)
  71         not (TextI x) =
  72                 TextI $ \p v ->
  73                         let p' = Precedence 9 in
  74                         paren p p' $ "not " <> x p' v
  75         (&&) = textI_infix "&&"    (Precedence 6)
  76         (||) = textI_infix "||"    (Precedence 5)
  77         xor  = textI_infix "`xor`" (Precedence 5)
  78 instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
  79         bool x = bool x `DupI` bool x
  80         not  = dupI1 sym_Bool not
  81         (&&) = dupI2 sym_Bool (&&)
  82         (||) = dupI2 sym_Bool (||)
  83         xor  = dupI2 sym_Bool xor
  84
  85 instance Const_from Text cs => Const_from Text (Proxy Bool ': cs) where
  86         const_from "Bool" k = k (ConstZ kind)
  87         const_from s k = const_from s $ k . ConstS
  88 instance Show_Const cs => Show_Const (Proxy Bool ': cs) where
  89         show_const ConstZ{} = "Bool"
  90         show_const (ConstS c) = show_const c
  91
  92 instance -- Proj_ConC
  93  ( Proj_Const cs Bool
  94  , Proj_Consts cs (Consts_imported_by Bool)
  95  ) => Proj_ConC cs (Proxy Bool) where
  96         proj_conC _ (TyConst q :$ TyConst c)
  97          | Just Refl <- eq_skind (kind_of_const c) SKiType
  98          , Just Refl <- proj_const c (Proxy::Proxy Bool)
  99          = Just $ case () of
 100                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Con
 101                    | Just Refl <- proj_const q (Proxy::Proxy Enum)    -> Just Con
 102                    | Just Refl <- proj_const q (Proxy::Proxy Eq)      -> Just Con
 103                    | Just Refl <- proj_const q (Proxy::Proxy Ord)     -> Just Con
 104                  _ -> Nothing
 105         proj_conC _c _q = Nothing
 106 instance -- Term_fromI
 107  ( AST ast
 108  , Lexem ast ~ LamVarName
 109  , Inj_Const (Consts_of_Ifaces is) Bool
 110  , Inj_Const (Consts_of_Ifaces is) (->)
 111  ) => Term_fromI is (Proxy Bool) ast where
 112         term_fromI ast _ctx k =
 113                 case ast_lexem ast of
 114                  "True"  -> k (ast_nodes ast) tyBool $ TermLC $ \_c -> bool True
 115                  "False" -> k (ast_nodes ast) tyBool $ TermLC $ \_c -> bool False
 116                  "not"   -> op1_from not
 117                  "&&"    -> op2_from (&&)
 118                  "||"    -> op2_from (||)
 119                  "xor"   -> op2_from xor
 120                  _ -> Left $ Error_Term_unsupported
 121                 where
 122                 op1_from (op::forall term. Sym_Bool term => term Bool -> term Bool) =
 123                         from_ast0 ast $ \_lex as ->
 124                         k as (tyBool ~> tyBool) $ TermLC $
 125                          \_c -> lam op
 126                 op2_from (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
 127                         from_ast0 ast $ \_lex as ->
 128                         k as (tyBool ~> tyBool ~> tyBool) $ TermLC $
 129                          \_c -> lam $ lam . op
 130
 131 -- | The 'Bool' 'Type'
 132 tyBool :: Inj_Const cs Bool => Type cs Bool
 133 tyBool = TyConst inj_const
 134
 135 sym_Bool :: Proxy Sym_Bool
 136 sym_Bool = Proxy
 137
 138 syBool :: IsString a => Syntax a
 139 syBool = Syntax "Bool" []
 140
 141 syTrue :: IsString a => Syntax a
 142 syTrue = Syntax "True" []
 143
 144 syFalse :: IsString a => Syntax a
 145 syFalse = Syntax "False" []