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

Agda.Compiler.MAlonzo.Pragmas

Synopsis

Documentation

data HaskellPragma Source #

GHC backend translation pragmas.

Constructors

HsDefn Range HaskellCode 
HsType Range HaskellType 
HsData Range HaskellType [HaskellCode]

@COMPILE GHC X = data D (c₁ | ... | cₙ)

HsExport Range HaskellCode
COMPILE GHC x as f

foreignHaskell :: TCM ([String], [String], [String]) Source #

Get content of FOREIGN GHC pragmas, sorted by KindOfForeignCode: file header pragmas, import statements, rest.

data KindOfForeignCode Source #

Classify FOREIGN Haskell code.

Constructors

ForeignFileHeaderPragma

A pragma that must appear before the module header.

ForeignImport

An import statement. Must appear right after the module header.

ForeignOther

The rest. To appear after the import statements.

classifyForeign :: String -> KindOfForeignCode Source #

Classify a FOREIGN GHC declaration.

classifyPragma :: String -> KindOfForeignCode Source #

Classify a Haskell pragma into whether it is a file header pragma or not.

partitionByKindOfForeignCode :: (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a]) Source #

Partition a list by KindOfForeignCode attribute.