symantic-lib/Language/Symantic/Lib/Bool/Test.hs

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