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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
{-# LANGUAGE EmptyDataDecls, TypeFamilies, UndecidableInstances,
ScopedTypeVariables, OverlappingInstances, TypeOperators,
FlexibleInstances, NoMonomorphismRestriction,
MultiParamTypeClasses #-}
module IndTypesPerfMerge where
data a :* b = a :* b
infixr 6 :*
data TRUE
data FALSE
data Zero
data Succ a
type family Equals m n
type instance Equals Zero Zero = TRUE
type instance Equals (Succ a) Zero = FALSE
type instance Equals Zero (Succ a) = FALSE
type instance Equals (Succ a) (Succ b) = Equals a b
type family LessThan m n
type instance LessThan Zero Zero = FALSE
type instance LessThan (Succ n) Zero = FALSE
type instance LessThan Zero (Succ n) = TRUE
type instance LessThan (Succ m) (Succ n) = LessThan m n
newtype Tagged n a = Tagged a deriving (Show,Eq)
type family Cond p a b
type instance Cond TRUE a b = a
type instance Cond FALSE a b = b
class Merger a where
type Merged a
type UnmergedLeft a
type UnmergedRight a
mkMerge :: a -> UnmergedLeft a -> UnmergedRight a -> Merged a
class Mergeable a b where
type MergerType a b
merger :: a -> b -> MergerType a b
merge x y = mkMerge (merger x y) x y
data TakeRight a
data TakeLeft a
data DiscardRightHead a b c d
data LeftHeadFirst a b c d
data RightHeadFirst a b c d
data EndMerge
instance Mergeable () () where
type MergerType () () = EndMerge
merger = undefined
instance Mergeable () (a :* b) where
type MergerType () (a :* b) = TakeRight (a :* b)
merger = undefined
instance Mergeable (a :* b) () where
type MergerType (a :* b) () = TakeLeft (a :* b)
merger = undefined
instance Mergeable (Tagged m a :* t1) (Tagged n b :* t2) where
type MergerType (Tagged m a :* t1) (Tagged n b :* t2) =
Cond (Equals m n) (DiscardRightHead (Tagged m a) t1 (Tagged n b) t2)
(Cond (LessThan m n) (LeftHeadFirst (Tagged m a) t1 (Tagged n b) t2)
(RightHeadFirst (Tagged m a ) t1 (Tagged n b) t2))
merger = undefined
instance Merger EndMerge where
type Merged EndMerge = ()
type UnmergedLeft EndMerge = ()
type UnmergedRight EndMerge = ()
mkMerge _ () () = ()
instance Merger (TakeRight a) where
type Merged (TakeRight a) = a
type UnmergedLeft (TakeRight a) = ()
type UnmergedRight (TakeRight a) = a
mkMerge _ () a = a
instance Merger (TakeLeft a) where
type Merged (TakeLeft a) = a
type UnmergedLeft (TakeLeft a) = a
type UnmergedRight (TakeLeft a) = ()
mkMerge _ a () = a
instance
(Mergeable t1 t2,
Merger (MergerType t1 t2),
t1 ~ UnmergedLeft (MergerType t1 t2),
t2 ~ UnmergedRight (MergerType t1 t2)) =>
Merger (DiscardRightHead h1 t1 h2 t2) where
type Merged (DiscardRightHead h1 t1 h2 t2) = h1 :* Merged (MergerType t1 t2)
type UnmergedLeft (DiscardRightHead h1 t1 h2 t2) = h1 :* t1
type UnmergedRight (DiscardRightHead h1 t1 h2 t2) = h2 :* t2
mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 t2) t1 t2
instance
(Mergeable t1 (h2 :* t2),
Merger (MergerType t1 (h2 :* t2)),
t1 ~ UnmergedLeft (MergerType t1 (h2 :* t2)),
(h2 :* t2) ~ UnmergedRight (MergerType t1 (h2 :* t2))) =>
Merger (LeftHeadFirst h1 t1 h2 t2) where
type Merged (LeftHeadFirst h1 t1 h2 t2) = h1 :* Merged (MergerType t1 (h2 :* t2))
type UnmergedLeft (LeftHeadFirst h1 t1 h2 t2) = h1 :* t1
type UnmergedRight (LeftHeadFirst h1 t1 h2 t2) = h2 :* t2
mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 (h2 :* t2)) t1 (h2 :* t2)
instance
(Mergeable (h1 :* t1) t2,
Merger (MergerType (h1 :* t1) t2),
(h1 :* t1) ~ UnmergedLeft (MergerType (h1 :* t1) t2),
t2 ~ UnmergedRight (MergerType (h1 :* t1) t2)) =>
Merger (RightHeadFirst h1 t1 h2 t2) where
type Merged (RightHeadFirst h1 t1 h2 t2) = h2 :* Merged (MergerType (h1 :* t1) t2)
type UnmergedLeft (RightHeadFirst h1 t1 h2 t2) = h1 :* t1
type UnmergedRight (RightHeadFirst h1 t1 h2 t2) = h2 :* t2
mkMerge _ (h1 :* t1) (h2 :* t2) = h2 :* mkMerge (merger (h1 :* t1) t2) (h1 :* t1) t2
|
