{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------

-- |

-- 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)