TFHOE/Expr/Bool.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE Rank2Types #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 -- {-# LANGUAGE ViewPatterns #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# OPTIONS_GHC -fno-warn-orphans #-}
  10 module TFHOE.Expr.Bool where
  11
  12 import Data.Proxy (Proxy(..))
  13 import Prelude hiding (and, or)
  14
  15 import TFHOE.Raw
  16 import TFHOE.Type
  17 import TFHOE.Expr.Common
  18 import TFHOE.Expr.Fun ()
  19 import TFHOE.Repr.Dup
  20
  21 -- * Class 'Expr_Bool'
  22
  23 -- | Symantics combinable with 'Type_Bool'.
  24 class Expr_Bool repr where
  25         bool :: Bool -> repr Bool
  26         neg :: repr Bool -> repr Bool
  27         and :: repr Bool -> repr Bool -> repr Bool
  28         or  :: repr Bool -> repr Bool -> repr Bool
  29         xor :: repr Bool -> repr Bool -> repr Bool
  30         xor x y = (x `or` y) `and` neg (x `and` y)
  31
  32 type instance Expr_from_Type (Type_Bool next) repr
  33  = ( Expr_Bool repr
  34    , Expr_from_Type next repr )
  35
  36 instance -- Expr_Bool Dup
  37  ( Expr_Bool r1
  38  , Expr_Bool r2
  39  ) => Expr_Bool (Dup r1 r2) where
  40         bool x = bool x `Dup` bool x
  41         neg (x1 `Dup` x2)               = neg x1    `Dup` neg x2
  42         and (x1 `Dup` x2) (y1 `Dup` y2) = and x1 y1 `Dup` and x2 y2
  43         or  (x1 `Dup` x2) (y1 `Dup` y2) = or  x1 y1 `Dup` or  x2 y2
  44         xor (x1 `Dup` x2) (y1 `Dup` y2) = xor x1 y1 `Dup` xor x2 y2
  45 instance -- Expr_from Raw Type_Bool Type_Fun_Bool
  46  ( Type_from Raw next
  47  , Expr_from Raw next (Type_Fun_Bool fun next)
  48  ) => Expr_from Raw (Type_Bool next) (Type_Fun_Bool fun next) where
  49         expr_from _px_ty _px_ty_end _ctx (Raw "bool" [Raw raw_bool []]) k = do
  50                 (i::Bool) <- read_safe raw_bool
  51                 k (Type_Fun_Next Type_Bool) $ Forall_Repr_with_Context $
  52                         const $ bool i
  53         expr_from _px_ty px_ty_end ctx (Raw "neg" [raw_x]) k =
  54                 expr_from px_ty_end px_ty_end ctx raw_x $ \ty_x (Forall_Repr_with_Context x) ->
  55                         case ty_x of
  56                          Type_Fun_Next Type_Bool ->
  57                                 k ty_x $ Forall_Repr_with_Context $
  58                                         neg . x
  59                          _ -> Left "Error: neg: the operand is not a Bool"
  60         expr_from _px_ty px_ty_end ctx (Raw op_name@"and" [raw_x, raw_y]) k =
  61                 expr_from px_ty_end px_ty_end ctx raw_x $ \ty_x (Forall_Repr_with_Context x) ->
  62                 expr_from px_ty_end px_ty_end ctx raw_y $ \ty_y (Forall_Repr_with_Context y) ->
  63                         case (ty_x, ty_y) of
  64                          (  Type_Fun_Next Type_Bool
  65                           , Type_Fun_Next Type_Bool ) ->
  66                                 k ty_x $ Forall_Repr_with_Context $
  67                                  \c -> x c `and` y c
  68                          _ -> Left $ "Error: "++op_name++": at least one operand is not a Bool"
  69         expr_from _px_ty px_ty_end ctx (Raw op_name@"or" [raw_x, raw_y]) k =
  70                 expr_from px_ty_end px_ty_end ctx raw_x $ \ty_x (Forall_Repr_with_Context x) ->
  71                 expr_from px_ty_end px_ty_end ctx raw_y $ \ty_y (Forall_Repr_with_Context y) ->
  72                         case (ty_x, ty_y) of
  73                          (  Type_Fun_Next Type_Bool
  74                           , Type_Fun_Next Type_Bool ) ->
  75                                 k ty_x $ Forall_Repr_with_Context $
  76                                  \c -> x c `or` y c
  77                          _ -> Left $ "Error: "++op_name++": at least one operand is not a Bool"
  78         expr_from _px_ty px_ty_end ctx (Raw op_name@"xor" [raw_x, raw_y]) k =
  79                 expr_from px_ty_end px_ty_end ctx raw_x $ \ty_x (Forall_Repr_with_Context x) ->
  80                 expr_from px_ty_end px_ty_end ctx raw_y $ \ty_y (Forall_Repr_with_Context y) ->
  81                         case (ty_x, ty_y) of
  82                          (  Type_Fun_Next Type_Bool
  83                           , Type_Fun_Next Type_Bool ) ->
  84                                 k ty_x $ Forall_Repr_with_Context $
  85                                  \c -> x c `xor` y c
  86                          _ -> Left $ "Error: "++op_name++": at least one operand is not a Bool"
  87         expr_from _px_ty px_ty_end ctx raw k =
  88                 expr_from (Proxy::Proxy next) px_ty_end ctx raw k
  89 instance Expr_from Raw Type_End (Type_Fun_Bool fun Type_End) where
  90         expr_from _px_ty _px_ty_end _ctx raw _k =
  91                 Left $ "Error: invalid Type_Fun_Bool: " ++ show raw
  92
  93 expr_fun_bool_from
  94  :: forall fun raw next.
  95  ( Expr_from raw (Type_Fun_Bool fun next)
  96                  (Type_Fun_Bool fun next)
  97  )
  98  => Proxy fun
  99  -> Proxy next
 100  -> raw
 101  -> Either Error_Type
 102            (Exists_Type_and_Repr
 103             (Type_Fun_Bool fun next)
 104             (Forall_Repr (Type_Fun_Bool fun next)))
 105 expr_fun_bool_from _px_call _px_next raw =
 106         expr_from
 107          (Proxy::Proxy (Type_Fun_Bool fun next))
 108          (Proxy::Proxy (Type_Fun_Bool fun next))
 109          Context_Empty raw $ \ty (Forall_Repr_with_Context repr) ->
 110                 Right $ Exists_Type_and_Repr ty $
 111                         Forall_Repr $ repr Context_Empty