ToTrain

This module contains everything related to the generation of the training data.

Wrapper around Agda's typechecking monad TCMT

type C = WriterT [Sample] TCM

Additionally records/outputs training samples.

runC :: C () -> TCM [Sample]

noop :: C ()

silently :: C a -> C ()

Training data generation

type TrainF = Type -> Term -> C ()

A training function generates training data for each typed sub-term, with access to the local context via the typechecking monad.

train :: TrainF

An example training function that records a Sample (i.e. context, type, and term) for a given subterm.

forEachHole :: TrainF -> Definition -> C ()

Run the training function on each subterm of a definition.

defsToSkip :: [String]

Read a list of definitions to skip from data/defsToSkip.txt.

names :: Term -> [QName]

Gathering names from terms.

Reduction

maxDuration :: Int

The hard limit on how much time can be spent on normalising a single term.

withTimeout :: TCM a -> TCM (Maybe a)

mkReduced :: (MonadFail m, MonadTCM m, PrettyTCM a, Simplify a, Reduce a, Normalise a, Eq a) => a -> m (Reduced a)

reportReduced :: (MonadTCM m, PrettyTCM a) => Reduced a -> m ()