Core.FC

(source)

Definitions

FilePos : Type

Totality: total
Visibility: public export

FileName : Type

Totality: total
Visibility: public export

data VirtualIdent : Type

Totality: total
Visibility: public export
Constructor:

Interactive : VirtualIdent

Hints:

Eq VirtualIdent
Show VirtualIdent
TTC VirtualIdent

data OriginDesc : Type

Totality: total
Visibility: public export
Constructors:

PhysicalIdrSrc : ModuleIdent -> OriginDesc

  Anything that originates in physical Idris source files is assigned a
  `PhysicalIdrSrc modIdent`,
    where `modIdent` is the top-level module identifier of that file.

PhysicalPkgSrc : FileName -> OriginDesc

  Anything parsed from a package file is decorated with `PhysicalPkgSrc fname`,
    where `fname` is path to the package file.

Virtual : VirtualIdent -> OriginDesc

Hints:

Eq OriginDesc
Show OriginDesc
TTC OriginDesc

data FC : Type

  A file context is a filename together with starting and ending positions.
  It's often carried by AST nodes that might have been created from a source
  file or by the compiler. That makes it useful to have the notion of
  `EmptyFC` as part of the type.

Totality: total
Visibility: public export
Constructors:

MkFC : OriginDesc -> FilePos -> FilePos -> FC

MkVirtualFC : OriginDesc -> FilePos -> FilePos -> FC

  Virtual FCs are FC attached to desugared/generated code. They can help with marking
  errors, but we shouldn't attach semantic highlighting metadata to them.

EmptyFC : FC

Hints:

Eq FC
HasNames (Int, (FC, Name))
HasNamespaces a => HasNamespaces (FC, a)
Hashable def => Hashable (FC, def)
Pretty Void FC
Show FC
TTC FC

NonEmptyFC : Type

  A version of a file context that cannot be empty

Totality: total
Visibility: public export

justFC : NonEmptyFC -> FC

  NonEmptyFC always embeds into FC