symantic-lib/test/HUnit/Bool.hs

   1 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   2 module HUnit.Bool where
   3
   4 import Test.Tasty
   5 import Data.Proxy (Proxy(..))
   6 import Prelude hiding ((&&), not, (||))
   7
   8 import Language.Symantic
   9 import Language.Symantic.Lib
  10 import Testing.Compiling
  11
  12 type SS =
  13  [ Proxy Bool
  14  , Proxy (->)
  15  , Proxy Integer
  16  , Proxy []
  17  , Proxy Char
  18  ]
  19 (==>) = readTe @() @SS
  20
  21 hunits :: TestTree
  22 hunits = testGroup "Bool" $
  23  [ "True"                           ==> Right (tyBool, True , "True")
  24  , "xor True True"                  ==> Right (tyBool, False, "True `xor` True")
  25  , "xor False True"                 ==> Right (tyBool, True , "False `xor` True")
  26  , "True `xor` True"                ==> Right (tyBool, False, "True `xor` True")
  27  , "(\\(xy:Bool) -> xy) True"       ==> Right (tyBool, True , "(\\x0 -> x0) True")
  28  , "(\\(False:Bool) -> False) True" ==> Right (tyBool, True , "(\\x0 -> x0) True")
  29  , "(\\(lett:Bool) -> lett) True"   ==> Right (tyBool, True , "(\\x0 -> x0) True")
  30  , "(\\(x:Bool) -> xor x x) True"   ==> Right (tyBool, False, "(\\x0 -> x0 `xor` x0) True")
  31  , "let x = True in xor x True"     ==> Right (tyBool, False, "let x0 = True in x0 `xor` True")
  32  , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right (tyBool, True, "(\\x0 -> x0) (False `xor` True)")
  33  , testGroup "Error_Term"
  34          [ "True True" ==> Left (tyBool,
  35                 Right $ Error_Term_Beta $
  36                 Error_Beta_Term_not_a_function $
  37                 TypeVT $ tyBool @_ @'[])
  38          , "x" ==> Left (tyBool,
  39                 Right $ Error_Term_unknown $ NameTe "x")
  40          , "x `xor` True" ==> Left (tyBool,
  41                 Right $ Error_Term_unknown $ NameTe "x")
  42          , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (tyBool,
  43                 Right $ Error_Term_unknown $ NameTe "Bool")
  44          , "(\\(x:Bool) -> x) True True" ==> Left (tyBool,
  45                 Right $ Error_Term_Beta $
  46                 Error_Beta_Term_not_a_function $
  47                 TypeVT $ tyBool @_ @'[])
  48          , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (tyBool,
  49                 Right $ Error_Term_Beta $ Error_Beta_Unify $
  50                 Error_Unify_Const_mismatch
  51                  (TypeVT $ tyFun @_ @'[])
  52                  (TypeVT $ tyBool @_ @'[]))
  53          ]
  54  ]
  55
  56 -- * Class 'Sym_Bool_Vars'
  57 -- | A few boolean variables.
  58 class Sym_Bool_Vars repr where
  59         x :: repr Bool
  60         y :: repr Bool
  61         z :: repr Bool
  62 instance Sym_Bool_Vars View where
  63         x = View $ \_p _v -> "x"
  64         y = View $ \_p _v -> "y"
  65         z = View $ \_p _v -> "z"
  66 {-
  67 instance -- Trans_Boo_Const
  68  ( Sym_Bool repr
  69  , Sym_Bool_Vars repr
  70  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  71         x = trans_lift x
  72         y = trans_lift y
  73         z = trans_lift z
  74 -}
  75
  76 -- * EDSL tests
  77 te1 = bool True && bool False
  78 te2 = (bool True && bool False) ||  (bool True && bool True)
  79 te3 = (bool True ||  bool False) && (bool True ||  bool True)
  80 te4 = bool True && not (bool False)
  81 te5 = bool True && not x
  82 te6 = x `xor` y
  83 te7 = (x `xor` y) `xor` z
  84 te8 = x `xor` (y `xor` bool True)