{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Type.Index.Quote
-- Copyright   :  Copyright (C) 2015 Kyle Carter
-- License     :  BSD3
--
-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
-- Stability   :  experimental
-- Portability :  RankNTypes
--
-- A 'QuasiQuoter' for the 'N' kind and the 'Nat' type.
--
-----------------------------------------------------------------------------

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 $ n-1) |]

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 $ n-1) |]

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 $ n-1) |]