module Data.Type.Natural.Class
( module Data.Type.Natural.Class.Arithmetic
, module Data.Type.Natural.Class.Order
,
mkSNatQQ) where
import Data.Type.Natural.Class.Arithmetic
import Data.Type.Natural.Class.Order
import Data.Singletons.Prelude (FromInteger, Sing, sing)
import Language.Haskell.TH
import Language.Haskell.TH.Quote
mkSNatQQ :: TypeQ -> QuasiQuoter
mkSNatQQ t = QuasiQuoter
{ quoteExp = mkExpQuote
, quotePat = error "no pattern quoter for snats"
, quoteType = mkTypeQuote
, quoteDec = error "not implemented"
}
where
mkExpQuote :: String -> ExpQ
mkExpQuote s = [| sing :: $(mkTypeQuote s) |]
mkTypeQuote :: String -> TypeQ
mkTypeQuote s =
let n = read s
in [t| Sing $(sigT [t| FromInteger $(litT $ numTyLit n)|] =<< t) |]