{-# LANGUAGE PatternGuards #-}
module Agda.Utils.Suffix where

import Data.Char

data Suffix = NoSuffix | Prime Int | Index Int

nextSuffix NoSuffix  = Prime 1
nextSuffix (Prime _) = Index 0	-- we only use single primes in generated names
nextSuffix (Index i) = Index $ i + 1

suffixView :: String -> (String, Suffix)
suffixView s
    | (ps@(_:_), s') <- span (=='\'') rs = (reverse s', Prime $ length ps)
    | (ns@(_:_), s') <- span isDigit rs	 = (reverse s', Index $ read $ reverse ns)
    | otherwise				 = (s, NoSuffix)
    where
	rs = reverse s

addSuffix :: String -> Suffix -> String
addSuffix s NoSuffix = s
addSuffix s (Prime n) = s ++ replicate n '\''
addSuffix s (Index i) = s ++ show i