Language/LOL/Symantic/Expr/Maybe/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.Maybe.Test where
   8
   9 import Test.Tasty
  10 import Test.Tasty.HUnit
  11
  12 import Data.Proxy (Proxy(..))
  13 import Data.Type.Equality ((:~:)(Refl))
  14 import Prelude hiding (maybe, not)
  15
  16 import Language.LOL.Symantic.Repr
  17 import Language.LOL.Symantic.AST
  18 import Language.LOL.Symantic.Expr
  19 import Language.LOL.Symantic.Type
  20
  21 -- * Expressions
  22 e1 = maybe (bool True) (\x -> x >>= \x' -> return $ not x') (just $ bool True)
  23
  24 -- * Tests
  25 (==>) :: forall h ast root.
  26       ( Eq h, Eq ast, Show h, Show ast
  27       , root ~ Expr_Lambda_Bool_Maybe IO
  28       , Expr_from ast (Expr_Lambda IO root)
  29       , Expr_from ast (Expr_Maybe IO root)
  30       , Expr_from ast (Expr_Bool root)
  31       )
  32       => ast -> (Type_Fun_Bool_Maybe IO h, h, String) -> TestTree
  33 (==>) ast expected@(ty_expected::Type_Fun_Bool_Maybe IO h, _::h, _::String) =
  34         testCase (show ast) $
  35         (>>= (@?= Right expected)) $
  36         case expr_lambda_bool_maybe_from (Proxy::Proxy IO) ast of
  37          Left err -> return $ Left err
  38          Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
  39                 case ty `type_eq` ty_expected of
  40                  Nothing -> return $ Left $
  41                         error_expr (Proxy::Proxy root) $ Error_Expr_Type
  42                          (error_type_lift $ Error_Type_Unsupported_here ast) ast
  43                  Just Refl -> do
  44                         h <- host_from_expr r
  45                         return $
  46                                 Right
  47                                  ( ty
  48                                  , h
  49                                  -- , string_from_expr r
  50                                  , (string_from_expr :: Repr_String IO h -> String) r
  51                                  )
  52 {-
  53 (Implicit_HBool (Is_Last_Expr
  54  (Expr_Lambda IO (Expr_Root (Expr_Alt Expr_Bool (Expr_Maybe IO))))
  55  (Expr_Maybe IO  (Expr_Root (Expr_Alt Expr_Bool (Expr_Maybe IO))))))
  56 -}
  57 tests :: TestTree
  58 tests = testGroup "Maybe"
  59  [ AST "just" [AST "bool" [AST "True" []]] ==>
  60          ( type_maybe type_bool
  61          , Just True
  62          , "just True" )
  63  , AST "just"
  64          [ AST "let_val"
  65                  [ AST "x" []
  66                  , AST "bool" [AST "True" []]
  67                  , AST "var" [AST "x" []]
  68                  ]
  69          ] ==>
  70          ( type_maybe type_bool
  71          , Just True
  72          , "just (let x0 = True in x0)" )
  73  {-, AST "xor"
  74          [ AST "bool" [AST "True" []]
  75          , AST "bool" [AST "True" []]
  76          ] ==>
  77          ( type_bool
  78          , False
  79          , "(True | True) & !(True & True)" )
  80  , AST "app"
  81          [ AST "val"
  82                  [ AST "x" []
  83                  , AST "Bool" []
  84                  , AST "var" [AST "x" []]
  85                  ]
  86          , AST "bool" [AST "True" []]
  87          ] ==>
  88          ( type_bool
  89          , True
  90          , "(\\x0 -> x0) True" )
  91  , AST "app"
  92          [ AST "val"
  93                  [ AST "x" []
  94                  , AST "Bool" []
  95                  , AST "xor"
  96                          [ AST "var" [AST "x" []]
  97                          , AST "bool" [AST "True" []]
  98                          ]
  99                  ]
 100          , AST "bool" [AST "True" []]
 101          ] ==>
 102          ( type_bool
 103          , False
 104          , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
 105  , AST "let_val"
 106          [ AST "x" []
 107          , AST "bool" [AST "True" []]
 108          , AST "xor"
 109                  [ AST "var" [AST "x" []]
 110                  , AST "bool" [AST "True" []]
 111                  ]
 112          ] ==>
 113          ( type_bool
 114          , False
 115          , "let x0 = True in (x0 | True) & !(x0 & True)" )
 116  -}]