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  , "(\\(x:Bool) -> x) 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_Constraint_Type $
  42                 Right $ Constraint_Type_App $
  43                 At (maybeRight $ test_tokenizer "True") $
  44                 EType $ ty @Bool)
  45          , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (ty @Bool,
  46                 Right $ Error_Term_unbound $ Term_Name "Bool")
  47          , "(\\(x:Bool) -> x) True True" ==> Left (ty @Bool,
  48                 Right $ Error_Term_Constraint_Type $
  49                 Right $ Constraint_Type_App $
  50                 At (maybeRight $ test_tokenizer "(\\(x:Bool) -> x) True") $
  51                 EType $ ty @Bool)
  52          , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (ty @Bool,
  53                 Right $ Error_Term_Constraint_Type $ Right $
  54                 Constraint_Type_Eq
  55                  (Right $ At (maybeRight $ test_tokenizer "(\\(x:Bool -> Bool) -> x True)") $
  56                         EType $ (ty @Bool ~> ty @Bool))
  57                  (At (maybeRight $ test_tokenizer "True") $
  58                         EType $ ty @Bool)
  59                  )
  60          ]
  61  ]
  62
  63 -- * Class 'Sym_Bool_Vars'
  64 -- | A few boolean variables.
  65 class Sym_Bool_Vars repr where
  66         x :: repr Bool
  67         y :: repr Bool
  68         z :: repr Bool
  69 instance Sym_Bool_Vars TextI where
  70         x = TextI $ \_p _v -> "x"
  71         y = TextI $ \_p _v -> "y"
  72         z = TextI $ \_p _v -> "z"
  73 {-
  74 instance -- Trans_Boo_Const
  75  ( Sym_Bool repr
  76  , Sym_Bool_Vars repr
  77  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  78         x = trans_lift x
  79         y = trans_lift y
  80         z = trans_lift z
  81 -}
  82
  83 -- * EDSL tests
  84 te1 = bool True && bool False
  85 te2 = (bool True && bool False) ||  (bool True && bool True)
  86 te3 = (bool True ||  bool False) && (bool True ||  bool True)
  87 te4 = bool True && not (bool False)
  88 te5 = bool True && not x
  89 te6 = x `xor` y
  90 te7 = (x `xor` y) `xor` z
  91 te8 = x `xor` (y `xor` bool True)