Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Mimer.Monad

Synopsis

Documentation

type SM a = ReaderT SearchOptions TCM a Source #

Agda internals

getRecordFields :: (HasConstInfo tcm, MonadTCM tcm) => QName -> tcm [QName] Source #

getRecordInfo :: (MonadTCM tcm, HasConstInfo tcm) => Type -> tcm (Maybe (QName, Args, [QName], Bool)) Source #

allOpenMetas :: (AllMetas t, ReadTCState tcm) => t -> tcm [MetaId] Source #

assignMeta :: MetaId -> Term -> Type -> SM [MetaId] Source #

getLocalVarTerms :: Int -> TCM [(Term, Dom Type)] Source #

getMetaInstantiation :: (MonadTCM tcm, PureTCM tcm, MonadDebug tcm, MonadInteractionPoints tcm, MonadFresh NameId tcm) => MetaId -> tcm (Maybe Expr) Source #

metaInstantiation :: (MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) => MetaId -> tcm (Maybe Term) Source #

isTypeDatatype :: (MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) => Type -> tcm Bool Source #

endsInLevelTester :: TCM (Type -> Bool) Source #

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.

getEverythingInScope :: MetaVariable -> [QName] Source #

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

applyToMetas :: Nat -> Term -> Type -> TCM (Term, Type, [MetaId]) Source #

Components

localVarCount :: SM Int Source #

getOpenComponent :: (MonadTCM tcm, MonadDebug tcm) => Open Component -> tcm Component Source #

newComponent :: MonadFresh CompId m => [MetaId] -> Cost -> Maybe Name -> Nat -> Term -> Type -> m Component Source #

newComponentQ :: MonadFresh CompId m => [MetaId] -> Cost -> QName -> Nat -> Term -> Type -> m Component Source #

getLocalVars :: Int -> Cost -> TCM [Component] Source #

collectComponents :: Options -> Costs -> InteractionId -> Maybe QName -> [QName] -> MetaId -> TCM BaseComponents Source #

NOTE: Collects components from the *current* context, not the context of the InteractionId.

qnameToComponent :: (HasConstInfo tcm, ReadTCState tcm, MonadFresh CompId tcm, MonadTCM tcm) => Cost -> QName -> tcm Component Source #

getLetVars :: (MonadFresh CompId tcm, MonadTCM tcm, Monad tcm) => Cost -> tcm [Open Component] Source #

Turn the let bindings of the current TCEnv into components.

collectLHSVars :: (ReadTCState tcm, MonadError TCErr tcm, MonadTCM tcm, HasConstInfo tcm) => InteractionId -> tcm (Open [(Term, Maybe Int)]) Source #

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.

declarationQnames :: Declaration -> [QName] Source #

applyProj :: Args -> Component -> QName -> SM Component Source #

applyToMetasG Source #

Arguments

:: Maybe Nat

Max number of arguments to apply.

-> Component 
-> SM Component 

createMeta :: Type -> SM (MetaId, Term) Source #

Search branches

startSearchBranch :: [MetaId] -> TCM SearchBranch Source #

withBranchState :: SearchBranch -> SM a -> SM a Source #

withBranchAndGoal :: SearchBranch -> Goal -> SM a -> SM a Source #

inGoalEnv :: Goal -> SM a -> SM a Source #

updateBranch' :: Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch Source #

updateBranch :: [MetaId] -> SearchBranch -> SM SearchBranch Source #

updateBranchCost :: Component -> [MetaId] -> SearchBranch -> SM SearchBranch Source #

checkSolved :: SearchBranch -> SM SearchStepResult Source #

normaliseSolution :: Term -> SM Term Source #

partitionStepResult :: [SearchStepResult] -> SM ([SearchBranch], [MimerResult]) Source #

Search options

makeSearchOptions :: Rewrite -> Options -> InteractionId -> TCM SearchOptions Source #

Unification

dumbUnifier :: Type -> Type -> SM Bool Source #

dumbUnifierErr :: Type -> Type -> SM (Maybe TCErr) Source #

Debugging

reportSMDoc :: VerboseKey -> VerboseLevel -> SM Doc -> SM () Source #

mimerTrace :: Int -> VerboseLevel -> SM Doc -> SM () Source #

topInstantiationDoc :: SM Doc Source #

prettyGoalInst :: Goal -> SM Doc Source #

branchInstantiationDocCost :: SearchBranch -> SM Doc Source #

branchInstantiationDoc :: SearchBranch -> SM Doc Source #

For debug

prettyBranch :: SearchBranch -> SM String Source #

customCosts :: TCM Costs Source #

Stats

updateStat :: (MimerStats -> MimerStats) -> SM () Source #

bench :: NFData a => [Phase] -> SM a -> SM a Source #

writeTime :: (ReadTCState m, MonadError TCErr m, MonadTCM m, MonadDebug m) => InteractionId -> CPUTime -> m () Source #