Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Interaction.Highlighting.Precise

Contents

- Files
  - Creation
  - Inspection
- Compressed files
  - Creation
  - Inspection
- Tests

Description

Types used for precise syntax highlighting.

Synopsis

- data Aspect
  - = Comment
  - | Keyword
  - | String
  - | Number
  - | Symbol
  - | PrimitiveType
  - | Name (Maybe NameKind) Bool
- data NameKind
  - = Bound
  - | Constructor Induction
  - | Datatype
  - | Field
  - | Function
  - | Module
  - | Postulate
  - | Primitive
  - | Record
- data OtherAspect
  - = Error
  - | DottedPattern
  - | UnsolvedMeta
  - | UnsolvedConstraint
  - | TerminationProblem
  - | IncompletePattern
  - | TypeChecks
- data MetaInfo = MetaInfo {
  - aspect :: Maybe Aspect
  - otherAspects :: [OtherAspect]
  - note :: Maybe String
  - definitionSite :: Maybe (TopLevelModuleName, Integer)
  }
- data File
- type HighlightingInfo = CompressedFile
- singleton :: Ranges -> MetaInfo -> File
- several :: [Ranges] -> MetaInfo -> File
- smallestPos :: File -> Maybe Integer
- toMap :: File -> Map Integer MetaInfo
- newtype CompressedFile = CompressedFile {
  - ranges :: [(Range, MetaInfo)]
  }
- compressedFileInvariant :: CompressedFile -> Bool
- compress :: File -> CompressedFile
- decompress :: CompressedFile -> File
- singletonC :: Ranges -> MetaInfo -> CompressedFile
- severalC :: [Ranges] -> MetaInfo -> CompressedFile
- splitAtC :: Integer -> CompressedFile -> (CompressedFile, CompressedFile)
- smallestPosC :: CompressedFile -> Maybe Integer
- tests :: IO Bool

# Files

data Aspect

Various more or less syntactic aspects of the code. (These cannot overlap.)

Constructors

Comment |
Keyword |
String |
Number |
Symbol | Symbols like forall, =, ->, etc.
PrimitiveType | Things like Set and Prop.
Name (Maybe NameKind) Bool | Is the name an operator part?

Instances

Eq Aspect |
Show Aspect |
Typeable Aspect |
Arbitrary Aspect |
CoArbitrary Aspect |
EmbPrj Aspect |

data NameKind

Constructors

Bound | Bound variable.
Constructor Induction | Inductive or coinductive constructor.
Datatype |
Field | Record field.
Function |
Module | Module name.
Postulate |
Primitive | Primitive.
Record | Record type.

Instances

Eq NameKind |
Show NameKind |
Typeable NameKind |
Arbitrary NameKind |
CoArbitrary NameKind |
EmbPrj NameKind |

data OtherAspect

Other aspects. (These can overlap with each other and with `Aspect`s.)

Constructors

Error |
DottedPattern |
UnsolvedMeta |
UnsolvedConstraint | Unsolved constraint not connected to meta-variable. This could for instance be an emptyness constraint.
TerminationProblem |
IncompletePattern | When this constructor is used it is probably a good idea to include a `note` explaining why the pattern is incomplete.
TypeChecks | Code which is being type-checked.

Instances

Bounded OtherAspect |
Enum OtherAspect |
Eq OtherAspect |
Show OtherAspect |
Typeable OtherAspect |
Arbitrary OtherAspect |
CoArbitrary OtherAspect |
EmbPrj OtherAspect |

data MetaInfo

Meta information which can be associated with a character/character range.

Constructors

MetaInfo |
Fields aspect :: Maybe Aspect otherAspects :: [OtherAspect] note :: Maybe String This note, if present, can be displayed as a tool-tip or something like that. It should contain useful information about the range (like the module containing a certain identifier, or the fixity of an operator). definitionSite :: Maybe (TopLevelModuleName, Integer) The definition site of the annotated thing, if applicable and known. File positions are counted from 1.

Instances

Eq MetaInfo |
Show MetaInfo |
Typeable MetaInfo |
Arbitrary MetaInfo |
CoArbitrary MetaInfo |
Monoid MetaInfo |
EmbPrj MetaInfo |

data File

A `File` is a mapping from file positions to meta information.

The first position in the file has number 1.

Instances

Eq File |
Show File |
Typeable File |
Arbitrary File |
CoArbitrary File |
Monoid File |

type HighlightingInfo = CompressedFile

Syntax highlighting information.

## Creation

singleton :: Ranges -> MetaInfo -> File

``singleton` rs m` is a file whose positions are those in `rs`, and in which every position is associated with `m`.

several :: [Ranges] -> MetaInfo -> File

Like `singleton`, but with several `Ranges` instead of only one.

## Inspection

smallestPos :: File -> Maybe Integer

Returns the smallest position, if any, in the `File`.

toMap :: File -> Map Integer MetaInfo

Convert the `File` to a map from file positions (counting from 1) to meta information.

# Compressed files

newtype CompressedFile

A compressed `File`, in which consecutive positions with the same `MetaInfo` are stored together.

Constructors

CompressedFile |
Fields ranges :: [(Range, MetaInfo)]

Instances

Eq CompressedFile |
Show CompressedFile |
Typeable CompressedFile |
Arbitrary CompressedFile |
Monoid CompressedFile |
EmbPrj CompressedFile |

compressedFileInvariant :: CompressedFile -> Bool

Invariant for compressed files.

Note that these files are not required to be maximally compressed, because ranges are allowed to be empty, and the `MetaInfo`s in adjacent ranges are allowed to be equal.

compress :: File -> CompressedFile

Compresses a file by merging consecutive positions with equal meta information into longer ranges.

decompress :: CompressedFile -> File

Decompresses a compressed file.

## Creation

singletonC :: Ranges -> MetaInfo -> CompressedFile

``singletonC` rs m` is a file whose positions are those in `rs`, and in which every position is associated with `m`.

severalC :: [Ranges] -> MetaInfo -> CompressedFile

Like `singletonR`, but with a list of `Ranges` instead of a single one.

splitAtC :: Integer -> CompressedFile -> (CompressedFile, CompressedFile)

`splitAtC p f` splits the compressed file `f` into `(f1, f2)`, where all the positions in `f1` are `< p`, and all the positions in `f2` are `>= p`.

## Inspection

smallestPosC :: CompressedFile -> Maybe Integer

Returns the smallest position, if any, in the `CompressedFile`.

# Tests

tests :: IO Bool

All the properties.