-- | 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.Monad
import Control.Monad.IO.Class (liftIO)
import Control.Monad.Reader (ReaderT(..), runReaderT, asks, ask, lift)
import Data.Functor ((<&>))
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Maybe (maybeToList)
import Data.PQueue.Min (MinQueue)
import qualified Data.PQueue.Min as Q

import qualified Agda.Benchmarking as Bench
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty qualified as P
import Agda.Syntax.Info (pattern UnificationMeta)
import Agda.Syntax.Internal
import Agda.Syntax.Position (Range, noRange)
import Agda.Syntax.Translation.InternalToAbstract (reify, blankNotInScope)

import Agda.TypeChecking.Empty (isEmptyType)
import Agda.TypeChecking.Level (levelType)
import Agda.TypeChecking.MetaVars (newValueMeta)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce (reduce, instantiateFull, instantiate)
import Agda.TypeChecking.Rules.Term  (makeAbsurdLambda)
import Agda.TypeChecking.Substitute (apply, NoSubst(..))

import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Maybe (catMaybes)
import Agda.Utils.Null
import Agda.Utils.Tuple (mapFst, mapSnd)
import Agda.Utils.Time (measureTime, getCPUTime, fromMilliseconds)

import Data.IORef (readIORef)

import Agda.Interaction.Base (Rewrite(..))
import Agda.Interaction.BasicOps (normalForm)
import Agda.Utils.Monad (concatMapM)

import Agda.Mimer.Types (MimerResult(..), BaseComponents(..), Component(..),
                         SearchBranch(..), SearchStepResult(..), SearchOptions(..),
                         Goal(..), Costs(..), goalMeta, replaceCompMeta,
                         incRefineFail, incRefineSuccess, incCompRegen, incCompNoRegen,
                         nextGoal, addCost, isNoResult)
import Agda.Mimer.Monad
import Agda.Mimer.Options

-- IDEA for implementing case-splitting:
--  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.

-- | 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 -> String -> tcm MimerResult
mimer Rewrite
norm InteractionId
ii Range
rng String
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
  String -> CompId -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.top" CompId
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
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> String
forall a. Show a => a -> String
show String
argStr)

  (sol, time) <- TCM MimerResult -> TCMT IO (MimerResult, CPUTime)
forall (m :: * -> *) a. MonadIO m => m a -> m (a, CPUTime)
measureTime (TCM MimerResult -> TCMT IO (MimerResult, CPUTime))
-> TCM MimerResult -> TCMT IO (MimerResult, CPUTime)
forall a b. (a -> b) -> a -> b
$ do

    opts <- InteractionId -> Range -> String -> TCM Options
parseOptions InteractionId
ii Range
rng String
argStr
    reportS "mimer.top" 15 ("Mimer options: " ++ show opts)

    sols <- localTCState $ runSearch norm opts ii rng

    -- Turn the solutions into the desired results (first solution or list of solutions).
    case drop (optSkip opts) $ zip [0..] sols of
      [] -> do
        String -> CompId -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> String -> m ()
reportSLn String
"mimer.top" CompId
10 String
"No solution found"
        MimerResult -> TCM MimerResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MimerResult
