Idris2Doc : Compiler.Separate

Compiler.Separate

(source)
Reexports
import public Core.FC
import public Core.Name
import public Core.Name.Namespace
import public Core.CompileExpr
import public Compiler.LambdaLift
import public Compiler.VMCode
import public Libraries.Data.Graph
import public Data.SortedMap
import public Data.SortedSet
import public Libraries.Data.StringMap
Definitions
record CompilationUnitId : Type
  Totality: total
  Visibility: export
  Constructor: 
CUID : Int -> CompilationUnitId

  Projection: 
.int : CompilationUnitId -> Int

  Hints:
  
Eq CompilationUnitId
  
Hashable CompilationUnitId
  
Ord CompilationUnitId
record CompilationUnit : Type -> Type
  A compilation unit is a set of namespaces.
  
  The record is parameterised by the type of the definition,
  which makes it reusable for various IRs provided by getCompileData.

  Totality: total
  Visibility: public export
  Constructor: 
MkCompilationUnit : CompilationUnitId -> List1 Namespace -> SortedSet CompilationUnitId -> List (Name, def) -> CompilationUnit def

  Projections:
  
.definitions : CompilationUnit def -> List (Name, def)
  The definitions belonging into this compilation unit.
  
.dependencies : CompilationUnit def -> SortedSet CompilationUnitId
  Other units that this unit depends on.
  
.id : CompilationUnit def -> CompilationUnitId
  Unique identifier of a compilation unit within a CompilationUnitInfo record.
  
.namespaces : CompilationUnit def -> List1 Namespace
  Namespaces contained within the compilation unit.

  Hint: 
Hashable def => Hashable (CompilationUnit def)
.id : CompilationUnit def -> CompilationUnitId
  Unique identifier of a compilation unit within a CompilationUnitInfo record.

  Visibility: public export
id : CompilationUnit def -> CompilationUnitId
  Unique identifier of a compilation unit within a CompilationUnitInfo record.

  Visibility: public export
.namespaces : CompilationUnit def -> List1 Namespace
  Namespaces contained within the compilation unit.

  Visibility: public export
namespaces : CompilationUnit def -> List1 Namespace
  Namespaces contained within the compilation unit.

  Visibility: public export
.dependencies : CompilationUnit def -> SortedSet CompilationUnitId
  Other units that this unit depends on.

  Visibility: public export
dependencies : CompilationUnit def -> SortedSet CompilationUnitId
  Other units that this unit depends on.

  Visibility: public export
.definitions : CompilationUnit def -> List (Name, def)
  The definitions belonging into this compilation unit.

  Visibility: public export
definitions : CompilationUnit def -> List (Name, def)
  The definitions belonging into this compilation unit.

  Visibility: public export
interface HasNamespaces : Type -> Type
  Parameters: a
Methods:
  
nsRefs : a -> SortedSet Namespace
  Return the set of namespaces mentioned within

Implementations:
  
HasNamespaces NamedCExp
  
HasNamespaces NamedConAlt
  
HasNamespaces NamedConstAlt
  
HasNamespaces NamedDef
  
HasNamespaces (Lifted vars)
  
HasNamespaces (LiftedConAlt vars)
  
HasNamespaces (LiftedConstAlt vars)
  
HasNamespaces LiftedDef
  
HasNamespaces VMInst
  
HasNamespaces VMDef
  
HasNamespaces a => HasNamespaces (FC, a)
nsRefs : HasNamespaces a => a -> SortedSet Namespace
  Return the set of namespaces mentioned within

  Visibility: public export
record CompilationUnitInfo : Type -> Type
  Output of the codegen separation algorithm.
  Should contain everything you need in a separately compiling codegen.

  Totality: total
  Visibility: public export
  Constructor: 
MkCompilationUnitInfo : List (CompilationUnit def) -> SortedMap CompilationUnitId (CompilationUnit def) -> SortedMap Namespace CompilationUnitId -> CompilationUnitInfo def

  Projections:
  
.byId : CompilationUnitInfo def -> SortedMap CompilationUnitId (CompilationUnit def)
  Mapping from ID to CompilationUnit.
  
.compilationUnits : CompilationUnitInfo def -> List (CompilationUnit def)
  Compilation units computed from the given definitions,
  ordered topologically, starting from units depending on no other unit.
  
.namespaceMap : CompilationUnitInfo def -> SortedMap Namespace CompilationUnitId
  Maps each namespace to the compilation unit that contains it.
.compilationUnits : CompilationUnitInfo def -> List (CompilationUnit def)
  Compilation units computed from the given definitions,
  ordered topologically, starting from units depending on no other unit.

  Visibility: public export
compilationUnits : CompilationUnitInfo def -> List (CompilationUnit def)
  Compilation units computed from the given definitions,
  ordered topologically, starting from units depending on no other unit.

  Visibility: public export
.byId : CompilationUnitInfo def -> SortedMap CompilationUnitId (CompilationUnit def)
  Mapping from ID to CompilationUnit.

  Visibility: public export
byId : CompilationUnitInfo def -> SortedMap CompilationUnitId (CompilationUnit def)
  Mapping from ID to CompilationUnit.

  Visibility: public export
.namespaceMap : CompilationUnitInfo def -> SortedMap Namespace CompilationUnitId
  Maps each namespace to the compilation unit that contains it.

  Visibility: public export
namespaceMap : CompilationUnitInfo def -> SortedMap Namespace CompilationUnitId
  Maps each namespace to the compilation unit that contains it.

  Visibility: public export
getCompilationUnits : HasNamespaces def => List (Name, def) -> CompilationUnitInfo def
  Group the given definitions into compilation units for separate code generation.

  Visibility: export