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_from is ast
 112  ) => Term_fromI is (Proxy Bool) ast where
 113         term_fromI ast ctx k =
 114                 case ast_lexem ast of
 115                  "True"  -> k tyBool $ TermLC $ \_c -> bool True
 116                  "False" -> k tyBool $ TermLC $ \_c -> bool False
 117                  "not" -> op1_from not
 118                  "&&"  -> op2_from (&&)
 119                  "||"  -> op2_from (||)
 120                  "xor" -> op2_from xor
 121                  _ -> Left $ Error_Term_unsupported
 122                 where
 123                 op1_from (op::forall term. Sym_Bool term => term Bool -> term Bool) =
 124                         case ast_nodes ast of
 125                          [] -> k (tyBool ~> tyBool) $ TermLC $
 126                                  \_c -> lam op
 127                          [ast_x] ->
 128                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
 129                                 check_type (At Nothing tyBool) (At (Just ast_x) ty_x) $ \Refl ->
 130                                 k tyBool $ TermLC $
 131                                  \c -> op (x c)
 132                          _ -> Left $ Error_Term_Syntax $
 133                                 Error_Syntax_too_many_arguments $ At (Just ast) 1
 134                 op2_from (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
 135                         case ast_nodes ast of
 136                          [] -> k (tyBool ~> tyBool ~> tyBool) $ TermLC $
 137                                  \_c -> lam $ lam . op
 138                          [ast_x] ->
 139                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
 140                                 check_type (At Nothing tyBool) (At (Just ast_x) ty_x) $ \Refl ->
 141                                 k (tyBool ~> tyBool) $ TermLC $
 142                                  \c -> lam $ op (x c)
 143                          [ast_x, ast_y] ->
 144                                 term_from ast_x ctx $ \ty_x (TermLC x) ->
 145                                 term_from ast_y ctx $ \ty_y (TermLC y) ->
 146                                 check_type (At Nothing tyBool) (At (Just ast_x) ty_x) $ \Refl ->
 147                                 check_type (At Nothing tyBool) (At (Just ast_y) ty_y) $ \Refl ->
 148                                 k tyBool $ TermLC $
 149                                  \c -> op (x c) (y c)
 150                          _ -> Left $ Error_Term_Syntax $
 151                                 Error_Syntax_too_many_arguments $ At (Just ast) 2
 152
 153 -- | The 'Bool' 'Type'
 154 tyBool :: Inj_Const cs Bool => Type cs Bool
 155 tyBool = TyConst inj_const
 156
 157 sym_Bool :: Proxy Sym_Bool
 158 sym_Bool = Proxy
 159
 160 syBool :: IsString a => Syntax a
 161 syBool = Syntax "Bool" []
 162
 163 syTrue :: IsString a => Syntax a
 164 syTrue = Syntax "True" []
 165
 166 syFalse :: IsString a => Syntax a
 167 syFalse = Syntax "False" []