content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  module Agda.Utils.Suffix where
  
  import Data.Char
  import qualified Data.List as List
  
  import Agda.Utils.Impossible
  
  ------------------------------------------------------------------------
  -- Subscript digits
  
  -- | Is the character one of the subscripts @'₀'@-@'₉'@?
  
  isSubscriptDigit :: Char -> Bool
  isSubscriptDigit c = '₀' <= c && c <= '₉'
  
  -- | Converts @'0'@-@'9'@ to @'₀'@-@'₉'@
  --
  -- Precondition: The digit needs to be in range.
  
  toSubscriptDigit :: Char -> Char
  toSubscriptDigit d
    | isDigit d = toEnum (fromEnum '₀' + (fromEnum d - fromEnum '0'))
    | otherwise = __IMPOSSIBLE__
  
  -- | Converts @'₀'@-@'₉'@ to @'0'@-@'9'@.
  --
  -- Precondition: The digit needs to be in range.
  
  fromSubscriptDigit :: Char -> Char
  fromSubscriptDigit d
    | isSubscriptDigit d = toEnum (fromEnum '0' + (fromEnum d - fromEnum '₀'))
    | otherwise          = __IMPOSSIBLE__
  
  ------------------------------------------------------------------------
  -- Suffices
  
  -- | Classification of identifier variants.
  
  data Suffix
    = Prime     Integer  -- ^ Identifier ends in @Integer@ many primes.
    | Index     Integer  -- ^ Identifier ends in number @Integer@ (ordinary digits).
    | Subscript Integer  -- ^ Identifier ends in number @Integer@ (subscript digits).
  
  -- | Increase the suffix by one.
  
  nextSuffix :: Suffix -> Suffix
  nextSuffix (Prime i)     = Prime $ i + 1
  nextSuffix (Index i)     = Index $ i + 1
  nextSuffix (Subscript i) = Subscript $ i + 1
  
  -- | Parse suffix.
  
  suffixView :: String -> (String, Maybe Suffix)
  suffixView s
      | (ps@(_:_), s') <- span (== '\'') rs        = (reverse s', Just $ Prime $ List.genericLength ps)
      | (ns@(_:_), s') <- span isDigit rs          = (reverse s', Just $ Index $ read $ reverse ns)
      | (ns@(_:_), s') <- span isSubscriptDigit rs = (reverse s', Just $ Subscript $ read $
                                                        map fromSubscriptDigit $ reverse ns)
      | otherwise                                  = (s, Nothing)
      where rs = reverse s
  
  -- Note: suffixView could be implemented using spanEnd, but the implementation using reverse
  -- looks more efficient, since the reversal is only done once.
  --
  -- suffixView :: String -> (String, Maybe Suffix)
  -- suffixView s
  --     | (s', ps@(_:_)) <- spanEnd (=='\'') s         = (s', Just $ Prime $ length ps)
  --     | (s', ns@(_:_)) <- spanEnd isDigit s          = (s', Just $ Index $ read ns)
  --     | (s', ns@(_:_)) <- spanEnd isSubscriptDigit s = (s', Just $ Subscript $ read $ map fromSubscriptDigit ns)
  --     | otherwise                                    = (s, Nothing)
  
  -- | Print suffix.
  
  renderSuffix :: Suffix -> String
  renderSuffix (Prime n)     = List.genericReplicate n '\''
  renderSuffix (Index i)     = show i
  renderSuffix (Subscript i) = map toSubscriptDigit (show i)
  
  addSuffix :: String -> Suffix -> String
  addSuffix str suffix = str ++ renderSuffix suffix
  