MimerNoResult
      [(CompId, 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
$ [(CompId, String)] -> MimerResult
MimerList [ (CompId
i, String
s) | (CompId
i, MimerExpr String
s) <- [(CompId, MimerResult)]
sols' ]
      (CompId
_, MimerResult
sol) : [(CompId, MimerResult)]
_ -> do
        String -> CompId -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.top" CompId
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.
  reportSDoc "mimer.top" 10 ("Total elapsed time:" <+> pretty time)
  when (not $ isNoResult sol) $
    verboseS "mimer.stats" 50 $ writeTime ii 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


------------------------------------------------------------------------------
-- * 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
  metaId <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
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
      String -> CompId -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> String -> m ()
reportSLn String
"mimer.init" CompId
20 String
"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 -> String) -> [Doc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Char
'{', Char
'}']) (String -> String) -> (Doc -> String) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Doc a -> String
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 = String -> MimerResult
MimerExpr String
str
          reportSDoc "mimer.init" 10 $ "Goal already solved. Solution:" <+> text str
          return [sol]
        MetaInstantiation
_ -> TCM [MimerResult]
forall a. HasCallStack => a
__IMPOSSIBLE__
    [MetaId]
_ -> do
      searchOptions <- Rewrite -> Options -> InteractionId -> TCM SearchOptions
makeSearchOptions Rewrite
norm Options
options InteractionId
ii
      -- Caution: startSearchBranch puts the current TCState in the branch, which includes
      --          the freshId counter for components, that gets bumped in makeSearchOptions
      --          above (computing the initial components), so it's important to not switch
      --          these two calls around.
      startBranch   <- startSearchBranch metaIds

      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 CompId
0 CompId
n MinQueue SearchBranch
_ = ([MimerResult], CompId) -> SM ([MimerResult], CompId)
forall a. a -> ReaderT SearchOptions TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], CompId
n)
            go CompId
need CompId
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
                String -> CompId -> String -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> String -> m ()
