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

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Prelude.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 Bounded, 'PBounded'
-- and 'SBounded'
--
-----------------------------------------------------------------------------

module Data.Singletons.Prelude.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.Singletons.Single
import Data.Singletons.Util
import Data.Singletons.Prelude.Num
import Data.Singletons.Prelude.Base
import Data.Singletons.Prelude.Ord
import Data.Singletons.Prelude.Eq
import Data.Singletons.Prelude.Instances
import Data.Singletons.TypeLits

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

$(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 'Nat'.
      toEnum              :: Nat -> a
      -- | Convert to a 'Nat'.
      fromEnum            :: a -> Nat

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

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

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

  -- Requires x2 >= x1
  efdtNatUp :: Nat -> Nat -> Nat -> [Nat]
  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 :: Nat -> Nat -> Nat -> [Nat]
  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 Nat  where
      succ x = x + 1
      pred x = x - 1

      toEnum   x = x
      fromEnum x = x

      enumFromTo = eftNat
      enumFromThenTo = efdtNat
  |])

$(singEnumInstances enumBasicTypes)