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

Agda.Compiler.MAlonzo.Pragmas

Synopsis

Documentation

type HaskellCode = String Source #

type HaskellType = String Source #

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

Instances

Instances details
Pretty HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

HasRange HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

Show HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

showsPrec :: Int -> HaskellPragma -> ShowS

show :: HaskellPragma -> String

showList :: [HaskellPragma] -> ShowS

Eq HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

foreignHaskell :: Interface -> ([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.