]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Bool/Test.hs
Add Typing.Family and Compiling.MonoFunctor.
[haskell/symantic.git] / Language / Symantic / Compiling / Bool / Test.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE NoMonomorphismRestriction #-}
3 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
4 module Compiling.Bool.Test where
5
6 import Test.Tasty
7
8 import Data.Proxy (Proxy(..))
9 import Prelude hiding ((&&), not, (||))
10
11 import Language.Symantic.Typing
12 import Language.Symantic.Compiling
13 import Language.Symantic.Interpreting
14 import Compiling.Term.Test
15
16 -- * Class 'Sym_Bool_Vars'
17
18 -- | A few boolean variables.
19 class Sym_Bool_Vars repr where
20 x :: repr Bool
21 y :: repr Bool
22 z :: repr Bool
23 instance Sym_Bool_Vars TextI where
24 x = TextI $ \_p _v -> "x"
25 y = TextI $ \_p _v -> "y"
26 z = TextI $ \_p _v -> "z"
27 {-
28 instance -- Trans_Boo_Const
29 ( Sym_Bool repr
30 , Sym_Bool_Vars repr
31 ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
32 x = trans_lift x
33 y = trans_lift y
34 z = trans_lift z
35 -}
36
37 -- * Terms
38 te1 = bool True && bool False
39 te2 = (bool True && bool False) || (bool True && bool True)
40 te3 = (bool True || bool False) && (bool True || bool True)
41 te4 = bool True && not (bool False)
42 te5 = bool True && not x
43 te6 = x `xor` y
44 te7 = (x `xor` y) `xor` z
45 te8 = x `xor` (y `xor` bool True)
46
47 -- * Tests
48 type Ifaces =
49 [ Proxy (->)
50 , Proxy Bool
51 ]
52 (==>) = test_term_from (Proxy::Proxy Ifaces)
53
54 tests :: TestTree
55 tests = testGroup "Bool" $
56 [ syTrue ==> Right (tyBool, True, "True")
57 , Syntax "xor" [syTrue, syTrue] ==> Right
58 (tyBool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
59 , syApp
60 (syLam (Syntax "x" []) syBool
61 (Syntax "x" []))
62 syTrue ==> Right
63 (tyBool, True, "(\\x0 -> x0) True")
64 , syApp
65 (syLam (Syntax "x" []) syBool
66 (Syntax "xor"
67 [ Syntax "x" []
68 , syTrue
69 ]))
70 syTrue ==> Right
71 (tyBool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True) True" )
72 , syLet (Syntax "x" []) syTrue
73 (Syntax "xor"
74 [ Syntax "x" []
75 , syTrue
76 ]) ==> Right
77 (tyBool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
78 , testGroup "Error_Term" $
79 [ syApp syTrue syTrue ==> Left (tyBool,
80 Error_Term_Type_is_not_an_application $ At (Just syTrue) $
81 EType tyBool)
82 , syApp
83 (syLam
84 (Syntax "x" []) syBool
85 (Syntax "xor"
86 [ Syntax "x" []
87 , syTrue
88 ])
89 )
90 syBool ==> Left (tyBool,
91 Error_Term_unknown $ At (Just syBool) $
92 "Bool")
93 , let sy = Syntax " "
94 [ syLam (Syntax "x" []) syBool
95 (Syntax "x" [])
96 ] in sy ==> Left (tyBool,
97 Error_Term_Syntax $ Error_Syntax_more_arguments_needed $
98 At (Just sy) 2)
99 , let sy = Syntax " "
100 [ syLam (Syntax "x" []) syBool
101 (Syntax "x" [])
102 , syTrue
103 , syTrue
104 ] in sy ==> Left (tyBool,
105 Error_Term_Type_is_not_an_application $
106 At (Just sy) $ EType tyBool)
107 , let sy =
108 syLam (Syntax "x" []) (syBool .> syBool)
109 (Syntax " " [Syntax "x" [], syTrue]) in
110 syApp sy syTrue ==> Left (tyBool,
111 Error_Term_Type_mismatch
112 (At (Just sy) $ EType $ (tyBool ~> tyBool))
113 (At (Just $ syTrue) $ EType tyBool)
114 )
115 ]
116 ]