1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE OverloadedStrings #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE Rank2Types #-}
7 module Repr.Host.Test where
9 -- import Data.Function (($))
10 -- import Data.Functor.Identity (Identity)
12 import Test.Tasty.HUnit
13 import Prelude hiding (and, not, or)
15 import Language.LOL.Symantic.Repr
16 import Language.LOL.Symantic.Expr
17 import qualified Expr.Lambda.Test as Lambda.Test
18 import qualified Expr.Bool.Test as Bool.Test
21 tests = testGroup "Host" $
22 let (==>) (expr::forall repr. Sym_of_Expr (Expr_Lambda_Bool IO) repr => repr h) expected =
23 testCase ((string_from_expr :: Repr_String IO _h -> String) $ expr) $
24 (>>= (@?= expected)) $
25 host_from_expr expr in
27 [ Bool.Test.e1 ==> False
28 , Bool.Test.e2 ==> True
29 , Bool.Test.e3 ==> True
30 , Bool.Test.e4 ==> True
34 [ (Lambda.Test.e1 `app` bool True `app` bool True) ==> False
35 , (Lambda.Test.e1 `app` bool True `app` bool False) ==> True
36 , (Lambda.Test.e1 `app` bool False `app` bool True) ==> True
37 , (Lambda.Test.e1 `app` bool False `app` bool False) ==> False
39 , (Lambda.Test.e2 `app` bool True `app` bool True) ==> False
40 , (Lambda.Test.e2 `app` bool True `app` bool False) ==> True
41 , (Lambda.Test.e2 `app` bool False `app` bool True) ==> True
42 , (Lambda.Test.e2 `app` bool False `app` bool False) ==> False
44 , Lambda.Test.e3 ==> True
45 , Lambda.Test.e4 ==> True
47 , (Lambda.Test.e5 `app` bool True `app` bool True) ==> True
48 , (Lambda.Test.e5 `app` bool True `app` bool False) ==> False
49 , (Lambda.Test.e5 `app` bool False `app` bool True) ==> False
50 , (Lambda.Test.e5 `app` bool False `app` bool False) ==> False
52 , Lambda.Test.e6 ==> False
53 , (Lambda.Test.e7 `app` val id) ==> True
54 , (Lambda.Test.e7 `app` val not) ==> False
58 [ If.e1 ==> "if True then False else True"
59 , If.e2 ==> "if True & True then False else True"