{-# LANGUAGE CPP,
             TupleSections, LambdaCase, RecordWildCards,
             OverloadedLists, OverloadedStrings,
             FlexibleContexts, RankNTypes, ScopedTypeVariables,
             ViewPatterns, MultiWayIf  #-}

#include "ghc-compat.h"

module HsToCoq.ConvertHaskell.Expr (
  convertTypedModuleBinding,
  convertMethodBinding,
  convertTypedModuleBindings,
  hsBindName,
  ) where

import Prelude hiding (Num())

import Control.Lens

import Control.Arrow ((&&&))
import Data.Bifunctor
import Data.Foldable
import HsToCoq.Util.Foldable
import Data.Functor (($>))
import Data.Traversable
import Data.Bitraversable
import HsToCoq.Util.Function
import Data.Maybe
import Data.Either
import Data.List (sortOn)
import HsToCoq.Util.List hiding (unsnoc)
import Data.List.NonEmpty (nonEmpty, NonEmpty(..))
import qualified Data.List.NonEmpty as NEL
import qualified HsToCoq.Util.List as NEL ((|>))
import Data.Text (Text)
import qualified Data.Text as T

import Control.Monad.Trans.Maybe
import Control.Monad.Except
import Control.Monad.Writer

import HsToCoq.Util.Containers

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

import GHC hiding (Name, HsChar, HsString, AsPat)
import qualified GHC
import Bag
import BasicTypes
import HsToCoq.Util.GHC.FastString
import RdrName
import HsToCoq.Util.GHC.Exception
import qualified Outputable as GHC

import HsToCoq.Util.GHC
import HsToCoq.Util.GHC.Name hiding (Name)
import HsToCoq.Util.GHC.HsExpr
import HsToCoq.Util.GHC.HsTypes (selectorFieldOcc_, fieldOcc)
#if __GLASGOW_HASKELL__ >= 806
import HsToCoq.Util.GHC.HsTypes (noExtCon)
#endif
import HsToCoq.Coq.Gallina as Coq
import HsToCoq.Coq.Gallina.Util
import HsToCoq.Coq.Gallina.UseTypeInBinders
import HsToCoq.Coq.Subst
import HsToCoq.Coq.Gallina.Rewrite as Coq
import HsToCoq.Coq.FreeVars
import HsToCoq.Util.FVs (ErrOrVars(..))
import HsToCoq.Coq.Pretty

import HsToCoq.ConvertHaskell.Parameters.Edits
import HsToCoq.ConvertHaskell.TypeInfo
import HsToCoq.ConvertHaskell.Monad
import HsToCoq.ConvertHaskell.Variables
import HsToCoq.ConvertHaskell.Definitions
import HsToCoq.ConvertHaskell.Literals
import HsToCoq.ConvertHaskell.Type
import HsToCoq.ConvertHaskell.Pattern
import HsToCoq.ConvertHaskell.Sigs
import HsToCoq.ConvertHaskell.Axiomatize

--------------------------------------------------------------------------------

rewriteExpr :: ConversionMonad r m => Term -> m Term
rewriteExpr tm = do
  rws <- view (edits.rewrites)
  return $ Coq.rewrite rws tm

-- Module-local
il_integer :: IntegralLit -> Integer
il_integer IL{..} = (if il_neg then negate else id) il_value

-- Module-local
convert_int_literal :: LocalConvMonad r m => String -> Integer -> m Term
convert_int_literal what = either convUnsupported (pure . Num)
                         . convertInteger (what ++ " literals")

convertExpr :: LocalConvMonad r m => HsExpr GhcRn -> m Term
convertExpr hsExpr = convertExpr_ hsExpr >>= rewriteExpr

convertExpr_ :: forall r m. LocalConvMonad r m => HsExpr GhcRn -> m Term
convertExpr_ (HsVar NOEXTP (L _ x)) =
  Qualid <$> var ExprNS x

convertExpr_ (HsUnboundVar NOEXTP x) =
  Var <$> freeVar (unboundVarOcc x)

convertExpr_ (HsRecFld NOEXTP fld) =
  Qualid <$> recordField fld

convertExpr_ HsOverLabel{} =
  convUnsupported "overloaded labels"

convertExpr_ (HsIPVar NOEXTP _) =
  convUnsupported "implicit parameters"

convertExpr_ (HsOverLit NOEXTP OverLit{..}) =
  case ol_val of
    HsIntegral   intl     -> App1 "GHC.Num.fromInteger" <$> convert_int_literal "integer" (il_integer intl)
    HsFractional fr       -> convertFractional fr
    HsIsString   _src str -> pure $ convertFastString str

convertExpr_ (HsLit NOEXTP lit) =
  case lit of
    GHC.HsChar   _ c       -> pure $ HsChar c
    HsCharPrim   _ _       -> convUnsupported "`Char#' literals"
    GHC.HsString _ fs      -> pure $ convertFastString fs
    HsStringPrim _ _       -> convUnsupported "`Addr#' literals"
    HsInt        _ intl    -> convert_int_literal "`Int'" (il_integer intl)
    HsIntPrim    _ int     -> convert_int_literal "`IntPrim'" int
    HsWordPrim   _ _       -> convUnsupported "`Word#' literals"
    HsInt64Prim  _ _       -> convUnsupported "`Int64#' literals"
    HsWord64Prim _ _       -> convUnsupported "`Word64#' literals"
    HsInteger    _ int _ty -> convert_int_literal "`Integer'" int
    HsRat        _ _ _     -> convUnsupported "`Rational' literals"
    HsFloatPrim  _ _       -> convUnsupported "`Float#' literals"
    HsDoublePrim _ _       -> convUnsupported "`Double#' literals"
#if __GLASGOW_HASKELL__ >= 806
    XLit v -> noExtCon v
#endif

convertExpr_ (HsLam NOEXTP mg) =
  uncurry Fun <$> convertFunction [] mg -- We don't skip any equations in an ordinary lambda

convertExpr_ (HsLamCase NOEXTP mg) = do
  skipPats <- views (edits.skippedCasePatterns) (S.map pure)
  uncurry Fun <$> convertFunction skipPats mg

convertExpr_ (HsApp NOEXTP e1 e2) =
  App1 <$> convertLExpr e1 <*> convertLExpr e2

#if __GLASGOW_HASKELL__ >= 808
convertExpr_ (HsAppType NOEXTP e1 _) =
#elif __GLASGOW_HASKELL__ == 806
convertExpr_ (HsAppType _ e1) =
#else
convertExpr_ (HsAppType e1 _) =
#endif
  convertLExpr e1
--  convUnsupported "type applications"
--  SCW: just ignore them for now, and let the user figure it out.

#if __GLASGOW_HASKELL__ >= 806
convertExpr_ (OpApp _fixity el eop er) =
#else
convertExpr_ (OpApp el eop _fixity er) =
#endif
  case eop of
    L _ (HsVar NOEXTP (L _ hsOp)) -> do
      op  <- var ExprNS hsOp
      op' <- rewriteExpr $ Qualid op
      l   <- convertLExpr el
      r   <- convertLExpr er
      pure $ App2 op' l r
    _ ->
      convUnsupported "non-variable infix operators"

convertExpr_ (NegApp NOEXTP e1 _) =
  App1 <$> (pure "GHC.Num.negate" >>= rewriteExpr) <*> convertLExpr e1

convertExpr_ (HsPar NOEXTP e) =
  Parens <$> convertLExpr e

convertExpr_ (SectionL NOEXTP l opE) =
  convert_section (Just l) opE Nothing

convertExpr_ (SectionR NOEXTP opE r) =
  convert_section Nothing opE (Just r)

-- TODO: Mark converted unboxed tuples specially?
convertExpr_ (ExplicitTuple NOEXTP exprs _boxity) = do
  -- TODO A tuple constructor in the Gallina grammar?
  (tuple, args) <- runWriterT
                .  fmap (foldl1 . App2 $ "pair")
                .  for exprs $ unLoc <&> \case
                     Present NOEXTP e -> lift $ convertLExpr e
                     Missing PlaceHolder ->
                       do arg <- lift (genqid "arg")
                          Qualid arg <$ tell [arg]
#if __GLASGOW_HASKELL__ >= 806
                     XTupArg v -> noExtCon v
#endif
  pure $ maybe id Fun (nonEmpty $ map (mkBinder Coq.Explicit . Ident) args) tuple

convertExpr_ (HsCase NOEXTP e mg) = do
  scrut    <- convertLExpr e
  skipPats <- views (edits.skippedCasePatterns) (S.map pure)
  bindIn "scrut" scrut $ \scrut -> convertMatchGroup skipPats [scrut] mg

convertExpr_ (HsIf NOEXTP overloaded c t f) =
  if maybe True isNoSyntaxExpr overloaded
  then ifThenElse <*> pure SymmetricIf <*> convertLExpr c <*> convertLExpr t <*> convertLExpr f
  else convUnsupported "overloaded if-then-else"

convertExpr_ (HsMultiIf PlaceHolder lgrhsList) =
  convertLGRHSList [] lgrhsList patternFailure

convertExpr_ (HsLet NOEXTP (L _ binds) body) =
  convertLocalBinds binds $ convertLExpr body

#if __GLASGOW_HASKELL__ >= 806
convertExpr_ (HsDo _ sty (L _ stmts)) =
#else
convertExpr_ (HsDo sty (L _ stmts) PlaceHolder) =
#endif
  case sty of
    ListComp        -> convertListComprehension stmts
    DoExpr          -> convertDoBlock stmts

    MonadComp       -> convUnsupported "monad comprehensions"
    MDoExpr         -> convUnsupported "`mdo' expressions"
    ArrowExpr       -> convUnsupported "arrow expressions"
    GhciStmtCtxt    -> convUnsupported "GHCi statement expressions"
    PatGuard _      -> convUnsupported "pattern guard expressions"
    ParStmtCtxt _   -> convUnsupported "parallel statement expressions"
    TransStmtCtxt _ -> convUnsupported "transform statement expressions"
#if __GLASGOW_HASKELL__ < 806
    PArrComp        -> convUnsupported "parallel array comprehensions"
#endif

convertExpr_ (ExplicitList PlaceHolder overloaded exprs) =
  if maybe True isNoSyntaxExpr overloaded
  then foldr (App2 "cons") "nil" <$> traverse convertLExpr exprs
  else convUnsupported "overloaded lists"

-- TODO: Unify with the `RecCon` case in `ConPatIn` for `convertPat` (in
-- `HsToCoq.ConvertHaskell.Pattern`)
#if __GLASGOW_HASKELL__ >= 806
convertExpr_ (RecordCon _ (L _ hsCon) HsRecFields{..}) = do
#else
convertExpr_ (RecordCon (L _ hsCon) PlaceHolder conExpr HsRecFields{..}) = do
  unless (isNoPostTcExpr conExpr) $
    convUnsupported "unexpected post-typechecker record constructor"
#endif

  let recConUnsupported what = do
        hsConStr <- ghcPpr hsCon
        convUnsupported $  "creating a record with the " ++ what
                        ++ " constructor `" ++ T.unpack hsConStr ++ "'"

  con <- var ExprNS hsCon

  lookupConstructorFields con >>= \case
    Just (RecordFields conFields) -> do
      let defaultVal field | isJust rec_dotdot = Qualid field
                           | otherwise         = missingValue

      vals <- fmap M.fromList . for rec_flds $
        \(L _ (HsRecField (L _ occ) hsVal pun)) -> do
                field <- var ExprNS (selectorFieldOcc_ occ)
                val   <- if pun
                         then pure $ Qualid field
                         else convertLExpr hsVal
                pure (field, val)
      pure . appList (Qualid con)
           $ map (\field -> PosArg $ M.findWithDefault (defaultVal field) field vals) conFields

    Just (NonRecordFields count)
      | null rec_flds && isNothing rec_dotdot ->
        pure . appList (Qualid con) $ replicate count (PosArg missingValue)

      | otherwise ->
        recConUnsupported "non-record"

    Nothing -> recConUnsupported "unknown"

#if __GLASGOW_HASKELL__ >= 806
convertExpr_ (RecordUpd _ recVal fields) = do
#else
convertExpr_ (RecordUpd recVal fields PlaceHolder PlaceHolder PlaceHolder PlaceHolder) = do
#endif
  updates <- fmap M.fromList . for fields $ \(L _ HsRecField{..}) -> do
               field <- recordField $ unLoc hsRecFieldLbl
               pure (field, if hsRecPun then Nothing else Just hsRecFieldArg)

  let updFields = M.keys updates
      prettyUpdFields what =
        let quote f = "`" ++ T.unpack (qualidToIdent f) ++ "'"
        in explainStrItems quote "no" "," "and" what (what ++ "s") updFields

  recType <- S.minView . S.fromList <$> traverse (\field -> lookupRecordFieldType field) updFields >>= \case
               Just (Just recType, []) -> pure recType
               Just (Nothing,      []) -> convUnsupported $ "invalid record update with " ++ prettyUpdFields "non-record-field"
               _                       -> convUnsupported $ "invalid mixed-data-type record updates with " ++ prettyUpdFields "the given field"

  ctors :: [Qualid]  <- maybe (convUnsupported "invalid unknown record type") pure =<< lookupConstructors recType

  let loc :: e -> Located e
      loc  = mkGeneralLocated "generated"
      toLPat_ :: Pat GhcRn -> LPat GhcRn
      toLPat_ = toLPat "generated"
      toHs = freshInternalName . T.unpack

  let partialUpdateError :: Qualid -> m (Match GhcRn (Located (HsExpr GhcRn)))
      partialUpdateError con = do
        hsCon   <- toHs (qualidToIdent con)
        hsError <- toHs "GHC.Err.error"
        pure $ GHC.Match
          { m_ctxt = LambdaExpr
          , m_pats   = [ toLPat_ . ConPatIn (loc hsCon)
                             . RecCon $ HsRecFields { rec_flds = []
                                                    , rec_dotdot = Nothing } ]
          , m_grhss  = GRHSs { grhssGRHSs = [ loc . GRHS NOEXT [] . loc $
                                              HsApp NOEXT
                                                    (loc . HsVar NOEXT . loc $ hsError)
                                                    (loc . HsLit NOEXT . GHC.HsString (SourceText "") $ fsLit "Partial record update") ]
                             , grhssLocalBinds = loc (EmptyLocalBinds NOEXT)
#if __GLASGOW_HASKELL__ >= 806
                             , grhssExt = NOEXT
#endif
                             }
#if __GLASGOW_HASKELL__ >= 806
          , m_ext = NOEXT
#endif
          }

  matches <- for ctors $ \con ->
    lookupConstructorFields con >>= \case
      Just (RecordFields fields) | all (`elem` fields) $ M.keysSet updates -> do
        let addFieldOcc :: HsRecField' GHC.Name arg -> HsRecField GhcRn arg
            addFieldOcc field@HsRecField{hsRecFieldLbl = L s lbl} =
              let rdrLbl = mkOrig <$> nameModule <*> nameOccName $ lbl
                  l = L s (fieldOcc (L s rdrLbl) lbl)
              in field{ hsRecFieldLbl = l }
            useFields fields = HsRecFields { rec_flds   = map (fmap addFieldOcc) fields
                                           , rec_dotdot = Nothing }
        (fieldPats, fieldVals) <- fmap (bimap useFields useFields . unzip) . for fields $ \field -> do
          fieldVar   <- gensym (qualidBase field)
          hsField    <- toHs (qualidToIdent field)
          hsFieldVar <- toHs fieldVar
          let mkField arg = loc $ HsRecField { hsRecFieldLbl = loc hsField
                                             , hsRecFieldArg = arg
                                             , hsRecPun      = False }
          pure ( mkField . toLPat_ . GHC.VarPat NOEXT . loc $ hsFieldVar
               , mkField . fromMaybe (loc . HsVar NOEXT $ loc hsField) -- NOT `fieldVar` – this was punned
                         $ M.findWithDefault (Just . loc . HsVar NOEXT $ loc hsFieldVar) field updates )

        hsCon <- toHs (qualidToIdent con)
#if __GLASGOW_HASKELL__ >= 806
        let r = RecordCon NOEXT (loc hsCon) fieldVals
#else
        let r = RecordCon (loc hsCon) PlaceHolder noPostTcExpr fieldVals
#endif
        pure GHC.Match { m_ctxt   = LambdaExpr
                       , m_pats   = [ toLPat_ . ConPatIn (loc hsCon) $ RecCon fieldPats ]
                       , m_grhss  = GRHSs { grhssGRHSs = [ loc . GRHS NOEXT [] . loc $ r ]
                                          , grhssLocalBinds = loc (EmptyLocalBinds NOEXT)
#if __GLASGOW_HASKELL__ >= 806
                                          , grhssExt = NOEXT
#endif
                                          }
#if __GLASGOW_HASKELL__ >= 806
                       , m_ext = NOEXT
#endif
                       }

      Just _ ->
        partialUpdateError con
      Nothing ->
        convUnsupported "invalid unknown constructor in record update"

#if __GLASGOW_HASKELL__ >= 806
  convertExpr . HsCase NOEXT recVal $
    MG { mg_alts    = loc $ map loc matches
       , mg_ext     = NOEXT
       , mg_origin  = Generated }
#else
  convertExpr . HsCase recVal $
    MG { mg_alts    = loc $ map loc matches
       , mg_arg_tys = []
       , mg_res_ty  = PlaceHolder
       , mg_origin  = Generated }
#endif


#if __GLASGOW_HASKELL__ >= 808
convertExpr_ (ExprWithTySig NOEXTP e sigWcTy) =
#elif __GLASGOW_HASKELL__ == 806
convertExpr_ (ExprWithTySig sigWcTy e) =
#else
convertExpr_ (ExprWithTySig e sigWcTy) =
#endif
  HasType <$> convertLExpr e <*> convertLHsSigWcType PreserveUnusedTyVars sigWcTy

convertExpr_ (ArithSeq _postTc _overloadedLists info) =
  -- TODO: Special-case infinite lists?
  -- TODO: `enumFrom{,Then}{,To}` is really…?
  -- TODO: Add Coq syntax sugar?  Something like
  --
  --     Notation "[ :: from        '..' ]"    := (enumFrom       from).
  --     Notation "[ :: from , next '..' ]"    := (enumFromThen   from next).
  --     Notation "[ :: from        '..' to ]" := (enumFromTo     from      to).
  --     Notation "[ :: from , next '..' to ]" := (enumFromThenTo from next to).
  --
  -- Only `'..'` doesn't work for some reason.
  case info of
    From       low           -> App1 "GHC.Enum.enumFrom"       <$> convertLExpr low
    FromThen   low next      -> App2 "GHC.Enum.enumFromThen"   <$> convertLExpr low <*> convertLExpr next
    FromTo     low      high -> App2 "GHC.Enum.enumFromTo"     <$> convertLExpr low                       <*> convertLExpr high
    FromThenTo low next high -> App3 "GHC.Enum.enumFromThenTo" <$> convertLExpr low <*> convertLExpr next <*> convertLExpr high

convertExpr_ (HsSCC NOEXTP _ _ e) =
  convertLExpr e

convertExpr_ (HsCoreAnn NOEXTP _ _ e) =
  convertLExpr e

convertExpr_ (HsBracket{}) =
  convUnsupported "Template Haskell brackets"

convertExpr_ (HsRnBracketOut{}) =
  convUnsupported "`HsRnBracketOut' constructor"

convertExpr_ (HsTcBracketOut{}) =
  convUnsupported "`HsTcBracketOut' constructor"

convertExpr_ (HsSpliceE{}) =
  convUnsupported "Quasiquoters and Template Haskell splices"

convertExpr_ (HsProc{}) =
  convUnsupported "`proc' expressions"

convertExpr_ HsStatic{} =
  convUnsupported "static pointers"

convertExpr_ (HsTick NOEXTP _ e) =
  convertLExpr e

convertExpr_ (HsBinTick NOEXTP _ _ e) =
  convertLExpr e

convertExpr_ (HsTickPragma NOEXTP _ _ _ e) =
  convertLExpr e

convertExpr_ (HsWrap{}) =
  convUnsupported "`HsWrap' constructor"

convertExpr_ (HsConLikeOut{}) =
  convUnsupported "`HsConLikeOut' constructor"

convertExpr_ (ExplicitSum{}) =
  convUnsupported "`ExplicitSum' constructor"

#if __GLASGOW_HASKELL__ >= 806
convertExpr_ (HsOverLit _ (XOverLit v)) = noExtCon v
convertExpr_ (XExpr v) = noExtCon v
#else
convertExpr_ (HsAppTypeOut _ _) =
  convUnsupported "`HsAppTypeOut' constructor"

convertExpr_ (ExprWithTySigOut e sigWcTy) =
  HasType <$> convertLExpr e <*> convertLHsSigWcType PreserveUnusedTyVars sigWcTy

convertExpr_ (ExplicitPArr _ _) =
  convUnsupported "explicit parallel arrays"

convertExpr_ (PArrSeq _ _) =
  convUnsupported "parallel array arithmetic sequences"
#endif

#if __GLASGOW_HASKELL__ < 810
convertExpr_ HsArrApp{} =
  convUnsupported "arrow application command"

convertExpr_ HsArrForm{} =
  convUnsupported "arrow command formation"

convertExpr_ EWildPat{} =
  convUnsupported "wildcard pattern in expression"

convertExpr_ EAsPat{} =
  convUnsupported "as-pattern in expression"

convertExpr_ EViewPat{} =
  convUnsupported "view-pattern in expression"

convertExpr_ ELazyPat{} =
  convUnsupported "lazy pattern in expression"
#endif

--------------------------------------------------------------------------------

-- Module-local
convert_section :: LocalConvMonad r m => Maybe (LHsExpr GhcRn) -> LHsExpr GhcRn -> Maybe (LHsExpr GhcRn) -> m Term
convert_section  ml opE mr = do
  let -- We need this type signature, and I think it's because @let@ isn't being
      -- generalized.
      hs :: ConversionMonad r m => Qualid -> m (HsExpr GhcRn)
      hs  = fmap (HsVar NOEXT . mkGeneralLocated "generated") . freshInternalName . T.unpack . qualidToIdent
      coq = mkBinder Coq.Explicit . Ident

  arg <- Bare <$> gensym "arg"
  let orArg = maybe (fmap noLoc $ hs arg) pure
  l <- orArg ml
  r <- orArg mr
#if __GLASGOW_HASKELL__ >= 806
  Fun [coq arg] <$> convertExpr (OpApp defaultFixity l opE r)
#else
  -- TODO RENAMER look up fixity?
  Fun [coq arg] <$> convertExpr (OpApp l opE defaultFixity r)
#endif

--------------------------------------------------------------------------------

convertLExpr :: LocalConvMonad r m => LHsExpr GhcRn -> m Term
convertLExpr = convertExpr . unLoc

--------------------------------------------------------------------------------

convertFunction :: LocalConvMonad r m
                => Set (NonEmpty NormalizedPattern)
                -> MatchGroup GhcRn (LHsExpr GhcRn)
                -> m (Binders, Term)
convertFunction _ mg | Just alt <- isTrivialMatch mg = convTrivialMatch alt
convertFunction skipEqns mg = do
  let n_args = matchGroupArity mg
  args <- replicateM n_args (genqid "arg") >>= maybe err pure . nonEmpty
  let argBinders = (mkBinder Coq.Explicit . Ident) <$> args
  match <- convertMatchGroup skipEqns (Qualid <$> args) mg
  pure (argBinders, match)
 where
   err = convUnsupported "convertFunction: Empty argument list"

isTrivialMatch :: MatchGroup GhcRn (LHsExpr GhcRn) -> Maybe (Match GhcRn (LHsExpr GhcRn))
isTrivialMatch (MG { mg_alts = L _ [L _ alt] }) = trivMatch alt where

  trivMatch :: Match GhcRn (LHsExpr GhcRn) -> Maybe (Match GhcRn (LHsExpr GhcRn))
  trivMatch alt = if all trivLPat (m_pats alt) then Just alt else Nothing

  trivPat :: Pat GhcRn -> Bool
  trivPat (GHC.WildPat _) = False
  trivPat (GHC.VarPat NOEXTP _)  = True
  trivPat (GHC.BangPat NOEXTP p) = trivLPat p
  trivPat (GHC.LazyPat NOEXTP p) = trivLPat p
  trivPat (GHC.ParPat  NOEXTP p) = trivLPat p
  trivPat _                     = False

  trivLPat = trivPat . unLPat
isTrivialMatch _ = Nothing

-- TODO: Unify with `isTrivialMatch` to return a `Maybe (Binders, Term)`
convTrivialMatch ::  LocalConvMonad r m =>
  Match GhcRn (LHsExpr GhcRn) ->  m (Binders, Term)
convTrivialMatch alt = do
  (MultPattern pats, _, rhs) <- convertMatch alt
                                  <&> maybe (error "internal error: convTrivialMatch: not a trivial match!") id
  names <- mapM patToName pats
  let argBinders = (mkBinder Explicit) <$> names
  body <- rhs patternFailure
  return (argBinders, body)

patToName :: LocalConvMonad r m => Pattern -> m Name
patToName UnderscorePat    = pure UnderscoreName
patToName (QualidPat qid)  = pure $ Ident qid
patToName _                = convUnsupported "patToArg: not a trivial pat"

--------------------------------------------------------------------------------

isTrueLExpr :: GhcMonad m => LHsExpr GhcRn -> m Bool
isTrueLExpr (L _ (HsVar NOEXTP x))         = ((||) <$> (== "otherwise") <*> (== "True")) <$> ghcPpr x
isTrueLExpr (L _ (HsTick NOEXTP _ e))      = isTrueLExpr e
isTrueLExpr (L _ (HsBinTick NOEXTP _ _ e)) = isTrueLExpr e
isTrueLExpr (L _ (HsPar NOEXTP e))         = isTrueLExpr e
isTrueLExpr _                       = pure False

--------------------------------------------------------------------------------

-- TODO: Unify `buildTrivial` and `buildNontrivial`?
convertPatternBinding :: LocalConvMonad r m
                      => LPat GhcRn -> LHsExpr GhcRn
                      -> (Term -> (Term -> Term) -> m a)
                      -> (Term -> Qualid -> (Term -> Term -> Term) -> m a)
                      -> (Qualid -> m a)
                      -> Term
                      -> m a
convertPatternBinding hsPat hsExp buildTrivial buildNontrivial buildSkipped fallback =
  runPatternT (convertLPat hsPat) >>= \case
    Left  skipped       -> buildSkipped skipped
    Right (pat, guards) -> do
      exp <- convertLExpr hsExp
     
      ib <- ifThenElse
     
      refutability pat >>= \case
        Trivial tpat | null guards ->
          buildTrivial exp $ Fun [mkBinder Coq.Explicit $ maybe UnderscoreName Ident tpat]
     
        nontrivial -> do
          cont <- genqid "cont"
          arg  <- genqid "arg"
     
          -- TODO: Use SSReflect's `let:` in the `SoleConstructor` case?
          -- (Involves adding a constructor to `Term`.)
          let fallbackMatches
                | SoleConstructor <- nontrivial = []
                | otherwise                     = [ Equation [MultPattern [UnderscorePat]] fallback ]
              guarded tm | null guards = tm
                         | otherwise   = ib LinearIf (foldr1 (App2 "andb") guards) tm fallback
     
          buildNontrivial exp cont $ \body rest ->
            Let cont [mkBinder Coq.Explicit $ Ident arg] Nothing
                     (Coq.Match [MatchItem (Qualid arg) Nothing Nothing] Nothing $
                       Equation [MultPattern [pat]] (guarded rest) : fallbackMatches)
              body

convertDoBlock :: LocalConvMonad r m => [ExprLStmt GhcRn] -> m Term
convertDoBlock allStmts = do
    case fmap unLoc <$> unsnoc allStmts of
      Just (stmts, lastStmt -> Just e) -> foldMap (Endo . toExpr . unLoc) stmts `appEndo` convertLExpr e
      Just _                           -> convUnsupported "invalid malformed `do' block"
      Nothing                          -> convUnsupported "invalid empty `do' block"
  where
#if __GLASGOW_HASKELL__ >= 806
    lastStmt (BodyStmt _ e _ _) = Just e
#else
    lastStmt (BodyStmt e _ _ _) = Just e
#endif
    lastStmt (LastStmt NOEXTP e _ _) = Just e
    lastStmt _                  = Nothing

    toExpr x rest = toExpr_ x rest >>= rewriteExpr

#if __GLASGOW_HASKELL__ >= 806
    toExpr_ (BodyStmt _ e _bind _guard) rest =
#else
    toExpr_ (BodyStmt e _bind _guard _PlaceHolder) rest =
#endif
      monThen <$> convertLExpr e <*> rest

#if __GLASGOW_HASKELL__ >= 806
    toExpr_ (BindStmt _ pat exp _bind _fail) rest =
#else
    toExpr_ (BindStmt pat exp _bind _fail PlaceHolder) rest =
#endif
      convertPatternBinding
        pat exp
        (\exp' fun          -> monBind exp' . fun <$> rest)
        (\exp' cont letCont -> letCont (monBind exp' (Qualid cont)) <$> rest)
        (\skipped           -> convUnsupported $
          "binding against the skipped constructor `" ++ showP skipped ++ "' in `do' notation")
        (missingValue `App1` HsString "Partial pattern match in `do' notation")

    toExpr_ (LetStmt NOEXTP (L _ binds)) rest =
      convertLocalBinds binds rest

    toExpr_ (RecStmt{}) _ =
      convUnsupported "`rec' statements in `do` blocks"

    toExpr_ _ _ =
      convUnsupported "impossibly fancy `do' block statements"

    monBind e1 e2 = mkInfix e1 "GHC.Base.>>=" e2
    monThen e1 e2 = mkInfix e1 "GHC.Base.>>"  e2

