module Combinatorics.Battleship.Count.Frontier (
   T,
   Position,
   maxShipSize,

   Use(Blocked, Free, Vertical),
   blockBounded,
   empty,
   insertNew,
   isFree,
   dilate,
   lookup,
   reverse, Reverse,
   foldMap,
   toList,
   mapToVector,

   fromList,
   fromString,

   propDilate,
   propReverse4,
   propReverse5,
   propReverse6,
   propReverse7,
   propReverse8,
   propReverse9,
   propReverse10,
   ) where

import qualified Combinatorics.Battleship.Size as Size
import Combinatorics.Battleship.Size
         (Nat, Size(Size), N4, N5, N6, N7, N8, N9, N10, N11)

import qualified Foreign.Storable.Newtype as Store
import qualified Foreign.Storable as St
import Foreign.Storable (Storable, alignment, poke, peek, )

import Control.Applicative ((<$>), )

import qualified Data.StorableVector.Lazy.Builder as SVBuilder
import qualified Data.StorableVector.Lazy as SVL
import qualified Data.StorableVector as SV
import qualified Data.Monoid.HT as Mn
import Data.Bits (Bits, (.&.), (.|.), shiftL, shiftR, complement, )
import Data.Word (Word32, Word64, )
import Data.Char (ord, chr, )

import Data.Monoid (Monoid, mempty, mappend, )
import Data.Function.HT (nest, )
import Data.Bool.HT (if', )

import qualified Test.QuickCheck as QC

import Prelude2010 hiding (lookup, reverse, )
import Prelude ()


type Position = Int

data Use =
     Free
   | Blocked
   | Vertical Int
   deriving (Use -> Use -> Bool
(Use -> Use -> Bool) -> (Use -> Use -> Bool) -> Eq Use
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Use -> Use -> Bool
$c/= :: Use -> Use -> Bool
== :: Use -> Use -> Bool
$c== :: Use -> Use -> Bool
Eq, Int -> Use -> ShowS
[Use] -> ShowS
Use -> String
(Int -> Use -> ShowS)
-> (Use -> String) -> ([Use] -> ShowS) -> Show Use
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Use] -> ShowS
$cshowList :: [Use] -> ShowS
show :: Use -> String
$cshow :: Use -> String
showsPrec :: Int -> Use -> ShowS
$cshowsPrec :: Int -> Use -> ShowS
Show)

{- |
Efficient representation of a (Map Position Use).

We need it for description of a cut of a board with ships.

>    ....#.....
>    ....#.....
>    ..........
>    ####......
>    ..........
> ___...#...#..___
>    ##.#...#..
>    ...#......
>    ...#..###.
>    ..........

Say, we are constructing the board with ships beginning from the bottom.
Using information from the cut,
we want to know at what positions in the upper plane are ships allowed.
In the example the frontier at the cut would be

> fromString "xxx3x.x1x."

The numbers 3 and 1 denotes lengths of the parts of vertical ships below the cut.
The @x@'s denote blocked columns,
i.e. in these columns it is not allowed to place ships
immediately above the cut.
-}
newtype T w = Cons {T w -> Word32
decons :: Word32}
   deriving (T w -> T w -> Bool
(T w -> T w -> Bool) -> (T w -> T w -> Bool) -> Eq (T w)
forall w. T w -> T w -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: T w -> T w -> Bool
$c/= :: forall w. T w -> T w -> Bool
== :: T w -> T w -> Bool
$c== :: forall w. T w -> T w -> Bool
Eq, Eq (T w)
Eq (T w)
-> (T w -> T w -> Ordering)
-> (T w -> T w -> Bool)
-> (T w -> T w -> Bool)
-> (T w -> T w -> Bool)
-> (T w -> T w -> Bool)
-> (T w -> T w -> T w)
-> (T w -> T w -> T w)
-> Ord (T w)
T w -> T w -> Bool
T w -> T w -> Ordering
T w -> T w -> T w
forall w. Eq (T w)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall w. T w -> T w -> Bool
forall w. T w -> T w -> Ordering
forall w. T w -> T w -> T w
min :: T w -> T w -> T w
$cmin :: forall w. T w -> T w -> T w
max :: T w -> T w -> T w
$cmax :: forall w. T w -> T w -> T w
>= :: T w -> T w -> Bool
$c>= :: forall w. T w -> T w -> Bool
> :: T w -> T w -> Bool
$c> :: forall w. T w -> T w -> Bool
<= :: T w -> T w -> Bool
$c<= :: forall w. T w -> T w -> Bool
< :: T w -> T w -> Bool
$c< :: forall w. T w -> T w -> Bool
compare :: T w -> T w -> Ordering
$ccompare :: forall w. T w -> T w -> Ordering
$cp1Ord :: forall w. Eq (T w)
Ord) -- for use as key in a Map


instance (Nat w) => Show (T w) where
   showsPrec :: Int -> T w -> ShowS
showsPrec Int
prec T w
x =
      Bool -> ShowS -> ShowS
showParen (Int
precInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
         String -> ShowS
showString String
"Frontier.fromString " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
         String -> ShowS
forall a. Show a => a -> ShowS
shows (T w -> String
forall w. Nat w => T w -> String
toString T w
x)

instance Storable (T w) where
   sizeOf :: T w -> Int
sizeOf = (T w -> Word32) -> T w -> Int
forall core wrapper.
Storable core =>
(wrapper -> core) -> wrapper -> Int
Store.sizeOf T w -> Word32
forall w. T w -> Word32
decons
   alignment :: T w -> Int
alignment = (T w -> Word32) -> T w -> Int
forall core wrapper.
Storable core =>
(wrapper -> core) -> wrapper -> Int
Store.alignment T w -> Word32
forall w. T w -> Word32
decons
   poke :: Ptr (T w) -> T w -> IO ()
poke = (T w -> Word32) -> Ptr (T w) -> T w -> IO ()
forall core wrapper.
Storable core =>
(wrapper -> core) -> Ptr wrapper -> wrapper -> IO ()
Store.poke T w -> Word32
forall w. T w -> Word32
decons
   peek :: Ptr (T w) -> IO (T w)
peek = (Word32 -> T w) -> Ptr (T w) -> IO (T w)
forall core wrapper.
Storable core =>
(core -> wrapper) -> Ptr wrapper -> IO wrapper
Store.peek Word32 -> T w
forall w. Word32 -> T w
Cons


debug :: Bool
debug :: Bool
debug = Bool
False

{-# INLINE checkPos #-}
checkPos :: String -> Size w -> Position -> a -> a
checkPos :: String -> Size w -> Int -> a -> a
checkPos String
name (Size Int
size) Int
pos =
   Bool -> a -> a -> a
forall a. Bool -> a -> a -> a
if' (Bool
debug Bool -> Bool -> Bool
&& (Int
posInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
0 Bool -> Bool -> Bool
|| Int
sizeInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=Int
pos)) (a -> a -> a) -> a -> a -> a
forall a b. (a -> b) -> a -> b
$
      String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": position " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
pos String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" out of range"

{-# INLINE validUse #-}
validUse :: Use -> Bool
validUse :: Use -> Bool
validUse Use
use =
   case Use
use of
      Vertical Int
k -> Int
0Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
k Bool -> Bool -> Bool
&& Int
kInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=Int
maxShipSize
      Use
_ -> Bool
True

{-# INLINE checkUse #-}
checkUse :: String -> Use -> a -> a
checkUse :: String -> Use -> a -> a
checkUse String
name Use
use =
   Bool -> a -> a -> a
forall a. Bool -> a -> a -> a
if' (Bool
debug Bool -> Bool -> Bool
&& Bool -> Bool
not (Use -> Bool
validUse Use
use)) (a -> a -> a) -> a -> a -> a
forall a b. (a -> b) -> a -> b
$
      String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": invalid use " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Use -> String
forall a. Show a => a -> String
show Use
use

{-# INLINE checkFree #-}
checkFree :: String -> Bool -> a -> a
checkFree :: String -> Bool -> a -> a
checkFree String
name Bool
free =
   Bool -> a -> a -> a
forall a. Bool -> a -> a -> a
if' (Bool
debug Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
free) (a -> a -> a) -> a -> a -> a
forall a b. (a -> b) -> a -> b
$
      String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": position not free"

bitsPerNumber :: Int
bitsPerNumber :: Int
bitsPerNumber = Int
3

mask :: Word32
mask :: Word32
mask = Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL Word32
1 Int
bitsPerNumber Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
- Word32
1

maxShipSize :: Int
maxShipSize :: Int
maxShipSize = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
mask Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

bitsFromUse :: Use -> Word32
bitsFromUse :: Use -> Word32
bitsFromUse Use
use =
   case Use
use of
      Use
Free -> Word32
0
      Use
Blocked -> Word32
mask
      Vertical Int
n -> Int -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n

useFromBits :: Word32 -> Use
useFromBits :: Word32 -> Use
useFromBits Word32
bits =
   Bool -> Use -> Use -> Use
forall a. Bool -> a -> a -> a
if' (Word32
bitsWord32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
==Word32
0) Use
Free (Use -> Use) -> Use -> Use
forall a b. (a -> b) -> a -> b
$
   Bool -> Use -> Use -> Use
forall a. Bool -> a -> a -> a
if' (Word32
bitsWord32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
==Word32
mask) Use
Blocked (Use -> Use) -> Use -> Use
forall a b. (a -> b) -> a -> b
$
   Int -> Use
