Agda.Compiler.UHC.FromAgda

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.

Documentation

opts :: EHCOpts

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

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

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

Translate an Agda definition to an UHC Core function where applicable

runTT :: TT a -> Compile a

data TTEnv

Constructors

TTEnv

Fields

• nmEnv :: [HsName]

type TT = ReaderT TTEnv Compile

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

data BuiltinKit

Constructors

BuiltinKit

Fields

• isNat :: QName -> Bool
• isInt :: QName -> Bool

builtinKit :: TCM BuiltinKit

compileTerm :: TTerm -> TT CExpr

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

Arguments

:: CExpr

equality function

-> CExpr

case scrutinee (in WHNF)

-> [TAlt]

-> CExpr

default value

-> TT CExpr

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

compileConAlt :: TAlt -> TT CAlt

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

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

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

litToCore :: Literal -> CExpr

getCTagArity :: CTag -> Int

coreError :: String -> CExpr

compilePrim :: TPrim -> CExpr

createMainModule :: ModuleName -> HsName -> CModule