------------------------------------------------------------------------
-- 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 forall a b. (a -> b) -> a -> b
$ case forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix [Char]
mazstr [Char]
s of
  Just [Char]
s' -> [Char]
mazstr forall a. [a] -> [a] -> [a]
++ 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]
"" forall a. a -> [a] -> [a]
: [Char] -> [[Char]]
h [Char]
cs
        Char
_ -> ([Char] -> [Char]) -> [Char] -> [[Char]]
g (Char
c 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 [] forall a. a -> [a] -> [a]
: [Char]
"" forall a. a -> [a] -> [a]
: [Char] -> [[Char]]
h [Char]
cs
        Char
_ -> ([Char] -> [Char]) -> [Char] -> [[Char]]
g ([Char] -> [Char]
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
c forall a. a -> [a] -> [a]
:)) [Char]
cs

  encNamePart :: [Char] -> [Char] -> [Char]
encNamePart [Char]
"" [Char]
r = Char
'.' forall a. a -> [a] -> [a]
: [Char]
r
  encNamePart [Char]
s  [Char]
r = [Char] -> [Char] -> [Char]
ensureFirstCharLarge [Char]
s forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => a -> a -> Bool
/= Char
largeChar -> [Char]
r
    [Char]
_                                    -> Char
largeChar 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 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 forall a. a -> [a] -> [a]
: [Char]
r
          | Bool
otherwise = Char
escapeChar forall a. a -> [a] -> [a]
: forall a. Show a => a -> [Char] -> [Char]
shows (forall a. Enum a => a -> Int
fromEnum Char
c) (Char
escapeChar forall a. a -> [a] -> [a]
: [Char]
r)