]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Bool/Test.hs
Clarify names, and add commentaries.
[haskell/symantic.git] / Language / Symantic / Compiling / Bool / Test.hs
1 {-# LANGUAGE NoMonomorphismRestriction #-}
2 {-# LANGUAGE UndecidableInstances #-}
3 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
4 {-# OPTIONS_GHC -fno-warn-orphans #-}
5 module Compiling.Bool.Test where
6
7 import Test.Tasty
8
9 import Data.Proxy (Proxy(..))
10 import Data.Text (Text)
11 import qualified Data.Text as Text
12 import Prelude hiding ((&&), not, (||))
13
14 import Language.Symantic.Parsing
15 import Language.Symantic.Typing
16 import Language.Symantic.Compiling
17 import Language.Symantic.Interpreting
18 import Compiling.Term.Test
19
20 import Parsing.Test
21
22 -- * Class 'Sym_Bool_Vars'
23
24 -- | A few boolean variables.
25 class Sym_Bool_Vars repr where
26 x :: repr Bool
27 y :: repr Bool
28 z :: repr Bool
29 instance Sym_Bool_Vars TextI where
30 x = TextI $ \_p _v -> "x"
31 y = TextI $ \_p _v -> "y"
32 z = TextI $ \_p _v -> "z"
33 {-
34 instance -- Trans_Boo_Const
35 ( Sym_Bool repr
36 , Sym_Bool_Vars repr
37 ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
38 x = trans_lift x
39 y = trans_lift y
40 z = trans_lift z
41 -}
42
43 -- * Terms
44 te1 = bool True && bool False
45 te2 = (bool True && bool False) || (bool True && bool True)
46 te3 = (bool True || bool False) && (bool True || bool True)
47 te4 = bool True && not (bool False)
48 te5 = bool True && not x
49 te6 = x `xor` y
50 te7 = (x `xor` y) `xor` z
51 te8 = x `xor` (y `xor` bool True)
52
53 instance
54 ( Inj_Token (Syntax Text) ts Bool
55 {-, Tokenize (Syntax Text) (Syntax Text) ts-} ) =>
56 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Bool) where
57 tokenizeT _t (Syntax "bool" (ast_b : as)) = Just $ do
58 b <- read_syntax ast_b
59 Right $ (as,) $ EToken $ inj_token (Syntax "bool" [ast_b]) $
60 Token_Term_Bool b
61 tokenizeT _t (Syntax "xor" as) = Just $
62 Right $ (as,) $ EToken $ inj_token (Syntax "xor" []) $
63 Token_Term_Bool_xor
64 tokenizeT _t (Syntax "not" as) = Just $
65 Right $ (as,) $ EToken $ inj_token (Syntax "not" []) $
66 Token_Term_Bool_not
67 tokenizeT _t _sy = Nothing
68
69 -- * Tests
70 type Ifaces =
71 [ Proxy Bool
72 , Proxy (->)
73 ]
74 (==>) = test_compile (Proxy::Proxy Ifaces)
75
76 syBool b = Syntax "bool" [Syntax (Text.pack $ Prelude.show b) []]
77
78 tests :: TestTree
79 tests = testGroup "Bool" $
80 [ syBool True ==> Right (ty @Bool, True, "True")
81 , Syntax "xor" [syBool True, syBool True] ==> Right
82 (ty @Bool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
83 , syApp (syLam "x" (sy @Bool) (syVar "x")) (syBool True) ==> Right
84 (ty @Bool, True, "(\\x0 -> x0) True")
85 , syApp
86 (syLam "x" (sy @Bool)
87 (Syntax "xor" [ syVar "x", syBool True ]))
88 (syBool True) ==> Right
89 (ty @Bool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True) True" )
90 , syLet "x" (syBool True)
91 (Syntax "xor" [ syVar "x", syBool True ]) ==> Right
92 (ty @Bool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
93 , testGroup "Error_Term" $
94 [ (syBool True `syApp` syBool True) ==> Left (ty @Bool,
95 Right $ Error_Term_Constraint_Type $
96 Right $ Constraint_Type_App $
97 At (maybeRight $ tokenize $ syBool True) $
98 EType $ ty @Bool)
99 , syApp
100 (syLam "x" (sy @Bool)
101 (Syntax "xor" [ syVar "x", syBool True ]))
102 (sy @Bool) ==> Left (ty @Bool,
103 Left $ Error_Syntax_unsupported $
104 sy @Bool)
105 , let syn = Syntax " "
106 [ syLam "x" (sy @Bool) (syVar "x")
107 ] in syn ==> Left (ty @Bool,
108 Left $ Error_Syntax_unsupported syn)
109 , Syntax " "
110 [ syLam "x" (sy @Bool) (syVar "x")
111 , syBool True
112 , syBool True
113 ] ==> Left (ty @Bool,
114 Right $ Error_Term_Constraint_Type $
115 Right $ Constraint_Type_App $
116 At (maybeRight $ tokenize $
117 Syntax " "
118 [ syLam "x" (sy @Bool) (syVar "x")
119 , syBool True
120 ]) $
121 EType $ ty @Bool)
122 , let syn =
123 syLam "x" (sy @Bool .> sy @Bool)
124 (Syntax " " [syVar "x", syBool True]) in
125 syApp syn (syBool True) ==> Left (ty @Bool,
126 Right $ Error_Term_Constraint_Type $ Right $
127 Constraint_Type_Eq
128 (Right $ At (maybeRight $ tokenize syn) $ EType $ (ty @Bool ~> ty @Bool))
129 (At (maybeRight $ tokenize $ syBool $ True) $ EType $ ty @Bool)
130 )
131 ]
132 ]