]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Eq/Test.hs
init
[haskell/symantic.git] / Language / Symantic / Expr / Eq / Test.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE NoMonomorphismRestriction #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE TypeOperators #-}
6 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
7
8 module Expr.Eq.Test where
9
10 import Test.Tasty
11 import Test.Tasty.HUnit
12
13 import Control.Arrow (left)
14 import Data.Proxy (Proxy(..))
15 import Data.Text (Text)
16 import Data.Type.Equality ((:~:)(Refl))
17 import Prelude hiding ((&&), not, (||), (==))
18
19 import Language.Symantic.Type
20 import Language.Symantic.Expr
21 import Language.Symantic.Repr
22
23 import AST.Test
24
25 -- * Expressions
26 t = bool True
27 f = bool False
28 e1 = if_ ((t && t) == (t || f)) t f
29 e2 = if_ (((t && t) || f) == (t && (t || f))) t f
30 e3 = if_ (not (t == f) == (t == t)) t f
31
32 -- * Tests
33 type Ex lam = Expr_Root (Expr_Lambda lam .|. Expr_Bool .|. Expr_Eq)
34 ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
35
36 (==>) ast expected =
37 testCase (show ast) $
38 case ex_from ast of
39 Left err -> Left err @?= snd `left` expected
40 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
41 case expected of
42 Left (_, err) -> Right ("…"::String) @?= Left err
43 Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
44 (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
45 case ty `eq_type` ty_expected of
46 Nothing -> return $ Left $
47 error_expr (Proxy::Proxy (Ex IO)) $
48 Error_Expr_Type_mismatch ast
49 (Exists_Type ty)
50 (Exists_Type ty_expected)
51 Just Refl -> do
52 h <- host_from_expr r
53 return $
54 Right
55 ( ty
56 , h
57 , text_from_expr r
58 -- , (text_from_expr :: Repr_String IO h -> Text) r
59 )
60
61 tests :: TestTree
62 tests = testGroup "Eq"
63 [ AST "==" [ AST "bool" [AST "True" []]
64 , AST "bool" [AST "True" []]
65 ] ==> Right
66 ( type_bool
67 , True
68 , "True == True" )
69 , AST "app"
70 [ AST "val"
71 [ AST "x" []
72 , AST "Bool" []
73 , AST "==" [ AST "var" [AST "x" []]
74 , AST "not" [AST "var" [AST "x" []]] ]
75 ]
76 , AST "bool" [AST "True" []]
77 ] ==> Right
78 ( type_bool
79 , False
80 , "(\\x0 -> x0 == !x0) True" )
81 ]