Safe Haskell	None
Language	Haskell2010

Language.Rzk.VSCode.ReferenceIndex

Synopsis

data Uri = Uri {
- uriPath :: FilePath
}
data Position = Position {
- positionLine :: Int
- positionCharacter :: Int
}
data Range = Range {
- rangeStart :: Position
- rangeEnd :: Position
}
data Location = Location {
- locationUri :: Uri
- locationRange :: Range
}
data Binding = Binding {
- bindingName :: Text
- bindingDef :: Location
- bindingType :: Maybe Text
- bindingRefs :: [Location]
}
data ReferenceIndex = ReferenceIndex {
- occurrences :: Map (FilePath, Int) [(Int, Int, Binding)]
- assumeSites :: Map Location AssumeScope
}
indexModules :: [(FilePath, Module)] -> ReferenceIndex
lookupAt :: ReferenceIndex -> Uri -> Position -> Maybe Binding
bindingSites :: Binding -> [Location]
locationPath :: Location -> FilePath
fileOccurrences :: ReferenceIndex -> FilePath -> [(Binding, Int, Int, Int)]
data AssumeScope
- = AssumeTopLevel
- | AssumeInSection
assumeScopeAt :: ReferenceIndex -> Location -> Maybe AssumeScope

Documentation

data Uri Source #

Constructors

Uri
Fields uriPath :: FilePath

Instances

Instances details

Show Uri Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods showsPrec :: Int -> Uri -> ShowS # show :: Uri -> String # showList :: [Uri] -> ShowS #
Eq Uri Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods (==) :: Uri -> Uri -> Bool # (/=) :: Uri -> Uri -> Bool #
Ord Uri Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods compare :: Uri -> Uri -> Ordering # (<) :: Uri -> Uri -> Bool # (<=) :: Uri -> Uri -> Bool # (>) :: Uri -> Uri -> Bool # (>=) :: Uri -> Uri -> Bool # max :: Uri -> Uri -> Uri # min :: Uri -> Uri -> Uri #

data Position Source #

Constructors

Position
Fields positionLine :: Int positionCharacter :: Int

Instances

Instances details

Show Position Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods showsPrec :: Int -> Position -> ShowS # show :: Position -> String # showList :: [Position] -> ShowS #
Eq Position Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods (==) :: Position -> Position -> Bool # (/=) :: Position -> Position -> Bool #
Ord Position Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods compare :: Position -> Position -> Ordering # (<) :: Position -> Position -> Bool # (<=) :: Position -> Position -> Bool # (>) :: Position -> Position -> Bool # (>=) :: Position -> Position -> Bool # max :: Position -> Position -> Position # min :: Position -> Position -> Position #

data Range Source #

Constructors

Range
Fields rangeStart :: Position rangeEnd :: Position

Instances

Instances details

Show Range Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods showsPrec :: Int -> Range -> ShowS # show :: Range -> String # showList :: [Range] -> ShowS #
Eq Range Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods (==) :: Range -> Range -> Bool # (/=) :: Range -> Range -> Bool #
Ord Range Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods compare :: Range -> Range -> Ordering # (<) :: Range -> Range -> Bool # (<=) :: Range -> Range -> Bool # (>) :: Range -> Range -> Bool # (>=) :: Range -> Range -> Bool # max :: Range -> Range -> Range # min :: Range -> Range -> Range #

data Location Source #

Constructors

Location
Fields locationUri :: Uri locationRange :: Range

Instances

Instances details

Show Location Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods showsPrec :: Int -> Location -> ShowS # show :: Location -> String # showList :: [Location] -> ShowS #
Eq Location Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods (==) :: Location -> Location -> Bool # (/=) :: Location -> Location -> Bool #
Ord Location Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods compare :: Location -> Location -> Ordering # (<) :: Location -> Location -> Bool # (<=) :: Location -> Location -> Bool # (>) :: Location -> Location -> Bool # (>=) :: Location -> Location -> Bool # max :: Location -> Location -> Location # min :: Location -> Location -> Location #

data Binding Source #

Constructors

Binding
Fields bindingName :: Text bindingDef :: Location bindingType :: Maybe Text The printed surface annotation of the binder, when it has one (e.g. `A` for `(x : A)`, `I \| φ t` for `(t : I \| φ t)`). Top-level names carry `Nothing`; their elaborated type comes from the typecheck cache instead. bindingRefs :: [Location]

Instances

Instances details

Show Binding Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods showsPrec :: Int -> Binding -> ShowS # show :: Binding -> String # showList :: [Binding] -> ShowS #
Eq Binding Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods (==) :: Binding -> Binding -> Bool # (/=) :: Binding -> Binding -> Bool #

data ReferenceIndex Source #

Constructors

ReferenceIndex

Fields

occurrences :: Map (FilePath, Int) [(Int, Int, Binding)]
Every occurrence (definition or reference), keyed by file and line, as column spans; identifiers never span lines. This is what makes lookupAt a map lookup rather than a scan over all bindings.
assumeSites :: Map Location AssumeScope
The definition sites of #assumed names, with their scope. Assumptions do not survive to the typechecked declarations (the section mechanism folds them into the definitions that use them), so the semantic token overlay recognises them here, syntactically. The scope is kept because the two kinds warrant different styling: a top-level assumption is a file-wide axiom (such as function extensionality), while one inside a section is a hypothesis the section abstracts over at its #end.

Instances

Instances details

Show ReferenceIndex Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods showsPrec :: Int -> ReferenceIndex -> ShowS # show :: ReferenceIndex -> String # showList :: [ReferenceIndex] -> ShowS #

indexModules :: [(FilePath, Module)] -> ReferenceIndex Source #

lookupAt :: ReferenceIndex -> Uri -> Position -> Maybe Binding Source #

bindingSites :: Binding -> [Location] Source #

locationPath :: Location -> FilePath Source #

fileOccurrences :: ReferenceIndex -> FilePath -> [(Binding, Int, Int, Int)] Source #

Every occurrence recorded for a file, with the binding it resolves to: 0-based line and column span. Zero-width spans (the derived def entries of generated eliminators) are skipped; they occupy no characters.

data AssumeScope Source #

Where a name was #assumed.

Constructors

AssumeTopLevel	outside any section: a file-wide axiom
AssumeInSection	inside a section: a hypothesis, discharged at `#end`

Instances

Instances details

Show AssumeScope Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods showsPrec :: Int -> AssumeScope -> ShowS # show :: AssumeScope -> String # showList :: [AssumeScope] -> ShowS #
Eq AssumeScope Source #
Instance details Defined in Language.Rzk.VSCode.ReferenceIndex Methods (==) :: AssumeScope -> AssumeScope -> Bool # (/=) :: AssumeScope -> AssumeScope -> Bool #

assumeScopeAt :: ReferenceIndex -> Location -> Maybe AssumeScope Source #

The assume-scope of a definition site, if it is one of an #assumed name. A local that shadows an assumption resolves to its own binder, not to a site recorded here.