Documentation

Fields

• backendName :: String
   
• backendVersion :: Maybe String

  Optional version information to be printed with --version.

• options :: opts

  Default options

• commandLineFlags :: [OptDescr (Flag opts)]

  Backend-specific command-line flags. Should at minimum contain a flag to enable the backend.

• isEnabled :: opts -> Bool

  Unless the backend has been enabled, runAgda will fall back to vanilla Agda behaviour.

• preCompile :: opts -> tcm env

  Called after type checking completes, but before compilation starts.

• postCompile :: env -> IsMain -> Map TopLevelModuleName mod -> tcm ()

  Called after module compilation has completed. The IsMain argument is NotMain if the --no-main flag is present.

• preModule :: env -> IsMain -> TopLevelModuleName -> Maybe FilePath -> tcm (Recompile menv mod)

  Called before compilation of each module. Gets the path to the .agdai file to allow up-to-date checking of previously written compilation results. Should return Skip m if compilation is not required. Will be Nothing if only scope checking.

• postModule :: env -> menv -> IsMain -> TopLevelModuleName -> [def] -> tcm mod

  Called after all definitions of a module have been compiled.

• compileDef :: env -> menv -> IsMain -> Definition -> tcm def

  Compile a single definition.

• scopeCheckingSuffices :: Bool

  True if the backend works if --only-scope-checking is used.

• mayEraseType :: QName -> tcm Bool

  The treeless compiler may ask the Backend if elements of the given type maybe possibly erased. The answer should be False if the compilation of the type is used by a third party, e.g. in a FFI binding.