Language/LOL/Symantic/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, not, or)
  17
  18 import Language.LOL.Symantic.Repr
  19 import Language.LOL.Symantic.AST
  20 import Language.LOL.Symantic.Expr
  21 import Language.LOL.Symantic.Type
  22 -- import Language.LOL.Symantic.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` not (bool False)
  50 e5 = bool True `and` not x
  51 e6 = x `xor` y
  52 e7 = (x `xor` y) `xor` z
  53 e8 = x `xor` (y `xor` bool True)
  54
  55 (==>) :: forall h raw.
  56       ( Eq h, Eq raw, Show h, Show raw
  57       , Sym_from raw (Expr_Lambda IO (Expr_Lambda_Bool IO))
  58       , Sym_from raw (Expr_Bool      (Expr_Lambda_Bool IO)))
  59       => raw -> (Type_Fun_Bool IO h, h, String) -> TestTree
  60 (==>) raw expected@(ty_expected::Type_Fun_Bool IO h, _::h, _::String) =
  61         testCase (show raw) $
  62                 (>>= (@?= Right expected)) $
  63                 case expr_lambda_bool_from (Proxy::Proxy IO) raw of
  64                  Left err -> return $ Left err
  65                  Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  66                         case ty `type_eq` ty_expected of
  67                          Nothing -> return $ Left $ Nothing -- Just $ "Type mismatch"
  68                          Just Refl -> do
  69                                 h <- host_repr r
  70                                 return $
  71                                         Right
  72                                          ( ty
  73                                          , h
  74                                          , string_repr r
  75                                          -- , (string_repr :: Repr_String IO h -> String) r
  76                                          )
  77
  78 tests :: TestTree
  79 tests = testGroup "Bool" $
  80  [ AST "bool" [AST "True" []] ==>
  81          ( type_bool
  82          , True
  83          , "True" )
  84  , AST "xor"
  85          [ AST "bool" [AST "True" []]
  86          , AST "bool" [AST "True" []]
  87          ] ==>
  88          ( type_bool
  89          , False
  90          , "(True | True) & !(True & True)" )
  91  , AST "app"
  92          [ AST "val"
  93                  [ AST "x" []
  94                  , AST "Bool" []
  95                  , AST "var" [AST "x" []]
  96                  ]
  97          , AST "bool" [AST "True" []]
  98          ] ==>
  99          ( type_bool
 100          , True
 101          , "(\\x0 -> x0) True" )
 102  , AST "app"
 103          [ AST "val"
 104                  [ AST "x" []
 105                  , AST "Bool" []
 106                  , AST "xor"
 107                          [ AST "var" [AST "x" []]
 108                          , AST "bool" [AST "True" []]
 109                          ]
 110                  ]
 111          , AST "bool" [AST "True" []]
 112          ] ==>
 113          ( type_bool
 114          , False
 115          , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
 116  ]