Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Compiler.MAlonzo.Pragmas

Synopsis

- type HaskellCode = String
- type HaskellType = String
- data HaskellPragma
  - = HsDefn Range HaskellCode
  - | HsType Range HaskellType
  - | HsData Range HaskellType [HaskellCode]
  - | HsExport Range HaskellCode
- parsePragma :: CompilerPragma -> Either String HaskellPragma
- parseHaskellPragma :: (MonadTCError m, MonadTrace m) => CompilerPragma -> m HaskellPragma
- getHaskellPragma :: QName -> TCM (Maybe HaskellPragma)
- sanityCheckPragma :: (HasBuiltins m, MonadTCError m, MonadReduce m) => Definition -> Maybe HaskellPragma -> m ()
- getHaskellConstructor :: QName -> HsCompileM (Maybe HaskellCode)
- foreignHaskell :: Interface -> ([String], [String], [String])
- data KindOfForeignCode
  - = ForeignFileHeaderPragma
  - | ForeignImport
  - | ForeignOther
- classifyForeign :: String -> KindOfForeignCode
- classifyPragma :: String -> KindOfForeignCode
- partitionByKindOfForeignCode :: (a -> KindOfForeignCode) -> [a] -> ([a], [a], [a])

# 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

HasRange HaskellPragma Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pragmas Methods getRange :: HaskellPragma -> Range Source #
Pretty HaskellPragma Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pragmas Methods pretty :: HaskellPragma -> Doc Source # prettyPrec :: Int -> HaskellPragma -> Doc Source # prettyList :: [HaskellPragma] -> Doc Source #
Show HaskellPragma Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pragmas Methods showsPrec :: Int -> HaskellPragma -> ShowS Source # show :: HaskellPragma -> String Source # showList :: [HaskellPragma] -> ShowS Source #
Eq HaskellPragma Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pragmas Methods (==) :: HaskellPragma -> HaskellPragma -> Bool Source # (/=) :: HaskellPragma -> HaskellPragma -> Bool Source #

parsePragma :: CompilerPragma -> Either String HaskellPragma Source #

parseHaskellPragma :: (MonadTCError m, MonadTrace m) => CompilerPragma -> m HaskellPragma Source #

getHaskellPragma :: QName -> TCM (Maybe HaskellPragma) Source #

sanityCheckPragma :: (HasBuiltins m, MonadTCError m, MonadReduce m) => Definition -> Maybe HaskellPragma -> m () Source #

getHaskellConstructor :: QName -> HsCompileM (Maybe HaskellCode) Source #

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.