Last active
June 18, 2018 07:38
-
-
Save i-am-tom/2b8cba142f26bdb1959491a9f9b0bba1 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE TypeFamilies #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| {-# LANGUAGE UndecidableInstances #-} | |
| module YassQueen where | |
| data Nil | |
| data Cons x xs | |
| type family First xs where | |
| First (Cons x xs) = x | |
| First Nil = Nil | |
| type family xs <> ys where | |
| Nil <> ys = ys | |
| Cons x xs <> ys = Cons x (xs <> ys) | |
| type family Join xs where | |
| Join Nil = Nil | |
| Join (Cons xs xss) = xs <> Join xss | |
| data True | |
| data False | |
| type family Any xs where | |
| Any Nil = False | |
| Any (Cons True xs) = True | |
| Any (Cons x xs) = Any xs | |
| type family Not x where | |
| Not True = False | |
| Not False = True | |
| type family x || y where | |
| True || y = True | |
| False || y = y | |
| data Z | |
| data S n | |
| type N0 = Z | |
| type N1 = S N0 | |
| type N2 = S N1 | |
| type N3 = S N2 | |
| type N4 = S N3 | |
| type N5 = S N4 | |
| type N6 = S N5 | |
| type N7 = S N6 | |
| type N8 = S N7 | |
| type family x == y where | |
| Z == Z = True | |
| S x == S y = x == y | |
| _ == _ = False | |
| type family x < y where | |
| Z < S y = True | |
| S x < S y = x < y | |
| _ < _ = False | |
| type family Diff x y where | |
| Diff (S x) (S y) = Diff x y | |
| Diff Z Z = Z | |
| Diff Z y = y | |
| Diff x Z = x | |
| type family Range n where | |
| Range Z = Nil | |
| Range (S x) = Cons (S x) (Range x) | |
| data AddQueen2 n x | |
| data Conj1 xs | |
| data Queen1 x | |
| data Safe1 x | |
| data Threatens1 x | |
| type family Apply f x where | |
| Apply (Conj1 xs) x = Cons x xs | |
| Apply (Queen1 x) y = Queen x y | |
| Apply (Safe1 x) y = Safe x y | |
| Apply (Threatens1 x) y = Threatens x y | |
| Apply (AddQueen2 n x) c = AddQueen n x c | |
| type family Map f xs where | |
| Map f Nil = Nil | |
| Map f (Cons x xs) = Cons (Apply f x) (Map f xs) | |
| type family FlatMap f xs where | |
| FlatMap f xs = Join (Map f xs) | |
| type family AppendIf p x xs where | |
| AppendIf True x xs = Cons x xs | |
| AppendIf False x xs = xs | |
| type family Filter f xs where | |
| Filter f Nil = Nil | |
| Filter f (Cons x xs) = AppendIf (Apply f x) x (Filter f xs) | |
| data Queen x y | |
| type family QueensInRow n x where | |
| QueensInRow n x = Map (Queen1 x) (Range n) | |
| type family Threatens a b where | |
| Threatens (Queen ax ay) (Queen bx by) | |
| = ((ax == bx) || (ay == by)) || (Diff ax bx == Diff ay by) | |
| type family Safe config queen where | |
| Safe config queen = Not (Any (Map (Threatens1 queen) config)) | |
| type family AddQueen n x c where | |
| AddQueen n x c = Map (Conj1 c) (Filter (Safe1 c) (QueensInRow n x)) | |
| type family AddQueenToAll n x cs where | |
| AddQueenToAll n x cs = FlatMap (AddQueen2 n x) cs | |
| type family AddQueensIf p n x cs where | |
| AddQueensIf False n x cs = cs | |
| AddQueensIf True n x cs = AddQueens n (S x) (AddQueenToAll n x cs) | |
| type family AddQueens n x cs where | |
| AddQueens n x cs = AddQueensIf (x < n) n x cs | |
| type family Solve n where | |
| Solve n = First (AddQueens n Z (Cons Nil Nil)) | |
| -- > :kind! Solve N6 | |
| -- Solve N6 :: * | |
| -- = Cons | |
| -- (Queen (S (S (S (S (S Z))))) (S (S N0))) | |
| -- (Cons | |
| -- (Queen (S (S (S (S Z)))) (S (S N2))) | |
| -- (Cons | |
| -- (Queen (S (S (S Z))) (S (S N4))) | |
| -- (Cons | |
| -- (Queen (S (S Z)) (S Z)) | |
| -- (Cons (Queen (S Z) (S (S N1))) (Cons (Queen Z (S (S N3))) Nil))))) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment