idris-0.9.11: Functional Programming Language with Dependent Types

Safe Haskell	None

IRTS.Lang

Documentation

data Endianness Source

Constructors

Native
BE
LE

Instances

Eq Endianness
Show Endianness

data LVar Source

Constructors

Loc Int
Glob Name

Instances

Eq LVar
Show LVar

data LExp Source

Constructors

LV LVar
LApp Bool LExp [LExp]
LLazyApp Name [LExp]
LLazyExp LExp
LForce LExp
LLet Name LExp LExp
LLam [Name] LExp
LProj LExp Int
LCon Int Name [LExp]
LCase LExp [LAlt]
LConst Const
LForeign FLang FType String [(FType, LExp)]
LOp PrimFn [LExp]
LNothing
LError String

Instances

Eq LExp
Show LExp

data PrimFn Source

Constructors

LPlus ArithTy
LMinus ArithTy
LTimes ArithTy
LUDiv IntTy
LSDiv ArithTy
LURem IntTy
LSRem ArithTy
LAnd IntTy
LOr IntTy
LXOr IntTy
LCompl IntTy
LSHL IntTy
LLSHR IntTy
LASHR IntTy
LEq ArithTy
LLt IntTy
LLe IntTy
LGt IntTy
LGe IntTy
LSLt ArithTy
LSLe ArithTy
LSGt ArithTy
LSGe ArithTy
LSExt IntTy IntTy
LZExt IntTy IntTy
LTrunc IntTy IntTy
LStrConcat
LStrLt
LStrEq
LStrLen
LIntFloat IntTy
LFloatInt IntTy
LIntStr IntTy
LStrInt IntTy
LFloatStr
LStrFloat
LChInt IntTy
LIntCh IntTy
LPrintNum
LPrintStr
LReadStr
LBitCast ArithTy ArithTy
LFExp
LFLog
LFSin
LFCos
LFTan
LFASin
LFACos
LFATan
LFSqrt
LFFloor
LFCeil
LMkVec NativeTy Int
LIdxVec NativeTy Int
LUpdateVec NativeTy Int
LStrHead
LStrTail
LStrCons
LStrIndex
LStrRev
LStdIn
LStdOut
LStdErr
LAllocate
LAppendBuffer
LAppend IntTy Endianness
LPeek IntTy Endianness
LFork
LPar
LVMPtr
LNullPtr
LNoOp

Instances

Eq PrimFn
Show PrimFn

data FCallType Source

Constructors

FStatic
FObject
FConstructor

Instances

Eq FCallType
Show FCallType

data FLang Source

Constructors

LANG_C
LANG_JAVA FCallType

Instances

Eq FLang
Show FLang

data FType Source

Constructors

FArith ArithTy
FFunction
FFunctionIO
FString
FUnit
FPtr
FAny

Instances

Eq FType
Show FType

data LAlt Source

Constructors

LConCase Int Name [Name] LExp
LConstCase Const LExp
LDefaultCase LExp

Instances

Eq LAlt
Show LAlt

data LDecl Source

Constructors

LFun [LOpt] Name [Name] LExp
LConstructor Name Int Int

Instances

Eq LDecl
Show LDecl

type LDefs = Ctxt LDecl Source

data LOpt Source

Constructors

Inline
NoInline

Instances

Eq LOpt
Show LOpt

addTags :: Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)])Source

data LiftState Source

Constructors

LS Name Int [(Name, LDecl)]

lname :: Name -> Int -> Name Source

liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]Source

lambdaLift :: Name -> LDecl -> [(Name, LDecl)]Source

getNextName :: State LiftState Name Source

addFn :: Name -> LDecl -> State LiftState ()Source

lift :: [Name] -> LExp -> State LiftState LExp Source

usedArg :: Eq t => [t] -> t -> [t]Source

usedIn :: [Name] -> LExp -> [Name]Source