reportSLn String
"mimer.search" CompId
30 (String -> ReaderT SearchOptions TCM ())
-> String -> ReaderT SearchOptions TCM ()
forall a b. (a -> b) -> a -> b
$ String
"No remaining search branches."
                ([MimerResult], CompId) -> SM ([MimerResult], CompId)
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], CompId
n)
              Just (SearchBranch
branch, MinQueue SearchBranch
branchQueue') -> do
                time <- IO CPUTime -> ReaderT SearchOptions TCM CPUTime
forall a. IO a -> ReaderT SearchOptions TCM 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' = CompId -> [MimerResult] -> [MimerResult]
forall a. CompId -> [a] -> [a]
take CompId
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 = CompId
10 CompId -> CompId -> CompId
forall a. Num a => a -> a -> a
+ Options -> CompId
optSkip Options
options
                         | Bool
otherwise       = CompId
1 CompId -> CompId -> CompId
forall a. Num a => a -> a -> a
+ Options -> CompId
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

-- | 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
  String -> CompId -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.components" CompId
50 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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 TCM 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 TCM ()
updateStat MimerStats -> MimerStats
incCompRegen
      String -> CompId -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.components" CompId
20 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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
        , CompId -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => CompId -> m Doc -> m Doc
nest CompId
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 TCM [(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 TCM (Component, [Component]))
-> [(Component, Maybe [Component])]
-> ReaderT SearchOptions TCM [(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 TCM (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 TCM (Component, [Component])
prepare (Component
sourceComp, Just [Component]
comps) = do
    (MimerStats -> MimerStats) -> ReaderT SearchOptions TCM ()
updateStat MimerStats -> MimerStats
incCompNoRegen
    (Component, [Component])
-> ReaderT SearchOptions TCM (Component, [Component])
forall a. a -> ReaderT SearchOptions TCM 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 TCM ()
updateStat MimerStats -> MimerStats
incCompRegen
    (Component
sourceComp,) ([Component] -> (Component, [Component]))
-> ReaderT SearchOptions TCM [Component]
-> ReaderT SearchOptions TCM (Component, [Component])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Component -> ReaderT SearchOptions TCM [Component]
genComponentsFrom Bool
True Component
sourceComp

genComponents :: SM [(Component, [Component])]
genComponents :: ReaderT SearchOptions TCM [(Component, [Component])]
genComponents = do
  opts <- ReaderT SearchOptions TCM 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 TCM [(Component, [Component])]
genAddSource Bool
genProj = (Component -> ReaderT SearchOptions TCM (Component, [Component]))
-> [Component]
-> ReaderT SearchOptions TCM [(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 TCM [Component]
-> ReaderT SearchOptions TCM (Component, [Component])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Component -> ReaderT SearchOptions TCM [Component]
genComponentsFrom Bool
genProj Component
comp)


genComponentsFrom :: Bool -- ^ Apply record elimination
                  -> Component
                  -> SM [Component]
genComponentsFrom :: Bool -> Component -> ReaderT SearchOptions TCM [Component]
genComponentsFrom Bool
appRecElims Component
origComp = do
  String -> CompId -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.components" CompId
50 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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
<+> CompId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CompId -> m Doc
prettyTCM (Component -> CompId
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 TCM Component)
-> [Component] -> ReaderT SearchOptions TCM [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 CompId -> Component -> ReaderT SearchOptions TCM Component
applyToMetasG Maybe CompId
forall a. Maybe a
Nothing) ([Component] -> ReaderT SearchOptions TCM [Component])
-> ReaderT SearchOptions TCM [Component]
-> ReaderT SearchOptions TCM [Component]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Component -> ReaderT SearchOptions TCM [Component]
genRecCalls Component
origComp
              | Bool
otherwise        -> (Component -> [Component] -> [Component]
forall a. a -> [a] -> [a]
:[]) (Component -> [Component])
-> ReaderT SearchOptions TCM Component
-> ReaderT SearchOptions TCM [Component]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CompId -> Component -> ReaderT SearchOptions TCM Component
applyToMetasG Maybe CompId
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 TCM [Component]
applyProjections Set QName
seenRecords Component
comp = do
    projComps <- Type
-> ReaderT SearchOptions TCM (Maybe (QName, Args, [QName], Bool))
forall (tcm :: * -> *).
(MonadTCM tcm, HasConstInfo tcm) =>
Type -> tcm (Maybe (QName, Args, [QName], Bool))
getRecordInfo (Component -> Type
compType Component
comp) ReaderT SearchOptions TCM (Maybe (QName, Args, [QName], Bool))
-> (Maybe (QName, Args, [QName], Bool)
    -> ReaderT SearchOptions TCM [Component])
-> ReaderT SearchOptions TCM [Component]
forall a b.
ReaderT SearchOptions TCM a
-> (a -> ReaderT SearchOptions TCM b)
-> ReaderT SearchOptions TCM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe (QName, Args, [QName], Bool)
Nothing -> [Component] -> ReaderT SearchOptions TCM [Component]
forall a. a -> ReaderT SearchOptions TCM 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
              String -> CompId -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.components" CompId
60 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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 TCM [Component]
forall a. a -> ReaderT SearchOptions TCM 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 TCM Component)
-> [QName] -> ReaderT SearchOptions TCM [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 TCM Component
applyProj Args
args Component
comp (QName -> ReaderT SearchOptions TCM Component)
-> (Component -> ReaderT SearchOptions TCM Component)
-> QName
-> ReaderT SearchOptions TCM Component
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Maybe CompId -> Component -> ReaderT SearchOptions TCM Component
applyToMetasG Maybe CompId
forall a. Maybe a
Nothing) [QName]
fields
              concatMapM (applyProjections seenRecords') comps
    return $ comp : projComps

genRecCalls :: Component -> SM [Component]
genRecCalls :: Component -> ReaderT SearchOptions TCM [Component]
genRecCalls Component
thisFn = do
  String -> CompId -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.components.open" CompId
40 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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
<+> CompId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CompId -> m Doc
prettyTCM (Component -> CompId
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)
  String -> CompId -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.components.open" CompId
60 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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 CompId)])
-> ReaderT SearchOptions TCM (Open [(Term, NoSubst Term CompId)])
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> Open [(Term, NoSubst Term CompId)]
hintRecVars (BaseComponents -> Open [(Term, NoSubst Term CompId)])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> Open [(Term, NoSubst Term CompId)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents) ReaderT SearchOptions TCM (Open [(Term, NoSubst Term CompId)])
-> (Open [(Term, NoSubst Term CompId)]
    -> ReaderT SearchOptions TCM [(Term, NoSubst Term CompId)])
-> ReaderT SearchOptions TCM [(Term, NoSubst Term CompId)]
forall a b.
ReaderT SearchOptions TCM a
-> (a -> ReaderT SearchOptions TCM b)
-> ReaderT SearchOptions TCM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Open [(Term, NoSubst Term CompId)]
-> ReaderT SearchOptions TCM [(Term, NoSubst Term CompId)]
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen ReaderT SearchOptions TCM [(Term, NoSubst Term CompId)]
-> ([(Term, NoSubst Term CompId)]
    -> ReaderT SearchOptions TCM [Component])
-> ReaderT SearchOptions TCM [Component]
forall a b.
ReaderT SearchOptions TCM a
-> (a -> ReaderT SearchOptions TCM b)
-> ReaderT SearchOptions TCM 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 TCM [Component]
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    [(Term, NoSubst Term CompId)]
recCandTerms -> do
      Costs{..} <- (SearchOptions -> Costs) -> ReaderT SearchOptions TCM 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, CompId
i) | t :: Component
t@(Component -> Term
compTerm -> v :: Term
v@Var{}) <- [Component]
localVars, NoSubst CompId
i <- Maybe (NoSubst Term CompId) -> [NoSubst Term CompId]
forall a. Maybe a -> [a]
maybeToList (Maybe (NoSubst Term CompId) -> [NoSubst Term CompId])
-> Maybe (NoSubst Term CompId) -> [NoSubst Term CompId]
forall a b. (a -> b) -> a -> b
$ Term
-> [(Term, NoSubst Term CompId)] -> Maybe (NoSubst Term CompId)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Term
v [(Term, NoSubst Term CompId)]
recCandTerms ]

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


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 TCM Type -> ReaderT SearchOptions TCM Type
forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase
Bench.Reduce] (ReaderT SearchOptions TCM Type -> ReaderT SearchOptions TCM Type)
-> ReaderT SearchOptions TCM Type -> ReaderT SearchOptions TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> ReaderT SearchOptions TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> ReaderT SearchOptions TCM Type)
-> ReaderT SearchOptions TCM Type -> ReaderT SearchOptions TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> ReaderT SearchOptions TCM 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
        CompId -> CompId -> SM Doc -> ReaderT SearchOptions TCM ()
