Language/Symantic/Expr/Eq/Test.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE NoMonomorphismRestriction #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE TypeOperators #-}
   6 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
   7
   8 module Expr.Eq.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 ((&&), not, (||), (==))
  20
  21 import Language.Symantic.Type
  22 import Language.Symantic.Expr
  23 import Language.Symantic.Repr
  24
  25 import AST.Test
  26
  27 -- * Expressions
  28 t = bool True
  29 f = bool False
  30 e1 = if_ ((t && t) == (t || f)) t f
  31 e2 = if_ (((t && t) || f) == (t && (t || f))) t f
  32 e3 = if_ (not (t == f) == (t == t)) t f
  33
  34 -- * Tests
  35 type Ex lam = Expr_Root
  36  (   Expr_Lambda_App lam
  37  .|. Expr_Lambda_Val lam
  38  .|. Expr_Bool
  39  .|. Expr_Eq
  40  )
  41 ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
  42
  43 (==>) ast expected =
  44         testCase (show ast) $
  45         case ex_from ast of
  46          Left err -> Left err @?= snd `Arrow.left` expected
  47          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  48                 case expected of
  49                  Left (_, err) -> Right ("…"::String) @?= Left err
  50                  Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
  51                         (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
  52                         case ty `eq_type` ty_expected of
  53                          Nothing -> Monad.return $ Left $
  54                                 error_expr (Proxy::Proxy (Ex Identity)) $
  55                                 Error_Expr_Type_mismatch ast
  56                                  (Exists_Type ty)
  57                                  (Exists_Type ty_expected)
  58                          Just Refl -> do
  59                                 let h = runIdentity $ host_from_expr r
  60                                 Monad.return $
  61                                         Right
  62                                          ( ty
  63                                          , h
  64                                          , text_from_expr r
  65                                          -- , (text_from_expr :: Repr_Text Identity h -> Text) r
  66                                          )
  67
  68 tests :: TestTree
  69 tests = testGroup "Eq"
  70  [ AST "==" [ AST "bool" [AST "True" []]
  71                   , AST "bool" [AST "True" []]
  72                   ] ==> Right
  73          ( type_bool
  74          , True
  75          , "True == True" )
  76  , AST "app"
  77          [ AST "val"
  78                  [ AST "x" []
  79                  , AST "Bool" []
  80                  , AST "==" [ AST "var" [AST "x" []]
  81                             , AST "not" [AST "var" [AST "x" []]] ]
  82                  ]
  83          , AST "bool" [AST "True" []]
  84          ] ==> Right
  85          ( type_bool
  86          , False
  87          , "(\\x0 -> x0 == !x0) True" )
  88  ]