Vertical (Int -> Use) -> Int -> Use
forall a b. (a -> b) -> a -> b
$ Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
bits

useFromChar :: Char -> Use
useFromChar :: Char -> Use
useFromChar Char
c =
   case Char
c of
      Char
'.' -> Use
Free
      Char
'x' -> Use
Blocked
      Char
_ ->
         Bool -> Use -> Use -> Use
forall a. Bool -> a -> a -> a
if' (Char
'1'Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<=Char
c Bool -> Bool -> Bool
&& Char
cChar -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<=Char
'9')
            (Int -> Use
Vertical (Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0'))
            (String -> Use
forall a. HasCallStack => String -> a
error (String -> Use) -> String -> Use
forall a b. (a -> b) -> a -> b
$ String
"useFromChar: illegal charactor '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: String
"'")

empty :: T w
empty :: T w
empty = Word32 -> T w
forall w. Word32 -> T w
Cons Word32
0

fromList :: [Use] -> T w
fromList :: [Use] -> T w
fromList =
   Word32 -> T w
forall w. Word32 -> T w
Cons (Word32 -> T w) -> ([Use] -> Word32) -> [Use] -> T w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word32 -> Word32 -> Word32) -> Word32 -> [Word32] -> Word32
forall a b. (a -> b -> a) -> a -> [b] -> a
foldl Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
(.|.) Word32
0 ([Word32] -> Word32) -> ([Use] -> [Word32]) -> [Use] -> Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   (Int -> Word32 -> Word32) -> [Int] -> [Word32] -> [Word32]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
pos Word32
x -> Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL Word32
x (Int
posInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
bitsPerNumber)) [Int
0..] ([Word32] -> [Word32]) -> ([Use] -> [Word32]) -> [Use] -> [Word32]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   (Use -> Word32) -> [Use] -> [Word32]
forall a b. (a -> b) -> [a] -> [b]
map Use -> Word32
bitsFromUse

fromString :: String -> T w
fromString :: String -> T w
fromString =
   [Use] -> T w
forall w. [Use] -> T w
fromList ([Use] -> T w) -> (String -> [Use]) -> String -> T w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Use) -> String -> [Use]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Use
useFromChar

sizeOf :: (Nat w) => T w -> Size w
sizeOf :: T w -> Size w
sizeOf T w
_ = Size w
forall n. Nat n => Size n
Size.size

lookup :: (Nat w) => T w -> Position -> Use
lookup :: T w -> Int -> Use
lookup frontier :: T w
frontier@(Cons Word32
bits) Int
pos =
   String -> Size w -> Int -> Use -> Use
forall w a. String -> Size w -> Int -> a -> a
checkPos String
"Frontier.lookup" (T w -> Size w
forall w. Nat w => T w -> Size w
sizeOf T w
frontier) Int
pos (Use -> Use) -> Use -> Use
forall a b. (a -> b) -> a -> b
$ Word32 -> Use
useFromBits (Word32 -> Use) -> Word32 -> Use
forall a b. (a -> b) -> a -> b
$
   Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftR Word32
bits (Int
posInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
bitsPerNumber) Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
mask

isFree :: (Nat w) => T w -> Position -> Bool
isFree :: T w -> Int -> Bool
isFree T w
frontier Int
pos =
   T w -> Int -> Use
forall w. Nat w => T w -> Int -> Use
lookup T w
frontier Int
pos Use -> Use -> Bool
forall a. Eq a => a -> a -> Bool
== Use
Free

{- |
Only allowed at positions containing 'Free'.
-}
insertNew :: (Nat w) => Position -> Use -> T w -> T w
insertNew :: Int -> Use -> T w -> T w
insertNew Int
pos Use
use frontier :: T w
frontier@(Cons Word32
bits) =
   let name :: String
name = String
"Frontier.insertNew"
   in  String -> Size w -> Int -> T w -> T w
forall w a. String -> Size w -> Int -> a -> a
checkPos String
name (T w -> Size w
forall w. Nat w => T w -> Size w
sizeOf T w
frontier) Int
pos (T w -> T w) -> T w -> T w
forall a b. (a -> b) -> a -> b
$ String -> Use -> T w -> T w
forall a. String -> Use -> a -> a
checkUse String
name Use
use (T w -> T w) -> T w -> T w
forall a b. (a -> b) -> a -> b
$
       String -> Bool -> T w -> T w
forall a. String -> Bool -> a -> a
checkFree String
name (T w -> Int -> Bool
forall w. Nat w => T w -> Int -> Bool
isFree T w
frontier Int
pos) (T w -> T w) -> T w -> T w
forall a b. (a -> b) -> a -> b
$
       Word32 -> T w
forall w. Word32 -> T w
Cons (Word32 -> T w) -> Word32 -> T w
forall a b. (a -> b) -> a -> b
$ Word32
bits Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL (Use -> Word32
bitsFromUse Use
use) (Int
posInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
bitsPerNumber)

{- |
Inserts at positions outside of the bounds are ignored.
You may overwrite Free or Blocked fields, but not Vertical ones.
-}
blockBounded :: (Nat w) => Size w -> Position -> T w -> T w
blockBounded :: Size w -> Int -> T w -> T w
blockBounded (Size Int
size) Int
pos frontier :: T w
frontier@(Cons Word32
bits) =
   Bool -> T w -> T w -> T w
forall a. Bool -> a -> a -> a
if' (Int
posInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
0 Bool -> Bool -> Bool
|| Int
sizeInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=Int
pos) T w
frontier (T w -> T w) -> T w -> T w
forall a b. (a -> b) -> a -> b
$
   Bool -> T w -> T w -> T w
forall a. Bool -> a -> a -> a
if' (Bool
debug Bool -> Bool -> Bool
&& case T w -> Int -> Use
forall w. Nat w => T w -> Int -> Use
lookup T w
frontier Int
pos of Vertical Int
_ -> Bool
True; Use
_ -> Bool
False)
      (String -> T w
forall a. HasCallStack => String -> a
error (String -> T w) -> String -> T w
forall a b. (a -> b) -> a -> b
$ String
"Frontier.insertBounded: tried to overwrite Vertical at position " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
pos)
      (Word32 -> T w
forall w. Word32 -> T w
Cons (Word32 -> T w) -> Word32 -> T w
forall a b. (a -> b) -> a -> b
$ Word32
bits Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL (Use -> Word32
bitsFromUse Use
Blocked) (Int
posInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
bitsPerNumber))


dilate :: Size w -> T w -> T w
dilate :: Size w -> T w -> T w
dilate = Size w -> T w -> T w
forall w. Size w -> T w -> T w
dilateComb

dilateComb :: Size w -> T w -> T w
dilateComb :: Size w -> T w -> T w
dilateComb (Size Int
size) =
   let comb :: Word32
comb = Int -> Int -> Word32
forall a. (Bits a, Integral a) => Int -> Int -> a
replicateOne Int
size Int
1
   in  \(Cons Word32
bits) ->
         let occupied :: Word32
occupied = Word32
bits Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftR Word32
bits Int
1 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftR Word32
bits Int
2
             additional :: Word32
additional =
               (Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL Word32
occupied Int
bitsPerNumber Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftR Word32
occupied Int
bitsPerNumber)
               Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&.
               Word32 -> Word32
forall a. Bits a => a -> a
complement Word32
occupied
               Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&.
               Word32
comb
         in  Word32 -> T w
forall w. Word32 -> T w
Cons (Word32 -> T w) -> Word32 -> T w
forall a b. (a -> b) -> a -> b
$ Word32
bits Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.
               Word32
additional Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL Word32
additional Int
1 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL Word32
additional Int
2

dilateGen :: (Nat w) => Size w -> T w -> T w
dilateGen :: Size w -> T w -> T w
dilateGen width :: Size w
width@(Size Int
size) T w
frontier =
   (T w -> Int -> T w) -> T w -> [Int] -> T w
forall a b. (a -> b -> a) -> a -> [b] -> a
foldl ((Int -> T w -> T w) -> T w -> Int -> T w
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Int -> T w -> T w) -> T w -> Int -> T w)
-> (Int -> T w -> T w) -> T w -> Int -> T w
forall a b. (a -> b) -> a -> b
$ Size w -> Int -> T w -> T w
forall w. Nat w => Size w -> Int -> T w -> T w
blockBounded Size w
width) T w
frontier ([Int] -> T w) -> [Int] -> T w
forall a b. (a -> b) -> a -> b
$
   (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (T w -> Int -> Bool
forall w. Nat w => T w -> Int -> Bool
isFree T w
frontier) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$
   (Int -> [Int]) -> [Int] -> [Int]
forall a b. (a -> [b]) -> [a] -> [b]
concatMap (\Int
k -> Bool -> [Int] -> [Int]
forall m. Monoid m => Bool -> m -> m
Mn.when (Int
kInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
0) [Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ Bool -> [Int] -> [Int]
forall m. Monoid m => Bool -> m -> m
Mn.when (Int
kInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
sizeInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1]) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$
   (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Int -> Bool) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T w -> Int -> Bool
forall w. Nat w => T w -> Int -> Bool
isFree T w
frontier) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
size [Int
0..]

propDilate :: QC.Property
propDilate :: Property
propDilate =
   Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll ((Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
QC.choose (Int
0,Int
10)) ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
   Int -> (forall n. Nat n => Size n -> Property) -> Property
forall a. Int -> (forall n. Nat n => Size n -> a) -> a
Size.reifyInt Int
n
      (\Size n
size -> Gen (T n) -> (T n -> [T n]) -> (T n -> Bool) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QC.forAllShrink Gen (T n)
forall a. Arbitrary a => Gen a
QC.arbitrary T n -> [T n]
forall a. Arbitrary a => a -> [a]
QC.shrink ((T n -> Bool) -> Property) -> (T n -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ Size n -> T n -> Bool
forall w. Nat w => Size w -> T w -> Bool
propDilateTyped Size n
size)

propDilateTyped :: (Nat w) => Size w -> T w -> Bool
propDilateTyped :: Size w -> T w -> Bool
propDilateTyped Size w
size T w
frontier =
   Size w -> T w -> T w
forall w. Size w -> T w -> T w
dilateComb Size w
size T w
frontier T w -> T w -> Bool
forall a. Eq a => a -> a -> Bool
== Size w -> T w -> T w
forall w. Nat w => Size w -> T w -> T w
dilateGen Size w
size T w
frontier

mapToVector ::
   (Nat w, Storable a) => Size w -> (Use -> a) -> T w -> SV.Vector a
mapToVector :: Size w -> (Use -> a) -> T w -> Vector a
mapToVector (Size Int
size) Use -> a
f T w
frontier =
   Int -> (Int -> a) -> Vector a
forall a. Storable a => Int -> (Int -> a) -> Vector a
SV.sample Int
size ((Int -> a) -> Vector a) -> (Int -> a) -> Vector a
forall a b. (a -> b) -> a -> b
$ Use -> a
f (Use -> a) -> (Int -> Use) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T w -> Int -> Use
forall w. Nat w => T w -> Int -> Use
lookup T w
frontier

_mapToVector ::
   (Nat w, Storable a) => Size w -> (Use -> a) -> T w -> SV.Vector a
_mapToVector :: Size w -> (Use -> a) -> T w -> Vector a
_mapToVector (Size Int
size) Use -> a
f =
   [Vector a] -> Vector a
forall a. Storable a => [Vector a] -> Vector a
SV.concat ([Vector a] -> Vector a) -> (T w -> [Vector a]) -> T w -> Vector a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector a -> [Vector a]
forall a. Vector a -> [Vector a]
SVL.chunks (Vector a -> [Vector a]) -> (T w -> Vector a) -> T w -> [Vector a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   ChunkSize -> Builder a -> Vector a
forall a. Storable a => ChunkSize -> Builder a -> Vector a
SVBuilder.toLazyStorableVector (Int -> ChunkSize
SVL.chunkSize Int
size) (Builder a -> Vector a) -> (T w -> Builder a) -> T w -> Vector a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
   (Use -> Builder a) -> T w -> Builder a
forall m w. Monoid m => (Use -> m) -> T w -> m
foldMap (a -> Builder a
forall a. Storable a => a -> Builder a
SVBuilder.put (a -> Builder a) -> (Use -> a) -> Use -> Builder a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Use -> a
f)


{- |
Can be faster than 'toList' since it does not build a list.
It ignores 'Free' squares at the end of the frontier.
-}
{-# INLINE foldMap #-}
foldMap :: (Monoid m) => (Use -> m) -> T w -> m
foldMap :: (Use -> m) -> T w -> m
foldMap Use -> m
f =
   let go :: m -> Word32 -> m
go m
m Word32
bits =
         if Word32
bitsWord32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
==Word32
0
           then m
m
           else m -> Word32 -> m
go (m -> m -> m
forall a. Monoid a => a -> a -> a
mappend m
m (Use -> m
f (Use -> m) -> Use -> m
forall a b. (a -> b) -> a -> b
$ Word32 -> Use
useFromBits (Word32 -> Use) -> Word32 -> Use
forall a b. (a -> b) -> a -> b
$ Word32
bits Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
mask)) (Word32 -> m) -> Word32 -> m
forall a b. (a -> b) -> a -> b
$
                Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftR Word32
bits Int
bitsPerNumber
   in  m -> Word32 -> m
go m
forall a. Monoid a => a
mempty (Word32 -> m) -> (T w -> Word32) -> T w -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T w -> Word32
forall w. T w -> Word32
decons

toListWithSize :: (Nat w) => Size w -> T w -> [Use]
toListWithSize :: Size w -> T w -> [Use]
toListWithSize (Size Int
width) T w
frontier = (Int -> Use) -> [Int] -> [Use]
forall a b. (a -> b) -> [a] -> [b]
map (T w -> Int -> Use
forall w. Nat w => T w -> Int -> Use
lookup T w
frontier) ([Int] -> [Use]) -> [Int] -> [Use]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
width [Int
0 ..]

toList :: (Nat w) => T w -> [Use]
toList :: T w -> [Use]
toList = Size w -> T w -> [Use]
forall w. Nat w => Size w -> T w -> [Use]
toListWithSize Size w
forall n. Nat n => Size n
Size.size

charFromUse :: Use -> Char
charFromUse :: Use -> Char
charFromUse Use
u =
   case Use
u of
      Use
Free -> Char
'.'
      Use
Blocked -> Char
'x'
      Vertical Int
n ->
         Bool -> Char -> Char -> Char
forall a. Bool -> a -> a -> a
if' (Int
1Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=Int
n Bool -> Bool -> Bool
&& Int
nInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=Int
9)
            (Int -> Char
chr (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
ord Char
'0'))
            (String -> Char
forall a. HasCallStack => String -> a
error (String -> Char) -> String -> Char
forall a b. (a -> b) -> a -> b
$ String
"charFromUse: illegal vertical number " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)

toString :: (Nat w) => T w -> String
toString :: T w -> String
toString = (Use -> Char) -> [Use] -> String
forall a b. (a -> b) -> [a] -> [b]
map Use -> Char
charFromUse ([Use] -> String) -> (T w -> [Use]) -> T w -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T w -> [Use]
forall w. Nat w => T w -> [Use]
toList


newtype Reverse w = Reverse {Reverse w -> T w -> T w
runReverse :: T w -> T w}
newtype Reverse1 w = Reverse1 {Reverse1 w -> T (P1 w) -> T (P1 w)
runReverse1 :: T (Size.P1 w) -> T (Size.P1 w)}
newtype Reverse2 w = Reverse2 {Reverse2 w -> T (P2 w) -> T (P2 w)
runReverse2 :: T (Size.P2 w) -> T (Size.P2 w)}
newtype Reverse3 w = Reverse3 {Reverse3 w -> T (P3 w) -> T (P3 w)
runReverse3 :: T (Size.P3 w) -> T (Size.P3 w)}
newtype Reverse4 w = Reverse4 {Reverse4 w -> T (P4 w) -> T (P4 w)
runReverse4 :: T (Size.P4 w) -> T (Size.P4 w)}
newtype Reverse5 w = Reverse5 {Reverse5 w -> T (P5 w) -> T (P5 w)
runReverse5 :: T (Size.P5 w) -> T (Size.P5 w)}
newtype Reverse6 w = Reverse6 {Reverse6 w -> T (P6 w) -> T (P6 w)
runReverse6 :: T (Size.P6 w) -> T (Size.P6 w)}
newtype Reverse7 w = Reverse7 {Reverse7 w -> T (P7 w) -> T (P7 w)
runReverse7 :: T (Size.P7 w) -> T (Size.P7 w)}
newtype Reverse8 w = Reverse8 {Reverse8 w -> T (P8 w) -> T (P8 w)
runReverse8 :: T (Size.P8 w) -> T (Size.P8 w)}
newtype Reverse9 w = Reverse9 {Reverse9 w -> T (P9 w) -> T (P9 w)
runReverse9 :: T (Size.P9 w) -> T (Size.P9 w)}
newtype Reverse10 w = Reverse10 {Reverse10 w -> T (P10 w) -> T (P10 w)
runReverse10 :: T (Size.P10 w) -> T (Size.P10 w)}

reverse :: Nat w => T w -> T w
reverse :: T w -> T w
reverse =
   Reverse w -> T w -> T w
forall w. Reverse w -> T w -> T w
runReverse (Reverse w -> T w -> T w) -> Reverse w -> T w -> T w
forall a b. (a -> b) -> a -> b
$ Reverse Zero -> (forall m. Nat m => Reverse (Succ m)) -> Reverse w
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T Zero -> T Zero) -> Reverse Zero
forall w. (T w -> T w) -> Reverse w
Reverse T Zero -> T Zero
forall a. a -> a
id) ((forall m. Nat m => Reverse (Succ m)) -> Reverse w)
-> (forall m. Nat m => Reverse (Succ m)) -> Reverse w
forall a b. (a -> b) -> a -> b
$ (T (P1 m) -> T (P1 m)) -> Reverse (P1 m)
forall w. (T w -> T w) -> Reverse w
Reverse ((T (P1 m) -> T (P1 m)) -> Reverse (P1 m))
-> (T (P1 m) -> T (P1 m)) -> Reverse (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse1 m -> T (P1 m) -> T (P1 m)
forall w. Reverse1 w -> T (P1 w) -> T (P1 w)
runReverse1 (Reverse1 m -> T (P1 m) -> T (P1 m))
-> Reverse1 m -> T (P1 m) -> T (P1 m)
forall a b. (a -> b) -> a -> b
$ Reverse1 Zero
-> (forall m. Nat m => Reverse1 (Succ m)) -> Reverse1 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P1 Zero) -> T (P1 Zero)) -> Reverse1 Zero
forall w. (T (P1 w) -> T (P1 w)) -> Reverse1 w
Reverse1 T (P1 Zero) -> T (P1 Zero)
forall a. a -> a
id) ((forall m. Nat m => Reverse1 (Succ m)) -> Reverse1 m)
-> (forall m. Nat m => Reverse1 (Succ m)) -> Reverse1 m
forall a b. (a -> b) -> a -> b
$ (T (P1 (P1 m)) -> T (P1 (P1 m))) -> Reverse1 (P1 m)
forall w. (T (P1 w) -> T (P1 w)) -> Reverse1 w
Reverse1 ((T (P1 (P1 m)) -> T (P1 (P1 m))) -> Reverse1 (P1 m))
-> (T (P1 (P1 m)) -> T (P1 (P1 m))) -> Reverse1 (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse2 m -> T (P1 (P1 m)) -> T (P1 (P1 m))
forall w. Reverse2 w -> T (P2 w) -> T (P2 w)
runReverse2 (Reverse2 m -> T (P1 (P1 m)) -> T (P1 (P1 m)))
-> Reverse2 m -> T (P1 (P1 m)) -> T (P1 (P1 m))
forall a b. (a -> b) -> a -> b
$ Reverse2 Zero
-> (forall m. Nat m => Reverse2 (Succ m)) -> Reverse2 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P2 Zero) -> T (P2 Zero)) -> Reverse2 Zero
forall w. (T (P2 w) -> T (P2 w)) -> Reverse2 w
Reverse2 ((T (P2 Zero) -> T (P2 Zero)) -> Reverse2 Zero)
-> (T (P2 Zero) -> T (P2 Zero)) -> Reverse2 Zero
forall a b. (a -> b) -> a -> b
$ Size (P2 Zero) -> T (P2 Zero) -> T (P2 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P2 Zero)
forall n. Nat n => Size n
Size.size) ((forall m. Nat m => Reverse2 (Succ m)) -> Reverse2 m)
-> (forall m. Nat m => Reverse2 (Succ m)) -> Reverse2 m
forall a b. (a -> b) -> a -> b
$ (T (P2 (P1 m)) -> T (P2 (P1 m))) -> Reverse2 (P1 m)
forall w. (T (P2 w) -> T (P2 w)) -> Reverse2 w
Reverse2 ((T (P2 (P1 m)) -> T (P2 (P1 m))) -> Reverse2 (P1 m))
-> (T (P2 (P1 m)) -> T (P2 (P1 m))) -> Reverse2 (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse3 m -> T (P2 (P1 m)) -> T (P2 (P1 m))
forall w. Reverse3 w -> T (P3 w) -> T (P3 w)
runReverse3 (Reverse3 m -> T (P2 (P1 m)) -> T (P2 (P1 m)))
-> Reverse3 m -> T (P2 (P1 m)) -> T (P2 (P1 m))
forall a b. (a -> b) -> a -> b
$ Reverse3 Zero
-> (forall m. Nat m => Reverse3 (Succ m)) -> Reverse3 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P3 Zero) -> T (P3 Zero)) -> Reverse3 Zero
forall w. (T (P3 w) -> T (P3 w)) -> Reverse3 w
Reverse3 ((T (P3 Zero) -> T (P3 Zero)) -> Reverse3 Zero)
-> (T (P3 Zero) -> T (P3 Zero)) -> Reverse3 Zero
forall a b. (a -> b) -> a -> b
$ Size (P3 Zero) -> T (P3 Zero) -> T (P3 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P3 Zero)
forall n. Nat n => Size n
Size.size) ((forall m. Nat m => Reverse3 (Succ m)) -> Reverse3 m)
-> (forall m. Nat m => Reverse3 (Succ m)) -> Reverse3 m
forall a b. (a -> b) -> a -> b
$ (T (P3 (P1 m)) -> T (P3 (P1 m))) -> Reverse3 (P1 m)
forall w. (T (P3 w) -> T (P3 w)) -> Reverse3 w
Reverse3 ((T (P3 (P1 m)) -> T (P3 (P1 m))) -> Reverse3 (P1 m))
-> (T (P3 (P1 m)) -> T (P3 (P1 m))) -> Reverse3 (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse4 m -> T (P3 (P1 m)) -> T (P3 (P1 m))
forall w. Reverse4 w -> T (P4 w) -> T (P4 w)
runReverse4 (Reverse4 m -> T (P3 (P1 m)) -> T (P3 (P1 m)))
-> Reverse4 m -> T (P3 (P1 m)) -> T (P3 (P1 m))
forall a b. (a -> b) -> a -> b
$ Reverse4 Zero
-> (forall m. Nat m => Reverse4 (Succ m)) -> Reverse4 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P4 Zero) -> T (P4 Zero)) -> Reverse4 Zero
forall w. (T (P4 w) -> T (P4 w)) -> Reverse4 w
Reverse4 T (P4 Zero) -> T (P4 Zero)
reverse4spread) ((forall m. Nat m => Reverse4 (Succ m)) -> Reverse4 m)
-> (forall m. Nat m => Reverse4 (Succ m)) -> Reverse4 m
forall a b. (a -> b) -> a -> b
$ (T (P4 (P1 m)) -> T (P4 (P1 m))) -> Reverse4 (P1 m)
forall w. (T (P4 w) -> T (P4 w)) -> Reverse4 w
Reverse4 ((T (P4 (P1 m)) -> T (P4 (P1 m))) -> Reverse4 (P1 m))
-> (T (P4 (P1 m)) -> T (P4 (P1 m))) -> Reverse4 (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse5 m -> T (P4 (P1 m)) -> T (P4 (P1 m))
forall w. Reverse5 w -> T (P5 w) -> T (P5 w)
runReverse5 (Reverse5 m -> T (P4 (P1 m)) -> T (P4 (P1 m)))
-> Reverse5 m -> T (P4 (P1 m)) -> T (P4 (P1 m))
forall a b. (a -> b) -> a -> b
$ Reverse5 Zero
-> (forall m. Nat m => Reverse5 (Succ m)) -> Reverse5 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P5 Zero) -> T (P5 Zero)) -> Reverse5 Zero
forall w. (T (P5 w) -> T (P5 w)) -> Reverse5 w
Reverse5 T (P5 Zero) -> T (P5 Zero)
reverse5spread) ((forall m. Nat m => Reverse5 (Succ m)) -> Reverse5 m)
-> (forall m. Nat m => Reverse5 (Succ m)) -> Reverse5 m
forall a b. (a -> b) -> a -> b
$ (T (P5 (P1 m)) -> T (P5 (P1 m))) -> Reverse5 (P1 m)
forall w. (T (P5 w) -> T (P5 w)) -> Reverse5 w
Reverse5 ((T (P5 (P1 m)) -> T (P5 (P1 m))) -> Reverse5 (P1 m))
-> (T (P5 (P1 m)) -> T (P5 (P1 m))) -> Reverse5 (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse6 m -> T (P5 (P1 m)) -> T (P5 (P1 m))
forall w. Reverse6 w -> T (P6 w) -> T (P6 w)
runReverse6 (Reverse6 m -> T (P5 (P1 m)) -> T (P5 (P1 m)))
-> Reverse6 m -> T (P5 (P1 m)) -> T (P5 (P1 m))
forall a b. (a -> b) -> a -> b
$ Reverse6 Zero
-> (forall m. Nat m => Reverse6 (Succ m)) -> Reverse6 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P6 Zero) -> T (P6 Zero)) -> Reverse6 Zero
forall w. (T (P6 w) -> T (P6 w)) -> Reverse6 w
Reverse6 T (P6 Zero) -> T (P6 Zero)
reverse6up) ((forall m. Nat m => Reverse6 (Succ m)) -> Reverse6 m)
-> (forall m. Nat m => Reverse6 (Succ m)) -> Reverse6 m
forall a b. (a -> b) -> a -> b
$ (T (P6 (P1 m)) -> T (P6 (P1 m))) -> Reverse6 (P1 m)
forall w. (T (P6 w) -> T (P6 w)) -> Reverse6 w
Reverse6 ((T (P6 (P1 m)) -> T (P6 (P1 m))) -> Reverse6 (P1 m))
-> (T (P6 (P1 m)) -> T (P6 (P1 m))) -> Reverse6 (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse7 m -> T (P6 (P1 m)) -> T (P6 (P1 m))
forall w. Reverse7 w -> T (P7 w) -> T (P7 w)
runReverse7 (Reverse7 m -> T (P6 (P1 m)) -> T (P6 (P1 m)))
-> Reverse7 m -> T (P6 (P1 m)) -> T (P6 (P1 m))
forall a b. (a -> b) -> a -> b
$ Reverse7 Zero
-> (forall m. Nat m => Reverse7 (Succ m)) -> Reverse7 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P7 Zero) -> T (P7 Zero)) -> Reverse7 Zero
forall w. (T (P7 w) -> T (P7 w)) -> Reverse7 w
Reverse7 T (P7 Zero) -> T (P7 Zero)
reverse7up) ((forall m. Nat m => Reverse7 (Succ m)) -> Reverse7 m)
-> (forall m. Nat m => Reverse7 (Succ m)) -> Reverse7 m
forall a b. (a -> b) -> a -> b
$ (T (P7 (P1 m)) -> T (P7 (P1 m))) -> Reverse7 (P1 m)
forall w. (T (P7 w) -> T (P7 w)) -> Reverse7 w
Reverse7 ((T (P7 (P1 m)) -> T (P7 (P1 m))) -> Reverse7 (P1 m))
-> (T (P7 (P1 m)) -> T (P7 (P1 m))) -> Reverse7 (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse8 m -> T (P7 (P1 m)) -> T (P7 (P1 m))
forall w. Reverse8 w -> T (P8 w) -> T (P8 w)
runReverse8 (Reverse8 m -> T (P7 (P1 m)) -> T (P7 (P1 m)))
-> Reverse8 m -> T (P7 (P1 m)) -> T (P7 (P1 m))
forall a b. (a -> b) -> a -> b
$ Reverse8 Zero
-> (forall m. Nat m => Reverse8 (Succ m)) -> Reverse8 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P8 Zero) -> T (P8 Zero)) -> Reverse8 Zero
forall w. (T (P8 w) -> T (P8 w)) -> Reverse8 w
Reverse8 T (P8 Zero) -> T (P8 Zero)
reverse8up) ((forall m. Nat m => Reverse8 (Succ m)) -> Reverse8 m)
-> (forall m. Nat m => Reverse8 (Succ m)) -> Reverse8 m
forall a b. (a -> b) -> a -> b
$ (T (P8 (P1 m)) -> T (P8 (P1 m))) -> Reverse8 (P1 m)
forall w. (T (P8 w) -> T (P8 w)) -> Reverse8 w
Reverse8 ((T (P8 (P1 m)) -> T (P8 (P1 m))) -> Reverse8 (P1 m))
-> (T (P8 (P1 m)) -> T (P8 (P1 m))) -> Reverse8 (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse9 m -> T (P8 (P1 m)) -> T (P8 (P1 m))
forall w. Reverse9 w -> T (P9 w) -> T (P9 w)
runReverse9 (Reverse9 m -> T (P8 (P1 m)) -> T (P8 (P1 m)))
-> Reverse9 m -> T (P8 (P1 m)) -> T (P8 (P1 m))
forall a b. (a -> b) -> a -> b
$ Reverse9 Zero
-> (forall m. Nat m => Reverse9 (Succ m)) -> Reverse9 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P9 Zero) -> T (P9 Zero)) -> Reverse9 Zero
forall w. (T (P9 w) -> T (P9 w)) -> Reverse9 w
Reverse9 T (P9 Zero) -> T (P9 Zero)
reverse9up) ((forall m. Nat m => Reverse9 (Succ m)) -> Reverse9 m)
-> (forall m. Nat m => Reverse9 (Succ m)) -> Reverse9 m
forall a b. (a -> b) -> a -> b
$ (T (P9 (P1 m)) -> T (P9 (P1 m))) -> Reverse9 (P1 m)
forall w. (T (P9 w) -> T (P9 w)) -> Reverse9 w
Reverse9 ((T (P9 (P1 m)) -> T (P9 (P1 m))) -> Reverse9 (P1 m))
-> (T (P9 (P1 m)) -> T (P9 (P1 m))) -> Reverse9 (P1 m)
forall a b. (a -> b) -> a -> b
$
   Reverse10 m -> T (P9 (P1 m)) -> T (P9 (P1 m))
forall w. Reverse10 w -> T (P10 w) -> T (P10 w)
runReverse10 (Reverse10 m -> T (P9 (P1 m)) -> T (P9 (P1 m)))
-> Reverse10 m -> T (P9 (P1 m)) -> T (P9 (P1 m))
forall a b. (a -> b) -> a -> b
$ Reverse10 Zero
-> (forall m. Nat m => Reverse10 (Succ m)) -> Reverse10 m
forall n (f :: * -> *).
Nat n =>
f Zero -> (forall m. Nat m => f (Succ m)) -> f n
Size.switch ((T (P10 Zero) -> T (P10 Zero)) -> Reverse10 Zero
forall w. (T (P10 w) -> T (P10 w)) -> Reverse10 w
Reverse10 T (P10 Zero) -> T (P10 Zero)
reverse10up) ((forall m. Nat m => Reverse10 (Succ m)) -> Reverse10 m)
-> (forall m. Nat m => Reverse10 (Succ m)) -> Reverse10 m
forall a b. (a -> b) -> a -> b
$ (T (P10 (Succ m)) -> T (P10 (Succ m))) -> Reverse10 (Succ m)
forall w. (T (P10 w) -> T (P10 w)) -> Reverse10 w
Reverse10 ((T (P10 (Succ m)) -> T (P10 (Succ m))) -> Reverse10 (Succ m))
-> (T (P10 (Succ m)) -> T (P10 (Succ m))) -> Reverse10 (Succ m)
forall a b. (a -> b) -> a -> b
$
   Size (P10 (Succ m)) -> T (P10 (Succ m)) -> T (P10 (Succ m))
