Core.CompileExpr

Definitions

data ConInfo : Type

Totality: total
Visibility: public export
Constructors:

DATACON : ConInfo

TYCON : ConInfo

NIL : ConInfo

CONS : ConInfo

ENUM : Nat -> ConInfo

NOTHING : ConInfo

JUST : ConInfo

RECORD : ConInfo

ZERO : ConInfo

SUCC : ConInfo

UNIT : ConInfo

Hints:

Eq ConInfo

Hashable ConInfo

Show ConInfo

TTC ConInfo

data InlineOk : Type

  Tagging let binders with whether it is safe to inline them

Totality: total
Visibility: public export
Constructors:

YesInline : InlineOk

NotInline : InlineOk

Hints:

Eq InlineOk

TTC InlineOk

data CExp : Scoped

  CExp - an expression ready for compiling.

Totality: total
Visibility: public export
Constructors:

CLocal : FC -> (0 _ : IsVar x idx vars) -> CExp vars

CRef : FC -> Name -> CExp vars

CLam : FC -> (x : Name) -> CExp (x :: vars) -> CExp vars

CLet : FC -> (x : Name) -> InlineOk -> CExp vars -> CExp (x :: vars) -> CExp vars

CApp : FC -> CExp vars -> List (CExp vars) -> CExp vars

CCon : FC -> Name -> ConInfo -> Maybe Int -> List (CExp vars) -> CExp vars

COp : FC -> PrimFn arity -> Vect arity (CExp vars) -> CExp vars

CExtPrim : FC -> Name -> List (CExp vars) -> CExp vars

CForce : FC -> LazyReason -> CExp vars -> CExp vars

CDelay : FC -> LazyReason -> CExp vars -> CExp vars

CConCase : FC -> CExp vars -> List (CConAlt vars) -> Maybe (CExp vars) -> CExp vars

CConstCase : FC -> CExp vars -> List (CConstAlt vars) -> Maybe (CExp vars) -> CExp vars

CPrimVal : FC -> Constant -> CExp vars

CErased : FC -> CExp vars

CCrash : FC -> String -> CExp vars

Hints:

Eq (CExp vars)

FreelyEmbeddable CExp

Ord (CExp vars)

Show (CExp vars)

TTC (CExp vars)

Weaken CExp

data CConAlt : Scoped

Totality: total
Visibility: public export
Constructor: 

MkConAlt : Name -> ConInfo -> Maybe Int -> (args : List Name) -> CExp (args ++ vars) -> CConAlt vars

Hints:

Eq (CConAlt vars)

Ord (CConAlt vars)

TTC (CConAlt vars)

Weaken CConAlt

data CConstAlt : Scoped

Totality: total
Visibility: public export
Constructor: 

MkConstAlt : Constant -> CExp vars -> CConstAlt vars

Hints:

Eq (CConstAlt vars)

Ord (CConstAlt vars)

TTC (CConstAlt vars)

ClosedCExp : Type

Visibility: public export

data NamedCExp : Type

  NamedCExp - as above, but without the name index, so with explicit
  names, which are faster (but less safe) to manipulate in the inliner.
  You can, howeveer, assume that name bindings are unique - translation
  to this form (and the liner) ensure that, even if the type doesn't
  guarantee it!

Totality: total
Visibility: public export
Constructors:

NmLocal : FC -> Name -> NamedCExp

NmRef : FC -> Name -> NamedCExp

NmLam : FC -> Name -> NamedCExp -> NamedCExp

NmLet : FC -> Name -> NamedCExp -> NamedCExp -> NamedCExp

NmApp : FC -> NamedCExp -> List NamedCExp -> NamedCExp

NmCon : FC -> Name -> ConInfo -> Maybe Int -> List NamedCExp -> NamedCExp

NmOp : FC -> PrimFn arity -> Vect arity NamedCExp -> NamedCExp

NmExtPrim : FC -> Name -> List NamedCExp -> NamedCExp

NmForce : FC -> LazyReason -> NamedCExp -> NamedCExp

NmDelay : FC -> LazyReason -> NamedCExp -> NamedCExp

