Safe Haskell	None
Language	Haskell98

Agda.Compiler.UHC.FromAgda

Description

Convert from Agda's internal representation to UHC Core via Treeless.

The coinduction kit is translated the same way as in MAlonzo: flat = id sharp = id -> There is no runtime representation of Coinductive values.

Synopsis

Documentation

opts :: EHCOpts Source

fromAgdaModule :: ModuleName -> [ModuleName] -> Interface -> TCM CModule Source

Convert from Agda's internal representation to our auxiliary AST.

translateDefn :: (QName, Definition) -> Compile [CBind] Source

Translate an Agda definition to an UHC Core function where applicable

runTT :: TT a -> Compile a Source

data TTEnv Source

Constructors

TTEnv
Fields nmEnv :: [HsName]

type TT = ReaderT TTEnv Compile Source

addToEnv :: [HsName] -> TT a -> TT a Source

data BuiltinKit Source

Constructors

BuiltinKit
Fields isNat :: QName -> Bool isInt :: QName -> Bool

builtinKit :: TCM BuiltinKit Source

compileTerm :: TTerm -> TT CExpr Source

Translate the actual Agda terms, with an environment of all the bound variables from patternmatching. Agda terms are in de Bruijn so we just check the new names in the position.

buildPrimCases Source

Arguments

:: CExpr	equality function
-> CExpr	case scrutinee (in WHNF)
-> [TAlt]
-> CExpr	default value
-> TT CExpr

mkIfThenElse :: CExpr -> CExpr -> CExpr -> CExpr Source

compileConAlt :: TAlt -> TT CAlt Source

makeConAlt :: QName -> ([HsName] -> TT CExpr) -> TT CAlt Source

defaultBranches :: QName -> [TAlt] -> CExpr -> TT [CAlt] Source

Constructs an alternative for all constructors not explicitly matched by a branch.

litToCore :: Literal -> CExpr Source

getCTagArity :: CTag -> Int Source

coreError :: String -> CExpr Source

compilePrim :: TPrim -> CExpr Source

createMainModule :: ModuleName -> HsName -> CModule Source