    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 :: Char -> Bool
    isSubscriptDigit Char
    c = Char
    '₀' Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    c Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    '₉'

    -- | Converts @'0'@-@'9'@ to @'₀'@-@'₉'@
    --
    -- Precondition: The digit needs to be in range.

    toSubscriptDigit :: Char -> Char
    toSubscriptDigit :: Char -> Char
    toSubscriptDigit Char
    d
      | Char -> Bool
    isDigit Char
    d = Int -> Char
    forall a. Enum a => Int -> a
    toEnum (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    '₀' Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    d Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    '0'))
      | Bool
    otherwise = Char
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Converts @'₀'@-@'₉'@ to @'0'@-@'9'@.
    --
    -- Precondition: The digit needs to be in range.

    fromSubscriptDigit :: Char -> Char
    fromSubscriptDigit :: Char -> Char
    fromSubscriptDigit Char
    d
      | Char -> Bool
    isSubscriptDigit Char
    d = Int -> Char
    forall a. Enum a => Int -> a
    toEnum (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    '0' Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    d Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    '₀'))
      | Bool
    otherwise          = Char
    forall a. HasCallStack => a
    __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 :: Suffix -> Suffix
    nextSuffix (Prime Integer
    i)     = Integer -> Suffix
    Prime (Integer -> Suffix) -> Integer -> Suffix
    forall a b. (a -> b) -> a -> b
    $ Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1
    nextSuffix (Index Integer
    i)     = Integer -> Suffix
    Index (Integer -> Suffix) -> Integer -> Suffix
    forall a b. (a -> b) -> a -> b
    $ Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1
    nextSuffix (Subscript Integer
    i) = Integer -> Suffix
    Subscript (Integer -> Suffix) -> Integer -> Suffix
    forall a b. (a -> b) -> a -> b
    $ Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1

    -- | Parse suffix.

    suffixView :: String -> (String, Maybe Suffix)
    suffixView :: String -> (String, Maybe Suffix)
    suffixView String
    s
        | (ps :: String
    ps@(Char
    _:String
    _), String
    s') <- (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    ==Char
    '\'') String
    rs         = (String -> String
    forall a. [a] -> [a]
    reverse String
    s', Suffix -> Maybe Suffix
    forall a. a -> Maybe a
    Just (Suffix -> Maybe Suffix) -> Suffix -> Maybe Suffix
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    Prime (Integer -> Suffix) -> Integer -> Suffix
    forall a b. (a -> b) -> a -> b
    $ String -> Integer
    forall i a. Num i => [a] -> i
    List.genericLength String
    ps)
        | (ns :: String
    ns@(Char
    _:String
    _), String
    s') <- (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span Char -> Bool
    isDigit String
    rs          = (String -> String
    forall a. [a] -> [a]
    reverse String
    s', Suffix -> Maybe Suffix
    forall a. a -> Maybe a
    Just (Suffix -> Maybe Suffix) -> Suffix -> Maybe Suffix
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    Index (Integer -> Suffix) -> Integer -> Suffix
    forall a b. (a -> b) -> a -> b
    $ String -> Integer
    forall a. Read a => String -> a
    read (String -> Integer) -> String -> Integer
    forall a b. (a -> b) -> a -> b
    $ String -> String
    forall a. [a] -> [a]
    reverse String
    ns)
        | (ns :: String
    ns@(Char
    _:String
    _), String
    s') <- (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span Char -> Bool
    isSubscriptDigit String
    rs = (String -> String
    forall a. [a] -> [a]
    reverse String
    s', Suffix -> Maybe Suffix
    forall a. a -> Maybe a
    Just (Suffix -> Maybe Suffix) -> Suffix -> Maybe Suffix
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    Subscript (Integer -> Suffix) -> Integer -> Suffix
    forall a b. (a -> b) -> a -> b
    $ String -> Integer
    forall a. Read a => String -> a
    read (String -> Integer) -> String -> Integer
    forall a b. (a -> b) -> a -> b
    $
                                                          (Char -> Char) -> String -> String
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    fromSubscriptDigit (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String -> String
    forall a. [a] -> [a]
    reverse String
    ns)
        | Bool
    otherwise                                  = (String
    s, Maybe Suffix
    forall a. Maybe a
    Nothing)
        where rs :: String
    rs = String -> String
    forall a. [a] -> [a]
    reverse String
    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 :: Suffix -> String
    renderSuffix (Prime Integer
    n)     = Integer -> Char -> String
    forall i a. Integral i => i -> a -> [a]
    List.genericReplicate Integer
    n Char
    '\''
    renderSuffix (Index Integer
    i)     = Integer -> String
    forall a. Show a => a -> String
    show Integer
    i
    renderSuffix (Subscript Integer
    i) = (Char -> Char) -> String -> String
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    toSubscriptDigit (Integer -> String
    forall a. Show a => a -> String
    show Integer
    i)

    addSuffix :: String -> Suffix -> String
    addSuffix :: String -> Suffix -> String
    addSuffix String
    str Suffix
    suffix = String
    str String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Suffix -> String
    renderSuffix Suffix
    suffix