idris-1.3.0: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

IRTS.CodegenCommon

Description

 

Synopsis

Documentation

data DbgLevel Source #

Constructors

NONE 
DEBUG 
TRACE 

Instances

data OutputType Source #

Constructors

Raw 
Object 
Executable 

Instances

Eq OutputType Source # 
Show OutputType Source # 
Generic OutputType Source # 

Associated Types

type Rep OutputType :: * -> * #

type Rep OutputType Source # 
type Rep OutputType = D1 * (MetaData "OutputType" "IRTS.CodegenCommon" "idris-1.3.0-sWdxO7YG1l525W5zQFBm8" False) ((:+:) * (C1 * (MetaCons "Raw" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "Object" PrefixI False) (U1 *)) (C1 * (MetaCons "Executable" PrefixI False) (U1 *))))

data CodegenInfo Source #

Everything which might be needed in a code generator.

A CG can choose which level of Decls to generate code from (simplified, defunctionalised or merely lambda lifted) and has access to the list of object files, libraries, etc.