はじめに
「PureScriptにはこんなに表現力の高い型システムがあるんだ！」というような気持ちで読んでもらえれば丁度いいと思います。
この方法を使うと「渡された値は整数か？」と同じ要領で「渡されたルービックキューブは不正ではないか？解くことが可能か？」といった検査がコンパイル時にできてしまいます！
※本記事で扱うルービックキューブは2x2x2のものです。
未公開のままだった記事を成仏させるために公開したので、PureScriptのバージョンが結構古めです（v0.13.5くらい）。
注意点
型レベル計算を多用するため、IDEがめちゃくちゃ頑張ることになります。エディタを開いているだけでCPUやメモリの使用率がとても上がる点にご注意ください（IDEを切っていれば平気）。
解く手順
今回の手順は以下の通りです。
- 完成しているかどうか確認する。
-
- で解けていたら、「直前に回した回転記号リスト」を返して終了。
-
- で解けていなかったら、以下に続く。
- 各回転記号を「直前に回した回転記号リスト」の後ろに結合したものを全てキューに入れる。
- キューの先頭を取り出す。
-
- で取り出した回転記号リストに従ってキューブを回す。
-
- に戻る。
幅優先探索を用いています。
回転記号
ルービックキューブの回転を表すために、以下のような回転記号が用いられます。
| 回転記号 | 意味 |
|---|---|
| f | 前面を時計回りに回す |
| b | 後面を時計回りに回す |
| r | 右面を時計回りに回す |
| l | 左面を時計回りに回す |
| u | 上面を時計回りに回す |
| d | 下面を時計回りに回す |
| x | 下面が正面になるように持ち替え |
| y | 右面が正面になるように持ち替え |
| z | 左面が上面になるように持ち替え |
| ○' | ○の逆 |
実際に書いていく
さっそくルービックキューブを解く準備をしていきます。
キューブをSymbolで表現する
こんなふうに展開した形式のキューブを用意したいです。
RR
RR
WWBBYYGG
WWBBYYGG
OO
OO
これは、このように表すことにします。
"RRRRWWBBYYGGWWBBYYGGOOOO"
SProxyに渡して幽霊型の値を作ることができます。
SProxy :: SProxy "RRRRWWBBYYGGWWBBYYGGOOOO"
キューブを分解・合成する
class ConsCube
(mode :: Symbol)
(c1 :: Symbol) (c2 :: Symbol) (c3 :: Symbol) (c4 :: Symbol)
(c5 :: Symbol) (c6 :: Symbol) (c7 :: Symbol) (c8 :: Symbol)
(c9 :: Symbol) (c10 :: Symbol) (c11 :: Symbol) (c12 :: Symbol)
(c13 :: Symbol) (c14 :: Symbol) (c15 :: Symbol) (c16 :: Symbol)
(c17 :: Symbol) (c18 :: Symbol) (c19 :: Symbol) (c20 :: Symbol)
(c21 :: Symbol) (c22 :: Symbol) (c23 :: Symbol) (c24 :: Symbol) (cube :: Symbol)
| mode
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24
-> cube
, mode
cube ->
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24
instance deConsCube ::
( Cons c1 t1 cube, Cons c2 t2 t1 , Cons c3 t3 t2 , Cons c4 t4 t3
, Cons c5 t5 t4 , Cons c6 t6 t5 , Cons c7 t7 t6 , Cons c8 t8 t7
, Cons c9 t9 t8 , Cons c10 t10 t9 , Cons c11 t11 t10, Cons c12 t12 t11
, Cons c13 t13 t12 , Cons c14 t14 t13, Cons c15 t15 t14, Cons c16 t16 t15
, Cons c17 t17 t16 , Cons c18 t18 t17, Cons c19 t19 t18, Cons c20 t20 t19
, Cons c21 t21 t20 , Cons c22 t22 t21, Cons c23 t23 t22, Cons c24 "" t23
) => ConsCube "DeCon"
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
else instance consCube ::
( Cons c1 "" t1 , Cons t1 c2 t2 , Append t2 c3 t3 , Append t3 c4 t4
, Append t4 c5 t5 , Append t5 c6 t6 , Append t6 c7 t7 , Append t7 c8 t8
, Append t8 c9 t9 , Append t9 c10 t10, Append t10 c11 t11, Append t11 c12 t12
, Append t12 c13 t13, Append t13 c14 t14, Append t14 c15 t15, Append t15 c16 t16
, Append t16 c17 t17, Append t17 c18 t18, Append t18 c19 t19, Append t19 c20 t20
, Append t20 c21 t21, Append t21 c22 t22, Append t22 c23 t23, Append t23 c24 cube
) => ConsCube "Con"
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
このクラスを以下のように呼び出すと分解や合成が可能です。
-- 分解
ConsCube "DeCon"
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24
"RRRRWWBBYYGGWWBBYYGGOOOO"
-- 合成
ConsCube "Con"
"R" "R" "R" "R" "W" "W" "B" "B" "Y" "Y" "G" "G"
"W" "W" "B" "B" "Y" "Y" "G" "G" "O" "O" "O" "O" cube
キューブを表示する
ConsCube型クラスを使って分解し、展開図の形になるように文字列として連結していきます。reflectSymbol関数はSymbolをStringに変換する関数で、これを使うためにはIsSymbol型クラス制約が必要になります。
showCube
:: forall c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
. ConsCube "DeCon"
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
=> IsSymbol c1 => IsSymbol c2 => IsSymbol c3 => IsSymbol c4 => IsSymbol c5 => IsSymbol c6
=> IsSymbol c7 => IsSymbol c8 => IsSymbol c9 => IsSymbol c10 => IsSymbol c11 => IsSymbol c12
=> IsSymbol c13 => IsSymbol c14 => IsSymbol c15 => IsSymbol c16 => IsSymbol c17 => IsSymbol c18
=> IsSymbol c19 => IsSymbol c20 => IsSymbol c21 => IsSymbol c22 => IsSymbol c23 => IsSymbol c24
=> SProxy cube -> String
showCube _ =
" " <> " " <> c1 <> c2
<> nl <> " " <> " " <> c3 <> c4
<> nl <> c5 <> c6 <> c7 <> c8 <> c9 <> c10 <> c11 <> c12
<> nl <> c13 <> c14 <> c15 <> c16 <> c17 <> c18 <> c19 <> c20
<> nl <> " " <> " " <> c21 <> c22
<> nl <> " " <> " " <> c23 <> c24
where
nl = "\n"
c1 = reflectSymbol (SProxy :: SProxy c1 )
c2 = reflectSymbol (SProxy :: SProxy c2 )
c3 = reflectSymbol (SProxy :: SProxy c3 )
c4 = reflectSymbol (SProxy :: SProxy c4 )
c5 = reflectSymbol (SProxy :: SProxy c5 )
c6 = reflectSymbol (SProxy :: SProxy c6 )
c7 = reflectSymbol (SProxy :: SProxy c7 )
c8 = reflectSymbol (SProxy :: SProxy c8 )
c9 = reflectSymbol (SProxy :: SProxy c9 )
c10 = reflectSymbol (SProxy :: SProxy c10)
c11 = reflectSymbol (SProxy :: SProxy c11)
c12 = reflectSymbol (SProxy :: SProxy c12)
c13 = reflectSymbol (SProxy :: SProxy c13)
c14 = reflectSymbol (SProxy :: SProxy c14)
c15 = reflectSymbol (SProxy :: SProxy c15)
c16 = reflectSymbol (SProxy :: SProxy c16)
c17 = reflectSymbol (SProxy :: SProxy c17)
c18 = reflectSymbol (SProxy :: SProxy c18)
c19 = reflectSymbol (SProxy :: SProxy c19)
c20 = reflectSymbol (SProxy :: SProxy c20)
c21 = reflectSymbol (SProxy :: SProxy c21)
c22 = reflectSymbol (SProxy :: SProxy c22)
c23 = reflectSymbol (SProxy :: SProxy c23)
c24 = reflectSymbol (SProxy :: SProxy c24)
次のように呼び出せます。
main :: Effect Unit
main = log $ showCube (SProxy :: SProxy "RRRRWWBBYYGGWWBBYYGGOOOO")
実行結果
RR
RR
WWBBYYGG
WWBBYYGG
OO
OO
キューブを回転させる
まずは前面の回転だけを考えることにします。
回転記号のためのカインドと型を作る
foreign import kind Notation
foreign import data F :: Notation
foreign import data F' :: Notation
前面の回転記号であるfとその反対のf'のために型を作り、Notationというカインドにしました。
キューブを回転させる型クラスを作る
class Rotate (notation :: Notation) (cube :: Symbol) (rotated :: Symbol) | notation cube -> rotated
instance rotateF ::
( ConsCube "DeCon" c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
, ConsCube "Con" c7 c2 c15 c4 c6 c14 c21 c8 c9 c10 c11 c3
c5 c13 c23 c16 c17 c18 c19 c1 c20 c22 c12 c24 rotated
) => Rotate F cube rotated
instance rotateF' ::
( Rotate F cube r'
, Rotate F r' r''
, Rotate F r'' rotate
) => Rotate F' cube rotated
rotateFではキューブを分解し、f回転後の状態に並べ替えて結合し直します。その反対のrotateF'ではrotateFを呼び出した結果を再びrotateFに渡すことを3回繰り返します（ルービックキューブは4回回すと元に戻るので、ある方向への3回転とその反対方向への1回転は同じ結果になります）。
回転順序を表すカインドPathを作る
foreign import kind Path
foreign import data Path :: Notation -> Path -> Path
foreign import data PNil :: Path
data PProxy (p :: Path) = PProxy
class RotatePath (path :: Path) (cube :: Symbol) (rotated :: Symbol) | cube path -> rotated
instance rotatedPathNil :: RotatePath PNil cube cube
instance rotatedPath ::
( Rotate notation cube cube'
, RotatePath tail cube' cube''
, TypeEquals (SProxy cube'') (SProxy rotated)
) => RotatePath (Path notation tail) cube rotated
class AppendPath (pl :: Path) (pr :: Path) (plr :: Path) | pl pr -> plr
instance appendPathNil :: AppendPath PNil pr pr
instance appendPath ::
( AppendPath tail pr plr'
, TypeEquals (PProxy (Path head plr')) (PProxy plr)
) => AppendPath (Path head tail) pr plr
PathとRotatePathを作ることによって、複数回の回転をシンプルに表せるようになります。
-- これが
instance rotateF' ::
( Rotate F cube r'
, Rotate F r' r''
, Rotate F r'' rotate
) => Rotate F' cube rotated
-- こうなる！
instance rotateF' ::
( RotatePath
(Path F (Path F (Path F PNil)))
cube rotated
) => Rotate F' cube rotated
中間の変数が消えてとても読みやすくなります。
また、AppendPathクラスはPathとPathを連結するための型クラスです。これは後ほど使います。
Pathを保持するキューを作る
foreign import kind Queue
foreign import data Queue :: Path -> Queue -> Queue
foreign import data QNil :: Queue
data QProxy (q :: Queue) = QProxy
class Enqueue (queue :: Queue) (path :: Path) (queue' :: Queue) | queue path -> queue'
instance enqueueNil :: Enqueue QNil path (Queue path QNil)
instance enqueue ::
( Enqueue tail newPath q'
, TypeEquals (QProxy (Queue path q')) (QProxy queue')
) => Enqueue (Queue path tail) newPath queue'
class Dequeue (queue :: Queue) (path :: Path) (queue' :: Queue) | queue -> path queue'
instance dequeueNil :: Dequeue (Queue path tail) path tail
instance dequeue :: Dequeue QNil PNil QNil
型レベルのキューです。Enqueueによってキューの末尾にPathを追加、Dequeueによってキューの先頭からPathを取り出すことができます。キューブの状態を各回転順序ごとに調べていく幅優先探索のために用います。
使用例
test1 :: QProxy (Queue (Path F PNil) QNil)
test1 = QProxy :: (forall q. Enqueue QNil (Path F PNil) q => QProxy q)
test2 :: PProxy (Path F PNil)
test2 = PProxy :: (forall q' q'' p. Enqueue QNil (Path F PNil) q' => Dequeue q' p q'' => PProxy p)
探索候補をキューに入れる
class EnqueueAllNotation (queue :: Queue) (currPath :: Path) (queue' :: Queue) | queue -> queue'
instance enqueueAllPath ::
( TypeEquals (QProxy queue) (QProxy q')
, AppendPath currPath (Path F PNil) pF
, Enqueue q' pF qF
, AppendPath currPath (Path F' PNil) pF'
, Enqueue qF pF' qF'
, TypeEquals (QProxy qF') (QProxy queue')
) => EnqueueAllNotation queue currPath queue'
これで現在のPathに対する次の深さの探索候補をすべてキューに追加することができます。
使用例
test1 :: QProxy (Queue (Path F PNil) (Queue (Path F' PNil) QNil))
test1 = QProxy :: forall q. EnqueueAllNotation QNil PNil q => QProxy q
test2 :: QProxy (Queue (Path F (Path F PNil)) (Queue (Path F (Path F' PNil)) QNil))
test2 = QProxy :: forall q. EnqueueAllNotation QNil (Path F PNil) q => QProxy q
上の例では、queueが空（QNil）で現在のpathが空（PNil）のときはqueue'がQueue (Path F PNil) (Queue (Path F' PNil) QNil)になり（test1）、queueが空で現在のpathがPath F PNilのときはqueue'がQueue (Path F' PNil) (Queue (Path F (Path F PNil)) (Queue (Path F (Path F' PNil)) QNil))になる（test2）ことを確かめています。
解く
ここまで積み上げてきたパーツを組み合わせ、実際に解いていきます。
cubeを渡すと完成までの回転順序をpathとして導出してくれる型クラスSolveを作ります。
class Solve (cube :: Symbol) (path :: Path) | cube -> path
instance initSolve ::
(SolveImpl cube "RRRRWWBBYYGGWWBBYYGGOOOO" prev QNil PNil path) => Solve cube path
class SolveImpl
(cube :: Symbol)
(goal :: Symbol)
(prevCube :: Symbol)
(queue :: Queue)
(currPath :: Path)
(path :: Path)
| cube goal -> path
instance solved :: SolveImpl goal goal prev queue currPath PNil
else instance solved' :: SolveImpl cube goal goal queue currPath path
else instance solveImpl ::
( EnqueueAllNotation queue currPath q
, Dequeue q pHead qTail
, RotatePath pHead cube rotated
, Equals rotated goal isEq
, If isEq (PProxy pHead) (PProxy path) (PProxy path)
, SolveImpl cube goal rotated qTail pHead path
) => SolveImpl cube goal prev queue currPath path
このように作りました。
SolveImplで行っているのは何の工夫もないただの幅優先探索で、ゴールはSolveのインスタンスinitSolveから渡された完成状態のキューブです。cubeとgoalが一致したところのcurrPath（直前に回した回転記号リスト）を返して終了します。
型クラスSolveの使い方
まだ前面のfとf'しか考えていないため、前面だけをシャッフルして解かせてみます。
まずは前面を時計回りに1回だけ回した結果のキューブを見ます。
-- f方向に回す
shuffle :: SProxy "BRBRWWOBYYGRWWOBYYGRGOGO"
shuffle = SProxy
:: forall shuffled
. RotatePath (Path F PNil) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
=> SProxy shuffled
1回だけですがシャッフルされました。これはfの方向に1度回しため、解き方としてはPath F' PNilが正しいです。結果を見てみましょう。
solve :: PProxy (Path F' PNil)
solve = PProxy
:: forall shuffled path
. RotatePath (Path F PNil) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
=> Solve shuffled path
=> PProxy path
正しく解き方を導出できています！
次はf方向に3回回した場合の解き方を導出させてみます。
solve :: PProxy (Path F PNil)
solve = PProxy
:: forall shuffled path
. RotatePath (Path F (Path F (Path F PNil))) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
=> Solve shuffled path
=> PProxy path
答えはPath F PNilとなりました。キューブは4回回すと元に戻ってくるので、同じ方向に3回回した場合はもう一度回せば戻ってきます。正しいです。
solve :: PProxy (Path F (Path F PNil))
solve = PProxy
:: forall shuffled path
. RotatePath (Path F (Path F PNil)) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
=> Solve shuffled path
=> PProxy path
次に、この方法の問題点が1つ発覚します。
-- 正しい
solve1 :: PProxy (Path F (Path F PNil))
solve1 = PProxy
:: forall shuffled path
. RotatePath (Path F (Path F PNil)) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
=> Solve shuffled path
=> PProxy path
-- 正しくない(エラー)
solve2 :: PProxy (Path F' (Path F' PNil))
solve2 = PProxy
:: forall shuffled path
. RotatePath (Path F (Path F PNil)) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
=> Solve shuffled path
=> PProxy path
この例では、f方向に2回、つまり前面を180度回転させたキューブを解かせています。fとf'のどちらに2回回しても解けるはずですが、関数の型定義にf'方向に2回回すPathを書いたsolve2ではエラーになってしまっています。
これは、型クラスEnqueueAllNotationでキューに入れる探索候補の順番と幅優先探索の方法によって起きてしまった問題です。候補が見つかり次第終了するこの方法では、それより後に見つかる別解を導出できません。
他の回転方法も追加する
ここまでは前面（fとf'）だけを考えてきましたが、他の回転も追加します。
まず、回転の型を追加します。
foreign import kind Notation
foreign import data F :: Notation
foreign import data F' :: Notation
foreign import data R :: Notation
foreign import data R' :: Notation
foreign import data B :: Notation
foreign import data B' :: Notation
foreign import data U :: Notation
foreign import data U' :: Notation
foreign import data L :: Notation
foreign import data L' :: Notation
foreign import data D :: Notation
foreign import data D' :: Notation
foreign import data X :: Notation
foreign import data X' :: Notation
foreign import data Y :: Notation
foreign import data Y' :: Notation
foreign import data Z :: Notation
foreign import data Z' :: Notation
次に、型クラスRotateのインスタンスを追加します。
class Rotate (notation :: Notation) (cube :: Symbol) (rotated :: Symbol) | notation cube -> rotated
instance rotateF ::
( ConsCube "DeCon" c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
, ConsCube "Con" c7 c2 c15 c4 c6 c14 c21 c8 c9 c10 c11 c3
c5 c13 c23 c16 c17 c18 c19 c1 c20 c22 c12 c24 rotated
) => Rotate F cube rotated
instance rotateF' ::
( RotatePath
(Path F (Path F (Path F PNil)))
cube rotated
) => Rotate F' cube rotated
instance rotateR ::
( RotatePath
(Path Y (Path F (Path Y' PNil)))
cube rotated
) => Rotate R cube rotated
instance rotateR' ::
( RotatePath
(Path R (Path R (Path R PNil)))
cube rotated
) => Rotate R' cube rotated
instance rotateB ::
( RotatePath
(Path Y (Path Y (Path F (Path Y (Path Y PNil)))))
cube rotated
) => Rotate B cube rotated
instance rotateB' ::
( RotatePath
(Path B (Path B (Path B PNil)))
cube rotated
) => Rotate B' cube rotated
instance rotateU ::
( RotatePath
(Path X' (Path F (Path X PNil)))
cube rotated
) => Rotate U cube rotated
instance rotateU' ::
( RotatePath
(Path U (Path U (Path U PNil)))
cube rotated
) => Rotate U' cube rotated
instance rotateL ::
( RotatePath
(Path Y' (Path F (Path Y PNil)))
cube rotated
) => Rotate L cube rotated
instance rotateL' ::
( RotatePath
(Path L (Path L (Path L PNil)))
cube rotated
) => Rotate L' cube rotated
instance rotateD ::
( RotatePath
(Path X (Path F (Path X' PNil)))
cube rotated
) => Rotate D cube rotated
instance rotateD' ::
( RotatePath
(Path D (Path D (Path D PNil)))
cube rotated
) => Rotate D' cube rotated
instance rotateX ::
( ConsCube "DeCon" c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
, ConsCube "Con" c3 c1 c4 c2 c7 c8 c9 c10 c11 c12 c5 c6
c15 c16 c17 c18 c19 c20 c13 c14 c22 c24 c21 c23 rotated
) => Rotate X cube rotated
instance rotateX' ::
( RotatePath
(Path X (Path X (Path X PNil)))
cube rotated
) => Rotate X' cube rotated
instance rotateY ::
( RotatePath
(Path U (Path D' PNil))
cube rotated
) => Rotate Y cube rotated
instance rotateY' ::
( RotatePath
(Path Y (Path Y (Path Y PNil)))
cube rotated
) => Rotate Y' cube rotated
instance rotateZ ::
( RotatePath
(Path F (Path B' PNil))
cube rotated
) => Rotate Z cube rotated
instance rotateZ' ::
( RotatePath
(Path Z (Path Z (Path Z PNil)))
cube rotated
) => Rotate Z' cube rotated
次に、全探索候補を追加する型クラスEnqueueAllNotationにも回転方法を追加します。
class EnqueueAllNotation (queue :: Queue) (currPath :: Path) (queue' :: Queue) | queue -> queue'
instance enqueueAllPath ::
( TypeEquals (QProxy queue) (QProxy q')
, AppendPath currPath (Path F PNil) pF
, Enqueue q' pF qF
, AppendPath currPath (Path F' PNil) pF'
, Enqueue qF pF' qF'
, AppendPath currPath (Path R PNil) pR
, Enqueue qF' pR qR
, AppendPath currPath (Path R' PNil) pR'
, Enqueue qR pR' qR'
, AppendPath currPath (Path B PNil) pB
, Enqueue qR' pB qB
, AppendPath currPath (Path B' PNil) pB'
, Enqueue qB pB' qB'
, AppendPath currPath (Path U PNil) pU
, Enqueue qB' pU qU
, AppendPath currPath (Path U' PNil) pU'
, Enqueue qU pU' qU'
, AppendPath currPath (Path L PNil) pL
, Enqueue qU' pL qL
, AppendPath currPath (Path L' PNil) pL'
, Enqueue qL pL' qL'
, AppendPath currPath (Path D PNil) pD
, Enqueue qL' pD qD
, AppendPath currPath (Path D' PNil) pD'
, Enqueue qD pD' qD'
, AppendPath currPath (Path X PNil) pX
, Enqueue qD' pX qX
, AppendPath currPath (Path X' PNil) pX'
, Enqueue qX pX' qX'
, AppendPath currPath (Path Y PNil) pY
, Enqueue qX' pY qY
, AppendPath currPath (Path Y' PNil) pY'
, Enqueue qY pY' qY'
, AppendPath currPath (Path Z PNil) pZ
, Enqueue qY' pZ qZ
, AppendPath currPath (Path Z' PNil) pZ'
, Enqueue qZ pZ' qZ'
, TypeEquals (QProxy qZ') (QProxy queue')
) => EnqueueAllNotation queue currPath queue'
ここまでのまとめ
ここまでのソースコード（クリックで開きます）
module Main where
import Prelude
import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
import Effect.Console (log)
import Prim.Symbol (class Append, class Cons)
import Type.Data.Boolean (class If)
import Type.Data.Symbol (class Equals)
import Type.Equality (class TypeEquals)
showCube
:: forall c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
. ConsCube "DeCon"
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
=> IsSymbol c1 => IsSymbol c2 => IsSymbol c3 => IsSymbol c4 => IsSymbol c5 => IsSymbol c6
=> IsSymbol c7 => IsSymbol c8 => IsSymbol c9 => IsSymbol c10 => IsSymbol c11 => IsSymbol c12
=> IsSymbol c13 => IsSymbol c14 => IsSymbol c15 => IsSymbol c16 => IsSymbol c17 => IsSymbol c18
=> IsSymbol c19 => IsSymbol c20 => IsSymbol c21 => IsSymbol c22 => IsSymbol c23 => IsSymbol c24
=> SProxy cube -> String
showCube _ =
" " <> " " <> c1 <> c2
<> nl <> " " <> " " <> c3 <> c4
<> nl <> c5 <> c6 <> c7 <> c8 <> c9 <> c10 <> c11 <> c12
<> nl <> c13 <> c14 <> c15 <> c16 <> c17 <> c18 <> c19 <> c20
<> nl <> " " <> " " <> c21 <> c22
<> nl <> " " <> " " <> c23 <> c24
where
nl = "\n"
c1 = reflectSymbol (SProxy :: SProxy c1 )
c2 = reflectSymbol (SProxy :: SProxy c2 )
c3 = reflectSymbol (SProxy :: SProxy c3 )
c4 = reflectSymbol (SProxy :: SProxy c4 )
c5 = reflectSymbol (SProxy :: SProxy c5 )
c6 = reflectSymbol (SProxy :: SProxy c6 )
c7 = reflectSymbol (SProxy :: SProxy c7 )
c8 = reflectSymbol (SProxy :: SProxy c8 )
c9 = reflectSymbol (SProxy :: SProxy c9 )
c10 = reflectSymbol (SProxy :: SProxy c10)
c11 = reflectSymbol (SProxy :: SProxy c11)
c12 = reflectSymbol (SProxy :: SProxy c12)
c13 = reflectSymbol (SProxy :: SProxy c13)
c14 = reflectSymbol (SProxy :: SProxy c14)
c15 = reflectSymbol (SProxy :: SProxy c15)
c16 = reflectSymbol (SProxy :: SProxy c16)
c17 = reflectSymbol (SProxy :: SProxy c17)
c18 = reflectSymbol (SProxy :: SProxy c18)
c19 = reflectSymbol (SProxy :: SProxy c19)
c20 = reflectSymbol (SProxy :: SProxy c20)
c21 = reflectSymbol (SProxy :: SProxy c21)
c22 = reflectSymbol (SProxy :: SProxy c22)
c23 = reflectSymbol (SProxy :: SProxy c23)
c24 = reflectSymbol (SProxy :: SProxy c24)
foreign import kind Notation
foreign import data F :: Notation
foreign import data F' :: Notation
foreign import data R :: Notation
foreign import data R' :: Notation
foreign import data B :: Notation
foreign import data B' :: Notation
foreign import data U :: Notation
foreign import data U' :: Notation
foreign import data L :: Notation
foreign import data L' :: Notation
foreign import data D :: Notation
foreign import data D' :: Notation
foreign import data X :: Notation
foreign import data X' :: Notation
foreign import data Y :: Notation
foreign import data Y' :: Notation
foreign import data Z :: Notation
foreign import data Z' :: Notation
foreign import kind Path
foreign import data Path :: Notation -> Path -> Path
foreign import data PNil :: Path
data PProxy (p :: Path) = PProxy
class AppendPath (pl :: Path) (pr :: Path) (plr :: Path) | pl pr -> plr
instance appendPathNil :: AppendPath PNil pr pr
instance appendPath ::
( AppendPath tail pr plr'
, TypeEquals (PProxy (Path head plr')) (PProxy plr)
) => AppendPath (Path head tail) pr plr
class HeadPath (p :: Path) (head :: Notation) (tail :: Path) | p -> head tail
instance headPath :: HeadPath (Path head tail) head tail
foreign import kind Queue
foreign import data Queue :: Path -> Queue -> Queue
foreign import data QNil :: Queue
data QProxy (q :: Queue) = QProxy
class Enqueue (queue :: Queue) (path :: Path) (queue' :: Queue) | queue path -> queue'
instance enqueueNil :: Enqueue QNil path (Queue path QNil)
instance enqueue ::
( Enqueue tail newPath q'
, TypeEquals (QProxy (Queue path q')) (QProxy queue')
) => Enqueue (Queue path tail) newPath queue'
class Dequeue (queue :: Queue) (path :: Path) (queue' :: Queue) | queue -> path queue'
instance dequeueNil :: Dequeue (Queue path tail) path tail
instance dequeue :: Dequeue QNil PNil QNil
class EnqueueAllNotation (queue :: Queue) (currPath :: Path) (queue' :: Queue) | queue -> queue'
instance enqueueAllPath ::
( TypeEquals (QProxy queue) (QProxy q')
, AppendPath currPath (Path F PNil) pF
, Enqueue q' pF qF
, AppendPath currPath (Path F' PNil) pF'
, Enqueue qF pF' qF'
, AppendPath currPath (Path R PNil) pR
, Enqueue qF' pR qR
, AppendPath currPath (Path R' PNil) pR'
, Enqueue qR pR' qR'
, AppendPath currPath (Path B PNil) pB
, Enqueue qR' pB qB
, AppendPath currPath (Path B' PNil) pB'
, Enqueue qB pB' qB'
, AppendPath currPath (Path U PNil) pU
, Enqueue qB' pU qU
, AppendPath currPath (Path U' PNil) pU'
, Enqueue qU pU' qU'
, AppendPath currPath (Path L PNil) pL
, Enqueue qU' pL qL
, AppendPath currPath (Path L' PNil) pL'
, Enqueue qL pL' qL'
, AppendPath currPath (Path D PNil) pD
, Enqueue qL' pD qD
, AppendPath currPath (Path D' PNil) pD'
, Enqueue qD pD' qD'
, AppendPath currPath (Path X PNil) pX
, Enqueue qD' pX qX
, AppendPath currPath (Path X' PNil) pX'
, Enqueue qX pX' qX'
, AppendPath currPath (Path Y PNil) pY
, Enqueue qX' pY qY
, AppendPath currPath (Path Y' PNil) pY'
, Enqueue qY pY' qY'
, AppendPath currPath (Path Z PNil) pZ
, Enqueue qY' pZ qZ
, AppendPath currPath (Path Z' PNil) pZ'
, Enqueue qZ pZ' qZ'
, TypeEquals (QProxy qZ') (QProxy queue')
) => EnqueueAllNotation queue currPath queue'
class Solve (cube :: Symbol) (path :: Path) | cube -> path
instance initSolve ::
(SolveImpl cube "RRRRWWBBYYGGWWBBYYGGOOOO" prev QNil PNil path) => Solve cube path
class SolveImpl
(cube :: Symbol)
(goal :: Symbol)
(prevCube :: Symbol)
(queue :: Queue)
(currPath :: Path)
(path :: Path)
| cube goal -> path
instance solved :: SolveImpl goal goal prev queue currPath PNil
else instance solved' :: SolveImpl cube goal goal queue currPath path
else instance solveImpl ::
( EnqueueAllNotation queue currPath q
, Dequeue q pHead qTail
, RotatePath pHead cube rotated
, Equals rotated goal isEq
, If isEq (PProxy pHead) (PProxy path) (PProxy path)
, SolveImpl cube goal rotated qTail pHead path
) => SolveImpl cube goal prev queue currPath path
class RotatePath (path :: Path) (cube :: Symbol) (rotated :: Symbol) | cube path -> rotated
instance rotatedPathNil :: RotatePath PNil cube cube
instance rotatedPath ::
( Rotate notation cube cube'
, RotatePath tail cube' cube''
, TypeEquals (SProxy cube'') (SProxy rotated)
) => RotatePath (Path notation tail) cube rotated
class ConsCube
(mode :: Symbol)
(c1 :: Symbol) (c2 :: Symbol) (c3 :: Symbol) (c4 :: Symbol)
(c5 :: Symbol) (c6 :: Symbol) (c7 :: Symbol) (c8 :: Symbol)
(c9 :: Symbol) (c10 :: Symbol) (c11 :: Symbol) (c12 :: Symbol)
(c13 :: Symbol) (c14 :: Symbol) (c15 :: Symbol) (c16 :: Symbol)
(c17 :: Symbol) (c18 :: Symbol) (c19 :: Symbol) (c20 :: Symbol)
(c21 :: Symbol) (c22 :: Symbol) (c23 :: Symbol) (c24 :: Symbol) (cube :: Symbol)
| mode
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24
-> cube
, mode
cube ->
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24
instance deConsCube ::
( Cons c1 t1 cube, Cons c2 t2 t1 , Cons c3 t3 t2 , Cons c4 t4 t3
, Cons c5 t5 t4 , Cons c6 t6 t5 , Cons c7 t7 t6 , Cons c8 t8 t7
, Cons c9 t9 t8 , Cons c10 t10 t9 , Cons c11 t11 t10, Cons c12 t12 t11
, Cons c13 t13 t12 , Cons c14 t14 t13, Cons c15 t15 t14, Cons c16 t16 t15
, Cons c17 t17 t16 , Cons c18 t18 t17, Cons c19 t19 t18, Cons c20 t20 t19
, Cons c21 t21 t20 , Cons c22 t22 t21, Cons c23 t23 t22, Cons c24 "" t23
) => ConsCube "DeCon"
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
else instance consCube ::
( Cons c1 "" t1 , Cons t1 c2 t2 , Append t2 c3 t3 , Append t3 c4 t4
, Append t4 c5 t5 , Append t5 c6 t6 , Append t6 c7 t7 , Append t7 c8 t8
, Append t8 c9 t9 , Append t9 c10 t10, Append t10 c11 t11, Append t11 c12 t12
, Append t12 c13 t13, Append t13 c14 t14, Append t14 c15 t15, Append t15 c16 t16
, Append t16 c17 t17, Append t17 c18 t18, Append t18 c19 t19, Append t19 c20 t20
, Append t20 c21 t21, Append t21 c22 t22, Append t22 c23 t23, Append t23 c24 cube
) => ConsCube "Con"
c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
class Rotate (notation :: Notation) (cube :: Symbol) (rotated :: Symbol) | notation cube -> rotated
instance rotateF ::
( ConsCube "DeCon" c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
, ConsCube "Con" c7 c2 c15 c4 c6 c14 c21 c8 c9 c10 c11 c3
c5 c13 c23 c16 c17 c18 c19 c1 c20 c22 c12 c24 rotated
) => Rotate F cube rotated
instance rotateF' ::
( RotatePath
(Path F (Path F (Path F PNil)))
cube rotated
) => Rotate F' cube rotated
instance rotateR ::
( RotatePath
(Path Y (Path F (Path Y' PNil)))
cube rotated
) => Rotate R cube rotated
instance rotateR' ::
( RotatePath
(Path R (Path R (Path R PNil)))
cube rotated
) => Rotate R' cube rotated
instance rotateB ::
( RotatePath
(Path Y (Path Y (Path F (Path Y (Path Y PNil)))))
cube rotated
) => Rotate B cube rotated
instance rotateB' ::
( RotatePath
(Path B (Path B (Path B PNil)))
cube rotated
) => Rotate B' cube rotated
instance rotateU ::
( RotatePath
(Path X' (Path F (Path X PNil)))
cube rotated
) => Rotate U cube rotated
instance rotateU' ::
( RotatePath
(Path U (Path U (Path U PNil)))
cube rotated
) => Rotate U' cube rotated
instance rotateL ::
( RotatePath
(Path Y' (Path F (Path Y PNil)))
cube rotated
) => Rotate L cube rotated
instance rotateL' ::
( RotatePath
(Path L (Path L (Path L PNil)))
cube rotated
) => Rotate L' cube rotated
instance rotateD ::
( RotatePath
(Path X (Path F (Path X' PNil)))
cube rotated
) => Rotate D cube rotated
instance rotateD' ::
( RotatePath
(Path D (Path D (Path D PNil)))
cube rotated
) => Rotate D' cube rotated
instance rotateX ::
( ConsCube "DeCon" c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12
c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
, ConsCube "Con" c3 c1 c4 c2 c7 c8 c9 c10 c11 c12 c5 c6
c15 c16 c17 c18 c19 c20 c13 c14 c22 c24 c21 c23 rotated
) => Rotate X cube rotated
instance rotateX' ::
( RotatePath
(Path X (Path X (Path X PNil)))
cube rotated
) => Rotate X' cube rotated
instance rotateY ::
( RotatePath
(Path U (Path D' PNil))
cube rotated
) => Rotate Y cube rotated
instance rotateY' ::
( RotatePath
(Path Y (Path Y (Path Y PNil)))
cube rotated
) => Rotate Y' cube rotated
instance rotateZ ::
( RotatePath
(Path F (Path B' PNil))
cube rotated
) => Rotate Z cube rotated
instance rotateZ' ::
( RotatePath
(Path Z (Path Z (Path Z PNil)))
cube rotated
) => Rotate Z' cube rotated
回転方法をすべて定義したので、これでどんなにシャッフルされたキューブが来ても解けるはずです。