convertListComprehension :: LocalConvMonad r m => [ExprLStmt GhcRn] -> m Term
convertListComprehension allStmts = case fmap unLoc <$> unsnoc allStmts of
  Just (stmts, LastStmt NOEXTP e _applicativeDoInfo _returnInfo) ->
    foldMap (Endo . toExpr . unLoc) stmts `appEndo`
      (App2 (Var "cons") <$> convertLExpr e <*> pure (Var "nil"))
  Just _ ->
    convUnsupported "invalid malformed list comprehensions"
  Nothing ->
    convUnsupported "invalid empty list comprehension"
  where
#if __GLASGOW_HASKELL__ >= 806
    toExpr (BodyStmt _ e _bind _guard) rest =
#else
    toExpr (BodyStmt e _bind _guard _PlaceHolder) rest =
#endif
      isTrueLExpr e >>= \case
        True  -> rest
        False -> ifThenElse <*> pure LinearIf
                            <*> convertLExpr e
                            <*> rest
                            <*> pure (Var "nil")

    -- TODO: `concatMap` is really…?
#if __GLASGOW_HASKELL__ >= 806
    toExpr (BindStmt _ pat exp _bind _fail) rest =
#else
    toExpr (BindStmt pat exp _bind _fail PlaceHolder) rest =
