pos (empty) → 0.1.0.0
raw patch · 4 files changed
+525/−0 lines, 4 filesdep +basedep +deepseqdep +pos
Dependencies added: base, deepseq, pos, tasty, tasty-hunit
Files
- LICENSE +29/−0
- pos.cabal +52/−0
- src/Data/Pos.hs +341/−0
- test/Main.hs +103/−0
+ LICENSE view
@@ -0,0 +1,29 @@+BSD 3-Clause License + +Copyright (c) 2018, Grant Weyburne +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ pos.cabal view
@@ -0,0 +1,52 @@+cabal-version: 1.12 ++-- This file has been generated from package.yaml by hpack version 0.34.4.+--+-- see: https://github.com/sol/hpack++name: pos+version: 0.1.0.0+synopsis: positive numbers+description: A library for representing positive integers. . Useful for handling nonempty containers and fixed containers.+category: Data, Numeric+homepage: https://github.com/gbwey/pos#readme+bug-reports: https://github.com/gbwey/pos.git/issues+author: Grant Weyburne <gbwey9@gmail.com>+maintainer: Grant Weyburne <gbwey9@gmail.com>+copyright: 2022 Grant Weyburne+license: BSD3+license-file: LICENSE+build-type: Simple++source-repository head+ type: git+ location: https://github.com/gbwey/pos.git++library+ exposed-modules:+ Data.Pos+ other-modules:+ Paths_pos+ hs-source-dirs:+ src+ ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wunused-type-patterns -Wredundant-constraints -Wmonomorphism-restriction -Wmissing-deriving-strategies -Wmissing-local-signatures -Wmissing-export-lists -Widentities+ build-depends:+ base >=4.7 && <5+ , deepseq+ default-language: Haskell2010++test-suite pos-test+ type: exitcode-stdio-1.0+ main-is: Main.hs+ other-modules:+ Paths_pos+ hs-source-dirs:+ test+ ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wunused-type-patterns -Wredundant-constraints -Wmissing-deriving-strategies -Widentities -Wno-missing-export-lists -Wno-missing-local-signatures+ build-depends:+ base+ , deepseq+ , pos+ , tasty+ , tasty-hunit+ default-language: Haskell2010
+ src/Data/Pos.hs view
@@ -0,0 +1,341 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# 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,++ -- ** enums+ predP,+ succP,+ posRange,++ -- ** type level+ type PosT,+ fromN,+ fromNP,+ NSC (..),++ -- ** miscellaneous++ -- _Pos,+ fromPositives,+ toPositives,++ -- * 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 (Eq, Ord)+ deriving newtype (NFData)++instance Show Pos where+ showsPrec _ (Pos i) = showsPrec 11 i . showChar 'P'++-- | readonly pattern synonym for 'Pos'+{-# COMPLETE Pos #-}++pattern Pos :: Int -> Pos+pattern Pos n <- Pos' n++-- | parser for an 'Int'+pInt :: P.ReadP Int+pInt = do+ P.skipSpaces+ ii <- P.many1 (P.satisfy isDigit)+ maybe P.pfail pure (readMaybe @Int ii)++-- | parser for a 'Pos'+pPos :: P.ReadP Pos+pPos = pPosInt <* P.char 'P'++-- | parser for an int converted positive number+pPosInt :: P.ReadP Pos+pPosInt = do+ i <- pInt+ either (const empty) return (eitherPos i)++-- | parser for a list of positive numbers as ints+pPositives :: Char -> Char -> P.ReadP (NonEmpty Pos)+pPositives o c = do+ xs <- P.char o *> P.sepBy1 pPosInt (P.char ',') <* P.char c+ case xs of+ [] -> error "pPositives: empty" -- should not fail+ a : as -> pure (a :| as)++instance Read Pos where+ readPrec = PC.readP_to_Prec (const pPos)++-- | unwrap 'Pos'+unP :: Pos -> Int+unP (Pos i) = i+{-# INLINE unP #-}++-- | 'Enum' instance for 'Pos'+instance Enum Pos where+ pred (Pos i) = unsafePos "Enum.pred" (i - 1)+ toEnum = unsafePos "Enum.toEnum"+ fromEnum (Pos i) = i+ enumFrom = boundedEnumFrom+ enumFromThen = boundedEnumFromThen++instance Bounded Pos where+ minBound = _1P+ maxBound = Pos' maxBound++infixl 7 *!++-- | multiply two positive numbers+(*!) :: Pos -> Pos -> Pos+Pos a *! Pos b = Pos' (a * b)+{-# INLINE (*!) #-}++infixl 6 +!++-- | add two positive numbers+(+!) :: Pos -> Pos -> Pos+Pos a +! Pos b = Pos' (a + b)+{-# INLINE (+!) #-}++-- | subtract two positive numbers+minusP :: Pos -> Pos -> Either String Pos+minusP = (eitherPos .) . on (-) unP++-- | try to convert an 'Int' to a 'Pos'+unsafePos :: HasCallStack => String -> Int -> Pos+unsafePos msg i+ | i >= 1 = Pos' i+ | otherwise = error $ "unsafePos:" ++ msg ++ " cannot be less than 1 found " ++ show i+{-# INLINE unsafePos #-}++-- | try to convert an 'Int' to a 'Pos'+eitherPos :: Int -> Either String Pos+eitherPos i+ | i <= 0 = Left $ "eitherPos: i<=0: found " ++ show i+ | otherwise = Right (Pos' i)+{-# INLINE eitherPos #-}++-- mod is always between 1 and N++-- | 'divMod' for 'Pos'+divModNextP :: Int -> Pos -> (Int, Pos)+divModNextP i (Pos j) = second (\n -> Pos' (n + 1)) (divMod i j)+{-# INLINE divModNextP #-}++-- | 'divMod' for 'Pos' returning 'Natural' for the remainder+divModP :: Int -> Pos -> (Int, Natural) -- second Int is always >= 0+divModP i (Pos n) = second toEnum (divMod i 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 i) (Pos j) = Pos' (mod i j + 1)+{-# INLINE safeDivP #-}++-- | product of list of 'Pos' values is always positive+productP :: Foldable t => t Pos -> Pos+productP = L.foldl' (*!) _1P+{-# INLINE productP #-}++-- | product of list of 'Pos' values is always positive+productPInt :: Foldable t => t Pos -> Int+productPInt = unP . productP+{-# INLINE productPInt #-}++-- | max of a 'Pos' and an 'Int'+maxP :: Pos -> Int -> Pos+maxP (Pos n) i = Pos' (max n i)+{-# INLINE maxP #-}++-- | next value for 'Pos' (not redundant as it is always successful and never partial)+succP :: Pos -> Pos+succP (Pos n) = Pos' (n + 1)+{-# INLINE succP #-}++-- | previous value for 'Pos'+predP :: Pos -> Either String Pos+predP (Pos n) = eitherPos (n - 1)+{-# INLINE predP #-}++-- | converts a restricted (positive) 'Nat' to an 'Int'+fromN :: forall n. PosT n => Int+fromN = pnat @n+{-# INLINE fromN #-}++-- | converts a 'Nat' to a 'Pos'+fromNP :: forall n. PosT n => Pos+fromNP = case eitherPos $ pnat @n of+ Left e -> error $ "fromNP:" ++ e -- shouldnt fail because of PosT constraint+ Right p -> p+{-# INLINE fromNP #-}++-- | extract an 'Int' from a 'Nat'+pnat :: forall n. GL.KnownNat n => Int+pnat = fromInteger (GL.natVal (Proxy @n))++-- | constraint that limits to positive 'Nat'+type PosT :: Nat -> Constraint+type PosT n =+ ( KnownNat n+ , FailUnless+ (1 GL.<=? n)+ ( 'GL.Text "PosT n: requires n >= 1 but found "+ 'GL.:<>: 'GL.ShowType 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 nonempty list of Nats to Positives+type NSC :: NonEmpty Nat -> Constraint+class NSC ns where+ fromNSP :: NonEmpty Pos+ fromNSTotalP :: Pos+ fromNSTotalP = productP (fromNSP @ns)+ nsLengthP :: Pos++instance PosT n => NSC (n ':| '[]) where+ fromNSP = fromNP @n :| []+ nsLengthP = _1P+instance (PosT n, NSC (n1 ':| ns)) => NSC (n ':| n1 ': ns) where+ fromNSP = fromNP @n N.<| fromNSP @(n1 ':| ns)+ nsLengthP = succP (nsLengthP @(n1 ':| ns))++-- | construct a valid 'Pos' using a 'Nat'+_P :: forall n. PosT n => Pos+_P = Pos' (pnat @n)++-- | converts a container of positives to a list of ints+fromPositives :: Foldable t => t Pos -> [Int]+fromPositives = foldr ((:) . unP) []++-- | converts a list of ints to a nonempty list of positives+toPositives :: Foldable t => t Int -> Either String (NonEmpty Pos)+toPositives is = do+ ps <- traverse eitherPos (toList is)+ case ps of+ [] -> Left "empty"+ x : xs -> Right (x :| xs)++-- | enumerate a nonempty list of 'Pos' from "i" to "j"+posRange :: Int -> Int -> Either String (NonEmpty Pos)+posRange i j = do+ i' <- eitherPos i+ j' <- eitherPos j+ case [i' .. j'] of+ [] -> Left $ "posRange: no values between " ++ show (unP i') ++ " and " ++ show (unP j')+ a : as -> Right (a :| 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' 1+_2P = Pos' 2+_3P = Pos' 3+_4P = Pos' 4+_5P = Pos' 5+_6P = Pos' 6+_7P = Pos' 7+_8P = Pos' 8+_9P = Pos' 9+_10P = Pos' 10+_11P = Pos' 11+_12P = Pos' 12+_13P = Pos' 13+_14P = Pos' 14+_15P = Pos' 15+_16P = Pos' 16+_17P = Pos' 17+_18P = Pos' 18+_19P = Pos' 19+_20P = Pos' 20
+ test/Main.hs view
@@ -0,0 +1,103 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Main where++import Data.List.NonEmpty (NonEmpty (..))+import Data.Pos+import Test.Tasty+import Test.Tasty.HUnit+import qualified Text.ParserCombinators.ReadP as P++main :: IO ()+main = defaultMain suite++suite :: TestTree+suite =+ testGroup+ "TestPos"+ [ testCase "succP" $ succP _4P @?= _5P+ , testCase "predP" $ predP _4P @?= Right _3P+ , testCase "add" $ (_P @11) +! (_P @23) @?= (_P @34)+ , testCase "enums" $ map unP [_1P, _3P .. _10P] @?= [1, 3 .. 10]+ , testCase "posRange" $ posRange 2 5 @?= Right (_2P :| [_3P, _4P, _5P])+ , testCase "minusP" $ minusP _4P _3P @?= Right _1P+ , testCase "minusP" $ minusP _4P _4P @?= Left "eitherPos: i<=0: found 0"+ , testCase "minusP" $ minusP _4P _7P @?= Left "eitherPos: i<=0: found -3"+ , testCase "fromPositives" $ fromPositives (_4P :| [_7P, _3P, _10P]) @?= [4, 7, 3, 10]+ , testCase "productP" $ productP [] @?= _1P+ , testCase "productP" $ productP (_3P :| [_1P, _5P, _7P]) @?= _P @105+ , testCase "productP" $ productP (_4P :| []) @?= _4P+ , testCase "productP" $ productP [_4P, _5P] @?= _P @20+ , testCase "productP" $ productP [_4P] @?= _4P+ , testCase "read" $ unP (read @Pos "1325P") @?= 1325+ , testCase "read" $ read @Pos "1325P" @?= _P @1325+ , testCase "show" $ show (_P @1325) @?= "1325P"+ , testCase "read/show" $ read @Pos (show (_P @1325)) @?= _P @1325+ , testCase "reads 0" $ reads @Pos "0P" @?= []+ , testCase "reads -4" $ reads @Pos "-4P" @?= []+ , testCase "reads space between" $ reads @Pos " 9 P" @?= []+ , testCase "reads leading spaces and extra" $ reads @Pos " 9P xyz" @?= [(_9P, " xyz")]+ , testCase "reads leading spaces and extra" $ reads @Pos " 123P" @?= [(_P @123, "")]+ , testCase "fromNSP" $ fromNSP @(4 ':| '[]) @?= (_4P :| [])+ , testCase "fromNSP" $ fromNSP @(4 ':| '[6, 3]) @?= (_4P :| [_6P, _3P])+ , testCase "fromNP 1" $ fromNP @1 @?= _1P+ , testCase "fromNP 2" $ fromNP @2 @?= _2P+ , testCase "fromNP 3" $ fromNP @3 @?= _3P+ , testCase "fromNP 4" $ fromNP @4 @?= _4P+ , testCase "fromNP 5" $ fromNP @5 @?= _5P+ , testCase "fromNP 6" $ fromNP @6 @?= _6P+ , testCase "fromNP 7" $ fromNP @7 @?= _7P+ , testCase "fromNP 8" $ fromNP @8 @?= _8P+ , testCase "fromNP 9" $ fromNP @9 @?= _9P+ , testCase "fromNP 10" $ fromNP @10 @?= _10P+ , testCase "fromNP 11" $ fromNP @11 @?= _11P+ , testCase "fromNP 12" $ fromNP @12 @?= _12P+ , testCase "fromNP 13" $ fromNP @13 @?= _13P+ , testCase "fromNP 14" $ fromNP @14 @?= _14P+ , testCase "fromNP 15" $ fromNP @15 @?= _15P+ , testCase "fromNP 16" $ fromNP @16 @?= _16P+ , testCase "fromNP 17" $ fromNP @17 @?= _17P+ , testCase "fromNP 18" $ fromNP @18 @?= _18P+ , testCase "fromNP 19" $ fromNP @19 @?= _19P+ , testCase "fromNP 20" $ fromNP @20 @?= _20P+ , testCase "fromN 4" $ fromN @4 @?= 4+ , testCase "fromN 1" $ fromN @1 @?= 1+ , testCase "fromNSTotalP" $+ fromNSTotalP @(2 ':| '[3, 20])+ @?= _P @120+ , testCase "fromNSP" $+ fromNSP @(2 ':| '[3, 20])+ @?= _2P :| [_3P, _20P]+ , testCase "pPosInt" $+ P.readP_to_S pPosInt " 12xyz"+ @?= [(_1P, "2xyz"), (_12P, "xyz")] -- ambiguous+ , testCase "pPos" $+ P.readP_to_S pPos " 12Pxyz"+ @?= [(_12P, "xyz")]+ , testCase "pPosInt" $+ P.readP_to_S pPosInt " 10xyz"+ @?= [(_1P, "0xyz"), (_10P, "xyz")]+ , testCase "pPosInt" $+ P.readP_to_S pPosInt " 023xyz"+ @?= [(_2P, "3xyz"), (_P @23, "xyz")]+ , testCase "pPos" $+ P.readP_to_S pPos " 12P xyz"+ @?= [(_12P, " xyz")]+ , testCase "readP pPositives" $+ P.readP_to_S ((,) <$> pInt <* P.char '@' <*> pPositives '{' '}') "1444@{1}"+ @?= [((1444, _1P :| []), "")]+ , testCase "readP pPositives" $+ P.readP_to_S ((,) <$> pInt <* P.char '@' <*> pPositives '{' '}') "1444@{1,2}"+ @?= [((1444, _1P :| [_2P]), "")]+ , testCase "readP pPositives" $+ P.readP_to_S ((,) <$> pInt <* P.char '@' <*> pPositives '{' '}') "1444@{1,2,3}"+ @?= [((1444, _1P :| [_2P, _3P]), "")]+ , testCase "readP pPositives" $+ P.readP_to_S ((,) <$> pInt <* P.char '@' <*> pPositives '{' '}') "0@{1,2,3}"+ @?= [((0, _1P :| [_2P, _3P]), "")]+ ]