]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Bool/Test.hs
Integer, Integral, Num
[haskell/symantic.git] / Language / Symantic / Expr / Bool / 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.Bool.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 Control.Monad.IO.Class (MonadIO(..))
16 import Data.Proxy (Proxy(..))
17 import Data.Text (Text)
18 import Data.Type.Equality ((:~:)(Refl))
19 import Prelude hiding ((&&), not, (||))
20
21 import Language.Symantic.Repr
22 import Language.Symantic.Expr
23 import Language.Symantic.Type
24 import Language.Symantic.Trans
25
26 import AST.Test
27
28 -- * Class 'Sym_Bool_Vars'
29
30 -- | A few boolean variables.
31 class Sym_Bool_Vars repr where
32 x :: repr Bool
33 y :: repr Bool
34 z :: repr Bool
35 instance Sym_Bool_Vars Repr_Text where
36 x = Repr_Text $ \_p _v -> "x"
37 y = Repr_Text $ \_p _v -> "y"
38 z = Repr_Text $ \_p _v -> "z"
39 instance -- Trans_Boo_Const
40 ( Sym_Bool repr
41 , Sym_Bool_Vars repr
42 ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
43 x = trans_lift x
44 y = trans_lift y
45 z = trans_lift z
46
47 -- * Expressions
48 e1 = bool True && bool False
49 e2 = (bool True && bool False) || (bool True && bool True)
50 e3 = (bool True || bool False) && (bool True || bool True)
51 e4 = bool True && not (bool False)
52 e5 = bool True && not x
53 e6 = x `xor` y
54 e7 = (x `xor` y) `xor` z
55 e8 = x `xor` (y `xor` bool True)
56
57 -- * Tests
58 type Ex = Expr_Root
59 ( Expr_Lambda
60 .|. Expr_Bool
61 )
62 ex_from = root_expr_from (Proxy::Proxy Ex)
63
64 (==>) ast expected =
65 testCase (show ast) $
66 case ex_from ast of
67 Left err -> Left err @?= Prelude.snd `Arrow.left` expected
68 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
69 case expected of
70 Left (_, err) -> Right ("…"::String) @?= Left err
71 Right (ty_expected::Type_Root_of_Expr Ex h, _::h, _::Text) ->
72 (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
73 case ty `eq_type` ty_expected of
74 Nothing -> Monad.return $ Left $
75 error_expr (Proxy::Proxy Ex) $
76 Error_Expr_Type_mismatch ast
77 (Exists_Type ty)
78 (Exists_Type ty_expected)
79 Just Refl -> do
80 let h = host_from_expr r
81 Monad.return $
82 Right
83 ( ty
84 , h
85 , text_from_expr r
86 -- , (text_from_expr :: Repr_Text h -> Text) r
87 )
88
89 tests :: TestTree
90 tests = testGroup "Bool" $
91 [ AST "bool" [AST "True" []] ==> Right
92 ( type_bool
93 , True
94 , "True" )
95 , AST "int" [AST "1" []] ==> Left (Proxy::Proxy Int,
96 Error_Expr_Alt_Curr $
97 Error_Expr_Unsupported $ AST "int" [AST "1" []])
98 , AST "xor"
99 [ AST "bool" [AST "True" []]
100 , AST "bool" [AST "True" []]
101 ] ==> Right
102 ( type_bool
103 , False
104 , "xor True True" )
105 , AST "$"
106 [ AST "\\"
107 [ AST "x" []
108 , AST "Bool" []
109 , AST "var" [AST "x" []]
110 ]
111 , AST "bool" [AST "True" []]
112 ] ==> Right
113 ( type_bool
114 , True
115 , "(\\x0 -> x0) True" )
116 , let ast = AST "$"
117 [ AST "bool" [AST "True" []]
118 , AST "bool" [AST "True" []]
119 ] in ast ==> Left (Proxy::Proxy Bool,
120 Error_Expr_Alt_Curr $
121 Error_Expr_Type_mismatch ast
122 (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
123 ::Type_Root (Type_Var0 :|: Type_Var1 :|: Type_Fun :|: Type_Bool)
124 ((->) Var0 Var0)))
125 (Exists_Type type_bool))
126 , AST "$"
127 [ AST "\\"
128 [ AST "x" []
129 , AST "Bool" []
130 , AST "xor"
131 [ AST "var" [AST "x" []]
132 , AST "bool" [AST "True" []]
133 ]
134 ]
135 , AST "bool" [AST "True" []]
136 ] ==> Right
137 ( type_bool
138 , False
139 , "(\\x0 -> xor x0 True) True" )
140 , AST "let"
141 [ AST "x" []
142 , AST "bool" [AST "True" []]
143 , AST "xor"
144 [ AST "var" [AST "x" []]
145 , AST "bool" [AST "True" []]
146 ]
147 ] ==> Right
148 ( type_bool
149 , False
150 , "let x0 = True in xor x0 True" )
151 ]