#endif
      convertPatternBinding
        pat exp
        (\exp' fun          -> App2 concatMapT <$> (fun <$> rest) <*> pure exp')
        (\exp' cont letCont -> letCont (App2 concatMapT (Qualid cont) exp') <$> rest)
        (\skipped           -> pure $ App1 (Qualid "GHC.Skip.nil_skipped") (String $ textP skipped))
        (Var "nil")
        -- `GHC.Skip.nil_skipped` always returns `[]`, but it has a note about
        -- what constructor was skipped.

    toExpr (LetStmt NOEXTP (L _ binds)) rest =
      convertLocalBinds binds rest

    toExpr _ _ =
      convUnsupported "impossibly fancy list comprehension conditions"

    concatMapT :: Term
    concatMapT = "Coq.Lists.List.flat_map"

--------------------------------------------------------------------------------

-- Could this pattern be considered a 'catch all' or exhaustive pattern?
isWildCoq :: Pattern -> Bool
isWildCoq UnderscorePat     = True
isWildCoq (QualidPat _)     = True
isWildCoq (AsPat p _)       = isWildCoq p
isWildCoq (ArgsPat qid nep) = qid == (Bare "pair") && all isWildCoq nep
isWildCoq _ = False


{-
  = ArgsPat Qualid (NE.NonEmpty Pattern)
  | ExplicitArgsPat Qualid (NE.NonEmpty Pattern)
  | InfixPat Pattern Op Pattern
  | AsPat Pattern Ident
  | InScopePat Pattern Ident
  | QualidPat Qualid
  | UnderscorePat
  | NumPat HsToCoq.Coq.Gallina.Num
  | StringPat T.Text
  | OrPats (NE.NonEmpty OrPattern)
-}

