TFHOE/Expr/Bool/Test.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE NoMonomorphismRestriction #-}
   4 {-# LANGUAGE Rank2Types #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   7 module Expr.Bool.Test where
   8
   9 import Test.Tasty
  10 import Test.Tasty.HUnit
  11
  12 -- import Data.Functor.Identity (Identity)
  13 -- import Control.Monad.IO.Class (MonadIO(..))
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Prelude hiding (and, or)
  17
  18 import TFHOE.Repr
  19 import TFHOE.Raw
  20 import TFHOE.Expr
  21 import TFHOE.Type
  22 -- import TFHOE.Expr.Trans
  23
  24 -- * Class 'Expr_Bool_Vars'
  25
  26 -- | A few boolean variables.
  27 class Expr_Bool_Vars repr where
  28         x :: repr Bool
  29         y :: repr Bool
  30         z :: repr Bool
  31 instance Expr_Bool_Vars (Repr_String fun) where
  32         x = Repr_String $ \_p _v -> "x"
  33         y = Repr_String $ \_p _v -> "y"
  34         z = Repr_String $ \_p _v -> "z"
  35 {-
  36 instance -- Trans_Boo_Const
  37  ( Expr_Bool_Vars repr
  38  , Expr_Lit repr
  39  ) => Expr_Bool_Vars (Trans_Bool_Const repr) where
  40         x = trans_lift x
  41         y = trans_lift y
  42         z = trans_lift z
  43 -}
  44
  45 -- * 'Expr's
  46 e1 = bool True `and` bool False
  47 e2 = (bool True `and` bool False) `or`  (bool True `and` bool True)
  48 e3 = (bool True `or`  bool False) `and` (bool True `or`  bool True)
  49 e4 = bool True `and` neg (bool False)
  50 e5 = bool True `and` neg x
  51 e6 = x `xor` y
  52 e7 = (x `xor` y) `xor` z
  53 e8 = x `xor` (y `xor` bool True)
  54
  55 (==>) raw expected@(ty_expected::Type_Fun_Bool_Int IO Type_End h, _::h, _::String) =
  56         testCase (show raw) $
  57                 (>>= (@?= Right expected)) $
  58                 case expr_fun_bool_int_from Proxy Proxy raw of
  59                  Left err -> return $ Left err
  60                  Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  61                         case ty `type_eq` ty_expected of
  62                          Nothing -> return $ Left "Type mismatch"
  63                          Just Refl -> do
  64                                 h <- host_repr r
  65                                 return $
  66                                         Right
  67                                          ( ty
  68                                          , h
  69                                          , string_repr r
  70                                          -- , (string_repr :: Repr_String IO h -> String) r
  71                                          )
  72
  73 tests :: TestTree
  74 tests = testGroup "Bool" $
  75  [ Raw "bool" [Raw "True" []] ==>
  76          ( Type_Fun_Next Type_Bool
  77          , True
  78          , "True" )
  79  , Raw "xor"
  80          [ Raw "bool" [Raw "True" []]
  81          , Raw "bool" [Raw "True" []]
  82          ] ==>
  83          ( Type_Fun_Next Type_Bool
  84          , False
  85          , "(True | True) & !(True & True)" )
  86  , Raw "app"
  87          [ Raw "val"
  88                  [ Raw "x" []
  89                  , Raw "Bool" []
  90                  , Raw "var" [Raw "x" []]
  91                  ]
  92          , Raw "bool" [Raw "True" []]
  93          ] ==>
  94          ( Type_Fun_Next Type_Bool
  95          , True
  96          , "(\\x0 -> x0) True" )
  97  , Raw "app"
  98          [ Raw "val"
  99                  [ Raw "x" []
 100                  , Raw "Bool" []
 101                  , Raw "xor"
 102                          [ Raw "var" [Raw "x" []]
 103                          , Raw "bool" [Raw "True" []]
 104                          ]
 105                  ]
 106          , Raw "bool" [Raw "True" []]
 107          ] ==>
 108          ( Type_Fun_Next Type_Bool
 109          , False
 110          , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
 111  ]
 112
 113 {-
 114 -- * Bool
 115 raw_ty_bool :: Raw
 116 raw_ty_bool = Raw "Bool" []
 117
 118 ty_bool
 119  :: forall repr.
 120  Either Error_Type (Type_Fun_Bool_End repr Bool)
 121 ty_bool = type_from raw_ty_bool $ \(ty::Type_Fun_Bool_End repr h) ->
 122         case ty of
 123          Type_Fun_Next Type_Bool -> Right ty
 124          _ -> Left "error"
 125
 126 -- ** Bool -> Bool
 127 raw_ty_bool2bool :: Raw
 128 raw_ty_bool2bool = Raw "->" [Raw "Bool" [], Raw "Bool" []]
 129
 130 ty0_bool2bool
 131  :: forall repr.
 132  Either Error_Type (Type_Fun_Bool_End repr (repr Bool -> repr Bool))
 133 ty0_bool2bool = type_from raw_ty_bool2bool $ \(ty::Type_Fun_Bool_End repr h) ->
 134         case ty of
 135          Type_Fun
 136           (Type_Fun_Next Type_Bool)
 137           (Type_Fun_Next Type_Bool) -> Right ty
 138          _ -> Left "error"
 139
 140 -- ** Bool -> Bool
 141 raw_xor_true :: Raw
 142 raw_xor_true =
 143         Raw "lam"
 144          [ Raw "x" []
 145          , raw_ty_bool
 146          , Raw "xor"
 147                  [ Raw "var" [Raw "x" []]
 148                  , Raw "bool" [Raw "True" []]
 149                  ]
 150          ]
 151
 152 expr_bool_xor_true
 153  :: forall repr. MonadIO repr =>
 154  Either Error_Type (repr (Repr_Host repr Bool -> Repr_Host repr Bool))
 155 expr_bool_xor_true =
 156         expr_fun_bool_int_from
 157          (Proxy::Proxy Type_End)
 158          raw_xor_true $ \ty (repr::Repr_Host repr h) ->
 159                 case ty of
 160                  Type_Fun
 161                   (Type_Fun_Next Type_Bool)
 162                   (Type_Fun_Next Type_Bool) ->
 163                         Right $ meta_repr repr
 164                  _ -> Left "error"
 165 -}