{-# 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