Language/Symantic/Expr/If/Test.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE NoMonomorphismRestriction #-}
   4 {-# LANGUAGE Rank2Types #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeOperators #-}
   7 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   8 module Expr.If.Test where
   9
  10 import Test.Tasty
  11 import Test.Tasty.HUnit
  12
  13 import qualified Control.Arrow as Arrow
  14 import qualified Control.Monad as Monad
  15 import Data.Functor.Identity
  16 import Data.Proxy (Proxy(..))
  17 import Data.Text (Text)
  18 import Data.Type.Equality ((:~:)(Refl))
  19 import Prelude hiding (maybe, not, (&&), Monad(..))
  20
  21 import Language.Symantic.Repr
  22 import Language.Symantic.Expr
  23 import Language.Symantic.Type
  24
  25 import AST.Test
  26
  27 -- * Expressions
  28 e1 = if_ (bool True) (bool False) (bool True)
  29 e2 = if_ (bool True && bool True) (bool False) (bool True)
  30
  31 -- * Tests
  32 type Ex lam = Expr_Root
  33  (   Expr_Lambda_App lam
  34  .|. Expr_Lambda_Val lam
  35  .|. Expr_If
  36  .|. Expr_Bool
  37  )
  38 ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
  39
  40 (==>) ast expected =
  41         testCase (show ast) $
  42         case ex_from ast of
  43          Left err -> Left err @?= snd `Arrow.left` expected
  44          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  45                 case expected of
  46                  Left (_, err) -> Right ("…"::String) @?= Left err
  47                  Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
  48                         (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
  49                         case ty `eq_type` ty_expected of
  50                          Nothing -> Monad.return $ Left $
  51                                 error_expr (Proxy::Proxy (Ex Identity)) $
  52                                 Error_Expr_Type_mismatch ast
  53                                  (Exists_Type ty)
  54                                  (Exists_Type ty_expected)
  55                          Just Refl -> do
  56                                 let h = runIdentity $ host_from_expr r
  57                                 Monad.return $
  58                                         Right
  59                                          ( ty
  60                                          , h
  61                                          , text_from_expr r
  62                                          -- , (text_from_expr :: Repr_Text Identity h -> Text) r
  63                                          )
  64
  65 tests :: TestTree
  66 tests = testGroup "If"
  67  [ AST "if"
  68          [ AST "bool" [AST "True" []]
  69          , AST "bool" [AST "False" []]
  70          , AST "bool" [AST "True" []]
  71          ] ==> Right
  72          ( type_bool
  73          , False
  74          , "if True then False else True" )
  75  ]