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.Trans
  23
  24 -- * Class 'Sym_Bool_Vars'
  25
  26 -- | A few boolean variables.
  27 class Sym_Bool_Vars repr where
  28         x :: repr Bool
  29         y :: repr Bool
  30         z :: repr Bool
  31 instance Sym_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 instance -- Trans_Boo_Const
  36  ( Sym_Bool repr
  37  , Sym_Bool_Vars repr
  38  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  39         x = trans_lift x
  40         y = trans_lift y
  41         z = trans_lift z
  42
  43 -- * Expressions
  44 e1 = bool True `and` bool False
  45 e2 = (bool True `and` bool False) `or`  (bool True `and` bool True)
  46 e3 = (bool True `or`  bool False) `and` (bool True `or`  bool True)
  47 e4 = bool True `and` not (bool False)
  48 e5 = bool True `and` not x
  49 e6 = x `xor` y
  50 e7 = (x `xor` y) `xor` z
  51 e8 = x `xor` (y `xor` bool True)
  52
  53 -- * Tests
  54 (==>) :: forall h raw root.
  55       ( Eq h, Eq raw, Show h, Show raw
  56       , root ~ Expr_Lambda_Bool IO
  57       , Expr_from raw (Expr_Lambda IO root)
  58       , Expr_from raw (Expr_Bool      root)
  59       )
  60       => raw -> (Type_Fun_Bool IO h, h, String) -> TestTree
  61 (==>) raw expected@(ty_expected::Type_Fun_Bool IO h, _::h, _::String) =
  62         testCase (show raw) $
  63         (>>= (@?= Right expected)) $
  64         case expr_lambda_bool_from (Proxy::Proxy IO) raw of
  65          Left err -> return $ Left err
  66          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  67                 case ty `type_eq` ty_expected of
  68                  Nothing -> return $ Left $
  69                         error_lambda_lift $ Error_Expr_Type
  70                          (error_type_lift $ Error_Type_Unsupported raw) raw
  71                  Just Refl -> do
  72                         h <- host_from_expr r
  73                         return $
  74                                 Right
  75                                  ( ty
  76                                  , h
  77                                  , string_from_expr r
  78                                  -- , (string_from_expr :: Repr_String IO h -> String) r
  79                                  )
  80         where
  81                 error_lambda_lift
  82                  :: (root ~ Expr_Lambda_Bool IO)
  83                  => Error_Expr_Lambda (Error_of_Type raw (Type_Root_of_Expr root))
  84                                       (Type_Root_of_Expr root)
  85                                       raw
  86                  -> Error_of_Expr raw root
  87                 error_lambda_lift = error_expr_lift
  88
  89 tests :: TestTree
  90 tests = testGroup "Bool" $
  91  [ AST "bool" [AST "True" []] ==>
  92          ( type_bool
  93          , True
  94          , "True" )
  95  , AST "xor"
  96          [ AST "bool" [AST "True" []]
  97          , AST "bool" [AST "True" []]
  98          ] ==>
  99          ( type_bool
 100          , False
 101          , "(True | True) & !(True & True)" )
 102  , AST "app"
 103          [ AST "val"
 104                  [ AST "x" []
 105                  , AST "Bool" []
 106                  , AST "var" [AST "x" []]
 107                  ]
 108          , AST "bool" [AST "True" []]
 109          ] ==>
 110          ( type_bool
 111          , True
 112          , "(\\x0 -> x0) True" )
 113  , AST "app"
 114          [ AST "val"
 115                  [ AST "x" []
 116                  , AST "Bool" []
 117                  , AST "xor"
 118                          [ AST "var" [AST "x" []]
 119                          , AST "bool" [AST "True" []]
 120                          ]
 121                  ]
 122          , AST "bool" [AST "True" []]
 123          ] ==>
 124          ( type_bool
 125          , False
 126          , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
 127  ]