]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Bool/Test.hs
Fix lambda application.
[haskell/symantic.git] / Language / Symantic / Compiling / Bool / Test.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE NoMonomorphismRestriction #-}
5 {-# LANGUAGE Rank2Types #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE TypeOperators #-}
8 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
9 module Compiling.Bool.Test where
10
11 import Test.Tasty
12 import Test.Tasty.HUnit
13
14 import qualified Control.Arrow as Arrow
15 import qualified Control.Monad as Monad
16 -- import Control.Monad.IO.Class (MonadIO(..))
17 import Data.Proxy (Proxy(..))
18 import Data.Text (Text)
19 import Data.Type.Equality ((:~:)(Refl))
20 import Prelude hiding ((&&), not, (||))
21
22 import Language.Symantic.Typing
23 import Language.Symantic.Compiling
24 import Language.Symantic.Interpreting
25
26 -- * Class 'Sym_Bool_Vars'
27
28 -- | A few boolean variables.
29 class Sym_Bool_Vars repr where
30 x :: repr Bool
31 y :: repr Bool
32 z :: repr Bool
33 instance Sym_Bool_Vars TextI where
34 x = TextI $ \_p _v -> "x"
35 y = TextI $ \_p _v -> "y"
36 z = TextI $ \_p _v -> "z"
37 {-
38 instance -- Trans_Boo_Const
39 ( Sym_Bool repr
40 , Sym_Bool_Vars repr
41 ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
42 x = trans_lift x
43 y = trans_lift y
44 z = trans_lift z
45 -}
46
47 -- * Terms
48 te1 = bool True && bool False
49 te2 = (bool True && bool False) || (bool True && bool True)
50 te3 = (bool True || bool False) && (bool True || bool True)
51 te4 = bool True && not (bool False)
52 te5 = bool True && not x
53 te6 = x `xor` y
54 te7 = (x `xor` y) `xor` z
55 te8 = x `xor` (y `xor` bool True)
56
57 -- * Tests
58 type Ifaces =
59 [ Proxy (->)
60 , Proxy Bool
61 ]
62 type Consts = Consts_of_Ifaces Ifaces
63
64 (==>) (ast::Syntax Text) expected =
65 testCase (show ast) $
66 case root_term_from ast of
67 Left err -> Left err @?= Prelude.snd `Arrow.left` expected
68 Right (ETerm ty (Term te)::ETerm Ifaces) ->
69 case expected of
70 Left (_, err) -> Right ("…"::Text) @?= Left err
71 Right (ty_expected::Type Consts h, _::h, _::Text) ->
72 (Monad.>>= (@?= (\(_::Type Consts h, err) -> err) `Arrow.left` expected)) $
73 case ty `eq_type` ty_expected of
74 Nothing -> Monad.return $ Left $
75 Error_Term_Type_mismatch
76 (At Nothing $ EType ty)
77 (At Nothing $ EType ty_expected)
78 Just Refl -> do
79 let h = host_from_term te
80 Monad.return $
81 Right
82 ( ty
83 , h
84 , text_from_term te
85 -- , (text_from_expr :: Repr_Text h -> Text) r
86 )
87
88 tests :: TestTree
89 tests = testGroup "Bool" $
90 [ syTrue ==> Right (tyBool, True, "True")
91 , Syntax "xor" [syTrue, syTrue] ==> Right
92 (tyBool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
93 , syApp
94 (syLam (Syntax "x" []) syBool
95 (Syntax "x" []))
96 syTrue ==> Right
97 (tyBool, True, "(\\x0 -> x0) True")
98 , syApp
99 (syLam (Syntax "x" []) syBool
100 (Syntax "xor"
101 [ Syntax "x" []
102 , syTrue
103 ]))
104 syTrue ==> Right
105 (tyBool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True) True" )
106 , syLet (Syntax "x" []) syTrue
107 (Syntax "xor"
108 [ Syntax "x" []
109 , syTrue
110 ]) ==> Right
111 (tyBool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
112 , testGroup "Error_Term" $
113 [ syApp syTrue syTrue ==> Left (tyBool,
114 Error_Term_Type_is_not_an_application $ At (Just syTrue) $
115 EType tyBool)
116 , syApp
117 (syLam
118 (Syntax "x" []) syBool
119 (Syntax "xor"
120 [ Syntax "x" []
121 , syTrue
122 ])
123 )
124 syBool ==> Left (tyBool,
125 Error_Term_unknown $ At (Just syBool) $
126 "Bool")
127 , let sy = Syntax " "
128 [ syLam (Syntax "x" []) syBool
129 (Syntax "x" [])
130 ] in sy ==> Left (tyBool,
131 Error_Term_Syntax $ Error_Syntax_more_arguments_needed $
132 At (Just sy) 2)
133 , let sy = Syntax " "
134 [ syLam (Syntax "x" []) syBool
135 (Syntax "x" [])
136 , syTrue
137 , syTrue
138 ] in sy ==> Left (tyBool,
139 Error_Term_Type_is_not_an_application $
140 At (Just sy) $ EType tyBool)
141 , let sy =
142 syLam (Syntax "x" []) (syBool .> syBool)
143 (Syntax " " [Syntax "x" [], syTrue]) in
144 syApp sy syTrue ==> Left (tyBool,
145 Error_Term_Type_mismatch
146 (At (Just sy) $ EType $ (tyBool ~> tyBool))
147 (At (Just $ syTrue) $ EType tyBool)
148 )
149 ]
150 ]