{-# LANGUAGE Rank2Types #-}
module Combinatorics.Battleship.Size where


data Zero = Zero
data Succ n = Succ n

type N0  = Zero
type N1  = Succ N0  ; type P1 w  = Succ w
type N2  = Succ N1  ; type P2 w  = Succ (P1  w)
type N3  = Succ N2  ; type P3 w  = Succ (P2  w)
type N4  = Succ N3  ; type P4 w  = Succ (P3  w)
type N5  = Succ N4  ; type P5 w  = Succ (P4  w)
type N6  = Succ N5  ; type P6 w  = Succ (P5  w)
type N7  = Succ N6  ; type P7 w  = Succ (P6  w)
type N8  = Succ N7  ; type P8 w  = Succ (P7  w)
type N9  = Succ N8  ; type P9 w  = Succ (P8  w)
type N10 = Succ N9  ; type P10 w = Succ (P9  w)
type N11 = Succ N10 ; type P11 w = Succ (P10 w)
type N12 = Succ N11 ; type P12 w = Succ (P11 w)

n0 :: Size N0; n0 :: Size N0
n0 = Size N0
forall n. Nat n => Size n
size
n1 :: Size N1; n1 :: Size N1
n1 = Size N1
forall n. Nat n => Size n
size
n2 :: Size N2; n2 :: Size N2
n2 = Size N2
forall n. Nat n => Size n
size
n3 :: Size N3; n3 :: Size N3
n3 = Size N3
forall n. Nat n => Size n
size
n4 :: Size N4; n4 :: Size N4
n4 = Size N4
forall n. Nat n => Size n
size
n5 :: Size N5; n5 :: Size N5
n5 = Size N5
forall n. Nat n => Size n
size
n6 :: Size N6; n6 :: Size N6
n6 = Size N6
forall n. Nat n => Size n
size
n7 :: Size N7; n7 :: Size N7
n7 = Size N7
forall n. Nat n => Size n
size
n8 :: Size N8; n8 :: Size N8
n8 = Size N8
forall n. Nat n => Size n
size
n9 :: Size N9; n9 :: Size N9
n9 = Size N9
forall n. Nat n => Size n
size
n10 :: Size N10; n10 :: Size N10
n10 = Size N10
forall n. Nat n => Size n
size


newtype Size n = Size {Size n -> Int
getSize :: Int}

incSize :: Size n -> Size (Succ n)
incSize :: Size n -> Size (Succ n)
incSize (Size Int
n) = Int -> Size (Succ n)
forall n. Int -> Size n
Size (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

class Nat n where switch :: f Zero -> (forall m. Nat m => f (Succ m)) -> f n
instance Nat Zero where switch :: f N0 -> (forall m. Nat m => f (Succ m)) -> f N0
switch f N0
f forall m. Nat m => f (Succ m)
_ = f N0
f
instance Nat n => Nat (Succ n) where switch :: f N0 -> (forall m. Nat m => f (Succ m)) -> f (Succ n)
switch f N0
_ forall m. Nat m => f (Succ m)
f = f (Succ n)
forall m. Nat m => f (Succ m)
f

size :: Nat n => Size n
size :: Size n
size = Size N0 -> (forall m. Nat m => Size (Succ m)) -> Size n
forall n (f :: * -> *).
Nat n =>
f N0 -> (forall m. Nat m => f (Succ m)) -> f n
switch (Int -> Size N0
forall n. Int -> Size n
Size Int
0) (Size m -> Size (Succ m)
forall n. Size n -> Size (Succ n)
incSize Size m
forall n. Nat n => Size n
size)


reifyInt :: Int -> (forall n. Nat n => Size n -> a) -> a
reifyInt :: Int -> (forall n. Nat n => Size n -> a) -> a
reifyInt Int
n forall n. Nat n => Size n -> a
f =
   if Int
nInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0
     then Size N0 -> a
forall n. Nat n => Size n -> a
f Size N0
n0
     else Int -> (forall n. Nat n => Size n -> a) -> a
forall a. Int -> (forall n. Nat n => Size n -> a) -> a
reifyInt (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ((forall n. Nat n => Size n -> a) -> a)
-> (forall n. Nat n => Size n -> a) -> a
forall a b. (a -> b) -> a -> b
$ Size (Succ n) -> a
forall n. Nat n => Size n -> a
f (Size (Succ n) -> a) -> (Size n -> Size (Succ n)) -> Size n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Size n -> Size (Succ n)
forall n. Size n -> Size (Succ n)
incSize