blob: b925c9f791e82c6244f0ec034693e2e4702b58b8 (
plain)
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
121
122
123
124
125
126
127
128
129
130
131
|
{-
- Instant Insanity using Closed Type Families, but no DataKinds
-
- See: http://stackoverflow.com/questions/26538595
-}
{-# OPTIONS_GHC -freduction-depth=400 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
import Prelude hiding (all, flip, map, filter )
data Proxy a = Proxy
main = print (Proxy :: Proxy (Solutions Cubes))
data R -- Red
data G -- Green
data B -- Blue
data W -- White
data Cube u f r b l d
data True
data False
type family And b1 b2 :: * where
And True True = True
And b1 b2 = False
type family NE x y :: * where
NE x x = False
NE x y = True
type family EQ x y :: * where
EQ a a = True
EQ a b = False
data Nil = Nil
data Cons x xs = Cons x xs
type family All l :: * where
All Nil = True
All (Cons False xs) = False
All (Cons True xs) = All xs
type family ListConcat xs ys :: * where
ListConcat Nil ys = ys
ListConcat (Cons x xs) ys = Cons x (ListConcat xs ys)
type family AppendIf b a as :: * where
AppendIf False a as = as
AppendIf True a as = Cons a as
data Rotate
data Twist
data Flip
type family Apply f a :: * where
Apply Rotate (Cube u f r b l d) = (Cube u r b l f d)
Apply Twist (Cube u f r b l d) = (Cube f r u l d b)
Apply Flip (Cube u f r b l d) = (Cube d l b r f u)
type family Map f as :: * where
Map f Nil = Nil
Map f (Cons a as) = Cons (Apply f a) (Map f as)
type family MapAppend f as :: * where
MapAppend f xs = ListConcat xs (Map f xs)
type family MapAppend2 f as :: * where
MapAppend2 f xs = ListConcat xs (MapAppend f (Map f xs))
type family MapAppend3 f as :: * where
MapAppend3 f xs = ListConcat xs (MapAppend2 f (Map f xs))
type family Iterate2 f as :: * where
Iterate2 f Nil = Nil
Iterate2 f (Cons a as) = ListConcat (Cons (Apply f a) (Cons a Nil)) (Iterate2 f as)
type family Iterate3 f as :: * where
Iterate3 f (Cons a as) =
ListConcat (Cons a
(Cons (Apply f a)
(Cons (Apply f (Apply f a))
Nil)))
(Iterate3 f as)
type family Iterate4 f as :: * where
Iterate4 f Nil = Nil
Iterate4 f (Cons a as) =
ListConcat (Cons a
(Cons (Apply f a)
(Cons (Apply f (Apply f a))
(Cons (Apply f (Apply f (Apply f a)))
Nil))))
(Iterate4 f as)
type family Orientations c :: * where
Orientations c = MapAppend3 Rotate (MapAppend2 Twist (MapAppend Flip (Cons c Nil)))
type Cube1 = Cube B G W G B R
type Cube2 = Cube W G B W R R
type Cube3 = Cube G W R B R R
type Cube4 = Cube B R G G W W
type Cubes = Cons Cube1 (Cons Cube2 (Cons Cube3 (Cons Cube4 Nil)))
type family Compatible c d :: * where
Compatible (Cube u1 f1 r1 b1 l1 d1) (Cube u2 f2 r2 b2 l2 d2) =
All (Cons (NE f1 f2) (Cons (NE r1 r2) (Cons (NE b1 b2) (Cons (NE l1 l2) Nil))))
type family Allowed c cs :: * where
Allowed c Nil = True
Allowed c (Cons s ss) = And (Compatible c s) (Allowed c ss)
type family MatchingOrientations as sol :: * where
MatchingOrientations Nil sol = Nil
MatchingOrientations (Cons o os) sol =
AppendIf (Allowed o sol) (Cons o sol) (MatchingOrientations os sol)
type family AllowedCombinations os sols :: * where
AllowedCombinations os Nil = Nil
AllowedCombinations os (Cons sol sols) =
ListConcat (MatchingOrientations os sol) (AllowedCombinations os sols)
type family Solutions c :: * where
Solutions Nil = Cons Nil Nil
Solutions (Cons c cs) = AllowedCombinations (Orientations c) (Solutions cs)
|
