{-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, ScopedTypeVariables,
             TypeFamilies, TypeOperators, GADTs, UndecidableInstances,
             FlexibleContexts, DefaultSignatures, BangPatterns,
             InstanceSigs, TypeApplications, StandaloneKindSignatures #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Base.Enum
-- Copyright   :  (C) 2014 Jan Stolarek, Richard Eisenberg
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Jan Stolarek (jan.stolarek@p.lodz.pl)
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Defines the promoted and singleton version of the 'Bounded' and 'Enum' type
-- classes.
--
-- While "Prelude.Singletons" re-exports the promoted and singled versions of
-- 'Enum', it deliberately avoids re-exporting 'Succ' and 'Pred', as these are
-- names are likely to clash with code that deals with unary natural numbers.
-- As a result, this module exists to provide 'Succ' and 'Pred' for those who
-- want them.
--
-----------------------------------------------------------------------------

module Data.Singletons.Base.Enum (
  PBounded(..), SBounded(..),
  PEnum(..), SEnum(..),

  -- ** Defunctionalization symbols
  MinBoundSym0,
  MaxBoundSym0,
  SuccSym0, SuccSym1,
  PredSym0, PredSym1,
  ToEnumSym0, ToEnumSym1,
  FromEnumSym0, FromEnumSym1,
  EnumFromToSym0, EnumFromToSym1, EnumFromToSym2,
  EnumFromThenToSym0, EnumFromThenToSym1, EnumFromThenToSym2,
  EnumFromThenToSym3

  ) where

import Data.Eq.Singletons
import Data.Ord.Singletons
import Data.Singletons.Base.Instances
import Data.Singletons.Base.Util
import Data.Singletons.TH
import GHC.Base.Singletons
import GHC.Num.Singletons
import GHC.TypeLits.Singletons

$(singletonsOnly [d|
  class Bounded a where
    minBound, maxBound :: a

  instance  Bounded Char  where
      minBound =  '\0'
      maxBound =  '\x10FFFF'
  |])

$(singBoundedInstances boundedBasicTypes)

$(singletonsOnly [d|
  class  Enum a   where
      -- | the successor of a value.  For numeric types, 'succ' adds 1.
      succ                :: a -> a
      -- | the predecessor of a value.  For numeric types, 'pred' subtracts 1.
      pred                :: a -> a
      -- | Convert from a 'Natural'.
      toEnum              :: Natural -> a
      -- | Convert to a 'Natural'.
      fromEnum            :: a -> Natural

      -- The following use infinite lists, and are not promotable:
      -- -- | Used in Haskell's translation of @[n..]@.
      -- enumFrom            :: a -> [a]
      -- -- | Used in Haskell's translation of @[n,n'..]@.
      -- enumFromThen        :: a -> a -> [a]

      -- | Used in Haskell's translation of @[n..m]@.
      enumFromTo          :: a -> a -> [a]
      -- | Used in Haskell's translation of @[n,n'..m]@.
      enumFromThenTo      :: a -> a -> a -> [a]

      succ                   = toEnum . (+1)  . fromEnum
      pred                   = toEnum . (subtract 1) . fromEnum
      -- enumFrom x             = map toEnum [fromEnum x ..]
      -- enumFromThen x y       = map toEnum [fromEnum x, fromEnum y ..]
      enumFromTo x y         = map toEnum [fromEnum x .. fromEnum y]
      enumFromThenTo x1 x2 y = map toEnum [fromEnum x1, fromEnum x2 .. fromEnum y]

  -- Natural instance for Enum
  eftNat :: Natural -> Natural -> [Natural]
  -- [x1..x2]
  eftNat x0 y | (x0 > y)  = []
              | otherwise = go x0
                 where
                   go x = x : if (x == y) then [] else go (x + 1)

  efdtNat :: Natural -> Natural -> Natural -> [Natural]
  -- [x1,x2..y]
  efdtNat x1 x2 y
   | x2 >= x1  = efdtNatUp x1 x2 y
   | otherwise = efdtNatDn x1 x2 y

  -- Requires x2 >= x1
  efdtNatUp :: Natural -> Natural -> Natural -> [Natural]
  efdtNatUp x1 x2 y    -- Be careful about overflow!
   | y < x2    = if y < x1 then [] else [x1]
   | otherwise = -- Common case: x1 <= x2 <= y
                 let delta = x2 - x1 -- >= 0
                     y' = y - delta  -- x1 <= y' <= y; hence y' is representable

                     -- Invariant: x <= y
                     -- Note that: z <= y' => z + delta won't overflow
                     -- so we are guaranteed not to overflow if/when we recurse
                     go_up x | x > y'    = [x]
                             | otherwise = x : go_up (x + delta)
                 in x1 : go_up x2

  -- Requires x2 <= x1
  efdtNatDn :: Natural -> Natural -> Natural -> [Natural]
  efdtNatDn x1 x2 y    -- Be careful about underflow!
   | y > x2    = if y > x1 then [] else [x1]
   | otherwise = -- Common case: x1 >= x2 >= y
                 let delta = x2 - x1 -- <= 0
                     y' = y - delta  -- y <= y' <= x1; hence y' is representable

                     -- Invariant: x >= y
                     -- Note that: z >= y' => z + delta won't underflow
                     -- so we are guaranteed not to underflow if/when we recurse
                     go_dn x | x < y'    = [x]
                             | otherwise = x : go_dn (x + delta)
     in x1 : go_dn x2

  instance  Enum Natural  where
      succ x = x + 1
      pred x = x - 1

      toEnum   x = x
      fromEnum x = x

      enumFromTo = eftNat
      enumFromThenTo = efdtNat

  instance  Enum Char  where
      toEnum   = natToChar
      fromEnum = charToNat
  |])

$(singEnumInstances enumBasicTypes)