Idris2Doc : Compiler.VMCode

Compiler.VMCode

(source)

Definitions

data Reg : Type
Totality: total
Visibility: public export
Constructors:
RVal : Reg
Loc : Int -> Reg
Discard : Reg

Hint: 
Show Reg
data VMInst : Type
Totality: total
Visibility: public export
Constructors:
DECLARE : Reg -> VMInst
START : VMInst
ASSIGN : Reg -> Reg -> VMInst
MKCON : Reg -> Either Int Name -> List Reg -> VMInst
MKCLOSURE : Reg -> Name -> Nat -> List Reg -> VMInst
MKCONSTANT : Reg -> Constant -> VMInst
APPLY : Reg -> Reg -> Reg -> VMInst
CALL : Reg -> Bool -> Name -> List Reg -> VMInst
OP : Reg -> PrimFn arity -> Vect arity Reg -> VMInst
EXTPRIM : Reg -> Name -> List Reg -> VMInst
CASE : Reg -> List (Either Int Name, List VMInst) -> Maybe (List VMInst) -> VMInst
CONSTCASE : Reg -> List (Constant, List VMInst) -> Maybe (List VMInst) -> VMInst
PROJECT : Reg -> Reg -> Int -> VMInst
NULL : Reg -> VMInst
ERROR : String -> VMInst

Hints:
HasNamespaces VMInst
Show VMInst
data VMDef : Type
Totality: total
Visibility: public export
Constructors:
MkVMFun : List Int -> List VMInst -> VMDef
MkVMForeign : List String -> List CFType -> CFType -> VMDef
MkVMError : List VMInst -> VMDef

Hints:
HasNamespaces VMDef
Show VMDef
toVMDef : ANFDef -> Maybe VMDef
Visibility: export
allDefs : List (Name, ANFDef) -> List (Name, VMDef)
Visibility: export