{-# LANGUAGE RecordWildCards #-}

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.Functor ( ($>) )
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)
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) => QName -> tcm [QName]
getRecordFields :: forall (tcm :: * -> *). HasConstInfo 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, HasCallStack) =>
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, [Arg Term], [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 :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
qname tcm (Maybe RecordData)
-> (Maybe RecordData
    -> tcm (Maybe (QName, [Arg Term], [QName], Bool)))
-> tcm (Maybe (QName, [Arg Term], [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, [Arg Term], [QName], Bool)
-> tcm (Maybe (QName, [Arg Term], [QName], Bool))
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, [Arg Term], [QName], Bool)
forall a. Maybe a
Nothing
    Just RecordData
defn -> do
      fields <- QName -> tcm [QName]
forall (tcm :: * -> *). HasConstInfo tcm => QName -> tcm [QName]
getRecordFields QName
qname
      return $ Just (qname, argsFromElims elims, fields, recRecursive_ defn)
  Term
_ -> Maybe (QName, [Arg Term], [QName], Bool)
-> tcm (Maybe (QName, [Arg Term], [QName], Bool))
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, [Arg Term], [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 ()
assignMeta :: MetaId -> Term -> Type -> SM ()
assignMeta MetaId
metaId Term
term Type
metaType = [Phase] -> SM () -> SM ()
forall a. [Phase] -> SM a -> SM a
bench [Phase
Bench.CheckRHS] (SM () -> SM ()) -> SM () -> SM ()
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 do
      tel <- getContextTelescope
      vcat $ concat
        [ [ "Assigning" <+> pretty term ]
        , [ nest 2 $ "to" <+> pretty metaId <+> ":" <+> pretty metaType ]
        , [ nest 2 $ "in context" <+> pretty tel | not $ null tel ]
        ]

    assignV DirLeq metaId metaArgs term (AsTermsOf metaType)

getLocalVarTerms :: Int -> TCM [(Term, Dom Type)]
getLocalVarTerms :: Int -> TCM [(Term, Dom Type)]
getLocalVarTerms Int
localCxt = do
  contextTerms <- TCMT IO [Term]
forall (m :: * -> *). MonadTCEnv m => m [Term]
getContextTerms
  contextTypes <- flattenTel <$> getContextTelescope
  let inScope Int
i Dom' Term Name
_ | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
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 Int
_ (Dom' Term Name -> Name
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, MonadInteractionPoints tcm, MonadFresh NameId tcm)
  => MetaId -> tcm (Maybe Expr)
getMetaInstantiation :: forall (tcm :: * -> *).
(MonadTCM tcm, PureTCM tcm, MonadInteractionPoints tcm,
 MonadFresh NameId tcm) =>
MetaId -> tcm (Maybe Expr)
getMetaInstantiation = MetaId -> tcm (Maybe Term)
forall (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 :: (MonadDebug tcm, ReadTCState tcm) => MetaId -> tcm (Maybe Term)
metaInstantiation :: forall (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) => Type -> tcm Bool
isTypeDatatype :: forall (tcm :: * -> *). MonadTCM 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 Tele (Dom Type)
_ (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
PatternSynName           -> Bool
False   -- could consider allowing pattern synonyms, but the problem is they can't be getConstInfo'd
        KindOfName
GeneralizeName           -> Bool
False   -- and any way finding the underlying constructors should be easy
        KindOfName
DisallowedGeneralizeName -> Bool
False
        KindOfName
MacroName                -> Bool
False
        KindOfName
QuotableName             -> Bool
False
        KindOfName
ConName                  -> Bool
True
        KindOfName
CoConName                -> Bool
True
        KindOfName
FldName                  -> Bool
True
        KindOfName
DataName                 -> Bool
True
        KindOfName
RecName                  -> Bool
True
        KindOfName
FunName                  -> Bool
True
        KindOfName
AxiomName                -> Bool
True
        KindOfName
PrimName                 -> Bool
True
        KindOfName
OtherDefName             -> Bool
True
      qnames :: [QName]
qnames = (AbstractName -> QName) -> [AbstractName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> QName
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
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 :: Int -> Term -> Type -> TCM (Term, Type, [MetaId])
applyToMetas Int
skip Term
term Type
typ = do
  ctx <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
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 -> TCM (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 Int
skip Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Term
term else Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> 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 Int
localVarCount = do
  top <- (SearchOptions -> Int) -> SM Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((SearchOptions -> Int) -> SM Int)
-> (SearchOptions -> Int) -> SM Int
forall a b. (a -> b) -> a -> b
$ Context' ContextEntry -> Int
forall a. Context' a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Context' ContextEntry -> Int)
-> (SearchOptions -> Context' ContextEntry) -> SearchOptions -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
-> TCEnv -> Context' ContextEntry
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext (TCEnv -> Context' ContextEntry)
-> (SearchOptions -> TCEnv)
-> SearchOptions
-> Context' 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 -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.components.open" Int
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
<+> Int -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM (Component -> Int
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 Int m =>
[MetaId] -> Int -> Maybe Name -> Int -> Term -> Type -> m Component
newComponent [MetaId]
metaIds Int
cost Maybe Name
mName Int
pars Term
term Type
typ = m Int
forall i (m :: * -> *). MonadFresh i m => m i
fresh m Int -> (Int -> Component) -> m Component
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Int
cId -> Int
-> [MetaId]
-> Int
-> Maybe Name
-> Int
-> Term
-> Type
-> Component
mkComponent Int
cId [MetaId]
metaIds Int
cost Maybe Name
mName Int
pars Term
term Type
typ

newComponentQ :: MonadFresh CompId m => [MetaId] -> Cost -> QName -> Nat -> Term -> Type -> m Component
newComponentQ :: forall (m :: * -> *).
MonadFresh Int m =>
[MetaId] -> Int -> QName -> Int -> Term -> Type -> m Component
newComponentQ [MetaId]
metaIds Int
cost QName
qname Int
pars Term
term Type
typ = m Int
forall i (m :: * -> *). MonadFresh i m => m i
fresh m Int -> (Int -> Component) -> m Component
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Int
cId -> Int
-> [MetaId]
-> Int
-> Maybe Name
-> Int
-> Term
-> Type
-> Component
mkComponent Int
cId [MetaId]
metaIds Int
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) Int
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 :: Int -> Int -> TCM [Component]
getLocalVars Int
localCxt Int
cost = do
  typedTerms <- Int -> TCM [(Term, Dom Type)]
getLocalVarTerms Int
localCxt
  let varZeroDiscount (Var Int
0 []) = a
1
      varZeroDiscount Term
_          = a
0
  mapM (\(Term
term, Dom Type
domTyp) -> [MetaId]
-> Int -> Maybe Name -> Int -> Term -> Type -> TCMT IO Component
forall (m :: * -> *).
MonadFresh Int m =>
[MetaId] -> Int -> Maybe Name -> Int -> Term -> Type -> m Component
newComponent [] (Int
cost Int -> Int -> Int
forall a. Num a => a -> a -> a
- Term -> Int
forall {a}. Num a => Term -> a
varZeroDiscount Term
term) Maybe Name
noName Int
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

  VerboseKey -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.components" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"collectComponents"
  VerboseKey -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.components" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
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
"ii =" 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
"mDefName =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Maybe QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Maybe QName
mDefName
     , TCMT IO Doc
"whereNames =" 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]
whereNames
     , TCMT IO Doc
"metaId =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
metaId
     ]

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

  reportSDoc "mimer.components" 40 $ "recVars =" <+> pretty recVars

  -- 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 Int)]
hintRecVars = Open [(Term, NoSubst Term Int)]
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 -> Int) -> [Component] -> [Component]
forall b a. Ord b => (a -> b) -> [a] -> [a]
List.sortOn (Type -> Int
arity (Type -> Int) -> (Component -> Type) -> Component -> Int
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, HasCallStack) =>
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 -> IsWithFunction QName
funWith = IsWithFunction QName
NoWithFunction, 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 (Int -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh Int tcm) =>
Int -> QName -> tcm Component
qnameToComponent (Costs -> Int
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 => 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  = Int -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh Int tcm) =>
Int -> QName -> tcm Component
qnameToComponent (Costs -> Int
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  = Int -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh Int tcm) =>
Int -> QName -> tcm Component
qnameToComponent (Costs -> Int
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 = Int -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh Int tcm) =>
Int -> QName -> tcm Component
qnameToComponent (Costs -> Int
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     = Int -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh Int tcm) =>
Int -> QName -> tcm Component
qnameToComponent (Costs -> Int
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   = Int -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh Int tcm) =>
Int -> QName -> tcm Component
qnameToComponent (Costs -> Int
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)
  => Cost -> QName -> tcm Component
qnameToComponent :: forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh Int tcm) =>
Int -> QName -> tcm Component
qnameToComponent Int
cost QName
qname = do
  defn <- QName -> tcm Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
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 -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
mParams, Int
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 -> Int
conPars Defn
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
mParams)
        Axiom{}            -> (Term, Int)
def
        GeneralizableVar{} -> (Term, Int)
def
        f :: Defn
f@Function{}
          | Right Projection
proj <- Defn -> Either ProjectionLikenessMissing Projection
funProjection Defn
f
          , Projection -> Int
projIndex Projection
proj Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 ->
            let totalToDrop :: Int
totalToDrop = Projection -> Int
projIndex Projection
proj Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
                term :: Term
term        = QName -> Elims -> Term
Def QName
qname (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
forall a b. (a -> b) -> a -> b
$ Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
drop Int
totalToDrop [Arg Term]
mParams
                stillToDrop :: Int
stillToDrop = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int
totalToDrop Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
mParams
            in  (Term
term , Int
stillToDrop)
        Function{}         -> (Term, Int)
def
        Datatype{}         -> (Term, Int)
def
        Record{}           -> (Term, Int)
def
        Primitive{}        -> (Term, Int)
def
        PrimitiveSort{}    -> (Term, Int)
def
        DataOrRecSig{}     -> (Term, Int)
forall a. HasCallStack => a
__IMPOSSIBLE__
        AbstractDefn{}     -> (Term, Int)
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) => Cost -> tcm [Open Component]
getLetVars :: forall (tcm :: * -> *).
(MonadFresh Int tcm, MonadTCM tcm) =>
Int -> tcm [Open Component]
getLetVars Int
cost = do
  bindings <- Lens' TCEnv (Map Name (Open LetBinding))
-> tcm (Map Name (Open LetBinding))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings
  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 Int
forall i (m :: * -> *). MonadFresh i m => m i
fresh
      return $ opn <&> \ (LetBinding IsAxiom
_isAxiom Origin
_origin Term
term Dom Type
typ) ->
                Int
-> [MetaId]
-> Int
-> Maybe Name
-> Int
-> Term
-> Type
-> Component
mkComponent Int
cId [] Int
cost (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name) Int
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 Int)])
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 Int)] -> tcm (Open [(Term, Maybe Int)])
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen []
    IPClause{ipcQName :: IPClause -> QName
ipcQName = QName
fnName, ipcClauseNo :: IPClause -> Int
ipcClauseNo = Int
clauseNr} -> do
      VerboseKey -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.components" Int
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
      VerboseKey -> Int -> TCMT IO Doc -> tcm ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.components" Int