forall w. Size w -> T w -> T w
reverseGen Size (P10 (Succ m))
forall n. Nat n => Size n
Size.size


reverseGen :: Size w -> T w -> T w
reverseGen :: Size w -> T w -> T w
reverseGen (Size Int
size) (Cons Word32
bits) =
   Word32 -> T w
forall w. Word32 -> T w
Cons (Word32 -> T w) -> Word32 -> T w
forall a b. (a -> b) -> a -> b
$ (Word32, Word32) -> Word32
forall a b. (a, b) -> b
snd ((Word32, Word32) -> Word32) -> (Word32, Word32) -> Word32
forall a b. (a -> b) -> a -> b
$
   Int
-> ((Word32, Word32) -> (Word32, Word32))
-> (Word32, Word32)
-> (Word32, Word32)
forall a. Int -> (a -> a) -> a -> a
nest Int
size
      (\(Word32
src, Word32
dst) ->
         (Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftR Word32
src Int
bitsPerNumber,
          Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL Word32
dst Int
bitsPerNumber Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|. (Word32
mask Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
src)))
      (Word32
bits, Word32
0)

{-# INLINE swap #-}
swap :: Int -> Word32 -> Word32 -> Word32
swap :: Int -> Word32 -> Word32 -> Word32
swap Int
n Word32
m Word32
bits =
   Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL (Word32
bits Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
m) (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
bitsPerNumber) Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.
   (Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftR Word32
bits (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
bitsPerNumber) Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
m)

reverse6up :: T N6 -> T N6
reverse6up :: T (P6 Zero) -> T (P6 Zero)
reverse6up (Cons Word32
bits0) =
   let bits1 :: Word32
bits1 = Int -> Word32 -> Word32 -> Word32
swap Int
1 Word32
0o070707 Word32
bits0
   in  Word32 -> T (P6 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P6 Zero)) -> Word32 -> T (P6 Zero)
forall a b. (a -> b) -> a -> b
$  Int -> Word32 -> Word32 -> Word32
swap Int
4 Word32
0o000077 Word32
bits1  Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.  Word32
bits1 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o007700

reverse7up :: T N7 -> T N7
reverse7up :: T (P7 Zero) -> T (P7 Zero)
reverse7up (Cons Word32
bits0) =
   let bits1 :: Word32
bits1 = Int -> Word32 -> Word32 -> Word32
swap Int
2 Word32
0o0070007 Word32
bits0  Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.  Word32
bits0 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o0700070
   in  Word32 -> T (P7 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P7 Zero)) -> Word32 -> T (P7 Zero)
forall a b. (a -> b) -> a -> b
$  Int -> Word32 -> Word32 -> Word32
swap Int
4 Word32
0o0000777 Word32
bits1  Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.  Word32
bits0 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o0007000

reverse8up :: T N8 -> T N8
reverse8up :: T (P8 Zero) -> T (P8 Zero)
reverse8up (Cons Word32
bits0) =
   let bits1 :: Word32
bits1 = Int -> Word32 -> Word32 -> Word32
swap Int
1 Word32
0o07070707 Word32
bits0
       bits2 :: Word32
bits2 = Int -> Word32 -> Word32 -> Word32
swap Int
2 Word32
0o00770077 Word32
bits1
   in  Word32 -> T (P8 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P8 Zero)) -> Word32 -> T (P8 Zero)
forall a b. (a -> b) -> a -> b
$  Int -> Word32 -> Word32 -> Word32
swap Int
4 Word32
0o00007777 Word32
bits2