mimerTrace CompId
1 CompId
10 (SM Doc -> ReaderT SearchOptions TCM ())
-> SM Doc -> ReaderT SearchOptions TCM ()
forall a b. (a -> b) -> a -> b
$ [SM Doc] -> SM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
              [ SM Doc
"Absurd bambda refinement", CompId -> SM Doc -> SM Doc
forall (m :: * -> *). Functor m => CompId -> m Doc -> m Doc
nest CompId
2 (SM Doc -> SM Doc) -> SM Doc -> SM Doc
forall a b. (a -> b) -> a -> b
$ Goal -> SM 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 TCM Args
-> ReaderT SearchOptions TCM Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT SearchOptions TCM 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

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 TCM 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 TCM [Maybe SearchBranch]
-> ReaderT SearchOptions TCM [SearchBranch]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Component -> ReaderT SearchOptions TCM (Maybe SearchBranch))
-> [Component] -> ReaderT SearchOptions TCM [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 TCM (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

-- | 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 TCM 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 TCM Bool
-> (Bool -> SM (Either SearchBranch (Goal, Type, SearchBranch)))
-> SM (Either SearchBranch (Goal, Type, SearchBranch))
forall a b.
ReaderT SearchOptions TCM a
-> (a -> ReaderT SearchOptions TCM b)
-> ReaderT SearchOptions TCM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True -> do
        f <- TCM QName -> ReaderT SearchOptions TCM QName
forall a. TCM a -> ReaderT SearchOptions TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM QName -> ReaderT SearchOptions TCM QName)
-> TCM QName -> ReaderT SearchOptions TCM 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
        String -> CompId -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.lam" CompId
40 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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' | String -> Bool
forall a. IsNoName a => a -> Bool
isNoName (Abs Type -> String
forall a. Abs a -> String
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 TCM (MetaId, Type, Term, TCEnv))
-> ReaderT SearchOptions TCM (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 TCM (MetaId, Type, Term, TCEnv))
 -> ReaderT SearchOptions TCM (MetaId, Type, Term, TCEnv))
