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

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

  ensureFirstCharLarge :: String -> String -> String
ensureFirstCharLarge String
s String
r = case String
s of
    Char
c : String
cs | Char -> Bool
isUpper Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
largeChar -> String
r
    String
_                                    -> Char
largeChar Char -> String -> String
forall a. a -> [a] -> [a]
: String
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 -> String -> String
enc Char
c String
r | Char -> Bool
isOK Char
c    = Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
r
          | Bool
otherwise = Char
escapeChar Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String -> String
forall a. Show a => a -> String -> String
shows (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c) (Char
escapeChar Char -> String -> String
forall a. a -> [a] -> [a]
: String
r)