-- | This module contains the implementation of Mimer, the current
-- implementation of the auto interactive command (C-c C-a) and the successor of
-- Agsy.
--
-- The overall idea is that Mimer gathers a collection of "components" that it
-- could use for building a solution and tries to refine the goal iteratively
-- using these components. Components include global definitions, local variables,
-- let-bound variables, and recursive calls to the function being defined.
--
-- Mimer manages multiple branches of the search at the same time and assigns a
-- cost to each branch, which is the sum of the costs of all its components. The
-- cost of a component in turn is determined by its type and the number of new
-- metas it introduces.
--
-- A branch can be refined by picking one of its unsolved metavariables and
-- refining it with all available components, resulting in a number of new
-- branches (each one with a higher cost than the original).
--
-- Mimer iteratively refines the branch with the lowest cost until it finds a
-- solution or runs out of time.

module Agda.Mimer.Mimer
  ( MimerResult(..)
  , mimer
  )
  where

import Prelude hiding (null)

import Control.DeepSeq (force, NFData(..))
import Control.Monad
import Control.Monad.Except (catchError)
import Control.Monad.Error.Class (MonadError)
import Control.Monad.IO.Class (liftIO)
import Control.Monad.Reader (ReaderT(..), runReaderT, asks, ask, lift)
import Data.Function (on)
import Data.Functor ((<&>))
import Data.List (sortOn, intersect, transpose, (\\))
import qualified Data.List.NonEmpty as NonEmptyList (head)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Maybe (maybeToList, fromMaybe, maybe, isNothing)
import Data.PQueue.Min (MinQueue)
import qualified Data.PQueue.Min as Q
import GHC.Generics (Generic)
import qualified Text.PrettyPrint.Boxes as Box
import qualified Data.Text as Text

import qualified Agda.Benchmarking as Bench
import Agda.Interaction.MakeCase (makeCase, getClauseZipperForIP, recheckAbstractClause)
import Agda.Syntax.Abstract (Expr(AbsurdLam))
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Abstract.Name (QName(..), Name(..))
import Agda.Syntax.Common (InteractionId(..), MetaId(..), ArgInfo(..), defaultArgInfo, Origin(..), ConOrigin(..), Hiding(..), setOrigin, NameId, Nat, namedThing, Arg(..), setHiding, getHiding, ProjOrigin(..), rangedThing, woThing, nameOf, visible)
import Agda.Syntax.Common.Pretty (Pretty)
import qualified Agda.Syntax.Common.Pretty as P
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Info (pattern UnificationMeta, exprNoRange)
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars (AllMetas(..))
import Agda.Syntax.Internal.Pattern (clausePerm)
import Agda.Syntax.Position (Range, rangeFile, rangeFilePath, noRange)
import qualified Agda.Syntax.Scope.Base as Scope
import Agda.Syntax.Translation.InternalToAbstract (reify, NamedClause(..), blankNotInScope)
import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete_)

