Commit 72562138 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Add a third test variant to Trac #9872

parent d45edfb3
- Instant Insanity using Closed Type Families, but no DataKinds
- See:
{-# OPTIONS_GHC -ftype-function-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))
(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)))
(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)
No instance for (Show
(Cube G B W R B G)
(Cube W G B W R R)
(Cons (Cube R W R B G R) (Cons (Cube B R G G W W) Nil))))
(Cube G B R W B G)
(Cube R R W B G W)
(Cons (Cube R G B R W R) (Cons (Cube W W G G R B) Nil))))
(Cube G W R B B G)
(Cube W B W R G R)
(Cons (Cube R R B G W R) (Cons (Cube B G G W R W) Nil))))
(Cube G R W B B G)
(Cube R W B G R W)
(Cube R B R W G R) (Cons (Cube W G G R W B) Nil))))
(Cube G R B B W G)
(Cube W W R G B R)
(Cube R B G W R R)
(Cons (Cube B G W R G W) Nil))))
(Cube G W B B R G)
(Cube R B G R W W)
(Cube R R W G B R)
(Cons (Cube W G R W G B) Nil))))
(Cube G B B W R G)
(Cube W R G B W R)
(Cube R G W R B R)
(Cons (Cube B W R G G W) Nil))))
(Cube G B B R W G)
(Cube R G R W B W)
(Cube R W G B R R)
(Cons (Cube W R W G G B) Nil))))
arising from a use of ‘print’
In the expression: print (Proxy :: Proxy (Solutions Cubes))
In an equation for ‘main’:
main = print (Proxy :: Proxy (Solutions Cubes))
......@@ -565,3 +565,12 @@ test('T9872b',
[ only_ways(['normal']),
compiler_stats_num_field('bytes allocated',
[(wordsize(64), 5495850096, 5)
# 2014-12-10 5495850096 Initally created
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment