]> Git — Sourcephile - haskell/symantic.git/blob - Language/LOL/Symantic/Expr/Int/Test.hs
init
[haskell/symantic.git] / Language / LOL / Symantic / Expr / Int / 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.Int.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_Int_Vars'
25
26 -- | A few boolean variables.
27 class Sym_Int_Vars repr where
28 x :: repr Int
29 y :: repr Int
30 z :: repr Int
31 instance Sym_Int_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
36 -- * Expressions
37 e1 = int 1 `add` int 0
38 e2 = (int 1 `add` int 0) `add` neg (int 1 `add` int 1)
39 e3 = (int 1 `add` neg (int 0)) `add` (int 1 `add` neg (int 1))
40 e4 = int 0 `add` neg (int 1)
41 e5 = int 1 `add` neg x
42 e6 = x `add` y
43 e7 = (x `add` y) `add` z
44 e8 = x `add` (y `add` int 1)
45
46 -- * Tests
47 (==>) :: forall h raw root.
48 ( Eq h, Eq raw, Show h, Show raw
49 , root ~ Expr_Lambda_Int IO
50 , Expr_from raw (Expr_Lambda IO root)
51 , Expr_from raw (Expr_Int root)
52 )
53 => raw -> (Type_Fun_Int IO h, h, String) -> TestTree
54 (==>) raw expected@(ty_expected::Type_Fun_Int IO h, _::h, _::String) =
55 testCase (show raw) $
56 (>>= (@?= Right expected)) $
57 case expr_lambda_int_from (Proxy::Proxy IO) raw of
58 Left err -> return $ Left err
59 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
60 case ty `type_eq` ty_expected of
61 Nothing -> return $ Left $
62 error_expr (Proxy::Proxy root) $ Error_Expr_Type
63 (error_type_lift $ Error_Type_Unsupported raw) raw
64 Just Refl -> do
65 h <- host_from_expr r
66 return $
67 Right
68 ( ty
69 , h
70 , string_from_expr r
71 -- , (string_from_expr :: Repr_String IO h -> String) r
72 )
73
74 tests :: TestTree
75 tests = testGroup "Int" $
76 [ AST "int" [AST "1" []] ==>
77 ( type_int
78 , 1
79 , "1" )
80 , AST "add"
81 [ AST "int" [AST "1" []]
82 , AST "int" [AST "1" []]
83 ] ==>
84 ( type_int
85 , 2
86 , "1 + 1" )
87 , AST "app"
88 [ AST "val"
89 [ AST "x" []
90 , AST "Int" []
91 , AST "var" [AST "x" []]
92 ]
93 , AST "int" [AST "1" []]
94 ] ==>
95 ( type_int
96 , 1
97 , "(\\x0 -> x0) 1" )
98 , AST "app"
99 [ AST "val"
100 [ AST "x" []
101 , AST "Int" []
102 , AST "add"
103 [ AST "var" [AST "x" []]
104 , AST "int" [AST "1" []]
105 ]
106 ]
107 , AST "int" [AST "1" []]
108 ] ==>
109 ( type_int
110 , 2
111 , "(\\x0 -> x0 + 1) 1" )
112 , AST "let_val"
113 [ AST "x" []
114 , AST "int" [AST "1" []]
115 , AST "add"
116 [ AST "var" [AST "x" []]
117 , AST "int" [AST "1" []]
118 ]
119 ] ==>
120 ( type_int
121 , 2
122 , "let x0 = 1 in x0 + 1" )
123 ]