content: module Agda2Hs.Compile.Name where
  
  import Control.Arrow ( (>>>) )
  import Control.Applicative ( (<|>) )
  import Control.Monad
  import Control.Monad.Except ( catchError )
  import Control.Monad.Reader
  
  import Data.Functor ( (<&>) )
  import Data.Bifunctor ( bimap )
  import Data.List ( intercalate, isPrefixOf, stripPrefix )
  import qualified Data.Text as Text
  import qualified Data.Map.Strict as Map
  
  import Agda.Compiler.Backend hiding ( topLevelModuleName )
  import Agda.Compiler.Common ( topLevelModuleName )
  
  import qualified Agda.Syntax.Abstract as A
  import Agda.Syntax.Common hiding (Rewrite)
  import Agda.Syntax.Internal
  import Agda.Syntax.Position
  import qualified Agda.Syntax.Concrete as C
  import Agda.Syntax.Scope.Base ( inverseScopeLookupName, amodName )
  import Agda.Syntax.Scope.Monad ( resolveName, isDatatypeModule )
  import Agda.Syntax.TopLevelModuleName
  import Agda.Syntax.Common.Pretty ( prettyShow )
  import qualified Agda.Syntax.Common.Pretty as P
  
  import Agda.TypeChecking.Datatypes ( isDataOrRecordType )
  import Agda.TypeChecking.Pretty
  import Agda.TypeChecking.Records ( isRecordConstructor )
  import Agda.TypeChecking.Warnings ( warning )
  
  import qualified Agda.Utils.List1 as List1
  import Agda.Utils.Maybe
  import Agda.Utils.Monad ( orM, whenM )
  
  import Agda2Hs.AgdaUtils
  import Agda2Hs.Compile.Types
  import Agda2Hs.Compile.Utils
  
  import qualified Agda2Hs.Language.Haskell as Hs
  import Agda2Hs.Language.Haskell.Utils ( hsName, hsModuleName, pp )
  
  
  isSpecialCon :: QName -> Maybe (Hs.QName ())
  isSpecialCon = prettyShow >>> \case
      "Agda.Builtin.List.List"     -> special Hs.ListCon
      "Agda.Builtin.List.List._∷_" -> special Hs.Cons
      "Agda.Builtin.List.List.[]"  -> special Hs.ListCon
      "Agda.Builtin.Unit.⊤"        -> special Hs.UnitCon
      "Agda.Builtin.Unit.tt"       -> special Hs.UnitCon
      _ -> Nothing
    where special c = Just (Hs.Special () $ c ())
  
  -- | Convert identifier and import module strings into the Haskell equivalent syntax.
  toNameImport :: String -> Maybe String -> (Hs.Name (), Maybe Import)
  toNameImport x Nothing = (hsName x, Nothing)
  toNameImport x (Just mod) =
    ( hsName x
    , Just $ Import (hsModuleName mod) Unqualified Nothing (hsName x) (Hs.NoNamespace ())
    )
  
  -- | Default rewrite rules.
  defaultSpecialRules :: SpecialRules
  defaultSpecialRules = Map.fromList
    [ "Agda.Builtin.Nat.Nat"          `to` "Natural"      `importing` Just "Numeric.Natural"
    , "Haskell.Prelude.coerce"        `to` "unsafeCoerce" `importing` Just "Unsafe.Coerce"
    , "Agda.Builtin.Int.Int"          `to` "Integer"      `importing` Nothing
    , "Agda.Builtin.Word.Word64"      `to` "Word"         `importing` Nothing
    , "Agda.Builtin.Float.Float"      `to` "Double"       `importing` Nothing
    , "Agda.Builtin.Bool.Bool.false"  `to` "False"        `importing` Nothing
    , "Agda.Builtin.Bool.Bool.true"   `to` "True"         `importing` Nothing
    , "Haskell.Prim._∘_"              `to` "_._"          `importing` Nothing
    , "Haskell.Prim.Monad.Dont._>>=_" `to` "_>>=_"        `importing` Nothing
    , "Haskell.Prim.Monad.Dont._>>_"  `to` "_>>_"         `importing` Nothing
    , "Haskell.Prim.Tuple.first"      `to` "first"        `importing` Just "Control.Arrow"
    , "Haskell.Prim.Tuple.second"     `to` "second"       `importing` Just "Control.Arrow"
    , "Haskell.Prim.Tuple._***_"      `to` "_***_"        `importing` Just "Control.Arrow"
    ]
    where infixr 6 `to`, `importing`
          to = (,)
          importing = toNameImport
  
  -- | Check whether the given name should be rewritten to a special Haskell name, possibly with new imports.
  isSpecialName :: QName -> C (Maybe (Hs.Name (), Maybe Import))
  isSpecialName f = asks (Map.lookup (prettyShow f) . rewrites)
  
  compileName :: Applicative m => Name -> m (Hs.Name ())
  compileName n = hsName . show <$> pretty (nameConcrete n)
  
  compileQName :: QName -> C (Hs.QName ())
  compileQName f = do
    whenJustM (getCompileToName f) $ \g ->
      reportSDoc "agda2hs.compile.to" 20 $ text $
        "compiling name " <> prettyShow f <> " to " <> prettyShow g
    f <- fromMaybe f <$> getCompileToName f
    let compileSpecialCon c = do
          reportSDoc "agda2hs.name" 25 $ text $
            "compiling name: " ++ prettyShow f ++
            " to special constructor: " ++ Hs.prettyPrint c
          return c
    ifJust (isSpecialCon f) compileSpecialCon $ do
      f <- isRecordConstructor f <&> \case
        Just (r, def) | not (_recNamedCon def) -> r -- use record name for unnamed constructors
        _                                      -> f
      hf0 <- compileName (qnameName f)
      special <- isSpecialName f
      let (hf, mimpBuiltin) = fromMaybe (hf0, Nothing) special
  
      parent <- parentName f
      par <- traverse (compileName . qnameName) parent
      let mod0 = qnameModule $ fromMaybe f parent
      (mkind, mod) <- compileModuleName mod0
  
      existsInHaskell <- orM
        [ pure $ isJust special
        , pure $ mkind == PrimModule
        , pure $ mkind == HsModule
        , hasCompilePragma f
        , isClassFunction f
        , isWhereFunction f
        , maybe (pure False) hasCompilePragma parent
        ]
  
      unless existsInHaskell $ do
        reportSDoc "agda2hs.name" 20 $ text "DOES NOT EXIST IN HASKELL"
        typeError $ CustomBackendError "agda2hs" $ P.text $
          "Symbol " ++ Hs.prettyPrint hf ++ " is missing a COMPILE pragma or rewrite rule"
  
      currMod <- asks $ hsTopLevelModuleName . currModule
      let skipModule = mod == currMod
                    || isJust mimpBuiltin
                    || prettyShow mod0 `elem` primMonadModules
      qual <- if skipModule then return Unqualified
                else getQualifier (fromMaybe f parent) mod
      -- we only calculate this when dealing with type operators; usually that's where 'type' prefixes are needed in imports
      namespace <- case hf of
            Hs.Symbol _ _ -> getNamespace f
            Hs.Ident  _ _ -> return (Hs.NoNamespace ())
      let
        -- We generate import statements for everything except
        -- unqualified prim modules (Prelude)
        mimp = if mkind == PrimModule && not (isQualified qual)
               then Nothing
               else Just (Import mod qual par hf namespace)
        qf = qualify mod hf qual
  
      -- add (possibly qualified) import
      whenM (asks writeImports) $
        whenJust (mimpBuiltin <|> mimp) tellImport
  
      reportSDoc "agda2hs.name" 25 $ text
         $ "-------------------------------------------------"
        ++ "\ncompiling name: " ++ prettyShow f
        ++ "\nhaskell name: " ++ Hs.prettyPrint hf
        ++ "\nparent name: " ++ prettyShow parent
        ++ "\nmod0: " ++ prettyShow mod0
        ++ "\nmodule name: " ++ Hs.prettyPrint mod
        ++ "\ncurrent module: " ++ Hs.prettyPrint currMod
        ++ "\nqualifier: " ++ prettyShow (fmap (fmap pp) qual)
        ++ "\n(qualified) haskell name: " ++ pp qf
      return qf
    where
      parentName :: QName -> C (Maybe QName)
      parentName q = (theDef <$> getConstInfo q) <&> \case
        Constructor {conData = dt} -> Just dt
        Function {funProjection = proj}
          | Right (Projection {projProper = Just{}, projFromType = rt}) <- proj
          -> Just $ unArg rt
        _ -> Nothing
  
      getQualifier :: QName -> Hs.ModuleName () -> C Qualifier
      getQualifier f mod =
        (inverseScopeLookupName f <$> getScope) >>= \case
          (C.QName{} : _) -> return Unqualified
          (C.Qual as C.QName{} : _) -> liftTCM $ do
            let qual = hsModuleName $ prettyShow as
            lookupModuleInCurrentModule as >>= \case
              (x:_) | qual /= mod -> do
                isDataMod <- isJust <$> isDatatypeModule (amodName x)
                return $ QualifiedAs (if isDataMod then Nothing else Just qual)
              _ -> return $ QualifiedAs Nothing
            `catchError` \_ -> return $ QualifiedAs Nothing
          _ -> return $ QualifiedAs Nothing
  
      qualify :: Hs.ModuleName () -> Hs.Name () -> Qualifier -> Hs.QName ()
      qualify mod n = \case
        (QualifiedAs as) -> Hs.Qual () (fromMaybe mod as) n
        Unqualified      -> Hs.UnQual () n
  
      primMonadModules = ["Haskell.Prim.Monad.Dont", "Haskell.Prim.Monad.Do"]
  
      -- Determine whether it is a type operator or an "ordinary" operator.
      -- _getSort is not for that; e. g. a data has the same sort as its constructor.
      getNamespace :: QName -> C (Hs.Namespace ())
      getNamespace qName = do
        qType <- unEl . getResultType . defType <$> getConstInfo qName
        if isJust $ isSort qType then do
          let fname = nameCanonical $ qnameName f
          reportSDoc "agda2hs.name" 25 $ pretty fname <+>
            " is a type operator; will add \"type\" prefix before it"
          return $ Hs.TypeNamespace ()
        else return $ Hs.NoNamespace ()
  
      -- Gets the type of the result of the function (the type after the last "->").
      getResultType :: Type -> Type
      getResultType typ = case unEl typ of
        (Pi _ absType) -> getResultType $ unAbs absType
        _              -> typ
  
  isWhereFunction :: QName -> C Bool
  isWhereFunction f = do
    whereMods <- asks whereModules
    return $ any (qnameModule f `isLeChildModuleOf`) whereMods
  
  hsTopLevelModuleName :: TopLevelModuleName -> Hs.ModuleName ()
  hsTopLevelModuleName = hsModuleName . Text.unpack . Text.intercalate "."
                       . List1.toList . moduleNameParts
  
  -- | Given a module name (assumed to be a toplevel module),
  -- compute the associated Haskell module name.
  compileModuleName :: ModuleName -> C (HsModuleKind, Hs.ModuleName ())
  compileModuleName m = do
    tlm <- liftTCM $ hsTopLevelModuleName <$> getTopLevelModuleForModuleName m
    reportSDoc "agda2hs.name" 25 $
      "Top-level module name for" <+> prettyTCM m <+> "is" <+> text (pp tlm)
    case hsModuleKind tlm of
      PrimModule -> return (PrimModule, Hs.ModuleName () "Prelude")
      HsModule   -> return (HsModule, dropHaskellPrefix tlm)
      AgdaModule -> return (AgdaModule, tlm)
  
  importInstance :: QName -> C ()
  importInstance f = do
    (kind, mod) <- compileModuleName $ qnameModule f
    unless (kind == PrimModule) $ do
      reportSLn "agda2hs.import" 20 $ "Importing instances from " ++ pp mod
      tellImport $ ImportInstances mod
  