Language/LOL/Symantic/Expr/Bool/Test.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE NoMonomorphismRestriction #-}
   4 {-# LANGUAGE Rank2Types #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   7 module Expr.Bool.Test where
   8
   9 import Test.Tasty
  10 import Test.Tasty.HUnit
  11
  12 -- import Data.Functor.Identity (Identity)
  13 -- import Control.Monad.IO.Class (MonadIO(..))
  14 import Data.Proxy (Proxy(..))
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Prelude hiding (and, not, or)
  17
  18 import Language.LOL.Symantic.Repr
  19 import Language.LOL.Symantic.AST
  20 import Language.LOL.Symantic.Expr
  21 import Language.LOL.Symantic.Type
  22 import Language.LOL.Symantic.Trans
  23
  24 -- * Class 'Sym_Bool_Vars'
  25
  26 -- | A few boolean variables.
  27 class Sym_Bool_Vars repr where
  28         x :: repr Bool
  29         y :: repr Bool
  30         z :: repr Bool
  31 instance Sym_Bool_Vars (Repr_String fun) where
  32         x = Repr_String $ \_p _v -> "x"
  33         y = Repr_String $ \_p _v -> "y"
  34         z = Repr_String $ \_p _v -> "z"
  35 instance -- Trans_Boo_Const
  36  ( Sym_Bool repr
  37  , Sym_Bool_Vars repr
  38  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  39         x = trans_lift x
  40         y = trans_lift y
  41         z = trans_lift z
  42
  43 -- * Expressions
  44 e1 = bool True `and` bool False
  45 e2 = (bool True `and` bool False) `or`  (bool True `and` bool True)
  46 e3 = (bool True `or`  bool False) `and` (bool True `or`  bool True)
  47 e4 = bool True `and` not (bool False)
  48 e5 = bool True `and` not x
  49 e6 = x `xor` y
  50 e7 = (x `xor` y) `xor` z
  51 e8 = x `xor` (y `xor` bool True)
  52
  53 -- * Tests
  54 (==>) :: forall h raw root.
  55       ( Eq h, Eq raw, Show h, Show raw
  56       , root ~ Expr_Lambda_Bool IO
  57       , Expr_from raw (Expr_Lambda IO root)
  58       , Expr_from raw (Expr_Bool      root)
  59       -- , Error_Type_Lift (Error_Type raw) (Error_of_Type raw (Type_Root_of_Expr (Expr_Lambda_Bool IO))))
  60       -- , Error_Type_Lift (Error_Type raw) err_ty0
  61       )
  62       => raw -> (Type_Fun_Bool IO h, h, String) -> TestTree
  63 (==>) raw expected@(ty_expected::Type_Fun_Bool IO h, _::h, _::String) =
  64         testCase (show raw) $
  65         (>>= (@?= Right expected)) $
  66         case expr_lambda_bool_from (Proxy::Proxy IO) raw of
  67          Left err -> return $ Left err
  68          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  69                 case ty `type_eq` ty_expected of
  70                  Nothing -> return $ Left $
  71                         error_lambda_lift $ Error_Expr_Type
  72                          (error_type_lift $ Error_Type_Unsupported raw) raw
  73                  Just Refl -> do
  74                         h <- host_from_expr r
  75                         return $
  76                                 Right
  77                                  ( ty
  78                                  , h
  79                                  , string_from_expr r
  80                                  -- , (string_from_expr :: Repr_String IO h -> String) r
  81                                  )
  82         where
  83                 error_lambda_lift
  84                  :: (root ~ Expr_Lambda_Bool IO)
  85                  => Error_Expr_Lambda (Error_of_Type raw (Type_Root_of_Expr root))
  86                                       (Type_Root_of_Expr root)
  87                                       raw
  88                  -> Error_of_Expr raw root
  89                 error_lambda_lift = error_expr_lift
  90
  91 tests :: TestTree
  92 tests = testGroup "Bool" $
  93  [ AST "bool" [AST "True" []] ==>
  94          ( type_bool
  95          , True
  96          , "True" )
  97  , AST "xor"
  98          [ AST "bool" [AST "True" []]
  99          , AST "bool" [AST "True" []]
 100          ] ==>
 101          ( type_bool
 102          , False
 103          , "(True | True) & !(True & True)" )
 104  , AST "app"
 105          [ AST "val"
 106                  [ AST "x" []
 107                  , AST "Bool" []
 108                  , AST "var" [AST "x" []]
 109                  ]
 110          , AST "bool" [AST "True" []]
 111          ] ==>
 112          ( type_bool
 113          , True
 114          , "(\\x0 -> x0) True" )
 115  , AST "app"
 116          [ AST "val"
 117                  [ AST "x" []
 118                  , AST "Bool" []
 119                  , AST "xor"
 120                          [ AST "var" [AST "x" []]
 121                          , AST "bool" [AST "True" []]
 122                          ]
 123                  ]
 124          , AST "bool" [AST "True" []]
 125          ] ==>
 126          ( type_bool
 127          , False
 128          , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
 129  ]