1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
{-# LANGUAGE TemplateHaskell #-}
module TestNat where
import Language.Haskell.TH
import Text.Printf
import TypeLevel.Number.Nat as N
import TypeLevel.Number.Int as I
----------------------------------------------------------------
-- Natural numbers
testAdd :: Integer -> Integer -> ExpQ
testAdd n m =
[| let flag = (n+m) == (N.toInt $ addN (undefined :: $(natT n)) (undefined :: $(natT m)) :: Integer)
in test "+" n m flag
|]
testSub :: Integer -> Integer -> ExpQ
testSub n m =
[| let flag = (n-m) == (N.toInt $ subN (undefined :: $(natT n)) (undefined :: $(natT m)) :: Integer)
in test "-" n m flag
|]
testMul :: Integer -> Integer -> ExpQ
testMul n m =
[| let flag = (n*m) == (N.toInt $ mulN (undefined :: $(natT n)) (undefined :: $(natT m)) :: Integer)
in test "*" n m flag
|]
----------------------------------------------------------------
-- Integer numbers
testAddZ :: Integer -> Integer -> ExpQ
testAddZ n m =
[| let flag = (n+m) == (I.toInt $ addN (undefined :: $(intT n)) (undefined :: $(intT m)) :: Integer)
in test "+" n m flag
|]
testSubZ :: Integer -> Integer -> ExpQ
testSubZ n m =
[| let flag = (n-m) == (I.toInt $ subN (undefined :: $(intT n)) (undefined :: $(intT m)) :: Integer)
in test "-" n m flag
|]
testMulZ :: Integer -> Integer -> ExpQ
testMulZ n m =
[| let flag = (n*m) == (I.toInt $ mulN (undefined :: $(intT n)) (undefined :: $(intT m)) :: Integer)
in test "*" n m flag
|]
test :: String -> Integer -> Integer -> Bool -> IO Bool
test op n m flag = do
_ <- printf "%3i %s %3i : %s\n" n op m (text flag)
return flag
where
text :: Bool -> String
text True = "OK"
text False = "Failed"
|