-> (Type -> ReaderT SearchOptions TCM (MetaId, Type, Term, TCEnv))
-> ReaderT SearchOptions TCM (MetaId, Type, Term, TCEnv)
forall a b. (a -> b) -> a -> b
$ \Type
bodyType -> do
          String -> CompId -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.lam" CompId
40 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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 TCM Type -> ReaderT SearchOptions TCM Type
forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase
Bench.Reduce] (ReaderT SearchOptions TCM Type -> ReaderT SearchOptions TCM Type)
-> ReaderT SearchOptions TCM Type -> ReaderT SearchOptions TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> ReaderT SearchOptions TCM 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 = String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs (Abs Type -> String
forall a. Abs a -> String
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')

-- 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 TCM Definition
-> ReaderT SearchOptions TCM Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ReaderT SearchOptions TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qname ReaderT SearchOptions TCM Defn
-> (Defn -> SM [SearchStepResult]) -> SM [SearchStepResult]
forall a b.
ReaderT SearchOptions TCM a
-> (a -> ReaderT SearchOptions TCM b)
-> ReaderT SearchOptions TCM 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 TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      -- TODO: Better way of checking that type is Level
      Axiom{}
        | QName -> String
forall a. Pretty a => a -> String
P.prettyShow QName
qname String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"Agda.Primitive.Level" -> do
            tryLevel
        | Bool
otherwise -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      DataOrRecSig{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      GeneralizableVar{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      AbstractDefn{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Function{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Constructor{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      PrimitiveSort{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions TCM 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 TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Term
_ -> [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions TCM 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 -> CompId) -> SM CompId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> CompId
costRecordCon (Costs -> CompId)
-> (SearchOptions -> Costs) -> SearchOptions -> CompId
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
      String -> CompId -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> CompId -> TCMT IO Doc -> m ()
reportSDoc String
"mimer.try" CompId
40 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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 -> CompId) -> SM CompId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> CompId
costDataCon (Costs -> CompId)
-> (SearchOptions -> Costs) -> SearchOptions -> CompId
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 TCM [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 TCM 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]
-> CompId
-> Maybe Name
-> CompId
-> Term
-> Type
-> ReaderT SearchOptions TCM Component
forall (m :: * -> *).
MonadFresh CompId m =>
[MetaId]
-> CompId -> Maybe Name -> CompId -> Term -> Type -> m Component
newComponent [] CompId
cost Maybe Name
forall a. Maybe a
Nothing CompId
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 TCM [(SearchBranch, Component)]
forall a. a -> ReaderT SearchOptions TCM 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 TCM Type -> SM (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT SearchOptions TCM 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 TCM (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 TCM (Maybe SearchBranch)
tryRefineWith Goal
goal Type
goalType SearchBranch
branch Component
comp = SearchBranch
-> Goal
-> ReaderT SearchOptions TCM (Maybe SearchBranch)
-> ReaderT SearchOptions TCM (Maybe SearchBranch)
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (ReaderT SearchOptions TCM (Maybe SearchBranch)
 -> ReaderT SearchOptions TCM (Maybe SearchBranch))
-> ReaderT SearchOptions TCM (Maybe SearchBranch)
-> ReaderT SearchOptions TCM (Maybe SearchBranch)
forall a b. (a -> b) -> a -> b
$ do

  ReaderT SearchOptions TCM (Maybe TCErr)
-> ReaderT SearchOptions TCM (Maybe TCErr, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (Type -> Type -> ReaderT SearchOptions TCM (Maybe TCErr)
dumbUnifierErr (Component -> Type
compType Component
comp) Type
goalType) ReaderT SearchOptions TCM (Maybe TCErr, LocalMetaStores)
-> ((Maybe TCErr, LocalMetaStores)
    -> ReaderT SearchOptions TCM (Maybe SearchBranch))
-> ReaderT SearchOptions TCM (Maybe SearchBranch)
forall a b.
ReaderT SearchOptions TCM a
-> (a -> ReaderT SearchOptions TCM b)
-> ReaderT SearchOptions TCM 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 TCM ()
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 TCM ()
updateStat MimerStats -> MimerStats
incRefineFail
      String -> CompId -> SM Doc -> ReaderT SearchOptions TCM ()
reportSMDoc String
"mimer.refine" CompId
50 (SM Doc -> ReaderT SearchOptions TCM ())
-> SM Doc -> ReaderT SearchOptions TCM ()
forall a b. (a -> b) -> a -> b
$ SM Doc
"Refinement failed"

      CompId -> CompId -> SM Doc -> ReaderT SearchOptions TCM ()
mimerTrace CompId
2 CompId
60 (SM Doc -> ReaderT SearchOptions TCM ())
-> SM Doc -> ReaderT SearchOptions TCM ()
forall a b. (a -> b) -> a -> b
$ [SM Doc] -> SM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ SM Doc
"Failed refinement"
        , CompId -> SM Doc -> SM Doc
forall (m :: * -> *). Functor m => CompId -> m Doc -> m Doc
nest CompId
2 (SM Doc -> SM Doc) -> SM Doc -> SM Doc
forall a b. (a -> b) -> a -> b
$ [SM Doc] -> SM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> SM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Component -> Term
compTerm Component
comp)
                       , SM Doc
":" SM Doc -> SM Doc -> SM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> SM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Component -> Type
compType Component
comp) ]
        , CompId -> SM Doc -> SM Doc
forall (m :: * -> *). Functor m => CompId -> m Doc -> m Doc
nest CompId
2 (SM Doc -> SM Doc) -> SM Doc -> SM Doc
forall a b. (a -> b) -> a -> b
$ TCErr -> SM 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 TCM (Maybe SearchBranch)
forall a. a -> ReaderT SearchOptions TCM 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 TCM Bool
-> ReaderT SearchOptions TCM (Bool, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (Type -> Type -> ReaderT SearchOptions TCM Bool
dumbUnifier (Component -> Type
compType Component
comp) Type
goalType) ReaderT SearchOptions TCM (Bool, LocalMetaStores)
-> ((Bool, LocalMetaStores) -> SM (Maybe ([MetaId], [MetaId])))
-> SM (Maybe ([MetaId], [MetaId]))
forall a b.
ReaderT SearchOptions TCM a
-> (a -> ReaderT SearchOptions TCM b)
-> ReaderT SearchOptions TCM 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 TCM 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 TCM (Maybe SearchBranch)
tryRefineAddMetas Goal
goal Type
goalType SearchBranch
branch Component
comp = SearchBranch
-> Goal
-> ReaderT SearchOptions TCM (Maybe SearchBranch)
-> ReaderT SearchOptions TCM (Maybe SearchBranch)
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (ReaderT SearchOptions TCM (Maybe SearchBranch)
 -> ReaderT SearchOptions TCM (Maybe SearchBranch))
-> ReaderT SearchOptions TCM (Maybe SearchBranch)
-> ReaderT SearchOptions TCM (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 CompId -> Component -> ReaderT SearchOptions TCM Component
applyToMetasG Maybe CompId
forall a. Maybe a
Nothing Component
comp
  branch' <- updateBranch [] branch
  tryRefineWith goal goalType branch' comp'