45 (TCMT IO Doc -> tcm ()) -> TCMT IO Doc -> tcm ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
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
"fnName =" 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
fnName
        , TCMT IO Doc
"clauseNr =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
clauseNr
        ]
      info <- QName -> tcm Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
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] -> Int -> Clause
forall a. HasCallStack => [a] -> Int -> a
!! Int
clauseNr
              naps :: NAPs
naps = Clause -> NAPs
namedClausePats Clause
clause

          -- Telescope at interaction point
          iTel <- tcm (Tele (Dom Type))
forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
getContextTelescope
          -- Telescope for the body of the clause
          let cTel = Clause -> Tele (Dom Type)
clauseTel Clause
clause
          -- HACK: To get the correct indices, we shift by the difference in telescope lengths
          let shift = [Arg VerboseKey] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Tele (Dom Type) -> [Arg VerboseKey]
forall a. TelToArgs a => a -> [Arg VerboseKey]
telToArgs Tele (Dom Type)
iTel) Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Arg VerboseKey] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Tele (Dom Type) -> [Arg VerboseKey]
forall a. TelToArgs a => a -> [Arg VerboseKey]
telToArgs Tele (Dom Type)
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 Int)] -> tcm (Open [(Term, Maybe Int)])
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen []
  where
    go :: Bool -> DeBruijnPattern -> [(Int, Bool)]
