Compiler.Common

Definitions

data ControlFlow : Type

  Tag to indicate if the compiler needs to stop execution immediately

Totality: total
Visibility: public export
Constructors:

Continue : ControlFlow

Abort : ControlFlow

record Codegen : Type

  Generic interface to some code generator

Totality: total
Visibility: public export
Constructor: 

MkCG : (Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> String -> ClosedTerm -> String -> Core (Maybe String)) -> (Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> ClosedTerm -> Core ()) -> Maybe (Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> Core (Maybe (String, List String))) -> Maybe String -> Codegen

Projections:

.compileExpr : Codegen -> Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> String -> ClosedTerm -> String -> Core (Maybe String)

  Compile an Idris 2 expression, saving it to a file.

.executeExpr : Codegen -> Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> ClosedTerm -> Core ()

  Execute an Idris 2 expression directly.

.incCompileFile : Codegen -> Maybe (Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> Core (Maybe (String, List String)))

  Incrementally compile definitions in the current module (toIR defs)
  if supported
  Takes a source file name, returns the name of the generated object
  file, if successful, plus any other backend specific data in a list
  of strings. The generated object file should be placed in the same
  directory as the associated TTC.

.incExt : Codegen -> Maybe String

  If incremental compilation is supported, get the output file extension

.compileExpr : Codegen -> Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> String -> ClosedTerm -> String -> Core (Maybe String)

  Compile an Idris 2 expression, saving it to a file.

Visibility: public export

compileExpr : Codegen -> Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> String -> ClosedTerm -> String -> Core (Maybe String)

  Compile an Idris 2 expression, saving it to a file.

Visibility: public export

.executeExpr : Codegen -> Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> ClosedTerm -> Core ()

  Execute an Idris 2 expression directly.

Visibility: public export

executeExpr : Codegen -> Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> ClosedTerm -> Core ()

  Execute an Idris 2 expression directly.

Visibility: public export

.incCompileFile : Codegen -> Maybe (Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> Core (Maybe (String, List String)))

  Incrementally compile definitions in the current module (toIR defs)
  if supported
  Takes a source file name, returns the name of the generated object
  file, if successful, plus any other backend specific data in a list
  of strings. The generated object file should be placed in the same
  directory as the associated TTC.

Visibility: public export

incCompileFile : Codegen -> Maybe (Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> Core (Maybe (String, List String)))

  Incrementally compile definitions in the current module (toIR defs)
  if supported
  Takes a source file name, returns the name of the generated object
  file, if successful, plus any other backend specific data in a list
  of strings. The generated object file should be placed in the same
  directory as the associated TTC.

Visibility: public export

.incExt : Codegen -> Maybe String

  If incremental compilation is supported, get the output file extension

Visibility: public export

incExt : Codegen -> Maybe String

  If incremental compilation is supported, get the output file extension

Visibility: public export

data UsePhase : Type

Totality: total
Visibility: public export
Constructors:

Cases : UsePhase

Lifted : UsePhase

ANF : UsePhase

VMCode : UsePhase

Hints:

Eq UsePhase

Ord UsePhase

record CompileData : Type

Totality: total
Visibility: public export
Constructor: 

MkCompileData : ClosedCExp -> List (Name, String) -> List (Name, (FC, NamedDef)) -> List (Name, LiftedDef) -> List (Name, ANFDef) -> List (Name, VMDef) -> CompileData

Projections:

.anf : CompileData -> List (Name, ANFDef)

.exported : CompileData -> List (Name, String)

.lambdaLifted : CompileData -> List (Name, LiftedDef)

.mainExpr : CompileData -> ClosedCExp

.namedDefs : CompileData -> List (Name, (FC, NamedDef))

.vmcode : CompileData -> List (Name, VMDef)

.mainExpr : CompileData -> ClosedCExp

Visibility: public export

mainExpr : CompileData -> ClosedCExp

Visibility: public export

.exported : CompileData -> List (Name, String)

Visibility: public export

exported : CompileData -> List (Name, String)

Visibility: public export

.namedDefs : CompileData -> List (Name, (FC, NamedDef))

Visibility: public export

namedDefs : CompileData -> List (Name, (FC, NamedDef))

Visibility: public export

.lambdaLifted : CompileData -> List (Name, LiftedDef)

