Language/Symantic/Compiling/Bool/Test.hs

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