NmConCase : FC -> NamedCExp -> List NamedConAlt -> Maybe NamedCExp -> NamedCExp

NmConstCase : FC -> NamedCExp -> List NamedConstAlt -> Maybe NamedCExp -> NamedCExp

NmPrimVal : FC -> Constant -> NamedCExp

NmErased : FC -> NamedCExp

NmCrash : FC -> String -> NamedCExp

Hints:

HasNamespaces NamedCExp

Hashable NamedCExp

Show NamedCExp

data NamedConAlt : Type

Totality: total
Visibility: public export
Constructor: 

MkNConAlt : Name -> ConInfo -> Maybe Int -> List Name -> NamedCExp -> NamedConAlt

Hints:

HasNamespaces NamedConAlt

Hashable NamedConAlt

Show NamedConAlt

data NamedConstAlt : Type

Totality: total
Visibility: public export
Constructor: 

MkNConstAlt : Constant -> NamedCExp -> NamedConstAlt

Hints:

HasNamespaces NamedConstAlt

Hashable NamedConstAlt

Show NamedConstAlt

data CFType : Type

Totality: total
Visibility: public export
Constructors:

CFUnit : CFType

CFInt : CFType

CFInteger : CFType

CFInt8 : CFType

CFInt16 : CFType

CFInt32 : CFType

CFInt64 : CFType

CFUnsigned8 : CFType

CFUnsigned16 : CFType

CFUnsigned32 : CFType

CFUnsigned64 : CFType

CFString : CFType

CFDouble : CFType

CFChar : CFType

CFPtr : CFType

CFGCPtr : CFType

CFBuffer : CFType

CFForeignObj : CFType

CFWorld : CFType

CFFun : CFType -> CFType -> CFType

CFIORes : CFType -> CFType

CFStruct : String -> List (String, CFType) -> CFType

CFUser : Name -> List CFType -> CFType

Hints:

Hashable CFType

Show CFType

TTC CFType

data CDef : Type

Totality: total
Visibility: public export
Constructors:

MkFun : (args : Scope) -> CExp args -> CDef

MkCon : Maybe Int -> Nat -> Maybe Nat -> CDef

MkForeign : List String -> List CFType -> CFType -> CDef

MkError : ClosedCExp -> CDef

Hints:

Show CDef

TTC CDef

data NamedDef : Type

Totality: total
Visibility: public export
Constructors:

MkNmFun : List Name -> NamedCExp -> NamedDef

MkNmCon : Maybe Int -> Nat -> Maybe Nat -> NamedDef

MkNmForeign : List String -> List CFType -> CFType -> NamedDef

MkNmError : NamedCExp -> NamedDef

Hints:

HasNamespaces NamedDef

Hashable NamedDef

Show NamedDef

data Names : Scoped

Totality: total
Visibility: export
Constructors:

Nil : Names []

(::) : Name -> Names xs -> Names (x :: xs)

getLocName : (idx : Nat) -> Names vars -> (0 _ : IsVar name idx vars) -> Name

Visibility: export

addLocs : (args : List Name) -> Names vars -> Names (args ++ vars)

Visibility: export

forget : CExp vars -> NamedCExp

Visibility: export

forgetDef : CDef -> NamedDef

Visibility: export

insertNames : SizeOf outer -> SizeOf ns -> CExp (outer ++ inner) -> CExp (outer ++ (ns ++ inner))

Visibility: export

shrinkCExp : Thin newvars vars -> CExp vars -> CExp newvars

Visibility: export

SubstCEnv : Scope -> Scoped

Visibility: public export

substs : SizeOf dropped -> SubstCEnv dropped vars -> CExp (dropped ++ vars) -> CExp vars

Visibility: export

mkLocals : SizeOf outer -> Bounds bound -> CExp (outer ++ vars) -> CExp (outer ++ (bound ++ vars))

Visibility: export

refsToLocals : Bounds bound -> CExp vars -> CExp (bound ++ vars)

Visibility: export

getFC : CExp args -> FC

Visibility: export

getFC : NamedCExp -> FC

Visibility: export