module Agda.Mimer.Monad where

import Control.DeepSeq (NFData(..))
import Control.Monad
import Control.Monad.Except (catchError, MonadError)
import Control.Monad.IO.Class (liftIO)
import Control.Monad.Reader (ReaderT(..), asks, ask, lift)
import Data.IORef (modifyIORef', newIORef)
import Data.Map qualified as Map
import Data.List qualified as List
import Data.List.NonEmpty qualified as NonEmptyList (head)
import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty qualified as P
import Agda.Syntax.Internal
import Agda.Syntax.Position (rangeFile, rangeFilePath)
import Agda.Syntax.Concrete.Name qualified as C
import Agda.Syntax.Abstract (Expr)
import Agda.Syntax.Abstract qualified as A
import Agda.Syntax.Abstract.Views qualified as A
import Agda.Syntax.Internal.MetaVars (AllMetas(..))
import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete_)
import Agda.Syntax.Translation.InternalToAbstract (reify, blankNotInScope)
import Agda.Syntax.Scope.Base qualified as Scope
import Agda.TypeChecking.Monad
import Agda.TypeChecking.MetaVars (newValueMeta)
import Agda.TypeChecking.Primitive (getBuiltinName)
import Agda.TypeChecking.Datatypes (isDataOrRecord)
import Agda.TypeChecking.Reduce (reduce, instantiateFull, instantiate)
import Agda.TypeChecking.Records (isRecord)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Conversion (equalType)
import Agda.TypeChecking.Constraints (noConstraints)
import Agda.TypeChecking.Telescope (flattenTel, piApplyM)
import Agda.TypeChecking.Substitute (pattern TelV, telView', piApply, apply, applyE, NoSubst(..))
import Agda.Interaction.BasicOps (normalForm)
import Agda.Interaction.Base (Rewrite(..))
import Agda.Benchmarking qualified as Bench
import Agda.Utils.Benchmark (billTo)
import Agda.Utils.Functor ((<&>), (<.>))
import Agda.Utils.FileName (filePath)
import Agda.Utils.Impossible
import Agda.Utils.Monad (ifM)
import Agda.Utils.Maybe.Strict qualified as SMaybe
import Agda.Utils.Time (CPUTime(..))

import Agda.Mimer.Options
import Agda.Mimer.Types

type SM a = ReaderT SearchOptions TCM a

------------------------------------------------------------------------
-- * Agda internals
------------------------------------------------------------------------

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

getRecordInfo :: (MonadTCM tcm, HasConstInfo tcm) => Type
              -> tcm (Maybe ( QName     -- Record name
                           , Args      -- Record parameters converted to (hidden) arguments
                           , [QName]   -- Field names
                           , Bool      -- Is recursive?
                           ))
getRecordInfo :: forall (tcm :: * -> *).
(MonadTCM tcm, HasConstInfo tcm) =>
Type -> tcm (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 -> tcm (Maybe RecordData)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
qname tcm (Maybe RecordData)
-> (Maybe RecordData -> tcm (Maybe (QName, Args, [QName], Bool)))
-> tcm (Maybe (QName, Args, [QName], Bool))
forall a b. tcm a -> (a -> tcm b) -> tcm b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe RecordData
Nothing -> Maybe (QName, Args, [QName], Bool)
-> tcm (Maybe (QName, Args, [QName], Bool))
forall a. a -> tcm 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 -> tcm [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)
-> tcm (Maybe (QName, Args, [QName], Bool))
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args, [QName], Bool)
forall a. Maybe a
Nothing

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 `List.intersect` openMetas

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 TCM ()
-> ReaderT SearchOptions TCM ((), LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (ReaderT SearchOptions TCM ()
 -> ReaderT SearchOptions TCM ((), LocalMetaStores))
-> ReaderT SearchOptions TCM ()
-> ReaderT SearchOptions TCM ((), LocalMetaStores)
forall a b. (a -> b) -> a -> b
$ do
    metaVar <- MetaId -> ReaderT SearchOptions TCM 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
      VerboseKey
-> VerboseLevel
-> ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM ()
reportSMDoc VerboseKey
"mimer.assignMeta" VerboseLevel
30 (ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM ())
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM ()
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions TCM Doc] -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ ReaderT SearchOptions TCM Doc
"Got error from assignV:" ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCErr -> ReaderT SearchOptions TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err
        , VerboseLevel
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc)
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions TCM Doc] -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ ReaderT SearchOptions TCM Doc
"when trying to assign" ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> ReaderT SearchOptions TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
term
          , ReaderT SearchOptions TCM Doc