reverse9up :: T N9 -> T N9
reverse9up :: T (P9 Zero) -> T (P9 Zero)
reverse9up (Cons Word32
bits0) =
   let bits1 :: Word32
bits1 = Int -> Word32 -> Word32 -> Word32
swap Int
1 Word32
0o070700707 Word32
bits0
       bits2 :: Word32
bits2 = Int -> Word32 -> Word32 -> Word32
swap Int
2 Word32
0o007700077 Word32
bits1
   in  Word32 -> T (P9 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P9 Zero)) -> Word32 -> T (P9 Zero)
forall a b. (a -> b) -> a -> b
$  Int -> Word32 -> Word32 -> Word32
swap Int
5 Word32
0o000007777 Word32
bits2  Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.  Word32
bits0 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o000070000

reverse10up :: T N10 -> T N10
reverse10up :: T (P10 Zero) -> T (P10 Zero)
reverse10up (Cons Word32
bits0) =
   let bits1 :: Word32
bits1 = Int -> Word32 -> Word32 -> Word32
swap Int
1 Word32
0o0707070707 Word32
bits0
       bits2 :: Word32
bits2 = Int -> Word32 -> Word32 -> Word32
swap Int
2 Word32
0o0077000077 Word32
bits1
   in  Word32 -> T (P10 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P10 Zero)) -> Word32 -> T (P10 Zero)
forall a b. (a -> b) -> a -> b
$  Int -> Word32 -> Word32 -> Word32
swap Int
6 Word32
0o0000007777 Word32
bits2  Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.  Word32
bits1 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o0000770000

reverse10down :: T N10 -> T N10
reverse10down :: T (P10 Zero) -> T (P10 Zero)
reverse10down (Cons Word32
bits0) =
   let bits1 :: Word32
bits1 = Int -> Word32 -> Word32 -> Word32
swap Int
5 Word32
0o0000077777 Word32
bits0
       bits2 :: Word32
bits2 = Int -> Word32 -> Word32 -> Word32
swap Int
3 Word32
0o0007700077 Word32
bits1
   in  Word32 -> T (P10 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P10 Zero)) -> Word32 -> T (P10 Zero)
forall a b. (a -> b) -> a -> b
$  Int -> Word32 -> Word32 -> Word32
swap Int
1 Word32
0o0700707007 Word32
bits2  Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.  Word32
bits1 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o0070000700

reverse11up :: T N11 -> T N11
reverse11up :: T N11 -> T N11
reverse11up (Cons Word32
bits0) =
   let bits1 :: Word32
bits1 = Int -> Word32 -> Word32 -> Word32
swap Int
1 Word32
0o07007007007 Word32
bits0
       bits2 :: Word32
bits2 = Int -> Word32 -> Word32 -> Word32
swap Int
3 Word32
0o00077000077 Word32
bits1  Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.  Word32
bits0 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o00700000700
   in  Word32 -> T N11
forall w. Word32 -> T w
Cons (Word32 -> T N11) -> Word32 -> T N11
forall a b. (a -> b) -> a -> b
$  Int -> Word32 -> Word32 -> Word32
swap Int
6 Word32
0o00000077777 Word32
bits2  Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.  Word32
bits0 Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o00000700000


reverse4spread :: T N4 -> T N4
reverse4spread :: T (P4 Zero) -> T (P4 Zero)
reverse4spread (Cons Word32
bits) =
   Word32 -> T (P4 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P4 Zero)) -> Word32 -> T (P4 Zero)
forall a b. (a -> b) -> a -> b
$
   let full :: Word32
full = Word32
0o7777
   in  if Word32
bits Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
full
         then Word32
full
         else Word32 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Word32) -> Word32 -> Word32
forall a b. (a -> b) -> a -> b
$ Word32 -> Word32 -> Word32
forall a. Integral a => a -> a -> a
mod ((Word32
bits Word32 -> Word32 -> Word32
forall a. Num a => a -> a -> a
* Word32
0o10000010) Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o7070070700) Word32
full
{-
dcba

0abc d00a bcd0
 |^  ^  ^  ^
-}

reverse5spread :: T N5 -> T N5
reverse5spread :: T (P5 Zero) -> T (P5 Zero)
reverse5spread (Cons Word32
bits) =
   Word32 -> T (P5 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P5 Zero)) -> Word32 -> T (P5 Zero)
forall a b. (a -> b) -> a -> b
$ Word64 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Word32) -> Word64 -> Word32
forall a b. (a -> b) -> a -> b
$
   Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
mod
      ((Word32 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
bits Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
0o10000000100000001)
       Word64 -> Word64 -> Word64
forall a. Bits a => a -> a -> a
.&. Word64
0o70070007007000000700)
      (Word64
0o777777 :: Word64)
{-
      ((fromIntegral bits * 0o_010000_000100_000001)
       .&. 0o70 070007 007000 000700)

 edcba

000abc de000a bcde00 0abcde
   |^   ^   ^   ^       ^
-}

reverse10spread :: T N10 -> T N10
reverse10spread :: T (P10 Zero) -> T (P10 Zero)
reverse10spread =
   let full :: Word32
full = Int -> Word32
forall a. (Bits a, Integral a) => Int -> a
multiMask Int
10
       spread :: Integer
spread = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL (Int -> Int -> Integer
forall a. (Bits a, Integral a) => Int -> Int -> a
replicateOne Int
5 Int
12) Int
bitsPerNumber
       revMask :: Integer
revMask = Int -> Int -> Integer
forall a. (Bits a, Integral a) => Int -> Int -> a
replicateOne Int
5 Int
11 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
0o70000700000
   in  \(Cons Word32
bits) ->
       Word32 -> T (P10 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P10 Zero)) -> Word32 -> T (P10 Zero)
forall a b. (a -> b) -> a -> b
$
       if Word32
bits Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
full
         then Word32
full
         else
            Integer -> Word32
forall a. Num a => Integer -> a
fromInteger (Integer -> Word32) -> Integer -> Word32
forall a b. (a -> b) -> a -> b
$
            Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod ((Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
bits Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
spread) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
revMask) (Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
full)
{-
         jihgfedcba

...abcde fghij00abc defghij00a bcdefghij0
     ^     ^     ^     ^     ^     ^
-}

reverse10splitSpread :: T N10 -> T N10
reverse10splitSpread :: T (P10 Zero) -> T (P10 Zero)
reverse10splitSpread (Cons Word32
bits) =
   Word32 -> T (P10 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P10 Zero)) -> Word32 -> T (P10 Zero)
forall a b. (a -> b) -> a -> b
$
      Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftL
         (T (P5 Zero) -> Word32
forall w. T w -> Word32
decons (T (P5 Zero) -> Word32) -> T (P5 Zero) -> Word32
forall a b. (a -> b) -> a -> b
$ T (P5 Zero) -> T (P5 Zero)
reverse5spread (T (P5 Zero) -> T (P5 Zero)) -> T (P5 Zero) -> T (P5 Zero)
forall a b. (a -> b) -> a -> b
$ Word32 -> T (P5 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P5 Zero)) -> Word32 -> T (P5 Zero)
forall a b. (a -> b) -> a -> b
$ Word32
bits Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
0o77777) (Int
5Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
bitsPerNumber)
      Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.|.
      (T (P5 Zero) -> Word32
forall w. T w -> Word32
decons (T (P5 Zero) -> Word32) -> T (P5 Zero) -> Word32
forall a b. (a -> b) -> a -> b
$ T (P5 Zero) -> T (P5 Zero)
reverse5spread (T (P5 Zero) -> T (P5 Zero)) -> T (P5 Zero) -> T (P5 Zero)
forall a b. (a -> b) -> a -> b
$ Word32 -> T (P5 Zero)
forall w. Word32 -> T w
Cons (Word32 -> T (P5 Zero)) -> Word32 -> T (P5 Zero)
forall a b. (a -> b) -> a -> b
$ Word32 -> Int -> Word32
forall a. Bits a => a -> Int -> a
shiftR Word32
bits (Int
5Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
bitsPerNumber))