Visibility: public export

lambdaLifted : CompileData -> List (Name, LiftedDef)

Visibility: public export

.anf : CompileData -> List (Name, ANFDef)

Visibility: public export

anf : CompileData -> List (Name, ANFDef)

Visibility: public export

.vmcode : CompileData -> List (Name, VMDef)

Visibility: public export

vmcode : CompileData -> List (Name, VMDef)

Visibility: public export

compile : Ref Ctxt Defs => Ref Syn SyntaxInfo => Codegen -> ClosedTerm -> String -> Core (Maybe String)

  compile
  Given a value of type Codegen, produce a standalone function
  that executes the `compileExpr` method of the Codegen

Visibility: export

execute : Ref Ctxt Defs => Ref Syn SyntaxInfo => Codegen -> ClosedTerm -> Core ()

  execute
  As with `compile`, produce a functon that executes
  the `executeExpr` method of the given Codegen

Visibility: export

incCompile : Ref Ctxt Defs => Ref Syn SyntaxInfo => Codegen -> String -> Core (Maybe (String, List String))

Visibility: export

nonErased : Ref Ctxt Defs => Name -> Core Bool

Visibility: export

addForeignImpl : Ref Ctxt Defs => Name -> Core ()

Visibility: export

getCompileDataWith : Ref Ctxt Defs => List String -> Bool -> UsePhase -> ClosedTerm -> Core CompileData

Visibility: export

getCompileData : Ref Ctxt Defs => Bool -> UsePhase -> ClosedTerm -> Core CompileData

Visibility: export

compileTerm : Ref Ctxt Defs => ClosedTerm -> Core ClosedCExp

Visibility: export

getIncCompileData : Ref Ctxt Defs => Bool -> UsePhase -> Core CompileData

Visibility: export

exists : String -> IO Bool

  check to see if a given file exists

Visibility: export

parseCC : List String -> List String -> Maybe (String, List String)

Visibility: export

dylib_suffix : String

Visibility: export

locate : Ref Ctxt Defs => String -> Core (String, String)

Visibility: export

copyLib : (String, String) -> Core ()

Visibility: export

getExtraRuntime : List String -> Core String

Visibility: export

getWeakMemoLazy : List String -> Bool

Visibility: export

record ConstantPrimitives' : Type -> Type

  Cast implementations. Values of `ConstantPrimitives` can
  be used in a call to `castInt`, which then determines
  the cast implementation based on the given pair of
  constants.

Totality: total
Visibility: public export
Constructor: 

MkConstantPrimitives : (IntKind -> str -> Core str) -> (IntKind -> str -> Core str) -> (IntKind -> str -> Core str) -> (IntKind -> str -> Core str) -> (IntKind -> str -> Core str) -> (IntKind -> str -> Core str) -> (IntKind -> IntKind -> str -> Core str) -> ConstantPrimitives' str

Projections:

.charToInt : ConstantPrimitives' str -> IntKind -> str -> Core str

.doubleToInt : ConstantPrimitives' str -> IntKind -> str -> Core str

.intToChar : ConstantPrimitives' str -> IntKind -> str -> Core str

.intToDouble : ConstantPrimitives' str -> IntKind -> str -> Core str

.intToInt : ConstantPrimitives' str -> IntKind -> IntKind -> str -> Core str

.intToString : ConstantPrimitives' str -> IntKind -> str -> Core str

.stringToInt : ConstantPrimitives' str -> IntKind -> str -> Core str

.charToInt : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

charToInt : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

.intToChar : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

intToChar : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

.stringToInt : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

stringToInt : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

.intToString : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

intToString : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

.doubleToInt : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

doubleToInt : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

.intToDouble : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

intToDouble : ConstantPrimitives' str -> IntKind -> str -> Core str

Visibility: public export

.intToInt : ConstantPrimitives' str -> IntKind -> IntKind -> str -> Core str

Visibility: public export

intToInt : ConstantPrimitives' str -> IntKind -> IntKind -> str -> Core str

Visibility: public export

ConstantPrimitives : Type

Visibility: public export

castInt : ConstantPrimitives' str -> PrimType -> PrimType -> str -> Core str

  Implements casts from and to integral types by using
  the implementations from the provided `ConstantPrimitives`.

Visibility: export