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.Parsing
  10 import Language.Symantic.Typing
  11 import Language.Symantic.Compiling
  12 import Language.Symantic.Interpreting
  13 import Language.Symantic.Lib.Bool
  14 import Language.Symantic.Lib.Lambda ((~>))
  15 import Compiling.Term.Test
  16
  17 type Ifaces =
  18  [ Proxy Bool
  19  , Proxy (->)
  20  , Proxy Integer
  21  ]
  22 (==>) = test_compile @Ifaces
  23
  24 tests :: TestTree
  25 tests = testGroup "Bool" $
  26  [ "True"            ==> Right (ty @Bool, True, "True")
  27  , "xor True True"   ==> Right (ty @Bool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
  28  , "xor False True"  ==> Right (ty @Bool, True, "((\\x0 -> (\\x1 -> x0 `xor` x1)) False) True")
  29  , "True `xor` True" ==> Right (ty @Bool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
  30  , "(\\(xy:Bool) -> xy) True" ==> Right (ty @Bool, True, "(\\x0 -> x0) True")
  31  , "(\\(False:Bool) -> False) True" ==> Right (ty @Bool, True, "(\\x0 -> x0) True")
  32  , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right
  33          (ty @Bool, True, "(\\x0 -> x0) (((\\x0 -> (\\x1 -> x0 `xor` x1)) False) True)")
  34  , "(\\(lett:Bool) -> lett) True" ==> Right (ty @Bool, True, "(\\x0 -> x0) True")
  35  , "(\\(x:Bool) -> xor x x) True" ==> Right
  36          (ty @Bool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) x0) True")
  37  , "let x = True in xor x True" ==> Right
  38          (ty @Bool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
  39  , testGroup "Error_Term"
  40          [ "True True" ==> Left (ty @Bool,
  41                 Right $ Error_Term_Con_Type $
  42                 Right $ Con_TyApp $
  43                 At (maybeRight $ test_tokenizer "True") $
  44                 EType $ ty @Bool)
  45          , "x" ==> Left (ty @Bool,
  46                 Right $ Error_Term_unbound $ TeName "x")
  47          , "x `xor` True" ==> Left (ty @Bool,
  48                 Right $ Error_Term_unbound $ TeName "x")
  49          , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (ty @Bool,
  50                 Right $ Error_Term_unbound $ TeName "Bool")
  51          , "(\\(x:Bool) -> x) True True" ==> Left (ty @Bool,
  52                 Right $ Error_Term_Con_Type $
  53                 Right $ Con_TyApp $
  54                 At (maybeRight $ test_tokenizer "(\\(x:Bool) -> x) True") $
  55                 EType $ ty @Bool)
  56          , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (ty @Bool,
  57                 Right $ Error_Term_Con_Type $ Right $
  58                 Con_TyEq
  59                  (Right $ At (maybeRight $ test_tokenizer "(\\(x:Bool -> Bool) -> x True)") $
  60                         EType $ (ty @Bool ~> ty @Bool))
  61                  (At (maybeRight $ test_tokenizer "True") $
  62                         EType $ ty @Bool)
  63                  )
  64          ]
  65  ]
  66
  67 -- * Class 'Sym_Bool_Vars'
  68 -- | A few boolean variables.
  69 class Sym_Bool_Vars repr where
  70         x :: repr Bool
  71         y :: repr Bool
  72         z :: repr Bool
  73 instance Sym_Bool_Vars TextI where
  74         x = TextI $ \_p _v -> "x"
  75         y = TextI $ \_p _v -> "y"
  76         z = TextI $ \_p _v -> "z"
  77 {-
  78 instance -- Trans_Boo_Const
  79  ( Sym_Bool repr
  80  , Sym_Bool_Vars repr
  81  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  82         x = trans_lift x
  83         y = trans_lift y
  84         z = trans_lift z
  85 -}
  86
  87 -- * EDSL tests
  88 te1 = bool True && bool False
  89 te2 = (bool True && bool False) ||  (bool True && bool True)
  90 te3 = (bool True ||  bool False) && (bool True ||  bool True)
  91 te4 = bool True && not (bool False)
  92 te5 = bool True && not x
  93 te6 = x `xor` y
  94 te7 = (x `xor` y) `xor` z
  95 te8 = x `xor` (y `xor` bool True)