{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Utils.Suffix where
import Data.Char
import qualified Data.List as List
import Agda.Utils.Impossible
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
'₉'
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__
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__
data Suffix
= Prime Integer
| Index Integer
| Subscript Integer
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
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
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