data-fin-simple (empty) → 0.1.0.0

raw patch · 6 files changed

+243/−0 lines, 6 filesdep +basedep +doctestsetup-changed

Dependencies added: base, doctest

Files

Data/Fin.hs +155/−0
LICENSE +30/−0
README.md +5/−0
Setup.hs +2/−0
data-fin-simple.cabal +39/−0
test/doctest.hs +12/−0

+ Data/Fin.hs view

@@ -0,0 +1,155 @@+{-# LANGUAGE KindSignatures,+             DataKinds,+             StandaloneDeriving,+             TypeOperators,+             TypeFamilies,+             DeriveDataTypeable,+             RankNTypes,+             ScopedTypeVariables,+             FlexibleContexts,+             FlexibleInstances #-}+module Data.Fin (+  Fin (..),+  natToFin, toFin, unsafeToFin, fromFin,+  finZ, finS, finLast,+  absurd,+  weaken, weakenN, strengthen,+  shift,+  finAdd, finAddN,+  finSub, finSubN,+  finMult+  ) where++import GHC.TypeLits+import Data.Proxy+import Data.Typeable+import Unsafe.Coerce++newtype Fin s (n :: Nat) = Fin s+                         deriving (Typeable)++deriving instance Ord s => Ord (Fin s n)+deriving instance Eq s => Eq (Fin s n)+deriving instance Show s => Show (Fin s n)++-- instance (Integral s, KnownNat (n + 1)) => Enum (Fin s (n + 1)) where+--   succ = finS+--   pred x@(Fin x')+--     | x == 0 = x+--     | otherwise = Fin (x - 1)+--  toEnum x = toFin . fromIntegral+--  fromEnum (Fin x) = fromIntegral x++finZ :: (Integral s, KnownNat (n + 1)) => Fin s (n + 1)+finZ = Fin 0+{-# INLINE finZ #-}++finS :: (Integral s, KnownNat n, KnownNat (n + 1)) => Fin s n -> Fin s (n + 1)+finS (Fin x) = Fin x+{-# INLINE finS #-}++-- |+-- >>> (finLast :: Fin Int 5)+-- Fin 4+--+finLast :: forall s n. (Integral s, KnownNat n, KnownNat (n + 1)) => Fin s (n + 1)+finLast = unsafeToFin $ fromIntegral $ natVal (Proxy :: Proxy n)+{-# INLINE finLast #-}++absurd :: Fin s 0 -> a+absurd = unsafeCoerce+{-# INLINE absurd #-}++-- |+-- >>> (natToFin (Proxy :: Proxy 10) :: Fin Int 11)+-- Fin 10+--+natToFin :: (Integral s, KnownNat n, KnownNat (m + 1), n <= m) => proxy n -> Fin s (m + 1)+natToFin = unsafeToFin . fromIntegral . natVal+{-# INLINE natToFin #-}+++-- |+-- >>> (toFin 0 :: Maybe (Fin Int 4))+-- Just (Fin 0)+--+-- >>> (toFin 4 :: Maybe (Fin Int 4))+-- Nothing+--+toFin :: forall s n. (Integral s, KnownNat (n :: Nat)) => s -> Maybe (Fin s n)+toFin x+  | x < 0 = Nothing+  | x < fromIntegral (natVal (Proxy :: Proxy n)) = Just $ Fin x+  | otherwise = Nothing++-- |+-- >>> (unsafeToFin 10 :: Fin Int 5)+-- Fin 10+--+unsafeToFin :: (Integral s, KnownNat n) => s -> Fin s n+unsafeToFin = Fin+{-# INLINE unsafeToFin #-}+++-- |+-- >>> fromFin (finZ :: Fin Int 10)+-- 0+--+-- >>> fromFin (finLast :: Fin Int 10)+-- 9+--+fromFin :: Fin s n -> s+fromFin (Fin x) = x+{-# INLINE fromFin #-}+++weaken :: (Integral s, KnownNat (n + 1)) => Fin s n -> Fin s (n + 1)+weaken (Fin x) = unsafeToFin x+{-# INLINE weaken #-}++weakenN :: (Integral s, KnownNat (n + m)) => proxy m -> Fin s n -> Fin s (n + m)+weakenN _ (Fin x) = unsafeToFin x+{-# INLINE weakenN #-}++strengthen :: forall n s. (KnownNat n, Integral s, Ord s) => Fin s (n + 1) -> Either (Fin s (n + 1)) (Fin s n)+strengthen x'@(Fin x)+  | x < fromIntegral (natVal (Proxy :: Proxy n)) = Right $ unsafeToFin x+  | otherwise = Left x'+{-# INLINE strengthen #-}++-- |+-- >>> shift (Proxy :: Proxy 1) (finZ :: Fin Int 20)+-- Fin 0+--+-- >>> (shift (Proxy :: Proxy 10) (finLast :: Fin Int 10) :: Fin Int 20)+-- Fin 9+--+shift :: (KnownNat (m + n), Integral s) => proxy m -> Fin s n -> Fin s (m + n)+shift _ (Fin x) = unsafeToFin x+{-# INLINE shift #-}++finAdd :: (Integral s, KnownNat (n + m)) => Fin s n -> Fin s m -> Fin s (n + m)+finAdd (Fin x) (Fin y) = unsafeToFin $ x + y+{-# INLINE finAdd #-}++finAddN :: forall n s. (KnownNat n, Integral s, Ord s) => Fin s n -> s -> Either (Fin s n) (Fin s n)+finAddN x@(Fin x') y+  | fromIntegral (natVal (Proxy :: Proxy n)) - x' > y = Right $ Fin (x' + y)+  | otherwise = Left x+{-# INLINE finAddN #-}++finSub :: (KnownNat n, Ord s, Integral s) => Fin s n -> Fin s m -> Either (Fin s n) (Fin s n)+finSub x (Fin y) = finSubN x y+{-# INLINE finSub #-}++finSubN :: (KnownNat n, Ord s, Integral s) => Fin s n -> s -> Either (Fin s n) (Fin s n)+finSubN x'@(Fin x) y+  | y <= x = Right $ unsafeToFin $ x - y+  | otherwise = Left $ x'+{-# INLINE finSubN #-}+++finMult :: (KnownNat (n * m), Integral s) => Fin s n -> Fin s m -> Fin s (n * m)+finMult (Fin x) (Fin y) = unsafeToFin $ x * y+{-# INLINE finMult #-}+

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2015, Hiroki Hattori++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * 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.++    * Neither the name of Hiroki Hattori nor the names of other+      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+OWNER 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.

+ README.md view

@@ -0,0 +1,5 @@+# data-fin-simple+[![Build Status](https://travis-ci.org/seagull-kamome/data-fin-simple.svg)](https+://travis-ci.org/seagull-kamome/data-fin-simple)++有限集合

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ data-fin-simple.cabal view

@@ -0,0 +1,39 @@+-- Initial data-fin-simple.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                data-fin-simple+version:             0.1.0.0+synopsis:            Simple integral finite set+description:         Typesafe finite unsigned-integral+license:             BSD3+license-file:        LICENSE+author:              Hiroki Hattori+maintainer:          seagull.kamome@gmail.com+-- copyright:           +homepage:            https://github.com/seagull-kamome/data-fin-simple+bug-reports:         https://github.com/seagull-kamome/data-fin-simple/issues+category:            Data+build-type:          Simple+extra-source-files:  +  README.md+cabal-version:       >=1.10++source-repository head+  type:                git+  location:            http://github.com/seagull-kamome/data-fin-simple.git++library+  exposed-modules:     Data.Fin+  -- other-modules:       +  other-extensions:    KindSignatures, DataKinds, StandaloneDeriving+  build-depends:       base >=4.7 && <4.9+  -- hs-source-dirs:      +  default-language:    Haskell2010++test-suite doctest+  type:                exitcode-stdio-1.0+  default-language:    Haskell2010+  hs-source-dirs:      test+  main-is:             doctest.hs+  build-depends:       base >=4.7 && <4.9, doctest >= 0.9.3+

+ test/doctest.hs view

@@ -0,0 +1,12 @@+module Main where++import Test.DocTest++main :: IO ()+main = doctest [+       "-XKindSignatures",+       "-XDataKinds",+       "-idist/build",+       "Data/Fin.hs"+       ]+