{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Expr.Maybe.Test where import Test.Tasty import Test.Tasty.HUnit import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (maybe, not) import Language.LOL.Symantic.Repr import Language.LOL.Symantic.AST import Language.LOL.Symantic.Expr import Language.LOL.Symantic.Type -- * Expressions e1 = maybe (bool True) (\x -> x >>= \x' -> return $ not x') (just $ bool True) -- * Tests (==>) :: forall h ast root. ( Eq h, Eq ast, Show h, Show ast , root ~ Expr_Lambda_Bool_Maybe IO , Expr_from ast (Expr_Lambda IO root) , Expr_from ast (Expr_Maybe IO root) , Expr_from ast (Expr_Bool root) ) => ast -> (Type_Fun_Bool_Maybe IO h, h, String) -> TestTree (==>) ast expected@(ty_expected::Type_Fun_Bool_Maybe IO h, _::h, _::String) = testCase (show ast) $ (>>= (@?= Right expected)) $ case expr_lambda_bool_maybe_from (Proxy::Proxy IO) ast of Left err -> return $ Left err Right (Exists_Type_and_Repr ty (Forall_Repr r)) -> case ty `type_eq` ty_expected of Nothing -> return $ Left $ error_expr (Proxy::Proxy root) $ Error_Expr_Type (error_type_lift $ Error_Type_Unsupported_here ast) ast Just Refl -> do h <- host_from_expr r return $ Right ( ty , h -- , string_from_expr r , (string_from_expr :: Repr_String IO h -> String) r ) {- (Implicit_HBool (Is_Last_Expr (Expr_Lambda IO (Expr_Root (Expr_Alt Expr_Bool (Expr_Maybe IO)))) (Expr_Maybe IO (Expr_Root (Expr_Alt Expr_Bool (Expr_Maybe IO)))))) -} tests :: TestTree tests = testGroup "Maybe" [ AST "just" [AST "bool" [AST "True" []]] ==> ( type_maybe type_bool , Just True , "just True" ) , AST "just" [ AST "let_val" [ AST "x" [] , AST "bool" [AST "True" []] , AST "var" [AST "x" []] ] ] ==> ( type_maybe type_bool , Just True , "just (let x0 = True in x0)" ) {-, AST "xor" [ AST "bool" [AST "True" []] , AST "bool" [AST "True" []] ] ==> ( type_bool , False , "(True | True) & !(True & True)" ) , AST "app" [ AST "val" [ AST "x" [] , AST "Bool" [] , AST "var" [AST "x" []] ] , AST "bool" [AST "True" []] ] ==> ( type_bool , True , "(\\x0 -> x0) True" ) , AST "app" [ AST "val" [ AST "x" [] , AST "Bool" [] , AST "xor" [ AST "var" [AST "x" []] , AST "bool" [AST "True" []] ] ] , AST "bool" [AST "True" []] ] ==> ( type_bool , False , "(\\x0 -> (x0 | True) & !(x0 & True)) True" ) , AST "let_val" [ AST "x" [] , AST "bool" [AST "True" []] , AST "xor" [ AST "var" [AST "x" []] , AST "bool" [AST "True" []] ] ] ==> ( type_bool , False , "let x0 = True in (x0 | True) & !(x0 & True)" ) -}]