Language/Symantic/Expr/Maybe/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.Maybe.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)
  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 = maybe (bool True) (val not) (just $ bool True)
  29
  30 -- * Tests
  31 type Ex lam = Expr_Root
  32  (   Expr_Lambda_App lam
  33  .|. Expr_Lambda_Val lam
  34  .|. Expr_Maybe lam
  35  .|. Expr_Bool
  36  )
  37 ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
  38
  39 (==>) ast expected =
  40         testCase (show ast) $
  41         case ex_from ast of
  42          Left err -> Left err @?= snd `Arrow.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 (Ex Identity) h, _::h, _::Text) ->
  47                         (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
  48                         case ty `eq_type` ty_expected of
  49                          Nothing -> Monad.return $ Left $
  50                                 error_expr (Proxy::Proxy (Ex Identity)) $
  51                                 Error_Expr_Type_mismatch ast
  52                                  (Exists_Type ty)
  53                                  (Exists_Type ty_expected)
  54                          Just Refl -> do
  55                                 let h = runIdentity $ host_from_expr r
  56                                 Monad.return $
  57                                         Right
  58                                          ( ty
  59                                          , h
  60                                          , text_from_expr r
  61                                          -- , (text_from_expr :: Repr_Text Identity h -> Text) r
  62                                          )
  63
  64 tests :: TestTree
  65 tests = testGroup "Maybe"
  66  [ AST "just" [AST "bool" [AST "True" []]] ==> Right
  67          ( type_maybe type_bool
  68          , Just True
  69          , "just True" )
  70  , AST "just"
  71          [ AST "let_val"
  72                  [ AST "x" []
  73                  , AST "bool" [AST "True" []]
  74                  , AST "var" [AST "x" []]
  75                  ]
  76          ] ==> Right
  77          ( type_maybe type_bool
  78          , Just True
  79          , "just (let x0 = True in x0)" )
  80  , AST "maybe"
  81          [ AST "bool" [AST "True" []]
  82          , AST "val"
  83                  [ AST "x" []
  84                  , AST "Bool" []
  85                  , AST "not" [AST "var" [AST "x" []]]
  86                  ]
  87          , AST "nothing"
  88                  [ AST "Bool" []
  89                  ]
  90          ] ==> Right
  91          ( type_bool
  92          , True
  93          , "maybe True (\\x0 -> !x0) nothing" )
  94  , AST "maybe"
  95          [ AST "bool" [AST "False" []]
  96          , AST "val"
  97                  [ AST "x" []
  98                  , AST "Bool" []
  99                  , AST "not" [AST "var" [AST "x" []]]
 100                  ]
 101          , AST "just"
 102                  [ AST "bool" [AST "True" []]
 103                  ]
 104          ] ==> Right
 105          ( type_bool
 106          , False
 107          , "maybe False (\\x0 -> !x0) (just True)" )
 108  ]