"to" ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> ReaderT SearchOptions TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
metaId ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ReaderT SearchOptions TCM Doc
":" ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> ReaderT SearchOptions TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
metaType
          , ReaderT SearchOptions TCM Doc
"in context" ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc)
-> (Telescope -> ReaderT SearchOptions TCM Doc)
-> Telescope
-> ReaderT SearchOptions TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ReaderT SearchOptions TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> ReaderT SearchOptions TCM Doc)
-> ReaderT SearchOptions TCM Telescope
-> ReaderT SearchOptions TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT SearchOptions TCM 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

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 -> TCMT IO 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 ]

-- 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 = TCMT IO 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) -> TCMT IO 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

-- | 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

-- | 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

-- 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 -> TCM (Term, Type, [MetaId])
applyToMetas :: VerboseLevel -> Term -> Type -> TCM (Term, Type, [MetaId])
applyToMetas VerboseLevel
skip Term
term Type
typ = do
  ctx <- 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) <- RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (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 <- 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 (max 0 $ skip - 1) newTerm newType
      return (term', typ', metaId' : metas)
    Term
_ -> (Term, Type, [MetaId]) -> TCM (Term, Type, [MetaId])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
term, Type
typ, [])

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

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

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
  VerboseKey -> VerboseLevel -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
    }

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

-- 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 -> TCM [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

-- | 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 ]

  -- 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
        }

  -- 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 List.\\ 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
    }
  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]
List.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] -> 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 (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] -> TCM [Component]) -> TCMT IO [QName] -> TCM [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}


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)

-- | 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)

-- | 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
      VerboseKey -> VerboseLevel -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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 VerboseKey] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Telescope -> [Arg VerboseKey]
forall a. TelToArgs a => a -> [Arg VerboseKey]
telToArgs Telescope
iTel) VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- [Arg VerboseKey] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Telescope -> [Arg VerboseKey]
forall a. TelToArgs a => a -> [Arg VerboseKey]
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 ]

applyProj :: Args -> Component -> QName -> SM Component
applyProj :: Args -> Component -> QName -> SM 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 -> SM Component
applyToMetasG (Just VerboseLevel
m) Component
comp | VerboseLevel
m VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
0 = Component -> SM Component
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Component
comp
applyToMetasG Maybe VerboseLevel
maxArgs Component
comp = do
  VerboseKey
-> VerboseLevel -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.component" VerboseLevel
25 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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 TCM 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
      let predNat a
n | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0     = a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1
                    | a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0    = a
0
                    | Bool
otherwise = a
forall a. HasCallStack => a
__IMPOSSIBLE__
      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 -> SM Component
forall a. a -> ReaderT SearchOptions TCM 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)

------------------------------------------------------------------------
-- * Search branches
------------------------------------------------------------------------

startSearchBranch :: [MetaId] -> TCM SearchBranch
startSearchBranch :: [MetaId] -> TCM SearchBranch
startSearchBranch [MetaId]
metaIds = do
  state <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  pure SearchBranch
        { sbTCState        = state
        , sbGoals          = map Goal metaIds
        , sbCost           = 0
        , sbCache          = Map.empty
        , sbComponentsUsed = Map.empty
        }

withBranchState :: SearchBranch -> SM a -> SM a
withBranchState :: forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
br SM a
ma = do
  TCState -> ReaderT SearchOptions TCM ()
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
  VerboseKey