go Bool
isUnderCon = \case
      VarP PatternInfo
patInf DBPatVar
x -> [(DBPatVar -> Int
dbPatVarIndex DBPatVar
x, Bool
isUnderCon)]
      DotP PatternInfo
patInf Term
t -> [] -- Ignore dot patterns
      ConP ConHead
conHead ConPatternInfo
conPatInf NAPs
namedArgs -> (NamedArg DeBruijnPattern -> [(Int, Bool)])
-> NAPs -> [(Int, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> DeBruijnPattern -> [(Int, Bool)]
go Bool
True (DeBruijnPattern -> [(Int, Bool)])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [(Int, 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 :: [Arg Term] -> Component -> QName -> SM Component
applyProj [Arg Term]
recordArgs Component
comp' QName
qname = do
  cost <- (SearchOptions -> Int) -> SM Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> Int
costProj (Costs -> Int) -> (SearchOptions -> Costs) -> SearchOptions -> Int
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
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 Int -> Component -> SM Component
applyToMetasG (Just Int
m) Component
comp | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Component -> SM Component
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Component
comp
applyToMetasG Maybe Int
maxArgs Component
comp = do
  VerboseKey -> Int -> TCMT IO Doc -> SM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.component" Int
25 (TCMT IO Doc -> SM ()) -> TCMT IO Doc -> SM ()
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
<+> Int -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM (Component -> Int
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 (Tele (Dom Type))
forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
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 -> Int
compPars Component
comp
          newTerm | Int
skip Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0  = Component -> Term
compTerm Component
comp
                  | Bool
otherwise = Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> 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) <- TCM (MetaId, Term) -> SM (MetaId, Term)
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 (TCM (MetaId, Term) -> SM (MetaId, Term))
-> TCM (MetaId, Term) -> SM (MetaId, Term)
forall a b. (a -> b) -> a -> b
$ RunMetaOccursCheck -> Comparison -> Type -> TCM (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 -> SM ()
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 -> Int -> TCMT IO Doc -> SM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer.env" Int
70 (TCMT IO Doc -> SM ()) -> TCMT IO Doc -> SM ()
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, MonadTrace 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 Int
sbComponentsUsed SearchBranch
branch
  (deltaCost, compsUsed') <- case mComp of
        Maybe Component
Nothing -> (Int, Map Name Int)
-> ReaderT SearchOptions TCM (Int, Map Name Int)
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
0, Map Name Int
compsUsed)
        Just Component
comp -> do
          case Component -> Maybe Name
compName Component
comp of
            Maybe Name
Nothing -> (Int, Map Name Int)
-> ReaderT SearchOptions TCM (Int, Map Name Int)
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Component -> Int
compCost Component
comp, Map Name Int
compsUsed)
            Just Name
name -> case Map Name Int
compsUsed Map Name Int -> Name -> Maybe Int
forall k a. Ord k => Map k a -> k -> Maybe a
Map.!? Name
name of
              Maybe Int
Nothing -> (Int, Map Name Int)
-> ReaderT SearchOptions TCM (Int, Map Name Int)
forall a. a -> ReaderT SearchOptions TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Component -> Int
compCost Component
comp, Name -> Int -> Map Name Int -> Map Name Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
name Int
1 Map Name Int
compsUsed)
              Just Int
uses -> do
                reuseCost <- (SearchOptions -> Int -> Int)
-> ReaderT SearchOptions TCM (Int -> Int)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> Int -> Int
costCompReuse (Costs -> Int -> Int)
-> (SearchOptions -> Costs) -> SearchOptions -> Int -> Int
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 -> Int -> TCMT IO Doc -> SM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer" Int
20 (TCMT IO Doc -> SM ()) -> TCMT IO Doc -> SM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking if branch is solved"
  VerboseKey -> Int -> TCMT IO Doc -> SM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"mimer" Int
30 (TCMT IO Doc -> SM ()) -> TCMT IO Doc -> SM ()
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
      VerboseKey -> Int -> VerboseKey -> SM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"mimer.search" Int
45 VerboseKey
"partitionStepResult: render ResultExpr"
      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 ()
dumbUnifier :: Type -> Type -> SM ()
dumbUnifier Type
t1 Type
t2 = [Phase] -> SM () -> SM ()
forall a. [Phase] -> SM a -> SM a
bench [Phase
Bench.UnifyIndices] (SM () -> SM ()) -> SM () -> SM ()
forall a b. (a -> b) -> a -> b
$ do
  (MimerStats -> MimerStats) -> SM ()
updateStat MimerStats -> MimerStats
incTypeEqChecks
  SM () -> SM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCMT IO () -> SM ()
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 () -> SM ()) -> TCMT IO () -> SM ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCMT IO ()
equalType Type
t2 Type
t1)

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

reportSMDoc :: VerboseKey -> VerboseLevel -> SM Doc -> SM ()
reportSMDoc :: VerboseKey -> Int -> ReaderT SearchOptions TCM Doc -> SM ()
reportSMDoc VerboseKey
vk Int
vl ReaderT SearchOptions TCM Doc
md = VerboseKey -> Int -> TCMT IO Doc -> SM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
vk Int
vl (TCMT IO Doc -> SM ())
-> (SearchOptions -> TCMT IO Doc) -> SearchOptions -> SM ()
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 -> SM ())
-> ReaderT SearchOptions TCM SearchOptions -> SM ()
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 :: Int -> Int -> ReaderT SearchOptions TCM Doc -> SM ()
mimerTrace Int
ilvl Int
vlvl ReaderT SearchOptions TCM Doc
doc = VerboseKey -> Int -> ReaderT SearchOptions TCM Doc -> SM ()
reportSMDoc VerboseKey
"mimer.trace" Int
vlvl (ReaderT SearchOptions TCM Doc -> SM ())
-> ReaderT SearchOptions TCM Doc -> SM ()
forall a b. (a -> b) -> a -> b
$ Int
-> ReaderT SearchOptions TCM Doc -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
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, 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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Elims)
-> ReaderT SearchOptions TCM [Arg Term]
-> ReaderT SearchOptions TCM Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT SearchOptions TCM [Arg Term]
forall (m :: * -> *). MonadTCEnv m => m [Arg Term]
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
<+> Int -> ReaderT SearchOptions TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchBranch -> Int
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 Int
forall {m :: * -> *}. MonadDebug m => VerboseKey -> m Int
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 Int
uses = Int
compReuse Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
uses Int -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
2
  pure Costs{..}
  where
    cost :: VerboseKey -> m Int
