cabal-version:      >=1.10
name:               fin
version:            0.0.3
synopsis:           Nat and Fin: peano naturals and finite numbers
category:           Data, Dependent Types, Singletons
description:
  This package provides two simple types, and some tools to work with them.
  Also on type level as @DataKinds@.
  .
  @
  \-- Peano naturals
  data Nat = Z | S Nat
  .
  \-- Finite naturals
  data Fin (n :: Nat) where
  \    Z :: Fin ('S n)
  \    S :: Fin n -> Fin ('Nat.S n)
  @
  .
  [vec](https://hackage.haskell.org/package/vec) implements length-indexed
  (sized) lists using this package for indexes.
  .
  The "Data.Fin.Enum" module let's work generically with enumerations.
  .
  See [Hasochism: the pleasure and pain of dependently typed haskell programming](https://doi.org/10.1145/2503778.2503786)
  by Sam Lindley and Conor McBride for answers to /how/ and /why/.
  Read [APLicative Programming with Naperian Functors](https://doi.org/10.1007/978-3-662-54434-1_21)
  by Jeremy Gibbons for (not so) different ones.
  .
  === Similar packages
  .
  * [finite-typelits](https://hackage.haskell.org/package/finite-typelits)
  . Is a great package, but uses @GHC.TypeLits@.
  .
  * [type-natural](https://hackage.haskell.org/package/type-natural) depends
  on @singletons@ package. @fin@ will try to stay light on the dependencies,
  and support as many GHC versions as practical.
  .
  * [peano](https://hackage.haskell.org/package/peano) is very incomplete
  .
  * [nat](https://hackage.haskell.org/package/nat) as well.
  .
  * [PeanoWitnesses](https://hackage.haskell.org/package/PeanoWitnesses)
  doesn't use @DataKinds@.
  .
  * [type-combinators](https://hackage.haskell.org/package/type-combinators)
  is big package too.

homepage:           https://github.com/phadej/vec
bug-reports:        https://github.com/phadej/vec/issues
license:            BSD3
license-file:       LICENSE
author:             Oleg Grenrus <oleg.grenrus@iki.fi>
maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
copyright:          (c) 2017-2019 Oleg Grenrus
build-type:         Simple
extra-source-files: ChangeLog.md
tested-with:
  GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4

source-repository head
  type:     git
  location: https://github.com/phadej/vec.git

library
  exposed-modules:
    Data.Fin
    Data.Fin.Enum
    Data.Nat
    Data.Type.Nat
    Data.Type.Nat.LE
    Data.Type.Nat.LE.ReflStep
    Data.Type.Nat.LT

  build-depends:
      base      >=4.7     && <4.13
    , dec       >=0.0.3   && <0.1
    , deepseq   >=1.3.0.2 && <1.5
    , hashable  >=1.2.7.0 && <1.4

  if !impl(ghc >=8.2)
    build-depends: bifunctors >=5.5.3 && <5.6

  if !impl(ghc >=8.0)
    build-depends: semigroups >=0.18.4 && <0.20

  if !impl(ghc >=7.10)
    build-depends:
        nats  >=1.1.2 && <1.2
      , void  >=0.7.2 && <0.8

  ghc-options:      -Wall -fprint-explicit-kinds
  hs-source-dirs:   src
  default-language: Haskell2010

-- dump-core
-- if impl(ghc >= 8.0)
--  build-depends: dump-core
--  ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html

test-suite inspection
  type:             exitcode-stdio-1.0
  main-is:          Inspection.hs
  ghc-options:      -Wall -fprint-explicit-kinds
  hs-source-dirs:   test
  default-language: Haskell2010
  build-depends:
      base
    , fin
    , inspection-testing  >=0.2.0.1 && <0.5
    , tagged

  if !impl(ghc >=8.0)
    buildable: False

  -- useful for development
  ghc-options: