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 Control.Arrow (left)
  13 -- import Data.Functor.Identity (Identity)
  14 -- import Control.Monad.IO.Class (MonadIO(..))
  15 import Data.Proxy (Proxy(..))
  16 import Data.Type.Equality ((:~:)(Refl))
  17 import Prelude hiding (and, not, or)
  18
  19 import Language.LOL.Symantic.Repr
  20 import Language.LOL.Symantic.AST
  21 import Language.LOL.Symantic.Expr
  22 import Language.LOL.Symantic.Type
  23 import Language.LOL.Symantic.Trans
  24
  25 -- * Class 'Sym_Bool_Vars'
  26
  27 -- | A few boolean variables.
  28 class Sym_Bool_Vars repr where
  29         x :: repr Bool
  30         y :: repr Bool
  31         z :: repr Bool
  32 instance Sym_Bool_Vars (Repr_String fun) where
  33         x = Repr_String $ \_p _v -> "x"
  34         y = Repr_String $ \_p _v -> "y"
  35         z = Repr_String $ \_p _v -> "z"
  36 instance -- Trans_Boo_Const
  37  ( Sym_Bool repr
  38  , Sym_Bool_Vars repr
  39  ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
  40         x = trans_lift x
  41         y = trans_lift y
  42         z = trans_lift z
  43
  44 -- * Expressions
  45 e1 = bool True `and` bool False
  46 e2 = (bool True `and` bool False) `or`  (bool True `and` bool True)
  47 e3 = (bool True `or`  bool False) `and` (bool True `or`  bool True)
  48 e4 = bool True `and` not (bool False)
  49 e5 = bool True `and` not x
  50 e6 = x `xor` y
  51 e7 = (x `xor` y) `xor` z
  52 e8 = x `xor` (y `xor` bool True)
  53
  54 -- * Tests
  55 {-
  56 (==>)
  57  :: forall h ast root.
  58  ( Eq h, Eq ast, Show h, Show ast
  59  , root ~ Expr_Lambda_Bool IO
  60  , Expr_from ast (Expr_Lambda IO root)
  61  , Expr_from ast (Expr_Bool      root)
  62  ) => ast
  63  -- -> (Type_Fun_Bool IO h, h, String)
  64  -> Either (Proxy h, Error_of_Expr ast root)
  65            (Type_Fun_Bool IO h, h, String)
  66  -> TestTree
  67 -}
  68 (==>) ast expected =
  69         testCase (show ast) $
  70         case expr_lambda_bool_from (Proxy::Proxy IO) ast of
  71          Left err -> Left err @?= snd `left` expected
  72          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  73                 case expected of
  74                  Left (_, err) -> Right ("…"::String) @?= Left err
  75                  Right (ty_expected::Type_Fun_Bool IO h, _::h, _::String) ->
  76                         (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
  77                         case ty `type_eq` ty_expected of
  78                          Nothing -> return $ Left $
  79                                 error_expr (Proxy::Proxy (Expr_Lambda_Bool IO)) $
  80                                 Error_Expr_Type_mismatch ast
  81                                  (Exists_Type ty)
  82                                  (Exists_Type ty_expected)
  83                          Just Refl -> do
  84                                 h <- host_from_expr r
  85                                 return $
  86                                         Right
  87                                          ( ty
  88                                          , h
  89                                          , string_from_expr r
  90                                          -- , (string_from_expr :: Repr_String IO h -> String) r
  91                                          )
  92
  93 tests :: TestTree
  94 tests = testGroup "Bool" $
  95  [ AST "bool" [AST "True" []] ==> Right
  96          ( type_bool
  97          , True
  98          , "True" )
  99  , AST "int" [AST "1" []] ==> Left (Proxy::Proxy Int,
 100         Error_Expr_Alt_Curr $
 101         Error_Expr_Unsupported $ AST "int" [AST "1" []])
 102  , AST "xor"
 103          [ AST "bool" [AST "True" []]
 104          , AST "bool" [AST "True" []]
 105          ] ==> Right
 106          ( type_bool
 107          , False
 108          , "(True | True) & !(True & True)" )
 109  , AST "app"
 110          [ AST "val"
 111                  [ AST "x" []
 112                  , AST "Bool" []
 113                  , AST "var" [AST "x" []]
 114                  ]
 115          , AST "bool" [AST "True" []]
 116          ] ==> Right
 117          ( type_bool
 118          , True
 119          , "(\\x0 -> x0) True" )
 120  , let ast = AST "app"
 121          [ AST "bool" [AST "True" []]
 122          , AST "bool" [AST "True" []]
 123          ] in ast ==> Left (Proxy::Proxy Bool,
 124         Error_Expr_Alt_Curr $
 125         Error_Expr_Type_mismatch ast
 126          (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
 127          ::Type_Fun_Bool IO (IO Zero -> IO (Succ Zero))))
 128          (Exists_Type type_bool))
 129  , AST "app"
 130          [ AST "val"
 131                  [ AST "x" []
 132                  , AST "Bool" []
 133                  , AST "xor"
 134                          [ AST "var" [AST "x" []]
 135                          , AST "bool" [AST "True" []]
 136                          ]
 137                  ]
 138          , AST "bool" [AST "True" []]
 139          ] ==> Right
 140          ( type_bool
 141          , False
 142          , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
 143  , AST "let_val"
 144          [ AST "x" []
 145          , AST "bool" [AST "True" []]
 146          , AST "xor"
 147                  [ AST "var" [AST "x" []]
 148                  , AST "bool" [AST "True" []]
 149                  ]
 150          ] ==> Right
 151          ( type_bool
 152          , False
 153          , "let x0 = True in (x0 | True) & !(x0 & True)" )
 154  ]