Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Backend.Base

Documentation

data Backend_boot (tcm :: Type -> Type) where Source #

Constructors

Backend :: forall opts (tcm :: Type -> Type) env menv mod def. NFData opts => Backend'_boot tcm opts env menv mod def -> Backend_boot tcm 

Instances

Instances details
NFData (Backend_boot tcm) Source # 
Instance details

Defined in Agda.Compiler.Backend.Base

Methods

rnf :: Backend_boot tcm -> ()

data Backend'_boot (tcm :: Type -> Type) opts env menv mod def Source #

Constructors

Backend' 

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.

Instances

Instances details
NFData opts => NFData (Backend'_boot tcm opts env menv mod def) Source # 
Instance details

Defined in Agda.Compiler.Backend.Base

Methods

rnf :: Backend'_boot tcm opts env menv mod def -> ()

Generic (Backend'_boot tcm opts env menv mod def) Source # 
Instance details

Defined in Agda.Compiler.Backend.Base

Associated Types

type Rep (Backend'_boot tcm opts env menv mod def) 
Instance details

Defined in Agda.Compiler.Backend.Base

type Rep (Backend'_boot tcm opts env menv mod def) = D1 ('MetaData "Backend'_boot" "Agda.Compiler.Backend.Base" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Backend'" 'PrefixI 'True) (((S1 ('MetaSel ('Just "backendName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "backendVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)) :*: S1 ('MetaSel ('Just "options") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 opts))) :*: (S1 ('MetaSel ('Just "commandLineFlags") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OptDescr (Flag opts)]) :*: (S1 ('MetaSel ('Just "isEnabled") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (opts -> Bool)) :*: S1 ('MetaSel ('Just "preCompile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (opts -> tcm env))))) :*: ((S1 ('MetaSel ('Just "postCompile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> IsMain -> Map TopLevelModuleName mod -> tcm ())) :*: (S1 ('MetaSel ('Just "preModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> IsMain -> TopLevelModuleName -> Maybe FilePath -> tcm (Recompile menv mod))) :*: S1 ('MetaSel ('Just "postModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> menv -> IsMain -> TopLevelModuleName -> [def] -> tcm mod)))) :*: (S1 ('MetaSel ('Just "compileDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> menv -> IsMain -> Definition -> tcm def)) :*: (S1 ('MetaSel ('Just "scopeCheckingSuffices") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "mayEraseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (QName -> tcm Bool)))))))

Methods

from :: Backend'_boot tcm opts env menv mod def -> Rep (Backend'_boot tcm opts env menv mod def) x

to :: Rep (Backend'_boot tcm opts env menv mod def) x -> Backend'_boot tcm opts env menv mod def

type Rep (Backend'_boot tcm opts env menv mod def) Source # 
Instance details

Defined in Agda.Compiler.Backend.Base

type Rep (Backend'_boot tcm opts env menv mod def) = D1 ('MetaData "Backend'_boot" "Agda.Compiler.Backend.Base" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "Backend'" 'PrefixI 'True) (((S1 ('MetaSel ('Just "backendName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "backendVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)) :*: S1 ('MetaSel ('Just "options") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 opts))) :*: (S1 ('MetaSel ('Just "commandLineFlags") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OptDescr (Flag opts)]) :*: (S1 ('MetaSel ('Just "isEnabled") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (opts -> Bool)) :*: S1 ('MetaSel ('Just "preCompile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (opts -> tcm env))))) :*: ((S1 ('MetaSel ('Just "postCompile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> IsMain -> Map TopLevelModuleName mod -> tcm ())) :*: (S1 ('MetaSel ('Just "preModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> IsMain -> TopLevelModuleName -> Maybe FilePath -> tcm (Recompile menv mod))) :*: S1 ('MetaSel ('Just "postModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> menv -> IsMain -> TopLevelModuleName -> [def] -> tcm mod)))) :*: (S1 ('MetaSel ('Just "compileDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> menv -> IsMain -> Definition -> tcm def)) :*: (S1 ('MetaSel ('Just "scopeCheckingSuffices") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "mayEraseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (QName -> tcm Bool)))))))

data Recompile menv mod Source #

Constructors

Recompile menv 
Skip mod