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 ast root.
  55       ( Eq h, Eq ast, Show h, Show ast
  56       , root ~ Expr_Lambda_Bool IO
  57       , Expr_from ast (Expr_Lambda IO root)
  58       , Expr_from ast (Expr_Bool      root)
  59       )
  60       => ast -> (Type_Fun_Bool IO h, h, String) -> TestTree
  61 (==>) ast expected@(ty_expected::Type_Fun_Bool IO h, _::h, _::String) =
  62         testCase (show ast) $
  63         (>>= (@?= Right expected)) $
  64         case expr_lambda_bool_from (Proxy::Proxy IO) ast of
  65          Left err -> return $ Left err
  66          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  67                 case ty `type_eq` ty_expected of
  68                  Nothing -> return $ Left $
  69                         error_expr (Proxy::Proxy root) $ Error_Expr_Type
  70                          (error_type_lift $ Error_Type_Unsupported_here ast) ast
  71                  Just Refl -> do
  72                         h <- host_from_expr r
  73                         return $
  74                                 Right
  75                                  ( ty
  76                                  , h
  77                                  , string_from_expr r
  78                                  -- , (string_from_expr :: Repr_String IO h -> String) r
  79                                  )
  80
  81 tests :: TestTree
  82 tests = testGroup "Bool" $
  83  [ AST "bool" [AST "True" []] ==>
  84          ( type_bool
  85          , True
  86          , "True" )
  87  , AST "xor"
  88          [ AST "bool" [AST "True" []]
  89          , AST "bool" [AST "True" []]
  90          ] ==>
  91          ( type_bool
  92          , False
  93          , "(True | True) & !(True & True)" )
  94  , AST "app"
  95          [ AST "val"
  96                  [ AST "x" []
  97                  , AST "Bool" []
  98                  , AST "var" [AST "x" []]
  99                  ]
 100          , AST "bool" [AST "True" []]
 101          ] ==>
 102          ( type_bool
 103          , True
 104          , "(\\x0 -> x0) True" )
 105  , AST "app"
 106          [ AST "val"
 107                  [ AST "x" []
 108                  , AST "Bool" []
 109                  , AST "xor"
 110                          [ AST "var" [AST "x" []]
 111                          , AST "bool" [AST "True" []]
 112                          ]
 113                  ]
 114          , AST "bool" [AST "True" []]
 115          ] ==>
 116          ( type_bool
 117          , False
 118          , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
 119  , AST "let_val"
 120          [ AST "x" []
 121          , AST "bool" [AST "True" []]
 122          , AST "xor"
 123                  [ AST "var" [AST "x" []]
 124                  , AST "bool" [AST "True" []]
 125                  ]
 126          ] ==>
 127          ( type_bool
 128          , False
 129          , "let x0 = True in (x0 | True) & !(x0 & True)" )
 130  ]