-> VerboseLevel -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.env" VerboseLevel
70 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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

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 TCM 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 TCM (VerboseLevel, Map Name VerboseLevel)
forall a. a -> ReaderT SearchOptions TCM 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 TCM (VerboseLevel, Map Name VerboseLevel)
forall a. a -> ReaderT SearchOptions TCM 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 TCM (VerboseLevel, Map Name VerboseLevel)
forall a. a -> ReaderT SearchOptions TCM 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 TCM (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)

checkSolved :: SearchBranch -> SM SearchStepResult
checkSolved :: SearchBranch -> SM SearchStepResult
checkSolved SearchBranch
branch = do
  VerboseKey
-> VerboseLevel -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer" VerboseLevel
20 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking if branch is solved"
  VerboseKey
-> VerboseLevel -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer" VerboseLevel
30 (TCMT IO Doc -> ReaderT SearchOptions TCM ())
-> TCMT IO Doc -> ReaderT SearchOptions TCM ()
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 TCM 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 TCM Expr -> SM SearchStepResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> ReaderT SearchOptions TCM Expr
forall (m :: * -> *) a.
(MonadTCEnv m, MonadDebug m, BlankVars a) =>
a -> m a
blankNotInScope (Expr -> ReaderT SearchOptions TCM Expr)
-> ReaderT SearchOptions TCM Expr -> ReaderT SearchOptions TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> ReaderT SearchOptions TCM (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 -> SM SearchStepResult
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (SearchStepResult -> SM SearchStepResult)
-> SearchStepResult -> SM SearchStepResult
forall a b. (a -> b) -> a -> b
$ SearchBranch -> SearchStepResult
OpenBranch SearchBranch
branch { sbGoals = goals }

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

partitionStepResult :: [SearchStepResult] -> SM ([SearchBranch], [MimerResult])
partitionStepResult :: [SearchStepResult] -> SM ([SearchBranch], [MimerResult])
partitionStepResult [] = ([SearchBranch], [MimerResult])
-> SM ([SearchBranch], [MimerResult])
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([],[])
partitionStepResult (SearchStepResult
x:[SearchStepResult]
xs) = do
  let rest :: SM ([SearchBranch], [MimerResult])
rest = [SearchStepResult] -> SM ([SearchBranch], [MimerResult])
partitionStepResult [SearchStepResult]
xs
  (brs',sols) <- SM ([SearchBranch], [MimerResult])
rest
  case x of
    SearchStepResult
NoSolution -> SM ([SearchBranch], [MimerResult])
rest
    OpenBranch SearchBranch
br -> ([SearchBranch], [MimerResult])
-> SM ([SearchBranch], [MimerResult])
forall a. a -> ReaderT SearchOptions TCM 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 -> VerboseKey
forall a. Doc a -> VerboseKey
P.render (Doc -> VerboseKey)
-> ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM VerboseKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ReaderT SearchOptions TCM 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)

------------------------------------------------------------------------
-- * Search options
------------------------------------------------------------------------

makeSearchOptions :: Rewrite
                  -> Options
                  -> InteractionId
                  -> TCM SearchOptions
makeSearchOptions :: Rewrite -> Options -> InteractionId -> TCM SearchOptions
makeSearchOptions Rewrite
norm Options
options InteractionId
ii = do
  metaId <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  (mTheFunctionQName, whereNames) <- fmap ipClause (lookupInteractionPoint ii) <&> \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

  env <- askTC
  costs <- ifM (hasVerbosity "mimer.cost.custom" 10)
             {- then -} customCosts
             {- else -} (return defaultCosts)
  reportSDoc "mimer.cost.custom" 10 $ "Using costs:" $$ nest 2 (pretty costs)
  components <- collectComponents options costs ii mTheFunctionQName whereNames metaId
  statsRef   <- liftIO $ newIORef emptyMimerStats
  checkpoint <- viewTC eCurrentCheckpoint
  mflat      <- getBuiltinName BuiltinFlat
  pure SearchOptions
        { searchBaseComponents         = components
        , searchHintMode               = optHintMode options
        , searchTimeout                = optTimeout options
        , searchGenProjectionsLocal    = True
        , searchGenProjectionsLet      = True
        , searchGenProjectionsExternal = False
        , searchGenProjectionsRec      = True
        , searchSpeculateProjections   = True
        , searchTopMeta                = metaId
        , searchTopEnv                 = env
        , searchTopCheckpoint          = checkpoint
        , searchInteractionId          = ii
        , searchFnName                 = mTheFunctionQName
        , searchCosts                  = costs
        , searchStats                  = statsRef
        , searchRewrite                = norm
        , searchBuiltinFlat            = mflat
        }

------------------------------------------------------------------------
-- * Unification
------------------------------------------------------------------------

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

dumbUnifierErr :: Type -> Type -> SM (Maybe TCErr)
dumbUnifierErr :: Type -> Type -> ReaderT SearchOptions TCM (Maybe TCErr)
dumbUnifierErr Type
t1 Type
t2 = [Phase]
-> ReaderT SearchOptions TCM (Maybe TCErr)
-> ReaderT SearchOptions TCM (Maybe TCErr)
forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase
Bench.UnifyIndices] (ReaderT SearchOptions TCM (Maybe TCErr)
 -> ReaderT SearchOptions TCM (Maybe TCErr))
