    ------------------------------------------------------------------------
    -- Module name encoding
    ------------------------------------------------------------------------

    module Agda.Compiler.MAlonzo.Encode
      ( encodeModuleName
      ) where

    import Data.Char
    import Data.Function
    import qualified Data.List as List
    import qualified Agda.Utils.Haskell.Syntax as HS

    import Agda.Compiler.MAlonzo.Misc

    -- | Haskell module names have to satisfy the Haskell (including the
    -- hierarchical module namespace extension) lexical syntax:
    --
    --   @modid -> [modid.] large {small | large | digit | ' }@
    --
    -- 'encodeModuleName' is an injective function into the set of module
    -- names defined by @modid@. The function preserves @.@s, and it also
    -- preserves module names whose first name part is not 'mazstr'.
    --
    -- Precondition: The input must not start or end with @.@, and no two
    -- @.@s may be adjacent.

    encodeModuleName :: HS.ModuleName -> HS.ModuleName
    encodeModuleName (HS.ModuleName s) = HS.ModuleName $ case List.stripPrefix mazstr s of
      Just s' -> mazstr ++ foldr encNamePart "" (splitUp' s')
      Nothing -> s
      where
      -- splitUp ".apa.bepa." == [".","apa",".","bepa","."]
      -- splitUp = groupBy ((&&) `on` (/= '.'))

      -- Since comparison against "." is wasteful, and modules name components are nonempty,
      -- we can use "" as the separator.
      -- Since modules name components are nonempty,
      -- this is more efficient than adding a Maybe wrapper:
      -- We are effectively using ``String = Maybe NEString''.
      --
      -- splitUp' ".apa.bepa." == ["","apa","","bepa",""]
      splitUp' :: String -> [String]
      splitUp' = h
        where
          h [] = []
          h (c : cs) = case c of
            '.' -> "" : h cs
            _ -> g (c :) cs
          g acc [] = [acc []]
          g acc (c : cs) = case c of
            '.' -> acc [] : "" : h cs
            _ -> g (acc . (c :)) cs

      encNamePart "" r = '.' : r
      encNamePart s  r = ensureFirstCharLarge s $ foldr enc r s

      ensureFirstCharLarge s r = case s of
        c : cs | isUpper c && c /= largeChar -> r
        _                                    -> largeChar : r

      largeChar  = 'Q'
      escapeChar = 'Z'

      isOK c = c /= escapeChar && isModChar c

      enc c r | isOK c    = c : r
              | otherwise = escapeChar : shows (fromEnum c) (escapeChar : r)