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.
  55       ( Eq h, Eq raw, Show h, Show raw
  56       , Expr_from raw (Expr_Lambda IO (Expr_Lambda_Bool IO))
  57       , Expr_from raw (Expr_Bool      (Expr_Lambda_Bool IO)))
  58       => raw -> (Type_Fun_Bool IO h, h, String) -> TestTree
  59 (==>) raw expected@(ty_expected::Type_Fun_Bool IO h, _::h, _::String) =
  60         testCase (show raw) $
  61         (>>= (@?= Right expected)) $
  62         case expr_lambda_bool_from (Proxy::Proxy IO) raw of
  63          Left err -> return $ Left err
  64          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  65                 case ty `type_eq` ty_expected of
  66                  Nothing -> return $ Left $ Nothing -- Just $ "Type mismatch"
  67                  Just Refl -> do
  68                         h <- host_from_expr r
  69                         return $
  70                                 Right
  71                                  ( ty
  72                                  , h
  73                                  , string_from_expr r
  74                                  -- , (string_from_expr :: Repr_String IO h -> String) r
  75                                  )
  76
  77 tests :: TestTree
  78 tests = testGroup "Bool" $
  79  [ AST "bool" [AST "True" []] ==>
  80          ( type_bool
  81          , True
  82          , "True" )
  83  , AST "xor"
  84          [ AST "bool" [AST "True" []]
  85          , AST "bool" [AST "True" []]
  86          ] ==>
  87          ( type_bool
  88          , False
  89          , "(True | True) & !(True & True)" )
  90  , AST "app"
  91          [ AST "val"
  92                  [ AST "x" []
  93                  , AST "Bool" []
  94                  , AST "var" [AST "x" []]
  95                  ]
  96          , AST "bool" [AST "True" []]
  97          ] ==>
  98          ( type_bool
  99          , True
 100          , "(\\x0 -> x0) True" )
 101  , AST "app"
 102          [ AST "val"
 103                  [ AST "x" []
 104                  , AST "Bool" []
 105                  , AST "xor"
 106                          [ AST "var" [AST "x" []]
 107                          , AST "bool" [AST "True" []]
 108                          ]
 109                  ]
 110          , AST "bool" [AST "True" []]
 111          ] ==>
 112          ( type_bool
 113          , False
 114          , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
 115  ]