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

Safe HaskellNone
LanguageHaskell98

Agda.Compiler.UHC.CompileState

Description

Contains the state monad that the compiler works in and some functions for tampering with the state.

Synopsis

Documentation

runCompileT Source

Arguments

:: MonadIO m 
=> ModuleName

The module to compile.

-> CompileT m a 
-> m a 

Used to run the Agda-to-UHC Core transformation. During this transformation,

getConstrCTag :: QName -> Compile CTag Source

Returns the CTag for a constructor. Not defined for Sharp and magic UNIT constructor.

getConstrFun :: QName -> Compile HsName Source

Returns the expression to use to build a value of the given datatype/constructor.

conArityAndPars :: QName -> TCM (Nat, Nat) Source

Copy pasted from MAlonzo.... Move somewhere else!