Ticket #8095: Types.hs

File Types.hs, 2.7 KB (added by MikeIzbicki, 6 years ago)
Line 
1import System.Environment
2
3code :: Int -> String -> String -> String
4code i familyTest instanceTest = concat $ map (++"\n") $
5    [ "{-# LANGUAGE TypeOperators,DataKinds,KindSignatures,TypeFamilies,PolyKinds,UndecidableInstances #-}"
6    , "import GHC.TypeLits"
7
8    , "data Nat1 = Zero | Succ Nat1"
9    ]
10    ++
11    case head familyTest of
12        'a' -> 
13            [ "type family Replicate1 (n :: Nat1) (x::a) :: [a]"
14            , "type instance Replicate1 Zero x = '[]"
15            , "type instance Replicate1 (Succ n) x = x ': (Replicate1 n x)"
16            ]
17        'b' -> 
18            [ "type family Replicate1 (n :: Nat1) (x::a) :: [a]"
19            , "type instance Replicate1 n x = Replicate1' '[] n x "
20            , "type family Replicate1' (acc::[a]) (n :: Nat1) (x::a)  :: [a]"
21            , "type instance Replicate1' acc Zero x = acc"
22            , "type instance Replicate1' acc (Succ n) x = Replicate1' (x ': acc) n x "
23            ]
24        'c' -> 
25            [ "type family Replicate1 (n :: Nat1) (x::a) :: [a]"
26            , "type instance Replicate1 n x = Replicate1' n x '[]"
27            , "type family Replicate1' (n :: Nat1) (x::a) (acc::[a]) :: [a]"
28            , "type instance Replicate1' Zero x acc = acc"
29            , "type instance Replicate1' (Succ n) x acc = Replicate1' n x (x ': acc)"
30            ]
31    ++
32    [ "class Class a where"
33    , "    f :: a -> a"
34
35    , "data Data (xs::a) = X | Y"
36    , "    deriving (Read,Show)"
37   
38    , "main = print test1"
39    ]
40    ++
41    case head instanceTest of
42        'a' -> 
43            [ "instance (xs ~ Replicate1 ("++mkNat1 i++") ()) => Class (Data xs) where"
44            , "    f X = Y"
45            , "    f Y = X"
46            , "test1 = f (X :: Data ( Replicate1 ("++mkNat1 i++") () ))"
47            ]
48        'b' -> 
49            [ "instance (xs ~ ("++mkList i++") ) => Class (Data xs) where"
50            , "    f X = Y"
51            , "    f Y = X"
52            , "test1 = f (X :: Data ( Replicate1 ("++mkNat1 i++") () ))"
53            ]
54        'c' -> 
55            [ "instance (xs ~ Replicate1 ("++mkNat1 i++") ()) => Class (Data xs) where"
56            , "    f X = Y"
57            , "    f Y = X"
58            , "test1 = f (X :: Data ( ("++mkList i++") ))"
59            ]
60        'd' -> 
61            [ "instance (xs ~ ("++mkList i++") ) => Class (Data xs) where"
62            , "    f X = Y"
63            , "    f Y = X"
64            , "test1 = f (X :: Data ( ("++mkList i++") ))"
65            ]
66
67mkList :: Int -> String
68mkList 0 = " '[] "
69mkList i = " () ': " ++ mkList (i-1)
70
71mkNat1 :: Int -> String
72mkNat1 0 = " Zero "
73mkNat1 i = " Succ ( " ++ mkNat1 (i-1) ++ ")"
74
75main = do
76    numstr : familyTest : instanceTest : xs <- getArgs
77    let num = read numstr :: Int
78   
79    putStrLn $ code num familyTest instanceTest
80