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

Safe Haskell	Safe
Language	Haskell98

Agda.Compiler.UHC.Bridge

Description

Exports the UHC API, and provides dummy definitions if the backend is disabled.

Documentation

uhcBackendEnabled :: Bool Source #

type PP_Doc = String Source #

putPPFile :: String -> PP_Doc -> Int -> IO () Source #

disp :: PP_Doc -> Int -> ShowS Source #

pp :: PP a => a -> PP_Doc Source #

class Serialize a Source #

Instances

Serialize CExpr Source #

Serialize CModule Source #

Serialize CTag Source #

Serialize HsName Source #

putSerializeFile :: FilePath -> a -> IO () Source #

serialize :: x -> Put Source #

unserialize :: Get x Source #

data EHCOpts Source #

defaultEHCOpts :: EHCOpts Source #

data HsName Source #

Instances

Eq HsName Source #
Methods (==) :: HsName -> HsName -> Bool # (/=) :: HsName -> HsName -> Bool #
Ord HsName Source #
Methods compare :: HsName -> HsName -> Ordering # (<) :: HsName -> HsName -> Bool # (<=) :: HsName -> HsName -> Bool # (>) :: HsName -> HsName -> Bool # (>=) :: HsName -> HsName -> Bool # max :: HsName -> HsName -> HsName # min :: HsName -> HsName -> HsName #
Show HsName Source #
Methods showsPrec :: Int -> HsName -> ShowS # show :: HsName -> String # showList :: [HsName] -> ShowS #
Serialize HsName Source #

data CTag Source #

Instances

Eq CTag Source #
Methods (==) :: CTag -> CTag -> Bool # (/=) :: CTag -> CTag -> Bool #
Ord CTag Source #
Methods compare :: CTag -> CTag -> Ordering # (<) :: CTag -> CTag -> Bool # (<=) :: CTag -> CTag -> Bool # (>) :: CTag -> CTag -> Bool # (>=) :: CTag -> CTag -> Bool # max :: CTag -> CTag -> CTag # min :: CTag -> CTag -> CTag #
Show CTag Source #
Methods showsPrec :: Int -> CTag -> ShowS # show :: CTag -> String # showList :: [CTag] -> ShowS #
Serialize CTag Source #

mkHsName :: [String] -> String -> HsName Source #

mkHsName1 :: String -> HsName Source #

mkUniqueHsName :: String -> [String] -> String -> HsName Source #

data CModule Source #

Instances

Serialize CModule Source #

data CImport Source #

data CExport Source #

data CDeclMeta Source #

data CDataCon Source #

data CExpr Source #

Instances

Eq CExpr Source #
Methods (==) :: CExpr -> CExpr -> Bool # (/=) :: CExpr -> CExpr -> Bool #
Ord CExpr Source #
Methods compare :: CExpr -> CExpr -> Ordering # (<) :: CExpr -> CExpr -> Bool # (<=) :: CExpr -> CExpr -> Bool # (>) :: CExpr -> CExpr -> Bool # (>=) :: CExpr -> CExpr -> Bool # max :: CExpr -> CExpr -> CExpr # min :: CExpr -> CExpr -> CExpr #
Show CExpr Source #
Methods showsPrec :: Int -> CExpr -> ShowS # show :: CExpr -> String # showList :: [CExpr] -> ShowS #
Serialize CExpr Source #

data CBind Source #

data CAlt Source #

data CPat Source #

data CPatFld Source #

mkUnit :: EHCOpts -> CExpr Source #

mkInt :: EHCOpts -> Int -> CExpr Source #

mkInteger :: EHCOpts -> Integer -> CExpr Source #

mkChar :: Char -> CExpr Source #

mkString :: EHCOpts -> String -> CExpr Source #

mkError :: EHCOpts -> String -> CExpr Source #

mkUndefined :: EHCOpts -> CExpr Source #

mkVar :: HsName -> CExpr Source #

mkLet1Plain :: HsName -> CExpr -> CExpr -> CExpr Source #

mkLet1Strict :: HsName -> CExpr -> CExpr -> CExpr Source #

mkLetRec :: [CBind] -> CExpr -> CExpr Source #

mkLam :: [HsName] -> CExpr -> CExpr Source #

mkApp :: CExpr -> [CExpr] -> CExpr Source #

mkBind1 :: HsName -> CExpr -> CBind Source #

mkBind1Nm1 :: HsName -> CBind Source #

mkCTag :: HsName -> HsName -> Int -> Int -> CTag Source #

destructCTag :: a -> (HsName -> HsName -> Int -> Int -> a) -> CTag -> a Source #

ctagUnit :: CTag Source #

ctagTrue :: EHCOpts -> CTag Source #

ctagFalse :: EHCOpts -> CTag Source #

ctagCons :: EHCOpts -> CTag Source #

ctagNil :: EHCOpts -> CTag Source #

mkCase :: CExpr -> [CAlt] -> CExpr Source #

mkAlt :: CPat -> CExpr -> CAlt Source #

mkPatCon :: CTag -> CPatRest -> [CPatFld] -> CPat Source #

mkPatRestEmpty :: CPatRest Source #

mkPatFldBind :: (HsName, CExpr) -> CBind -> CPatFld Source #

mkTagTup :: CTag -> [CExpr] -> CExpr Source #

mkModule :: HsName -> [CExport] -> [CImport] -> [CDeclMeta] -> CExpr -> CModule Source #

mkImport :: HsName -> CImport Source #

mkExport :: HsName -> CExport Source #

mkMetaData :: HsName -> [CDataCon] -> CDeclMeta Source #

mkMetaDataCon :: HsName -> Int -> Int -> CDataCon Source #

mkMetaDataConFromCTag :: CTag -> Maybe CDataCon Source #

mkMain :: HsName -> CExpr Source #

parseExpr :: EHCOpts -> String -> Either [String] CExpr Source #

printModule :: EHCOpts -> CModule -> PP_Doc Source #