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