content: {-# LANGUAGE LambdaCase, OverloadedStrings #-}
  
  module HsToCoq.ConvertHaskell.InfixNames (
    identIsVariable,
    infixToPrefix, toPrefix, toLocalPrefix,
    prefixOpToInfix,
    infixToCoq,
    identIsOp, identToOp,
    splitModule -- a bit out of place here. oh well.
    ) where
  
  import Control.Lens
  
  import Control.Applicative
  import Control.Monad
  import Data.Semigroup (Semigroup(..))
  import Data.Char
  import Data.Text (Text)
  import qualified Data.Text as T
  import Text.Parsec hiding ((<|>), many)
  
  import Encoding (zEncodeString, zDecodeString)
  
  import GHC.Stack
  
  --------------------------------------------------------------------------------
  
  -- Lets keep this module self-contained (but use the same type synonyms)
  type Op = T.Text
  type Ident = T.Text
  type ModuleIdent = T.Text
  type AccessIdent = T.Text
  
  identIsVariable_ :: Text -> Bool
  identIsVariable_ = T.uncons <&> \case
    Just (h,t) -> (isAlpha h || h == '_') && T.all (\c -> isAlphaNum c || c == '_' || c == '\'') t
    Nothing    -> False
  
  identIsVariable :: Text -> Bool
  identIsVariable = all identIsVariable_ . T.splitOn "."
  
  -- An operator's user-facing name in Coq (a notation)
  infixToPrefix :: Op -> Ident
  infixToPrefix = ("_" <>) . (<> "_")
  
  toPrefix :: Ident -> Ident
  toPrefix x | identIsVariable x = x
             | otherwise         = infixToCoq x
  
  toLocalPrefix :: Ident -> Ident
  toLocalPrefix x | identIsVariable x = x
                  | otherwise         = "l" <> infixToCoq x
  
  prefixOpToInfix :: Ident -> Maybe Op
  prefixOpToInfix px = do
    x <- T.stripSuffix "_" =<< T.stripPrefix "_" px
    guard . not $ identIsVariable x
    pure x
  
  -- An operator's defined name in Coq (hidden by a notation)
  infixToCoq_ :: Op -> Ident
  infixToCoq_ name = "op_" <> T.pack (zEncodeString $ T.unpack name) <> "__"
  
  -- This is code smell: Why do we return an unstructured Ident, and not a QualId?
  infixToCoq :: HasCallStack => Op -> Ident
  infixToCoq op = case splitModule op of
      Just (m,op) -> m <> "." <> infixToCoq_ op
      Nothing     -> infixToCoq_ op
  
  splitModule :: Ident -> Maybe (ModuleIdent, AccessIdent)
  splitModule = fmap fixup . either (const Nothing) Just . parse qualid "" where
    qualid = do
      let modFrag = T.cons <$> upper <*> (T.pack <$> many (alphaNum <|> char '_' <|> char '\''))
      mod <- T.intercalate "." <$> many1 (try (modFrag <* char '.'))
      base <- T.pack <$> some anyChar -- since we're assuming we get a valid name
      pure $ (mod, base)
  
    -- When we have a module name that ends in .Z or .N then that should be
    -- considered part of the name of the function. This is a hack to make the
    -- common case of working with names like Coq.ZArith.BinInt.Z.eqb more convenient,
    -- without solving the problem of handling non-filesystem-modules in general
    fixup (mod, name)
      | ".Z" `T.isSuffixOf` mod = (T.take (T.length mod - 2) mod, "Z." <> name)
      | ".N" `T.isSuffixOf` mod = (T.take (T.length mod - 2) mod, "N." <> name)
      | otherwise               = (mod, name)
  
  identIsOp :: Ident -> Bool
  identIsOp t = "op_" `T.isPrefixOf` t && "__" `T.isSuffixOf` t
      -- the next clause is a work-around as long as the dict accessors are named
      -- op_...____ – these do not have notations
      && not ("____" `T.isSuffixOf` t)
      && T.length t > 5
  
  identToOp :: Ident -> Maybe Op
  identToOp t
     | identIsOp t = Just $ T.pack (zDecodeString (T.unpack (T.drop 3 (T.dropEnd 2 t))))
     | otherwise   = Nothing
  
  