NatQQ.hs

{-# OPTIONS_GHC -fno-warn-missing-fields #-}
{-# LANGUAGE TemplateHaskell #-}
module RlangQQ.NatQQ (n) where

import Language.Haskell.TH.Quote
import Language.Haskell.TH
import Data.HList.CommonMain

{- | HList uses it's own nat, distinct from 'GHC.TypeLits.Nat', for various reasons.

Specifying those 'HNat' can be done like:

> [n| 5 |]

which is shorter than the equivalent

> hSucc $ hSucc $ hSucc $ hSucc $ hSucc hZero

-}
n :: QuasiQuoter
n = QuasiQuoter { quoteExp = natExp . read, quoteType = natTy . read, quotePat = natPat . read }

natExp :: Int -> ExpQ
natExp n = foldr appE [| hZero |] (replicate n [| hSucc |])

natTy n = [t| Proxy $(foldr appT (promotedT 'HZero) (replicate n (promotedT 'HSucc))) |]


natPat n = sigP (varP (mkName ("nat"++show n))) (natTy n)