-> ReaderT SearchOptions TCM (Maybe TCErr)
-> ReaderT SearchOptions TCM (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ do
  (MimerStats -> MimerStats) -> ReaderT SearchOptions TCM ()
updateStat MimerStats -> MimerStats
incTypeEqChecks
  ReaderT SearchOptions TCM (Maybe TCErr)
-> ReaderT SearchOptions TCM (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 TCM ()
-> ReaderT SearchOptions TCM (Maybe TCErr)
forall a b.
a -> ReaderT SearchOptions TCM b -> ReaderT SearchOptions TCM a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type -> Type -> ReaderT SearchOptions TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t2 Type
t1) ReaderT SearchOptions TCM (Maybe TCErr)
-> (TCErr -> ReaderT SearchOptions TCM (Maybe TCErr))
-> ReaderT SearchOptions TCM (Maybe TCErr)
forall a.
ReaderT SearchOptions TCM a
-> (TCErr -> ReaderT SearchOptions TCM a)
-> ReaderT SearchOptions TCM a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> do
    VerboseKey
-> VerboseLevel -> TCMT IO Doc -> ReaderT SearchOptions TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.unify" VerboseLevel
80 (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
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 TCM (Maybe TCErr)
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TCErr -> ReaderT SearchOptions TCM (Maybe TCErr))
-> Maybe TCErr -> ReaderT SearchOptions TCM (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ TCErr -> Maybe TCErr
forall a. a -> Maybe a
Just TCErr
err

------------------------------------------------------------------------
-- * Debugging
------------------------------------------------------------------------

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

mimerTrace :: Int -> VerboseLevel -> SM Doc -> SM ()
mimerTrace :: VerboseLevel
-> VerboseLevel
-> ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM ()
mimerTrace VerboseLevel
ilvl VerboseLevel
vlvl ReaderT SearchOptions TCM Doc
doc = VerboseKey
-> VerboseLevel
-> ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM ()
reportSMDoc VerboseKey
"mimer.trace" VerboseLevel
vlvl (ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM ())
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM 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 TCM Doc -> ReaderT SearchOptions TCM Doc)
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall a b. (a -> b) -> a -> b
$ ReaderT SearchOptions TCM Doc
"-" ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ReaderT SearchOptions TCM Doc
doc

topInstantiationDoc :: SM Doc
topInstantiationDoc :: ReaderT SearchOptions TCM Doc
topInstantiationDoc = (SearchOptions -> MetaId) -> ReaderT SearchOptions TCM MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> MetaId
searchTopMeta ReaderT SearchOptions TCM MetaId
-> (MetaId -> ReaderT SearchOptions TCM (Maybe Expr))
-> ReaderT SearchOptions TCM (Maybe Expr)
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
>>= MetaId -> ReaderT SearchOptions TCM (Maybe Expr)
forall (tcm :: * -> *).
(MonadTCM tcm, PureTCM tcm, MonadDebug tcm,
 MonadInteractionPoints tcm, MonadFresh NameId tcm) =>
MetaId -> tcm (Maybe Expr)
getMetaInstantiation ReaderT SearchOptions TCM (Maybe Expr)
-> (Maybe Expr -> ReaderT SearchOptions TCM Doc)
-> ReaderT SearchOptions TCM Doc
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
>>= ReaderT SearchOptions TCM Doc
-> (Expr -> ReaderT SearchOptions TCM Doc)
-> Maybe Expr
-> ReaderT SearchOptions TCM Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Doc -> ReaderT SearchOptions TCM Doc
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
"(nothing)") Expr -> ReaderT SearchOptions TCM 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 TCM Doc
prettyGoalInst Goal
goal = Goal
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall a. Goal -> SM a -> SM a
inGoalEnv Goal
goal (ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc)
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM 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 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
  prettyTCM =<< instantiate (MetaV (goalMeta goal) args)

