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

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

    import Data.Char
    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 :: ModuleName -> ModuleName
    encodeModuleName (HS.ModuleName [Char]
    s) = [Char] -> ModuleName
    HS.ModuleName ([Char] -> ModuleName) -> [Char] -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ case [Char] -> [Char] -> Maybe [Char]
    forall a. Eq a => [a] -> [a] -> Maybe [a]
    List.stripPrefix [Char]
    mazstr [Char]
    s of
      Just [Char]
    s' -> [Char]
    mazstr [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ([Char] -> [Char] -> [Char]) -> [Char] -> [[Char]] -> [Char]
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr [Char] -> [Char] -> [Char]
    encNamePart [Char]
    "" ([Char] -> [[Char]]
    splitUp' [Char]
    s')
      Maybe [Char]
    Nothing -> [Char]
    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' :: [Char] -> [[Char]]
    splitUp' = [Char] -> [[Char]]
    h
        where
          h :: [Char] -> [[Char]]
    h [] = []
          h (Char
    c : [Char]
    cs) = case Char
    c of
            Char
    '.' -> [Char]
    "" [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [Char] -> [[Char]]
    h [Char]
    cs
            Char
    _ -> ([Char] -> [Char]) -> [Char] -> [[Char]]
    g (Char
    c Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    :) [Char]
    cs
          g :: ([Char] -> [Char]) -> [Char] -> [[Char]]
    g [Char] -> [Char]
    acc [] = [[Char] -> [Char]
    acc []]
          g [Char] -> [Char]
    acc (Char
    c : [Char]
    cs) = case Char
    c of
            Char
    '.' -> [Char] -> [Char]
    acc [] [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [Char]
    "" [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [Char] -> [[Char]]
    h [Char]
    cs
            Char
    _ -> ([Char] -> [Char]) -> [Char] -> [[Char]]
    g ([Char] -> [Char]
    acc ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char
    c Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    :)) [Char]
    cs

      encNamePart :: [Char] -> [Char] -> [Char]
    encNamePart [Char]
    "" [Char]
    r = Char
    '.' Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    : [Char]
    r
      encNamePart [Char]
    s  [Char]
    r = [Char] -> [Char] -> [Char]
    ensureFirstCharLarge [Char]
    s ([Char] -> [Char]) -> [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ (Char -> [Char] -> [Char]) -> [Char] -> [Char] -> [Char]
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Char -> [Char] -> [Char]
    enc [Char]
    r [Char]
    s

      ensureFirstCharLarge :: [Char] -> [Char] -> [Char]
    ensureFirstCharLarge [Char]
    s [Char]
    r = case [Char]
    s of
        Char
    c : [Char]
    cs | Char -> Bool
    isUpper Char
    c Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    largeChar -> [Char]
    r
        [Char]
    _                                    -> Char
    largeChar Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    : [Char]
    r

      largeChar :: Char
    largeChar  = Char
    'Q'
      escapeChar :: Char
    escapeChar = Char
    'Z'

      isOK :: Char -> Bool
    isOK Char
    c = Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    escapeChar Bool -> Bool -> Bool
    && Char -> Bool
    isModChar Char
    c

      enc :: Char -> [Char] -> [Char]
    enc Char
    c [Char]
    r | Char -> Bool
    isOK Char
    c    = Char
    c Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    : [Char]
    r
              | Bool
    otherwise = Char
    escapeChar Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    : Int -> [Char] -> [Char]
    forall a. Show a => a -> [Char] -> [Char]
    shows (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    c) (Char
    escapeChar Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    : [Char]
    r)