]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Bool/Test.hs
init
[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 Control.Arrow (left)
14 -- import Data.Functor.Identity (Identity)
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 fun) 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 lam = Expr_Root (Expr_Lambda lam .|. Expr_Bool)
59 ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
60
61 (==>) ast expected =
62 testCase (show ast) $
63 case ex_from ast of
64 Left err -> Left err @?= snd `left` expected
65 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
66 case expected of
67 Left (_, err) -> Right ("…"::String) @?= Left err
68 Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
69 (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
70 case ty `eq_type` ty_expected of
71 Nothing -> return $ Left $
72 error_expr (Proxy::Proxy (Ex IO)) $
73 Error_Expr_Type_mismatch ast
74 (Exists_Type ty)
75 (Exists_Type ty_expected)
76 Just Refl -> do
77 h <- host_from_expr r
78 return $
79 Right
80 ( ty
81 , h
82 , text_from_expr r
83 -- , (text_from_expr :: Repr_Text IO h -> String) r
84 )
85
86 tests :: TestTree
87 tests = testGroup "Bool" $
88 [ AST "bool" [AST "True" []] ==> Right
89 ( type_bool
90 , True
91 , "True" )
92 , AST "int" [AST "1" []] ==> Left (Proxy::Proxy Int,
93 Error_Expr_Alt_Curr $
94 Error_Expr_Unsupported $ AST "int" [AST "1" []])
95 , AST "xor"
96 [ AST "bool" [AST "True" []]
97 , AST "bool" [AST "True" []]
98 ] ==> Right
99 ( type_bool
100 , False
101 , "xor 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 ] ==> Right
110 ( type_bool
111 , True
112 , "(\\x0 -> x0) True" )
113 , let ast = AST "app"
114 [ AST "bool" [AST "True" []]
115 , AST "bool" [AST "True" []]
116 ] in ast ==> Left (Proxy::Proxy Bool,
117 Error_Expr_Alt_Curr $
118 Error_Expr_Type_mismatch ast
119 (Exists_Type (type_var SZero `type_fun` type_var (SSucc SZero)
120 ::Type_Root (Type_Var :|: Type_Fun IO :|: Type_Bool)
121 (Lambda IO Zero (Succ Zero))))
122 (Exists_Type type_bool))
123 , AST "app"
124 [ AST "val"
125 [ AST "x" []
126 , AST "Bool" []
127 , AST "xor"
128 [ AST "var" [AST "x" []]
129 , AST "bool" [AST "True" []]
130 ]
131 ]
132 , AST "bool" [AST "True" []]
133 ] ==> Right
134 ( type_bool
135 , False
136 , "(\\x0 -> xor x0 True) True" )
137 , AST "let_val"
138 [ AST "x" []
139 , AST "bool" [AST "True" []]
140 , AST "xor"
141 [ AST "var" [AST "x" []]
142 , AST "bool" [AST "True" []]
143 ]
144 ] ==> Right
145 ( type_bool
146 , False
147 , "let x0 = True in xor x0 True" )
148 ]