-- This function, used by both convertMatchGroup for the various matches,
-- as well as in convertMatch for the various guarded RHS, implements
-- fall-though semantics, by binding each item to a jump point and passing
-- the right failure jump target to the prevoius item.
chainFallThroughs :: LocalConvMonad r m =>
    [Term -> m Term] -> -- The matches, in syntax order
    Term -> -- The final failure value
    m Term
chainFallThroughs cases failure = go (reverse cases) failure where
   go (m:ls) next_case = do
      this_match <- m next_case
      bindIn "j" this_match $ \failure -> go ls failure
   go [] failure = pure failure


-- A match group contains multiple alternatives, and each can have guards, and
-- there is fall-through semantics. But often we know that if one pattern fall-through,
-- then the next pattern will not match. In that case, we want to bind them in the same
-- match-with clause, in the hope of obtaining a full pattern match
--
-- The plan is:
-- * Convert each alternative individually into a pair of a pattern and a RHS.
--   The RHS is a (shallow) function that takes the fall-through target.
--   This is done by convertMatch
-- * Group patterns that are mutually exclusive, and put them in match-with clauses.
--   Add a catch-all case if that group is not complete already.
-- * Chain these groups.
convertMatchGroup :: LocalConvMonad r m
                  => Set (NonEmpty NormalizedPattern)
                  -> NonEmpty Term
                  -> MatchGroup GhcRn (LHsExpr GhcRn)
                  -> m Term
convertMatchGroup skipEqns args (MG { mg_alts = L _ alts }) = do
    allConvAlts <- traverse (convertMatch . unLoc) alts
    let convAlts = [alt | Just alt@(MultPattern pats, _, _) <- allConvAlts
                        , (normalizePattern <$> pats) `notElem` skipEqns ]
    -- TODO: Group
    convGroups <- groupMatches convAlts

    let scrut = args <&> \arg -> MatchItem arg Nothing Nothing
    let matches = buildMatch scrut <$> convGroups

    chainFallThroughs matches patternFailure
