]> 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 ast root.
55 ( Eq h, Eq ast, Show h, Show ast
56 , root ~ Expr_Lambda_Bool IO
57 , Expr_from ast (Expr_Lambda IO root)
58 , Expr_from ast (Expr_Bool root)
59 )
60 => ast -> (Type_Fun_Bool IO h, h, String) -> TestTree
61 (==>) ast expected@(ty_expected::Type_Fun_Bool IO h, _::h, _::String) =
62 testCase (show ast) $
63 (>>= (@?= Right expected)) $
64 case expr_lambda_bool_from (Proxy::Proxy IO) ast 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_expr (Proxy::Proxy root) $ Error_Expr_Type
70 (error_type_lift $ Error_Type_Unsupported_here ast) ast
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
81 tests :: TestTree
82 tests = testGroup "Bool" $
83 [ AST "bool" [AST "True" []] ==>
84 ( type_bool
85 , True
86 , "True" )
87 , AST "xor"
88 [ AST "bool" [AST "True" []]
89 , AST "bool" [AST "True" []]
90 ] ==>
91 ( type_bool
92 , False
93 , "(True | True) & !(True & True)" )
94 , AST "app"
95 [ AST "val"
96 [ AST "x" []
97 , AST "Bool" []
98 , AST "var" [AST "x" []]
99 ]
100 , AST "bool" [AST "True" []]
101 ] ==>
102 ( type_bool
103 , True
104 , "(\\x0 -> x0) True" )
105 , AST "app"
106 [ AST "val"
107 [ AST "x" []
108 , AST "Bool" []
109 , AST "xor"
110 [ AST "var" [AST "x" []]
111 , AST "bool" [AST "True" []]
112 ]
113 ]
114 , AST "bool" [AST "True" []]
115 ] ==>
116 ( type_bool
117 , False
118 , "(\\x0 -> (x0 | True) & !(x0 & True)) True" )
119 , AST "let_val"
120 [ AST "x" []
121 , AST "bool" [AST "True" []]
122 , AST "xor"
123 [ AST "var" [AST "x" []]
124 , AST "bool" [AST "True" []]
125 ]
126 ] ==>
127 ( type_bool
128 , False
129 , "let x0 = True in (x0 | True) & !(x0 & True)" )
130 ]