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

   1 {-# LANGUAGE NoMonomorphismRestriction #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE ScopedTypeVariables #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   6
   7 module Expr.Eq.Test where
   8
   9 import Test.Tasty
  10 import Test.Tasty.HUnit
  11
  12 import Control.Arrow (left)
  13 import Data.Proxy (Proxy(..))
  14 import Data.Text (Text)
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Prelude hiding (and, not, or)
  17
  18 import Language.LOL.Symantic.Type
  19 import Language.LOL.Symantic.Expr
  20 import Language.LOL.Symantic.Repr
  21
  22 import AST.Test
  23
  24 -- * Expressions
  25 t = bool True
  26 f = bool False
  27 e1 = if_ ((t `and` t) `eq` (t `or` f)) t f
  28 e2 = if_ (((t `and` t) `or` f) `eq` (t `and` (t `or` f))) t f
  29 e3 = if_ (not (t `eq` f) `eq` (t `eq` t)) t f
  30
  31 -- * Tests
  32 (==>) ast expected =
  33         testCase (show ast) $
  34         case expr_lambda_bool_eq_from (Proxy::Proxy IO) ast of
  35          Left err -> Left err @?= snd `left` expected
  36          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  37                 case expected of
  38                  Left (_, err) -> Right ("…"::String) @?= Left err
  39                  Right (ty_expected::Type_Root_of_Expr (Expr_Lambda_Bool_Eq IO) h, _::h, _::Text) ->
  40                         (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
  41                         case ty `type_eq` ty_expected of
  42                          Nothing -> return $ Left $
  43                                 error_expr (Proxy::Proxy (Expr_Lambda_Bool_Eq IO)) $
  44                                 Error_Expr_Type_mismatch ast
  45                                  (Exists_Type ty)
  46                                  (Exists_Type ty_expected)
  47                          Just Refl -> do
  48                                 h <- host_from_expr r
  49                                 return $
  50                                         Right
  51                                          ( ty
  52                                          , h
  53                                          , text_from_expr r
  54                                          -- , (text_from_expr :: Repr_String IO h -> Text) r
  55                                          )
  56
  57 tests :: TestTree
  58 tests = testGroup "Eq"
  59  [ AST "eq" [ AST "bool" [AST "True" []]
  60                   , AST "bool" [AST "True" []]
  61                   ] ==> Right
  62          ( type_bool
  63          , True
  64          , "True == True" )
  65  , AST "app"
  66          [ AST "val"
  67                  [ AST "x" []
  68                  , AST "Bool" []
  69                  , AST "eq" [ AST "var" [AST "x" []]
  70                             , AST "not" [AST "var" [AST "x" []]] ]
  71                  ]
  72          , AST "bool" [AST "True" []]
  73          ] ==> Right
  74          ( type_bool
  75          , False
  76          , "(\\x0 -> x0 == !x0) True" )
  77  ]