branchInstantiationDocCost :: SearchBranch -> SM Doc
branchInstantiationDocCost :: SearchBranch -> ReaderT SearchOptions TCM Doc
branchInstantiationDocCost SearchBranch
branch = SearchBranch -> ReaderT SearchOptions TCM Doc
branchInstantiationDoc SearchBranch
branch ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (ReaderT SearchOptions TCM Doc
"cost:" ReaderT SearchOptions TCM Doc
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> ReaderT SearchOptions TCM 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 TCM Doc
branchInstantiationDoc SearchBranch
branch = SearchBranch
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
branch ReaderT SearchOptions TCM Doc
topInstantiationDoc

prettyBranch :: SearchBranch -> SM String
prettyBranch :: SearchBranch -> ReaderT SearchOptions TCM VerboseKey
prettyBranch SearchBranch
branch = SearchBranch
-> ReaderT SearchOptions TCM VerboseKey
-> ReaderT SearchOptions TCM VerboseKey
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
branch (ReaderT SearchOptions TCM VerboseKey
 -> ReaderT SearchOptions TCM VerboseKey)
-> ReaderT SearchOptions TCM VerboseKey
-> ReaderT SearchOptions TCM VerboseKey
forall a b. (a -> b) -> a -> b
$ do
    metaId <- (SearchOptions -> MetaId) -> ReaderT SearchOptions TCM 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)
      ])

-- Hack to let you experiment with costs using verbosity flags.
customCosts :: TCM Costs
customCosts :: TCMT IO Costs
customCosts = do
  costLocal         <- VerboseKey -> TCM VerboseLevel
forall {m :: * -> *}. MonadDebug m => VerboseKey -> m VerboseLevel
cost VerboseKey
"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 :: VerboseKey -> m VerboseLevel
cost VerboseKey
key = VerboseKey -> m VerboseLevel
forall {m :: * -> *}. MonadDebug m => VerboseKey -> m VerboseLevel
getVerbosityLevel (VerboseKey
"mimer-cost." VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
key)

------------------------------------------------------------------------
-- * Stats
------------------------------------------------------------------------

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

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 TCM)) -> 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

writeTime :: (ReadTCState m, MonadError TCErr m, MonadTCM m, MonadDebug m)
          => InteractionId
          -> CPUTime
          -> m ()
writeTime :: forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCM m, MonadDebug m) =>
InteractionId -> CPUTime -> m ()
writeTime InteractionId
ii (CPUTime Integer
time) = do
  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 ->
      VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"mimer.stats" VerboseLevel
2 VerboseKey
"No file found for interaction id"
    SMaybe.Just RangeFile
file -> do
      let path :: VerboseKey
path = AbsolutePath -> VerboseKey
filePath (RangeFile -> AbsolutePath
rangeFilePath RangeFile
file) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
".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
$ VerboseKey -> VerboseKey -> IO ()
appendFile VerboseKey
path (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (InteractionId -> VerboseLevel
interactionId InteractionId
ii) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Integer -> VerboseKey
forall a. Show a => a -> VerboseKey
show Integer
time VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n")