Language/LOL/Symantic/Expr/If/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.If.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.Type.Equality ((:~:)(Refl))
  15 import Prelude hiding (maybe, not)
  16
  17 import Language.LOL.Symantic.Repr
  18 import Language.LOL.Symantic.AST
  19 import Language.LOL.Symantic.Expr
  20 import Language.LOL.Symantic.Type
  21
  22 -- * Expressions
  23 e1 = if_ (bool True)
  24          (bool False)
  25          (bool True)
  26
  27 -- * Tests
  28 (==>)
  29  :: forall h ast root.
  30  ( Eq h, Eq ast, Show h, Show ast
  31  , root ~ Expr_Lambda_If_Bool IO
  32  , Expr_from ast (Expr_Lambda IO root)
  33  , Expr_from ast (Expr_Bool      root)
  34  , Expr_from ast (Expr_If        root)
  35  ) => ast
  36  -> Either (Proxy h, Error_of_Expr ast root)
  37            (Type_Root_of_Expr (Expr_Lambda_If_Bool IO) h, h, String)
  38  -> TestTree
  39 (==>) ast expected =
  40         testCase (show ast) $
  41         case expr_lambda_if_bool_from (Proxy::Proxy IO) ast of
  42          Left err -> Left err @?= snd `left` expected
  43          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  44                 case expected of
  45                  Left (_, err) -> Right ("…"::String) @?= Left err
  46                  Right (ty_expected::Type_Root_of_Expr (Expr_Lambda_If_Bool IO) h, _::h, _::String) ->
  47                         (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
  48                         case ty `type_eq` ty_expected of
  49                          Nothing -> return $ Left $
  50                                 error_expr (Proxy::Proxy (Expr_Lambda_If_Bool IO)) $
  51                                 Error_Expr_Type_mismatch ast
  52                                  (Exists_Type ty)
  53                                  (Exists_Type ty_expected)
  54                          Just Refl -> do
  55                                 h <- host_from_expr r
  56                                 return $
  57                                         Right
  58                                          ( ty
  59                                          , h
  60                                          , string_from_expr r
  61                                          -- , (string_from_expr :: Repr_String IO h -> String) r
  62                                          )
  63
  64 tests :: TestTree
  65 tests = testGroup "If"
  66  [ AST "if"
  67          [ AST "bool" [AST "True" []]
  68          , AST "bool" [AST "False" []]
  69          , AST "bool" [AST "True" []]
  70          ] ==> Right
  71          ( type_bool
  72          , False
  73          , "if True then False else True" )
  74  ]