#if __GLASGOW_HASKELL__ >= 806
convertMatchGroup _ _ (XMatchGroup v) = noExtCon v
#endif

data HasGuard = HasGuard | HasNoGuard deriving (Eq, Ord, Enum, Bounded, Show, Read)

groupMatches :: forall r m a. ConversionMonad r m =>
    [(MultPattern, HasGuard, a)] -> m [[(MultPattern, a)]]
groupMatches pats = map (map snd) . go <$> mapM summarize pats
  where
    -- Gather some summary information on the alternatives
    --  - do they have guards
    --  - what is their PatternSummary
    summarize :: (MultPattern, HasGuard, a) -> m ([PatternSummary], HasGuard, (MultPattern, a))
    summarize (mp,hg,x) = do
        s <- multPatternSummary mp
        return (s,hg,(mp,x))

    go :: forall x. [([PatternSummary], HasGuard, x)] -> [[([PatternSummary], x)]]
    go [] = pure []
    go ((ps,hg,x):xs) = case go xs of
        -- Append to a group if it has no guard
        (g:gs) | HasNoGuard <- hg          -> ((ps,x):g)  : gs
        -- Append to a group, if mutually exclusive with all members
               | all (mutExcls ps . fst) g -> ((ps,x):g)  : gs
        -- Otherwise, start a new group
        gs                                 -> ((ps,x):[]) : gs


convertMatch :: LocalConvMonad r m =>
    Match GhcRn (LHsExpr GhcRn) -> -- the match
    m (Maybe (MultPattern, HasGuard, Term -> m Term)) -- the pattern, hasGuards, the right-hand side
convertMatch GHC.Match{..} =
  (runPatternT $    maybe (convUnsupported "no-pattern case arms") pure . nonEmpty
               =<< traverse convertLPat m_pats) <&> \case
    Left _skipped        -> Nothing
    Right (pats, guards) ->
      let extraGuards = map BoolGuard guards
          rhs = convertGRHSs extraGuards m_grhss
     
          hg | null extraGuards = hasGuards m_grhss
             | otherwise        = HasGuard
     
      in Just (MultPattern pats, hg, rhs)
#if __GLASGOW_HASKELL__ >= 806
convertMatch (XMatch v) = noExtCon v
#endif

buildMatch :: ConversionMonad r m =>
    NonEmpty MatchItem -> [(MultPattern, Term -> m Term)] -> Term -> m Term
-- This short-cuts wildcard matches (avoid introducing a match-with alltogether)
buildMatch _ [(pats,mkRhs)] failure
    | isUnderscoreMultPattern pats = mkRhs failure
