this repo has no description www.jonmsterling.com/01HC/
dependent-types proof-assistant swift
13
fork

Configure Feed

Select the types of activity you want to include in your feed.

Refactoring elaboration queries to return a delta

+63 -65
+13 -6
Sources/PterodactylBuild/Elaborator/ElabEnv.swift
··· 7 7 import PterodactylSyntax 8 8 9 9 struct ElabEnv: Sendable { 10 - let state: ElabState 10 + let signature: Signature 11 + let sink: EmissionSink 11 12 var namespace: [Name] 12 13 private var localNames: [Name?] 13 14 private var localValueTypes: [Value.Type_.Thunk] 14 15 var localValues: [Value] 15 16 16 - public init(state: ElabState, namespace: [Name] = []) { 17 - self.state = state 17 + init(signature: Signature, sink: EmissionSink, namespace: [Name] = []) { 18 + self.signature = signature 19 + self.sink = sink 18 20 self.namespace = namespace 19 21 self.localNames = [] 20 22 self.localValueTypes = [] ··· 23 25 24 26 func evaluator() async -> Evaluator { 25 27 return Evaluator( 26 - globals: state.lookup(_:), 28 + globals: { [sink, signature] name in 29 + if let def = await sink.lookupEmitted(name) { 30 + return def 31 + } 32 + return await signature.lookup(name) 33 + }, 27 34 locals: localValues 28 35 ) 29 36 } ··· 49 56 } 50 57 51 58 let resolver = NameResolver(namespace: namespace) 52 - if let (resolvedName, defId) = resolver.resolve(name: name, in: state.toplevelEnv.decls), 53 - let def = try? await defId.read(state.buildContext) 59 + if let (resolvedName, defId) = resolver.resolve(name: name, in: signature.toplevelEnv.decls), 60 + let def = try? await defId.read(signature.buildContext) 54 61 { 55 62 let type = await evaluator().evaluate(type: def.type) 56 63 let term = Term.global(name: resolvedName)
+4 -4
Sources/PterodactylBuild/Elaborator/ElabRules.swift
··· 22 22 rhsEnv.extendNamespace(name: Name(agent: .machine, string: "type")) 23 23 let itype = await type.elabType(rhsEnv) 24 24 let emission = Emission(def: GlobalDef(type: itype, cause: .user)) 25 - await env.state.emit(name: NamespacedName(namespace: env.namespace, name: Name(agent: .user, string: name)), emission) 25 + await env.sink.emit(name: NamespacedName(namespace: env.namespace, name: Name(agent: .user, string: name)), emission) 26 26 } 27 27 } 28 28 ··· 77 77 func elabTypedTerm(_ env: ElabEnv) async -> (Value.Type_, Term) { 78 78 if let typedTerm = await env.resolve(name: name) { return typedTerm } 79 79 if let provenance { 80 - await env.state.emitFeedback( 80 + await env.sink.emitFeedback( 81 81 .diagnostic( 82 82 Diagnostic( 83 83 message: "Could not resolve identifier `\(name)`", ··· 111 111 } 112 112 113 113 if let provenance { 114 - await env.state.emitFeedback( 114 + await env.sink.emitFeedback( 115 115 .diagnostic( 116 116 Diagnostic( 117 117 message: "Cannot apply element of non-function type", ··· 194 194 default: 195 195 let type = env.localAnalysis.quote(type: type) 196 196 if let provenance { 197 - await env.state.emitFeedback( 197 + await env.sink.emitFeedback( 198 198 .diagnostic( 199 199 Diagnostic( 200 200 message: "Attempted to put a lambda abstraction where a value of type \(type) was expected.",
+13 -20
Sources/PterodactylBuild/Elaborator/ElabState.swift
··· 6 6 import PterodactylSyntax 7 7 import TSCUtility 8 8 9 + struct Signature: Sendable { 10 + let buildContext: TSCUtility.Context 11 + let toplevelEnv: ToplevelEnv 12 + 13 + func lookup(_ name: NamespacedName) async -> GlobalDef? { 14 + guard let defID = toplevelEnv.decls[name] else { return nil } 15 + return try? await defID.read(buildContext) 16 + } 17 + } 18 + 9 19 struct Emission: Sendable { 10 20 var provenance: SyntaxTreeCursor.Options? 11 21 var def: GlobalDef 12 22 } 13 23 14 - actor ElabState { 15 - let buildContext: TSCUtility.Context 16 - let toplevelEnv: ToplevelEnv 17 - 24 + actor EmissionSink { 18 25 private(set) var emitted: [NamespacedName: Emission] = [:] 19 26 private(set) var feedbacks: [Feedback] = [] 20 27 21 - init( 22 - buildContext: TSCUtility.Context, 23 - toplevelEnv: ToplevelEnv, 24 - ) { 25 - self.buildContext = buildContext 26 - self.toplevelEnv = toplevelEnv 27 - } 28 - 29 - func lookup(_ name: NamespacedName) async -> GlobalDef? { 30 - if let emission = emitted[name] { 31 - return emission.def 32 - } else if let defID = toplevelEnv.decls[name] { 33 - return try? await defID.read(buildContext) 34 - } 35 - 36 - return nil 28 + func lookupEmitted(_ name: NamespacedName) -> GlobalDef? { 29 + emitted[name]?.def 37 30 } 38 31 39 32 func emit(name: NamespacedName, _ emission: Emission) {
+2 -2
Sources/PterodactylBuild/Elaborator/Judgements.swift
··· 36 36 37 37 let holeName = NamespacedName(namespace: env.namespace, name: name) 38 38 let emission = Emission(provenance: provenance, def: GlobalDef(type: generalisedType, cause: cause)) 39 - await env.state.emit(name: holeName, emission) 39 + await env.sink.emit(name: holeName, emission) 40 40 41 41 if let provenance, cause == .user { 42 - await env.state.emitFeedback( 42 + await env.sink.emitFeedback( 43 43 .inlay( 44 44 InlayHint( 45 45 label: holeName.description,
+4 -4
Sources/PterodactylBuild/Elaborator/SyntaxTreeCursor+Elab.swift
··· 135 135 if let identifier { 136 136 return await identifier.elabTypedTerm(env) 137 137 } 138 - 138 + 139 139 if let applications { 140 140 return await applications.elabTypedTerm(env) 141 141 } 142 - 142 + 143 143 if kind == .hole { 144 144 return await emitTypedTermHole(env, name: Name(agent: .machine, string: "hole"), cause: .user) 145 145 } 146 146 147 147 if kind != .error { 148 - await env.state.emitFeedback( 148 + await env.sink.emitFeedback( 149 149 .diagnostic( 150 150 Diagnostic( 151 151 message: "Expected a synthesizable term expression", ··· 170 170 let term = await emitTermHole(env, type: type, name: Name(agent: .machine, string: "recovery"), cause: .recovery) 171 171 172 172 if kind != .error { 173 - await env.state.emitFeedback( 173 + await env.sink.emitFeedback( 174 174 .diagnostic( 175 175 Diagnostic( 176 176 message: "Expected a checkable term expression",
+17 -13
Sources/PterodactylBuild/Keys/DriverKeys.swift
··· 8 8 9 9 public struct ElaborateDecl: AsyncFXKey { 10 10 public struct ValueType: Codable, FXValue { 11 - public var toplevelEnv: ToplevelEnv 11 + public var newDecls: [NamespacedName: TypedDataID<GlobalDef>] 12 12 public var feedbacks: [Feedback] 13 13 } 14 14 ··· 19 19 public static let versionDependencies: [any FXVersioning.Type] = [ElaborateDecl.self] 20 20 21 21 func elabEnv(_ context: Context) -> ElabEnv { 22 - ElabEnv(state: ElabState(buildContext: context, toplevelEnv: toplevelEnv), namespace: namespace) 22 + ElabEnv(signature: Signature(buildContext: context, toplevelEnv: toplevelEnv), sink: EmissionSink(), namespace: namespace) 23 23 } 24 24 25 25 public func computeValue(_ fi: llbuild2fx.FXFunctionInterface<Self>, _ ctx: TSCUtility.Context) async throws -> ValueType { ··· 30 30 let theoryName = subtrees.first { $0.kind == .theoryName }?.text 31 31 let decls = subtrees.filter { $0.kind.isDecl } 32 32 33 - var result = ValueType(toplevelEnv: toplevelEnv, feedbacks: []) 33 + var newDecls: [NamespacedName: TypedDataID<GlobalDef>] = [:] 34 + var feedbacks: [Feedback] = [] 35 + var runningEnv = toplevelEnv 34 36 35 37 for decl in decls { 36 38 let namespace = if let theoryName { namespace + [Name(agent: .user, string: theoryName)] } else { namespace } 37 - let declResult = try await fi.request(ElaborateDecl(namespace: namespace, toplevelEnv: result.toplevelEnv, code: decl.tree), ctx) 38 - result.toplevelEnv = declResult.toplevelEnv 39 - result.feedbacks += declResult.feedbacks.map { 39 + let declResult = try await fi.request(ElaborateDecl(namespace: namespace, toplevelEnv: runningEnv, code: decl.tree), ctx) 40 + runningEnv.decls.merge(declResult.newDecls) { _, new in new } 41 + newDecls.merge(declResult.newDecls) { _, new in new } 42 + feedbacks += declResult.feedbacks.map { 40 43 $0.offsettingUtf16Range(by: decl.utf16Offset) 41 44 } 42 45 } 43 46 44 - return result 47 + return ValueType(newDecls: newDecls, feedbacks: feedbacks) 45 48 46 49 case .claimDecl: 47 50 guard let claim = cursor.claim else { fatalError() } 48 51 let elabEnv = elabEnv(ctx) 49 52 await claim.elabDecl(elabEnv) 50 53 51 - var result = ValueType(toplevelEnv: toplevelEnv, feedbacks: []) 52 - try await result.toplevelEnv.update(from: elabEnv.state, in: ctx) 53 - result.feedbacks += await elabEnv.state.feedbacks 54 - return result 54 + var newDecls: [NamespacedName: TypedDataID<GlobalDef>] = [:] 55 + for (name, emission) in await elabEnv.sink.emitted { 56 + newDecls[name] = try await emission.def.save(ctx) 57 + } 58 + return ValueType(newDecls: newDecls, feedbacks: await elabEnv.sink.feedbacks) 55 59 56 60 case .defineDecl, .refineDecl: 57 61 let diagnostic = Diagnostic(message: "This kind of declaration is not yet supported", severity: .warning, absoluteRange: cursor.utf16Range) 58 - return ValueType(toplevelEnv: toplevelEnv, feedbacks: [.diagnostic(diagnostic)]) 62 + return ValueType(newDecls: [:], feedbacks: [.diagnostic(diagnostic)]) 59 63 default: fatalError() 60 64 } 61 65 } ··· 106 110 107 111 if childTree.kind.isDecl { 108 112 let localResult = try await fi.request(ElaborateDecl(namespace: [], toplevelEnv: result.toplevelEnv, code: childTree.tree), ctx) 109 - result.toplevelEnv = localResult.toplevelEnv 113 + result.toplevelEnv.decls.merge(localResult.newDecls) { _, new in new } 110 114 result.feedbacks += localResult.feedbacks.map { $0.offsettingUtf16Range(by: childTree.utf16Offset) } 111 115 } 112 116 }
-7
Sources/PterodactylBuild/ToplevelEnv.swift
··· 3 3 // SPDX-License-Identifier: MPL-2.0 4 4 5 5 import PterodactylKernel 6 - import PterodactylSyntax 7 6 import llbuild2fx 8 7 9 8 public struct ToplevelEnv: Codable, Sendable { ··· 11 10 12 11 mutating func `import`(env: Self) { 13 12 decls.merge(env.decls) { original, new in new } 14 - } 15 - 16 - mutating func update(from state: ElabState, in context: Context) async throws { 17 - for (name, emission) in await state.emitted { 18 - decls[name] = try await emission.def.save(context) 19 - } 20 13 } 21 14 }
+2 -2
Sources/PterodactylKernel/Core Types/Value.swift
··· 72 72 public let head: Head 73 73 public let spine: Spine 74 74 public let boundary: AsyncThunk<Boundary> 75 - 75 + 76 76 public init(head: Head, spine: Spine, boundary: AsyncThunk<Boundary>) { 77 77 self.head = head 78 78 self.spine = spine 79 79 self.boundary = boundary 80 80 } 81 - 81 + 82 82 public var globalHead: NamespacedName? { 83 83 switch head { 84 84 case .global(let name): name
+1 -1
Sources/PterodactylKernel/Evaluator.swift
··· 8 8 case user 9 9 case recovery 10 10 } 11 - 11 + 12 12 public let type: Term.Type_ 13 13 public let term: Term? 14 14 public let cause: Cause?
+1 -1
Sources/PterodactylLanguageServer/Event Handlers/RequestHandler.swift
··· 116 116 let position = info.lineMap.lspPosition(at: range.endIndex) 117 117 return InlayHint(position: position, label: .optionA(hint)) 118 118 } 119 - 119 + 120 120 if let state = await actor.savedFeedbacks[params.textDocument.uri] { 121 121 lspHints += state.allFeedbacks.compactMap { feedback in 122 122 switch feedback {
+1 -1
Sources/PterodactylSyntax/Diagnostic.swift
··· 31 31 public struct InlayHint: Codable, Sendable, Equatable, RelativelyLocated { 32 32 public var label: String 33 33 public var utf16Offset: Int 34 - 34 + 35 35 public init(label: String, utf16Offset: Int) { 36 36 self.label = label 37 37 self.utf16Offset = utf16Offset
+1 -1
Sources/PterodactylSyntax/LineMap.swift
··· 30 30 let columnNumber = utf16Offset - lineStart 31 31 return Position(line: lineNumber, character: columnNumber) 32 32 } 33 - 33 + 34 34 public func lspRange(of range: Range<Int>) -> LanguageServerProtocol.LSPRange { 35 35 let start = lspPosition(at: range.lowerBound) 36 36 let end = lspPosition(at: range.upperBound)
+4 -3
Tests/PterodactylBuildTests/Test.swift
··· 160 160 161 161 @Test 162 162 func testElab() async throws { 163 - let state = ElabState(buildContext: Context(), toplevelEnv: ToplevelEnv()) 164 - let env = ElabEnv(state: state) 163 + let signature = Signature(buildContext: Context(), toplevelEnv: ToplevelEnv()) 164 + let sink = EmissionSink() 165 + let env = ElabEnv(signature: signature, sink: sink) 165 166 166 167 let funType = 167 168 await ElabRules.FunType( ··· 186 187 } 187 188 188 189 #expect(result, "Identity function incorrectly elaborated as: \(lambda)") 189 - #expect(await state.emitted.count == 0) 190 + #expect(await sink.emitted.count == 0) 190 191 } 191 192 }