{-|
Copyright  :  (C) 2013-2016, University of Twente
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
-}

{-# LANGUAGE TemplateHaskell #-}

{-# LANGUAGE Trustworthy #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module Clash.Promoted.Nat.TH
  ( -- * Declare a single @d\<N\>@ literal
    decLiteralD
    -- * Declare ranges of @d\<N\>@ literals
  , decLiteralsD
  )
where

import Language.Haskell.TH
import Clash.Promoted.Nat

{- $setup
>>> :set -XDataKinds
>>> let d1111 = SNat :: SNat 1111
>>> let d1200 = SNat :: SNat 1200
>>> let d1201 = SNat :: SNat 1201
>>> let d1202 = SNat :: SNat 1202
-}

-- | Create an 'SNat' literal
--
-- > $(decLiteralD 1111)
--
-- >>> :t d1111
-- d1111 :: SNat 1111
--
decLiteralD :: Integer
            -> Q [Dec]
decLiteralD :: Integer -> Q [Dec]
decLiteralD n :: Integer
n = do
  let suffix :: String
suffix  = if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then String -> String
forall a. HasCallStack => String -> a
error ("Can't make negative SNat: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n) else Integer -> String
forall a. Show a => a -> String
show Integer
n
      valName :: Name
valName = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ 'd'Char -> String -> String
forall a. a -> [a] -> [a]
:String
suffix
  Dec
sig   <- Name -> TypeQ -> DecQ
sigD Name
valName (TypeQ -> TypeQ -> TypeQ
appT (Name -> TypeQ
conT ''SNat) (TyLitQ -> TypeQ
litT (Integer -> TyLitQ
numTyLit Integer
n)))
  Dec
val   <- PatQ -> BodyQ -> [DecQ] -> DecQ
valD (Name -> PatQ
varP Name
valName) (ExpQ -> BodyQ
normalB [| SNat |]) []
  [Dec] -> Q [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Dec
sig, Dec
val ]

-- | Create a range of 'SNat' literals
--
-- > $(decLiteralsD 1200 1202)
--
-- >>> :t d1200
-- d1200 :: SNat 1200
-- >>> :t d1201
-- d1201 :: SNat 1201
-- >>> :t d1202
-- d1202 :: SNat 1202
--
decLiteralsD :: Integer
             -> Integer
             -> Q [Dec]
decLiteralsD :: Integer -> Integer -> Q [Dec]
decLiteralsD from :: Integer
from to :: Integer
to =
    ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Q [[Dec]] -> Q [Dec]) -> Q [[Dec]] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ [Q [Dec]] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Q [Dec]] -> Q [[Dec]]) -> [Q [Dec]] -> Q [[Dec]]
forall a b. (a -> b) -> a -> b
$ [ Integer -> Q [Dec]
decLiteralD Integer
n | Integer
n <- [Integer
from..Integer
to] ]