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

Configure Feed

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

Disentangling the elaboration rules from llbuild2fx

+19 -22
+3 -7
Sources/PterodactylBuild/Elaborator/ElabEnv.swift
··· 50 50 51 51 func lookupDef(name: QName) async -> GlobalDef? { 52 52 if let def = await sink.lookupEmitted(name) { return def } 53 - if let defId = signature.toplevelEnv.decls[name] { 54 - return try? await defId.read(signature.buildContext) 55 - } 56 - 57 - return nil 53 + return await signature.lookup(name) 58 54 } 59 55 60 56 func resolveLocal(name: String) async -> (Value.Type_, Term)? { ··· 90 86 91 87 let resolver = NameResolver(namespace: self.namespace) 92 88 guard 93 - let (resolvedName, defId) = resolver.resolve(name: .user(name), in: signature.toplevelEnv.decls), 94 - let def = try? await defId.read(signature.buildContext) 89 + let resolvedName = resolver.resolve(name: .user(name), in: signature.knownDecls), 90 + let def = await signature.lookup(resolvedName) 95 91 else { return nil } 96 92 97 93 let type = await evaluator().evaluate(type: def.type)
+3 -8
Sources/PterodactylBuild/Elaborator/ElabSignature.swift
··· 2 2 // 3 3 // SPDX-License-Identifier: MPL-2.0 4 4 5 + import OrderedCollections 5 6 import PterodactylCore 6 - import TSCUtility 7 7 8 8 struct ElabSignature: Sendable { 9 - let buildContext: TSCUtility.Context 10 - let toplevelEnv: ToplevelEnv 11 - 12 - func lookup(_ name: QName) async -> GlobalDef? { 13 - guard let defID = toplevelEnv.decls[name] else { return nil } 14 - return try? await defID.read(buildContext) 15 - } 9 + let lookup: @Sendable (QName) async -> GlobalDef? 10 + let knownDecls: OrderedSet<QName> 16 11 }
-1
Sources/PterodactylBuild/Elaborator/ElabSink.swift
··· 5 5 import OrderedCollections 6 6 import PterodactylFeedback 7 7 import PterodactylCore 8 - import TSCUtility 9 8 10 9 struct Emission: Sendable { 11 10 var provenance: Range<Int>?
+4 -4
Sources/PterodactylBuild/Elaborator/NameResolver.swift
··· 10 10 struct NameResolver { 11 11 let namespace: [Name] 12 12 13 - /// Resolve an unqualified name against a dictionary of known declarations. 13 + /// Resolve an unqualified name against a set of known declarations. 14 14 /// Tries the current namespace first, then each enclosing namespace, and finally the top level. 15 - func resolve<V>(name: Name, in decls: OrderedDictionary<QName, V>) -> (QName, V)? { 15 + func resolve(name: Name, in decls: OrderedSet<QName>) -> QName? { 16 16 for i in stride(from: namespace.count, through: 0, by: -1) { 17 17 let candidate = QName(names: Array(namespace.prefix(i)) + [name]) 18 - if let value = decls[candidate] { 19 - return (candidate, value) 18 + if decls.contains(candidate) { 19 + return candidate 20 20 } 21 21 } 22 22 return nil
+9 -2
Sources/PterodactylBuild/Keys/DriverKeys.swift
··· 26 26 public static let versionDependencies: [any FXVersioning.Type] = [ElaborateDecl.self] 27 27 28 28 func elabEnv(_ context: Context) -> ElabEnv { 29 - ElabEnv( 30 - signature: ElabSignature(buildContext: context, toplevelEnv: toplevelEnv), 29 + let toplevelEnv = toplevelEnv 30 + return ElabEnv( 31 + signature: ElabSignature( 32 + lookup: { name in 33 + guard let defID = toplevelEnv.decls[name] else { return nil } 34 + return try? await defID.read(context) 35 + }, 36 + knownDecls: OrderedSet(toplevelEnv.decls.keys) 37 + ), 31 38 sink: ElabSink(), 32 39 namespace: namespace.names 33 40 )