import Agda.TypeChecking.Primitive (getBuiltinName)
import Agda.TypeChecking.Constraints (noConstraints)
import Agda.TypeChecking.Datatypes (isDataOrRecord)
import Agda.TypeChecking.Conversion (equalType)
import Agda.TypeChecking.Empty (isEmptyType)
import Agda.TypeChecking.Free (flexRigOccurrenceIn, freeVars)
import Agda.TypeChecking.Level (levelType)
import Agda.TypeChecking.MetaVars (newValueMeta)
import Agda.TypeChecking.Monad -- (MonadTCM, lookupInteractionId, getConstInfo, liftTCM, clScope, getMetaInfo, lookupMeta, MetaVariable(..), metaType, typeOfConst, getMetaType, MetaInfo(..), getMetaTypeInContext)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records (isRecord, isRecursiveRecord)
import Agda.TypeChecking.Reduce (reduce, instantiateFull, instantiate)
import Agda.TypeChecking.Rules.LHS.Problem (AsBinding(..))
import Agda.TypeChecking.Rules.Term  (makeAbsurdLambda)
import Agda.TypeChecking.Substitute (apply, applyE, piApply, NoSubst(..), pattern TelV, telView')
import Agda.TypeChecking.Telescope (piApplyM, flattenTel, teleArgs)

import Agda.Utils.Benchmark (billTo)
import Agda.Utils.FileName (filePath)
import Agda.Utils.Functor ((<.>))
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Maybe (catMaybes)
import Agda.Utils.Monad (ifM, and2M)
import qualified Agda.Utils.Maybe.Strict as SMaybe
-- import Agda.Utils.Permutation (idP, permute, takeP)
import Agda.Utils.Null
import Agda.Utils.Time (CPUTime(..), getCPUTime, fromMilliseconds)
import Agda.Utils.Tuple (mapFst, mapSnd)
import Agda.Utils.FileName (AbsolutePath(..))

import Agda.Mimer.Options

import System.IO.Unsafe (unsafePerformIO)
import Data.IORef (IORef, writeIORef, readIORef, newIORef, modifyIORef')

-- Temporary (used for custom cost verbosity hack)
import qualified Agda.Utils.Maybe.Strict as Strict
import qualified Agda.Utils.Trie as Trie
import Agda.Interaction.Base (Rewrite(..))
import Agda.Interaction.BasicOps (normalForm)
import Agda.Interaction.Options.Base (parseVerboseKey)
import Agda.Utils.List (lastWithDefault)

data MimerResult
  = MimerExpr String -- ^ Returns 'String' rather than 'Expr' because the give action expects a string.
  | MimerClauses QName [A.Clause]
  | MimerList [(Int, String)]
  | MimerNoResult
  deriving (Generic)

instance NFData MimerResult

-- | Entry point.
--   Run Mimer on the given interaction point, returning the desired solution(s).
--   Also debug prints timing statistics.
mimer :: MonadTCM tcm
  => Rewrite         -- ^ Degree of normalization of solution terms.
  -> InteractionId   -- ^ Hole to run on.
  -> Range           -- ^ Range of hole (for parse errors).
  -> String          -- ^ Content of hole (to parametrize Mimer).
  -> tcm MimerResult
mimer norm ii rng argStr = liftTCM $ do
    reportSDoc "mimer.top" 10 do
      "Running Mimer on interaction point" <+> pretty ii <+> "with argument string" <+> text (show argStr)

    start <- liftIO $ getCPUTime

    opts <- parseOptions ii rng argStr
    reportS "mimer.top" 15 ("Mimer options: " ++ show opts)

    -- Andreas, 2025-04-16, changing the plain getTC/putTC bracket to localTCState.
    -- localTCState should be used by default,
    -- it keeps the Statistics about metas and constraints.
    -- Was there a reason to use plain getTC/putTC or is it "don't care" since
    -- mimer is an interactive command and no one looks at the statistics?
    sols <- localTCState $ runSearch norm opts ii rng

    -- Turn the solutions into the desired results (first solution or list of solutions).
    sol <- case drop (optSkip opts) $ zip [0..] sols of
          [] -> do
            reportSLn "mimer.top" 10 "No solution found"
            return MimerNoResult
          sols' | optList opts -> pure $ MimerList [ (i, s) | (i, MimerExpr s) <- sols' ]
          (_, sol) : _ -> do
            reportSDoc "mimer.top" 10 $ "Solution:" <+> prettyTCM sol
            return sol

    -- Print timing statistic.
    stop <- liftIO $ getCPUTime
    let time = stop - start
    reportSDoc "mimer.top" 10 ("Total elapsed time:" <+> pretty time)
    verboseS "mimer.stats" 50 $ writeTime ii (if null sols then Nothing else Just time)

    return sol


-- Order to try things in:
-- 1. Local variables (including let-bound)
-- 2. Data constructors
-- 3. Where clauses
-- 4. Lambda abstract
-- Other: Equality, empty type, record projections
-- - If we only use constructors if the target type is a data type, we might
--   generate η-reducible expressions, e.g. λ xs → _∷_ 0 xs


------------------------------------------------------------------------------
-- * Data types
------------------------------------------------------------------------------

type SM a = ReaderT SearchOptions TCM a

data SearchBranch = SearchBranch
  { sbTCState :: TCState
  , sbGoals :: [Goal]
  , sbCost :: Int
  , sbCache :: Map CheckpointId ComponentCache
  , sbComponentsUsed :: Map Name Int -- ^ Number of times each component has been used
  }
  deriving (Generic)
instance NFData SearchBranch

-- | NOTE: Equality is only on the fields `sbCost` and `sbGoals`
instance Eq SearchBranch where
  sb1 == sb2 = sbCost sb1 == sbCost sb2 && sbGoals sb1 == sbGoals sb2

-- TODO: Explain
instance Ord SearchBranch where
  compare = compare `on` sbCost

-- Map source component to generated components
type ComponentCache = Map Component (Maybe [Component])

data Goal = Goal
  { goalMeta :: MetaId
  }
  deriving (Generic)
instance NFData Goal

-- TODO: Is this a reasonable Eq instance?
instance Eq Goal where
  g1 == g2 = goalMeta g1 == goalMeta g2

-- | Components that are not changed during search. Components that do change
-- (local variables and let bindings) are stored in each 'SearchBranch'.
data BaseComponents = BaseComponents
  { hintFns :: [Component]
  , hintDataTypes :: [Component]
  , hintRecordTypes :: [Component]
  , hintAxioms :: [Component]
  -- ^ Excluding those producing Level
  , hintLevel :: [Component]
  -- ^ A definition in a where clause
  , hintProjections :: [Component]
  -- ^ Variables that are candidates for arguments to recursive calls
  , hintThisFn :: Maybe Component
  , hintLetVars :: [Open Component]
  , hintRecVars :: Open [(Term, NoSubst Term Int)] -- ^ Variable terms and which argument they come from
  , hintSplitVars :: Open [Term]
  }
  deriving (Generic)

instance NFData BaseComponents

type CompId = Int
data Component = Component
  { compId    :: CompId -- ^ Unique id for the component. Used for the cache.
  , compName  :: Maybe Name -- ^ Used for keeping track of how many times a component has been used
  , compPars  :: Nat -- ^ How many arguments should be dropped (e.g. constructor parameters)
  , compTerm  :: Term
  , compType  :: Type
  , compRec   :: Bool -- ^ Is this a recursive call
  , compMetas :: [MetaId]
  , compCost  :: Cost
  }
  deriving (Eq, Generic)

instance NFData Component

-- TODO: Is this reasonable?
instance Ord Component where
  compare = compare `on` compId

data SearchStepResult
  = ResultExpr Expr
  | ResultClauses [A.Clause]
  | OpenBranch SearchBranch
  | NoSolution
  deriving (Generic)
instance NFData SearchStepResult


data SearchOptions = SearchOptions
  { searchBaseComponents :: BaseComponents
  , searchHintMode :: HintMode
  , searchTimeout :: MilliSeconds
  , searchGenProjectionsLocal :: Bool
  , searchGenProjectionsLet :: Bool
  , searchGenProjectionsExternal :: Bool
  , searchGenProjectionsRec :: Bool
  , searchSpeculateProjections :: Bool
  , searchTopMeta :: MetaId
  , searchTopEnv :: TCEnv
  , searchTopCheckpoint :: CheckpointId
  , searchInteractionId :: InteractionId
  , searchFnName :: Maybe QName
  , searchCosts :: Costs
  , searchStats :: IORef MimerStats
  , searchRewrite :: Rewrite
  , searchBuiltinFlat :: Maybe QName
      -- Cache BUILTIN_FLAT for issue #7662 workaround
  }

type Cost = Int
data Costs = Costs
  { costLocal :: Cost
  , costFn :: Cost
  , costDataCon :: Cost
  , costRecordCon :: Cost
  , costSpeculateProj :: Cost
  , costProj :: Cost
  , costAxiom :: Cost
  , costLet :: Cost
  , costLevel :: Cost
  , costSet :: Cost -- Should probably be replaced with multiple different costs
  , costRecCall :: Cost
  , costNewMeta :: Cost -- ^ Cost of a new meta-variable appearing in a non-implicit position
  , costNewHiddenMeta :: Cost -- ^ Cost of a new meta-variable appearing in an implicit position
  , costCompReuse :: Nat -> Cost -- ^ Cost of reusing a component @n@ times. Only counted when @n>1@.
  }

noCost :: Cost
noCost = 0

defaultCosts :: Costs
defaultCosts = Costs
  { costLocal = 3
  , costFn = 10
  , costDataCon = 3
  , costRecordCon = 3
  , costSpeculateProj = 20
  , costProj = 3
  , costAxiom = 10
  , costLet = 5
  , costLevel = 3
  , costSet = 10
  , costRecCall = 8
  , costNewMeta = 10
  , costNewHiddenMeta = 1
  , costCompReuse = \uses -> 10 * (uses - 1) ^ 2
  }

------------------------------------------------------------------------------
-- * Helper functions
------------------------------------------------------------------------------

predNat :: Nat -> Nat
predNat n | n > 0 = n - 1
          | n == 0 = 0
          | otherwise = error "predNat of negative value"

getRecordFields :: (HasConstInfo tcm, MonadTCM tcm) => QName -> tcm [QName]
getRecordFields = fmap (map unDom . recFields . theDef) . getConstInfo

allOpenMetas :: (AllMetas t, ReadTCState tcm) => t -> tcm [MetaId]
allOpenMetas t = do
  openMetas <- getOpenMetas
  return $ allMetas (:[]) t `intersect` openMetas

getOpenComponent :: (MonadTCM tcm, MonadDebug tcm) => Open Component -> tcm Component
getOpenComponent openComp = do
  let comp = openThing openComp
  reportSDoc "mimer.components.open" 40 $ "Opening component" <+> prettyTCM (compId comp) <+> prettyTCM (compName comp)
  term <- getOpen $ compTerm <$> openComp
  reportSDoc "mimer.components.open" 40 $ "  term = " <+> prettyTCM term
  typ <- getOpen $ compType <$> openComp
  reportSDoc "mimer.components.open" 40 $ "  typ  =" <+> prettyTCM typ
  when (not $ null $ compMetas comp) __IMPOSSIBLE__
  return Component
    { compId    = compId comp
    , compName  = compName comp
    , compPars  = compPars comp
    , compTerm  = term
    , compType  = typ
    , compRec   = compRec comp
    , compMetas = compMetas comp
    , compCost  = compCost comp
    }

mkComponent :: CompId -> [MetaId] -> Cost -> Maybe Name -> Nat -> Term -> Type -> Component
mkComponent cId metaIds cost mName pars term typ = Component
  { compId    = cId
  , compName  = mName
  , compPars  = pars
  , compTerm  = term
  , compType  = typ
  , compRec   = False
  , compMetas = metaIds
  , compCost  = cost }

mkComponentQ :: CompId -> Cost -> QName -> Nat -> Term -> Type -> Component
mkComponentQ cId cost qname = mkComponent cId [] cost (Just $ qnameName qname)

noName :: Maybe Name
noName = Nothing

newComponent :: MonadFresh CompId m => [MetaId] -> Cost -> Maybe Name -> Nat -> Term -> Type -> m Component
newComponent metaIds cost mName pars term typ = fresh <&> \cId -> mkComponent cId metaIds cost mName pars term typ

newComponentQ :: MonadFresh CompId m => [MetaId] -> Cost -> QName -> Nat -> Term -> Type -> m Component
newComponentQ metaIds cost qname pars term typ = fresh <&> \cId -> mkComponent cId metaIds cost (Just $ qnameName qname) pars term typ

addCost :: Cost -> Component -> Component
addCost cost comp = comp { compCost = cost + compCost comp }

addBranchGoals :: [Goal] -> SearchBranch -> SearchBranch
addBranchGoals goals branch = branch {sbGoals = goals ++ sbGoals branch}

withBranchState :: SearchBranch -> SM a -> SM a
withBranchState br ma = do
  putTC (sbTCState br)
  ma

withBranchAndGoal :: SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal br goal ma = inGoalEnv goal $ withBranchState br ma

inGoalEnv :: Goal -> SM a -> SM a
inGoalEnv goal  ret = do
  reportSDoc "mimer.env" 70 $ "going into environment of goal" <+> prettyTCM (goalMeta goal)
  withMetaId (goalMeta goal) ret

-- | Take the first goal off a search branch.
--   Precondition: the set of goals is non-empty.
nextGoal :: SearchBranch -> (Goal, SearchBranch)
nextGoal branch =
  case sbGoals branch of
    [] -> __IMPOSSIBLE__
    goal : goals -> (goal, branch{ sbGoals = goals })

-- TODO: Rename (see metaInstantiation)
getMetaInstantiation :: (MonadTCM tcm, PureTCM tcm, MonadDebug tcm, MonadInteractionPoints tcm, MonadFresh NameId tcm)
  => MetaId -> tcm (Maybe Expr)
getMetaInstantiation = metaInstantiation >=> traverse (instantiateFull >=> reify)

metaInstantiation :: (MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) => MetaId -> tcm (Maybe Term)
metaInstantiation metaId = lookupLocalMeta metaId <&> mvInstantiation >>= \case
  InstV inst -> return $ Just $ instBody inst
  _ -> return Nothing

-- TODO: why not also accept pattern record types here?
isTypeDatatype :: (MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) => Type -> tcm Bool
isTypeDatatype typ = liftTCM do
  reduce typ <&> unEl >>= isDataOrRecord <&> \case
    Just (_, IsData) -> True
    _ -> False

------------------------------------------------------------------------------
-- * Components
------------------------------------------------------------------------------

-- | NOTE: Collects components from the *current* context, not the context of
-- the 'InteractionId'.
collectComponents :: Options -> Costs -> InteractionId -> Maybe QName -> [QName] -> MetaId -> TCM BaseComponents
collectComponents opts costs ii mDefName whereNames metaId = do

  lhsVars <- collectLHSVars ii
  let recVars = lhsVars <&> \ vars -> [ (tm, NoSubst i) | (tm, Just i) <- vars ]

  -- TODO: implement case splitting
  -- splitVars <- getSplitVars lhsVars
  splitVars <- makeOpen []

  -- Prepare the initial component record
  letVars <- getLetVars (costLet costs)
  let components = BaseComponents
        { hintFns = []
        , hintDataTypes = []
        , hintRecordTypes = []
        , hintProjections = []
        , hintAxioms = []
        , hintLevel = []
        , hintThisFn = Nothing
        , hintRecVars = recVars
        , hintLetVars = letVars
        , hintSplitVars = splitVars
        }

  -- Extract additional components from the names given as hints.
  hintNames <- getEverythingInScope <$> lookupLocalMeta metaId
  isToLevel <- endsInLevelTester
  scope <- getScope
  components' <- foldM (go isToLevel scope) components $
    explicitHints ++ (hintNames \\ explicitHints)

  return BaseComponents
    { hintFns = doSort $ hintFns components'
    , hintDataTypes = doSort $ hintDataTypes components'
    , hintRecordTypes = doSort $ hintRecordTypes components'
    , hintProjections = doSort $ hintProjections components'
    , hintAxioms = doSort $ hintAxioms components'
    , hintLevel = doSort $ hintLevel components'
    , hintThisFn = hintThisFn components'
    , hintRecVars = recVars
    , hintLetVars = letVars
    , hintSplitVars = splitVars
    }
  where
    hintMode = optHintMode opts
    explicitHints = optExplicitHints opts
    -- Sort by the arity of the type
    doSort = sortOn (arity . compType)

    isNotMutual qname f = case mDefName of
      Nothing -> True
      Just defName -> defName /= qname && fmap (defName `elem`) (funMutual f) /= Just True

    go isToLevel scope comps qname = do
        def <- getConstInfo qname
        let typ = defType def
        case theDef def of
          Axiom{}
            | isToLevel typ -> addLevel
            | shouldKeep    -> addAxiom
            | otherwise     -> done
          -- We can't use pattern lambdas as components nor with-functions.
          -- If the function is in the same mutual block, do not include it.
          f@Function{ funWith = Nothing, funExtLam = Nothing }
            | Just qname == mDefName   -> addThisFn
            | notMutual, isToLevel typ -> addLevel
            | notMutual, shouldKeep    -> addFn
            where notMutual = isNotMutual qname f
          Function{} -> done
          Datatype{} -> addData
          Record{} -> do
            projections <- mapM (qnameToComponent (costSpeculateProj costs)) =<< getRecordFields qname
            comp <- qnameToComponent (costSet costs) qname
            return comps{ hintRecordTypes = comp : hintRecordTypes comps
                        , hintProjections = projections ++ hintProjections comps }
          -- We look up constructors when we need them
          Constructor{} -> done
          -- TODO: special treatment for primitives?
          Primitive{}
            | isToLevel typ  -> addLevel
            | shouldKeep     -> addFn
            | otherwise      -> done
          PrimitiveSort{}    -> done
          -- TODO: Check if we want to use these
          DataOrRecSig{}     -> done
          GeneralizableVar{} -> done
          AbstractDefn{}     -> done
        where
          done = return comps
          -- TODO: There is probably a better way of finding the module name
          mThisModule = qnameModule <$> mDefName

          shouldKeep = or
            [ qname `elem` explicitHints
            , qname `elem` whereNames
            , case hintMode of
                Unqualified -> Scope.isNameInScopeUnqualified qname scope
                AllModules  -> True
                Module      -> Just (qnameModule qname) == mThisModule
                NoHints     -> False
            ]
          addLevel  = qnameToComponent (costLevel   costs) qname <&> \ comp -> comps{hintLevel     = comp : hintLevel  comps}
          addAxiom  = qnameToComponent (costAxiom   costs) qname <&> \ comp -> comps{hintAxioms    = comp : hintAxioms comps}
          addThisFn = qnameToComponent (costRecCall costs) qname <&> \ comp -> comps{hintThisFn    = Just comp{ compRec = True }}
          addFn     = qnameToComponent (costFn      costs) qname <&> \ comp -> comps{hintFns       = comp : hintFns comps}
          addData   = qnameToComponent (costSet     costs) qname <&> \ comp -> comps{hintDataTypes = comp : hintDataTypes comps}

-- | Is an element of the given type computing a level?
--
-- The returned checker is only sound but not complete because the type is taken as-is
-- rather than being reduced.
endsInLevelTester :: TCM (Type -> Bool)
endsInLevelTester = do
  getBuiltinName builtinLevel >>= \case
    Nothing    -> return $ const False
    Just level -> return \ t ->
      -- NOTE: We do not reduce the type before checking, so some user definitions
      -- will not be included here.
      case telView' t of
        TelV _ (El _ (Def x _)) -> x == level
        _ -> False


qnameToComponent :: (HasConstInfo tcm, ReadTCState tcm, MonadFresh CompId tcm, MonadTCM tcm)
  => Cost -> QName -> tcm Component
qnameToComponent cost qname = do
  defn <- getConstInfo qname
  -- #7120: we need to apply the module params to everything
  mParams <- freeVarsToApply qname
  let def = (Def qname [] `apply` mParams, 0)
  let (term, pars) = case theDef defn of
        c@Constructor{}    -> (Con (conSrcCon c) ConOCon [], conPars c - length mParams)
        Axiom{}            -> def
        GeneralizableVar{} -> def
        Function{}         -> def
        Datatype{}         -> def
        Record{}           -> def
        Primitive{}        -> def
        PrimitiveSort{}    -> def
        DataOrRecSig{}     -> __IMPOSSIBLE__
        AbstractDefn{}     -> __IMPOSSIBLE__
  newComponentQ [] cost qname pars term (defType defn `piApply` mParams)

-- | From the scope of the given meta variable,
--   extract all names in scope that we could use during synthesis.
--   (This excludes macros, generalizable variables, pattern synonyms.)
getEverythingInScope :: MetaVariable -> [QName]
getEverythingInScope metaVar = do
  let scope = clScope $ getMetaInfo metaVar
  let nameSpace = Scope.everythingInScope scope
      names = Scope.nsNames nameSpace
      validKind = \ case
        Scope.PatternSynName           -> False   -- could consider allowing pattern synonyms, but the problem is they can't be getConstInfo'd
        Scope.GeneralizeName           -> False   -- and any way finding the underlying constructors should be easy
        Scope.DisallowedGeneralizeName -> False
        Scope.MacroName                -> False
        Scope.QuotableName             -> False
        Scope.ConName                  -> True
        Scope.CoConName                -> True
        Scope.FldName                  -> True
        Scope.DataName                 -> True
        Scope.RecName                  -> True
        Scope.FunName                  -> True
        Scope.AxiomName                -> True
        Scope.PrimName                 -> True
        Scope.OtherDefName             -> True
      qnames = map Scope.anameName
             . filter (validKind . Scope.anameKind)
             . map NonEmptyList.head
             $ Map.elems names
  qnames

-- | Turn the let bindings of the current 'TCEnv' into components.
getLetVars :: forall tcm. (MonadFresh CompId tcm, MonadTCM tcm, Monad tcm) => Cost -> tcm [Open Component]
getLetVars cost = do
  bindings <- asksTC envLetBindings
  mapM makeComp $ Map.toAscList bindings
  where
    makeComp :: (Name, Open LetBinding) -> tcm (Open Component)
    makeComp (name, opn) = do
      cId <- fresh
      return $ opn <&> \ (LetBinding _origin term typ) ->
                mkComponent cId [] cost (Just name) 0 term (unDom typ)

-- IDEA for implementing case-splitting:
-- [x] 1. Modify the collectRecVarCandidates to get all variables.
-- [ ] 2. Go through all variables to see if they are data types (not records)
-- [ ] 3. Run makeCase for those variables.
-- [ ] 4. Find out how to get the new interaction points/metas from the cases
-- [ ] 5. After search is done, compute out-of-scope variables.
-- [ ] 6. Run make-case again to introduce those variables.
-- [ ] 7. Redo the reification in the new clauses.
-- [ ] 8. Return the new clauses and follow Auto for insertion.

getSplitVars :: Open [(Term, Maybe Int)] -> TCM (Open [Term])
getSplitVars lhsVars' = do

    -- Compute the hintSplitVars from the pattern variables of function at the interaction point.
    lhsVars <- getOpen $ map fst <$> lhsVars'
    typedLocals <- getLocalVarTerms 0
    reportSDoc "mimer.components" 40 $ "All LHS variables:" <+> prettyTCM lhsVars <+> parens ("or" <+> pretty lhsVars)
    let typedLhsVars = filter (\(term,typ) -> term `elem` lhsVars) typedLocals
    reportSDoc "mimer.components" 40 $
      "LHS variables with types:" <+> prettyList (map prettyTCMTypedTerm typedLhsVars) <+> parens ("or"
        <+> prettyList (map prettyTypedTerm typedLhsVars))
    -- TODO: For now, we *never* split on implicit arguments even if they are
    -- written explicitly on the LHS.
    splitVarsTyped <-
      filterM (\ (term, dom) -> pure (visible dom) `and2M` isTypeDatatype (unDom dom))
              typedLhsVars
    reportSDoc "mimer.components" 40 $
      "Splittable variables" <+> prettyList (map prettyTCMTypedTerm splitVarsTyped) <+> parens ("or"
        <+> prettyList (map prettyTypedTerm splitVarsTyped))
    makeOpen $ map fst splitVarsTyped
  where
    prettyTCMTypedTerm :: (PrettyTCM tm, PrettyTCM ty) => (tm, ty) -> TCM Doc
    prettyTCMTypedTerm (term, typ) = prettyTCM term <+> ":" <+> prettyTCM typ
    prettyTypedTerm (term, typ) = pretty term <+> ":" <+> pretty typ

-- | Returns the variables as terms together with whether they where found under
-- some constructor, and if so which argument of the function they appeared in. This
-- information is used when building recursive calls, where it's important that we don't try to
-- construct non-terminating solutions.
collectLHSVars :: (ReadTCState tcm, MonadError TCErr tcm, MonadTCM tcm, HasConstInfo tcm)
  => InteractionId -> tcm (Open [(Term, Maybe Int)])
collectLHSVars ii = do
  ipc <- ipClause <$> lookupInteractionPoint ii
  case ipc of
    IPNoClause -> makeOpen []
    IPClause{ipcQName = fnName, ipcClauseNo = clauseNr} -> do
      reportSDoc "mimer.components" 40 $ "Collecting LHS vars for" <+> prettyTCM ii
      info <- getConstInfo fnName
      parCount <- liftTCM getCurrentModuleFreeVars
      case theDef info of
        fnDef@Function{} -> do
          let clause = funClauses fnDef !! clauseNr
              naps = namedClausePats clause

          -- Telescope at interaction point
          iTel <- getContextTelescope
          -- Telescope for the body of the clause
          let cTel = clauseTel clause
          -- HACK: To get the correct indices, we shift by the difference in telescope lengths
          let shift = length (telToArgs iTel) - length (telToArgs cTel)

          reportSDoc "mimer" 60 $ vcat
            [ "Tel:"
            , nest 2 $ pretty iTel $$ prettyTCM iTel
            , "CTel:"
            , nest 2 $ pretty cTel $$ prettyTCM cTel
            ]
          reportSDoc "mimer" 60 $ "Shift:" <+> pretty shift

          makeOpen [ (Var (n + shift) [], (i - parCount) <$ guard underCon)    -- We count arguments excluding module parameters
                   | (i, nap) <- zip [0..] naps
                   , (n, underCon) <- go False $ namedThing $ unArg nap
                   ]
        _ -> do
          makeOpen []
  where
    go isUnderCon = \case
      VarP patInf x -> [(dbPatVarIndex x, isUnderCon)]
      DotP patInf t -> [] -- Ignore dot patterns
      ConP conHead conPatInf namedArgs -> concatMap (go True . namedThing . unArg) namedArgs
      LitP{} -> []
      ProjP{} -> []
      IApplyP{} -> [] -- Only for Cubical?
      DefP{} -> [] -- Only for Cubical?

declarationQnames :: A.Declaration -> [QName]
declarationQnames dec = [ q | Scope.WithKind _ q <- A.declaredNames dec ]

------------------------------------------------------------------------------
-- * Measure performance
------------------------------------------------------------------------------
data MimerStats = MimerStats
  { statCompHit :: Nat -- ^ Could make use of an already generated component
  , statCompGen :: Nat -- ^ Could use a generator for a component
  , statCompRegen :: Nat -- ^ Had to regenerate the cache (new context)
  , statCompNoRegen :: Nat -- ^ Did not have to regenerate the cache
  , statMetasCreated :: Nat -- ^ Total number of meta-variables created explicitly (not through unification)
  , statTypeEqChecks :: Nat -- ^ Number of times type equality is tested (with unification)
  , statRefineSuccess :: Nat -- ^ Number of times a refinement has been successful
  , statRefineFail :: Nat -- ^ Number of times a refinement has failed
  } deriving (Show, Eq, Generic)
instance NFData MimerStats

emptyMimerStats :: MimerStats
emptyMimerStats = MimerStats
  { statCompHit = 0, statCompGen = 0, statCompRegen = 0 , statCompNoRegen = 0 , statMetasCreated = 0, statTypeEqChecks = 0, statRefineSuccess = 0 , statRefineFail = 0}

incCompHit, incCompGen, incCompRegen, incCompNoRegen, incMetasCreated, incTypeEqChecks, incRefineSuccess, incRefineFail :: MimerStats -> MimerStats
incCompHit       stats = stats {statCompHit       = succ $ statCompHit stats}
incCompGen       stats = stats {statCompGen       = succ $ statCompGen stats}
incCompRegen     stats = stats {statCompRegen     = succ $ statCompRegen stats}
incCompNoRegen   stats = stats {statCompNoRegen   = succ $ statCompNoRegen stats}
incMetasCreated  stats = stats {statMetasCreated  = succ $ statMetasCreated stats}
incTypeEqChecks  stats = stats {statTypeEqChecks  = succ $ statTypeEqChecks stats}
incRefineSuccess stats = stats {statRefineSuccess = succ $ statRefineSuccess stats}
incRefineFail    stats = stats {statRefineFail    = succ $ statRefineFail stats}

updateStat :: (MimerStats -> MimerStats) -> SM ()
updateStat f = verboseS "mimer.stats" 10 $ do
  ref <- asks searchStats
  liftIO $ modifyIORef' ref f


------------------------------------------------------------------------------
-- * Core algorithm
------------------------------------------------------------------------------

runSearch :: Rewrite -> Options -> InteractionId -> Range -> TCM [MimerResult]
runSearch norm options ii rng = withInteractionId ii $ do
  (mTheFunctionQName, whereNames) <- fmap ipClause (lookupInteractionPoint ii) <&> \case
    clause@IPClause{} -> ( Just $ ipcQName clause
                         , case A.whereDecls $ A.clauseWhereDecls $ ipcClause clause of
                             Just decl -> declarationQnames decl
                             _ -> []
                         )
    IPNoClause -> (Nothing, [])

  reportSDoc "mimer.init" 15 $ "Interaction point in function:" <+> pretty mTheFunctionQName
  reportSDoc "mimer.init" 25 $ "Names in where-block" <+> pretty whereNames

  metaId <- lookupInteractionId ii
  metaVar <- lookupLocalMeta metaId

  -- We want to be able to solve with recursive calls
  setMetaOccursCheck metaId DontRunMetaOccursCheck

  metaIds <- case mvInstantiation metaVar of
    InstV inst -> do

      metaIds <- allOpenMetas (instBody inst)

      -- TODO: Make pretty instantiation for 'Instantiation'?
      reportSDoc "mimer.init" 20 $ sep [ "Interaction point already instantiated:" <+> pretty (instBody inst)
                                       , "with args" <+> pretty (instTel inst) ]

      -- ctx <- getContextTelescope
      -- #7402: still solve the top-level meta, because we don't have the correct contexts for the
      --        submetas
      return [metaId | not $ null metaIds]
    OpenMeta UnificationMeta -> do
      reportSLn "mimer.init" 20 "Interaction point not instantiated."
      return [metaId]
    _ -> __IMPOSSIBLE__
  -- TODO: Print each meta-variable's full context telescope
  reportSDoc "mimer.init" 20 $ "Remaining meta-variables to solve:" <+> prettyTCM metaIds
  reportSDoc "mimer.init" 20 $ "Meta var args" <+> (prettyTCM =<< getMetaContextArgs metaVar)


  fnArgs1 <- withShowAllArguments' False $ getContextArgs >>= mapM prettyTCM
  fnArgs2 <- withShowAllArguments' True  $ getContextArgs >>= mapM prettyTCM
  let bringScope = map snd $ filter (uncurry (/=)) $ zip fnArgs1 fnArgs2
      bringScopeNoBraces = map (filter (`notElem` ['{', '}']) . P.render) bringScope
  reportSDoc "mimer.temp" 20 $ vcat
    [ "Things to bring into scope:"
    , nest 2 $ vcat
      [ "Context args (don't show):" <+> pretty fnArgs1
      , "Context args (show all):  " <+> pretty fnArgs2
      , "To bring into scope:      " <+> pretty bringScope
      , "To bring into scope (str):" <+> pretty bringScopeNoBraces
      ]
    ]

  -- Check if there are any meta-variables to be solved
  case metaIds of
    -- No variables to solve, return the instantiation given
    [] -> do
      case mvInstantiation metaVar of
        InstV inst -> do
          expr <- withInteractionId ii $ do
            metaArgs <- getMetaContextArgs metaVar
            instantiateFull (apply (MetaV metaId []) metaArgs) >>= normalForm norm >>= reify
          str <- P.render <$> prettyTCM expr
          let sol = MimerExpr str
          reportSDoc "mimer.init" 10 $ "Goal already solved. Solution:" <+> text str
          return [sol]
        _ -> __IMPOSSIBLE__
    _ -> do
      costs <- ifM (hasVerbosity "mimer.cost.custom" 10)
                 {- then -} customCosts
                 {- else -} (return defaultCosts)
      reportSDoc "mimer.cost.custom" 10 $ "Using costs:" $$ nest 2 (pretty costs)
      components <- collectComponents options costs ii mTheFunctionQName whereNames metaId
      let startGoals = map Goal metaIds

      state <- getTC
      env <- askTC

      let startBranch = SearchBranch
            { sbTCState = state
            , sbGoals = startGoals
            , sbCost = 0
            , sbCache = Map.empty
            , sbComponentsUsed = Map.empty
            }

      statsRef <- liftIO $ newIORef emptyMimerStats
      checkpoint <- viewTC eCurrentCheckpoint
      mflat <- getBuiltinName BuiltinFlat
      let searchOptions = SearchOptions
            { searchBaseComponents = components
            , searchHintMode = optHintMode options
            , searchTimeout = optTimeout options
            , searchGenProjectionsLocal = True
            , searchGenProjectionsLet = True
            , searchGenProjectionsExternal = False
            , searchGenProjectionsRec = True
            , searchSpeculateProjections = True
            , searchTopMeta = metaId
            , searchTopEnv = env
            , searchTopCheckpoint = checkpoint
            , searchInteractionId = ii
            , searchFnName = mTheFunctionQName
            , searchCosts = costs
            , searchStats = statsRef
            , searchRewrite = norm
            , searchBuiltinFlat = mflat
            }

      reportSDoc "mimer.init" 20 $ "Using search options:" $$ nest 2 (prettyTCM searchOptions)
      reportSDoc "mimer.init" 20 $ "Initial search branch:" $$ nest 2 (pretty startBranch)

      flip runReaderT searchOptions $ bench [] $ do

        -- TODO: Check what timing stuff is used in Agda.Utils.Time
        timeout <- fromMilliseconds <$> asks searchTimeout
        startTime <- liftIO getCPUTime
        let go :: Int -> Int -> MinQueue SearchBranch -> SM ([MimerResult], Int)
            go 0 n _ = pure ([], n)
            go need n branchQueue = case Q.minView branchQueue of
              Nothing -> do
                reportSLn "mimer.search" 30 $ "No remaining search branches."
                return ([], n)
              Just (branch, branchQueue') -> do
                time <- liftIO getCPUTime
                mimerTrace 0 10 $ vcat
                  [ "Choosing branch"
                  , nest 2 $ sep
                    [ branchInstantiationDocCost branch <> ","
                    , nest 2 $ "metas:" <+> prettyTCM (map goalMeta $ sbGoals branch)
                    ]
                  ]
                reportSDoc "mimer.search" 50 $ "Full branch:" <+> pretty branch
                reportSMDoc "mimer.search" 50 $
                  "Instantiation of other branches:" <+> prettyList (map branchInstantiationDocCost $ Q.toAscList branchQueue')

                let elapsed = time - startTime
                if elapsed < timeout
                then do
                  (newBranches, sols) <- refine branch >>= partitionStepResult
                  let branchQueue'' = foldr Q.insert branchQueue' newBranches
                  reportSLn "mimer.search" 40 $ show (length sols) ++ " solutions found during cycle " ++ show (n + 1)
                  reportSMDoc "mimer.search" 45 $ "Solutions:" <+> prettyTCM sols
                  mimerTrace 0 40 $ vcat
                     [ "Cycle" <+> pretty (n + 1) <+> "branches"
                     , nest 2 $ vcat $ map branchInstantiationDocCost $ Q.toAscList branchQueue''
                     ]
                  unless (null sols) $ mimerTrace 0 20 $ vcat
                     [ "Cycle" <+> pretty (n + 1) <+> "solutions"
                     , nest 2 $ vcat $ map prettyTCM sols
                     ]

                  let sols' = take need sols
                  mapFst (sols' ++) <$> go (need - length sols') (n + 1) branchQueue''
                else do
                  reportSLn "mimer.search" 30 $ "Search time limit reached. Elapsed search time: " ++ show elapsed
                  return ([], n)
        let numSolutions | optList options = 10 + optSkip options
                         | otherwise       = 1 + optSkip options
        (sols, nrSteps) <- go numSolutions 0 $ Q.singleton startBranch
        reportSLn "mimer.search" 20 $ "Search ended after " ++ show (nrSteps + 1) ++ " cycles"
        -- results <- liftTCM $ mapM exprToStringAndVars sols
        reportSDoc "mimer.search" 15 $ "Solutions found: " <+> prettyList (map prettyTCM sols)
        reportSMDoc "mimer.stats" 10 $ do
          ref <- asks searchStats
          stats <- liftIO $ readIORef ref
          "Statistics:" <+> text (show stats)
        return sols

tryComponents :: Goal -> Type -> SearchBranch -> [(Component, [Component])] -> SM [SearchStepResult]
tryComponents goal goalType branch comps = withBranchAndGoal branch goal $ do
  checkpoint <- viewTC eCurrentCheckpoint
  let tryFor (sourceComp, comps') = do
        -- Clear out components that depend on meta-variables that have been used.
        let newCache = Map.insert sourceComp Nothing (sbCache branch Map.! checkpoint)
        newBranches <- catMaybes <$> mapM (tryRefineWith goal goalType branch) comps'
        return $ map (\br -> br{sbCache = Map.insert checkpoint newCache (sbCache branch)}) newBranches
  newBranches <- concatMapM tryFor comps
  mapM checkSolved newBranches

-- | If there is no cache entry for the checkpoint, create one. If there already
-- is one, even if the components are not yet generated for some entries, it is
-- returned as is.
prepareComponents :: Goal -> SearchBranch -> SM (SearchBranch, [(Component, [Component])])
prepareComponents goal branch = withBranchAndGoal branch goal $ do
  reportSDoc "mimer.components" 50 $ "Preparing components for goal" <+> prettyTCM (goalMeta goal)
  checkpoint <- viewTC eCurrentCheckpoint
  -- Check if we there is something in the cache for this checkpoint
  comps <- case Map.lookup checkpoint (sbCache branch) of
    -- No, generate components from scratch
    Nothing -> do
      updateStat incCompRegen
      reportSDoc "mimer.components" 20 $ vcat
        [ "No cache found checkpoint:" <+> pretty checkpoint
        , nest 2 $ "with context:" <+> (inTopContext . prettyTCM =<< getContextTelescope) ]
      -- Generate components for this context
      comps <- genComponents
      reportSDoc "mimer.components" 20 $ "Generated" <+> pretty (sum $ map (length . snd) comps) <+> "components"
      return comps
    -- Yes, just update the missing generated components
    Just cache -> mapM prepare (Map.toAscList cache)
  let newCache = Map.fromList $ map (mapSnd Just) comps
  branch' <- updateBranch [] branch{sbCache = Map.insert checkpoint newCache (sbCache branch)}
  return (branch', comps)
  where
  prepare :: (Component, Maybe [Component]) -> SM (Component, [Component])
  prepare (sourceComp, Just comps) = do
    updateStat incCompNoRegen
    return (sourceComp, comps)
  prepare (sourceComp, Nothing) = do
    updateStat incCompRegen
    (sourceComp,) <$> genComponentsFrom True sourceComp

localVarCount :: SM Int
localVarCount = do
  top <- asks $ length . envContext . searchTopEnv
  cur <- length <$> getContext
  pure $ cur - top

genComponents :: SM [(Component, [Component])]
genComponents = do
  opts <- ask
  let comps = searchBaseComponents opts
  n <- localVarCount
  localVars <- lift (getLocalVars n (costLocal $ searchCosts opts))
    >>= genAddSource (searchGenProjectionsLocal opts)
  recCalls <- genAddSource (searchGenProjectionsRec opts) (maybeToList $ hintThisFn comps)
  letVars <- mapM getOpenComponent (hintLetVars comps)
    >>= genAddSource (searchGenProjectionsLet opts)
  fns <- genAddSource (searchGenProjectionsExternal opts) (hintFns comps)
  axioms <- genAddSource (searchGenProjectionsExternal opts) (hintAxioms comps)
  return $ localVars ++ letVars ++ recCalls ++ fns ++ axioms
  where
    genAddSource :: Bool -> [Component] -> SM [(Component, [Component])]
    genAddSource genProj = mapM (\comp -> (comp,) <$> genComponentsFrom genProj comp)


genComponentsFrom :: Bool -- ^ Apply record elimination
                  -> Component
                  -> SM [Component]
genComponentsFrom appRecElims origComp = do
  reportSDoc "mimer.components" 50 $ "Generating components from original component" <+> prettyTCM (compId origComp) <+> prettyTCM (compName origComp)
  comps <- if | compRec origComp -> mapM (applyToMetasG Nothing) =<< genRecCalls origComp
              | otherwise        -> (:[]) <$> applyToMetasG Nothing origComp
  if appRecElims
  then concat <$> mapM (applyProjections Set.empty) comps
  else return comps
  where
  applyProjections :: Set QName -> Component -> SM [Component]
  applyProjections seenRecords comp = do
    projComps <- getRecordInfo (compType comp) >>= \case
      Nothing -> return []
      Just (recordName, args, fields, isRecursive)
          | Set.member recordName seenRecords -> do
              reportSDoc "mimer.components" 60 $
                "Skipping projection because recursive record already seen:" <+> pretty recordName
              return []
          | otherwise -> do
              let seenRecords' = if isRecursive then Set.insert recordName seenRecords else seenRecords
              comps <- mapM (applyProj args comp >=> applyToMetasG Nothing) fields
              concatMapM (applyProjections seenRecords') comps
    return $ comp : projComps

getRecordInfo :: Type
  -> SM (Maybe ( QName     -- Record name
               , Args      -- Record parameters converted to (hidden) arguments
               , [QName]   -- Field names
               , Bool      -- Is recursive?
               ))
getRecordInfo typ = case unEl typ of
  Def qname elims -> isRecord qname >>= \case
    Nothing -> return Nothing
    Just defn -> do
      fields <- getRecordFields qname
      return $ Just (qname, argsFromElims elims, fields, recRecursive_ defn)
  _ -> return Nothing

applyProj :: Args -> Component -> QName -> SM Component
applyProj recordArgs comp' qname = do
  cost <- asks (costProj . searchCosts)
  -- Andreas, 2025-03-31, issue #7662: hack to prevent postfix printing of ♭
  projOrigin <- maybe ProjSystem (\ flat -> if qname == flat then ProjPrefix else ProjSystem)
    <$> asks searchBuiltinFlat
  let newTerm = applyE (compTerm comp') [Proj projOrigin qname]
  projType <- defType <$> getConstInfo qname
  projTypeWithArgs <- piApplyM projType recordArgs
  newType <- piApplyM projTypeWithArgs (compTerm comp')
  newComponentQ (compMetas comp') (compCost comp' + cost) qname 0 newTerm newType


-- TODO: currently reducing twice
applyToMetasG
  :: Maybe Nat -- ^ Max number of arguments to apply.
  -> Component -> SM Component
applyToMetasG (Just m) comp | m <= 0 = return comp
applyToMetasG maxArgs comp = do
  reportSDoc "mimer.component" 25 $ "Applying component to metas" <+> prettyTCM (compId comp) <+> prettyTCM (compTerm comp)
  ctx <- getContextTelescope
  compTyp <- reduce $ compType comp
  case unEl compTyp of
    Pi dom abs -> do
      let domainType = unDom dom
      (metaId, metaTerm) <- createMeta domainType
      reportSDoc "mimer.component" 30 $ "New arg meta" <+> prettyTCM metaTerm
      let arg = setOrigin Inserted $ metaTerm <$ argFromDom dom
      newType <- reduce =<< piApplyM (compType comp) metaTerm
      -- Constructor parameters are not included in the term
      let skip = compPars comp
          newTerm | skip > 0  = compTerm comp
                  | otherwise = apply (compTerm comp) [arg]
      cost <- asks $ (if getHiding arg == Hidden then costNewHiddenMeta else costNewMeta) . searchCosts
      applyToMetasG (predNat <$> maxArgs)
                    comp{ compTerm = newTerm
                        , compType = newType
                        , compPars = predNat skip
                        , compMetas = metaId : compMetas comp
                        , compCost = cost + compCost comp
                        }
    _ ->
      -- Set the type to the reduced version
      return comp{compType = compTyp}

createMeta :: Type -> SM (MetaId, Term)
createMeta typ = do
  (metaId, metaTerm) <- newValueMeta DontRunMetaOccursCheck CmpLeq typ
  verboseS "mimer.stats" 20 $ updateStat incMetasCreated
  reportSDoc "mimer.components" 80 $ do
    "Created meta-variable (type in context):" <+> pretty metaTerm <+> ":" <+> (pretty =<< getMetaTypeInContext metaId)
  return (metaId, metaTerm)


partitionStepResult :: [SearchStepResult] -> SM ([SearchBranch], [MimerResult])
partitionStepResult [] = return ([],[])
partitionStepResult (x:xs) = do
  let rest = partitionStepResult xs
  (brs',sols) <- rest
  case x of
    NoSolution -> rest
    OpenBranch br -> return (br:brs', sols)
    ResultExpr exp -> do
      str <- P.render <$> prettyTCM exp
      return $ (brs', MimerExpr str : sols)
    ResultClauses cls -> do
      f <- fromMaybe __IMPOSSIBLE__ <$> asks searchFnName
      return $ (brs', MimerClauses f cls : sols)


topInstantiationDoc :: SM Doc
topInstantiationDoc = asks searchTopMeta >>= getMetaInstantiation >>= maybe (return "(nothing)") prettyTCM

prettyGoalInst :: Goal -> SM Doc
prettyGoalInst goal = inGoalEnv goal $ do
  args <- map Apply <$> getContextArgs
  prettyTCM =<< instantiate (MetaV (goalMeta goal) args)

branchInstantiationDocCost :: SearchBranch -> SM Doc
branchInstantiationDocCost branch = branchInstantiationDoc branch <+> parens ("cost:" <+> pretty (sbCost branch))

-- | For debug
branchInstantiationDoc :: SearchBranch -> SM Doc
branchInstantiationDoc branch = withBranchState branch topInstantiationDoc

refine :: SearchBranch -> SM [SearchStepResult]
refine branch = withBranchState branch $ do
  let (goal1, branch1) = nextGoal branch

  withBranchAndGoal branch1 goal1 $ do
    goalType1 <- bench [Bench.Reduce] $ reduce =<< getMetaTypeInContext (goalMeta goal1)

    mimerTrace 1 10 $ sep
      [ "Refining goal"
      , nest 2 $ prettyTCM (goalMeta goal1) <+> ":" <+> prettyTCM goalType1
      , nest 2 $ "in context" <+> (inTopContext . prettyTCM =<< getContextTelescope)
      ]

    reportSDoc "mimer.refine" 30 $ "Goal type:" <+> pretty goalType1
    reportSDoc "mimer.refine" 30 $ "Goal context:" <+> (pretty =<< getContextTelescope)

    -- Lambda-abstract as far as possible
    tryLamAbs goal1 goalType1 branch1 >>= \case
      -- Absurd lambda
      Left branch2 -> do
        mimerTrace 1 10 $ sep
              [ "Absurd bambda refinement", nest 2 $ prettyGoalInst goal1 ]
        args <- map Apply <$> getContextArgs
        e <- blankNotInScope =<< reify (MetaV (goalMeta goal1) args)
        return [ResultExpr e]
      -- Normal abstraction
      Right (goal2, goalType2, branch2) -> withBranchAndGoal branch2 goal2 $ do
        (branch3, components) <- prepareComponents goal2 branch2
        withBranchAndGoal branch3 goal2 $ do

          when (goalMeta goal2 /= goalMeta goal1) $ do
            mimerTrace 1 10 $ sep
              [ "Lambda refinement", nest 2 $ prettyGoalInst goal1 ]
            mimerTrace 1 10 $ sep
              [ "Refining goal"
              , nest 2 $ prettyTCM (goalMeta goal2) <+> ":" <+> prettyTCM goalType2
              , nest 2 $ "in context" <+> (inTopContext . prettyTCM =<< getContextTelescope)
              ]

          mimerTrace 2 40 $ vcat
            [ "Components:"
            , nest 2 $ vcat $ map prettyTCM $ concatMap snd components
            ]

          results1 <- tryComponents goal2 goalType2 branch3 components
          results2 <- tryDataRecord goal2 goalType2 branch3
          return $ results1 ++ results2

tryFns :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryFns goal goalType branch = withBranchAndGoal branch goal $ do
  reportSDoc "mimer.refine.fn" 50 $ "Trying functions"
  fns <- asks (hintFns . searchBaseComponents)
  newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) fns
  mapM checkSolved newBranches

tryProjs :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryProjs goal goalType branch = withBranchAndGoal branch goal $ do
  projs <- asks (hintProjections . searchBaseComponents)
  newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) projs
  mapM checkSolved newBranches

tryAxioms :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryAxioms goal goalType branch = withBranchAndGoal branch goal $ do
  axioms <- asks (hintAxioms . searchBaseComponents)
  newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) axioms
  mapM checkSolved newBranches

tryLet :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryLet goal goalType branch = withBranchAndGoal branch goal $ do
  letVars <- asks (hintLetVars . searchBaseComponents) >>= mapM getOpenComponent
  newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) letVars
  mapM checkSolved newBranches

-- | Returns @Right@ for normal lambda abstraction and @Left@ for absurd lambda.
tryLamAbs :: Goal -> Type -> SearchBranch -> SM (Either SearchBranch (Goal, Type, SearchBranch))
tryLamAbs goal goalType branch =
  case unEl goalType of
    Pi dom abs -> isEmptyType (unDom dom) >>= \case
      True -> do
        f <- liftTCM $ makeAbsurdLambda noRange dom abs
        args <- map Apply <$> getContextArgs
        newMetaIds <- assignMeta (goalMeta goal) (Def f args) goalType
        Left <$> updateBranch newMetaIds branch
      False -> do
        reportSDoc "mimer.lam" 40 $ "Trying lambda abstraction for pi type" <+> prettyTCM goalType
        let abs' | isNoName (absName abs) = abs { absName = "z" }
                 | otherwise = abs
        (metaId', bodyType, metaTerm, env) <- underAbstractionAbs dom abs' $ \bodyType -> do
          reportSDoc "mimer.lam" 40 $ "  bodyType = " <+> prettyTCM bodyType
          bodyType <- bench [Bench.Reduce] $ reduce bodyType -- TODO: Good place to reduce?
          reportSDoc "mimer.lam" 40 $ "  bodyType (reduced) = " <+> prettyTCM bodyType
          (metaId', metaTerm) <- bench [Bench.Free] $ newValueMeta DontRunMetaOccursCheck CmpLeq bodyType
          reportSDoc "mimer.lam" 40 $ "  metaId' = " <+> prettyTCM metaId'
          env <- askTC
          return (metaId', bodyType, metaTerm, env)

        let argInf = domInfo dom -- TODO: is this the correct arg info?
            newAbs = Abs (absName abs') metaTerm
            -- look at mkLam
            term = Lam argInf newAbs

        newMetaIds <- assignMeta (goalMeta goal) term goalType

        withEnv env $ do
          branch' <- updateBranch newMetaIds branch
          tryLamAbs (Goal metaId') bodyType branch'
    _ -> done
  where
    done = do
      branch' <- updateBranch [] branch -- TODO: Is this necessary?
      return $ Right (goal, goalType, branch')


genRecCalls :: Component -> SM [Component]
genRecCalls thisFn = do
  reportSDoc "mimer.components.open" 40 $ "Generating recursive calls for component" <+> prettyTCM (compId thisFn) <+> prettyTCM (compName thisFn)
  reportSDoc "mimer.components.open" 60 $ "  checkpoint =" <+> (prettyTCM =<< viewTC eCurrentCheckpoint)
  -- TODO: Make sure there are no pruning problems
  asks (hintRecVars . searchBaseComponents) >>= getOpen >>= \case
    -- No candidate arguments for a recursive call
    [] -> return []
    recCandTerms -> do
      Costs{..} <- asks searchCosts
      n <- localVarCount
      localVars <- lift $ getLocalVars n costLocal
      let recCands = [ (t, i) | t@(compTerm -> v@Var{}) <- localVars, NoSubst i <- maybeToList $ lookup v recCandTerms ]

      let newRecCall = do
            -- Apply the recursive call to new metas
            (thisFnTerm, thisFnType, newMetas) <- applyToMetas 0 (compTerm thisFn) (compType thisFn)
            let argGoals = map Goal newMetas
            comp <- newComponent newMetas (compCost thisFn) (compName thisFn) 0 thisFnTerm thisFnType
            return (comp, zip argGoals [0..])

          -- go :: Component -- ^ Recursive call function applied to meta-variables
          --   -> [(Goal, Int)] -- ^ Remaining parameters to try to fill
          --   -> [(Component, Int)] -- ^ Remaining argument candidates for the current parameter
          --   -> SM [Component]
          go _thisFn [] _args = return []
          go thisFn (_ : goals) [] = go thisFn goals recCands
          go thisFn ((goal, i) : goals) ((arg, j) : args) | i == j = do
            reportSMDoc "mimer.components.rec" 80 $ hsep
              [ "Trying to generate recursive call"
              , prettyTCM (compTerm thisFn)
              , "with" <+> prettyTCM (compTerm arg)
              , "for" <+> prettyTCM (goalMeta goal) ]
            goalType <- getMetaTypeInContext (goalMeta goal)
            state <- getTC
            tryRefineWith' goal goalType arg >>= \case
              Nothing -> do
                putTC state
                go thisFn ((goal, i) : goals) args
              Just (newMetas1, newMetas2) -> do
                let newComp = thisFn{compMetas = newMetas1 ++ newMetas2 ++ (compMetas thisFn \\ [goalMeta goal])}
                (thisFn', goals') <- newRecCall
                (newComp:) <$> go thisFn' (drop (length goals' - length goals - 1) goals') args
          go thisFn goals (_ : args) = go thisFn goals args
      (thisFn', argGoals) <- newRecCall
      comps <- go thisFn' argGoals recCands
      -- Compute costs for the calls:
      --  - costNewMeta/costNewHiddenMeta for each unsolved argument
      --  - zero for solved arguments
      --  - costLocal for the parameter we recurse on
      let callCost comp = (costLocal +) . sum <$> argCosts (compTerm comp)
          argCosts (Def _ elims) = mapM argCost elims
          argCosts _ = __IMPOSSIBLE__
          argCost (Apply arg) = instantiate arg <&> \ case
            Arg h MetaV{} | visible h -> costNewMeta
                          | otherwise -> costNewHiddenMeta
            _ -> 0
          argCost Proj{}   = pure 0
          argCost IApply{} = pure 0
      mapM (\ c -> (`addCost` c) <$> callCost c) comps


-- TODO: Factor out `checkSolved`
tryDataRecord :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryDataRecord goal goalType branch = withBranchAndGoal branch goal $ do
  -- TODO: There is a `isRecord` function, which performs a similar case
  -- analysis as here, but it does not work for data types.
  case unEl goalType of
    Def qname elims -> theDef <$> getConstInfo qname >>= \case
      recordDefn@Record{} -> do
        tryRecord recordDefn
      dataDefn@Datatype{} -> do
        tryData dataDefn
      primitive@Primitive{} -> do
        return []
      -- TODO: Better way of checking that type is Level
      Axiom{}
        | P.prettyShow qname == "Agda.Primitive.Level" -> do
            tryLevel
        | otherwise -> do
        return []
      DataOrRecSig{} -> do
        return []
      GeneralizableVar{} -> do
        return []
      AbstractDefn{} -> do
        return []
      Function{} -> do
        return []
      Constructor{} -> do
        return []
      PrimitiveSort{} -> do
        return []
    Sort (Type level) -> do
      trySet level
    Sort sort -> do
      return []
    _ -> return []
  where
      -- TODO: Alternatively, the constructor can be accessed via `getRecordConstructor`
      -- TODO: There might be a neater way of applying the constructor to new metas
    tryRecord :: Defn -> SM [SearchStepResult]
    tryRecord recordDefn = do
      cost <- asks (costRecordCon . searchCosts) -- TODO: Use lenses for this?
      comp <- qnameToComponent cost $ conName $ recConHead recordDefn
      -- NOTE: at most 1
      newBranches <- maybeToList <$> tryRefineAddMetas goal goalType branch comp
      mapM checkSolved newBranches

    tryData :: Defn -> SM [SearchStepResult]
    tryData dataDefn = do
      let constructors = dataCons dataDefn
      reportSDoc "mimer.try" 40 $ hsep $ "tryData" : map prettyTCM constructors
      cost <- asks (costDataCon . searchCosts)
      comps <- mapM (qnameToComponent cost) constructors
      newBranches <- mapM (tryRefineAddMetas goal goalType branch) comps
      -- TODO: Reduce overlap between e.g. tryLocals, this and tryRecord
      mapM checkSolved (catMaybes newBranches)

    tryLevel :: SM [SearchStepResult]
    tryLevel = do
      levelHints <- asks (hintLevel . searchBaseComponents)
      newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) levelHints
      mapM checkSolved newBranches

    -- TODO: Add an extra filtering on the sort
    trySet :: Level -> SM [SearchStepResult]
    trySet level = do
      reducedLevel <- reduce level
      cost <- asks (costSet . searchCosts)
      setCandidates <- case reducedLevel of
        (Max i [])
          | i > 0 -> do
              comp <- newComponent [] cost Nothing 0 (Sort $ Type $ Max (i - 1) []) goalType
              return [(branch, comp)]
          | otherwise -> return []
        (Max i ps) -> do
              (metaId, metaTerm) <- createMeta =<< levelType
              comp <- newComponent [metaId] cost Nothing 0 (Sort $ Type $ Max (max 0 (i - 1)) [Plus 0 metaTerm]) goalType
              branch' <- updateBranch [metaId] branch
              return [(branch', comp)]
      reportSDoc "mimer.refine.set" 40 $
        "Trying" <+> prettyTCM (map snd setCandidates) <+> "for" <+> prettyTCM goalType
      newBranches <- catMaybes <$> mapM (\(br,c) -> tryRefineWith goal goalType br c) setCandidates
      components <- asks searchBaseComponents
      newBranches' <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch)
                      (concatMap ($ components)
                       [ hintDataTypes
                       , hintRecordTypes
                       , hintAxioms])
      mapM checkSolved (newBranches ++ newBranches')

-- | Type should already be reduced here
-- NOTE: Does not reset the state!
-- TODO: Make sure the type is always reduced
tryRefineWith :: Goal -> Type -> SearchBranch -> Component -> SM (Maybe SearchBranch)
tryRefineWith goal goalType branch comp = withBranchAndGoal branch goal $ do

  metasCreatedBy (dumbUnifierErr (compType comp) goalType) >>= \case
    (Nothing, newMetaStore) -> do
      updateStat incRefineSuccess
      -- TODO: Why is newMetaIds not used here?
      newMetaIds <- assignMeta (goalMeta goal) (compTerm comp) goalType
      let newMetaIds' = Map.keys (openMetas newMetaStore)
      reportSDoc "mimer.refine" 60 $
        "Refine: assignMeta created new metas:" <+> prettyTCM newMetaIds

      reportSMDoc "mimer.refine" 50 $ "Refinement succeeded"

      mimerTrace 2 10 $ sep
        [ "Found refinement"
        , nest 2 $ sep [ prettyTCM (compTerm comp)
                       , ":" <+> prettyTCM (compType comp) ] ]
      -- Take the metas stored in the component and add them as sub-goals
      Just <$> updateBranchCost comp (newMetaIds' ++ compMetas comp) branch
    (Just err, _) -> do
      updateStat incRefineFail
      reportSMDoc "mimer.refine" 50 $ "Refinement failed"

      mimerTrace 2 60 $ vcat
        [ "Failed refinement"
        , nest 2 $ sep [ prettyTCM (compTerm comp)
                       , ":" <+> prettyTCM (compType comp) ]
        , nest 2 $ prettyTCM err ]
      return Nothing

tryRefineWith' :: Goal -> Type -> Component -> SM (Maybe ([MetaId], [MetaId]))
tryRefineWith' goal goalType comp = do
  metasCreatedBy (dumbUnifier (compType comp) goalType) >>= \case
    (True, newMetaStore) -> do
      newMetaIds <- assignMeta (goalMeta goal) (compTerm comp) goalType
      let newMetaIds' = Map.keys (openMetas newMetaStore)
      return $ Just (newMetaIds, newMetaIds')
    (False, _) -> return Nothing

-- TODO: Make policy for when state should be put
tryRefineAddMetas :: Goal -> Type -> SearchBranch -> Component -> SM (Maybe SearchBranch)
tryRefineAddMetas goal goalType branch comp = withBranchAndGoal branch goal $ do
  -- Apply the hint to new metas (generating @c@, @c ?@, @c ? ?@, etc.)
  -- TODO: Where is the best place to reduce the hint type?
  comp' <- applyToMetasG Nothing comp
  branch' <- updateBranch [] branch
  tryRefineWith goal goalType branch' comp'

-- TODO: Make sure the type is reduced the first time this is called
-- TODO: Rewrite with Component?
-- NOTE: The new metas are in left-to-right order -- the opposite of the
-- order they should be solved in.
applyToMetas :: Nat -> Term -> Type -> SM (Term, Type, [MetaId])
applyToMetas skip term typ = do
  ctx <- getContextTelescope
  case unEl typ of
    Pi dom abs -> do
      let domainType = unDom dom
      -- TODO: What exactly does the occur check do?
      (metaId', metaTerm) <- bench [Bench.Free] $ newValueMeta DontRunMetaOccursCheck CmpLeq domainType
      let arg = setOrigin Inserted $ metaTerm <$ argFromDom dom
      newType <- bench [Bench.Reduce] $ reduce =<< piApplyM typ metaTerm -- TODO: Is this the best place to reduce?
      -- For records, the parameters are not included in the term
      let newTerm = if skip > 0 then term else apply term [arg]
      (term', typ', metas) <- applyToMetas (predNat skip) newTerm newType
      return (term', typ', metaId' : metas)
    _ -> return (term, typ, [])

normaliseSolution :: Term -> SM Term
normaliseSolution t = do
  norm <- asks searchRewrite
  lift . normalForm norm =<< instantiateFull t

checkSolved :: SearchBranch -> SM SearchStepResult
checkSolved branch = do
  reportSDoc "mimer" 20 $ "Checking if branch is solved"
  reportSDoc "mimer" 30 $ "  remaining subgoals: " <+> prettyTCM (map goalMeta $ sbGoals branch)
  topMetaId <- asks searchTopMeta
  topMeta <- lookupLocalMeta topMetaId
  ii <- asks searchInteractionId
  withInteractionId ii $ withBranchState branch $ do
    metaArgs <- getMetaContextArgs topMeta
    inst <- normaliseSolution $ apply (MetaV topMetaId []) metaArgs
    -- Issue #7639: The subgoals as generated by `applyToMetasG` (and other functions)
    -- are already stored in the `sbGoals` field of the branch.
    -- Here we just prune the subgoals that are already solved by unification.
    goals <- filterM (isNothing <.> getMetaInstantiation . goalMeta) $ sbGoals branch
    case goals of
      -- Issue #378: Blank out variables that are not in scope.
      -- This might leave unsolved metas but is probably better
      -- than generating out-of-scope variables.
      [] -> ResultExpr <$> (blankNotInScope =<< reify inst)
      _ -> do
        return $ OpenBranch branch { sbGoals = goals }

setAt :: Int -> a -> [a] -> [a]
setAt i x xs = case splitAt i xs of
  (ls, _r:rs) -> ls ++ (x : rs)
  _ -> error "setAt: index out of bounds"

updateBranch' :: Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch' mComp newMetaIds branch = do
  state <- getTC
  let compsUsed = sbComponentsUsed branch
  (deltaCost, compsUsed') <- case mComp of
        Nothing -> return (0, compsUsed)
        Just comp -> do
          case compName comp of
            Nothing -> return (compCost comp, compsUsed)
            Just name -> case compsUsed Map.!? name of
              Nothing -> return (compCost comp, Map.insert name 1 compsUsed)
              Just uses -> do
                reuseCost <- asks (costCompReuse . searchCosts)
                return (compCost comp + reuseCost uses, Map.adjust succ name compsUsed)
  return branch{ sbTCState = state
               , sbGoals = map Goal newMetaIds ++ sbGoals branch
               , sbCost = sbCost branch + deltaCost
               , sbComponentsUsed = compsUsed'
               }

updateBranch :: [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch = updateBranch' Nothing

updateBranchCost :: Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranchCost comp = updateBranch' (Just comp)

assignMeta :: MetaId -> Term -> Type -> SM [MetaId]
assignMeta metaId term metaType = bench [Bench.CheckRHS] $ do
  ((), newMetaStore) <- metasCreatedBy $ do
    metaVar <- lookupLocalMeta metaId
    metaArgs <- getMetaContextArgs metaVar

    reportSMDoc "mimer.assignMeta" 60 $ vcat
      [ "Assigning" <+> pretty term
      , nest 2 $ vcat [ "to" <+> pretty metaId <+> ":" <+> pretty metaType
                      , "in context" <+> (pretty =<< getContextTelescope)
                      ]
      ]

    assignV DirLeq metaId metaArgs term (AsTermsOf metaType) `catchError` \err -> do
      reportSMDoc "mimer.assignMeta" 30 $ vcat
        [ "Got error from assignV:" <+> prettyTCM err
        , nest 2 $ vcat
          [ "when trying to assign" <+> prettyTCM term
          , "to" <+> prettyTCM metaId <+> ":" <+> prettyTCM metaType
          , "in context" <+> (inTopContext . prettyTCM =<< getContextTelescope)
          ]
        ]

  let newMetaIds = Map.keys (openMetas newMetaStore)
  return newMetaIds

dumbUnifier :: Type -> Type -> SM Bool
dumbUnifier t1 t2 = isNothing <$> dumbUnifierErr t1 t2

dumbUnifierErr :: Type -> Type -> SM (Maybe TCErr)
dumbUnifierErr t1 t2 = bench [Bench.UnifyIndices] $ do
  updateStat incTypeEqChecks
  noConstraints (Nothing <$ equalType t2 t1) `catchError` \err -> do
    reportSDoc "mimer.unify" 80 $ sep [ "Unification failed with error:", nest 2 $ prettyTCM err ]
    return $ Just err

-- Duplicate of a local definition in Agda.Interaction.BasicOps
showTCM :: (MonadPretty tcm, PrettyTCM a) => a -> tcm String
showTCM v = P.render <$> prettyTCM v

bench :: NFData a => [Bench.Phase] -> SM a -> SM a
bench k ma = billTo (mimerAccount : k) ma
  where
    -- Dummy account to avoid updating Bench. Doesn't matter since this is only used interactively
    -- to debug Mimer performance.
    mimerAccount = Bench.Sort

-- Local variables:
-- getContext :: MonadTCEnv m => m [Dom (Name, Type)]
-- getContextArgs :: (Applicative m, MonadTCEnv m) => m Args
-- getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope
-- getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term]
getLocalVars :: Int -> Cost -> TCM [Component]
getLocalVars localCxt cost = do
  typedTerms <- getLocalVarTerms localCxt
  let varZeroDiscount (Var 0 []) = 1
      varZeroDiscount _          = 0
  mapM (\(term, domTyp) -> newComponent [] (cost - varZeroDiscount term) noName 0 term (unDom domTyp)) typedTerms

getLocalVarTerms :: Int -> TCM [(Term, Dom Type)]
getLocalVarTerms localCxt = do
  contextTerms <- getContextTerms
  contextTypes <- flattenTel <$> getContextTelescope
  let inScope i _ | i < localCxt = pure True   -- Ignore scope for variables we inserted ourselves
      inScope _ Dom{ unDom = name } = do
        x <- abstractToConcrete_ name
        pure $ C.isInScope x == C.InScope
  scope <- mapM (uncurry inScope) =<< getContextVars
  return [ e | (True, e) <- zip scope $ zip contextTerms contextTypes ]



prettyBranch :: SearchBranch -> SM String
prettyBranch branch = withBranchState branch $ do
    metaId <- asks searchTopMeta
    P.render <$> "Branch" <> braces (sep $ punctuate ","
      [ "cost:" <+> pretty (sbCost branch)
      , "metas:" <+> prettyTCM (map goalMeta (sbGoals branch))
      , sep [ "instantiation:"
            , nest 2 $ pretty metaId <+> "=" <+> (prettyTCM =<< getMetaInstantiation metaId) ]
      , "used components:" <+> pretty (Map.toList $ sbComponentsUsed branch)
      ])


instance Pretty Goal where
  pretty goal = P.pretty $ goalMeta goal

instance Pretty SearchBranch where
  pretty branch = keyValueList
    [ ("sbTCState", "[...]")
    , ("sbGoals", P.pretty $ sbGoals branch)
    , ("sbCost", P.pretty $ sbCost branch)
    , ("sbComponentsUsed", P.pretty $ sbComponentsUsed branch)
    ]


instance PrettyTCM BaseComponents where
  prettyTCM comps = do
    let thisFn = case hintThisFn comps of
          Nothing -> "(nothing)"
          Just comp -> prettyComp comp
    vcat [ "Base components:"
         , nest 2 $ vcat
           [ f "hintFns" (hintFns comps)
           , f "hintDataTypes" (hintDataTypes comps)
           , f "hintRecordTypes" (hintRecordTypes comps)
           , f "hintAxioms" (hintAxioms comps)
           , f "hintLevel" (hintLevel comps)
           , f "hintProjections" (hintProjections comps)
           , "hintThisFn:" <+> thisFn
           , g prettyOpenComp "hintLetVars" (hintLetVars comps)
           , "hintRecVars: Open" <+> pretty (mapSnd unNoSubst <$> openThing (hintRecVars comps))
           , "hintSplitVars: Open" <+> pretty (openThing $ hintSplitVars comps)
           ]
         ]
    where
      prettyComp comp = pretty (compTerm comp) <+> ":" <+> pretty (compType comp)
      prettyOpenComp openComp = "Open" <+> parens (prettyComp $ openThing openComp)
      prettyTCMComp comp = prettyTCM (compTerm comp) <+> ":" <+> prettyTCM (compType comp)
      f = g prettyTCMComp
      g p n [] = n <> ": []"
      g p n xs = (n <> ":") $+$ nest 2 (vcat $ map p xs)


-- -- TODO: Is it possible to derive the pretty instances?
instance Pretty BaseComponents where
  pretty comps = P.vcat
      [ f "hintFns" (hintFns comps)
      , f "hintDataTypes" (hintDataTypes comps)
      , f "hintRecordTypes" (hintRecordTypes comps)
      , f "hintAxioms" (hintAxioms comps)
      , f "hintLevel" (hintLevel comps)
      , f "hintProjections" (hintProjections comps)
      ]
    where
      f n [] = n P.<> ": []"
      f n xs = (n P.<> ":") P.$$ P.nest 2 (P.pretty xs)

instance Pretty SearchOptions where
  pretty opts = P.vcat
    [ "searchBaseComponents:"
    , P.nest 2 $ P.pretty $ searchBaseComponents opts
    , keyValueList
      [ ("searchHintMode", P.pretty $ searchHintMode opts)
      , ("searchTimeout",  P.pretty $ searchTimeout opts)
      , ("searchTopMeta",  P.pretty $ searchTopMeta opts)
      , ("searchTopEnv", "[...]")
      ]
    , "searchCosts:"
    , P.nest 2 (P.pretty $ searchCosts opts)
    ]

instance PrettyTCM SearchOptions where
  prettyTCM opts = vcat
    [ "searchBaseComponents:"
    , nest 2 $ prettyTCM $ searchBaseComponents opts
    , vcat
      [ "searchHintMode:" <+> pretty (searchHintMode opts)
      , "searchTimeout:" <+> pretty (searchTimeout opts)
      , "searchTopMeta:" <+> prettyTCM (searchTopMeta opts)
      , "searchTopEnv: [...]"
      , "searchTopCheckpoint:" <+> prettyTCM (searchTopCheckpoint opts)
      , "searchInteractionId:" <+> pretty (searchInteractionId opts)
      , "searchFnName:" <+> pretty (searchFnName opts)
      , "searchStats: [...]"
      ]
    , "searchCosts:"
    , nest 2 $ pretty $ searchCosts opts
    ]

instance Pretty Component where
  pretty comp = haskellRecord "Component"
    [ ("compId", P.pretty $ compId comp)
    , ("compTerm", P.pretty $ compTerm comp)
    , ("compType", P.pretty $ compType comp)
    , ("compMetas", P.pretty $ compMetas comp)
    , ("compCost", P.pretty $ compCost comp)
    ]

instance Pretty Costs where
  pretty costs = P.align 20 entries
    where
      entries =
        [ ("costLocal:"         , P.pretty $ costLocal costs)
        , ("costFn:"            , P.pretty $ costFn costs)
        , ("costDataCon:"       , P.pretty $ costDataCon costs)
        , ("costRecordCon:"     , P.pretty $ costRecordCon costs)
        , ("costSpeculateProj:" , P.pretty $ costSpeculateProj costs)
        , ("costProj:"          , P.pretty $ costProj costs)
        , ("costAxiom:"         , P.pretty $ costAxiom costs)
        , ("costLet:"           , P.pretty $ costLet costs)
        , ("costLevel:"         , P.pretty $ costLevel costs)
        , ("costSet:"           , P.pretty $ costSet costs)
        , ("costRecCall:"       , P.pretty $ costRecCall costs)
        , ("costNewMeta:"       , P.pretty $ costNewMeta costs)
        , ("costNewHiddenMeta:" , P.pretty $ costNewHiddenMeta costs)
        , ("costCompReuse:"     , "{function}")
        ]

instance PrettyTCM Component where
  prettyTCM Component{..} = parens (prettyTCM compId) <+> sep
    [ sep [ prettyTCM compTerm
          , ":" <+> prettyTCM compType ]
    , parens $ fsep $ punctuate ","
      [ "cost:" <+> prettyTCM compCost
      , "metas:" <+> prettyTCM compMetas
      ]
    ]

instance PrettyTCM MimerResult where
  prettyTCM = \case
    MimerExpr expr    -> pretty expr
    MimerClauses f cl -> "MimerClauses" <+> pretty f <+> "[..]" -- TODO: display the clauses
    MimerNoResult     -> "MimerNoResult"
    MimerList sols    -> "MimerList" <+> pretty sols

concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM f = fmap concat . mapM f

reportSMDoc :: VerboseKey -> VerboseLevel -> SM Doc -> SM ()
reportSMDoc vk vl md = reportSDoc vk vl . runReaderT md =<< ask

mimerTrace :: Int -> VerboseLevel -> SM Doc -> SM ()
mimerTrace ilvl vlvl doc = reportSMDoc "mimer.trace" vlvl $ nest (2 * ilvl) $ "-" <+> doc

haskellRecord :: Doc -> [(Doc, Doc)] -> Doc
haskellRecord name fields = P.sep [ name, P.nest 2 $ P.braces (P.sep $ P.punctuate "," [ P.hang (k P.<+> "=") 2 v | (k, v) <- fields ]) ]

keyValueList :: [(Doc, Doc)] -> Doc
keyValueList kvs = P.braces $ P.sep $ P.punctuate "," [ P.hang (k P.<> ":") 2 v | (k, v) <- kvs ]

writeTime :: (ReadTCState m, MonadError TCErr m, MonadTCM m, MonadDebug m) => InteractionId -> Maybe CPUTime -> m ()
writeTime ii mTime = do
  let time = case mTime of
        Nothing -> "n/a"
        Just (CPUTime t) -> show t
  file <- rangeFile . ipRange <$> lookupInteractionPoint ii
  case file of
    SMaybe.Nothing ->
      reportSLn "mimer.stats" 2 "No file found for interaction id"
    SMaybe.Just file -> do
      let path = filePath (rangeFilePath file) ++ ".stats"
      liftIO $ appendFile path (show (interactionId ii) ++ " " ++ time ++ "\n")

-- Hack to let you experiment with costs using verbosity flags.
customCosts :: TCM Costs
customCosts = do
  costLocal         <- cost "local"
  costFn            <- cost "fn"
  costDataCon       <- cost "dataCon"
  costRecordCon     <- cost "recordCon"
  costSpeculateProj <- cost "speculateProj"
  costProj          <- cost "proj"
  costAxiom         <- cost "axiom"
  costLet           <- cost "let"
  costLevel         <- cost "level"
  costSet           <- cost "set"
  costRecCall       <- cost "recCall"
  costNewMeta       <- cost "newMeta"
  costNewHiddenMeta <- cost "newHiddenMeta"
  compReuse         <- cost "compReuse"
  let costCompReuse uses = compReuse * uses ^ 2
  pure Costs{..}
  where
    cost key = getVerbosityLevel ("mimer-cost." ++ key)

getVerbosityLevel :: MonadDebug m => VerboseKey -> m VerboseLevel
getVerbosityLevel k = do
  t <- getVerbosity
  return $ case t of
    Strict.Nothing -> 1
    Strict.Just t
      | t == Trie.singleton [] 0 -> 0
      | otherwise -> lastWithDefault 0 $ Trie.lookupPath ks t
  where ks = parseVerboseKey k