buildMatch scruts eqns failure = do
    -- Pass the failure
    eqns' <- forM eqns $ \(pat,mkRhs) -> (pat,) <$> mkRhs failure
    is_complete <- isCompleteMultiPattern (map fst eqns')
    pure $ Coq.Match scruts Nothing $
      [ Equation [pats] rhs | (pats, rhs) <- eqns' ] ++
      [ Equation [MultPattern (UnderscorePat <$ scruts)] failure | not is_complete ]
    -- Only add a catch-all clause if the the patterns can fail


--------------------------------------------------------------------------------

hasGuards :: GRHSs b e -> HasGuard
hasGuards (GRHSs NOEXTP [ L _ (GRHS NOEXTP [] _) ] _) = HasNoGuard
hasGuards _                             = HasGuard

convertGRHS :: LocalConvMonad r m
            => [ConvertedGuard m]
            -> GRHS GhcRn (LHsExpr GhcRn)
            -> ExceptT Qualid m (Term -> m Term)
convertGRHS extraGuards (GRHS NOEXTP gs rhs) = do
  convGuards <- (extraGuards ++) <$> convertGuard gs
  rhs <- convertLExpr rhs
  pure $ \failure -> guardTerm convGuards rhs failure
#if __GLASGOW_HASKELL__ >= 806
convertGRHS _ (XGRHS v) = noExtCon v
#endif

convertLGRHSList :: LocalConvMonad r m
                 => [ConvertedGuard m]
                 -> [LGRHS GhcRn (LHsExpr GhcRn)]
                 -> Term
                 -> m Term
convertLGRHSList extraGuards lgrhs failure = do
    let rhss = unLoc <$> lgrhs
    convRhss <- rights <$> traverse (runExceptT . convertGRHS extraGuards) rhss
    chainFallThroughs convRhss failure

convertGRHSs :: LocalConvMonad r m
             => [ConvertedGuard m]
             -> GRHSs GhcRn (LHsExpr GhcRn)
             -> Term
             -> m Term
convertGRHSs extraGuards GRHSs{..} failure =
    convertLocalBinds (unLoc grhssLocalBinds) $
      convertLGRHSList extraGuards grhssGRHSs failure
#if __GLASGOW_HASKELL__ >= 806
convertGRHSs _ (XGRHSs v) _ = noExtCon v
#endif

--------------------------------------------------------------------------------

data ConvertedGuard m = OtherwiseGuard
                      | BoolGuard      Term
                      | PatternGuard   Pattern Term
                      | LetGuard       (m Term -> m Term)

convertGuard :: LocalConvMonad r m => [GuardLStmt GhcRn] -> ExceptT Qualid m [ConvertedGuard m]
convertGuard [] = pure []
convertGuard gs = collapseGuards <$> traverse (toCond . unLoc) gs where
#if __GLASGOW_HASKELL__ >= 806
  toCond (BodyStmt _ e _bind _guard) =
#else
  toCond (BodyStmt e _bind _guard _PlaceHolder) =
#endif
    isTrueLExpr e >>= \case
      True  -> pure [OtherwiseGuard]
      False -> (:[]) . BoolGuard <$> convertLExpr e
  toCond (LetStmt NOEXTP (L _ binds)) =
    pure . (:[]) . LetGuard $ convertLocalBinds binds
#if __GLASGOW_HASKELL__ >= 806
  toCond (BindStmt _ pat exp _bind _fail) = do
#else
  toCond (BindStmt pat exp _bind _fail PlaceHolder) = do
#endif
    (pat', guards) <- runWriterT (convertLPat pat)
    exp'           <- convertLExpr exp
    pure $ PatternGuard pat' exp' : map BoolGuard guards
  toCond _ =
    convUnsupported "impossibly fancy guards"

  -- We optimize the code a bit, and combine
  -- successive boolean guards with andb
  collapseGuards = foldr addGuard [] . concat

  -- TODO: Add multi-pattern-guard case
  addGuard g [] =
    [g]
  addGuard (BoolGuard cond') (BoolGuard cond : gs) =
    BoolGuard (App2 (Var "andb") cond' cond) : gs
  addGuard g' (g:gs) =
    g':g:gs


-- Returns a function waiting for the "else case"
guardTerm :: LocalConvMonad r m =>
    [ConvertedGuard m] ->
    Term -> -- The guarded expression
    Term -> -- the failure expression
    m Term
guardTerm gs rhs failure = go gs where
  go [] =
    pure rhs
  go (OtherwiseGuard : gs) =
    go gs

  -- A little innocent but useful hack: Detect the pattern
  --     | foo `seq` False = …
  -- And hard-code that it fails
  go (BoolGuard (App2 "GHC.Prim.seq" _ p) : gs) = go (BoolGuard p : gs)
  go (BoolGuard "false" : _) = pure failure

  go (BoolGuard cond : gs) =
    ifThenElse <*> pure LinearIf <*> pure cond <*> go gs <*> pure failure
  -- if the pattern is exhaustive, don't include an otherwise case
  go (PatternGuard pat exp : gs) | isWildCoq pat = do
    guarded' <- go gs
    pure $ Coq.Match [MatchItem exp Nothing Nothing] Nothing
                     [ Equation [MultPattern [pat]] guarded' ]
  go (PatternGuard pat exp : gs) = do
    guarded' <- go gs
    pure $ Coq.Match [MatchItem exp Nothing Nothing] Nothing
                     [ Equation [MultPattern [pat]] guarded'
                     , Equation [MultPattern [UnderscorePat]] failure ]
  go (LetGuard bind : gs) =
    bind $ go gs

--------------------------------------------------------------------------------

-- Does not detect recursion/introduce `fix`
convertTypedBinding :: LocalConvMonad r m => Maybe Term -> HsBind GhcRn -> m (Maybe ConvertedBinding)
convertTypedBinding _convHsTy VarBind{}     = convUnsupported "[internal] `VarBind'"
convertTypedBinding _convHsTy AbsBinds{}    = convUnsupported "[internal?] `AbsBinds'"
convertTypedBinding _convHsTy PatSynBind{}  = convUnsupported "pattern synonym bindings"
#if __GLASGOW_HASKELL__ >= 806
convertTypedBinding _ (XHsBindsLR v) = noExtCon v
#endif
convertTypedBinding _convHsTy PatBind{..}   = do -- TODO use `_convHsTy`?
  -- TODO: Respect `skipped'?
  -- TODO: what if we need to rename this definition? (i.e. for a class member)
  ax <- view currentModuleAxiomatized
  if ax
    then
      liftIO $ Nothing <$ putStrLn "skipping a pattern binding in an axiomatized module" -- TODO: FIX HACK
      -- convUnsupported "pattern bindings in axiomatized modules"
    else
      runPatternT (convertLPat pat_lhs) >>= \case
        Left  _skipped      -> pure Nothing
        Right (pat, guards) -> Just . ConvertedPatternBinding pat <$> convertGRHSs (map BoolGuard guards) pat_rhs patternFailure
convertTypedBinding convHsTy FunBind{..}   = do
    name <- var ExprNS (unLoc fun_id)
    
    -- Skip it?  Axiomatize it?
    definitionTask name >>= \case
      SkipIt ->
        pure . Just $ SkippedBinding name
      
      RedefineIt def ->
        pure . Just $ RedefinedBinding name def
      
      AxiomatizeIt axMode ->
        let missingType = case axMode of
              SpecificAxiomatize -> convUnsupported "axiomatizing definitions without type signatures"
              GeneralAxiomatize  -> pure bottomType
        in Just . ConvertedAxiomBinding name <$> maybe missingType pure convHsTy
      
      TranslateIt -> do
        let (tvs, coqTy) =
              -- The @forall@ed arguments need to be brought into scope
              let peelForall (Forall tvs body) = first (NEL.toList tvs ++) $ peelForall body
                  peelForall ty                = ([], ty)
              in maybe ([], Nothing) (second Just . peelForall) convHsTy
              -- in maybe ([], Nothing) (second Just . peelForall) (Just $ Qualid $ Bare "test")


        let tryCollapseLet defn = do
              view (edits.collapsedLets.contains name) >>= \case
                True  -> collapseLet name defn
                           & maybe (convUnsupported "collapsing non-`let x=… in x` lets") pure
                False -> pure defn
        
        defn <-
          tryCollapseLet =<<
            if all (null . m_pats . unLoc) . unLoc $ mg_alts fun_matches
            then case unLoc $ mg_alts fun_matches of
                   [L _ (GHC.Match NOEXTP _ [] grhss)] -> convertGRHSs [] grhss patternFailure
                   _ -> convUnsupported "malformed multi-match variable definitions"
            else do
              skipEqns <- view $ edits.skippedEquations.at name.non mempty
              uncurry Fun <$> convertFunction skipEqns fun_matches

        addScope <- maybe id (flip InScope) <$> view (edits.additionalScopes.at (SPValue, name))
        
        pure . Just . ConvertedDefinitionBinding $ ConvertedDefinition name tvs coqTy (addScope defn)

collapseLet :: Qualid -> Term -> Maybe Term
collapseLet outer (Let x args _oty defn (Qualid x')) | x == x' =
  Just . maybeFun args $ case defn of
    Fix (FixOne (FixBody f args' _mord _oty body)) -> Fun args' $ subst1 f (Qualid outer) body
    _                                              -> defn
collapseLet _ _ =
  Nothing

wfFix :: ConversionMonad r m => TerminationArgument -> FixBody -> m Term
wfFix Deferred (FixBody ident argBinders Nothing Nothing rhs)
 = pure $ App1 (Qualid deferredFixN) $ Fun (mkBinder Explicit (Ident ident) NEL.<| argBinders ) rhs
  where
    deferredFixN = qualidMapBase (<> T.pack (show (NEL.length argBinders)))
        "GHC.DeferredFix.deferredFix"

wfFix (WellFoundedTA order) (FixBody ident argBinders Nothing Nothing rhs)
 = do (rel, measure) <- case order of
        MeasureOrder_ measure Nothing    -> pure ("Coq.Init.Peano.lt", measure)
        MeasureOrder_ measure (Just rel) -> pure (rel, measure)
        WFOrder_ rel arg                 -> pure (rel, Qualid arg)
      pure . appList (Qualid wfFixN) $ map PosArg
        [ rel
        , Fun argBinders measure
        , Underscore
        , Fun (argBinders NEL.|> mkBinder Explicit (Ident ident)) rhs
        ]
  where
    wfFixN = qualidMapBase (<> T.pack (show (NEL.length argBinders)))
        "GHC.Wf.wfFix"

wfFix Corecursive fb = pure . Cofix $ FixOne fb

wfFix StructOrderTA{} (FixBody ident _ _ _ _) = convUnsupportedIn
  "well-founded recursion does not include structural recursion"
  "fixpoint" (showP ident)

wfFix _ fb = convUnsupportedIn "well-founded recursion cannot handle annotations or types"
                               "fixpoint"
                               (showP $ fb^.fixBodyName)

--------------------------------------------------------------------------------

-- find the first name in a pattern binding
patBindName :: ConversionMonad r m => Pat GhcRn -> m Qualid
patBindName p = case p of
  WildPat _ -> convUnsupported' ("no name in binding pattern")
  GHC.VarPat NOEXTP (L _ hsName)  -> var ExprNS hsName
  LazyPat NOEXTP p -> lpatBindName p
  GHC.AsPat NOEXTP (L _ hsName) _ -> var ExprNS hsName
  ParPat NOEXTP p -> lpatBindName p
  BangPat NOEXTP p -> lpatBindName p
#if __GLASGOW_HASKELL__ >= 806
  ListPat _ (p:_) -> lpatBindName p
  TuplePat _ (p:_) _ -> lpatBindName p
#else
  ListPat (p:_) _ _ -> lpatBindName p
  TuplePat (p:_) _ _ -> lpatBindName p
#endif
  _ -> convUnsupported' ("Cannot find name in pattern: " ++  GHC.showSDocUnsafe (GHC.ppr p))

lpatBindName :: ConversionMonad r m => LPat GhcRn -> m Qualid
lpatBindName = patBindName . unLPat

unLPat :: LPat GhcRn -> Pat GhcRn
toLPat :: String -> Pat GhcRn -> LPat GhcRn
#if __GLASGOW_HASKELL__ == 808
unLPat = id
toLPat _ = id
#else
unLPat = unLoc
toLPat = mkGeneralLocated
#endif

hsBindName :: ConversionMonad r m => HsBind GhcRn -> m Qualid
hsBindName defn = case defn of
    FunBind{fun_id = L _ hsName} -> var ExprNS hsName
    PatBind{pat_lhs = p} -> lpatBindName p

    _ -> convUnsupported' ( "non-function top level bindings: " ++ GHC.showSDocUnsafe (GHC.ppr defn))

-- | Warn and immediately return 'Nothing' for unsupported top-level bindings.
withHsBindName
  :: ConversionMonad r m => HsBind GhcRn -> (Qualid -> m (Maybe a)) -> m (Maybe a)
withHsBindName b continue = case b of
    FunBind{fun_id = L _ hsName} -> var ExprNS hsName >>= continue
    PatBind{pat_lhs = p} ->
      warnConvUnsupported' (getLoc p) "top-level pattern binding" $> Nothing
    PatSynBind NOEXTP PSB{psb_id = i} ->
      warnConvUnsupported' (getLoc i) "pattern synonym" $> Nothing
    VarBind{} -> convUnsupported' "[internal] `VarBind' can't be a top-level binding"
    AbsBinds{} -> convUnsupported' "[internal] `AbsBinds' can't be a top-level binding"
#if __GLASGOW_HASKELL__ >= 806
    PatSynBind NOEXTP (XPatSynBind v) -> noExtCon v
    XHsBindsLR v -> noExtCon v
#endif

-- This is where we switch from the global monad to the local monad
convertTypedModuleBinding :: ConversionMonad r m => Maybe Term -> HsBind GhcRn -> m (Maybe ConvertedBinding)
convertTypedModuleBinding ty defn =
  withHsBindName defn $ \name ->
    withCurrentDefinition name $ convertTypedBinding ty defn

convertTypedModuleBindings :: ConversionMonad r m
                           => [LHsBind GhcRn]
                           -> Map Qualid Signature
                           -> (ConvertedBinding -> m a)
                           -> Maybe (HsBind GhcRn -> GhcException -> m a)
                           -> m [a]
convertTypedModuleBindings = convertMultipleBindings convertTypedModuleBinding

-- | A variant of convertTypedModuleBinding that ignores the name in the HsBind
-- and uses the provided one instead
--
-- It also does not allow skipping or axiomatization, does not create fixpoints,
-- does not support a type, and always returns a binding (or fails with
-- convUnsupported).
--
-- It does, however, support redefinition.
convertMethodBinding :: ConversionMonad r m => Qualid -> HsBind GhcRn -> m ConvertedBinding
convertMethodBinding name VarBind{}     = convUnsupportedIn "[internal] `VarBind'"     "method" (showP name)
convertMethodBinding name AbsBinds{}    = convUnsupportedIn "[internal?] `AbsBinds'"   "method" (showP name)
convertMethodBinding name PatSynBind{}  = convUnsupportedIn "pattern synonym bindings" "method" (showP name)
convertMethodBinding name PatBind{}     = convUnsupportedIn "pattern bindings"         "method" (showP name)
convertMethodBinding name FunBind{..}   = withCurrentDefinition name $ do
  definitionTask name >>= \case
    SkipIt ->
      convUnsupported "skipping instance method definitions (without `skip method')"
    RedefineIt def ->
      pure $ RedefinedBinding name def
    AxiomatizeIt _ ->
      convUnsupported "axiomatizing instance method definitions"
    TranslateIt -> do
      defn <-
        if all (null . m_pats . unLoc) . unLoc $ mg_alts fun_matches
        then case unLoc $ mg_alts fun_matches of
               [L _ (GHC.Match NOEXTP _ [] grhss)] -> convertGRHSs [] grhss patternFailure
               _ -> convUnsupported "malformed multi-match variable definitions"
        else do
          skipEqns <- view $ edits.skippedEquations.at name.non mempty
          uncurry Fun <$> convertFunction skipEqns fun_matches
      pure $ ConvertedDefinitionBinding $ ConvertedDefinition name [] Nothing defn
#if __GLASGOW_HASKELL__ >= 806
convertMethodBinding _ (XHsBindsLR v) = noExtCon v
#endif

convertTypedBindings :: LocalConvMonad r m
                     => [LHsBind GhcRn] -> Map Qualid Signature
                     -> (ConvertedBinding -> m a)
                     -> Maybe (HsBind GhcRn -> GhcException -> m a)
                     -> m [a]
convertTypedBindings = convertMultipleBindings convertTypedBinding

convertMultipleBindings :: ConversionMonad r m
                        => (Maybe Term -> HsBind GhcRn -> m (Maybe ConvertedBinding))
                        -> [LHsBind GhcRn]
                        -> Map Qualid Signature
                        -> (ConvertedBinding -> m a)
                        -> Maybe (HsBind GhcRn -> GhcException -> m a)
                        -> m [a]
convertMultipleBindings convertSingleBinding defns0 sigs build mhandler =
  let defns = sortOn getLoc defns0
      (handler, wrap) = case mhandler of
        Just handler -> ( uncurry handler
                        , \defn -> ghandle $ pure . Left . (defn,))
        Nothing      -> ( const $ throwProgramError
          "INTERNAL ERROR: convertMultipleBindings tried to both handle and ignore an exception"
                            -- Safe because the only place `Left' is introduced
                            -- is in the previous case branch
                        , flip const )
  in traverse (either handler build) <=< addRecursion <=< fmap catMaybes . for defns $ \(L _ defn) ->
       -- 'MaybeT' is responsible for handling the skipped definitions, and
       -- nothing else
       runMaybeT . wrap defn . fmap Right $ do
         ty <- case defn of
                 FunBind{fun_id = L _ hsName} ->
                   fmap (fmap sigType) . (`lookupSig` sigs) =<< var ExprNS hsName
                 _ ->
                   pure Nothing
         MaybeT $ convertSingleBinding ty defn

-- ALMOST a 'ConvertedDefinition', but:
--   (a) It's guaranteed to have arguments; and
--   (b) We store two types: the result type AFTER the argument types
--       ('rdResultType'), and the full type including the argument types
--       ('rdFullType')
data RecDef = RecDef { rdName       :: !Qualid
                     , rdArgs       :: !Binders
                     , rdStruct     :: !(Maybe Order)
                     , rdResultType :: !(Maybe Term)
                     , rdFullType   :: !(Maybe Term)
                     , rdBody       :: !Term }
            deriving (Eq, Ord, Show, Read)

-- CURRENT IMPLEMENTATION: If we can't move the type to arguments, then:
--   * If it was translated, fail-safe, and translate without the type
--   * If it was specified, abort
-- We can't unilaterally abort unless we can change type signatures.

rdToFixBody :: RecDef -> FixBody
rdToFixBody RecDef{..} = FixBody rdName rdArgs rdStruct rdResultType rdBody

rdToLet :: RecDef -> Term -> Term
rdToLet RecDef{..} = Let rdName (toList rdArgs) rdResultType rdBody

rdStripResultType :: RecDef -> RecDef
rdStripResultType rd = rd{rdResultType = Nothing}

splitInlinesWith :: Foldable f => Set Qualid -> f RecDef -> Maybe (Map Qualid RecDef, NonEmpty RecDef)
splitInlinesWith inlines =
  bitraverse (pure . fold) nonEmpty .: mapPartitionEithers $ \rd@RecDef{..} ->
    if rdName `elem` inlines
    then Left $ M.singleton rdName rd
    else Right rd

data RecType = Standalone | Mutual deriving (Eq, Ord, Enum, Bounded, Show, Read)

mutualRecursionInlining :: ConversionMonad r m => NonEmpty RecDef -> m (Map Qualid (RecType, RecDef))
mutualRecursionInlining mutGroup = do
  -- TODO: Names of recursive functions in inlining errors
  
  inlines      <- view $ edits.inlinedMutuals
  (lets, recs) <- splitInlinesWith inlines mutGroup
                    & maybe (editFailure "can't inline every function in a mutually-recursive group") pure
  
  let rdFVs   = getFreeVars . rdBody
      letUses = rdFVs <$> lets
      letDeps = transitiveClosure Reflexive letUses

  orderedLets <- for (topoSortEnvironmentWith id letUses) $ \case
    solo :| []  -> pure solo
    _    :| _:_ -> editFailure "recursion forbidden amongst inlined mutually-recursive functions"
  
  let recMap = flip foldMap recs $ \rd ->
        let neededLets  = foldMap (M.findWithDefault mempty ?? letDeps) $ rdFVs rd
            inlinedDeps = filter (`elem` neededLets) orderedLets
        in M.singleton (rdName rd)
                       (Mutual, rd{rdBody = foldr (rdToLet . (lets M.!)) (rdBody rd) inlinedDeps})
  
  pure $ ((Standalone,) <$> lets) <> recMap

addRecursion :: ConversionMonad r m => [Either e ConvertedBinding] -> m [Either e ConvertedBinding]
addRecursion eBindings = do
  fixedBindings <-  M.fromList . fmap (view convDefName &&& id) . foldMap toList
                <$> traverse fixConnComp (stronglyConnCompNE
                      [ (cd, cd^.convDefName, S.toAscList . getFreeVars $ cd^.convDefBody)
                      | Right (ConvertedDefinitionBinding cd) <- eBindings ])
      
  pure . topoSortByVariablesBy ErrOrVars M.empty . flip map eBindings $ \case
    Right (ConvertedDefinitionBinding cd) -> case M.lookup (cd^.convDefName) fixedBindings of
      Just cd' -> Right $ ConvertedDefinitionBinding cd'
      Nothing  -> error "INTERNAL ERROR: lost track of converted definition during mutual recursion check"
    untouched ->
      untouched
  where
    fixConnComp (cd :| []) | cd^.convDefName `notElem` getFreeVars (cd^.convDefBody) =
      pure $ cd :| []
    fixConnComp cds = do
      (commonArgs, cds) <- splitArgs cds
      tbodies <- for cds fixConvertedDefinition

      let bodies = fst <$> tbodies

      let nonstructural = listToMaybe [t | (_, Just t) <- toList tbodies, isNonstructural t]
          isNonstructural (StructOrderTA _) = False
          isNonstructural _ = True

      let getInfo = fmap $ rdName &&& rdFullType
      
      (fixFor, recInfos, extraDefs) <- case (nonstructural, bodies) of
        (Just order, body1 :| []) -> do
          fixed <- wfFix order . rdToFixBody $ rdStripResultType body1
          pure (const fixed, getInfo bodies, [])
        
        (Just _, _ :| _ : _) ->
          convUnsupportedIn "non-structural mutual recursion" "definitions"
                            (explainStrItems (showP . rdName) "" "," "and" "" "" bodies)
        
        (Nothing, body1 :| []) ->
          pure (const . Fix . FixOne $ rdToFixBody body1, getInfo bodies, [])
        
        (Nothing, _ :| _ : _) -> do
          mutRecInfo <- mutualRecursionInlining bodies
          let (recs', lets) = flip mapPartitionEithers cds $ \cd ->
                case M.lookup (cd^.convDefName) mutRecInfo of
                  Just (Standalone, _)  -> Right $ cd & convDefArgs %~ (commonArgs ++)
                  Just (Mutual,     rd) -> Left rd
                  Nothing               -> error "INTERNAL ERROR: lost track of mutually-recursive function"
              recs = fromMaybe (error "INTERNAL ERROR: \
                                      \all mutually-recursive functions in this group vanished!")
                   $ nonEmpty recs'
          
          let fixFor = case recs of
                body1 :| []              ->
                  const . Fix . FixOne $ rdToFixBody body1
                body1 :| body2 : bodies' ->
                  Fix . FixMany (rdToFixBody body1) (rdToFixBody <$> (body2 :| bodies'))
          
          pure (fixFor, getInfo recs, lets)
          
      let recDefs = recInfos <&> \(name,mty) ->
            ConvertedDefinition { _convDefName = name
                                , _convDefArgs = commonArgs
                                , _convDefType = mty
                                , _convDefBody = fixFor name }
      pure $ recDefs ++> extraDefs

fixConvertedDefinition ::
  ConversionMonad r m => ConvertedDefinition -> m (RecDef, Maybe TerminationArgument)
fixConvertedDefinition (ConvertedDefinition{_convDefBody = Fun args body, ..}) = do
  let fullType = maybeForall _convDefArgs <$> _convDefType
      allArgs = _convDefArgs <++ args
      (resultType, convArgs') = case fullType of
        Just ty | Right (ty', args', UTIBIsTypeTooShort False) <- useTypeInBinders ty allArgs ->
          (Just ty', args')
        _ -> (Nothing, allArgs)
  termination <- view (edits.termination.at _convDefName)
  struct <- case termination of
    Just (StructOrderTA (StructId_  n)) -> (pure . Just) (StructOrder n)
    Just (StructOrderTA (StructPos_ i)) ->
      case args ^? elementOf (traverse . binderNames) (i - 1) of
        Just (Ident name) -> (pure . Just) (StructOrder name)
        Just UnderscoreName ->
          throwProgramError ("error: function " ++ showP _convDefName ++ ": its " ++ show i ++ "-th argument is unnamed")
        Nothing -> throwProgramError ("error: function " ++ showP _convDefName ++ " has fewer than " ++ show i ++ " arguments")
    _ -> pure Nothing
  let b = RecDef
        { rdName       = _convDefName
        , rdArgs       = convArgs'
        , rdStruct     = struct
        , rdResultType = resultType
        , rdFullType   = fullType
        , rdBody       = body }
  pure (b, termination)
fixConvertedDefinition cd =
  convUnsupportedIn "recursion through non-lambda value" "definition" (showP $ cd^.convDefName)

splitArgs :: (ConversionMonad r m, Traversable t) => t ConvertedDefinition -> m ([Binder], t ConvertedDefinition)
splitArgs cds = do
  polyrec <- findM (\rd -> view $ edits.polyrecs.at (_convDefName rd)) cds
  case polyrec of
    Nothing -> pure (splitCommonPrefixOf convDefArgs cds)
    Just _  -> pure ([], cds)

--------------------------------------------------------------------------------

convertLocalBinds :: LocalConvMonad r m => HsLocalBinds GhcRn -> m Term -> m Term
#if __GLASGOW_HASKELL__ >= 806
convertLocalBinds (XHsLocalBindsLR v) _ = noExtCon v
convertLocalBinds (HsValBinds _ (ValBinds{})) _ =
  convUnsupported "Unexpected ValBinds in post-renamer AST"

convertLocalBinds (HsValBinds _ (XValBindsLR (NValBinds recBinds lsigs))) body = do
#else
convertLocalBinds (HsValBinds (ValBindsIn{})) _ =
  convUnsupported "Unexpected ValBindsIn in post-renamer AST"

convertLocalBinds (HsValBinds (ValBindsOut recBinds lsigs)) body = do
#endif
  sigs     <- convertLSigs lsigs
  -- We are not actually using the rec_flag from GHC, because due to renamings
  -- or `redefinition` edits, maybe the group is no longer recursive.
  convDefss <- for recBinds $ \(_rec_flag, mut_group) ->
    convertTypedBindings (bagToList mut_group) sigs pure Nothing
  let convDefs = concat convDefss

  let fromConvertedBinding cb body = case cb of
        ConvertedDefinitionBinding (ConvertedDefinition{..}) ->
          pure (Let _convDefName _convDefArgs _convDefType _convDefBody body)
        ConvertedPatternBinding pat term -> do
          is_complete <- isCompleteMultiPattern [MultPattern [pat]]
          pure $ Coq.Match [MatchItem term Nothing Nothing] Nothing $
              [ Equation [MultPattern [pat]] body] ++
              [ Equation [MultPattern [UnderscorePat]] patternFailure | not is_complete ]
        ConvertedAxiomBinding ax _ty ->
          convUnsupported $ "local axiom `" ++ T.unpack (qualidToIdent ax) ++ "' unsupported"
        RedefinedBinding _nm _sn -> convUnsupported "redefining local bindings"
        SkippedBinding _nm -> convUnsupported "skipping local binding"
      
  (foldrM fromConvertedBinding ?? convDefs) =<< body

convertLocalBinds (HsIPBinds NOEXTP _) _ =
  convUnsupported "local implicit parameter bindings"
convertLocalBinds (EmptyLocalBinds NOEXTP) body =
  body

--------------------------------------------------------------------------------

-- Create `let x := rhs in genBody x`
-- Unless the rhs is very small, in which case it creates `genBody rhs`
bindIn :: LocalConvMonad r m => Text -> Term -> (Term -> m Term) -> m Term
bindIn _ rhs@(Qualid _) genBody = genBody rhs
bindIn tmpl rhs genBody = do
  j <- genqid tmpl
  body <- genBody (Qualid j)
  pure $ smartLet j rhs body


-- This prevents the pattern conversion code to create
-- `let j_24__ := … in j_24__`
-- and a few other common and obviously stupid forms
--
-- Originally, we avoided pushing the `rhs` past a binder. But it turned out
-- that we need to do that to get useful termination proof obligations out of
-- program fixpoint. So now we move the `rhs` past a binder if that binder is fresh (i.e. cannot be captured).
-- Let’s cross our fingers that we calculate all free variables properly.
smartLet :: Qualid -> Term -> Term -> Term
-- Move into the else branch
smartLet ident rhs (If is c Nothing t e)
    | ident `S.notMember` getFreeVars c
    , ident `S.notMember` getFreeVars t
    = If is c Nothing t (smartLet ident rhs e)
-- Move into the scrutinee
smartLet ident rhs
    (Coq.Match [MatchItem t Nothing Nothing] Nothing eqns)
    | ident `S.notMember` getFreeVars eqns
    = Coq.Match [MatchItem (smartLet ident rhs t) Nothing Nothing] Nothing eqns
-- Move into the last equation
-- (only if not mentioned in any earlier equation and only if no matched
-- variables is caught)
smartLet ident rhs
    (Coq.Match scruts Nothing eqns)
    | ident `S.notMember` getFreeVars (fmap NoBinding scruts)
    , let intoEqns [] = Just []
          intoEqns [Equation pats body] = do
            let bound = S.fromList $ foldMap definedBy pats
            guard $ ident `S.notMember` bound
            guard $ S.null $ bound `S.intersection` getFreeVars rhs
            return [Equation pats (smartLet ident rhs body)]
          intoEqns (e:es) = do
            guard $ ident `S.notMember` getFreeVars e
            (e:) <$> intoEqns es
    , Just eqns' <- intoEqns eqns
    = Coq.Match scruts Nothing eqns'
smartLet ident rhs (Qualid v) | ident == v = rhs
smartLet ident rhs body = Let ident [] Nothing rhs body

patternFailure :: Term
patternFailure = "GHC.Err.patternFailure"

missingValue :: Term
missingValue = "missingValue"

-- | Program does not work nicely with if-then-else, so if we believe we are
-- producing a term that ends up in a Program Fixpoint or Program Definition,
-- then desguar if-then-else using case statements.
ifThenElse :: LocalConvMonad r m => m (IfStyle -> Term -> Term -> Term -> Term)
ifThenElse = useProgramHere >>= \case
    False -> pure $ evalConstScrut IfBool
    True ->  pure $ evalConstScrut IfCase
  where
    -- Reduce `if true` and `if false`
    evalConstScrut :: (IfStyle -> Term -> Term -> Term -> Term)
                   -> (IfStyle -> Term -> Term -> Term -> Term)
    evalConstScrut _ _ "true"  e _ = e
    evalConstScrut _ _ "false" _ e = e
    evalConstScrut ifComb is scrut e1 e2 = ifComb is scrut e1 e2
