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

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Prelude.Base
-- Copyright   :  (C) 2014 Jan Stolarek
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Jan Stolarek (jan.stolarek@p.lodz.pl)
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Implements singletonized versions of functions from @GHC.Base@ module.
--
-- Because many of these definitions are produced by Template Haskell,
-- it is not possible to create proper Haddock documentation. Please look
-- up the corresponding operation in @Data.Tuple@. Also, please excuse
-- the apparent repeated variable names. This is due to an interaction
-- between Template Haskell and Haddock.
--
----------------------------------------------------------------------------

module Data.Singletons.Prelude.Base (
  -- * Basic functions
  Foldr, sFoldr, Map, sMap, type (++), (%++), Otherwise, sOtherwise,
  Id, sId, Const, sConst, type (.), (%.), type ($), type ($!), (%$), (%$!),
  Until, sUntil, Flip, sFlip, AsTypeOf, sAsTypeOf,
  Seq, sSeq,

  -- * Defunctionalization symbols
  FoldrSym0, FoldrSym1, FoldrSym2, FoldrSym3,
  MapSym0, MapSym1, MapSym2,
  type (++@#@$), type (++@#@$$), type (++@#@$$$),
  OtherwiseSym0,
  IdSym0, IdSym1,
  ConstSym0, ConstSym1, ConstSym2,
  type (.@#@$),  type (.@#@$$),  type (.@#@$$$), type (.@#@$$$$),
  type ($@#@$),  type ($@#@$$),  type ($@#@$$$),
  type ($!@#@$), type ($!@#@$$), type ($!@#@$$$),
  UntilSym0, UntilSym1, UntilSym2, UntilSym3,
  FlipSym0, FlipSym1, FlipSym2, FlipSym3,
  AsTypeOfSym0, AsTypeOfSym1, AsTypeOfSym2,
  SeqSym0, SeqSym1, SeqSym2
  ) where

import Data.Singletons.Prelude.Instances
import Data.Singletons.Single
import Data.Singletons.Prelude.Bool

-- Promoted and singletonized versions of "otherwise" are imported and
-- re-exported from Data.Singletons.Prelude.Bool. This is done to avoid cyclic
-- module dependencies.

$(singletonsOnly [d|
  foldr                   :: (a -> b -> b) -> b -> [a] -> b
  foldr k z = go
            where
              go []     = z
              go (y:ys) = y `k` go ys

  map                     :: (a -> b) -> [a] -> [b]
  map _ []                = []
  map f (x:xs)            = f x : map f xs

  (++)                    :: [a] -> [a] -> [a]
  (++) []     ys          = ys
  (++) (x:xs) ys          = x : xs ++ ys
  infixr 5 ++

  id                      :: a -> a
  id x                    =  x

  const                   :: a -> b -> a
  const x _               =  x

  (.)    :: (b -> c) -> (a -> b) -> a -> c
  (.) f g = \x -> f (g x)
  infixr 9 .

  flip                    :: (a -> b -> c) -> b -> a -> c
  flip f x y              =  f y x

  asTypeOf                :: a -> a -> a
  asTypeOf                =  const

  ($)                     :: (a -> b) -> a -> b
  f $ x                   =  f x
  infixr 0 $

  ($!)                    :: (a -> b) -> a -> b
  f $! x                  = let {-!-}vx = x in f vx
  infixr 0 $!

  until                   :: (a -> Bool) -> (a -> a) -> a -> a
  until p f = go
    where
      -- Does not singletonize due to overlapping patterns.
      {-
      go x | p x          = x
           | otherwise    = go (f x)
      -}
      go x = if p x then x else go (f x)

  -- This is not part of GHC.Base, but we need to emulate seq and this is a good
  -- place to do it.
  seq :: a -> b -> b
  seq _ x = x
  infixr 0 `seq`
 |])