module Data.Type.Nat.Quote where
import Data.Type.Nat
import Type.Family.Nat
import Language.Haskell.TH
import Language.Haskell.TH.Quote
import Control.Monad
import Text.Read (readMaybe)
n :: QuasiQuoter
n = QuasiQuoter
{ quoteExp = parseNatExp
, quotePat = parseNatPat
, quoteType = parseNatType
, quoteDec = error "n: quoteDec not defined"
}
parseNatExp :: String -> Q Exp
parseNatExp s = maybe (fail $ "n: couldn't parse Int: " ++ show s)
(notNeg >=> go)
$ readMaybe s
where
notNeg :: Int -> Q Int
notNeg n
| n < 0 = fail $ "n: negative: " ++ show n
| True = return n
go :: Int -> Q Exp
go = \case
0 -> [| Z_ |]
n -> [| S_ $(go $ n1) |]
parseNatPat :: String -> Q Pat
parseNatPat s = maybe (fail $ "n: couldn't parse Int: " ++ show s)
(notNeg >=> go)
$ readMaybe s
where
notNeg :: Int -> Q Int
notNeg n
| n < 0 = fail $ "n: negative: " ++ show n
| True = return n
go :: Int -> Q Pat
go = \case
0 -> [p| Z_ |]
n -> [p| S_ $(go $ n1) |]
parseNatType :: String -> Q Type
parseNatType s = maybe (fail $ "n: couldn't parse Int: " ++ show s)
(notNeg >=> go)
$ readMaybe s
where
notNeg :: Int -> Q Int
notNeg n
| n < 0 = fail $ "n: negative: " ++ show n
| True = return n
go :: Int -> Q Type
go = \case
0 -> [t| Z |]
n -> [t| S $(go $ n1) |]