Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- object InstantInsanity extends App {
- // scalastyle:off
- def undefined[T]: T = ???
- def ⊥[T]: T = undefined
- trait R
- trait G
- trait B
- trait W
- trait Cube[u, f, b, r, l, d]
- 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]
- trait Transform[u, f, r, b, l, d] {
- def rot: Cube[u, f, r, b, l, d] => Cube[u, r, b, l, f, d]
- def twist: Cube[u, f, r, b, l, d] => Cube[f, r, u, l, d, b]
- def flip: Cube[u, f, r, b, l, d] => Cube[d, l, b, r, f, u]
- }
- implicit def transform[u, f, r, b, l, d] = new Transform[u, f, r, b, l, d] {
- def rot: (Cube[u, f, r, b, l, d]) => Cube[u, r, b, l, f, d] = ⊥
- def twist: (Cube[u, f, r, b, l, d]) => Cube[f, r, u, l, d, b] = ⊥
- def flip: (Cube[u, f, r, b, l, d]) => Cube[d, l, b, r, f, u] = ⊥
- }
- def rot[u, f, r, b, l, d](cube: Cube[u, f, r, b, l, d])(implicit t: Transform[u, f, r, b, l, d]) = t.rot(cube)
- def twist[u, f, r, b, l, d](cube: Cube[u, f, r, b, l, d])(implicit t: Transform[u, f, r, b, l, d]) = t.twist(cube)
- def flip[u, f, r, b, l, d](cube: Cube[u, f, r, b, l, d])(implicit t: Transform[u, f, r, b, l, d]) = t.flip(cube)
- // :type rot(⊥[Cube1])
- // :type twist(flip(rot(⊥[Cube1])))
- trait True
- trait False
- trait And[l, r, o]
- implicit object ttt extends And[True, True, True]
- implicit object tff extends And[True, False, False]
- implicit object ftf extends And[False, True, False]
- implicit object fff extends And[False, False, False]
- def and[l, r, o](l: l, r: r)(implicit and: And[l, r, o]): o = ⊥
- // :type and(⊥[True], ⊥[False])
- trait Nil
- trait :::[x, xs]
- trait ListConcat[l1, l2, l]
- implicit def nilConcat[l]: ListConcat[Nil, l, l] = ⊥
- implicit def notNilConcat[x, xs, ys, zs](implicit
- lc: ListConcat[xs, ys, zs]
- ): ListConcat[x ::: xs, ys, x ::: zs] = ⊥
- def listConcat[xs, ys, zs](l1: xs, l2: ys)(implicit
- lc: ListConcat[xs, ys, zs]
- ): zs = ⊥
- // :type listConcat(⊥[R ::: Nil], ⊥[G ::: W ::: Nil])
- trait Rotation
- trait Twist
- trait Flip
- trait Apply[f, a, b]
- implicit def apRotation[u, f, r, b, l, d]: Apply[Rotation, Cube[u, f, r, b, l, d], Cube[u, r, b, l, f, d]] = ⊥
- implicit def apTwist[u, f, r, b, l, d]: Apply[Twist, Cube[u, f, r, b, l, d], Cube[f, r, u, l, d, b]] = ⊥
- implicit def apFlip[u, f, r, b, l, d]: Apply[Flip, Cube[u, f, r, b, l, d], Cube[d, l, b, r, f, u]] = ⊥
- def ap[t, u, f, r, b, l, d, o](r: t, c1: Cube[u, f, r, b, l, d])(implicit
- ap: Apply[t, Cube[u, f, r, b, l, d], o]
- ): o = ⊥
- // :type ap(⊥[Rotation], ⊥[Cube1])
- trait Map[f, xs, zs]
- implicit def mapNil[f]: Map[f, Nil, Nil] = ⊥
- implicit def mapCons[f, x, z, xs, zs](implicit
- ap: Apply[f, x, z],
- map: Map[f, xs, zs]
- ): Map[f, x ::: xs, z ::: zs] = ⊥
- def map[f, xs, zs](f: f, xs: xs)(implicit
- map: Map[f, xs, zs]
- ): zs = ⊥
- // :type map(⊥[Flip], ⊥[Cube1 ::: Cube2 ::: Nil])
- trait AppendIf[b, x, ys, zs]
- implicit def appendIfTrue[x, ys]: AppendIf[True, x, ys, x ::: ys] = ⊥
- implicit def appendIfFalse[x, ys]: AppendIf[False, x, ys, ys] = ⊥
- def append[b, x, ys, zs](b: b, x: x, ys: ys)(implicit
- apn: AppendIf[b, x, ys, zs]
- ): zs = ⊥
- // :type append(⊥[True], ⊥[R], ⊥[G ::: W ::: Nil])
- // :type append(⊥[False], ⊥[R], ⊥[G ::: W ::: Nil])
- trait Filter[f, xs, zs]
- implicit def filterNil[f]: Filter[f, Nil, Nil] = ⊥
- implicit def filterCons[f, x, b, xs, ys, zs](implicit
- ap: Apply[f, x, b],
- f: Filter[f, xs, ys],
- apn: AppendIf[b, x, ys, zs]
- ): Filter[f, x ::: xs, zs] = ⊥
- //
- trait MapAppend[f, xs, zs]
- implicit def mapAppendNil[f]: MapAppend[f, Nil, Nil] = ⊥
- implicit def mapAppendCons[f, xs, ys, zs](implicit
- m: Map[f, xs, ys],
- lc: ListConcat[xs, ys, zs]
- ): MapAppend[f, xs, zs] = ⊥
- trait MapAppend2[f, xs, zs]
- implicit def mapAppend2Nil[f]: MapAppend2[f, Nil, Nil] = ⊥
- implicit def mapAppend2Cons[f, xs, ys, _ys, zs](implicit
- m: Map[f, xs, ys],
- ma: MapAppend[f, ys, _ys],
- lc: ListConcat[xs, _ys, zs]
- ): MapAppend2[f, xs, zs] = ⊥
- trait MapAppend3[f, xs, zs]
- implicit def mapAppend3Nil[f]: MapAppend3[f, Nil, Nil] = ⊥
- implicit def mapAppend3Cons[f, xs, ys, _ys, zs](implicit
- m: Map[f, xs, ys],
- ma2: MapAppend2[f, ys, _ys],
- lc: ListConcat[xs, _ys, zs]
- ): MapAppend3[f, xs, zs] = ⊥
- trait Orientations
- implicit def orientations[c, fs, ts, zs](implicit
- ma: MapAppend[Flip, c ::: Nil, fs],
- ma2: MapAppend2[Twist, fs, ts],
- ma3: MapAppend3[Rotation, ts, zs]
- ): Apply[Orientations, c, zs] = ⊥
- // :type ap(⊥[Orientations], ⊥[Cube1])
- trait NE[x, y, b]
- implicit object neRR extends NE[R, R, False]
- implicit object neRG extends NE[R, G, True]
- implicit object neRB extends NE[R, B, True]
- implicit object neRW extends NE[R, W, True]
- implicit object neGR extends NE[G, R, True]
- implicit object neGG extends NE[G, G, False]
- implicit object neGB extends NE[G, B, True]
- implicit object neGW extends NE[G, W, True]
- implicit object neBR extends NE[B, R, True]
- implicit object neBG extends NE[B, G, True]
- implicit object neBB extends NE[B, B, False]
- implicit object neBW extends NE[B, W, True]
- implicit object neWR extends NE[W, R, True]
- implicit object neWG extends NE[W, G, True]
- implicit object neWB extends NE[W, B, True]
- implicit object neWW extends NE[W, W, False]
- trait All[l, b]
- implicit def allNil: All[Nil, True]
- = ⊥
- implicit def allFalse[xs]: All[False ::: xs, False] = ⊥
- implicit def allTrue[b, xs](implicit all: All[xs, b]): All[True ::: xs, b] = ⊥
- def all[b, xs](l: xs)(implicit all: All[xs, b]): b = ⊥
- // :type all(⊥[Nil])
- // :type all(⊥[False ::: Nil])
- // :type all(⊥[True ::: False ::: Nil])
- // :type all(⊥[True ::: True ::: Nil])
- trait Compatible[c1, c2, b]
- implicit def compatibleInstance[f1, f2, bF, r1, r2, bR, b1, b2, bB, l1, l2, bL, u1, u2, d1, d2, b](implicit
- ne1: NE[f1, f2, bF],
- ne2: NE[r1, r2, bR],
- ne3: NE[b1, b2, bB],
- ne4: NE[l1, l2, bL],
- all: All[bF ::: bR ::: bB ::: bL ::: Nil, b]
- ): Compatible[Cube[u1, f1, r1, b1, l1, d1], Cube[u2, f2, r2, b2, l2, d2], b] = ⊥
- def compatible[c1, c2, b](c1: c1, c2: c2)(implicit
- c: Compatible[c1, c2, b]
- ): b = ⊥
- // :type compatible(⊥[Cube[R, R, R, R, R, R]], ⊥[Cube[B, B, B, B, B, B]])
- // :type compatible(⊥[Cube[R, R, G, R, R, R]], ⊥[Cube[B, B, G, B, B, B]])
- trait Allowed[c, cs, b]
- implicit def allowedNil[c]: Allowed[c, Nil, True] = ⊥
- implicit def allowedCons[c, y, b1, ys, b2, b](implicit
- c: Compatible[c, y, b1],
- allowed: Allowed[c, ys, b2],
- and: And[b1, b2, b]
- ): Allowed[c, y ::: ys, b] = ⊥
- def allowed[c, cs, b](c: c, cs: cs)(implicit a: Allowed[c, cs, b]): b = ⊥
- type CubeRed = Cube[R, R, R, R, R, R]
- type CubeBlue = Cube[B, B, B, B, B, B]
- // :type allowed(⊥[CubeRed], ⊥[CubeBlue ::: CubeRed ::: Nil])
- trait MatchingOrientations[os, sols, zs]
- implicit def matchingOrientationsNil[sol]: MatchingOrientations[Nil, sol, Nil] = ⊥
- implicit def matchingOrientationsCons[os, sol, as, o, b, zs](implicit
- mo: MatchingOrientations[os, sol, as],
- a: Allowed[o, sol, b],
- apn: AppendIf[b, o ::: sol, as, zs]
- ): MatchingOrientations[o ::: os, sol, zs] = ⊥
- trait AllowedCombinations[os, sols, zs]
- implicit def allowedCombinationsNil[os]: AllowedCombinations[os, Nil, Nil] = ⊥
- implicit def allowedCombinationsCons[os, sols, as, s, bs, zs](implicit
- ac: AllowedCombinations[os, sols, as],
- mo: MatchingOrientations[os, s, bs],
- lc: ListConcat[as, bs, zs]
- ): AllowedCombinations[os, s ::: sols, zs] = ⊥
- class Solutions[cs, ss]
- implicit def solutionsNil: Solutions[Nil, Nil ::: Nil] = ⊥
- implicit def solutionsCons[cs, sols, c, os, zs](implicit
- s: Solutions[cs, sols],
- ap: Apply[Orientations, c, os],
- ac: AllowedCombinations[os, sols, zs]
- ): Solutions[c ::: cs, zs] = ⊥
- type Cubes = (Cube1 ::: Cube2 ::: Cube3 ::: Cube4 ::: Nil)
- def solutions[cs, ss](cs: cs)(implicit sol: Solutions[cs, ss]): ss = ⊥
- // :type solutions(⊥[Cubes])
- }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement