{-# LANGUAGE CPP #-}
{-# LANGUAGE TupleSections, LambdaCase, FlexibleContexts, FlexibleInstances, ScopedTypeVariables #-}

#include "ghc-compat.h"

module HsToCoq.ConvertHaskell.Sigs (
  convertLSigs, convertSigs, lookupSig,
  HsSignature(..), collectSigs, collectSigsWithErrors, convertSignatures, convertSignature,
  ) where

import Prelude hiding (Num)

import Control.Lens

import Data.Maybe
import Data.Semigroup (Semigroup(..))
import Data.Traversable (for)
import qualified Data.Text as T

import Control.Monad.Reader
import Control.Monad.Except

import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as M

import GHC hiding (Name)
import qualified GHC

import HsToCoq.Util.GHC
#if __GLASGOW_HASKELL__ >= 806
import HsToCoq.Util.GHC.HsTypes (noExtCon)
#endif
import HsToCoq.Coq.Gallina

import HsToCoq.ConvertHaskell.Parameters.Edits
import HsToCoq.ConvertHaskell.Monad
import HsToCoq.ConvertHaskell.Variables
import HsToCoq.ConvertHaskell.Type



-- From Haskell declaration
data HsSignature = HsSignature { hsSigType   :: LHsSigType GhcRn
                               , hsSigFixity :: Maybe Fixity }


collectSigs :: [Sig GhcRn] -> Either String (Map GHC.Name (Either String HsSignature))
collectSigs sigs = do
  let asType x = ([x], [])
      --asFixity = (S.singleton mname, [], ) . pure

      asTypes lnames sigTy = pure (map ((, asType sigTy) . unLoc) lnames)
      --asFixities lnames fixity = list . map (, asFixity fixity) . filter isRdrOperator $ map unLoc lnames

  multimap :: M.Map GHC.Name ([LHsSigType GhcRn],[Fixity])
   <- fmap (M.fromListWith (<>) . concat) . for sigs $ \case
    TypeSig NOEXTP lnames (HsWC wcs hsib)
      | null wcs  -> asTypes lnames hsib
      | otherwise -> throwError "type wildcards found"
#if __GLASGOW_HASKELL__ >= 806
    TypeSig NOEXTP _ (XHsWildCardBndrs v) -> noExtCon v
    XSig v -> noExtCon v
#endif
    ClassOpSig NOEXTP False lnames sigTy -> asTypes lnames sigTy
    ClassOpSig NOEXTP True _ _ -> pure [] -- Ignore default methods signatures
    FixSig NOEXTP _            -> pure []
    InlineSig NOEXTP _ _       -> pure []
    SpecSig   NOEXTP _ _ _     -> pure []
    SpecInstSig NOEXTP _ _     -> pure []
    MinimalSig  NOEXTP _ _     -> pure []
    SCCFunSig{}          -> pure []
    CompleteMatchSig{}   -> pure []
    PatSynSig NOEXTP _ _ -> pure []
    IdSig     NOEXTP _   -> throwError "generated-code signatures"

  pure $ flip M.mapWithKey multimap $ \_key info@(_,_) -> case info of
         ([ty],  [fixity])  -> Right $ HsSignature ty (Just fixity)
         ([ty],  [])        -> Right $ HsSignature ty Nothing
         ([],    [_fixity]) -> Left $ "a fixity annotation without a type signature"
         ([],    _)         -> Left $ "multiple fixity annotations without a type signature"
         (_,     [])        -> Left $ "multiple type signatures for the same identifier"
         (_,     _)         -> Left $ "multiple type and fixity signatures for the same identifier"

collectSigsWithErrors :: ConversionMonad r m => [Sig GhcRn] -> m (Map GHC.Name HsSignature)
collectSigsWithErrors =
  either convUnsupported' (M.traverseWithKey multiplesError) . collectSigs
  where multiplesError name (Left err) = do
          nameStr <- T.unpack <$> ghcPpr name
          convUnsupported' $ err ++ " for `" ++ nameStr ++ "'"
        multiplesError _ (Right sig) =
          pure sig

convertSignature :: ConversionMonad r m => Qualid -> UnusedTyVarMode -> HsSignature -> m Signature
convertSignature coqName utvm (HsSignature sigTy _hsFix) = do
  withCurrentDefinition coqName (Signature <$> convertLHsSigType utvm sigTy <*> pure Nothing)

-- Incorporates @set type …@ edits ('replacedTypes') for all bindings that
-- /already had/ a type signature; use 'lookupSig' to get the rest.
convertSignatures :: ConversionMonad r m => Map GHC.Name HsSignature -> m (Map Qualid Signature)
convertSignatures = fmap (M.fromList . catMaybes) . traverse conv . M.toList where
  conv (hsName, hsSig) = do
    coqName <- var ExprNS hsName
    view (edits.replacedTypes.at coqName) >>= \case
      Just (Just ty) -> pure $ Just (coqName, Signature ty Nothing)
      Just Nothing   -> pure Nothing
      Nothing -> do
        utvm <- unusedTyVarModeFor coqName
        Just . (coqName,) <$> convertSignature coqName utvm hsSig

-- Incorporates @set type …@ edits ('replacedTypes') for all bindings that
-- /already had/ a type signature; use 'lookupSig' to get the rest.
convertSigs :: ConversionMonad r m => [Sig GhcRn] -> m (Map Qualid Signature)
convertSigs = convertSignatures <=< collectSigsWithErrors

-- Incorporates @set type …@ edits ('replacedTypes') for all bindings that
-- /already had/ a type signature; use 'lookupSig' to get the rest.
convertLSigs :: ConversionMonad r m => [LSig GhcRn] -> m (Map Qualid Signature)
convertLSigs = convertSigs . map unLoc

-- Falls back on the @set type …@ edits ('replacedTypes') if there's no
-- 'Signature' in the map.
lookupSig :: (MonadReader r m, HasEdits r Edits) => Qualid -> Map Qualid Signature -> m (Maybe Signature)
lookupSig qid sigs = case M.lookup qid sigs of
                       sig@Just{} -> pure sig
                       Nothing    -> views (edits.replacedTypes.at qid) (fmap (Signature ?? Nothing) . join)
