| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.MAlonzo.Pragmas
Synopsis
- type HaskellCode = String
- type HaskellType = String
- data HaskellPragma
- 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
- 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
| Pretty HaskellPragma Source # | |
Defined in Agda.Compiler.MAlonzo.Pragmas Methods pretty :: HaskellPragma -> Doc Source # prettyPrec :: Int -> HaskellPragma -> Doc Source # prettyList :: [HaskellPragma] -> Doc Source # | |
| HasRange HaskellPragma Source # | |
Defined in Agda.Compiler.MAlonzo.Pragmas Methods getRange :: HaskellPragma -> Range Source # | |
| Show HaskellPragma Source # | |
Defined in Agda.Compiler.MAlonzo.Pragmas Methods showsPrec :: Int -> HaskellPragma -> ShowS show :: HaskellPragma -> String showList :: [HaskellPragma] -> ShowS | |
| Eq HaskellPragma Source # | |
Defined in Agda.Compiler.MAlonzo.Pragmas | |
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.