this repo has no description www.jonmsterling.com/01HC/
dependent-types proof-assistant swift
at pattern-unification 171 lines 4.5 kB view raw
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 protocol Located { 9 var utf16Offset: Int { get } 10 var utf16Length: Int { get } 11} 12 13extension Located { 14 public var utf16Range: Range<Int> { 15 utf16Offset..<utf16Offset + utf16Length 16 } 17} 18 19public struct SyntaxTokenCursor: Located { 20 public let token: Token 21 public let metadata: TokenMetadata? 22 public let utf16Offset: Int 23 public var utf16Length: Int { token.utf16Length } 24 25 public var kind: TokenKind { token.kind } 26 27 public init(token: Token, metadata: TokenMetadata?, utf16Offset: Int) { 28 self.token = token 29 self.metadata = metadata 30 self.utf16Offset = utf16Offset 31 } 32 33 public var text: String { token.text } 34} 35 36public struct AbsoluteSyntaxInfo: Located, Sendable { 37 public let lineMap: LineMap 38 39 /// The offset below must be taken from the start of the file. 40 public let cursorOptions: SyntaxTreeCursor.Options 41 42 public init(lineMap: LineMap, cursorOptions: SyntaxTreeCursor.Options) { 43 self.lineMap = lineMap 44 self.cursorOptions = cursorOptions 45 } 46 47 public var cursor: SyntaxTreeCursor { cursorOptions.cursor } 48 public var utf16Length: Int { cursorOptions.tree.utf16Length } 49 public var utf16Offset: Int { cursorOptions.utf16Offset } 50} 51 52/// This is similar to a red tree in the sense of Roslyn. In essence it instruments syntax trees with location information; unlike Roslyn, offsets are understood to be relative to some base offset known to the owner of the cursor. 53public final class SyntaxTreeCursor: Located { 54 public let tree: SyntaxTree 55 public let utf16Offset: Int 56 57 public init(tree: SyntaxTree, utf16Offset: Int) { 58 self.tree = tree 59 self.utf16Offset = utf16Offset 60 } 61 62 public var utf16Length: Int { tree.utf16Length } 63 public var kind: SyntaxTreeKind { tree.kind } 64 65 public enum Child { 66 case token(SyntaxTokenCursor) 67 case tree(SyntaxTreeCursor) 68 } 69 70 public private(set) lazy var children: [Child] = { 71 var children: [Child] = [] 72 var utf16Offset = utf16Offset 73 for childNode in tree.children { 74 switch childNode { 75 case .token(let token, let metadata): 76 let tokenCursor = SyntaxTokenCursor(token: token, metadata: metadata, utf16Offset: utf16Offset) 77 children.append(.token(tokenCursor)) 78 case .tree(let tree): 79 let treeCursor = SyntaxTreeCursor(tree: tree, utf16Offset: utf16Offset) 80 children.append(.tree(treeCursor)) 81 } 82 83 utf16Offset += childNode.utf16Length 84 } 85 86 return children 87 }() 88 89 public private(set) lazy var subtrees: [SyntaxTreeCursor] = { 90 children.compactMap(\.treeCursor) 91 }() 92 93 public var text: String { tree.text } 94} 95 96extension SyntaxTreeCursor.Child: Located { 97 public var treeCursor: SyntaxTreeCursor? { 98 switch self { 99 case .tree(let cursor): cursor 100 default: nil 101 } 102 } 103 104 public var tokenCursor: SyntaxTokenCursor? { 105 switch self { 106 case .token(let cursor): cursor 107 default: nil 108 } 109 } 110 111 public var text: String { 112 delocated.text 113 } 114 115 public var utf16Offset: Int { 116 switch self { 117 case .token(let syntaxTokenCursor): syntaxTokenCursor.utf16Offset 118 case .tree(let syntaxTreeCursor): syntaxTreeCursor.utf16Offset 119 } 120 } 121 122 public var utf16Length: Int { 123 switch self { 124 case .token(let syntaxTokenCursor): syntaxTokenCursor.utf16Length 125 case .tree(let syntaxTreeCursor): syntaxTreeCursor.utf16Length 126 } 127 } 128} 129 130extension SyntaxTreeCursor.Child { 131 var delocated: SyntaxTree.Child { 132 switch self { 133 case .token(let syntaxTokenCursor): .token(syntaxTokenCursor.token, metadata: syntaxTokenCursor.metadata) 134 case .tree(let syntaxTreeCursor): .tree(syntaxTreeCursor.tree) 135 } 136 } 137} 138 139extension SyntaxTreeCursor { 140 /// A sendable type capturing the initialisation parameters of a ``SyntaxCursor``. 141 public struct Options: Sendable { 142 let tree: SyntaxTree 143 let utf16Offset: Int 144 public init(tree: SyntaxTree, utf16Offset: Int) { 145 self.tree = tree 146 self.utf16Offset = utf16Offset 147 } 148 149 public var cursor: SyntaxTreeCursor { 150 SyntaxTreeCursor(tree: tree, utf16Offset: utf16Offset) 151 } 152 } 153 154 public var options: Options { 155 Options(tree: tree, utf16Offset: utf16Offset) 156 } 157} 158 159extension SyntaxTreeCursor { 160 public func collectHints(sink: inout [(Range<Int>, String)], in range: Range<Int>) { 161 guard range.overlaps(utf16Range) else { return } 162 163 if let hint = tree.metadata?.hint { 164 sink.append((utf16Range, hint)) 165 } 166 167 for subtree in subtrees { 168 subtree.collectHints(sink: &sink, in: range) 169 } 170 } 171}