Main

Main driver for the agda2train executable.

Documentation

main :: IO ()

The main entrypoint for the agda2train executable.

mkBackend :: TrainF -> Backend' Options Options ([ScopeEntry], [ScopeEntry]) () (String, [Sample])

Make an Agda backend from a given training function (c.f. TrainF).

Command-line flags

data Options

Available options to configure how agda2train generates training data:

recurse

whether to recursively generate data from all transitive dependencies

noJson

mock run without generating any actual JSON files

ignoreJson

compile everything from scratch

includeDefs

whether to include definitions in scope, or just their type

includePrivs

whether to include private definitions as well

(run agda2train -h/--help for a human-readable description of all options)

Constructors

Options

Fields

• recurse, noJson, ignoreJson, printJson, includeDefs, includePrivs :: Bool
• outDir :: Maybe FilePath

Instances

Generic Options

Defined in Main

Associated Types

type Rep Options :: Type -> Type

Methods

from :: Options -> Rep Options x

to :: Rep Options x -> Options

NFData Options

Defined in Main

Methods

rnf :: Options -> ()

type Rep Options

Defined in Main

type Rep Options = D1 ('MetaData "Options" "Main" "main" 'False) (C1 ('MetaCons "Options" 'PrefixI 'True) ((S1 ('MetaSel ('Just "recurse") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "noJson") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "ignoreJson") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "printJson") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "includeDefs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "includePrivs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "outDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath))))))

defaultOptions :: Options

The default options.

recOpt :: Monad m => Options -> m Options

noJsonOpt :: Monad m => Options -> m Options

ignoreJsonOpt :: Monad m => Options -> m Options

printJsonOpt :: Monad m => Options -> m Options

includeDefsOpt :: Monad m => Options -> m Options

includePrivsOpt :: Monad m => Options -> m Options

outDirOpt :: Monad m => FilePath -> Options -> m Options

getOutDir :: Options -> FilePath

getOutFn :: Options -> String -> FilePath

JSON encoding

encode :: ToJSON a => a -> ByteString

Uses Aeson.Pretty to order the JSON fields.

encodeFile :: ToJSON a => FilePath -> a -> IO ()