{-# INLINE multiMask #-}
multiMask :: (Bits a, Integral a) => Int -> a
multiMask :: Int -> a
multiMask Int
n = a -> Int -> a
forall a. Bits a => a -> Int -> a
shiftL a
1 (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
bitsPerNumber) a -> a -> a
forall a. Num a => a -> a -> a
- a
1

{-# INLINE replicateOne #-}
replicateOne :: (Bits a, Integral a) => Int -> Int -> a
replicateOne :: Int -> Int -> a
replicateOne Int
n Int
k = Int -> a
forall a. (Bits a, Integral a) => Int -> a
multiMask (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
k) a -> a -> a
forall a. Integral a => a -> a -> a
`div` Int -> a
forall a. (Bits a, Integral a) => Int -> a
multiMask Int
k



cons :: Size w -> Word32 -> T w
cons :: Size w -> Word32 -> T w
cons (Size Int
width) Word32
bits = Word32 -> T w
forall w. Word32 -> T w
Cons (Word32 -> T w) -> Word32 -> T w
forall a b. (a -> b) -> a -> b
$ Int -> Word32
forall a. (Bits a, Integral a) => Int -> a
multiMask Int
width Word32 -> Word32 -> Word32
forall a. Bits a => a -> a -> a
.&. Word32
bits

instance (Nat w) => QC.Arbitrary (T w) where
   arbitrary :: Gen (T w)
arbitrary = Size w -> Word32 -> T w
forall w. Size w -> Word32 -> T w
cons Size w
forall n. Nat n => Size n
Size.size (Word32 -> T w) -> Gen Word32 -> Gen (T w)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word32, Word32) -> Gen Word32
forall a. Random a => (a, a) -> Gen a
QC.choose (Word32
forall a. Bounded a => a
minBound, Word32
forall a. Bounded a => a
maxBound)
   shrink :: T w -> [T w]
shrink = (Word32 -> T w) -> [Word32] -> [T w]
forall a b. (a -> b) -> [a] -> [b]
map (Size w -> Word32 -> T w
forall w. Size w -> Word32 -> T w
cons Size w
forall n. Nat n => Size n
Size.size) ([Word32] -> [T w]) -> (T w -> [Word32]) -> T w -> [T w]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> [Word32]
forall a. Arbitrary a => a -> [a]
QC.shrink (Word32 -> [Word32]) -> (T w -> Word32) -> T w -> [Word32]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T w -> Word32
forall w. T w -> Word32
decons

propReverse4 :: T N4 -> Bool
propReverse4 :: T (P4 Zero) -> Bool
propReverse4 T (P4 Zero)
frontier =
   Size (P4 Zero) -> T (P4 Zero) -> T (P4 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P4 Zero)
forall n. Nat n => Size n
Size.size T (P4 Zero)
frontier T (P4 Zero) -> T (P4 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P4 Zero) -> T (P4 Zero)
reverse4spread T (P4 Zero)
frontier

propReverse5 :: T N5 -> Bool
propReverse5 :: T (P5 Zero) -> Bool
propReverse5 T (P5 Zero)
frontier =
   Size (P5 Zero) -> T (P5 Zero) -> T (P5 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P5 Zero)
forall n. Nat n => Size n
Size.size T (P5 Zero)
frontier T (P5 Zero) -> T (P5 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P5 Zero) -> T (P5 Zero)
reverse5spread T (P5 Zero)
frontier

propReverse6 :: T N6 -> Bool
propReverse6 :: T (P6 Zero) -> Bool
propReverse6 T (P6 Zero)
frontier =
   Size (P6 Zero) -> T (P6 Zero) -> T (P6 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P6 Zero)
forall n. Nat n => Size n
Size.size T (P6 Zero)
frontier T (P6 Zero) -> T (P6 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P6 Zero) -> T (P6 Zero)
reverse6up T (P6 Zero)
frontier

propReverse7 :: T N7 -> Bool
propReverse7 :: T (P7 Zero) -> Bool
propReverse7 T (P7 Zero)
frontier =
   Size (P7 Zero) -> T (P7 Zero) -> T (P7 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P7 Zero)
forall n. Nat n => Size n
Size.size T (P7 Zero)
frontier T (P7 Zero) -> T (P7 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P7 Zero) -> T (P7 Zero)
reverse7up T (P7 Zero)
frontier

propReverse8 :: T N8 -> Bool
propReverse8 :: T (P8 Zero) -> Bool
propReverse8 T (P8 Zero)
frontier =
   Size (P8 Zero) -> T (P8 Zero) -> T (P8 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P8 Zero)
forall n. Nat n => Size n
Size.size T (P8 Zero)
frontier T (P8 Zero) -> T (P8 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P8 Zero) -> T (P8 Zero)
reverse8up T (P8 Zero)
frontier

propReverse9 :: T N9 -> Bool
propReverse9 :: T (P9 Zero) -> Bool
propReverse9 T (P9 Zero)
frontier =
   Size (P9 Zero) -> T (P9 Zero) -> T (P9 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P9 Zero)
forall n. Nat n => Size n
Size.size T (P9 Zero)
frontier T (P9 Zero) -> T (P9 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P9 Zero) -> T (P9 Zero)
reverse9up T (P9 Zero)
frontier

propReverse10 :: T N10 -> Bool
propReverse10 :: T (P10 Zero) -> Bool
propReverse10 T (P10 Zero)
frontier =
   Size (P10 Zero) -> T (P10 Zero) -> T (P10 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P10 Zero)
forall n. Nat n => Size n
Size.size T (P10 Zero)
frontier T (P10 Zero) -> T (P10 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P10 Zero) -> T (P10 Zero)
reverse10up T (P10 Zero)
frontier Bool -> Bool -> Bool
&&
   Size (P10 Zero) -> T (P10 Zero) -> T (P10 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P10 Zero)
forall n. Nat n => Size n
Size.size T (P10 Zero)
frontier T (P10 Zero) -> T (P10 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P10 Zero) -> T (P10 Zero)
reverse10down T (P10 Zero)
frontier Bool -> Bool -> Bool
&&
   Size (P10 Zero) -> T (P10 Zero) -> T (P10 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P10 Zero)
forall n. Nat n => Size n
Size.size T (P10 Zero)
frontier T (P10 Zero) -> T (P10 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P10 Zero) -> T (P10 Zero)
reverse10spread T (P10 Zero)
frontier Bool -> Bool -> Bool
&&
   Size (P10 Zero) -> T (P10 Zero) -> T (P10 Zero)
forall w. Size w -> T w -> T w
reverseGen Size (P10 Zero)
forall n. Nat n => Size n
Size.size T (P10 Zero)
frontier T (P10 Zero) -> T (P10 Zero) -> Bool
forall a. Eq a => a -> a -> Bool
== T (P10 Zero) -> T (P10 Zero)
reverse10splitSpread T (P10 Zero)
frontier

-- too big for Word32
_propReverse11 :: T N11 -> Bool
_propReverse11 :: T N11 -> Bool
_propReverse11 T N11
frontier =
   Size N11 -> T N11 -> T N11
forall w. Size w -> T w -> T w
reverseGen Size N11
forall n. Nat n => Size n
Size.size T N11
frontier T N11 -> T N11 -> Bool
forall a. Eq a => a -> a -> Bool
== T N11 -> T N11
reverse11up T N11
frontier