cost VerboseKey
key = VerboseKey -> m Int
forall {m :: * -> *}. MonadDebug m => VerboseKey -> m Int
getVerbosityLevel (VerboseKey
"mimer-cost." VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
key)

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

updateStat :: (MimerStats -> MimerStats) -> SM ()
updateStat :: (MimerStats -> MimerStats) -> SM ()
updateStat MimerStats -> MimerStats
f = VerboseKey -> Int -> SM () -> SM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> m () -> m ()
verboseS VerboseKey
"mimer.stats" Int
10 (SM () -> SM ()) -> SM () -> SM ()
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 :: [Bench.Phase] -> SM a -> SM a
bench :: forall 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 -> Maybe RangeFile
rangeFile (Range -> Maybe RangeFile)
-> (InteractionPoint -> Range)
-> InteractionPoint
-> Maybe RangeFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Range
ipRange (InteractionPoint -> Maybe RangeFile)
-> m InteractionPoint -> m (Maybe RangeFile)
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
    Maybe RangeFile
SMaybe.Nothing ->
      VerboseKey -> Int -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> VerboseKey -> m ()
reportSLn VerboseKey
"mimer.stats" Int
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 (Int -> VerboseKey
forall a. Show a => a -> VerboseKey
show (InteractionId -> Int
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")