{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{- |
Module      : Data.Pos
Description : positive numbers
Copyright   : (c) Grant Weyburne, 2022
License     : BSD-3
-}
module Data.Pos (
  -- ** core type
  Pos,

  -- ** destructors
  pattern Pos,
  unP,

  -- ** constructors
  _P,
  unsafePos,
  eitherPos,

  -- ** values
  _1P,
  _2P,
  _3P,
  _4P,
  _5P,
  _6P,
  _7P,
  _8P,
  _9P,
  _10P,
  _11P,
  _12P,
  _13P,
  _14P,
  _15P,
  _16P,
  _17P,
  _18P,
  _19P,
  _20P,

  -- ** arithmetic
  (*!),
  (+!),
  minusP,
  productP,
  productPInt,
  safeDivP,
  divModP,
  divModNextP,
  maxP,
  predP,
  succP,

  -- ** type level
  PosC (..),
  NS (..),

  -- ** miscellaneous
  fromPositives,
  toPositives,
  posRange,

  -- * parsers
  pPositives,
  pPos,
  pPosInt,
  pInt,
) where

import Control.Applicative
import Control.Arrow
import Control.DeepSeq
import Data.Char
import Data.Foldable
import Data.Function
import Data.Kind
import qualified Data.List as L
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as N
import Data.Proxy
import GHC.Enum
import GHC.Natural
import GHC.Read (readPrec)
import GHC.Stack
import GHC.TypeLits (KnownNat, Nat)
import qualified GHC.TypeLits as GL
import qualified Text.ParserCombinators.ReadP as P
import qualified Text.ParserCombinators.ReadPrec as PC
import Text.Read (readMaybe)

-- | holds a positive number
newtype Pos = Pos' Int
  deriving stock (Pos -> Pos -> Bool
(Pos -> Pos -> Bool) -> (Pos -> Pos -> Bool) -> Eq Pos
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pos -> Pos -> Bool
$c/= :: Pos -> Pos -> Bool
== :: Pos -> Pos -> Bool
$c== :: Pos -> Pos -> Bool
Eq, Eq Pos
Eq Pos
-> (Pos -> Pos -> Ordering)
-> (Pos -> Pos -> Bool)
-> (Pos -> Pos -> Bool)
-> (Pos -> Pos -> Bool)
-> (Pos -> Pos -> Bool)
-> (Pos -> Pos -> Pos)
-> (Pos -> Pos -> Pos)
-> Ord Pos
Pos -> Pos -> Bool
Pos -> Pos -> Ordering
Pos -> Pos -> Pos
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
min :: Pos -> Pos -> Pos
$cmin :: Pos -> Pos -> Pos
max :: Pos -> Pos -> Pos
$cmax :: Pos -> Pos -> Pos
>= :: Pos -> Pos -> Bool
$c>= :: Pos -> Pos -> Bool
> :: Pos -> Pos -> Bool
$c> :: Pos -> Pos -> Bool
<= :: Pos -> Pos -> Bool
$c<= :: Pos -> Pos -> Bool
< :: Pos -> Pos -> Bool
$c< :: Pos -> Pos -> Bool
compare :: Pos -> Pos -> Ordering
$ccompare :: Pos -> Pos -> Ordering
$cp1Ord :: Eq Pos
Ord)
  deriving newtype (Pos -> ()
(Pos -> ()) -> NFData Pos
forall a. (a -> ()) -> NFData a
rnf :: Pos -> ()
$crnf :: Pos -> ()
NFData)

instance Show Pos where
  showsPrec :: Int -> Pos -> ShowS
showsPrec Int
_ (Pos Int
i) = Char -> ShowS
showChar Char
'_' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Int
i ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
'P'

-- | readonly pattern synonym for 'Pos'
{-# COMPLETE Pos #-}

pattern Pos :: Int -> Pos
pattern $mPos :: forall r. Pos -> (Int -> r) -> (Void# -> r) -> r
Pos n <- Pos' n

-- | parser for an 'Int'
pInt :: P.ReadP Int
pInt :: ReadP Int
pInt = do
  String
ii <- ReadP Char -> ReadP String
forall a. ReadP a -> ReadP [a]
P.many1 ((Char -> Bool) -> ReadP Char
P.satisfy Char -> Bool
isDigit)
  ReadP Int -> (Int -> ReadP Int) -> Maybe Int -> ReadP Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReadP Int
forall a. ReadP a
P.pfail Int -> ReadP Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe @Int String
ii)

-- | parser for a 'Pos'
pPos :: P.ReadP Pos
pPos :: ReadP Pos
pPos = ReadP ()
P.skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ReadP Char
P.char Char
'_' ReadP Char -> ReadP Pos -> ReadP Pos
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReadP Pos
pPosInt' ReadP Pos -> ReadP Char -> ReadP Pos
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> ReadP Char
P.char Char
'P'

-- | parser for a 'Pos' but just reading in a positive number
pPosInt :: P.ReadP Pos
pPosInt :: ReadP Pos
pPosInt = ReadP ()
P.skipSpaces ReadP () -> ReadP Pos -> ReadP Pos
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReadP Pos
pPosInt'

-- | parser for an int converted positive number
pPosInt' :: P.ReadP Pos
pPosInt' :: ReadP Pos
pPosInt' = do
  Int
i <- ReadP Int
pInt
  (String -> ReadP Pos)
-> (Pos -> ReadP Pos) -> Either String Pos -> ReadP Pos
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (ReadP Pos -> String -> ReadP Pos
forall a b. a -> b -> a
const ReadP Pos
forall (f :: * -> *) a. Alternative f => f a
empty) Pos -> ReadP Pos
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Either String Pos
eitherPos Int
i)

-- | parser for a list of positive numbers as ints
pPositives :: Char -> Char -> P.ReadP (NonEmpty Pos)
pPositives :: Char -> Char -> ReadP (NonEmpty Pos)
pPositives Char
o Char
c = do
  [Pos]
xs <- Char -> ReadP Char
P.char Char
o ReadP Char -> ReadP [Pos] -> ReadP [Pos]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ReadP Pos -> ReadP Char -> ReadP [Pos]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
P.sepBy1 ReadP Pos
pPosInt (Char -> ReadP Char
P.char Char
',') ReadP [Pos] -> ReadP Char -> ReadP [Pos]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> ReadP Char
P.char Char
c
  case [Pos]
xs of
    [] -> String -> ReadP (NonEmpty Pos)
forall a. HasCallStack => String -> a
error String
"pPositives: empty" -- should not fail
    Pos
a : [Pos]
as -> NonEmpty Pos -> ReadP (NonEmpty Pos)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pos
a Pos -> [Pos] -> NonEmpty Pos
forall a. a -> [a] -> NonEmpty a
:| [Pos]
as)

