Core.Metadata

(source)

Reexports

import public Protocol.IDE.Decoration as Protocol.IDE

Definitions

nameDecoration : Name -> NameType -> Decoration

Visibility: export

ASemanticDecoration : Type

Visibility: public export

SemanticDecorations : Type

Visibility: public export

record Metadata : Type

Totality: total
Visibility: public export
Constructor:

MkMetadata : List (NonEmptyFC, (Nat, ClosedTerm)) -> List (NonEmptyFC, (Name, (Nat, ClosedTerm))) -> List (NonEmptyFC, (Name, (Nat, ClosedTerm))) -> Maybe ClosedTerm -> List (Name, ClosedTerm) -> PosMap (NonEmptyFC, Name) -> OriginDesc -> PosMap ASemanticDecoration -> PosMap (NonEmptyFC, NonEmptyFC) -> PosMap ASemanticDecoration -> Metadata

Projections:

.currentLHS : Metadata -> Maybe ClosedTerm

.holeLHS : Metadata -> List (Name, ClosedTerm)

.lhsApps : Metadata -> List (NonEmptyFC, (Nat, ClosedTerm))

.nameLocMap : Metadata -> PosMap (NonEmptyFC, Name)

.names : Metadata -> List (NonEmptyFC, (Name, (Nat, ClosedTerm)))

.semanticAliases : Metadata -> PosMap (NonEmptyFC, NonEmptyFC)

  Posmap of aliases (in `with` clauses the LHS disapear during
  elaboration after making sure that they match their parents'

.semanticDefaults : Metadata -> PosMap ASemanticDecoration

  Posmap of decorations to default to if the elaboration does not
  produce any highlighting for this range

.semanticHighlighting : Metadata -> PosMap ASemanticDecoration

  Semantic Highlighting
  Posmap of known semantic decorations

.sourceIdent : Metadata -> OriginDesc

.tydecls : Metadata -> List (NonEmptyFC, (Name, (Nat, ClosedTerm)))

Hints:

HasNames Metadata
Show Metadata
TTC Metadata

.lhsApps : Metadata -> List (NonEmptyFC, (Nat, ClosedTerm))

Visibility: public export

lhsApps : Metadata -> List (NonEmptyFC, (Nat, ClosedTerm))

Visibility: public export

.names : Metadata -> List (NonEmptyFC, (Name, (Nat, ClosedTerm)))

Visibility: public export

names : Metadata -> List (NonEmptyFC, (Name, (Nat, ClosedTerm)))

Visibility: public export

.tydecls : Metadata -> List (NonEmptyFC, (Name, (Nat, ClosedTerm)))

Visibility: public export

tydecls : Metadata -> List (NonEmptyFC, (Name, (Nat, ClosedTerm)))

Visibility: public export

.currentLHS : Metadata -> Maybe ClosedTerm

Visibility: public export

currentLHS : Metadata -> Maybe ClosedTerm

Visibility: public export

.holeLHS : Metadata -> List (Name, ClosedTerm)

Visibility: public export

holeLHS : Metadata -> List (Name, ClosedTerm)

Visibility: public export

.nameLocMap : Metadata -> PosMap (NonEmptyFC, Name)

Visibility: public export

nameLocMap : Metadata -> PosMap (NonEmptyFC, Name)

Visibility: public export

.sourceIdent : Metadata -> OriginDesc

Visibility: public export

sourceIdent : Metadata -> OriginDesc

Visibility: public export

.semanticHighlighting : Metadata -> PosMap ASemanticDecoration

  Semantic Highlighting
  Posmap of known semantic decorations

Visibility: public export

semanticHighlighting : Metadata -> PosMap ASemanticDecoration

  Semantic Highlighting
  Posmap of known semantic decorations

Visibility: public export

.semanticAliases : Metadata -> PosMap (NonEmptyFC, NonEmptyFC)

  Posmap of aliases (in `with` clauses the LHS disapear during
  elaboration after making sure that they match their parents'

Visibility: public export

semanticAliases : Metadata -> PosMap (NonEmptyFC, NonEmptyFC)

  Posmap of aliases (in `with` clauses the LHS disapear during
  elaboration after making sure that they match their parents'

Visibility: public export

.semanticDefaults : Metadata -> PosMap ASemanticDecoration

  Posmap of decorations to default to if the elaboration does not
  produce any highlighting for this range

Visibility: public export

semanticDefaults : Metadata -> PosMap ASemanticDecoration

  Posmap of decorations to default to if the elaboration does not
  produce any highlighting for this range

Visibility: public export

allSemanticHighlighting : Ref Ctxt Defs => Metadata -> Core (PosMap ASemanticDecoration)

  Combine semanticHighlighting, semanticAliases, and semanticDefaults into
  a single posmap with all the information

Visibility: export

initMetadata : OriginDesc -> Metadata

Visibility: export

data MD : Type

Totality: total
Visibility: export

addLHS : Ref Ctxt Defs => Ref MD Metadata => FC -> Nat -> Env Term vars -> Term vars -> Core ()

Visibility: export

addNameType : Ref Ctxt Defs => Ref MD Metadata => FC -> Name -> Env Term vars -> Term vars -> Core ()

Visibility: export

addTyDecl : Ref Ctxt Defs => Ref MD Metadata => FC -> Name -> Env Term vars -> Term vars -> Core ()

Visibility: export

addNameLoc : Ref MD Metadata => Ref Ctxt Defs => FC -> Name -> Core ()

Visibility: export

setHoleLHS : Ref MD Metadata => ClosedTerm -> Core ()

Visibility: export

clearHoleLHS : Ref MD Metadata => Core ()

Visibility: export

withCurrentLHS : Ref Ctxt Defs => Ref MD Metadata => Name -> Core ()

Visibility: export

findLHSAt : Ref MD Metadata => (NonEmptyFC -> ClosedTerm -> Bool) -> Core (Maybe (NonEmptyFC, (Nat, ClosedTerm)))

Visibility: export

findTypeAt : Ref MD Metadata => (NonEmptyFC -> (Name, (Nat, ClosedTerm)) -> Bool) -> Core (Maybe (Name, (Nat, ClosedTerm)))

Visibility: export

findTyDeclAt : Ref MD Metadata => (NonEmptyFC -> (Name, (Nat, ClosedTerm)) -> Bool) -> Core (Maybe (NonEmptyFC, (Name, (Nat, ClosedTerm))))

Visibility: export

findHoleLHS : Ref MD Metadata => Name -> Core (Maybe ClosedTerm)

Visibility: export

addSemanticDefault : Ref MD Metadata => ASemanticDecoration -> Core ()

Visibility: export

addSemanticAlias : Ref MD Metadata => NonEmptyFC -> NonEmptyFC -> Core ()

Visibility: export

addSemanticDecorations : Ref MD Metadata => Ref Ctxt Defs => SemanticDecorations -> Core ()

Visibility: export

writeToTTM : Ref Ctxt Defs => Ref MD Metadata => String -> Core ()

Visibility: export

readFromTTM : Ref MD Metadata => String -> Core ()

Visibility: export

readMetadata : String -> Core Metadata

  Read Metadata from given file

Visibility: export

dumpTTM : String -> Core ()

  Dump content of a .ttm file in human-readable format

Visibility: export