Agda.Compiler.MAlonzo.Pragmas

Documentation

type HaskellCode = String

type HaskellType = String

data HaskellPragma

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

Eq HaskellPragma

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

(==) :: HaskellPragma -> HaskellPragma -> Bool

(/=) :: HaskellPragma -> HaskellPragma -> Bool

Show HaskellPragma

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

showsPrec :: Int -> HaskellPragma -> ShowS

show :: HaskellPragma -> String

showList :: [HaskellPragma] -> ShowS

Pretty HaskellPragma

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

pretty :: HaskellPragma -> Doc

prettyPrec :: Int -> HaskellPragma -> Doc

prettyList :: [HaskellPragma] -> Doc

HasRange HaskellPragma

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

getRange :: HaskellPragma -> Range

parsePragma :: CompilerPragma -> Either String HaskellPragma

parseHaskellPragma :: CompilerPragma -> TCM HaskellPragma

getHaskellPragma :: QName -> TCM (Maybe HaskellPragma)

sanityCheckPragma :: Definition -> Maybe HaskellPragma -> TCM ()

getHaskellConstructor :: QName -> TCM (Maybe HaskellCode)

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

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

data KindOfForeignCode

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

Classify a FOREIGN GHC declaration.

classifyPragma :: String -> KindOfForeignCode

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

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

Partition a list by KindOfForeignCode attribute.