1// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
2// SPDX-FileCopyrightText: 2026 The Project Pterodactyl Developers
3//
4// SPDX-License-Identifier: MPL-2.0
5
6import LanguageServerProtocol
7
8public enum Keyword: String, Codable, Sendable, CaseIterable {
9 case theory = "theory"
10 case `where` = "where"
11 case `import` = "import"
12 case type = "Type"
13 case refl = "refl"
14}
15
16extension Keyword: CustomStringConvertible {
17 public var description: String { rawValue }
18}
19
20public enum Punctuation: String, CaseIterable, Codable, Equatable, Sendable {
21 case lparen = "("
22 case rparen = ")"
23 case lbrace = "{"
24 case rbrace = "}"
25 case comma = ","
26 case dot = "."
27 case colon = ":"
28 case semicolon = ";"
29 case doubleLeftArrow = "<="
30 case doubleRightArrow = "=>"
31 case rightArrow = "->"
32 case equal = "="
33 case questionMark = "?"
34}
35
36extension Punctuation: CustomStringConvertible {
37 public var description: String { rawValue }
38}
39
40public enum TokenKind: Codable, Equatable, Sendable, Hashable {
41 case eof
42 case keyword(Keyword)
43 case punctuation(Punctuation)
44 case error
45 case identifier
46 case newline
47 case whitespace
48 case blockBegin
49 case blockEnd
50 case blockSep
51 case lineComment
52 case blockComment(terminated: Bool)
53}
54
55extension Keyword {
56 public var isBlockHerald: Bool {
57 switch self {
58 case .where: true
59 default: false
60 }
61 }
62}
63
64extension TokenKind {
65 public var isTrivia: Bool {
66 switch self {
67 case .whitespace, .newline, .lineComment, .blockComment: true
68 default: false
69 }
70 }
71
72 public var isVisible: Bool {
73 switch self {
74 case .whitespace, .blockBegin, .blockSep, .blockEnd, .newline: false
75 default: true
76 }
77 }
78
79 public var canDetermineLayoutColumn: Bool {
80 switch self {
81 case .whitespace, .eof: false
82 default: true
83 }
84 }
85
86 public var isBlockHerald: Bool {
87 switch self {
88 case .keyword(let kwd): kwd.isBlockHerald
89 default: false
90 }
91 }
92}
93
94public enum RecordItemKind: Codable, Equatable, Sendable {
95 case spec
96 case impl
97}
98
99public enum SyntaxTreeKind: Codable, Equatable, Sendable {
100 case document
101 case `import`
102 case importName
103 case theory
104 case theoryName
105 case claimDecl
106 case probeDecl
107 case refineDecl
108 case defineDecl
109 case declLhs
110 case declRhs
111 case typedBinder
112 case untypedBinder
113 case depFunType
114 case record
115 case recordItem(kind: RecordItemKind)
116 case funType
117 case lambda
118 case spine
119 case appFrame
120 case projFrame
121 case identifier
122 case universeCodes
123 case idType
124 case hole
125 case refl
126
127 case hint
128 case error
129}
130
131extension SyntaxTreeKind {
132 public var isDecl: Bool {
133 switch self {
134 case .theory, .claimDecl, .refineDecl, .defineDecl, .probeDecl: true
135 default: false
136 }
137 }
138}
139
140public struct TokenMetadata: Equatable, Codable, Sendable {
141 public var semanticTokenType: SemanticTokenTypes
142 public var semanticTokenModifiers: Set<SemanticTokenModifiers> = []
143 public var delimitedFoldingRangeKind: FoldingRangeKind? = nil
144}
145
146public struct SyntaxTreeMetadata: Codable, Equatable, Sendable {
147 public var delimitedFoldingRangeKind: FoldingRangeKind? = nil
148 public var hint: String? = nil
149}
jonmsterling.com