instance Read Pos where
  readPrec :: ReadPrec Pos
readPrec = (Int -> ReadP Pos) -> ReadPrec Pos
forall a. (Int -> ReadP a) -> ReadPrec a
PC.readP_to_Prec (ReadP Pos -> Int -> ReadP Pos
forall a b. a -> b -> a
const ReadP Pos
pPos)

-- | unwrap 'Pos'
unP :: Pos -> Int
unP :: Pos -> Int
unP (Pos Int
i) = Int
i
{-# INLINE unP #-}

-- | 'Enum' instance for 'Pos'
instance Enum Pos where
  pred :: Pos -> Pos
pred (Pos Int
i) = HasCallStack => String -> Int -> Pos
String -> Int -> Pos
unsafePos String
"Enum.pred" (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  toEnum :: Int -> Pos
toEnum = HasCallStack => String -> Int -> Pos
String -> Int -> Pos
unsafePos String
"Enum.toEnum"
  fromEnum :: Pos -> Int
fromEnum (Pos Int
i) = Int
i
  enumFrom :: Pos -> [Pos]
enumFrom = Pos -> [Pos]
forall a. (Enum a, Bounded a) => a -> [a]
boundedEnumFrom
  enumFromThen :: Pos -> Pos -> [Pos]
enumFromThen = Pos -> Pos -> [Pos]
forall a. (Enum a, Bounded a) => a -> a -> [a]
boundedEnumFromThen

instance Bounded Pos where
  minBound :: Pos
minBound = Pos
_1P
  maxBound :: Pos
maxBound = Int -> Pos
Pos' Int
forall a. Bounded a => a
maxBound

infixl 7 *!

-- | multiply two positive numbers
(*!) :: Pos -> Pos -> Pos
Pos Int
a *! :: Pos -> Pos -> Pos
*! Pos Int
b = Int -> Pos
Pos' (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
b)
{-# INLINE (*!) #-}

infixl 6 +!

-- | add two positive numbers
(+!) :: Pos -> Pos -> Pos
Pos Int
a +! :: Pos -> Pos -> Pos
+! Pos Int
b = Int -> Pos
Pos' (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b)
{-# INLINE (+!) #-}

-- | subtract two positive numbers
minusP :: Pos -> Pos -> Either String Pos
minusP :: Pos -> Pos -> Either String Pos
minusP = (Int -> Either String Pos
eitherPos (Int -> Either String Pos)
-> (Pos -> Int) -> Pos -> Either String Pos
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Pos -> Int) -> Pos -> Either String Pos)
-> (Pos -> Pos -> Int) -> Pos -> Pos -> Either String Pos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int) -> (Pos -> Int) -> Pos -> Pos -> Int
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on (-) Pos -> Int
unP

-- | try to convert an 'Int' to a 'Pos'
unsafePos :: HasCallStack => String -> Int -> Pos
unsafePos :: String -> Int -> Pos
unsafePos String
msg Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 = Int -> Pos
Pos' Int
i
  | Bool
otherwise = String -> Pos
forall a. HasCallStack => String -> a
error (String -> Pos) -> String -> Pos
forall a b. (a -> b) -> a -> b
$ String
"unsafePos:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" cannot be less than 1 found " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
{-# INLINE unsafePos #-}

-- | try to convert an 'Int' to a 'Pos'
eitherPos :: Int -> Either String Pos
eitherPos :: Int -> Either String Pos
eitherPos Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> Either String Pos
forall a b. a -> Either a b
Left (String -> Either String Pos) -> String -> Either String Pos
forall a b. (a -> b) -> a -> b
$ String
"eitherPos: i<=0: found " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  | Bool
otherwise = Pos -> Either String Pos
forall a b. b -> Either a b
Right (Int -> Pos
Pos' Int
i)
{-# INLINE eitherPos #-}

-- mod is always between 1 and N

-- | 'divMod' for 'Pos'
divModNextP :: Int -> Pos -> (Int, Pos)
divModNextP :: Int -> Pos -> (Int, Pos)
divModNextP Int
i (Pos Int
j) = (Int -> Pos) -> (Int, Int) -> (Int, Pos)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (\Int
n -> Int -> Pos
Pos' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) (Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
i Int
j)
{-# INLINE divModNextP #-}

-- | 'divMod' for 'Pos' returning 'Natural' for the remainder
divModP :: Int -> Pos -> (Int, Natural) -- second Int is always >= 0
divModP :: Int -> Pos -> (Int, Natural)
divModP Int
i (Pos Int
n) = (Int -> Natural) -> (Int, Int) -> (Int, Natural)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Int -> Natural
forall a. Enum a => Int -> a
toEnum (Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
divMod Int
i Int
n) -- works fine
{-# INLINE divModP #-}

-- adds 1 to any division! this is useful for chunks where there is usually a remainder: also guarantees that Pos is valid

-- | safely divide 'Pos' values but the result is increased by one to guarantee the result is still positive
safeDivP :: Pos -> Pos -> Pos -- have to completely spell it out! else liquid gets confused
safeDivP :: Pos -> Pos -> Pos
safeDivP (Pos Int
i) (Pos Int
j) = Int -> Pos
Pos' (Int -> Int -> Int
forall a. Integral a => a -> a -> a
mod Int
i Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
{-# INLINE safeDivP #-}

-- | product of list of 'Pos' values is always positive
productP :: Foldable t => t Pos -> Pos
productP :: t Pos -> Pos
productP = (Pos -> Pos -> Pos) -> Pos -> t Pos -> Pos
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Pos -> Pos -> Pos
(*!) Pos
_1P
{-# INLINE productP #-}

-- | product of list of 'Pos' values is always positive
productPInt :: Foldable t => t Pos -> Int
productPInt :: t Pos -> Int
productPInt = Pos -> Int
unP (Pos -> Int) -> (t Pos -> Pos) -> t Pos -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t Pos -> Pos
forall (t :: * -> *). Foldable t => t Pos -> Pos
productP
{-# INLINE productPInt #-}

-- | max of a 'Pos' and an 'Int'
maxP :: Pos -> Int -> Pos
maxP :: Pos -> Int -> Pos
maxP (Pos Int
n) Int
i = Int -> Pos
Pos' (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n Int
i)
{-# INLINE maxP #-}

-- | next value for 'Pos' (not redundant as it is always successful and never partial)
succP :: Pos -> Pos
succP :: Pos -> Pos
succP (Pos Int
n) = Int -> Pos
Pos' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
{-# INLINE succP #-}

-- | previous value for 'Pos'
predP :: Pos -> Either String Pos
predP :: Pos -> Either String Pos
predP (Pos Int
n) = Int -> Either String Pos
eitherPos (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
{-# INLINE predP #-}

-- | extract an 'Int' from a 'Nat'
pnat :: forall n. GL.KnownNat n => Int
pnat :: Int
pnat = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
GL.natVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n))

-- | constraint for positive numbers
type PosC :: Nat -> Constraint
class KnownNat n => PosC n where
  fromNP :: Pos
  fromN :: Int
  fromN = Pos -> Int
unP (PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n)
instance
  ( KnownNat n
  , FailUnless
      (1 GL.<=? n)
      ( 'GL.Text "PosC n: requires n >= 1 but found "
          'GL.:<>: 'GL.ShowType n
      )
  ) =>
  PosC n
  where
  fromNP :: Pos
fromNP = HasCallStack => String -> Int -> Pos
String -> Int -> Pos
unsafePos String
"fromN" (KnownNat n => Int
forall (n :: Nat). KnownNat n => Int
pnat @n)

type FailUnless :: Bool -> GL.ErrorMessage -> Constraint
type family FailUnless b err where
  FailUnless 'False err = GL.TypeError ( 'GL.Text "FailUnless: " 'GL.:<>: err)
  FailUnless 'True _ = ()

-- | conversion from list of Nats to Positives
type NS :: [Nat] -> Constraint
class NS ns where
  fromNSP :: NonEmpty Pos
  fromNSTotalP :: Pos
  fromNSTotalP = NonEmpty Pos -> Pos
forall (t :: * -> *). Foldable t => t Pos -> Pos
productP (NS ns => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @ns)
  nsLengthP :: Pos

instance GL.TypeError ( 'GL.Text "NS: empty dimensions are not supported") => NS '[] where
  fromNSP :: NonEmpty Pos
fromNSP = String -> NonEmpty Pos
forall a. HasCallStack => String -> a
error String
"fromNSP: should not be here"
  nsLengthP :: Pos
nsLengthP = String -> Pos
forall a. HasCallStack => String -> a
error String
"fromNSP: should not be here"
instance PosC n => NS '[n] where
  fromNSP :: NonEmpty Pos
fromNSP = PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n Pos -> [Pos] -> NonEmpty Pos
forall a. a -> [a] -> NonEmpty a
:| []
  nsLengthP :: Pos
nsLengthP = Pos
_1P
instance (PosC n, NS (n1 ': ns)) => NS (n ': n1 ': ns) where
  fromNSP :: NonEmpty Pos
fromNSP = PosC n => Pos
forall (n :: Nat). PosC n => Pos
fromNP @n Pos -> NonEmpty Pos -> NonEmpty Pos
forall a. a -> NonEmpty a -> NonEmpty a
N.<| NS (n1 : ns) => NonEmpty Pos
forall (ns :: [Nat]). NS ns => NonEmpty Pos
fromNSP @(n1 ': ns)
  nsLengthP :: Pos
nsLengthP = Pos -> Pos
succP (NS (n1 : ns) => Pos
forall (ns :: [Nat]). NS ns => Pos
nsLengthP @(n1 ': ns))

-- | construct a valid 'Pos' using a 'Nat'
_P :: forall n. PosC n => Pos
_P :: Pos
_P = Int -> Pos
Pos' (KnownNat n => Int
forall (n :: Nat). KnownNat n => Int
pnat @n)

-- | converts a container of positives to a list of ints
fromPositives :: Foldable t => t Pos -> [Int]
fromPositives :: t Pos -> [Int]
fromPositives = (Pos -> [Int] -> [Int]) -> [Int] -> t Pos -> [Int]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (Int -> [Int] -> [Int]) -> (Pos -> Int) -> Pos -> [Int] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pos -> Int
unP) []

-- | converts a list of ints to a nonempty list of positives
toPositives :: Foldable t => t Int -> Either String (NonEmpty Pos)
toPositives :: t Int -> Either String (NonEmpty Pos)
toPositives t Int
is = do
  [Pos]
ps <- (Int -> Either String Pos) -> [Int] -> Either String [Pos]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Int -> Either String Pos
eitherPos (t Int -> [Int]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t Int
is)
  case [Pos]
ps of
    [] -> String -> Either String (NonEmpty Pos)
forall a b. a -> Either a b
Left String
"toPositives: empty"
    Pos
x : [Pos]
xs -> NonEmpty Pos -> Either String (NonEmpty Pos)
forall a b. b -> Either a b
Right (Pos
x Pos -> [Pos] -> NonEmpty Pos
forall a. a -> [a] -> NonEmpty a
:| [Pos]
xs)

-- | enumerate a nonempty list of 'Pos' from "i" to "j"
posRange :: Int -> Int -> Either String (NonEmpty Pos)
posRange :: Int -> Int -> Either String (NonEmpty Pos)
posRange Int
i Int
j = do
  Pos
i' <- Int -> Either String Pos
eitherPos Int
i
  Pos
j' <- Int -> Either String Pos
eitherPos Int
j
  case [Pos
i' .. Pos
j'] of
    [] -> String -> Either String (NonEmpty Pos)
forall a b. a -> Either a b
Left (String -> Either String (NonEmpty Pos))
-> String -> Either String (NonEmpty Pos)
forall a b. (a -> b) -> a -> b
$ String
"posRange: no values between " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Pos -> Int
unP Pos
i') String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Pos -> Int
unP Pos
j')
    Pos
a : [Pos]
as -> NonEmpty Pos -> Either String (NonEmpty Pos)
forall a b. b -> Either a b
Right (Pos
a Pos -> [Pos] -> NonEmpty Pos
forall a. a -> [a] -> NonEmpty a
:| [Pos]
as)

-- | commonly used values for 'Pos'
_1P, _2P, _3P, _4P, _5P, _6P, _7P, _8P, _9P, _10P, _11P, _12P, _13P, _14P, _15P, _16P, _17P, _18P, _19P, _20P :: Pos
_1P :: Pos
_1P = Int -> Pos
Pos' Int
1
_2P :: Pos
_2P = Int -> Pos
Pos' Int
2
_3P :: Pos
_3P = Int -> Pos
Pos' Int
3
_4P :: Pos
_4P = Int -> Pos
Pos' Int
4
_5P :: Pos
_5P = Int -> Pos
Pos' Int
5
_6P :: Pos
_6P = Int -> Pos
Pos' Int
6
_7P :: Pos
_7P = Int -> Pos
Pos' Int
7
_8P :: Pos
_8P = Int -> Pos
Pos' Int
8
_9P :: Pos
_9P = Int -> Pos
Pos' Int
9
_10P :: Pos
_10P = Int -> Pos
Pos' Int
10
_11P :: Pos
_11P = Int -> Pos
Pos' Int
11
_12P :: Pos
_12P = Int -> Pos
Pos' Int
12
_13P :: Pos
_13P = Int -> Pos
Pos' Int
13
_14P :: Pos
_14P = Int -> Pos
Pos' Int
14
_15P :: Pos
_15P = Int -> Pos
Pos' Int
15
_16P :: Pos
_16P = Int -> Pos
Pos' Int
16
_17P :: Pos
_17P = Int -> Pos
Pos' Int
17
_18P :: Pos
_18P = Int -> Pos
Pos' Int
18
_19P :: Pos
_19P = Int -> Pos
Pos' Int
19
_20P :: Pos
_20P = Int -> Pos
Pos' Int
20