    -- | 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 ((forall x. MimerResult -> Rep MimerResult x)
    -> (forall x. Rep MimerResult x -> MimerResult)
    -> Generic MimerResult
    forall x. Rep MimerResult x -> MimerResult
    forall x. MimerResult -> Rep MimerResult x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. MimerResult -> Rep MimerResult x
    from :: forall x. MimerResult -> Rep MimerResult x
    $cto :: forall x. Rep MimerResult x -> MimerResult
    to :: forall x. Rep MimerResult x -> MimerResult
    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 :: forall (tcm :: * -> *).
    MonadTCM tcm =>
    Rewrite -> InteractionId -> Range -> ArgName -> tcm MimerResult
    mimer Rewrite
    norm InteractionId
    ii Range
    rng ArgName
    argStr = TCM MimerResult -> tcm MimerResult
    forall a. TCM a -> tcm a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM MimerResult -> tcm MimerResult)
    -> TCM MimerResult -> tcm MimerResult
    forall a b. (a -> b) -> a -> b
    $ do
        ArgName -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.top" VerboseLevel
    10 do
          TCMT IO Doc
    "Running Mimer on interaction point" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> InteractionId -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty InteractionId
    ii TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "with argument string" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> ArgName
    forall a. Show a => a -> ArgName
    show ArgName
    argStr)

        start <- IO CPUTime -> TCMT IO CPUTime
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO CPUTime -> TCMT IO CPUTime) -> IO CPUTime -> TCMT IO CPUTime
    forall a b. (a -> b) -> a -> b
    $ IO CPUTime
    forall (m :: * -> *). MonadIO m => m CPUTime
    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
                ArgName -> VerboseLevel -> ArgName -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> ArgName -> m ()
    reportSLn ArgName
    "mimer.top" VerboseLevel
    10 ArgName
    "No solution found"
                MimerResult -> TCM MimerResult
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MimerResult
    MimerNoResult
              [(VerboseLevel, MimerResult)]
    sols' | Options -> Bool
    optList Options
    opts -> MimerResult -> TCM MimerResult
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MimerResult -> TCM MimerResult) -> MimerResult -> TCM MimerResult
    forall a b. (a -> b) -> a -> b
    $ [(VerboseLevel, ArgName)] -> MimerResult
    MimerList [ (VerboseLevel
    i, ArgName
    s) | (VerboseLevel
    i, MimerExpr ArgName
    s) <- [(VerboseLevel, MimerResult)]
    sols' ]
              (VerboseLevel
    _, MimerResult
    sol) : [(VerboseLevel, MimerResult)]
    _ -> do
                ArgName -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.top" VerboseLevel
    10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Solution:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MimerResult -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MimerResult -> m Doc
    prettyTCM MimerResult
    sol
                MimerResult -> TCM MimerResult
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MimerResult
    sol

        -- Print timing statistic.
        stop <- liftIO $ getCPUTime
        let time = CPUTime
    stop CPUTime -> CPUTime -> CPUTime
    forall a. Num a => a -> a -> a
    - CPUTime
    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
      { SearchBranch -> TCState
    sbTCState :: TCState
      , SearchBranch -> [Goal]
    sbGoals :: [Goal]
      , SearchBranch -> VerboseLevel
    sbCost :: Int
      , SearchBranch -> Map CheckpointId ComponentCache
    sbCache :: Map CheckpointId ComponentCache
      , SearchBranch -> Map Name VerboseLevel
    sbComponentsUsed :: Map Name Int -- ^ Number of times each component has been used
      }
      deriving ((forall x. SearchBranch -> Rep SearchBranch x)
    -> (forall x. Rep SearchBranch x -> SearchBranch)
    -> Generic SearchBranch
    forall x. Rep SearchBranch x -> SearchBranch
    forall x. SearchBranch -> Rep SearchBranch x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. SearchBranch -> Rep SearchBranch x
    from :: forall x. SearchBranch -> Rep SearchBranch x
    $cto :: forall x. Rep SearchBranch x -> SearchBranch
    to :: forall x. Rep SearchBranch x -> SearchBranch
    Generic)
    instance NFData SearchBranch

    -- | NOTE: Equality is only on the fields `sbCost` and `sbGoals`
    instance Eq SearchBranch where
      SearchBranch
    sb1 == :: SearchBranch -> SearchBranch -> Bool
    == SearchBranch
    sb2 = SearchBranch -> VerboseLevel
    sbCost SearchBranch
    sb1 VerboseLevel -> VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == SearchBranch -> VerboseLevel
    sbCost SearchBranch
    sb2 Bool -> Bool -> Bool
    && SearchBranch -> [Goal]
    sbGoals SearchBranch
    sb1 [Goal] -> [Goal] -> Bool
    forall a. Eq a => a -> a -> Bool
    == SearchBranch -> [Goal]
    sbGoals SearchBranch
    sb2

    -- TODO: Explain
    instance Ord SearchBranch where
      compare :: SearchBranch -> SearchBranch -> Ordering
    compare = VerboseLevel -> VerboseLevel -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (VerboseLevel -> VerboseLevel -> Ordering)
    -> (SearchBranch -> VerboseLevel)
    -> SearchBranch
    -> SearchBranch
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` SearchBranch -> VerboseLevel
    sbCost

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

    data Goal = Goal
      { Goal -> MetaId
    goalMeta :: MetaId
      }
      deriving ((forall x. Goal -> Rep Goal x)
    -> (forall x. Rep Goal x -> Goal) -> Generic Goal
    forall x. Rep Goal x -> Goal
    forall x. Goal -> Rep Goal x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Goal -> Rep Goal x
    from :: forall x. Goal -> Rep Goal x
    $cto :: forall x. Rep Goal x -> Goal
    to :: forall x. Rep Goal x -> Goal
    Generic)
    instance NFData Goal

    -- TODO: Is this a reasonable Eq instance?
    instance Eq Goal where
      Goal
    g1 == :: Goal -> Goal -> Bool
    == Goal
    g2 = Goal -> MetaId
    goalMeta Goal
    g1 MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    == Goal -> MetaId
    goalMeta Goal
    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
      { BaseComponents -> [Component]
    hintFns :: [Component]
      , BaseComponents -> [Component]
    hintDataTypes :: [Component]
      , BaseComponents -> [Component]
    hintRecordTypes :: [Component]
      , BaseComponents -> [Component]
    hintAxioms :: [Component]
      -- ^ Excluding those producing Level
      , BaseComponents -> [Component]
    hintLevel :: [Component]
      -- ^ A definition in a where clause
      , BaseComponents -> [Component]
    hintProjections :: [Component]
      -- ^ Variables that are candidates for arguments to recursive calls
      , BaseComponents -> Maybe Component
    hintThisFn :: Maybe Component
      , BaseComponents -> [Open Component]
    hintLetVars :: [Open Component]
      , BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)]
    hintRecVars :: Open [(Term, NoSubst Term Int)] -- ^ Variable terms and which argument they come from
      , BaseComponents -> Open [Term]
    hintSplitVars :: Open [Term]
      }
      deriving ((forall x. BaseComponents -> Rep BaseComponents x)
    -> (forall x. Rep BaseComponents x -> BaseComponents)
    -> Generic BaseComponents
    forall x. Rep BaseComponents x -> BaseComponents
    forall x. BaseComponents -> Rep BaseComponents x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. BaseComponents -> Rep BaseComponents x
    from :: forall x. BaseComponents -> Rep BaseComponents x
    $cto :: forall x. Rep BaseComponents x -> BaseComponents
    to :: forall x. Rep BaseComponents x -> BaseComponents
    Generic)

    instance NFData BaseComponents

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

    instance NFData Component

    -- TODO: Is this reasonable?
    instance Ord Component where
      compare :: Component -> Component -> Ordering
    compare = VerboseLevel -> VerboseLevel -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (VerboseLevel -> VerboseLevel -> Ordering)
    -> (Component -> VerboseLevel)
    -> Component
    -> Component
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Component -> VerboseLevel
    compId

    data SearchStepResult
      = ResultExpr Expr
      | ResultClauses [A.Clause]
      | OpenBranch SearchBranch
      | NoSolution
      deriving ((forall x. SearchStepResult -> Rep SearchStepResult x)
    -> (forall x. Rep SearchStepResult x -> SearchStepResult)
    -> Generic SearchStepResult
    forall x. Rep SearchStepResult x -> SearchStepResult
    forall x. SearchStepResult -> Rep SearchStepResult x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. SearchStepResult -> Rep SearchStepResult x
    from :: forall x. SearchStepResult -> Rep SearchStepResult x
    $cto :: forall x. Rep SearchStepResult x -> SearchStepResult
    to :: forall x. Rep SearchStepResult x -> SearchStepResult
    Generic)
    instance NFData SearchStepResult

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

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

    noCost :: Cost
    noCost :: VerboseLevel
    noCost = VerboseLevel
    0

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

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

    predNat :: Nat -> Nat
    predNat :: VerboseLevel -> VerboseLevel
    predNat VerboseLevel
    n | VerboseLevel
    n VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    > VerboseLevel
    0 = VerboseLevel
    n VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    - VerboseLevel
    1
              | VerboseLevel
    n VerboseLevel -> VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == VerboseLevel
    0 = VerboseLevel
    0
              | Bool
    otherwise = ArgName -> VerboseLevel
    forall a. HasCallStack => ArgName -> a
    error ArgName
    "predNat of negative value"

    getRecordFields :: (HasConstInfo tcm, MonadTCM tcm) => QName -> tcm [QName]
    getRecordFields :: forall (tcm :: * -> *).
    (HasConstInfo tcm, MonadTCM tcm) =>
    QName -> tcm [QName]
    getRecordFields = (Definition -> [QName]) -> tcm Definition -> tcm [QName]
    forall a b. (a -> b) -> tcm a -> tcm b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Dom' Term QName -> QName) -> [Dom' Term QName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term QName -> QName
    forall t e. Dom' t e -> e
    unDom ([Dom' Term QName] -> [QName])
    -> (Definition -> [Dom' Term QName]) -> Definition -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Defn -> [Dom' Term QName]
    recFields (Defn -> [Dom' Term QName])
    -> (Definition -> Defn) -> Definition -> [Dom' Term QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef) (tcm Definition -> tcm [QName])
    -> (QName -> tcm Definition) -> QName -> tcm [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> tcm Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo

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

    getOpenComponent :: (MonadTCM tcm, MonadDebug tcm) => Open Component -> tcm Component
    getOpenComponent :: forall (tcm :: * -> *).
    (MonadTCM tcm, MonadDebug tcm) =>
    Open Component -> tcm Component
    getOpenComponent Open Component
    openComp = do
      let comp :: Component
    comp = Open Component -> Component
    forall a. Open a -> a
    openThing Open Component
    openComp
      ArgName -> VerboseLevel -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.components.open" VerboseLevel
    40 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Opening component" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> VerboseLevel -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
    prettyTCM (Component -> VerboseLevel
    compId Component
    comp) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Maybe Name -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Maybe Name -> m Doc
    prettyTCM (Component -> Maybe Name
    compName Component
    comp)
      term <- Open Term -> tcm Term
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen (Open Term -> tcm Term) -> Open Term -> tcm Term
    forall a b. (a -> b) -> a -> b
    $ Component -> Term
    compTerm (Component -> Term) -> Open Component -> Open Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Open Component
    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 :: VerboseLevel
    -> [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> Component
    mkComponent VerboseLevel
    cId [MetaId]
    metaIds VerboseLevel
    cost Maybe Name
    mName VerboseLevel
    pars Term
    term Type
    typ = Component
      { compId :: VerboseLevel
    compId    = VerboseLevel
    cId
      , compName :: Maybe Name
    compName  = Maybe Name
    mName
      , compPars :: VerboseLevel
    compPars  = VerboseLevel
    pars
      , compTerm :: Term
    compTerm  = Term
    term
      , compType :: Type
    compType  = Type
    typ
      , compRec :: Bool
    compRec   = Bool
    False
      , compMetas :: [MetaId]
    compMetas = [MetaId]
    metaIds
      , compCost :: VerboseLevel
    compCost  = VerboseLevel
    cost }

    mkComponentQ :: CompId -> Cost -> QName -> Nat -> Term -> Type -> Component
    mkComponentQ :: VerboseLevel
    -> VerboseLevel
    -> QName
    -> VerboseLevel
    -> Term
    -> Type
    -> Component
    mkComponentQ VerboseLevel
    cId VerboseLevel
    cost QName
    qname = VerboseLevel
    -> [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> Component
    mkComponent VerboseLevel
    cId [] VerboseLevel
    cost (Name -> Maybe Name
    forall a. a -> Maybe a
    Just (Name -> Maybe Name) -> Name -> Maybe Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    qname)

    noName :: Maybe Name
    noName :: Maybe Name
    noName = Maybe Name
    forall a. Maybe a
    Nothing

    newComponent :: MonadFresh CompId m => [MetaId] -> Cost -> Maybe Name -> Nat -> Term -> Type -> m Component
    newComponent :: forall (m :: * -> *).
    MonadFresh VerboseLevel m =>
    [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> m Component
    newComponent [MetaId]
    metaIds VerboseLevel
    cost Maybe Name
    mName VerboseLevel
    pars Term
    term Type
    typ = m VerboseLevel
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh m VerboseLevel -> (VerboseLevel -> Component) -> m Component
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \VerboseLevel
    cId -> VerboseLevel
    -> [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> Component
    mkComponent VerboseLevel
    cId [MetaId]
    metaIds VerboseLevel
    cost Maybe Name
    mName VerboseLevel
    pars Term
    term Type
    typ

    newComponentQ :: MonadFresh CompId m => [MetaId] -> Cost -> QName -> Nat -> Term -> Type -> m Component
    newComponentQ :: forall (m :: * -> *).
    MonadFresh VerboseLevel m =>
    [MetaId]
    -> VerboseLevel
    -> QName
    -> VerboseLevel
    -> Term
    -> Type
    -> m Component
    newComponentQ [MetaId]
    metaIds VerboseLevel
    cost QName
    qname VerboseLevel
    pars Term
    term Type
    typ = m VerboseLevel
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh m VerboseLevel -> (VerboseLevel -> Component) -> m Component
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \VerboseLevel
    cId -> VerboseLevel
    -> [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> Component
    mkComponent VerboseLevel
    cId [MetaId]
    metaIds VerboseLevel
    cost (Name -> Maybe Name
    forall a. a -> Maybe a
    Just (Name -> Maybe Name) -> Name -> Maybe Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    qname) VerboseLevel
    pars Term
    term Type
    typ

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

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

    withBranchState :: SearchBranch -> SM a -> SM a
    withBranchState :: forall a. SearchBranch -> SM a -> SM a
    withBranchState SearchBranch
    br SM a
    ma = do
      TCState -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC (SearchBranch -> TCState
    sbTCState SearchBranch
    br)
      SM a
    ma

    withBranchAndGoal :: SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal :: forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    br Goal
    goal SM a
    ma = Goal -> SM a -> SM a
    forall a. Goal -> SM a -> SM a
    inGoalEnv Goal
    goal (SM a -> SM a) -> SM a -> SM a
    forall a b. (a -> b) -> a -> b
    $ SearchBranch -> SM a -> SM a
    forall a. SearchBranch -> SM a -> SM a
    withBranchState SearchBranch
    br SM a
    ma

    inGoalEnv :: Goal -> SM a -> SM a
    inGoalEnv :: forall a. Goal -> SM a -> SM a
    inGoalEnv Goal
    goal  SM a
    ret = do
      ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.env" VerboseLevel
    70 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "going into environment of goal" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM (Goal -> MetaId
    goalMeta Goal
    goal)
      MetaId -> SM a -> SM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
     ReadTCState m) =>
    MetaId -> m a -> m a
    withMetaId (Goal -> MetaId
    goalMeta Goal
    goal) SM a
    ret

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

    -- TODO: Rename (see metaInstantiation)
    getMetaInstantiation :: (MonadTCM tcm, PureTCM tcm, MonadDebug tcm, MonadInteractionPoints tcm, MonadFresh NameId tcm)
      => MetaId -> tcm (Maybe Expr)
    getMetaInstantiation :: forall (tcm :: * -> *).
    (MonadTCM tcm, PureTCM tcm, MonadDebug tcm,
     MonadInteractionPoints tcm, MonadFresh NameId tcm) =>
    MetaId -> tcm (Maybe Expr)
    getMetaInstantiation = MetaId -> tcm (Maybe Term)
    forall (tcm :: * -> *).
    (MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) =>
    MetaId -> tcm (Maybe Term)
    metaInstantiation (MetaId -> tcm (Maybe Term))
    -> (Maybe Term -> tcm (Maybe Expr)) -> MetaId -> tcm (Maybe Expr)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> (Term -> tcm Expr) -> Maybe Term -> tcm (Maybe Expr)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse (Term -> tcm Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (Term -> tcm Term) -> (Term -> tcm Expr) -> Term -> tcm Expr
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Term -> tcm Expr
    Term -> tcm (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify)

    metaInstantiation :: (MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) => MetaId -> tcm (Maybe Term)
    metaInstantiation :: forall (tcm :: * -> *).
    (MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) =>
    MetaId -> tcm (Maybe Term)
    metaInstantiation MetaId
    metaId = MetaId -> tcm MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    metaId tcm MetaVariable
    -> (MetaVariable -> MetaInstantiation) -> tcm MetaInstantiation
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> MetaVariable -> MetaInstantiation
    mvInstantiation tcm MetaInstantiation
    -> (MetaInstantiation -> tcm (Maybe Term)) -> tcm (Maybe Term)
    forall a b. tcm a -> (a -> tcm b) -> tcm b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      InstV Instantiation
    inst -> Maybe Term -> tcm (Maybe Term)
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Term -> tcm (Maybe Term)) -> Maybe Term -> tcm (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Instantiation -> Term
    instBody Instantiation
    inst
      MetaInstantiation
    _ -> Maybe Term -> tcm (Maybe Term)
    forall a. a -> tcm a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Term
    forall a. Maybe a
    Nothing

    -- TODO: why not also accept pattern record types here?
    isTypeDatatype :: (MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) => Type -> tcm Bool
    isTypeDatatype :: forall (tcm :: * -> *).
    (MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) =>
    Type -> tcm Bool
    isTypeDatatype Type
    typ = TCM Bool -> tcm Bool
    forall a. TCM a -> tcm a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM do
      Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    typ TCMT IO Type -> (Type -> Term) -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> Type -> Term
    forall t a. Type'' t a -> a
    unEl TCMT IO Term
    -> (Term -> TCMT IO (Maybe (QName, DataOrRecord)))
    -> TCMT IO (Maybe (QName, DataOrRecord))
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Term -> TCMT IO (Maybe (QName, DataOrRecord))
    isDataOrRecord TCMT IO (Maybe (QName, DataOrRecord))
    -> (Maybe (QName, DataOrRecord) -> Bool) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
        Just (QName
    _, DataOrRecord
    IsData) -> Bool
    True
        Maybe (QName, DataOrRecord)
    _ -> Bool
    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 :: Options
    -> Costs
    -> InteractionId
    -> Maybe QName
    -> [QName]
    -> MetaId
    -> TCM BaseComponents
    collectComponents Options
    opts Costs
    costs InteractionId
    ii Maybe QName
    mDefName [QName]
    whereNames MetaId
    metaId = do

      lhsVars <- InteractionId -> TCMT IO (Open [(Term, Maybe VerboseLevel)])
    forall (tcm :: * -> *).
    (ReadTCState tcm, MonadError TCErr tcm, MonadTCM tcm,
     HasConstInfo tcm) =>
    InteractionId -> tcm (Open [(Term, Maybe VerboseLevel)])
    collectLHSVars InteractionId
    ii
      let recVars = Open [(Term, Maybe VerboseLevel)]
    lhsVars Open [(Term, Maybe VerboseLevel)]
    -> ([(Term, Maybe VerboseLevel)]
        -> [(Term, NoSubst Term VerboseLevel)])
    -> Open [(Term, NoSubst Term VerboseLevel)]
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ [(Term, Maybe VerboseLevel)]
    vars -> [ (Term
    tm, VerboseLevel -> NoSubst Term VerboseLevel
    forall t a. a -> NoSubst t a
    NoSubst VerboseLevel
    i) | (Term
    tm, Just VerboseLevel
    i) <- [(Term, Maybe VerboseLevel)]
    vars ]

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

      -- Prepare the initial component record
      letVars <- getLetVars (costLet costs)
      let components = BaseComponents
            { hintFns :: [Component]
    hintFns = []
            , hintDataTypes :: [Component]
    hintDataTypes = []
            , hintRecordTypes :: [Component]
    hintRecordTypes = []
            , hintProjections :: [Component]
    hintProjections = []
            , hintAxioms :: [Component]
    hintAxioms = []
            , hintLevel :: [Component]
    hintLevel = []
            , hintThisFn :: Maybe Component
    hintThisFn = Maybe Component
    forall a. Maybe a
    Nothing
            , hintRecVars :: Open [(Term, NoSubst Term VerboseLevel)]
    hintRecVars = Open [(Term, NoSubst Term VerboseLevel)]
    recVars
            , hintLetVars :: [Open Component]
    hintLetVars = [Open Component]
    letVars
            , hintSplitVars :: Open [Term]
    hintSplitVars = Open [Term]
    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 :: HintMode
    hintMode = Options -> HintMode
    optHintMode Options
    opts
        explicitHints :: [QName]
    explicitHints = Options -> [QName]
    optExplicitHints Options
    opts
        -- Sort by the arity of the type
        doSort :: [Component] -> [Component]
    doSort = (Component -> VerboseLevel) -> [Component] -> [Component]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    sortOn (Type -> VerboseLevel
    arity (Type -> VerboseLevel)
    -> (Component -> Type) -> Component -> VerboseLevel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Component -> Type
    compType)

        isNotMutual :: QName -> Defn -> Bool
    isNotMutual QName
    qname Defn
    f = case Maybe QName
    mDefName of
          Maybe QName
    Nothing -> Bool
    True
          Just QName
    defName -> QName
    defName QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    /= QName
    qname Bool -> Bool -> Bool
    && ([QName] -> Bool) -> Maybe [QName] -> Maybe Bool
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName
    defName QName -> [QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem`) (Defn -> Maybe [QName]
    funMutual Defn
    f) Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True

        go :: (Type -> Bool)
    -> ScopeInfo -> BaseComponents -> QName -> TCM BaseComponents
    go Type -> Bool
    isToLevel ScopeInfo
    scope BaseComponents
    comps QName
    qname = do
            def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    qname
            let typ = Definition -> Type
    defType Definition
    def
            case theDef def of
              Axiom{}
                | Type -> Bool
    isToLevel Type
    typ -> TCM BaseComponents
    addLevel
                | Bool
    shouldKeep    -> TCM BaseComponents
    addAxiom
                | Bool
    otherwise     -> TCM BaseComponents
    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 :: Defn
    f@Function{ funWith :: Defn -> Maybe QName
    funWith = Maybe QName
    Nothing, funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Maybe ExtLamInfo
    Nothing }
                | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    qname Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mDefName   -> TCM BaseComponents
    addThisFn
                | Bool
    notMutual, Type -> Bool
    isToLevel Type
    typ -> TCM BaseComponents
    addLevel
                | Bool
    notMutual, Bool
    shouldKeep    -> TCM BaseComponents
    addFn
                where notMutual :: Bool
    notMutual = QName -> Defn -> Bool
    isNotMutual QName
    qname Defn
    f
              Function{} -> TCM BaseComponents
    done
              Datatype{} -> TCM BaseComponents
    addData
              Record{} -> do
                projections <- (QName -> TCMT IO Component) -> [QName] -> TCMT IO [Component]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (VerboseLevel -> QName -> TCMT IO Component
    forall (tcm :: * -> *).
    (HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
     MonadTCM tcm) =>
    VerboseLevel -> QName -> tcm Component
    qnameToComponent (Costs -> VerboseLevel
    costSpeculateProj Costs
    costs)) ([QName] -> TCMT IO [Component])
    -> TCMT IO [QName] -> TCMT IO [Component]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO [QName]
    forall (tcm :: * -> *).
    (HasConstInfo tcm, MonadTCM tcm) =>
    QName -> tcm [QName]
    getRecordFields QName
    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{} -> TCM BaseComponents
    done
              -- TODO: special treatment for primitives?
              Primitive{}
                | Type -> Bool
    isToLevel Type
    typ  -> TCM BaseComponents
    addLevel
                | Bool
    shouldKeep     -> TCM BaseComponents
    addFn
                | Bool
    otherwise      -> TCM BaseComponents
    done
              PrimitiveSort{}    -> TCM BaseComponents
    done
              -- TODO: Check if we want to use these
              DataOrRecSig{}     -> TCM BaseComponents
    done
              GeneralizableVar{} -> TCM BaseComponents
    done
              AbstractDefn{}     -> TCM BaseComponents
    done
            where
              done :: TCM BaseComponents
    done = BaseComponents -> TCM BaseComponents
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return BaseComponents
    comps
              -- TODO: There is probably a better way of finding the module name
              mThisModule :: Maybe ModuleName
    mThisModule = QName -> ModuleName
    qnameModule (QName -> ModuleName) -> Maybe QName -> Maybe ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe QName
    mDefName

              shouldKeep :: Bool
    shouldKeep = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or
                [ QName
    qname QName -> [QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    explicitHints
                , QName
    qname QName -> [QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    whereNames
                , case HintMode
    hintMode of
                    HintMode
    Unqualified -> QName -> ScopeInfo -> Bool
    Scope.isNameInScopeUnqualified QName
    qname ScopeInfo
    scope
                    HintMode
    AllModules  -> Bool
    True
                    HintMode
    Module      -> ModuleName -> Maybe ModuleName
    forall a. a -> Maybe a
    Just (QName -> ModuleName
    qnameModule QName
    qname) Maybe ModuleName -> Maybe ModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe ModuleName
    mThisModule
                    HintMode
    NoHints     -> Bool
    False
                ]
              addLevel :: TCM BaseComponents
    addLevel  = VerboseLevel -> QName -> TCMT IO Component
    forall (tcm :: * -> *).
    (HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
     MonadTCM tcm) =>
    VerboseLevel -> QName -> tcm Component
    qnameToComponent (Costs -> VerboseLevel
    costLevel   Costs
    costs) QName
    qname TCMT IO Component
    -> (Component -> BaseComponents) -> TCM BaseComponents
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Component
    comp -> BaseComponents
    comps{hintLevel     = comp : hintLevel  comps}
              addAxiom :: TCM BaseComponents
    addAxiom  = VerboseLevel -> QName -> TCMT IO Component
    forall (tcm :: * -> *).
    (HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
     MonadTCM tcm) =>
    VerboseLevel -> QName -> tcm Component
    qnameToComponent (Costs -> VerboseLevel
    costAxiom   Costs
    costs) QName
    qname TCMT IO Component
    -> (Component -> BaseComponents) -> TCM BaseComponents
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Component
    comp -> BaseComponents
    comps{hintAxioms    = comp : hintAxioms comps}
              addThisFn :: TCM BaseComponents
    addThisFn = VerboseLevel -> QName -> TCMT IO Component
    forall (tcm :: * -> *).
    (HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
     MonadTCM tcm) =>
    VerboseLevel -> QName -> tcm Component
    qnameToComponent (Costs -> VerboseLevel
    costRecCall Costs
    costs) QName
    qname TCMT IO Component
    -> (Component -> BaseComponents) -> TCM BaseComponents
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Component
    comp -> BaseComponents
    comps{hintThisFn    = Just comp{ compRec = True }}
              addFn :: TCM BaseComponents
    addFn     = VerboseLevel -> QName -> TCMT IO Component
    forall (tcm :: * -> *).
    (HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
     MonadTCM tcm) =>
    VerboseLevel -> QName -> tcm Component
    qnameToComponent (Costs -> VerboseLevel
    costFn      Costs
    costs) QName
    qname TCMT IO Component
    -> (Component -> BaseComponents) -> TCM BaseComponents
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Component
    comp -> BaseComponents
    comps{hintFns       = comp : hintFns comps}
              addData :: TCM BaseComponents
    addData   = VerboseLevel -> QName -> TCMT IO Component
    forall (tcm :: * -> *).
    (HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
     MonadTCM tcm) =>
    VerboseLevel -> QName -> tcm Component
    qnameToComponent (Costs -> VerboseLevel
    costSet     Costs
    costs) QName
    qname TCMT IO Component
    -> (Component -> BaseComponents) -> TCM BaseComponents
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Component
    comp -> BaseComponents
    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 :: TCM (Type -> Bool)
    endsInLevelTester = do
      BuiltinId -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    BuiltinId -> m (Maybe QName)
    getBuiltinName BuiltinId
    builtinLevel TCMT IO (Maybe QName)
    -> (Maybe QName -> TCM (Type -> Bool)) -> TCM (Type -> Bool)
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe QName
    Nothing    -> (Type -> Bool) -> TCM (Type -> Bool)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Type -> Bool) -> TCM (Type -> Bool))
    -> (Type -> Bool) -> TCM (Type -> Bool)
    forall a b. (a -> b) -> a -> b
    $ Bool -> Type -> Bool
    forall a b. a -> b -> a
    const Bool
    False
        Just QName
    level -> (Type -> Bool) -> TCM (Type -> Bool)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return \ Type
    t ->
          -- NOTE: We do not reduce the type before checking, so some user definitions
          -- will not be included here.
          case Type -> TelView
    telView' Type
    t of
            TelV Telescope
    _ (El Sort' Term
    _ (Def QName
    x Elims
    _)) -> QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    level
            TelView
    _ -> Bool
    False

    qnameToComponent :: (HasConstInfo tcm, ReadTCState tcm, MonadFresh CompId tcm, MonadTCM tcm)
      => Cost -> QName -> tcm Component
    qnameToComponent :: forall (tcm :: * -> *).
    (HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
     MonadTCM tcm) =>
    VerboseLevel -> QName -> tcm Component
    qnameToComponent VerboseLevel
    cost QName
    qname = do
      defn <- QName -> tcm Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    qname
      -- #7120: we need to apply the module params to everything
      mParams <- freeVarsToApply qname
      let def = (QName -> Elims -> Term
    Def QName
    qname [] Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` Args
    mParams, VerboseLevel
    0)
      let (term, pars) = case theDef defn of
            c :: Defn
    c@Constructor{}    -> (ConHead -> ConInfo -> Elims -> Term
    Con (Defn -> ConHead
    conSrcCon Defn
    c) ConInfo
    ConOCon [], Defn -> VerboseLevel
    conPars Defn
    c VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    - Args -> VerboseLevel
    forall a. [a] -> VerboseLevel
    forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
    length Args
    mParams)
            Axiom{}            -> (Term, VerboseLevel)
    def
            GeneralizableVar{} -> (Term, VerboseLevel)
    def
            Function{}         -> (Term, VerboseLevel)
    def
            Datatype{}         -> (Term, VerboseLevel)
    def
            Record{}           -> (Term, VerboseLevel)
    def
            Primitive{}        -> (Term, VerboseLevel)
    def
            PrimitiveSort{}    -> (Term, VerboseLevel)
    def
            DataOrRecSig{}     -> (Term, VerboseLevel)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            AbstractDefn{}     -> (Term, VerboseLevel)
    forall a. HasCallStack => a
    __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 :: MetaVariable -> [QName]
    getEverythingInScope MetaVariable
    metaVar = do
      let scope :: ScopeInfo
    scope = Closure Range -> ScopeInfo
    forall a. Closure a -> ScopeInfo
    clScope (Closure Range -> ScopeInfo) -> Closure Range -> ScopeInfo
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Closure Range
    getMetaInfo MetaVariable
    metaVar
      let nameSpace :: NameSpace
    nameSpace = ScopeInfo -> NameSpace
    Scope.everythingInScope ScopeInfo
    scope
          names :: NamesInScope
    names = NameSpace -> NamesInScope
    Scope.nsNames NameSpace
    nameSpace
          validKind :: KindOfName -> Bool
    validKind = \ case
            KindOfName
    Scope.PatternSynName           -> Bool
    False   -- could consider allowing pattern synonyms, but the problem is they can't be getConstInfo'd
            KindOfName
    Scope.GeneralizeName           -> Bool
    False   -- and any way finding the underlying constructors should be easy
            KindOfName
    Scope.DisallowedGeneralizeName -> Bool
    False
            KindOfName
    Scope.MacroName                -> Bool
    False
            KindOfName
    Scope.QuotableName             -> Bool
    False
            KindOfName
    Scope.ConName                  -> Bool
    True
            KindOfName
    Scope.CoConName                -> Bool
    True
            KindOfName
    Scope.FldName                  -> Bool
    True
            KindOfName
    Scope.DataName                 -> Bool
    True
            KindOfName
    Scope.RecName                  -> Bool
    True
            KindOfName
    Scope.FunName                  -> Bool
    True
            KindOfName
    Scope.AxiomName                -> Bool
    True
            KindOfName
    Scope.PrimName                 -> Bool
    True
            KindOfName
    Scope.OtherDefName             -> Bool
    True
          qnames :: [QName]
    qnames = (AbstractName -> QName) -> [AbstractName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map AbstractName -> QName
    Scope.anameName
                 ([AbstractName] -> [QName])
    -> ([NonEmpty AbstractName] -> [AbstractName])
    -> [NonEmpty AbstractName]
    -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName -> Bool) -> [AbstractName] -> [AbstractName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (KindOfName -> Bool
    validKind (KindOfName -> Bool)
    -> (AbstractName -> KindOfName) -> AbstractName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    Scope.anameKind)
                 ([AbstractName] -> [AbstractName])
    -> ([NonEmpty AbstractName] -> [AbstractName])
    -> [NonEmpty AbstractName]
    -> [AbstractName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NonEmpty AbstractName -> AbstractName)
    -> [NonEmpty AbstractName] -> [AbstractName]
    forall a b. (a -> b) -> [a] -> [b]
    map NonEmpty AbstractName -> AbstractName
    forall a. NonEmpty a -> a
    NonEmptyList.head
                 ([NonEmpty AbstractName] -> [QName])
    -> [NonEmpty AbstractName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ NamesInScope -> [NonEmpty AbstractName]
    forall k a. Map k a -> [a]
    Map.elems NamesInScope
    names
      [QName]
    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 :: forall (tcm :: * -> *).
    (MonadFresh VerboseLevel tcm, MonadTCM tcm, Monad tcm) =>
    VerboseLevel -> tcm [Open Component]
    getLetVars VerboseLevel
    cost = do
      bindings <- (TCEnv -> LetBindings) -> tcm LetBindings
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> LetBindings
    envLetBindings
      mapM makeComp $ Map.toAscList bindings
      where
        makeComp :: (Name, Open LetBinding) -> tcm (Open Component)
        makeComp :: (Name, Open LetBinding) -> tcm (Open Component)
    makeComp (Name
    name, Open LetBinding
    opn) = do
          cId <- tcm VerboseLevel
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
          return $ opn <&> \ (LetBinding Origin
    _origin Term
    term Dom Type
    typ) ->
                    VerboseLevel
    -> [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> Component
    mkComponent VerboseLevel
    cId [] VerboseLevel
    cost (Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    name) VerboseLevel
    0 Term
    term (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    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 :: Open [(Term, Maybe VerboseLevel)] -> TCMT IO (Open [Term])
    getSplitVars Open [(Term, Maybe VerboseLevel)]
    lhsVars' = do

        -- Compute the hintSplitVars from the pattern variables of function at the interaction point.
        lhsVars <- Open [Term] -> TCMT IO [Term]
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen (Open [Term] -> TCMT IO [Term]) -> Open [Term] -> TCMT IO [Term]
    forall a b. (a -> b) -> a -> b
    $ ((Term, Maybe VerboseLevel) -> Term)
    -> [(Term, Maybe VerboseLevel)] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term, Maybe VerboseLevel) -> Term
    forall a b. (a, b) -> a
    fst ([(Term, Maybe VerboseLevel)] -> [Term])
    -> Open [(Term, Maybe VerboseLevel)] -> Open [Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Open [(Term, Maybe VerboseLevel)]
    lhsVars'
        typedLocals <- getLocalVarTerms 0
        reportSDoc "mimer.components" 40 $ "All LHS variables:" <+> prettyTCM lhsVars <+> parens ("or" <+> pretty lhsVars)
        let typedLhsVars = ((Term, Dom Type) -> Bool)
    -> [(Term, Dom Type)] -> [(Term, Dom Type)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\(Term
    term,Dom Type
    typ) -> Term
    term Term -> [Term] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Term]
    lhsVars) [(Term, Dom Type)]
    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
    term, Dom Type
    dom) -> Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom Type
    dom) TCM Bool -> TCM Bool -> TCM Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Type -> TCM Bool
    forall (tcm :: * -> *).
    (MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) =>
    Type -> tcm Bool
    isTypeDatatype (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    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 :: forall tm ty.
    (PrettyTCM tm, PrettyTCM ty) =>
    (tm, ty) -> TCMT IO Doc
    prettyTCMTypedTerm (tm
    term, ty
    typ) = tm -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => tm -> m Doc
    prettyTCM tm
    term TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ty -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ty -> m Doc
    prettyTCM ty
    typ
        prettyTypedTerm :: (a, a) -> m Doc
    prettyTypedTerm (a
    term, a
    typ) = a -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty a
    term m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty a
    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 :: forall (tcm :: * -> *).
    (ReadTCState tcm, MonadError TCErr tcm, MonadTCM tcm,
     HasConstInfo tcm) =>
    InteractionId -> tcm (Open [(Term, Maybe VerboseLevel)])
    collectLHSVars InteractionId
    ii = do
      ipc <- InteractionPoint -> IPClause
    ipClause (InteractionPoint -> IPClause)
    -> tcm InteractionPoint -> tcm IPClause
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InteractionId -> tcm InteractionPoint
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint InteractionId
    ii
      case ipc of
        IPClause
    IPNoClause -> [(Term, Maybe VerboseLevel)]
    -> tcm (Open [(Term, Maybe VerboseLevel)])
    forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    a -> m (Open a)
    makeOpen []
        IPClause{ipcQName :: IPClause -> QName
    ipcQName = QName
    fnName, ipcClauseNo :: IPClause -> VerboseLevel
    ipcClauseNo = VerboseLevel
    clauseNr} -> do
          ArgName -> VerboseLevel -> TCMT IO Doc -> tcm ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.components" VerboseLevel
    40 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Collecting LHS vars for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> InteractionId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => InteractionId -> m Doc
    prettyTCM InteractionId
    ii
          info <- QName -> tcm Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    fnName
          parCount <- liftTCM getCurrentModuleFreeVars
          case theDef info of
            fnDef :: Defn
    fnDef@Function{} -> do
              let clause :: Clause
    clause = Defn -> [Clause]
    funClauses Defn
    fnDef [Clause] -> VerboseLevel -> Clause
    forall a. HasCallStack => [a] -> VerboseLevel -> a
    !! VerboseLevel
    clauseNr
                  naps :: NAPs
    naps = Clause -> NAPs
    namedClausePats Clause
    clause

              -- Telescope at interaction point
              iTel <- tcm Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
              -- Telescope for the body of the clause
              let cTel = Clause -> Telescope
    clauseTel Clause
    clause
              -- HACK: To get the correct indices, we shift by the difference in telescope lengths
              let shift = [Arg ArgName] -> VerboseLevel
    forall a. [a] -> VerboseLevel
    forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
    length (Telescope -> [Arg ArgName]
    forall a. TelToArgs a => a -> [Arg ArgName]
    telToArgs Telescope
    iTel) VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    - [Arg ArgName] -> VerboseLevel
    forall a. [a] -> VerboseLevel
    forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
    length (Telescope -> [Arg ArgName]
    forall a. TelToArgs a => a -> [Arg ArgName]
    telToArgs Telescope
    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
                       ]
            Defn
    _ -> do
              [(Term, Maybe VerboseLevel)]
    -> tcm (Open [(Term, Maybe VerboseLevel)])
    forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    a -> m (Open a)
    makeOpen []
      where
        go :: Bool -> DeBruijnPattern -> [(VerboseLevel, Bool)]
    go Bool
    isUnderCon = \case
          VarP PatternInfo
    patInf DBPatVar
    x -> [(DBPatVar -> VerboseLevel
    dbPatVarIndex DBPatVar
    x, Bool
    isUnderCon)]
          DotP PatternInfo
    patInf Term
    t -> [] -- Ignore dot patterns
          ConP ConHead
    conHead ConPatternInfo
    conPatInf NAPs
    namedArgs -> (NamedArg DeBruijnPattern -> [(VerboseLevel, Bool)])
    -> NAPs -> [(VerboseLevel, Bool)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (Bool -> DeBruijnPattern -> [(VerboseLevel, Bool)]
    go Bool
    True (DeBruijnPattern -> [(VerboseLevel, Bool)])
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> [(VerboseLevel, Bool)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Named NamedName DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
    forall e. Arg e -> e
    unArg) NAPs
    namedArgs
          LitP{} -> []
          ProjP{} -> []
          IApplyP{} -> [] -- Only for Cubical?
          DefP{} -> [] -- Only for Cubical?

    declarationQnames :: A.Declaration -> [QName]
    declarationQnames :: Declaration -> [QName]
    declarationQnames Declaration
    dec = [ QName
    q | Scope.WithKind KindOfName
    _ QName
    q <- Declaration -> [KName]
    forall m. Collection KName m => Declaration -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    A.declaredNames Declaration
    dec ]

    ------------------------------------------------------------------------------
    -- * Measure performance
    ------------------------------------------------------------------------------
    data MimerStats = MimerStats
      { MimerStats -> VerboseLevel
    statCompHit :: Nat -- ^ Could make use of an already generated component
      , MimerStats -> VerboseLevel
    statCompGen :: Nat -- ^ Could use a generator for a component
      , MimerStats -> VerboseLevel
    statCompRegen :: Nat -- ^ Had to regenerate the cache (new context)
      , MimerStats -> VerboseLevel
    statCompNoRegen :: Nat -- ^ Did not have to regenerate the cache
      , MimerStats -> VerboseLevel
    statMetasCreated :: Nat -- ^ Total number of meta-variables created explicitly (not through unification)
      , MimerStats -> VerboseLevel
    statTypeEqChecks :: Nat -- ^ Number of times type equality is tested (with unification)
      , MimerStats -> VerboseLevel
    statRefineSuccess :: Nat -- ^ Number of times a refinement has been successful
      , MimerStats -> VerboseLevel
    statRefineFail :: Nat -- ^ Number of times a refinement has failed
      } deriving (VerboseLevel -> MimerStats -> ArgName -> ArgName
    [MimerStats] -> ArgName -> ArgName
    MimerStats -> ArgName
    (VerboseLevel -> MimerStats -> ArgName -> ArgName)
    -> (MimerStats -> ArgName)
    -> ([MimerStats] -> ArgName -> ArgName)
    -> Show MimerStats
    forall a.
    (VerboseLevel -> a -> ArgName -> ArgName)
    -> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
    $cshowsPrec :: VerboseLevel -> MimerStats -> ArgName -> ArgName
    showsPrec :: VerboseLevel -> MimerStats -> ArgName -> ArgName
    $cshow :: MimerStats -> ArgName
    show :: MimerStats -> ArgName
    $cshowList :: [MimerStats] -> ArgName -> ArgName
    showList :: [MimerStats] -> ArgName -> ArgName
    Show, MimerStats -> MimerStats -> Bool
    (MimerStats -> MimerStats -> Bool)
    -> (MimerStats -> MimerStats -> Bool) -> Eq MimerStats
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: MimerStats -> MimerStats -> Bool
    == :: MimerStats -> MimerStats -> Bool
    $c/= :: MimerStats -> MimerStats -> Bool
    /= :: MimerStats -> MimerStats -> Bool
    Eq, (forall x. MimerStats -> Rep MimerStats x)
    -> (forall x. Rep MimerStats x -> MimerStats) -> Generic MimerStats
    forall x. Rep MimerStats x -> MimerStats
    forall x. MimerStats -> Rep MimerStats x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. MimerStats -> Rep MimerStats x
    from :: forall x. MimerStats -> Rep MimerStats x
    $cto :: forall x. Rep MimerStats x -> MimerStats
    to :: forall x. Rep MimerStats x -> MimerStats
    Generic)
    instance NFData MimerStats

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

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

    updateStat :: (MimerStats -> MimerStats) -> SM ()
    updateStat :: (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
    updateStat MimerStats -> MimerStats
    f = ArgName
    -> VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) ()
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> m () -> m ()
    verboseS ArgName
    "mimer.stats" VerboseLevel
    10 (ReaderT SearchOptions (TCMT IO) ()
     -> ReaderT SearchOptions (TCMT IO) ())
    -> ReaderT SearchOptions (TCMT IO) ()
    -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ do
      ref <- (SearchOptions -> IORef MimerStats)
    -> ReaderT SearchOptions (TCMT IO) (IORef MimerStats)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SearchOptions -> IORef MimerStats
    searchStats
      liftIO $ modifyIORef' ref f

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

    runSearch :: Rewrite -> Options -> InteractionId -> Range -> TCM [MimerResult]
    runSearch :: Rewrite -> Options -> InteractionId -> Range -> TCM [MimerResult]
    runSearch Rewrite
    norm Options
    options InteractionId
    ii Range
    rng = InteractionId -> TCM [MimerResult] -> TCM [MimerResult]
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCM [MimerResult] -> TCM [MimerResult])
    -> TCM [MimerResult] -> TCM [MimerResult]
    forall a b. (a -> b) -> a -> b
    $ do
      (mTheFunctionQName, whereNames) <- (InteractionPoint -> IPClause)
    -> TCMT IO InteractionPoint -> TCMT IO IPClause
    forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap InteractionPoint -> IPClause
    ipClause (InteractionId -> TCMT IO InteractionPoint
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint InteractionId
    ii) TCMT IO IPClause
    -> (IPClause -> (Maybe QName, [QName]))
    -> TCMT IO (Maybe QName, [QName])
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
        clause :: IPClause
    clause@IPClause{} -> ( QName -> Maybe QName
    forall a. a -> Maybe a
    Just (QName -> Maybe QName) -> QName -> Maybe QName
    forall a b. (a -> b) -> a -> b
    $ IPClause -> QName
    ipcQName IPClause
    clause
                             , case WhereDeclarations -> Maybe Declaration
    A.whereDecls (WhereDeclarations -> Maybe Declaration)
    -> WhereDeclarations -> Maybe Declaration
    forall a b. (a -> b) -> a -> b
    $ Clause' SpineLHS -> WhereDeclarations
    forall lhs. Clause' lhs -> WhereDeclarations
    A.clauseWhereDecls (Clause' SpineLHS -> WhereDeclarations)
    -> Clause' SpineLHS -> WhereDeclarations
    forall a b. (a -> b) -> a -> b
    $ IPClause -> Clause' SpineLHS
    ipcClause IPClause
    clause of
                                 Just Declaration
    decl -> Declaration -> [QName]
    declarationQnames Declaration
    decl
                                 Maybe Declaration
    _ -> []
                             )
        IPClause
    IPNoClause -> (Maybe QName
    forall a. Maybe a
    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 Instantiation
    inst -> do

          metaIds <- Term -> TCMT IO [MetaId]
    forall t (tcm :: * -> *).
    (AllMetas t, ReadTCState tcm) =>
    t -> tcm [MetaId]
    allOpenMetas (Instantiation -> Term
    instBody Instantiation
    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 MetaKind
    UnificationMeta -> do
          ArgName -> VerboseLevel -> ArgName -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> ArgName -> m ()
    reportSLn ArgName
    "mimer.init" VerboseLevel
    20 ArgName
    "Interaction point not instantiated."
          [MetaId] -> TCMT IO [MetaId]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [MetaId
    metaId]
        MetaInstantiation
    _ -> TCMT IO [MetaId]
    forall a. HasCallStack => a
    __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 = ((Doc, Doc) -> Doc) -> [(Doc, Doc)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc, Doc) -> Doc
    forall a b. (a, b) -> b
    snd ([(Doc, Doc)] -> [Doc]) -> [(Doc, Doc)] -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ ((Doc, Doc) -> Bool) -> [(Doc, Doc)] -> [(Doc, Doc)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Doc -> Doc -> Bool) -> (Doc, Doc) -> Bool
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Doc -> Doc -> Bool
    forall a. Eq a => a -> a -> Bool
    (/=)) ([(Doc, Doc)] -> [(Doc, Doc)]) -> [(Doc, Doc)] -> [(Doc, Doc)]
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> [Doc] -> [(Doc, Doc)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Doc]
    fnArgs1 [Doc]
    fnArgs2
          bringScopeNoBraces = (Doc -> ArgName) -> [Doc] -> [ArgName]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Char -> Bool) -> ArgName -> ArgName
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Char -> ArgName -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [Char
    '{', Char
    '}']) (ArgName -> ArgName) -> (Doc -> ArgName) -> Doc -> ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> ArgName
    forall a. Doc a -> ArgName
    P.render) [Doc]
    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 MetaVariable -> MetaInstantiation
    mvInstantiation MetaVariable
    metaVar of
            InstV Instantiation
    inst -> do
              expr <- InteractionId -> TCMT IO Expr -> TCMT IO Expr
    forall (m :: * -> *) a.
    (MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    ii (TCMT IO Expr -> TCMT IO Expr) -> TCMT IO Expr -> TCMT IO Expr
    forall a b. (a -> b) -> a -> b
    $ do
                metaArgs <- MetaVariable -> TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
    getMetaContextArgs MetaVariable
    metaVar
                instantiateFull (apply (MetaV metaId []) metaArgs) >>= normalForm norm >>= reify
              str <- P.render <$> prettyTCM expr
              let sol = ArgName -> MimerResult
    MimerExpr ArgName
    str
              reportSDoc "mimer.init" 10 $ "Goal already solved. Solution:" <+> text str
              return [sol]
            MetaInstantiation
    _ -> TCM [MimerResult]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        [MetaId]
    _ -> do
          costs <- TCM Bool -> TCMT IO Costs -> TCMT IO Costs -> TCMT IO Costs
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (ArgName -> VerboseLevel -> TCM Bool
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> m Bool
    hasVerbosity ArgName
    "mimer.cost.custom" VerboseLevel
    10)
                     {- then -} TCMT IO Costs
    customCosts
                     {- else -} (Costs -> TCMT IO Costs
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Costs
    defaultCosts)
          reportSDoc "mimer.cost.custom" 10 $ "Using costs:" $$ nest 2 (pretty costs)
          components <- collectComponents options costs ii mTheFunctionQName whereNames metaId
          let startGoals = (MetaId -> Goal) -> [MetaId] -> [Goal]
    forall a b. (a -> b) -> [a] -> [b]
    map MetaId -> Goal
    Goal [MetaId]
    metaIds

          state <- getTC
          env <- askTC

          let startBranch = SearchBranch
                { sbTCState :: TCState
    sbTCState = TCState
    state
                , sbGoals :: [Goal]
    sbGoals = [Goal]
    startGoals
                , sbCost :: VerboseLevel
    sbCost = VerboseLevel
    0
                , sbCache :: Map CheckpointId ComponentCache
    sbCache = Map CheckpointId ComponentCache
    forall k a. Map k a
    Map.empty
                , sbComponentsUsed :: Map Name VerboseLevel
    sbComponentsUsed = Map Name VerboseLevel
    forall k a. Map k a
    Map.empty
                }

          statsRef <- liftIO $ newIORef emptyMimerStats
          checkpoint <- viewTC eCurrentCheckpoint
          mflat <- getBuiltinName BuiltinFlat
          let searchOptions = SearchOptions
                { searchBaseComponents :: BaseComponents
    searchBaseComponents = BaseComponents
    components
                , searchHintMode :: HintMode
    searchHintMode = Options -> HintMode
    optHintMode Options
    options
                , searchTimeout :: Integer
    searchTimeout = Options -> Integer
    optTimeout Options
    options
                , searchGenProjectionsLocal :: Bool
    searchGenProjectionsLocal = Bool
    True
                , searchGenProjectionsLet :: Bool
    searchGenProjectionsLet = Bool
    True
                , searchGenProjectionsExternal :: Bool
    searchGenProjectionsExternal = Bool
    False
                , searchGenProjectionsRec :: Bool
    searchGenProjectionsRec = Bool
    True
                , searchSpeculateProjections :: Bool
    searchSpeculateProjections = Bool
    True
                , searchTopMeta :: MetaId
    searchTopMeta = MetaId
    metaId
                , searchTopEnv :: TCEnv
    searchTopEnv = TCEnv
    env
                , searchTopCheckpoint :: CheckpointId
    searchTopCheckpoint = CheckpointId
    checkpoint
                , searchInteractionId :: InteractionId
    searchInteractionId = InteractionId
    ii
                , searchFnName :: Maybe QName
    searchFnName = Maybe QName
    mTheFunctionQName
                , searchCosts :: Costs
    searchCosts = Costs
    costs
                , searchStats :: IORef MimerStats
    searchStats = IORef MimerStats
    statsRef
                , searchRewrite :: Rewrite
    searchRewrite = Rewrite
    norm
                , searchBuiltinFlat :: Maybe QName
    searchBuiltinFlat = Maybe QName
    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 VerboseLevel
    0 VerboseLevel
    n MinQueue SearchBranch
    _ = ([MimerResult], VerboseLevel) -> SM ([MimerResult], VerboseLevel)
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([], VerboseLevel
    n)
                go VerboseLevel
    need VerboseLevel
    n MinQueue SearchBranch
    branchQueue = case MinQueue SearchBranch
    -> Maybe (SearchBranch, MinQueue SearchBranch)
    forall a. Ord a => MinQueue a -> Maybe (a, MinQueue a)
    Q.minView MinQueue SearchBranch
    branchQueue of
                  Maybe (SearchBranch, MinQueue SearchBranch)
    Nothing -> do
                    ArgName
    -> VerboseLevel -> ArgName -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> ArgName -> m ()
    reportSLn ArgName
    "mimer.search" VerboseLevel
    30 (ArgName -> ReaderT SearchOptions (TCMT IO) ())
    -> ArgName -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "No remaining search branches."
                    ([MimerResult], VerboseLevel) -> SM ([MimerResult], VerboseLevel)
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], VerboseLevel
    n)
                  Just (SearchBranch
    branch, MinQueue SearchBranch
    branchQueue') -> do
                    time <- IO CPUTime -> ReaderT SearchOptions (TCMT IO) CPUTime
    forall a. IO a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO CPUTime
    forall (m :: * -> *). MonadIO m => m CPUTime
    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 = CPUTime
    time CPUTime -> CPUTime -> CPUTime
    forall a. Num a => a -> a -> a
    - CPUTime
    startTime
                    if elapsed < timeout
                    then do
                      (newBranches, sols) <- refine branch >>= partitionStepResult
                      let branchQueue'' = (SearchBranch -> MinQueue SearchBranch -> MinQueue SearchBranch)
    -> MinQueue SearchBranch -> [SearchBranch] -> MinQueue SearchBranch
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SearchBranch -> MinQueue SearchBranch -> MinQueue SearchBranch
    forall a. Ord a => a -> MinQueue a -> MinQueue a
    Q.insert MinQueue SearchBranch
    branchQueue' [SearchBranch]
    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' = VerboseLevel -> [MimerResult] -> [MimerResult]
    forall a. VerboseLevel -> [a] -> [a]
    take VerboseLevel
    need [MimerResult]
    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 | Options -> Bool
    optList Options
    options = VerboseLevel
    10 VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    + Options -> VerboseLevel
    optSkip Options
    options
                             | Bool
    otherwise       = VerboseLevel
    1 VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    + Options -> VerboseLevel
    optSkip Options
    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
    -> Type
    -> SearchBranch
    -> [(Component, [Component])]
    -> SM [SearchStepResult]
    tryComponents Goal
    goal Type
    goalType SearchBranch
    branch [(Component, [Component])]
    comps = SearchBranch
    -> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch Goal
    goal (SM [SearchStepResult] -> SM [SearchStepResult])
    -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a b. (a -> b) -> a -> b
    $ do
      checkpoint <- Lens' TCEnv CheckpointId
    -> ReaderT SearchOptions (TCMT IO) CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint
      let tryFor (Component
    sourceComp, [Component]
    comps') = do
            -- Clear out components that depend on meta-variables that have been used.
            let newCache :: ComponentCache
    newCache = Component -> Maybe [Component] -> ComponentCache -> ComponentCache
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Component
    sourceComp Maybe [Component]
    forall a. Maybe a
    Nothing (SearchBranch -> Map CheckpointId ComponentCache
    sbCache SearchBranch
    branch Map CheckpointId ComponentCache -> CheckpointId -> ComponentCache
    forall k a. Ord k => Map k a -> k -> a
    Map.! CheckpointId
    checkpoint)
            newBranches <- [Maybe SearchBranch] -> [SearchBranch]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe SearchBranch] -> [SearchBranch])
    -> ReaderT SearchOptions (TCMT IO) [Maybe SearchBranch]
    -> ReaderT SearchOptions (TCMT IO) [SearchBranch]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Component -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
    -> [Component]
    -> ReaderT SearchOptions (TCMT IO) [Maybe SearchBranch]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Goal
    -> Type
    -> SearchBranch
    -> Component
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    tryRefineWith Goal
    goal Type
    goalType SearchBranch
    branch) [Component]
    comps'
            return $ map (\SearchBranch
    br -> SearchBranch
    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
    -> SearchBranch -> SM (SearchBranch, [(Component, [Component])])
    prepareComponents Goal
    goal SearchBranch
    branch = SearchBranch
    -> Goal
    -> SM (SearchBranch, [(Component, [Component])])
    -> SM (SearchBranch, [(Component, [Component])])
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch Goal
    goal (SM (SearchBranch, [(Component, [Component])])
     -> SM (SearchBranch, [(Component, [Component])]))
    -> SM (SearchBranch, [(Component, [Component])])
    -> SM (SearchBranch, [(Component, [Component])])
    forall a b. (a -> b) -> a -> b
    $ do
      ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.components" VerboseLevel
    50 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Preparing components for goal" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM (Goal -> MetaId
    goalMeta Goal
    goal)
      checkpoint <- Lens' TCEnv CheckpointId
    -> ReaderT SearchOptions (TCMT IO) CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    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
        Maybe ComponentCache
    Nothing -> do
          (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
    updateStat MimerStats -> MimerStats
    incCompRegen
          ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.components" VerboseLevel
    20 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "No cache found checkpoint:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> CheckpointId -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty CheckpointId
    checkpoint
            , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "with context:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope) ]
          -- Generate components for this context
          comps <- ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
    genComponents
          reportSDoc "mimer.components" 20 $ "Generated" <+> pretty (sum $ map (length . snd) comps) <+> "components"
          return comps
        -- Yes, just update the missing generated components
        Just ComponentCache
    cache -> ((Component, Maybe [Component])
     -> ReaderT SearchOptions (TCMT IO) (Component, [Component]))
    -> [(Component, Maybe [Component])]
    -> ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Component, Maybe [Component])
    -> ReaderT SearchOptions (TCMT IO) (Component, [Component])
    prepare (ComponentCache -> [(Component, Maybe [Component])]
    forall k a. Map k a -> [(k, a)]
    Map.toAscList ComponentCache
    cache)
      let newCache = [(Component, Maybe [Component])] -> ComponentCache
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(Component, Maybe [Component])] -> ComponentCache)
    -> [(Component, Maybe [Component])] -> ComponentCache
    forall a b. (a -> b) -> a -> b
    $ ((Component, [Component]) -> (Component, Maybe [Component]))
    -> [(Component, [Component])] -> [(Component, Maybe [Component])]
    forall a b. (a -> b) -> [a] -> [b]
    map (([Component] -> Maybe [Component])
    -> (Component, [Component]) -> (Component, Maybe [Component])
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd [Component] -> Maybe [Component]
    forall a. a -> Maybe a
    Just) [(Component, [Component])]
    comps
      branch' <- updateBranch [] branch{sbCache = Map.insert checkpoint newCache (sbCache branch)}
      return (branch', comps)
      where
      prepare :: (Component, Maybe [Component]) -> SM (Component, [Component])
      prepare :: (Component, Maybe [Component])
    -> ReaderT SearchOptions (TCMT IO) (Component, [Component])
    prepare (Component
    sourceComp, Just [Component]
    comps) = do
        (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
    updateStat MimerStats -> MimerStats
    incCompNoRegen
        (Component, [Component])
    -> ReaderT SearchOptions (TCMT IO) (Component, [Component])
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Component
    sourceComp, [Component]
    comps)
      prepare (Component
    sourceComp, Maybe [Component]
    Nothing) = do
        (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
    updateStat MimerStats -> MimerStats
    incCompRegen
        (Component
    sourceComp,) ([Component] -> (Component, [Component]))
    -> ReaderT SearchOptions (TCMT IO) [Component]
    -> ReaderT SearchOptions (TCMT IO) (Component, [Component])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
    genComponentsFrom Bool
    True Component
    sourceComp

    localVarCount :: SM Int
    localVarCount :: SM VerboseLevel
    localVarCount = do
      top <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((SearchOptions -> VerboseLevel) -> SM VerboseLevel)
    -> (SearchOptions -> VerboseLevel) -> SM VerboseLevel
    forall a b. (a -> b) -> a -> b
    $ [ContextEntry] -> VerboseLevel
    forall a. [a] -> VerboseLevel
    forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
    length ([ContextEntry] -> VerboseLevel)
    -> (SearchOptions -> [ContextEntry])
    -> SearchOptions
    -> VerboseLevel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCEnv -> [ContextEntry]
    envContext (TCEnv -> [ContextEntry])
    -> (SearchOptions -> TCEnv) -> SearchOptions -> [ContextEntry]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> TCEnv
    searchTopEnv
      cur <- length <$> getContext
      pure $ cur - top

    genComponents :: SM [(Component, [Component])]
    genComponents :: ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
    genComponents = do
      opts <- ReaderT SearchOptions (TCMT IO) SearchOptions
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      let comps = SearchOptions -> BaseComponents
    searchBaseComponents SearchOptions
    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 :: Bool
    -> [Component]
    -> ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
    genAddSource Bool
    genProj = (Component
     -> ReaderT SearchOptions (TCMT IO) (Component, [Component]))
    -> [Component]
    -> ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\Component
    comp -> (Component
    comp,) ([Component] -> (Component, [Component]))
    -> ReaderT SearchOptions (TCMT IO) [Component]
    -> ReaderT SearchOptions (TCMT IO) (Component, [Component])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
    genComponentsFrom Bool
    genProj Component
    comp)

    genComponentsFrom :: Bool -- ^ Apply record elimination
                      -> Component
                      -> SM [Component]
    genComponentsFrom :: Bool -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
    genComponentsFrom Bool
    appRecElims Component
    origComp = do
      ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.components" VerboseLevel
    50 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Generating components from original component" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> VerboseLevel -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
    prettyTCM (Component -> VerboseLevel
    compId Component
    origComp) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Maybe Name -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Maybe Name -> m Doc
    prettyTCM (Component -> Maybe Name
    compName Component
    origComp)
      comps <- if | Component -> Bool
    compRec Component
    origComp -> (Component -> ReaderT SearchOptions (TCMT IO) Component)
    -> [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Maybe VerboseLevel
    -> Component -> ReaderT SearchOptions (TCMT IO) Component
    applyToMetasG Maybe VerboseLevel
    forall a. Maybe a
    Nothing) ([Component] -> ReaderT SearchOptions (TCMT IO) [Component])
    -> ReaderT SearchOptions (TCMT IO) [Component]
    -> ReaderT SearchOptions (TCMT IO) [Component]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Component -> ReaderT SearchOptions (TCMT IO) [Component]
    genRecCalls Component
    origComp
                  | Bool
    otherwise        -> (Component -> [Component] -> [Component]
    forall a. a -> [a] -> [a]
    :[]) (Component -> [Component])
    -> ReaderT SearchOptions (TCMT IO) Component
    -> ReaderT SearchOptions (TCMT IO) [Component]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe VerboseLevel
    -> Component -> ReaderT SearchOptions (TCMT IO) Component
    applyToMetasG Maybe VerboseLevel
    forall a. Maybe a
    Nothing Component
    origComp
      if appRecElims
      then concat <$> mapM (applyProjections Set.empty) comps
      else return comps
      where
      applyProjections :: Set QName -> Component -> SM [Component]
      applyProjections :: Set QName
    -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
    applyProjections Set QName
    seenRecords Component
    comp = do
        projComps <- Type -> SM (Maybe (QName, Args, [QName], Bool))
    getRecordInfo (Component -> Type
    compType Component
    comp) SM (Maybe (QName, Args, [QName], Bool))
    -> (Maybe (QName, Args, [QName], Bool)
        -> ReaderT SearchOptions (TCMT IO) [Component])
    -> ReaderT SearchOptions (TCMT IO) [Component]
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Maybe (QName, Args, [QName], Bool)
    Nothing -> [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          Just (QName
    recordName, Args
    args, [QName]
    fields, Bool
    isRecursive)
              | QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    recordName Set QName
    seenRecords -> do
                  ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.components" VerboseLevel
    60 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
                    TCMT IO Doc
    "Skipping projection because recursive record already seen:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    recordName
                  [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
              | Bool
    otherwise -> do
                  let seenRecords' :: Set QName
    seenRecords' = if Bool
    isRecursive then QName -> Set QName -> Set QName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert QName
    recordName Set QName
    seenRecords else Set QName
    seenRecords
                  comps <- (QName -> ReaderT SearchOptions (TCMT IO) Component)
    -> [QName] -> ReaderT SearchOptions (TCMT IO) [Component]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Args
    -> Component -> QName -> ReaderT SearchOptions (TCMT IO) Component
    applyProj Args
    args Component
    comp (QName -> ReaderT SearchOptions (TCMT IO) Component)
    -> (Component -> ReaderT SearchOptions (TCMT IO) Component)
    -> QName
    -> ReaderT SearchOptions (TCMT IO) Component
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Maybe VerboseLevel
    -> Component -> ReaderT SearchOptions (TCMT IO) Component
    applyToMetasG Maybe VerboseLevel
    forall a. Maybe a
    Nothing) [QName]
    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 :: Type -> SM (Maybe (QName, Args, [QName], Bool))
    getRecordInfo Type
    typ = case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    typ of
      Def QName
    qname Elims
    elims -> QName -> ReaderT SearchOptions (TCMT IO) (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    qname ReaderT SearchOptions (TCMT IO) (Maybe RecordData)
    -> (Maybe RecordData -> SM (Maybe (QName, Args, [QName], Bool)))
    -> SM (Maybe (QName, Args, [QName], Bool))
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe RecordData
    Nothing -> Maybe (QName, Args, [QName], Bool)
    -> SM (Maybe (QName, Args, [QName], Bool))
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args, [QName], Bool)
    forall a. Maybe a
    Nothing
        Just RecordData
    defn -> do
          fields <- QName -> ReaderT SearchOptions (TCMT IO) [QName]
    forall (tcm :: * -> *).
    (HasConstInfo tcm, MonadTCM tcm) =>
    QName -> tcm [QName]
    getRecordFields QName
    qname
          return $ Just (qname, argsFromElims elims, fields, recRecursive_ defn)
      Term
    _ -> Maybe (QName, Args, [QName], Bool)
    -> SM (Maybe (QName, Args, [QName], Bool))
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args, [QName], Bool)
    forall a. Maybe a
    Nothing

    applyProj :: Args -> Component -> QName -> SM Component
    applyProj :: Args
    -> Component -> QName -> ReaderT SearchOptions (TCMT IO) Component
    applyProj Args
    recordArgs Component
    comp' QName
    qname = do
      cost <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (Costs -> VerboseLevel
    costProj (Costs -> VerboseLevel)
    -> (SearchOptions -> Costs) -> SearchOptions -> VerboseLevel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> Costs
    searchCosts)
      -- Andreas, 2025-03-31, issue #7662: hack to prevent postfix printing of ♭
      projOrigin <- maybe ProjSystem (\ QName
    flat -> if QName
    qname QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    flat then ProjOrigin
    ProjPrefix else ProjOrigin
    ProjSystem)
        <$> asks searchBuiltinFlat
      let newTerm = Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE (Component -> Term
    compTerm Component
    comp') [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    projOrigin QName
    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 :: Maybe VerboseLevel
    -> Component -> ReaderT SearchOptions (TCMT IO) Component
    applyToMetasG (Just VerboseLevel
    m) Component
    comp | VerboseLevel
    m VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    <= VerboseLevel
    0 = Component -> ReaderT SearchOptions (TCMT IO) Component
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Component
    comp
    applyToMetasG Maybe VerboseLevel
    maxArgs Component
    comp = do
      ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.component" VerboseLevel
    25 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Applying component to metas" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> VerboseLevel -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
    prettyTCM (Component -> VerboseLevel
    compId Component
    comp) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Component -> Term
    compTerm Component
    comp)
      ctx <- ReaderT SearchOptions (TCMT IO) Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
      compTyp <- reduce $ compType comp
      case unEl compTyp of
        Pi Dom Type
    dom Abs Type
    abs -> do
          let domainType :: Type
    domainType = Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    dom
          (metaId, metaTerm) <- Type -> SM (MetaId, Term)
    createMeta Type
    domainType
          reportSDoc "mimer.component" 30 $ "New arg meta" <+> prettyTCM metaTerm
          let arg = Origin -> Arg Term -> Arg Term
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted (Arg Term -> Arg Term) -> Arg Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Term
    metaTerm Term -> Arg Type -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    dom
          newType <- reduce =<< piApplyM (compType comp) metaTerm
          -- Constructor parameters are not included in the term
          let skip = Component -> VerboseLevel
    compPars Component
    comp
              newTerm | VerboseLevel
    skip VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    > VerboseLevel
    0  = Component -> Term
    compTerm Component
    comp
                      | Bool
    otherwise = Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    apply (Component -> Term
    compTerm Component
    comp) [Arg Term
    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
                            }
        Term
    _ ->
          -- Set the type to the reduced version
          Component -> ReaderT SearchOptions (TCMT IO) Component
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Component
    comp{compType = compTyp}

    createMeta :: Type -> SM (MetaId, Term)
    createMeta :: Type -> SM (MetaId, Term)
    createMeta Type
    typ = do
      (metaId, metaTerm) <- RunMetaOccursCheck -> Comparison -> Type -> SM (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta RunMetaOccursCheck
    DontRunMetaOccursCheck Comparison
    CmpLeq Type
    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 :: [SearchStepResult]
    -> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
    partitionStepResult [] = ([SearchBranch], [MimerResult])
    -> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([],[])
    partitionStepResult (SearchStepResult
    x:[SearchStepResult]
    xs) = do
      let rest :: ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
    rest = [SearchStepResult]
    -> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
    partitionStepResult [SearchStepResult]
    xs
      (brs',sols) <- ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
    rest
      case x of
        SearchStepResult
    NoSolution -> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
    rest
        OpenBranch SearchBranch
    br -> ([SearchBranch], [MimerResult])
    -> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SearchBranch
    brSearchBranch -> [SearchBranch] -> [SearchBranch]
    forall a. a -> [a] -> [a]
    :[SearchBranch]
    brs', [MimerResult]
    sols)
        ResultExpr Expr
    exp -> do
          str <- Doc -> ArgName
    forall a. Doc a -> ArgName
    P.render (Doc -> ArgName)
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ArgName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Expr -> m Doc
    prettyTCM Expr
    exp
          return $ (brs', MimerExpr str : sols)
        ResultClauses [Clause]
    cls -> do
          f <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName)
    -> ReaderT SearchOptions (TCMT IO) (Maybe QName)
    -> ReaderT SearchOptions (TCMT IO) QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (SearchOptions -> Maybe QName)
    -> ReaderT SearchOptions (TCMT IO) (Maybe QName)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SearchOptions -> Maybe QName
    searchFnName
          return $ (brs', MimerClauses f cls : sols)

    topInstantiationDoc :: SM Doc
    topInstantiationDoc :: ReaderT SearchOptions (TCMT IO) Doc
    topInstantiationDoc = (SearchOptions -> MetaId) -> ReaderT SearchOptions (TCMT IO) MetaId
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SearchOptions -> MetaId
    searchTopMeta ReaderT SearchOptions (TCMT IO) MetaId
    -> (MetaId -> ReaderT SearchOptions (TCMT IO) (Maybe Expr))
    -> ReaderT SearchOptions (TCMT IO) (Maybe Expr)
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= MetaId -> ReaderT SearchOptions (TCMT IO) (Maybe Expr)
    forall (tcm :: * -> *).
    (MonadTCM tcm, PureTCM tcm, MonadDebug tcm,
     MonadInteractionPoints tcm, MonadFresh NameId tcm) =>
    MetaId -> tcm (Maybe Expr)
    getMetaInstantiation ReaderT SearchOptions (TCMT IO) (Maybe Expr)
    -> (Maybe Expr -> ReaderT SearchOptions (TCMT IO) Doc)
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= ReaderT SearchOptions (TCMT IO) Doc
    -> (Expr -> ReaderT SearchOptions (TCMT IO) Doc)
    -> Maybe Expr
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Doc -> ReaderT SearchOptions (TCMT IO) Doc
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Doc
    "(nothing)") Expr -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Expr -> m Doc
    prettyTCM

    prettyGoalInst :: Goal -> SM Doc
    prettyGoalInst :: Goal -> ReaderT SearchOptions (TCMT IO) Doc
    prettyGoalInst Goal
    goal = Goal
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall a. Goal -> SM a -> SM a
    inGoalEnv Goal
    goal (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) Doc)
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ do
      args <- (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Elims)
    -> ReaderT SearchOptions (TCMT IO) Args
    -> ReaderT SearchOptions (TCMT IO) Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT SearchOptions (TCMT IO) Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      prettyTCM =<< instantiate (MetaV (goalMeta goal) args)

    branchInstantiationDocCost :: SearchBranch -> SM Doc
    branchInstantiationDocCost :: SearchBranch -> ReaderT SearchOptions (TCMT IO) Doc
    branchInstantiationDocCost SearchBranch
    branch = SearchBranch -> ReaderT SearchOptions (TCMT IO) Doc
    branchInstantiationDoc SearchBranch
    branch ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (ReaderT SearchOptions (TCMT IO) Doc
    "cost:" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> VerboseLevel -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (SearchBranch -> VerboseLevel
    sbCost SearchBranch
    branch))

    -- | For debug
    branchInstantiationDoc :: SearchBranch -> SM Doc
    branchInstantiationDoc :: SearchBranch -> ReaderT SearchOptions (TCMT IO) Doc
    branchInstantiationDoc SearchBranch
    branch = SearchBranch
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall a. SearchBranch -> SM a -> SM a
    withBranchState SearchBranch
    branch ReaderT SearchOptions (TCMT IO) Doc
    topInstantiationDoc

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

      SearchBranch
    -> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch1 Goal
    goal1 (SM [SearchStepResult] -> SM [SearchStepResult])
    -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a b. (a -> b) -> a -> b
    $ do
        goalType1 <- [Phase]
    -> ReaderT SearchOptions (TCMT IO) Type
    -> ReaderT SearchOptions (TCMT IO) Type
    forall a. NFData a => [Phase] -> SM a -> SM a
    bench [Phase
    Bench.Reduce] (ReaderT SearchOptions (TCMT IO) Type
     -> ReaderT SearchOptions (TCMT IO) Type)
    -> ReaderT SearchOptions (TCMT IO) Type
    -> ReaderT SearchOptions (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ Type -> ReaderT SearchOptions (TCMT IO) Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> ReaderT SearchOptions (TCMT IO) Type)
    -> ReaderT SearchOptions (TCMT IO) Type
    -> ReaderT SearchOptions (TCMT IO) Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< MetaId -> ReaderT SearchOptions (TCMT IO) Type
    forall (m :: * -> *).
    (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
     MonadTCEnv m, ReadTCState m) =>
    MetaId -> m Type
    getMetaTypeInContext (Goal -> MetaId
    goalMeta Goal
    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 SearchBranch
    branch2 -> do
            VerboseLevel
    -> VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    mimerTrace VerboseLevel
    1 VerboseLevel
    10 (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) ())
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [ReaderT SearchOptions (TCMT IO) Doc]
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                  [ ReaderT SearchOptions (TCMT IO) Doc
    "Absurd bambda refinement", VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) Doc)
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ Goal -> ReaderT SearchOptions (TCMT IO) Doc
    prettyGoalInst Goal
    goal1 ]
            args <- (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Elims)
    -> ReaderT SearchOptions (TCMT IO) Args
    -> ReaderT SearchOptions (TCMT IO) Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT SearchOptions (TCMT IO) Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
            e <- blankNotInScope =<< reify (MetaV (goalMeta goal1) args)
            return [ResultExpr e]
          -- Normal abstraction
          Right (Goal
    goal2, Type
    goalType2, SearchBranch
    branch2) -> SearchBranch
    -> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch2 Goal
    goal2 (SM [SearchStepResult] -> SM [SearchStepResult])
    -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a b. (a -> b) -> a -> b
    $ do
            (branch3, components) <- Goal
    -> SearchBranch -> SM (SearchBranch, [(Component, [Component])])
    prepareComponents Goal
    goal2 SearchBranch
    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 -> Type -> SearchBranch -> SM [SearchStepResult]
    tryFns Goal
    goal Type
    goalType SearchBranch
    branch = SearchBranch
    -> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch Goal
    goal (SM [SearchStepResult] -> SM [SearchStepResult])
    -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a b. (a -> b) -> a -> b
    $ do
      ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.refine.fn" VerboseLevel
    50 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Trying functions"
      fns <- (SearchOptions -> [Component])
    -> ReaderT SearchOptions (TCMT IO) [Component]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (BaseComponents -> [Component]
    hintFns (BaseComponents -> [Component])
    -> (SearchOptions -> BaseComponents)
    -> SearchOptions
    -> [Component]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> BaseComponents
    searchBaseComponents)
      newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) fns
      mapM checkSolved newBranches

    tryProjs :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
    tryProjs :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
    tryProjs Goal
    goal Type
    goalType SearchBranch
    branch = SearchBranch
    -> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch Goal
    goal (SM [SearchStepResult] -> SM [SearchStepResult])
    -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a b. (a -> b) -> a -> b
    $ do
      projs <- (SearchOptions -> [Component])
    -> ReaderT SearchOptions (TCMT IO) [Component]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (BaseComponents -> [Component]
    hintProjections (BaseComponents -> [Component])
    -> (SearchOptions -> BaseComponents)
    -> SearchOptions
    -> [Component]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> BaseComponents
    searchBaseComponents)
      newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) projs
      mapM checkSolved newBranches

    tryAxioms :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
    tryAxioms :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
    tryAxioms Goal
    goal Type
    goalType SearchBranch
    branch = SearchBranch
    -> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch Goal
    goal (SM [SearchStepResult] -> SM [SearchStepResult])
    -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a b. (a -> b) -> a -> b
    $ do
      axioms <- (SearchOptions -> [Component])
    -> ReaderT SearchOptions (TCMT IO) [Component]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (BaseComponents -> [Component]
    hintAxioms (BaseComponents -> [Component])
    -> (SearchOptions -> BaseComponents)
    -> SearchOptions
    -> [Component]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> BaseComponents
    searchBaseComponents)
      newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) axioms
      mapM checkSolved newBranches

    tryLet :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
    tryLet :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
    tryLet Goal
    goal Type
    goalType SearchBranch
    branch = SearchBranch
    -> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch Goal
    goal (SM [SearchStepResult] -> SM [SearchStepResult])
    -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a b. (a -> b) -> a -> b
    $ do
      letVars <- (SearchOptions -> [Open Component])
    -> ReaderT SearchOptions (TCMT IO) [Open Component]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (BaseComponents -> [Open Component]
    hintLetVars (BaseComponents -> [Open Component])
    -> (SearchOptions -> BaseComponents)
    -> SearchOptions
    -> [Open Component]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> BaseComponents
    searchBaseComponents) ReaderT SearchOptions (TCMT IO) [Open Component]
    -> ([Open Component]
        -> ReaderT SearchOptions (TCMT IO) [Component])
    -> ReaderT SearchOptions (TCMT IO) [Component]
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (Open Component -> ReaderT SearchOptions (TCMT IO) Component)
    -> [Open Component] -> ReaderT SearchOptions (TCMT IO) [Component]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Open Component -> ReaderT SearchOptions (TCMT IO) Component
    forall (tcm :: * -> *).
    (MonadTCM tcm, MonadDebug tcm) =>
    Open Component -> tcm Component
    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
    -> Type
    -> SearchBranch
    -> SM (Either SearchBranch (Goal, Type, SearchBranch))
    tryLamAbs Goal
    goal Type
    goalType SearchBranch
    branch =
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    goalType of
        Pi Dom Type
    dom Abs Type
    abs -> Type -> ReaderT SearchOptions (TCMT IO) Bool
    forall (tcm :: * -> *). MonadTCM tcm => Type -> tcm Bool
    isEmptyType (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    dom) ReaderT SearchOptions (TCMT IO) Bool
    -> (Bool -> SM (Either SearchBranch (Goal, Type, SearchBranch)))
    -> SM (Either SearchBranch (Goal, Type, SearchBranch))
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Bool
    True -> do
            f <- TCM QName -> ReaderT SearchOptions (TCMT IO) QName
    forall a. TCM a -> ReaderT SearchOptions (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM QName -> ReaderT SearchOptions (TCMT IO) QName)
    -> TCM QName -> ReaderT SearchOptions (TCMT IO) QName
    forall a b. (a -> b) -> a -> b
    $ Range -> Dom Type -> Abs Type -> TCM QName
    makeAbsurdLambda Range
    forall a. Range' a
    noRange Dom Type
    dom Abs Type
    abs
            args <- map Apply <$> getContextArgs
            newMetaIds <- assignMeta (goalMeta goal) (Def f args) goalType
            Left <$> updateBranch newMetaIds branch
          Bool
    False -> do
            ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.lam" VerboseLevel
    40 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Trying lambda abstraction for pi type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    goalType
            let abs' :: Abs Type
    abs' | ArgName -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    abs) = Abs Type
    abs { absName = "z" }
                     | Bool
    otherwise = Abs Type
    abs
            (metaId', bodyType, metaTerm, env) <- Dom Type
    -> Abs Type
    -> (Type
        -> ReaderT SearchOptions (TCMT IO) (MetaId, Type, Term, TCEnv))
    -> ReaderT SearchOptions (TCMT IO) (MetaId, Type, Term, TCEnv)
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs Dom Type
    dom Abs Type
    abs' ((Type
      -> ReaderT SearchOptions (TCMT IO) (MetaId, Type, Term, TCEnv))
     -> ReaderT SearchOptions (TCMT IO) (MetaId, Type, Term, TCEnv))
    -> (Type
        -> ReaderT SearchOptions (TCMT IO) (MetaId, Type, Term, TCEnv))
    -> ReaderT SearchOptions (TCMT IO) (MetaId, Type, Term, TCEnv)
    forall a b. (a -> b) -> a -> b
    $ \Type
    bodyType -> do
              ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.lam" VerboseLevel
    40 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "  bodyType = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    bodyType
              bodyType <- [Phase]
    -> ReaderT SearchOptions (TCMT IO) Type
    -> ReaderT SearchOptions (TCMT IO) Type
    forall a. NFData a => [Phase] -> SM a -> SM a
    bench [Phase
    Bench.Reduce] (ReaderT SearchOptions (TCMT IO) Type
     -> ReaderT SearchOptions (TCMT IO) Type)
    -> ReaderT SearchOptions (TCMT IO) Type
    -> ReaderT SearchOptions (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ Type -> ReaderT SearchOptions (TCMT IO) Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    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 = Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    dom -- TODO: is this the correct arg info?
                newAbs = ArgName -> Term -> Abs Term
    forall a. ArgName -> a -> Abs a
    Abs (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    abs') Term
    metaTerm
                -- look at mkLam
                term = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    argInf Abs Term
    newAbs

            newMetaIds <- assignMeta (goalMeta goal) term goalType

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

    genRecCalls :: Component -> SM [Component]
    genRecCalls :: Component -> ReaderT SearchOptions (TCMT IO) [Component]
    genRecCalls Component
    thisFn = do
      ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.components.open" VerboseLevel
    40 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Generating recursive calls for component" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> VerboseLevel -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
    prettyTCM (Component -> VerboseLevel
    compId Component
    thisFn) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Maybe Name -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Maybe Name -> m Doc
    prettyTCM (Component -> Maybe Name
    compName Component
    thisFn)
      ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.components.open" VerboseLevel
    60 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "  checkpoint =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (CheckpointId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => CheckpointId -> m Doc
    prettyTCM (CheckpointId -> TCMT IO Doc)
    -> TCMT IO CheckpointId -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint)
      -- TODO: Make sure there are no pruning problems
      (SearchOptions -> Open [(Term, NoSubst Term VerboseLevel)])
    -> ReaderT
         SearchOptions (TCMT IO) (Open [(Term, NoSubst Term VerboseLevel)])
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)]
    hintRecVars (BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)])
    -> (SearchOptions -> BaseComponents)
    -> SearchOptions
    -> Open [(Term, NoSubst Term VerboseLevel)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> BaseComponents
    searchBaseComponents) ReaderT
      SearchOptions (TCMT IO) (Open [(Term, NoSubst Term VerboseLevel)])
    -> (Open [(Term, NoSubst Term VerboseLevel)]
        -> ReaderT
             SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)])
    -> ReaderT
         SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)]
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Open [(Term, NoSubst Term VerboseLevel)]
    -> ReaderT
         SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)]
    forall a (m :: * -> *).
    (TermSubst a, MonadTCEnv m) =>
    Open a -> m a
    getOpen ReaderT SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)]
    -> ([(Term, NoSubst Term VerboseLevel)]
        -> ReaderT SearchOptions (TCMT IO) [Component])
    -> ReaderT SearchOptions (TCMT IO) [Component]
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        -- No candidate arguments for a recursive call
        [] -> [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        [(Term, NoSubst Term VerboseLevel)]
    recCandTerms -> do
          Costs{..} <- (SearchOptions -> Costs) -> ReaderT SearchOptions (TCMT IO) Costs
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SearchOptions -> Costs
    searchCosts
          n <- localVarCount
          localVars <- lift $ getLocalVars n costLocal
          let recCands = [ (Component
    t, VerboseLevel
    i) | t :: Component
    t@(Component -> Term
    compTerm -> v :: Term
    v@Var{}) <- [Component]
    localVars, NoSubst VerboseLevel
    i <- Maybe (NoSubst Term VerboseLevel) -> [NoSubst Term VerboseLevel]
    forall a. Maybe a -> [a]
    maybeToList (Maybe (NoSubst Term VerboseLevel) -> [NoSubst Term VerboseLevel])
    -> Maybe (NoSubst Term VerboseLevel) -> [NoSubst Term VerboseLevel]
    forall a b. (a -> b) -> a -> b
    $ Term
    -> [(Term, NoSubst Term VerboseLevel)]
    -> Maybe (NoSubst Term VerboseLevel)
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup Term
    v [(Term, NoSubst Term VerboseLevel)]
    recCandTerms ]

          let newRecCall = do
                -- Apply the recursive call to new metas
                (thisFnTerm, thisFnType, newMetas) <- VerboseLevel -> Term -> Type -> SM (Term, Type, [MetaId])
    applyToMetas VerboseLevel
    0 (Component -> Term
    compTerm Component
    thisFn) (Component -> Type
    compType Component
    thisFn)
                let argGoals = (MetaId -> Goal) -> [MetaId] -> [Goal]
    forall a b. (a -> b) -> [a] -> [b]
    map MetaId -> Goal
    Goal [MetaId]
    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 Component
    _thisFn [] [(Component, VerboseLevel)]
    _args = [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
              go Component
    thisFn ((Goal, VerboseLevel)
    _ : [(Goal, VerboseLevel)]
    goals) [] = Component
    -> [(Goal, VerboseLevel)]
    -> [(Component, VerboseLevel)]
    -> ReaderT SearchOptions (TCMT IO) [Component]
    go Component
    thisFn [(Goal, VerboseLevel)]
    goals [(Component, VerboseLevel)]
    recCands
              go Component
    thisFn ((Goal
    goal, VerboseLevel
    i) : [(Goal, VerboseLevel)]
    goals) ((Component
    arg, VerboseLevel
    j) : [(Component, VerboseLevel)]
    args) | VerboseLevel
    i VerboseLevel -> VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == VerboseLevel
    j = do
                ArgName
    -> VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    reportSMDoc ArgName
    "mimer.components.rec" VerboseLevel
    80 (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) ())
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [ReaderT SearchOptions (TCMT IO) Doc]
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep
                  [ ReaderT SearchOptions (TCMT IO) Doc
    "Trying to generate recursive call"
                  , Term -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Component -> Term
    compTerm Component
    thisFn)
                  , ReaderT SearchOptions (TCMT IO) Doc
    "with" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Component -> Term
    compTerm Component
    arg)
                  , ReaderT SearchOptions (TCMT IO) Doc
    "for" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM (Goal -> MetaId
    goalMeta Goal
    goal) ]
                goalType <- MetaId -> ReaderT SearchOptions (TCMT IO) Type
    forall (m :: * -> *).
    (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
     MonadTCEnv m, ReadTCState m) =>
    MetaId -> m Type
    getMetaTypeInContext (Goal -> MetaId
    goalMeta Goal
    goal)
                state <- getTC
                tryRefineWith' goal goalType arg >>= \case
                  Maybe ([MetaId], [MetaId])
    Nothing -> do
                    TCState -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    state
                    Component
    -> [(Goal, VerboseLevel)]
    -> [(Component, VerboseLevel)]
    -> ReaderT SearchOptions (TCMT IO) [Component]
    go Component
    thisFn ((Goal
    goal, VerboseLevel
    i) (Goal, VerboseLevel)
    -> [(Goal, VerboseLevel)] -> [(Goal, VerboseLevel)]
    forall a. a -> [a] -> [a]
    : [(Goal, VerboseLevel)]
    goals) [(Component, VerboseLevel)]
    args
                  Just ([MetaId]
    newMetas1, [MetaId]
    newMetas2) -> do
                    let newComp :: Component
    newComp = Component
    thisFn{compMetas = newMetas1 ++ newMetas2 ++ (compMetas thisFn \\ [goalMeta goal])}
                    (thisFn', goals') <- ReaderT SearchOptions (TCMT IO) (Component, [(Goal, VerboseLevel)])
    newRecCall
                    (newComp:) <$> go thisFn' (drop (length goals' - length goals - 1) goals') args
              go Component
    thisFn [(Goal, VerboseLevel)]
    goals ((Component, VerboseLevel)
    _ : [(Component, VerboseLevel)]
    args) = Component
    -> [(Goal, VerboseLevel)]
    -> [(Component, VerboseLevel)]
    -> ReaderT SearchOptions (TCMT IO) [Component]
    go Component
    thisFn [(Goal, VerboseLevel)]
    goals [(Component, VerboseLevel)]
    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 Component
    comp = (VerboseLevel
    costLocal VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    +) (VerboseLevel -> VerboseLevel)
    -> ([VerboseLevel] -> VerboseLevel)
    -> [VerboseLevel]
    -> VerboseLevel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [VerboseLevel] -> VerboseLevel
    forall a. Num a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([VerboseLevel] -> VerboseLevel)
    -> ReaderT SearchOptions (TCMT IO) [VerboseLevel]
    -> SM VerboseLevel
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> ReaderT SearchOptions (TCMT IO) [VerboseLevel]
    argCosts (Component -> Term
    compTerm Component
    comp)
              argCosts (Def QName
    _ Elims
    elims) = (Elim' Term -> SM VerboseLevel)
    -> Elims -> ReaderT SearchOptions (TCMT IO) [VerboseLevel]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim' Term -> SM VerboseLevel
    argCost Elims
    elims
              argCosts Term
    _ = ReaderT SearchOptions (TCMT IO) [VerboseLevel]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              argCost (Apply Arg Term
    arg) = Arg Term -> ReaderT SearchOptions (TCMT IO) (Arg Term)
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Arg Term
    arg ReaderT SearchOptions (TCMT IO) (Arg Term)
    -> (Arg Term -> VerboseLevel) -> SM VerboseLevel
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ case
                Arg ArgInfo
    h MetaV{} | ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    visible ArgInfo
    h -> VerboseLevel
    costNewMeta
                              | Bool
    otherwise -> VerboseLevel
    costNewHiddenMeta
                Arg Term
    _ -> VerboseLevel
    0
              argCost Proj{}   = VerboseLevel -> SM VerboseLevel
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure VerboseLevel
    0
              argCost IApply{} = VerboseLevel -> SM VerboseLevel
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure VerboseLevel
    0
          mapM (\ Component
    c -> (VerboseLevel -> Component -> Component
    `addCost` Component
    c) (VerboseLevel -> Component)
    -> SM VerboseLevel -> ReaderT SearchOptions (TCMT IO) Component
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Component -> SM VerboseLevel
    callCost Component
    c) comps

    -- TODO: Factor out `checkSolved`
    tryDataRecord :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
    tryDataRecord :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
    tryDataRecord Goal
    goal Type
    goalType SearchBranch
    branch = SearchBranch
    -> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch Goal
    goal (SM [SearchStepResult] -> SM [SearchStepResult])
    -> SM [SearchStepResult] -> SM [SearchStepResult]
    forall a b. (a -> b) -> a -> b
    $ do
      -- TODO: There is a `isRecord` function, which performs a similar case
      -- analysis as here, but it does not work for data types.
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    goalType of
        Def QName
    qname Elims
    elims -> Definition -> Defn
    theDef (Definition -> Defn)
    -> ReaderT SearchOptions (TCMT IO) Definition
    -> ReaderT SearchOptions (TCMT IO) Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> ReaderT SearchOptions (TCMT IO) Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    qname ReaderT SearchOptions (TCMT IO) Defn
    -> (Defn -> SM [SearchStepResult]) -> SM [SearchStepResult]
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          recordDefn :: Defn
    recordDefn@Record{} -> do
            Defn -> SM [SearchStepResult]
    tryRecord Defn
    recordDefn
          dataDefn :: Defn
    dataDefn@Datatype{} -> do
            Defn -> SM [SearchStepResult]
    tryData Defn
    dataDefn
          primitive :: Defn
    primitive@Primitive{} -> do
            [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          -- TODO: Better way of checking that type is Level
          Axiom{}
            | QName -> ArgName
    forall a. Pretty a => a -> ArgName
    P.prettyShow QName
    qname ArgName -> ArgName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgName
    "Agda.Primitive.Level" -> do
                tryLevel
            | Bool
    otherwise -> do
            [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          DataOrRecSig{} -> do
            [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          GeneralizableVar{} -> do
            [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          AbstractDefn{} -> do
            [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          Function{} -> do
            [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          Constructor{} -> do
            [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          PrimitiveSort{} -> do
            [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        Sort (Type Level
    level) -> do
          Level -> SM [SearchStepResult]
    trySet Level
    level
        Sort Sort' Term
    sort -> do
          [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        Term
    _ -> [SearchStepResult] -> SM [SearchStepResult]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    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 :: Defn -> SM [SearchStepResult]
    tryRecord Defn
    recordDefn = do
          cost <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (Costs -> VerboseLevel
    costRecordCon (Costs -> VerboseLevel)
    -> (SearchOptions -> Costs) -> SearchOptions -> VerboseLevel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> Costs
    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 :: Defn -> SM [SearchStepResult]
    tryData Defn
    dataDefn = do
          let constructors :: [QName]
    constructors = Defn -> [QName]
    dataCons Defn
    dataDefn
          ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.try" VerboseLevel
    40 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "tryData" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM [QName]
    constructors
          cost <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (Costs -> VerboseLevel
    costDataCon (Costs -> VerboseLevel)
    -> (SearchOptions -> Costs) -> SearchOptions -> VerboseLevel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> Costs
    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 :: SM [SearchStepResult]
    tryLevel = do
          levelHints <- (SearchOptions -> [Component])
    -> ReaderT SearchOptions (TCMT IO) [Component]
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (BaseComponents -> [Component]
    hintLevel (BaseComponents -> [Component])
    -> (SearchOptions -> BaseComponents)
    -> SearchOptions
    -> [Component]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> BaseComponents
    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 -> SM [SearchStepResult]
    trySet Level
    level = do
          reducedLevel <- Level -> ReaderT SearchOptions (TCMT IO) Level
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Level
    level
          cost <- asks (costSet . searchCosts)
          setCandidates <- case reducedLevel of
            (Max Integer
    i [])
              | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 -> do
                  comp <- [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> ReaderT SearchOptions (TCMT IO) Component
    forall (m :: * -> *).
    MonadFresh VerboseLevel m =>
    [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> m Component
    newComponent [] VerboseLevel
    cost Maybe Name
    forall a. Maybe a
    Nothing VerboseLevel
    0 (Sort' Term -> Term
    Sort (Sort' Term -> Term) -> Sort' Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Level -> Sort' Term
    forall t. Level' t -> Sort' t
    Type (Level -> Sort' Term) -> Level -> Sort' Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) []) Type
    goalType
                  return [(branch, comp)]
              | Bool
    otherwise -> [(SearchBranch, Component)]
    -> ReaderT SearchOptions (TCMT IO) [(SearchBranch, Component)]
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
            (Max Integer
    i [PlusLevel' Term]
    ps) -> do
                  (metaId, metaTerm) <- Type -> SM (MetaId, Term)
    createMeta (Type -> SM (MetaId, Term))
    -> ReaderT SearchOptions (TCMT IO) Type -> SM (MetaId, Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT SearchOptions (TCMT IO) Type
    forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
    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 (\(SearchBranch
    br,Component
    c) -> Goal
    -> Type
    -> SearchBranch
    -> Component
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    tryRefineWith Goal
    goal Type
    goalType SearchBranch
    br Component
    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
    -> Type
    -> SearchBranch
    -> Component
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    tryRefineWith Goal
    goal Type
    goalType SearchBranch
    branch Component
    comp = SearchBranch
    -> Goal
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch Goal
    goal (ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
     -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    forall a b. (a -> b) -> a -> b
    $ do

      ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr, LocalMetaStores)
    forall (m :: * -> *) a.
    ReadTCState m =>
    m a -> m (a, LocalMetaStores)
    metasCreatedBy (Type -> Type -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    dumbUnifierErr (Component -> Type
    compType Component
    comp) Type
    goalType) ReaderT SearchOptions (TCMT IO) (Maybe TCErr, LocalMetaStores)
    -> ((Maybe TCErr, LocalMetaStores)
        -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        (Maybe TCErr
    Nothing, LocalMetaStores
    newMetaStore) -> do
          (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
    updateStat MimerStats -> MimerStats
    incRefineSuccess
          -- TODO: Why is newMetaIds not used here?
          newMetaIds <- MetaId -> Term -> Type -> SM [MetaId]
    assignMeta (Goal -> MetaId
    goalMeta Goal
    goal) (Component -> Term
    compTerm Component
    comp) Type
    goalType
          let newMetaIds' = Map MetaId MetaVariable -> [MetaId]
    forall k a. Map k a -> [k]
    Map.keys (LocalMetaStores -> Map MetaId MetaVariable
    openMetas LocalMetaStores
    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 TCErr
    err, LocalMetaStores
    _) -> do
          (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
    updateStat MimerStats -> MimerStats
    incRefineFail
          ArgName
    -> VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    reportSMDoc ArgName
    "mimer.refine" VerboseLevel
    50 (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) ())
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ ReaderT SearchOptions (TCMT IO) Doc
    "Refinement failed"

          VerboseLevel
    -> VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    mimerTrace VerboseLevel
    2 VerboseLevel
    60 (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) ())
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [ReaderT SearchOptions (TCMT IO) Doc]
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ ReaderT SearchOptions (TCMT IO) Doc
    "Failed refinement"
            , VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) Doc)
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ [ReaderT SearchOptions (TCMT IO) Doc]
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Component -> Term
    compTerm Component
    comp)
                           , ReaderT SearchOptions (TCMT IO) Doc
    ":" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM (Component -> Type
    compType Component
    comp) ]
            , VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) Doc)
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ TCErr -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
    prettyTCM TCErr
    err ]
          Maybe SearchBranch
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe SearchBranch
    forall a. Maybe a
    Nothing

    tryRefineWith' :: Goal -> Type -> Component -> SM (Maybe ([MetaId], [MetaId]))
    tryRefineWith' :: Goal -> Type -> Component -> SM (Maybe ([MetaId], [MetaId]))
    tryRefineWith' Goal
    goal Type
    goalType Component
    comp = do
      ReaderT SearchOptions (TCMT IO) Bool
    -> ReaderT SearchOptions (TCMT IO) (Bool, LocalMetaStores)
    forall (m :: * -> *) a.
    ReadTCState m =>
    m a -> m (a, LocalMetaStores)
    metasCreatedBy (Type -> Type -> ReaderT SearchOptions (TCMT IO) Bool
    dumbUnifier (Component -> Type
    compType Component
    comp) Type
    goalType) ReaderT SearchOptions (TCMT IO) (Bool, LocalMetaStores)
    -> ((Bool, LocalMetaStores) -> SM (Maybe ([MetaId], [MetaId])))
    -> SM (Maybe ([MetaId], [MetaId]))
    forall a b.
    ReaderT SearchOptions (TCMT IO) a
    -> (a -> ReaderT SearchOptions (TCMT IO) b)
    -> ReaderT SearchOptions (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        (Bool
    True, LocalMetaStores
    newMetaStore) -> do
          newMetaIds <- MetaId -> Term -> Type -> SM [MetaId]
    assignMeta (Goal -> MetaId
    goalMeta Goal
    goal) (Component -> Term
    compTerm Component
    comp) Type
    goalType
          let newMetaIds' = Map MetaId MetaVariable -> [MetaId]
    forall k a. Map k a -> [k]
    Map.keys (LocalMetaStores -> Map MetaId MetaVariable
    openMetas LocalMetaStores
    newMetaStore)
          return $ Just (newMetaIds, newMetaIds')
        (Bool
    False, LocalMetaStores
    _) -> Maybe ([MetaId], [MetaId]) -> SM (Maybe ([MetaId], [MetaId]))
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ([MetaId], [MetaId])
    forall a. Maybe a
    Nothing

    -- TODO: Make policy for when state should be put
    tryRefineAddMetas :: Goal -> Type -> SearchBranch -> Component -> SM (Maybe SearchBranch)
    tryRefineAddMetas :: Goal
    -> Type
    -> SearchBranch
    -> Component
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    tryRefineAddMetas Goal
    goal Type
    goalType SearchBranch
    branch Component
    comp = SearchBranch
    -> Goal
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    forall a. SearchBranch -> Goal -> SM a -> SM a
    withBranchAndGoal SearchBranch
    branch Goal
    goal (ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
     -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
    forall a b. (a -> b) -> a -> b
    $ do
      -- Apply the hint to new metas (generating @c@, @c ?@, @c ? ?@, etc.)
      -- TODO: Where is the best place to reduce the hint type?
      comp' <- Maybe VerboseLevel
    -> Component -> ReaderT SearchOptions (TCMT IO) Component
    applyToMetasG Maybe VerboseLevel
    forall a. Maybe a
    Nothing Component
    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 :: VerboseLevel -> Term -> Type -> SM (Term, Type, [MetaId])
    applyToMetas VerboseLevel
    skip Term
    term Type
    typ = do
      ctx <- ReaderT SearchOptions (TCMT IO) Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
      case unEl typ of
        Pi Dom Type
    dom Abs Type
    abs -> do
          let domainType :: Type
    domainType = Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    dom
          -- TODO: What exactly does the occur check do?
          (metaId', metaTerm) <- [Phase] -> SM (MetaId, Term) -> SM (MetaId, Term)
    forall a. NFData a => [Phase] -> SM a -> SM a
    bench [Phase
    Bench.Free] (SM (MetaId, Term) -> SM (MetaId, Term))
    -> SM (MetaId, Term) -> SM (MetaId, Term)
    forall a b. (a -> b) -> a -> b
    $ RunMetaOccursCheck -> Comparison -> Type -> SM (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta RunMetaOccursCheck
    DontRunMetaOccursCheck Comparison
    CmpLeq Type
    domainType
          let arg = Origin -> Arg Term -> Arg Term
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted (Arg Term -> Arg Term) -> Arg Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Term
    metaTerm Term -> Arg Type -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    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 VerboseLevel
    skip VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    > VerboseLevel
    0 then Term
    term else Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    apply Term
    term [Arg Term
    arg]
          (term', typ', metas) <- applyToMetas (predNat skip) newTerm newType
          return (term', typ', metaId' : metas)
        Term
    _ -> (Term, Type, [MetaId]) -> SM (Term, Type, [MetaId])
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term
    term, Type
    typ, [])

    normaliseSolution :: Term -> SM Term
    normaliseSolution :: Term -> ReaderT SearchOptions (TCMT IO) Term
    normaliseSolution Term
    t = do
      norm <- (SearchOptions -> Rewrite)
    -> ReaderT SearchOptions (TCMT IO) Rewrite
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SearchOptions -> Rewrite
    searchRewrite
      lift . normalForm norm =<< instantiateFull t

    checkSolved :: SearchBranch -> SM SearchStepResult
    checkSolved :: SearchBranch -> ReaderT SearchOptions (TCMT IO) SearchStepResult
    checkSolved SearchBranch
    branch = do
      ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer" VerboseLevel
    20 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Checking if branch is solved"
      ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer" VerboseLevel
    30 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "  remaining subgoals: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [MetaId] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [MetaId] -> m Doc
    prettyTCM ((Goal -> MetaId) -> [Goal] -> [MetaId]
    forall a b. (a -> b) -> [a] -> [b]
    map Goal -> MetaId
    goalMeta ([Goal] -> [MetaId]) -> [Goal] -> [MetaId]
    forall a b. (a -> b) -> a -> b
    $ SearchBranch -> [Goal]
    sbGoals SearchBranch
    branch)
      topMetaId <- (SearchOptions -> MetaId) -> ReaderT SearchOptions (TCMT IO) MetaId
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SearchOptions -> MetaId
    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.
          [] -> Expr -> SearchStepResult
    ResultExpr (Expr -> SearchStepResult)
    -> ReaderT SearchOptions (TCMT IO) Expr
    -> ReaderT SearchOptions (TCMT IO) SearchStepResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> ReaderT SearchOptions (TCMT IO) Expr
    forall (m :: * -> *) a.
    (MonadTCEnv m, MonadDebug m, BlankVars a) =>
    a -> m a
    blankNotInScope (Expr -> ReaderT SearchOptions (TCMT IO) Expr)
    -> ReaderT SearchOptions (TCMT IO) Expr
    -> ReaderT SearchOptions (TCMT IO) Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> ReaderT SearchOptions (TCMT IO) (ReifiesTo Term)
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
    reify Term
    inst)
          [Goal]
    _ -> do
            SearchStepResult
    -> ReaderT SearchOptions (TCMT IO) SearchStepResult
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SearchStepResult
     -> ReaderT SearchOptions (TCMT IO) SearchStepResult)
    -> SearchStepResult
    -> ReaderT SearchOptions (TCMT IO) SearchStepResult
    forall a b. (a -> b) -> a -> b
    $ SearchBranch -> SearchStepResult
    OpenBranch SearchBranch
    branch { sbGoals = goals }

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

    updateBranch' :: Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
    updateBranch' :: Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
    updateBranch' Maybe Component
    mComp [MetaId]
    newMetaIds SearchBranch
    branch = do
      state <- ReaderT SearchOptions (TCMT IO) TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
      let compsUsed = SearchBranch -> Map Name VerboseLevel
    sbComponentsUsed SearchBranch
    branch
      (deltaCost, compsUsed') <- case mComp of
            Maybe Component
    Nothing -> (VerboseLevel, Map Name VerboseLevel)
    -> ReaderT
         SearchOptions (TCMT IO) (VerboseLevel, Map Name VerboseLevel)
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (VerboseLevel
    0, Map Name VerboseLevel
    compsUsed)
            Just Component
    comp -> do
              case Component -> Maybe Name
    compName Component
    comp of
                Maybe Name
    Nothing -> (VerboseLevel, Map Name VerboseLevel)
    -> ReaderT
         SearchOptions (TCMT IO) (VerboseLevel, Map Name VerboseLevel)
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Component -> VerboseLevel
    compCost Component
    comp, Map Name VerboseLevel
    compsUsed)
                Just Name
    name -> case Map Name VerboseLevel
    compsUsed Map Name VerboseLevel -> Name -> Maybe VerboseLevel
    forall k a. Ord k => Map k a -> k -> Maybe a
    Map.!? Name
    name of
                  Maybe VerboseLevel
    Nothing -> (VerboseLevel, Map Name VerboseLevel)
    -> ReaderT
         SearchOptions (TCMT IO) (VerboseLevel, Map Name VerboseLevel)
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Component -> VerboseLevel
    compCost Component
    comp, Name
    -> VerboseLevel -> Map Name VerboseLevel -> Map Name VerboseLevel
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    name VerboseLevel
    1 Map Name VerboseLevel
    compsUsed)
                  Just VerboseLevel
    uses -> do
                    reuseCost <- (SearchOptions -> VerboseLevel -> VerboseLevel)
    -> ReaderT SearchOptions (TCMT IO) (VerboseLevel -> VerboseLevel)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (Costs -> VerboseLevel -> VerboseLevel
    costCompReuse (Costs -> VerboseLevel -> VerboseLevel)
    -> (SearchOptions -> Costs)
    -> SearchOptions
    -> VerboseLevel
    -> VerboseLevel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SearchOptions -> Costs
    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 :: [MetaId] -> SearchBranch -> SM SearchBranch
    updateBranch = Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
    updateBranch' Maybe Component
    forall a. Maybe a
    Nothing

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

    assignMeta :: MetaId -> Term -> Type -> SM [MetaId]
    assignMeta :: MetaId -> Term -> Type -> SM [MetaId]
    assignMeta MetaId
    metaId Term
    term Type
    metaType = [Phase] -> SM [MetaId] -> SM [MetaId]
    forall a. NFData a => [Phase] -> SM a -> SM a
    bench [Phase
    Bench.CheckRHS] (SM [MetaId] -> SM [MetaId]) -> SM [MetaId] -> SM [MetaId]
    forall a b. (a -> b) -> a -> b
    $ do
      ((), newMetaStore) <- ReaderT SearchOptions (TCMT IO) ()
    -> ReaderT SearchOptions (TCMT IO) ((), LocalMetaStores)
    forall (m :: * -> *) a.
    ReadTCState m =>
    m a -> m (a, LocalMetaStores)
    metasCreatedBy (ReaderT SearchOptions (TCMT IO) ()
     -> ReaderT SearchOptions (TCMT IO) ((), LocalMetaStores))
    -> ReaderT SearchOptions (TCMT IO) ()
    -> ReaderT SearchOptions (TCMT IO) ((), LocalMetaStores)
    forall a b. (a -> b) -> a -> b
    $ do
        metaVar <- MetaId -> ReaderT SearchOptions (TCMT IO) MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    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` \TCErr
    err -> do
          ArgName
    -> VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    reportSMDoc ArgName
    "mimer.assignMeta" VerboseLevel
    30 (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) ())
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [ReaderT SearchOptions (TCMT IO) Doc]
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ ReaderT SearchOptions (TCMT IO) Doc
    "Got error from assignV:" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCErr -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
    prettyTCM TCErr
    err
            , VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) Doc)
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ [ReaderT SearchOptions (TCMT IO) Doc]
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ ReaderT SearchOptions (TCMT IO) Doc
    "when trying to assign" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    term
              , ReaderT SearchOptions (TCMT IO) Doc
    "to" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    metaId ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ReaderT SearchOptions (TCMT IO) Doc
    ":" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    metaType
              , ReaderT SearchOptions (TCMT IO) Doc
    "in context" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) Doc)
    -> (Telescope -> ReaderT SearchOptions (TCMT IO) Doc)
    -> Telescope
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> ReaderT SearchOptions (TCMT IO) Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM (Telescope -> ReaderT SearchOptions (TCMT IO) Doc)
    -> ReaderT SearchOptions (TCMT IO) Telescope
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT SearchOptions (TCMT IO) Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope)
              ]
            ]

      let newMetaIds = Map MetaId MetaVariable -> [MetaId]
    forall k a. Map k a -> [k]
    Map.keys (LocalMetaStores -> Map MetaId MetaVariable
    openMetas LocalMetaStores
    newMetaStore)
      return newMetaIds

    dumbUnifier :: Type -> Type -> SM Bool
    dumbUnifier :: Type -> Type -> ReaderT SearchOptions (TCMT IO) Bool
    dumbUnifier Type
    t1 Type
    t2 = Maybe TCErr -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe TCErr -> Bool)
    -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    -> ReaderT SearchOptions (TCMT IO) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Type -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    dumbUnifierErr Type
    t1 Type
    t2

    dumbUnifierErr :: Type -> Type -> SM (Maybe TCErr)
    dumbUnifierErr :: Type -> Type -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    dumbUnifierErr Type
    t1 Type
    t2 = [Phase]
    -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    forall a. NFData a => [Phase] -> SM a -> SM a
    bench [Phase
    Bench.UnifyIndices] (ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
     -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr))
    -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    forall a b. (a -> b) -> a -> b
    $ do
      (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
    updateStat MimerStats -> MimerStats
    incTypeEqChecks
      ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (Maybe TCErr
    forall a. Maybe a
    Nothing Maybe TCErr
    -> ReaderT SearchOptions (TCMT IO) ()
    -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    forall a b.
    a
    -> ReaderT SearchOptions (TCMT IO) b
    -> ReaderT SearchOptions (TCMT IO) a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Type -> Type -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    t2 Type
    t1) ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    -> (TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr))
    -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    forall a.
    ReaderT SearchOptions (TCMT IO) a
    -> (TCErr -> ReaderT SearchOptions (TCMT IO) a)
    -> ReaderT SearchOptions (TCMT IO) a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    err -> do
        ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "mimer.unify" VerboseLevel
    80 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "Unification failed with error:", VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCErr -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
    prettyTCM TCErr
    err ]
        Maybe TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    forall a. a -> ReaderT SearchOptions (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr))
    -> Maybe TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
    forall a b. (a -> b) -> a -> b
    $ TCErr -> Maybe TCErr
    forall a. a -> Maybe a
    Just TCErr
    err

    -- Duplicate of a local definition in Agda.Interaction.BasicOps
    showTCM :: (MonadPretty tcm, PrettyTCM a) => a -> tcm String
    showTCM :: forall (tcm :: * -> *) a.
    (MonadPretty tcm, PrettyTCM a) =>
    a -> tcm ArgName
    showTCM a
    v = Doc -> ArgName
    forall a. Doc a -> ArgName
    P.render (Doc -> ArgName) -> tcm Doc -> tcm ArgName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> tcm Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    v

    bench :: NFData a => [Bench.Phase] -> SM a -> SM a
    bench :: forall a. NFData a => [Phase] -> SM a -> SM a
    bench [Phase]
    k SM a
    ma = Account (BenchPhase (ReaderT SearchOptions (TCMT IO)))
    -> SM a -> SM a
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    billTo (Phase
    mimerAccount Phase -> [Phase] -> [Phase]
    forall a. a -> [a] -> [a]
    : [Phase]
    k) SM a
    ma
      where
        -- Dummy account to avoid updating Bench. Doesn't matter since this is only used interactively
        -- to debug Mimer performance.
        mimerAccount :: Phase
    mimerAccount = Phase
    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 :: VerboseLevel -> VerboseLevel -> TCMT IO [Component]
    getLocalVars VerboseLevel
    localCxt VerboseLevel
    cost = do
      typedTerms <- VerboseLevel -> TCM [(Term, Dom Type)]
    getLocalVarTerms VerboseLevel
    localCxt
      let varZeroDiscount (Var VerboseLevel
    0 []) = a
    1
          varZeroDiscount Term
    _          = a
    0
      mapM (\(Term
    term, Dom Type
    domTyp) -> [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> TCMT IO Component
    forall (m :: * -> *).
    MonadFresh VerboseLevel m =>
    [MetaId]
    -> VerboseLevel
    -> Maybe Name
    -> VerboseLevel
    -> Term
    -> Type
    -> m Component
    newComponent [] (VerboseLevel
    cost VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    - Term -> VerboseLevel
    forall {a}. Num a => Term -> a
    varZeroDiscount Term
    term) Maybe Name
    noName VerboseLevel
    0 Term
    term (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    domTyp)) typedTerms

    getLocalVarTerms :: Int -> TCM [(Term, Dom Type)]
    getLocalVarTerms :: VerboseLevel -> TCM [(Term, Dom Type)]
    getLocalVarTerms VerboseLevel
    localCxt = do
      contextTerms <- TCMT IO [Term]
    forall (m :: * -> *). MonadTCEnv m => m [Term]
    getContextTerms
      contextTypes <- flattenTel <$> getContextTelescope
      let inScope VerboseLevel
    i Dom' Term Name
    _ | VerboseLevel
    i VerboseLevel -> VerboseLevel -> Bool
    forall a. Ord a => a -> a -> Bool
    < VerboseLevel
    localCxt = Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True   -- Ignore scope for variables we inserted ourselves
          inScope VerboseLevel
    _ Dom{ unDom :: forall t e. Dom' t e -> e
    unDom = Name
    name } = do
            x <- Name -> TCMT IO (ConOfAbs Name)
    forall a (m :: * -> *).
    (ToConcrete a, MonadAbsToCon m) =>
    a -> m (ConOfAbs a)
    abstractToConcrete_ Name
    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 :: SearchBranch -> ReaderT SearchOptions (TCMT IO) ArgName
    prettyBranch SearchBranch
    branch = SearchBranch
    -> ReaderT SearchOptions (TCMT IO) ArgName
    -> ReaderT SearchOptions (TCMT IO) ArgName
    forall a. SearchBranch -> SM a -> SM a
    withBranchState SearchBranch
    branch (ReaderT SearchOptions (TCMT IO) ArgName
     -> ReaderT SearchOptions (TCMT IO) ArgName)
    -> ReaderT SearchOptions (TCMT IO) ArgName
    -> ReaderT SearchOptions (TCMT IO) ArgName
    forall a b. (a -> b) -> a -> b
    $ do
        metaId <- (SearchOptions -> MetaId) -> ReaderT SearchOptions (TCMT IO) MetaId
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks SearchOptions -> MetaId
    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 -> Doc
    pretty Goal
    goal = MetaId -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (MetaId -> Doc) -> MetaId -> Doc
    forall a b. (a -> b) -> a -> b
    $ Goal -> MetaId
    goalMeta Goal
    goal

    instance Pretty SearchBranch where
      pretty :: SearchBranch -> Doc
    pretty SearchBranch
    branch = [(Doc, Doc)] -> Doc
    keyValueList
        [ (Doc
    "sbTCState", Doc
    "[...]")
        , (Doc
    "sbGoals", [Goal] -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty ([Goal] -> Doc) -> [Goal] -> Doc
    forall a b. (a -> b) -> a -> b
    $ SearchBranch -> [Goal]
    sbGoals SearchBranch
    branch)
        , (Doc
    "sbCost", VerboseLevel -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
    forall a b. (a -> b) -> a -> b
    $ SearchBranch -> VerboseLevel
    sbCost SearchBranch
    branch)
        , (Doc
    "sbComponentsUsed", Map Name VerboseLevel -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (Map Name VerboseLevel -> Doc) -> Map Name VerboseLevel -> Doc
    forall a b. (a -> b) -> a -> b
    $ SearchBranch -> Map Name VerboseLevel
    sbComponentsUsed SearchBranch
    branch)
        ]

    instance PrettyTCM BaseComponents where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => BaseComponents -> m Doc
    prettyTCM BaseComponents
    comps = do
        let thisFn :: m Doc
    thisFn = case BaseComponents -> Maybe Component
    hintThisFn BaseComponents
    comps of
              Maybe Component
    Nothing -> m Doc
    "(nothing)"
              Just Component
    comp -> Component -> m Doc
    forall {m :: * -> *}.
    (Applicative m, IsString (m Doc)) =>
    Component -> m Doc
    prettyComp Component
    comp
        [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ m Doc
    "Base components:"
             , VerboseLevel -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
               [ m Doc -> [Component] -> m Doc
    f m Doc
    "hintFns" (BaseComponents -> [Component]
    hintFns BaseComponents
    comps)
               , m Doc -> [Component] -> m Doc
    f m Doc
    "hintDataTypes" (BaseComponents -> [Component]
    hintDataTypes BaseComponents
    comps)
               , m Doc -> [Component] -> m Doc
    f m Doc
    "hintRecordTypes" (BaseComponents -> [Component]
    hintRecordTypes BaseComponents
    comps)
               , m Doc -> [Component] -> m Doc
    f m Doc
    "hintAxioms" (BaseComponents -> [Component]
    hintAxioms BaseComponents
    comps)
               , m Doc -> [Component] -> m Doc
    f m Doc
    "hintLevel" (BaseComponents -> [Component]
    hintLevel BaseComponents
    comps)
               , m Doc -> [Component] -> m Doc
    f m Doc
    "hintProjections" (BaseComponents -> [Component]
    hintProjections BaseComponents
    comps)
               , m Doc
    "hintThisFn:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    thisFn
               , (Open Component -> m Doc) -> m Doc -> [Open Component] -> m Doc
    forall {m :: * -> *} {a}.
    (Semigroup (m Doc), IsString (m Doc), Applicative m) =>
    (a -> m Doc) -> m Doc -> [a] -> m Doc
    g Open Component -> m Doc
    forall {m :: * -> *}.
    (Applicative m, IsString (m Doc)) =>
    Open Component -> m Doc
    prettyOpenComp m Doc
    "hintLetVars" (BaseComponents -> [Open Component]
    hintLetVars BaseComponents
    comps)
               , m Doc
    "hintRecVars: Open" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [(Term, VerboseLevel)] -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ((NoSubst Term VerboseLevel -> VerboseLevel)
    -> (Term, NoSubst Term VerboseLevel) -> (Term, VerboseLevel)
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd NoSubst Term VerboseLevel -> VerboseLevel
    forall t a. NoSubst t a -> a
    unNoSubst ((Term, NoSubst Term VerboseLevel) -> (Term, VerboseLevel))
    -> [(Term, NoSubst Term VerboseLevel)] -> [(Term, VerboseLevel)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Open [(Term, NoSubst Term VerboseLevel)]
    -> [(Term, NoSubst Term VerboseLevel)]
    forall a. Open a -> a
    openThing (BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)]
    hintRecVars BaseComponents
    comps))
               , m Doc
    "hintSplitVars: Open" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Open [Term] -> [Term]
    forall a. Open a -> a
    openThing (Open [Term] -> [Term]) -> Open [Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ BaseComponents -> Open [Term]
    hintSplitVars BaseComponents
    comps)
               ]
             ]
        where
          prettyComp :: Component -> m Doc
    prettyComp Component
    comp = Term -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Component -> Term
    compTerm Component
    comp) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Component -> Type
    compType Component
    comp)
          prettyOpenComp :: Open Component -> m Doc
    prettyOpenComp Open Component
    openComp = m Doc
    "Open" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (Component -> m Doc
    forall {m :: * -> *}.
    (Applicative m, IsString (m Doc)) =>
    Component -> m Doc
    prettyComp (Component -> m Doc) -> Component -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Open Component -> Component
    forall a. Open a -> a
    openThing Open Component
    openComp)
          prettyTCMComp :: Component -> m Doc
    prettyTCMComp Component
    comp = Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Component -> Term
    compTerm Component
    comp) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM (Component -> Type
    compType Component
    comp)
          f :: m Doc -> [Component] -> m Doc
    f = (Component -> m Doc) -> m Doc -> [Component] -> m Doc
    forall {m :: * -> *} {a}.
    (Semigroup (m Doc), IsString (m Doc), Applicative m) =>
    (a -> m Doc) -> m Doc -> [a] -> m Doc
    g Component -> m Doc
    forall {m :: * -> *}.
    (MonadFresh NameId m, MonadInteractionPoints m,
     MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
     Semigroup (m Doc)) =>
    Component -> m Doc
    prettyTCMComp
          g :: (a -> m Doc) -> m Doc -> [a] -> m Doc
    g a -> m Doc
    p m Doc
    n [] = m Doc
    n m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ": []"
          g a -> m Doc
    p m Doc
    n [a]
    xs = (m Doc
    n m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ":") m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $+$ VerboseLevel -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 ([m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ (a -> m Doc) -> [a] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> m Doc
    p [a]
    xs)

    -- -- TODO: Is it possible to derive the pretty instances?
    instance Pretty BaseComponents where
      pretty :: BaseComponents -> Doc
    pretty BaseComponents
    comps = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.vcat
          [ Doc -> [Component] -> Doc
    forall {a}. Pretty a => Doc -> [a] -> Doc
    f Doc
    "hintFns" (BaseComponents -> [Component]
    hintFns BaseComponents
    comps)
          , Doc -> [Component] -> Doc
    forall {a}. Pretty a => Doc -> [a] -> Doc
    f Doc
    "hintDataTypes" (BaseComponents -> [Component]
    hintDataTypes BaseComponents
    comps)
          , Doc -> [Component] -> Doc
    forall {a}. Pretty a => Doc -> [a] -> Doc
    f Doc
    "hintRecordTypes" (BaseComponents -> [Component]
    hintRecordTypes BaseComponents
    comps)
          , Doc -> [Component] -> Doc
    forall {a}. Pretty a => Doc -> [a] -> Doc
    f Doc
    "hintAxioms" (BaseComponents -> [Component]
    hintAxioms BaseComponents
    comps)
          , Doc -> [Component] -> Doc
    forall {a}. Pretty a => Doc -> [a] -> Doc
    f Doc
    "hintLevel" (BaseComponents -> [Component]
    hintLevel BaseComponents
    comps)
          , Doc -> [Component] -> Doc
    forall {a}. Pretty a => Doc -> [a] -> Doc
    f Doc
    "hintProjections" (BaseComponents -> [Component]
    hintProjections BaseComponents
    comps)
          ]
        where
          f :: Doc -> [a] -> Doc
    f Doc
    n [] = Doc
    n Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Doc
    ": []"
          f Doc
    n [a]
    xs = (Doc
    n Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Doc
    ":") Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    P.$$ VerboseLevel -> Doc -> Doc
    forall a. VerboseLevel -> Doc a -> Doc a
    P.nest VerboseLevel
    2 ([a] -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty [a]
    xs)

    instance Pretty SearchOptions where
      pretty :: SearchOptions -> Doc
    pretty SearchOptions
    opts = [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.vcat
        [ Doc
    "searchBaseComponents:"
        , VerboseLevel -> Doc -> Doc
    forall a. VerboseLevel -> Doc a -> Doc a
    P.nest VerboseLevel
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ BaseComponents -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (BaseComponents -> Doc) -> BaseComponents -> Doc
    forall a b. (a -> b) -> a -> b
    $ SearchOptions -> BaseComponents
    searchBaseComponents SearchOptions
    opts
        , [(Doc, Doc)] -> Doc
    keyValueList
          [ (Doc
    "searchHintMode", HintMode -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (HintMode -> Doc) -> HintMode -> Doc
    forall a b. (a -> b) -> a -> b
    $ SearchOptions -> HintMode
    searchHintMode SearchOptions
    opts)
          , (Doc
    "searchTimeout",  Integer -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (Integer -> Doc) -> Integer -> Doc
    forall a b. (a -> b) -> a -> b
    $ SearchOptions -> Integer
    searchTimeout SearchOptions
    opts)
          , (Doc
    "searchTopMeta",  MetaId -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (MetaId -> Doc) -> MetaId -> Doc
    forall a b. (a -> b) -> a -> b
    $ SearchOptions -> MetaId
    searchTopMeta SearchOptions
    opts)
          , (Doc
    "searchTopEnv", Doc
    "[...]")
          ]
        , Doc
    "searchCosts:"
        , VerboseLevel -> Doc -> Doc
    forall a. VerboseLevel -> Doc a -> Doc a
    P.nest VerboseLevel
    2 (Costs -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (Costs -> Doc) -> Costs -> Doc
    forall a b. (a -> b) -> a -> b
    $ SearchOptions -> Costs
    searchCosts SearchOptions
    opts)
        ]

    instance PrettyTCM SearchOptions where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => SearchOptions -> m Doc
    prettyTCM SearchOptions
    opts = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ m Doc
    "searchBaseComponents:"
        , VerboseLevel -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ BaseComponents -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => BaseComponents -> m Doc
    prettyTCM (BaseComponents -> m Doc) -> BaseComponents -> m Doc
    forall a b. (a -> b) -> a -> b
    $ SearchOptions -> BaseComponents
    searchBaseComponents SearchOptions
    opts
        , [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ m Doc
    "searchHintMode:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> HintMode -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (SearchOptions -> HintMode
    searchHintMode SearchOptions
    opts)
          , m Doc
    "searchTimeout:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Integer -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (SearchOptions -> Integer
    searchTimeout SearchOptions
    opts)
          , m Doc
    "searchTopMeta:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM (SearchOptions -> MetaId
    searchTopMeta SearchOptions
    opts)
          , m Doc
    "searchTopEnv: [...]"
          , m Doc
    "searchTopCheckpoint:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> CheckpointId -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => CheckpointId -> m Doc
    prettyTCM (SearchOptions -> CheckpointId
    searchTopCheckpoint SearchOptions
    opts)
          , m Doc
    "searchInteractionId:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> InteractionId -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (SearchOptions -> InteractionId
    searchInteractionId SearchOptions
    opts)
          , m Doc
    "searchFnName:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Maybe QName -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (SearchOptions -> Maybe QName
    searchFnName SearchOptions
    opts)
          , m Doc
    "searchStats: [...]"
          ]
        , m Doc
    "searchCosts:"
        , VerboseLevel -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest VerboseLevel
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ Costs -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Costs -> m Doc) -> Costs -> m Doc
    forall a b. (a -> b) -> a -> b
    $ SearchOptions -> Costs
    searchCosts SearchOptions
    opts
        ]

    instance Pretty Component where
      pretty :: Component -> Doc
    pretty Component
    comp = Doc -> [(Doc, Doc)] -> Doc
    haskellRecord Doc
    "Component"
        [ (Doc
    "compId", VerboseLevel -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
    forall a b. (a -> b) -> a -> b
    $ Component -> VerboseLevel
    compId Component
    comp)
        , (Doc
    "compTerm", Term -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (Term -> Doc) -> Term -> Doc
    forall a b. (a -> b) -> a -> b
    $ Component -> Term
    compTerm Component
    comp)
        , (Doc
    "compType", Type -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (Type -> Doc) -> Type -> Doc
    forall a b. (a -> b) -> a -> b
    $ Component -> Type
    compType Component
    comp)
        , (Doc
    "compMetas", [MetaId] -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty ([MetaId] -> Doc) -> [MetaId] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Component -> [MetaId]
    compMetas Component
    comp)
        , (Doc
    "compCost", VerboseLevel -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
    forall a b. (a -> b) -> a -> b
    $ Component -> VerboseLevel
    compCost Component
    comp)
        ]

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

    instance PrettyTCM Component where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => Component -> m Doc
    prettyTCM Component{Bool
    VerboseLevel
    [MetaId]
    Maybe Name
    Type
    Term
    compId :: Component -> VerboseLevel
    compName :: Component -> Maybe Name
    compPars :: Component -> VerboseLevel
    compTerm :: Component -> Term
    compType :: Component -> Type
    compRec :: Component -> Bool
    compMetas :: Component -> [MetaId]
    compCost :: Component -> VerboseLevel
    compId :: VerboseLevel
    compName :: Maybe Name
    compPars :: VerboseLevel
    compTerm :: Term
    compType :: Type
    compRec :: Bool
    compMetas :: [MetaId]
    compCost :: VerboseLevel
    ..} = m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (VerboseLevel -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
    prettyTCM VerboseLevel
    compId) m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
        [ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ Term -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    compTerm
              , m Doc
    ":" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    compType ]
        , m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ m Doc -> [m Doc] -> [m Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate m Doc
    ","
          [ m Doc
    "cost:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> VerboseLevel -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
    prettyTCM VerboseLevel
    compCost
          , m Doc
    "metas:" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [MetaId] -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [MetaId] -> m Doc
    prettyTCM [MetaId]
    compMetas
          ]
        ]

    instance PrettyTCM MimerResult where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => MimerResult -> m Doc
    prettyTCM = \case
        MimerExpr ArgName
    expr    -> ArgName -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ArgName
    expr
        MimerClauses QName
    f [Clause]
    cl -> m Doc
    "MimerClauses" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    f m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "[..]" -- TODO: display the clauses
        MimerResult
    MimerNoResult     -> m Doc
    "MimerNoResult"
        MimerList [(VerboseLevel, ArgName)]
    sols    -> m Doc
    "MimerList" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [(VerboseLevel, ArgName)] -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [(VerboseLevel, ArgName)]
    sols

    concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
    concatMapM :: forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
    concatMapM a -> m [b]
    f = ([[b]] -> [b]) -> m [[b]] -> m [b]
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [[b]] -> [b]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat (m [[b]] -> m [b]) -> ([a] -> m [[b]]) -> [a] -> m [b]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m [b]) -> [a] -> m [[b]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM a -> m [b]
    f

    reportSMDoc :: VerboseKey -> VerboseLevel -> SM Doc -> SM ()
    reportSMDoc :: ArgName
    -> VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    reportSMDoc ArgName
    vk VerboseLevel
    vl ReaderT SearchOptions (TCMT IO) Doc
    md = ArgName
    -> VerboseLevel
    -> TCMT IO Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    vk VerboseLevel
    vl (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
    -> (SearchOptions -> TCMT IO Doc)
    -> SearchOptions
    -> ReaderT SearchOptions (TCMT IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ReaderT SearchOptions (TCMT IO) Doc -> SearchOptions -> TCMT IO Doc
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT SearchOptions (TCMT IO) Doc
    md (SearchOptions -> ReaderT SearchOptions (TCMT IO) ())
    -> ReaderT SearchOptions (TCMT IO) SearchOptions
    -> ReaderT SearchOptions (TCMT IO) ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT SearchOptions (TCMT IO) SearchOptions
    forall r (m :: * -> *). MonadReader r m => m r
    ask

    mimerTrace :: Int -> VerboseLevel -> SM Doc -> SM ()
    mimerTrace :: VerboseLevel
    -> VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    mimerTrace VerboseLevel
    ilvl VerboseLevel
    vlvl ReaderT SearchOptions (TCMT IO) Doc
    doc = ArgName
    -> VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    reportSMDoc ArgName
    "mimer.trace" VerboseLevel
    vlvl (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) ())
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ VerboseLevel
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
    nest (VerboseLevel
    2 VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    * VerboseLevel
    ilvl) (ReaderT SearchOptions (TCMT IO) Doc
     -> ReaderT SearchOptions (TCMT IO) Doc)
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall a b. (a -> b) -> a -> b
    $ ReaderT SearchOptions (TCMT IO) Doc
    "-" ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    -> ReaderT SearchOptions (TCMT IO) Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ReaderT SearchOptions (TCMT IO) Doc
    doc

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

    keyValueList :: [(Doc, Doc)] -> Doc
    keyValueList :: [(Doc, Doc)] -> Doc
    keyValueList [(Doc, Doc)]
    kvs = Doc -> Doc
    P.braces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.sep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
    P.punctuate Doc
    "," [ Doc -> VerboseLevel -> Doc -> Doc
    forall a. Doc a -> VerboseLevel -> Doc a -> Doc a
    P.hang (Doc
    k Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    P.<> Doc
    ":") VerboseLevel
    2 Doc
    v | (Doc
    k, Doc
    v) <- [(Doc, Doc)]
    kvs ]

    writeTime :: (ReadTCState m, MonadError TCErr m, MonadTCM m, MonadDebug m) => InteractionId -> Maybe CPUTime -> m ()
    writeTime :: forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCM m, MonadDebug m) =>
    InteractionId -> Maybe CPUTime -> m ()
    writeTime InteractionId
    ii Maybe CPUTime
    mTime = do
      let time :: ArgName
    time = case Maybe CPUTime
    mTime of
            Maybe CPUTime
    Nothing -> ArgName
    "n/a"
            Just (CPUTime Integer
    t) -> Integer -> ArgName
    forall a. Show a => a -> ArgName
    show Integer
    t
      file <- Range -> SrcFile
    rangeFile (Range -> SrcFile)
    -> (InteractionPoint -> Range) -> InteractionPoint -> SrcFile
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InteractionPoint -> Range
    ipRange (InteractionPoint -> SrcFile) -> m InteractionPoint -> m SrcFile
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> InteractionId -> m InteractionPoint
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint InteractionId
    ii
      case file of
        SrcFile
    SMaybe.Nothing ->
          ArgName -> VerboseLevel -> ArgName -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> VerboseLevel -> ArgName -> m ()
    reportSLn ArgName
    "mimer.stats" VerboseLevel
    2 ArgName
    "No file found for interaction id"
        SMaybe.Just RangeFile
    file -> do
          let path :: ArgName
    path = AbsolutePath -> ArgName
    filePath (RangeFile -> AbsolutePath
    rangeFilePath RangeFile
    file) ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    ".stats"
          IO () -> m ()
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> ArgName -> IO ()
    appendFile ArgName
    path (VerboseLevel -> ArgName
    forall a. Show a => a -> ArgName
    show (InteractionId -> VerboseLevel
    interactionId InteractionId
    ii) ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    time ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    "\n")

    -- Hack to let you experiment with costs using verbosity flags.
    customCosts :: TCM Costs
    customCosts :: TCMT IO Costs
    customCosts = do
      costLocal         <- ArgName -> TCM VerboseLevel
    forall {m :: * -> *}. MonadDebug m => ArgName -> m VerboseLevel
    cost ArgName
    "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 VerboseLevel
    uses = VerboseLevel
    compReuse VerboseLevel -> VerboseLevel -> VerboseLevel
    forall a. Num a => a -> a -> a
    * VerboseLevel
    uses VerboseLevel -> Integer -> VerboseLevel
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer
    2
      pure Costs{..}
      where
        cost :: ArgName -> m VerboseLevel
    cost ArgName
    key = ArgName -> m VerboseLevel
    forall {m :: * -> *}. MonadDebug m => ArgName -> m VerboseLevel
    getVerbosityLevel (ArgName
    "mimer-cost." ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    key)

    getVerbosityLevel :: MonadDebug m => VerboseKey -> m VerboseLevel
    getVerbosityLevel :: forall {m :: * -> *}. MonadDebug m => ArgName -> m VerboseLevel
    getVerbosityLevel ArgName
    k = do
      t <- m Verbosity
    forall (m :: * -> *). MonadDebug m => m Verbosity
    getVerbosity
      return $ case t of
        Verbosity
    Strict.Nothing -> VerboseLevel
    1
        Strict.Just Trie VerboseKeyItem VerboseLevel
    t
          | Trie VerboseKeyItem VerboseLevel
    t Trie VerboseKeyItem VerboseLevel
    -> Trie VerboseKeyItem VerboseLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == [VerboseKeyItem]
    -> VerboseLevel -> Trie VerboseKeyItem VerboseLevel
    forall k v. [k] -> v -> Trie k v
    Trie.singleton [] VerboseLevel
    0 -> VerboseLevel
    0
          | Bool
    otherwise -> VerboseLevel -> [VerboseLevel] -> VerboseLevel
    forall a. a -> [a] -> a
    lastWithDefault VerboseLevel
    0 ([VerboseLevel] -> VerboseLevel) -> [VerboseLevel] -> VerboseLevel
    forall a b. (a -> b) -> a -> b
    $ [VerboseKeyItem]
    -> Trie VerboseKeyItem VerboseLevel -> [VerboseLevel]
    forall k v. Ord k => [k] -> Trie k v -> [v]
    Trie.lookupPath [VerboseKeyItem]
    ks Trie VerboseKeyItem VerboseLevel
    t
      where ks :: [VerboseKeyItem]
    ks = ArgName -> [VerboseKeyItem]
    parseVerboseKey ArgName
    k