]> Git — Sourcephile - haskell/symantic.git/blob - Language/LOL/Symantic/Expr/Bool/Test.hs
init
[haskell/symantic.git] / Language / LOL / Symantic / Expr / Bool / 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.Bool.Test where
8
9 import Test.Tasty
10 import Test.Tasty.HUnit
11
12 -- import Data.Functor.Identity (Identity)
13 -- import Control.Monad.IO.Class (MonadIO(..))
14 import Data.Proxy (Proxy(..))
15 import Data.Type.Equality ((:~:)(Refl))
16 import Prelude hiding (and, not, or)
17
18 import Language.LOL.Symantic.Repr
19 import Language.LOL.Symantic.AST
20 import Language.LOL.Symantic.Expr
21 import Language.LOL.Symantic.Type
22 import Language.LOL.Symantic.Trans
23
24 -- * Class 'Sym_Bool_Vars'
25
26 -- | A few boolean variables.
27 class Sym_Bool_Vars repr where
28 x :: repr Bool
29 y :: repr Bool
30 z :: repr Bool
31 instance Sym_Bool_Vars (Repr_String fun) where
32 x = Repr_String $ \_p _v -> "x"
33 y = Repr_String $ \_p _v -> "y"
34 z = Repr_String $ \_p _v -> "z"
35 instance -- Trans_Boo_Const
36 ( Sym_Bool repr
37 , Sym_Bool_Vars repr
38 ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
39 x = trans_lift x
40 y = trans_lift y
41 z = trans_lift z
42
43 -- * Expressions
44 e1 = bool True `and` bool False
45 e2 = (bool True `and` bool False) `or` (bool True `and` bool True)
46 e3 = (bool True `or` bool False) `and` (bool True `or` bool True)
47 e4 = bool True `and` not (bool False)
48 e5 = bool True `and` not x
49 e6 = x `xor` y
50 e7 = (x `xor` y) `xor` z
51 e8 = x `xor` (y `xor` bool True)
52
53 -- * Tests
54 (==>) :: forall h raw root.
55 ( Eq h, Eq raw, Show h, Show raw
56 , root ~ Expr_Lambda_Bool IO
57 , Expr_from raw (Expr_Lambda IO root)
58 , Expr_from raw (Expr_Bool root)
59 )
60 => raw -> (Type_Fun_Bool IO h, h, String) -> TestTree
61 (==>) raw expected@(ty_expected::Type_Fun_Bool IO h, _::h, _::String) =
62 testCase (show raw) $
63 (>>= (@?= Right expected)) $
64 case expr_lambda_bool_from (Proxy::Proxy IO) raw of
65 Left err -> return $ Left err
66 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
67 case ty `type_eq` ty_expected of
68 Nothing -> return $ Left $
69 error_lambda_lift $ Error_Expr_Type
70 (error_type_lift $ Error_Type_Unsupported raw) raw
71 Just Refl -> do
72 h <- host_from_expr r
73 return $
74 Right
75 ( ty
76 , h
77 , string_from_expr r
78 -- , (string_from_expr :: Repr_String IO h -> String) r
79 )
80 where
81 error_lambda_lift
82 :: (root ~ Expr_Lambda_Bool IO)
83 => Error_Expr_Lambda (Error_of_Type raw (Type_Root_of_Expr root))
84 (Type_Root_of_Expr root)
85 raw
86 -> Error_of_Expr raw root
87 error_lambda_lift = error_expr_lift
88
89 tests :: TestTree
90 tests = testGroup "Bool" $
91 [ AST "bool" [AST "True" []] ==>
92 ( type_bool
93 , True
94 , "True" )
95 , AST "xor"
96 [ AST "bool" [AST "True" []]
97 , AST "bool" [AST "True" []]
98 ] ==>
99 ( type_bool
100 , False
101 , "(True | True) & !(True & True)" )
102 , AST "app"
103 [ AST "val"
104 [ AST "x" []
105 , AST "Bool" []
106 , AST "var" [AST "x" []]
107 ]
108 , AST "bool" [AST "True" []]
109 ] ==>
110 ( type_bool
111 , True
112 , "(\\x0 -> x0) True" )
113 , AST "app"
114 [ AST "val"
115 [ AST "x" []
116 , AST "Bool" []
117 , AST "xor"
118 [ AST "var" [AST "x" []]
119 , AST "bool" [AST "True" []]
120 ]
121 ]
122 , AST "bool" [AST "True" []]
123 ] ==>
124 ( type_bool
125 , False
126 , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
127 ]