jonmsterling.com
Separate out the kernel into a new library
+369
-281
+14
Package.swift
+14
Package.swift
···
25
25
targets: ["PterodactylSyntax"]
26
26
),
27
27
.library(
28
+
name: "PterodactylKernel",
29
+
targets: ["PterodactylKernel"]
30
+
),
31
+
.library(
28
32
name: "PterodactylBuild",
29
33
targets: ["PterodactylBuild"]
30
34
),
···
65
69
]
66
70
),
67
71
.target(
72
+
name: "PterodactylKernel",
73
+
dependencies: [
74
+
"PterodactylCore",
75
+
"PterodactylFeedback",
76
+
.product(name: "OrderedCollections", package: "swift-collections"),
77
+
]
78
+
),
79
+
.target(
68
80
name: "PterodactylBuild",
69
81
dependencies: [
70
82
"PterodactylSyntax",
83
+
"PterodactylKernel",
71
84
"PterodactylCore",
72
85
"PterodactylFeedback",
73
86
.product(name: "OrderedCollections", package: "swift-collections"),
···
91
104
name: "PterodactylBuildTests",
92
105
dependencies: [
93
106
"PterodactylBuild",
107
+
"PterodactylKernel",
94
108
"PterodactylSyntax",
95
109
.product(name: "llbuild2fx", package: "swift-llbuild2")
96
110
]
+11
-11
Sources/PterodactylBuild/Distillation/Distill.swift
Sources/PterodactylKernel/Distillation/Distill.swift
+11
-11
Sources/PterodactylBuild/Distillation/Distill.swift
Sources/PterodactylKernel/Distillation/Distill.swift
···
8
8
// The code in this module is very bad, it should be replaced as soon as the concrete syntax starts to emerge.
9
9
10
10
/// A naming context for resolving de Bruijn indices back to names.
11
-
struct DistillContext {
11
+
public struct DistillContext {
12
12
private var names: [Name?]
13
13
14
-
init(names: [Name?] = []) {
14
+
public init(names: [Name?] = []) {
15
15
self.names = names
16
16
}
17
17
18
-
func resolve(index: Int) -> String {
18
+
public func resolve(index: Int) -> String {
19
19
let i = names.count - 1 - index
20
20
if names.indices.contains(i), let name = names[i] {
21
21
return name.description
···
23
23
return "#\(index)"
24
24
}
25
25
26
-
mutating func extend(name: Name?) {
26
+
public mutating func extend(name: Name?) {
27
27
names.append(name)
28
28
}
29
29
30
-
func extending(name: Name?) -> DistillContext {
30
+
public func extending(name: Name?) -> DistillContext {
31
31
var ctx = self
32
32
ctx.extend(name: name)
33
33
return ctx
34
34
}
35
35
}
36
36
37
-
enum Prec: Int, Comparable {
37
+
public enum Prec: Int, Comparable {
38
38
case top = 0 // anything goes, no parens
39
39
case head = 1 // head of application or projection: wraps depfun, not app
40
40
case atom = 2 // argument of application: wraps app and depfun
41
41
42
-
static func < (lhs: Prec, rhs: Prec) -> Bool {
42
+
public static func < (lhs: Prec, rhs: Prec) -> Bool {
43
43
lhs.rawValue < rhs.rawValue
44
44
}
45
45
}
···
49
49
}
50
50
51
51
extension Term {
52
-
func distill(_ ctx: DistillContext, prec: Prec = .top) -> String {
52
+
public func distill(_ ctx: DistillContext, prec: Prec = .top) -> String {
53
53
switch self {
54
54
case let .local(index: index): return ctx.resolve(index: index)
55
55
case let .global(name: name): return name.description
···
80
80
}
81
81
}
82
82
83
-
func distill(_ ctx: DistillContext, prec: Prec = .top) -> String {
83
+
public func distill(_ ctx: DistillContext, prec: Prec = .top) -> String {
84
84
Self.distillSpine(ctx, names: names, spine: spine[...], prec: prec)
85
85
}
86
86
}
87
87
88
88
extension Term.ProblemPattern {
89
-
func distill(_ ctx: DistillContext, prec: Prec = .top) -> String {
89
+
public func distill(_ ctx: DistillContext, prec: Prec = .top) -> String {
90
90
switch self {
91
91
case let .return(typedTerm): typedTerm.term.distill(ctx, prec: prec)
92
92
}
···
94
94
}
95
95
96
96
extension Term.Type_ {
97
-
func distill(_ ctx: DistillContext, prec: Prec = .top) -> String {
97
+
public func distill(_ ctx: DistillContext, prec: Prec = .top) -> String {
98
98
switch self {
99
99
case .funType(let dom, let boundName, let fam):
100
100
if let boundName {
+21
-21
Sources/PterodactylBuild/Elaborator/ElabEnv.swift
Sources/PterodactylKernel/Elaborator/ElabEnv.swift
+21
-21
Sources/PterodactylBuild/Elaborator/ElabEnv.swift
Sources/PterodactylKernel/Elaborator/ElabEnv.swift
···
5
5
6
6
import PterodactylCore
7
7
8
-
struct ElabEnv: Sendable {
9
-
private(set) var signature: ElabSignature
10
-
let sink: ElabSink
11
-
private(set) var localNames: [Name?]
12
-
private(set) var localValueTypes: [Value.Type_.Thunk]
13
-
private(set) var localValues: [Value]
8
+
public struct ElabEnv: Sendable {
9
+
public private(set) var signature: ElabSignature
10
+
public let sink: ElabSink
11
+
public private(set) var localNames: [Name?]
12
+
public private(set) var localValueTypes: [Value.Type_.Thunk]
13
+
public private(set) var localValues: [Value]
14
14
15
15
/// The name of the target problem.
16
-
var namespace: [Name]
16
+
public var namespace: [Name]
17
17
18
18
/// The elaboration cursor tracks the spine built up by intro rules (e.g. lambdas and records),
19
19
/// separated from `namespace` which identifies the target problem.
20
20
private(set) var cursor: ProblemSpine<Term.Erased> = []
21
21
22
-
init(signature: ElabSignature, sink: ElabSink, namespace: [Name]) {
22
+
public init(signature: ElabSignature, sink: ElabSink, namespace: [Name]) {
23
23
self.signature = signature
24
24
self.sink = sink
25
25
self.namespace = namespace
···
28
28
self.localValues = []
29
29
}
30
30
31
-
func evaluator() async -> Evaluator {
31
+
public func evaluator() async -> Evaluator {
32
32
return Evaluator(
33
33
globals: { await lookupDef(name: $0) },
34
34
locals: localValues.reversed()
35
35
)
36
36
}
37
37
38
-
var localAnalysis: LocalAnalysis {
38
+
public var localAnalysis: LocalAnalysis {
39
39
LocalAnalysis(depth: localValues.count)
40
40
}
41
41
42
-
var droppingLocals: Self {
42
+
public var droppingLocals: Self {
43
43
var env = self
44
44
env.localNames = []
45
45
env.localValueTypes = []
···
48
48
return env
49
49
}
50
50
51
-
func lookupDef(name: QName) async -> GlobalDef? {
51
+
public func lookupDef(name: QName) async -> GlobalDef? {
52
52
if let def = await sink.lookupEmitted(name) { return def }
53
53
return await signature.lookup(name)
54
54
}
···
81
81
return nil
82
82
}
83
83
84
-
func resolve(name: String) async -> (Value.Type_, Term)? {
84
+
public func resolve(name: String) async -> (Value.Type_, Term)? {
85
85
if let result = await resolveLocal(name: name) { return result }
86
86
87
87
let resolver = NameResolver(namespace: self.namespace)
···
96
96
return (type, term)
97
97
}
98
98
99
-
mutating func extendNamespace(_ name: Name) {
99
+
public mutating func extendNamespace(_ name: Name) {
100
100
self.namespace.append(name)
101
101
}
102
102
103
-
mutating func extendCursor(_ frame: ProblemFrame<Term.Erased>) {
103
+
public mutating func extendCursor(_ frame: ProblemFrame<Term.Erased>) {
104
104
cursor.append(frame)
105
105
}
106
106
107
-
mutating func bind(name: Name?, type: Value.Type_.Thunk) async {
107
+
public mutating func bind(name: Name?, type: Value.Type_.Thunk) async {
108
108
let fresh = localAnalysis.fresh(type: type)
109
109
localValues.append(fresh)
110
110
localValueTypes.append(type)
111
111
localNames.append(name)
112
112
}
113
113
114
-
mutating func bind(name: Name?, type: Term.Type_) async {
114
+
public mutating func bind(name: Name?, type: Term.Type_) async {
115
115
let evaluator = await evaluator()
116
116
let type = Value.Type_.Thunk { evaluator.evaluate(type: type) }
117
117
return await bind(name: name, type: type)
118
118
}
119
119
120
-
func binding(name: Name?, type: Value.Type_.Thunk) async -> Self {
120
+
public func binding(name: Name?, type: Value.Type_.Thunk) async -> Self {
121
121
var copy = self
122
122
await copy.bind(name: name, type: type)
123
123
return copy
124
124
}
125
125
126
-
func binding(name: Name?, type: Term.Type_) async -> Self {
126
+
public func binding(name: Name?, type: Term.Type_) async -> Self {
127
127
var copy = self
128
128
await copy.bind(name: name, type: type)
129
129
return copy
130
130
}
131
131
132
-
func extendingNamespace(_ name: Name) -> Self {
132
+
public func extendingNamespace(_ name: Name) -> Self {
133
133
var copy = self
134
134
copy.extendNamespace(name)
135
135
return copy
···
138
138
139
139
140
140
extension ElabEnv {
141
-
func antecedents() async -> [(name: Name?, type: Term.Type_)] {
141
+
public func antecedents() async -> [(name: Name?, type: Term.Type_)] {
142
142
var sequentEnv = droppingLocals
143
143
var antecedents: [(name: Name?, type: Term.Type_)] = []
144
144
+1
-1
Sources/PterodactylBuild/Elaborator/ElabRules.swift
Sources/PterodactylKernel/Elaborator/ElabRules.swift
+1
-1
Sources/PterodactylBuild/Elaborator/ElabRules.swift
Sources/PterodactylKernel/Elaborator/ElabRules.swift
-25
Sources/PterodactylBuild/Elaborator/ElabRules/Binders.swift
-25
Sources/PterodactylBuild/Elaborator/ElabRules/Binders.swift
···
1
-
// SPDX-FileCopyrightText: 2026 The Project Pterodactyl Developers
2
-
//
3
-
// SPDX-License-Identifier: MPL-2.0
4
-
5
-
import PterodactylFeedback
6
-
import PterodactylCore
7
-
8
-
extension ElabRules {
9
-
struct TypedBinder {
10
-
let name: String?
11
-
let type: ElabType
12
-
13
-
init(name: String?, type: ElabType) {
14
-
self.name = name
15
-
self.type = type
16
-
}
17
-
}
18
-
19
-
struct UntypedBinder {
20
-
let name: Name?
21
-
init(name: Name?) {
22
-
self.name = name
23
-
}
24
-
}
25
-
}
+56
-29
Sources/PterodactylBuild/Elaborator/ElabRules/Declarations.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Declarations.swift
+56
-29
Sources/PterodactylBuild/Elaborator/ElabRules/Declarations.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Declarations.swift
···
17
17
}
18
18
19
19
extension Problem: ElabProblem where Leaf == Name? {
20
-
func elabProblem(_ env: ElabEnv) async throws(ElabError) -> Problem<Name?> {
20
+
public func elabProblem(_ env: ElabEnv) async throws(ElabError) -> Problem<Name?> {
21
21
return self
22
22
}
23
23
}
···
67
67
}
68
68
69
69
extension ElabRules {
70
-
struct ExtendingCursor: ElabTerm {
70
+
public struct ExtendingCursor: ElabTerm {
71
71
var frame: ProblemFrame<Term.Erased>
72
72
var body: () -> ElabTerm
73
-
func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
73
+
public func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
74
74
var env = env
75
75
env.extendCursor(frame)
76
76
return try await body().elabTerm(env, type: type)
···
94
94
}
95
95
}
96
96
97
-
struct ProblemApplication: ElabProblem {
98
-
let problem: ElabProblem
99
-
let argument: ElabProblemPattern
97
+
public struct ProblemApplication: ElabProblem {
98
+
public let problem: ElabProblem
99
+
public let argument: ElabProblemPattern
100
100
101
-
func elabProblem(_ env: ElabEnv) async throws(ElabError) -> Problem<Name?> {
101
+
public init(problem: ElabProblem, argument: ElabProblemPattern) {
102
+
self.problem = problem
103
+
self.argument = argument
104
+
}
105
+
106
+
public func elabProblem(_ env: ElabEnv) async throws(ElabError) -> Problem<Name?> {
102
107
let iproblem = try await problem.elabProblem(env)
103
108
let iargument = try await argument.elabProblemPattern(env)
104
109
return iproblem.appending(frame: .app(arg: iargument))
105
110
}
106
111
}
107
112
108
-
struct ProblemProjection: ElabProblem {
109
-
let problem: ElabProblem
110
-
let fieldName: String
113
+
public struct ProblemProjection: ElabProblem {
114
+
public let problem: ElabProblem
115
+
public let fieldName: String
116
+
117
+
public init(problem: ElabProblem, fieldName: String) {
118
+
self.problem = problem
119
+
self.fieldName = fieldName
120
+
}
111
121
112
-
func elabProblem(_ env: ElabEnv) async throws(ElabError) -> Problem<Name?> {
122
+
public func elabProblem(_ env: ElabEnv) async throws(ElabError) -> Problem<Name?> {
113
123
let iproblem = try await problem.elabProblem(env)
114
124
return iproblem.appending(.frame(.proj(fieldName: fieldName)))
115
125
}
···
117
127
118
128
119
129
120
-
struct Claim: ElabDecl, HasProvenance {
121
-
let provenance: Range<Int>?
130
+
public struct Claim: ElabDecl, HasProvenance {
131
+
public let provenance: Range<Int>?
122
132
let problem: ElabProblem
123
133
let type: ElabType
124
134
125
-
init(provenance: Range<Int>?, problem: ElabProblem, type: ElabType) {
135
+
public init(provenance: Range<Int>?, problem: ElabProblem, type: ElabType) {
126
136
self.provenance = provenance
127
137
self.problem = problem
128
138
self.type = type
129
139
}
130
140
131
-
func elabDecl(_ env: ElabEnv) async throws(ElabError) {
141
+
public func elabDecl(_ env: ElabEnv) async throws(ElabError) {
132
142
let iproblem = try await problem.elabProblem(env)
133
143
134
144
guard iproblem.spine.count == 0 else {
···
154
164
}
155
165
}
156
166
157
-
struct Probe: ElabDecl, HasProvenance {
158
-
let provenance: Range<Int>?
159
-
let problem: ElabProblem
167
+
public struct Probe: ElabDecl, HasProvenance {
168
+
public let provenance: Range<Int>?
169
+
public let problem: ElabProblem
160
170
161
-
func elabDecl(_ env: ElabEnv) async throws(ElabError) {
171
+
public init(provenance: Range<Int>?, problem: ElabProblem) {
172
+
self.provenance = provenance
173
+
self.problem = problem
174
+
}
175
+
176
+
public func elabDecl(_ env: ElabEnv) async throws(ElabError) {
162
177
let iproblem = try await problem.elabProblem(env)
163
178
let defType = try await ensureClaim(env, problem: iproblem)
164
179
guard let provenance else { return }
···
177
192
}
178
193
}
179
194
180
-
struct Define: ElabDecl, HasProvenance {
181
-
let provenance: Range<Int>?
182
-
let problem: ElabProblem
183
-
let body: ElabTerm
195
+
public struct Define: ElabDecl, HasProvenance {
196
+
public let provenance: Range<Int>?
197
+
public let problem: ElabProblem
198
+
public let body: ElabTerm
184
199
185
-
func elabDecl(_ env: ElabEnv) async throws(ElabError) {
200
+
public init(provenance: Range<Int>?, problem: ElabProblem, body: ElabTerm) {
201
+
self.provenance = provenance
202
+
self.problem = problem
203
+
self.body = body
204
+
}
205
+
206
+
public func elabDecl(_ env: ElabEnv) async throws(ElabError) {
186
207
let iproblem = try await problem.elabProblem(env)
187
208
let defType = try await ensureClaim(env, problem: iproblem)
188
209
let vtype = await env.evaluator().evaluate(type: defType)
···
203
224
}
204
225
}
205
226
206
-
struct Refine: HasProvenance, ElabDecl {
207
-
let provenance: Range<Int>?
208
-
let problem: ElabProblem
209
-
let gadget: String
227
+
public struct Refine: HasProvenance, ElabDecl {
228
+
public let provenance: Range<Int>?
229
+
public let problem: ElabProblem
230
+
public let gadget: String
210
231
211
-
func elabDecl(_ env: ElabEnv) async throws(ElabError) {
232
+
public init(provenance: Range<Int>?, problem: ElabProblem, gadget: String) {
233
+
self.provenance = provenance
234
+
self.problem = problem
235
+
self.gadget = gadget
236
+
}
237
+
238
+
public func elabDecl(_ env: ElabEnv) async throws(ElabError) {
212
239
guard gadget == "intro" else {
213
240
throw ElabError(
214
241
Diagnostic(
+19
-13
Sources/PterodactylBuild/Elaborator/ElabRules/Function Types.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Function Types.swift
+19
-13
Sources/PterodactylBuild/Elaborator/ElabRules/Function Types.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Function Types.swift
···
6
6
import PterodactylCore
7
7
8
8
extension ElabRules {
9
-
struct DepFunType: ElabType {
9
+
public struct DepFunType: ElabType {
10
10
let binder: TypedBinder
11
11
let fam: ElabType
12
12
13
-
init(binder: TypedBinder, fam: ElabType) {
13
+
public init(binder: TypedBinder, fam: ElabType) {
14
14
self.binder = binder
15
15
self.fam = fam
16
16
}
17
17
18
-
init(dom: ElabType, cod: ElabType) {
18
+
public init(dom: ElabType, cod: ElabType) {
19
19
self.init(binder: TypedBinder(name: nil, type: dom), fam: cod) // consider adding explicit weakening rule to use in 'fam' here
20
20
}
21
21
22
-
func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
22
+
public func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
23
23
let env_dom = env.extendingNamespace(.machine("dom"))
24
24
let idom = try await binder.type.elabType(env_dom, size: size)
25
25
···
32
32
}
33
33
}
34
34
35
-
struct Application: ElabTypedTerm, HasProvenance {
36
-
let provenance: Range<Int>?
37
-
let function: ElabTypedTerm
38
-
let argument: ElabTerm
35
+
public struct Application: ElabTypedTerm, HasProvenance {
36
+
public let provenance: Range<Int>?
37
+
public let function: ElabTypedTerm
38
+
public let argument: ElabTerm
39
39
40
-
func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term) {
40
+
public init(provenance: Range<Int>?, function: ElabTypedTerm, argument: ElabTerm) {
41
+
self.provenance = provenance
42
+
self.function = function
43
+
self.argument = argument
44
+
}
45
+
46
+
public func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term) {
41
47
let funEnv = env.extendingNamespace(.machine("fun"))
42
48
let argEnv = env.extendingNamespace(.machine("arg"))
43
49
···
62
68
}
63
69
}
64
70
65
-
struct Lambda: ElabTerm, HasProvenance {
66
-
let provenance: Range<Int>?
71
+
public struct Lambda: ElabTerm, HasProvenance {
72
+
public let provenance: Range<Int>?
67
73
let binder: UntypedBinder
68
74
let body: ElabTerm
69
75
70
-
init(provenance: Range<Int>? = nil, binder: UntypedBinder, body: () -> ElabTerm) {
76
+
public init(provenance: Range<Int>? = nil, binder: UntypedBinder, body: () -> ElabTerm) {
71
77
self.provenance = provenance
72
78
self.binder = binder
73
79
self.body = body()
74
80
}
75
81
76
-
func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
82
+
public func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
77
83
switch await type.whnf() {
78
84
case let .funType(dom: dom, boundName: typeBoundName, fam: fam):
79
85
let domThunk = AsyncThunk(value: dom)
+6
-6
Sources/PterodactylBuild/Elaborator/ElabRules/Identifier.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Identifier.swift
+6
-6
Sources/PterodactylBuild/Elaborator/ElabRules/Identifier.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Identifier.swift
···
6
6
import PterodactylCore
7
7
8
8
extension ElabRules {
9
-
struct Identifier: ElabTypedTerm, ElabProblem, ElabProblemPattern, HasProvenance {
10
-
let provenance: Range<Int>?
9
+
public struct Identifier: ElabTypedTerm, ElabProblem, ElabProblemPattern, HasProvenance {
10
+
public let provenance: Range<Int>?
11
11
let name: String
12
12
13
-
init(provenance: Range<Int>? = nil, name: String) {
13
+
public init(provenance: Range<Int>? = nil, name: String) {
14
14
self.provenance = provenance
15
15
self.name = name
16
16
}
17
17
18
-
func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term) {
18
+
public func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term) {
19
19
if var (type, term) = await env.resolve(name: name) {
20
20
21
21
// TODO: Instead, we should *require* lblType for global resolutions. This means that ElabEnv.resolve(name:) should instead return whether it was a global or a local.
···
40
40
)
41
41
}
42
42
43
-
func elabProblem(_ env: ElabEnv) async -> Problem<Name?> {
43
+
public func elabProblem(_ env: ElabEnv) async -> Problem<Name?> {
44
44
await env.namedProblem().appending(name: .user(name))
45
45
}
46
46
47
-
func elabProblemPattern(_ env: ElabEnv) async -> ProblemPattern<Name?> {
47
+
public func elabProblemPattern(_ env: ElabEnv) async -> ProblemPattern<Name?> {
48
48
name == "_" ? .return(nil) : .return(.user(name))
49
49
}
50
50
}
+3
-3
Sources/PterodactylBuild/Elaborator/ElabRules/Labelled Types.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Labelled Types.swift
+3
-3
Sources/PterodactylBuild/Elaborator/ElabRules/Labelled Types.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Labelled Types.swift
···
6
6
import PterodactylCore
7
7
8
8
extension ElabRules {
9
-
struct Return: ElabTerm, HasProvenance {
10
-
let provenance: Range<Int>?
9
+
public struct Return: ElabTerm, HasProvenance {
10
+
public let provenance: Range<Int>?
11
11
let body: ElabTerm
12
12
13
13
init(provenance: Range<Int>?, body: () -> ElabTerm) {
···
15
15
self.body = body()
16
16
}
17
17
18
-
func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
18
+
public func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
19
19
let type = await type.whnf()
20
20
switch type {
21
21
case let .lblType(problem: _, type: innerType):
+33
-18
Sources/PterodactylBuild/Elaborator/ElabRules/Record Types.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Record Types.swift
+33
-18
Sources/PterodactylBuild/Elaborator/ElabRules/Record Types.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Record Types.swift
···
8
8
9
9
extension ElabRules {
10
10
11
-
struct RecordFieldSpec: HasProvenance {
12
-
let provenance: Range<Int>?
11
+
public struct RecordFieldSpec: HasProvenance {
12
+
public let provenance: Range<Int>?
13
13
let name: String?
14
14
let type: ElabType
15
15
16
-
init(provenance: Range<Int>?, name: String?, type: ElabType) {
16
+
public init(provenance: Range<Int>?, name: String?, type: ElabType) {
17
17
self.provenance = provenance
18
18
self.name = name
19
19
self.type = type
···
21
21
}
22
22
23
23
24
-
struct RecordFieldImpl: HasProvenance {
25
-
let provenance: Range<Int>?
24
+
public struct RecordFieldImpl: HasProvenance {
25
+
public let provenance: Range<Int>?
26
26
let name: String?
27
27
let impl: ElabTerm
28
-
init(provenance: Range<Int>?, name: String?, impl: ElabTerm) {
28
+
public init(provenance: Range<Int>?, name: String?, impl: ElabTerm) {
29
29
self.provenance = provenance
30
30
self.name = name
31
31
self.impl = impl
32
32
}
33
33
}
34
34
35
-
struct RecordType: ElabType {
36
-
let fields: [RecordFieldSpec]
35
+
public struct RecordType: ElabType {
36
+
public let fields: [RecordFieldSpec]
37
+
38
+
public init(fields: [RecordFieldSpec]) {
39
+
self.fields = fields
40
+
}
37
41
38
-
func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
42
+
public func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
39
43
var runningTermSpecs: OrderedDictionary<String, Term.FieldSpec> = [:]
40
44
var runningValueSpecs: OrderedDictionary<String, Value.FieldSpec> = [:]
41
45
···
57
61
}
58
62
}
59
63
60
-
struct Record: HasProvenance, ElabTerm {
61
-
let provenance: Range<Int>?
62
-
let fields: [RecordFieldImpl]
64
+
public struct Record: HasProvenance, ElabTerm {
65
+
public let provenance: Range<Int>?
66
+
public let fields: [RecordFieldImpl]
67
+
68
+
public init(provenance: Range<Int>?, fields: [RecordFieldImpl]) {
69
+
self.provenance = provenance
70
+
self.fields = fields
71
+
}
63
72
64
-
func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
73
+
public func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
65
74
switch await type.whnf() {
66
75
case let .recordType(fields: fieldSpecs):
67
76
var slice = fields[...]
···
138
147
}
139
148
140
149
141
-
struct RecordProj: ElabTypedTerm, HasProvenance {
142
-
let provenance: Range<Int>?
143
-
let target: ElabTypedTerm
144
-
let fieldName: String
150
+
public struct RecordProj: ElabTypedTerm, HasProvenance {
151
+
public let provenance: Range<Int>?
152
+
public let target: ElabTypedTerm
153
+
public let fieldName: String
145
154
146
-
func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term) {
155
+
public init(provenance: Range<Int>?, target: ElabTypedTerm, fieldName: String) {
156
+
self.provenance = provenance
157
+
self.target = target
158
+
self.fieldName = fieldName
159
+
}
160
+
161
+
public func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term) {
147
162
let (recordType, recordTerm) = try await target.elabTypedTerm(env)
148
163
switch await recordType.whnf() {
149
164
case let .recordType(fields: fields):
+18
-12
Sources/PterodactylBuild/Elaborator/ElabRules/Structural.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Structural.swift
+18
-12
Sources/PterodactylBuild/Elaborator/ElabRules/Structural.swift
Sources/PterodactylKernel/Elaborator/ElabRules/Structural.swift
···
6
6
import PterodactylCore
7
7
8
8
extension ElabRules {
9
-
struct Hole: HasProvenance, ElabTerm, ElabTypedTerm, ElabType {
10
-
var provenance: Range<Int>?
11
-
var appendages: [Value.Problem.Appendage]
12
-
var cause: GlobalDef.Cause
9
+
public struct Hole: HasProvenance, ElabTerm, ElabTypedTerm, ElabType {
10
+
public var provenance: Range<Int>?
11
+
public var appendages: [Value.Problem.Appendage]
12
+
public var cause: GlobalDef.Cause
13
+
14
+
public init(provenance: Range<Int>? = nil, appendages: [Value.Problem.Appendage], cause: GlobalDef.Cause) {
15
+
self.provenance = provenance
16
+
self.appendages = appendages
17
+
self.cause = cause
18
+
}
13
19
14
-
func elabTerm(_ env: ElabEnv, type: Value.Type_) async -> Term {
20
+
public func elabTerm(_ env: ElabEnv, type: Value.Type_) async -> Term {
15
21
let ttype = await env.localAnalysis.quote(type: type)
16
22
17
23
let antecedents = await env.antecedents()
···
62
68
return .cut(term: term, frame: .lblCall(holeProblem))
63
69
}
64
70
65
-
func elabTypedTerm(_ env: ElabEnv) async -> (Value.Type_, Term) {
71
+
public func elabTypedTerm(_ env: ElabEnv) async -> (Value.Type_, Term) {
66
72
var typeHole = self
67
73
typeHole.appendages.append(.name(.machine("type")))
68
74
···
72
78
return (vtype, term)
73
79
}
74
80
75
-
func elabType(_ env: ElabEnv, size: Size<Value>?) async -> Term.Type_ {
81
+
public func elabType(_ env: ElabEnv, size: Size<Value>?) async -> Term.Type_ {
76
82
let code = await elabTerm(env, type: .universeCodes(size: size ?? .big))
77
83
return .decode(size: .big, code: code)
78
84
}
79
85
}
80
86
81
-
struct ModeSwitch: HasProvenance, ElabTerm, ElabType {
82
-
let provenance: Range<Int>?
87
+
public struct ModeSwitch: HasProvenance, ElabTerm, ElabType {
88
+
public let provenance: Range<Int>?
83
89
let instance: ElabTypedTerm
84
90
85
-
init(provenance: Range<Int>? = nil, instance: () -> ElabTypedTerm) {
91
+
public init(provenance: Range<Int>? = nil, instance: () -> ElabTypedTerm) {
86
92
self.provenance = provenance
87
93
self.instance = instance()
88
94
}
89
95
90
-
func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
96
+
public func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term {
91
97
var (foundType, term) = try await instance.elabTypedTerm(env)
92
98
let tfoundType = await env.localAnalysis.quote(type: foundType.whnf())
93
99
foundType = await env.evaluator().evaluate(type: tfoundType)
···
125
131
}
126
132
}
127
133
128
-
func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
134
+
public func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
129
135
let term = try await elabTerm(env, type: .universeCodes(size: size ?? .big))
130
136
return .decode(size: .big, code: term)
131
137
}
-68
Sources/PterodactylBuild/Elaborator/ElabRules/Universes.swift
-68
Sources/PterodactylBuild/Elaborator/ElabRules/Universes.swift
···
1
-
// SPDX-FileCopyrightText: 2026 The Project Pterodactyl Developers
2
-
//
3
-
// SPDX-License-Identifier: MPL-2.0
4
-
5
-
import PterodactylFeedback
6
-
import PterodactylCore
7
-
8
-
extension ElabRules {
9
-
struct UniverseType: HasProvenance, ElabType {
10
-
let provenance: Range<Int>?
11
-
12
-
init(provenance: Range<Int>? = nil) {
13
-
self.provenance = provenance
14
-
}
15
-
16
-
func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
17
-
guard size == nil else {
18
-
throw ElabError(
19
-
Diagnostic(message: "The type of universes is not small.", severity: .warning, absoluteRange: provenance)
20
-
)
21
-
}
22
-
23
-
return .universeType
24
-
}
25
-
}
26
-
27
-
struct UniverseCodes: HasProvenance, ElabType {
28
-
let provenance: Range<Int>?
29
-
30
-
init(provenance: Range<Int>? = nil) {
31
-
self.provenance = provenance
32
-
}
33
-
34
-
// TODO: specify the size
35
-
func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
36
-
guard size == nil else {
37
-
throw ElabError(
38
-
Diagnostic(message: "The universe of big types is not small.", severity: .warning, absoluteRange: provenance)
39
-
)
40
-
}
41
-
42
-
return .universeCodes(size: .big)
43
-
}
44
-
}
45
-
46
-
struct Shrink: ElabTerm, HasProvenance {
47
-
let provenance: Range<Int>?
48
-
var type: ElabType
49
-
50
-
func elabTerm(_ env: ElabEnv, type goal: Value.Type_) async throws(ElabError) -> Term {
51
-
switch await goal.whnf() {
52
-
case let .universeCodes(size: size):
53
-
let itype = try await type.elabType(env, size: size)
54
-
let tsize = await env.localAnalysis.quote(size: size)
55
-
return .shrink(size: tsize, type: itype)
56
-
57
-
default:
58
-
throw ElabError(
59
-
Diagnostic(
60
-
message: "Did not expect to see a type in this position.",
61
-
severity: .warning,
62
-
absoluteRange: provenance
63
-
)
64
-
)
65
-
}
66
-
}
67
-
}
68
-
}
-11
Sources/PterodactylBuild/Elaborator/ElabSignature.swift
-11
Sources/PterodactylBuild/Elaborator/ElabSignature.swift
···
1
-
// SPDX-FileCopyrightText: 2026 The Project Pterodactyl Developers
2
-
//
3
-
// SPDX-License-Identifier: MPL-2.0
4
-
5
-
import OrderedCollections
6
-
import PterodactylCore
7
-
8
-
struct ElabSignature: Sendable {
9
-
let lookup: @Sendable (QName) async -> GlobalDef?
10
-
let knownDecls: OrderedSet<QName>
11
-
}
-29
Sources/PterodactylBuild/Elaborator/ElabSink.swift
-29
Sources/PterodactylBuild/Elaborator/ElabSink.swift
···
1
-
// SPDX-FileCopyrightText: 2026 The Project Pterodactyl Developers
2
-
//
3
-
// SPDX-License-Identifier: MPL-2.0
4
-
5
-
import OrderedCollections
6
-
import PterodactylFeedback
7
-
import PterodactylCore
8
-
9
-
struct Emission: Sendable {
10
-
var provenance: Range<Int>?
11
-
var def: GlobalDef
12
-
}
13
-
14
-
actor ElabSink {
15
-
private(set) var emitted: OrderedDictionary<QName, Emission> = [:]
16
-
private(set) var feedbacks: [Feedback] = []
17
-
18
-
func lookupEmitted(_ name: QName) -> GlobalDef? {
19
-
emitted[name]?.def
20
-
}
21
-
22
-
func emit(name: QName, _ emission: Emission) {
23
-
emitted[name] = emission
24
-
}
25
-
26
-
func emitFeedback(_ feedback: Feedback) {
27
-
feedbacks.append(feedback)
28
-
}
29
-
}
+11
-7
Sources/PterodactylBuild/Elaborator/ElabTactics.swift
Sources/PterodactylKernel/Elaborator/ElabTactics.swift
+11
-7
Sources/PterodactylBuild/Elaborator/ElabTactics.swift
Sources/PterodactylKernel/Elaborator/ElabTactics.swift
···
6
6
import PterodactylFeedback
7
7
import PterodactylCore
8
8
9
-
enum ElabTactics {
10
-
static func lambdas(provenance: Range<Int>? = nil, binders: ArraySlice<ElabRules.UntypedBinder>, body: () -> ElabTerm) -> ElabTerm {
9
+
public enum ElabTactics {
10
+
public static func lambdas(provenance: Range<Int>? = nil, binders: ArraySlice<ElabRules.UntypedBinder>, body: () -> ElabTerm) -> ElabTerm {
11
11
binders.reversed().reduce(body()) { partialResult, binder in
12
12
ElabRules.Lambda(provenance: provenance, binder: binder) { partialResult }
13
13
}
14
14
}
15
15
16
-
static func depFunTypes(binders: ArraySlice<ElabRules.TypedBinder>, body: () -> ElabType) -> ElabType {
16
+
public static func depFunTypes(binders: ArraySlice<ElabRules.TypedBinder>, body: () -> ElabType) -> ElabType {
17
17
binders.reversed().reduce(body()) { partialResult, binder in
18
18
ElabRules.DepFunType(binder: binder, fam: partialResult)
19
19
}
20
20
}
21
21
22
-
static func intro(provenance: Range<Int>? = nil, body: @escaping () -> ElabTerm) -> ElabTerm {
22
+
public static func intro(provenance: Range<Int>? = nil, body: @escaping () -> ElabTerm) -> ElabTerm {
23
23
MatchGoal { goal throws(ElabError) in
24
24
switch goal {
25
25
case let .funType(_, boundName: boundName, _):
···
43
43
}
44
44
}
45
45
46
-
struct MatchGoal: ElabTerm {
47
-
let body: (Value.Type_) throws(ElabError) -> ElabTerm
46
+
public struct MatchGoal: ElabTerm {
47
+
public let body: (Value.Type_) throws(ElabError) -> ElabTerm
48
48
49
-
func elabTerm(_ env: ElabEnv, type: PterodactylCore.Value.Type_) async throws(ElabError) -> PterodactylCore.Term {
49
+
public init(body: @escaping (Value.Type_) throws(ElabError) -> ElabTerm) {
50
+
self.body = body
51
+
}
52
+
53
+
public func elabTerm(_ env: ElabEnv, type: PterodactylCore.Value.Type_) async throws(ElabError) -> PterodactylCore.Term {
50
54
let type = await type.whnf()
51
55
return try await body(type).elabTerm(env, type: type)
52
56
}
+17
-17
Sources/PterodactylBuild/Elaborator/Judgements.swift
Sources/PterodactylKernel/Elaborator/Judgements.swift
+17
-17
Sources/PterodactylBuild/Elaborator/Judgements.swift
Sources/PterodactylKernel/Elaborator/Judgements.swift
···
5
5
import PterodactylFeedback
6
6
import PterodactylCore
7
7
8
-
struct ElabError: Error, HasProvenance {
9
-
var feedback: Feedback
8
+
public struct ElabError: Error, HasProvenance {
9
+
public var feedback: Feedback
10
10
11
11
public init(_ feedback: Feedback) {
12
12
self.feedback = feedback
···
16
16
self.feedback = .diagnostic(diagnostic)
17
17
}
18
18
19
-
var provenance: Range<Int>? {
19
+
public var provenance: Range<Int>? {
20
20
switch feedback {
21
21
case .diagnostic(let diagnostic):
22
22
diagnostic.utf16Range
···
26
26
}
27
27
}
28
28
29
-
protocol ElabDecl {
29
+
public protocol ElabDecl {
30
30
func elabDecl(_ env: ElabEnv) async throws(ElabError)
31
31
}
32
32
33
-
protocol ElabProblem {
33
+
public protocol ElabProblem {
34
34
func elabProblem(_ env: ElabEnv) async throws(ElabError) -> Problem<Name?>
35
35
}
36
36
37
-
protocol ElabProblemPattern {
37
+
public protocol ElabProblemPattern {
38
38
func elabProblemPattern(_ env: ElabEnv) async throws(ElabError) -> ProblemPattern<Name?>
39
39
}
40
40
41
-
protocol ElabType {
41
+
public protocol ElabType {
42
42
func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_
43
43
}
44
44
45
-
protocol ElabTerm {
45
+
public protocol ElabTerm {
46
46
func elabTerm(_ env: ElabEnv, type: Value.Type_) async throws(ElabError) -> Term
47
47
}
48
48
49
-
protocol ElabTypedTerm {
49
+
public protocol ElabTypedTerm {
50
50
func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term)
51
51
}
52
52
53
-
protocol HasProvenance {
53
+
public protocol HasProvenance {
54
54
var provenance: Range<Int>? { get }
55
55
}
56
56
57
57
extension ElabTerm {
58
-
func recoverElabTerm(_ env: ElabEnv, type: Value.Type_) async -> Term {
58
+
public func recoverElabTerm(_ env: ElabEnv, type: Value.Type_) async -> Term {
59
59
do {
60
60
return try await elabTerm(env, type: type)
61
61
} catch {
···
67
67
}
68
68
69
69
extension ElabTypedTerm {
70
-
func recoverElabTypedTerm(_ env: ElabEnv) async -> (Value.Type_, Term) {
70
+
public func recoverElabTypedTerm(_ env: ElabEnv) async -> (Value.Type_, Term) {
71
71
do {
72
72
return try await elabTypedTerm(env)
73
73
} catch {
···
79
79
}
80
80
81
81
extension ElabType {
82
-
func recoverElabType(_ env: ElabEnv, size: Size<Value>?) async -> Term.Type_ {
82
+
public func recoverElabType(_ env: ElabEnv, size: Size<Value>?) async -> Term.Type_ {
83
83
do {
84
84
return try await elabType(env, size: size)
85
85
} catch {
···
92
92
93
93
94
94
extension ElabEnv {
95
-
func richProblemSpine() async -> Term.ProblemSpine {
95
+
public func richProblemSpine() async -> Term.ProblemSpine {
96
96
var spine: Term.ProblemSpine = []
97
97
var localIx = 0
98
98
for frame in cursor {
···
113
113
return spine
114
114
}
115
115
116
-
func namedProblemSpine() -> ProblemSpine<Name?> {
116
+
public func namedProblemSpine() -> ProblemSpine<Name?> {
117
117
var spine: ProblemSpine<Name?> = []
118
118
var localIx = 0
119
119
for frame in cursor {
···
130
130
return spine
131
131
}
132
132
133
-
func namedProblem() async -> Problem<Name?> {
133
+
public func namedProblem() async -> Problem<Name?> {
134
134
Problem(names: namespace, spine: namedProblemSpine())
135
135
}
136
136
137
-
func richProblem() async -> Term.Problem {
137
+
public func richProblem() async -> Term.Problem {
138
138
Term.Problem(names: namespace, spine: await richProblemSpine())
139
139
}
140
140
}
+3
-3
Sources/PterodactylBuild/Elaborator/NameResolver.swift
Sources/PterodactylKernel/Elaborator/NameResolver.swift
+3
-3
Sources/PterodactylBuild/Elaborator/NameResolver.swift
Sources/PterodactylKernel/Elaborator/NameResolver.swift
···
7
7
8
8
/// Resolves unqualified user-written names to fully-qualified ``QName``s
9
9
/// by searching from the innermost enclosing namespace outward.
10
-
struct NameResolver {
11
-
let namespace: [Name]
10
+
public struct NameResolver {
11
+
public let namespace: [Name]
12
12
13
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(name: Name, in decls: OrderedSet<QName>) -> QName? {
15
+
public 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
18
if decls.contains(candidate) {
+7
-6
Sources/PterodactylBuild/Elaborator/SyntaxTreeCursor+Elab.swift
+7
-6
Sources/PterodactylBuild/Elaborator/SyntaxTreeCursor+Elab.swift
···
5
5
6
6
import PterodactylFeedback
7
7
import PterodactylCore
8
+
import PterodactylKernel
8
9
import PterodactylSyntax
9
10
10
11
extension SyntaxTreeCursor {
···
245
246
}
246
247
247
248
extension SyntaxTreeCursor: HasProvenance {
248
-
var provenance: Range<Int>? { visibleUtf16Range }
249
+
public var provenance: Range<Int>? { visibleUtf16Range }
249
250
}
250
251
251
252
extension SyntaxTreeCursor: ElabType {
252
-
func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
253
+
public func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
253
254
let rule: ElabType = typeConstructor ?? hole ?? modeSwitch
254
255
return try await rule.elabType(env, size: size)
255
256
}
256
257
}
257
258
258
259
extension SyntaxTreeCursor: ElabTypedTerm {
259
-
func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term) {
260
+
public func elabTypedTerm(_ env: ElabEnv) async throws(ElabError) -> (Value.Type_, Term) {
260
261
let rule: ElabTypedTerm? = identifier ?? spine ?? hole
261
262
if let rule {
262
263
return try await rule.elabTypedTerm(env)
···
273
274
}
274
275
275
276
extension SyntaxTreeCursor: ElabTerm {
276
-
func elabTerm(_ env: ElabEnv, type: Value.Type_) async -> Term {
277
+
public func elabTerm(_ env: ElabEnv, type: Value.Type_) async -> Term {
277
278
let rule: ElabTerm = lambdas ?? record ?? typeCode ?? hole ?? modeSwitch
278
279
return await rule.recoverElabTerm(env, type: type)
279
280
}
280
281
}
281
282
282
283
extension SyntaxTreeCursor: ElabProblem {
283
-
func elabProblem(_ env: ElabEnv) async throws(ElabError) -> PterodactylCore.Problem<Name?> {
284
+
public func elabProblem(_ env: ElabEnv) async throws(ElabError) -> PterodactylCore.Problem<Name?> {
284
285
let rule: ElabProblem? = identifier ?? problemSpine
285
286
if let rule {
286
287
return try await rule.elabProblem(env)
···
293
294
}
294
295
295
296
extension SyntaxTreeCursor: ElabProblemPattern {
296
-
func elabProblemPattern(_ env: ElabEnv) async throws(ElabError) -> ProblemPattern<Name?> {
297
+
public func elabProblemPattern(_ env: ElabEnv) async throws(ElabError) -> ProblemPattern<Name?> {
297
298
if let identifier {
298
299
return await identifier.elabProblemPattern(env)
299
300
}
+1
Sources/PterodactylBuild/Keys/AssistantKeys.swift
+1
Sources/PterodactylBuild/Keys/AssistantKeys.swift
+1
Sources/PterodactylBuild/Keys/DriverKeys.swift
+1
Sources/PterodactylBuild/Keys/DriverKeys.swift
+25
Sources/PterodactylKernel/Elaborator/ElabRules/Binders.swift
+25
Sources/PterodactylKernel/Elaborator/ElabRules/Binders.swift
···
1
+
// SPDX-FileCopyrightText: 2026 The Project Pterodactyl Developers
2
+
//
3
+
// SPDX-License-Identifier: MPL-2.0
4
+
5
+
import PterodactylFeedback
6
+
import PterodactylCore
7
+
8
+
extension ElabRules {
9
+
public struct TypedBinder {
10
+
public let name: String?
11
+
public let type: ElabType
12
+
13
+
public init(name: String?, type: ElabType) {
14
+
self.name = name
15
+
self.type = type
16
+
}
17
+
}
18
+
19
+
public struct UntypedBinder {
20
+
public let name: Name?
21
+
public init(name: Name?) {
22
+
self.name = name
23
+
}
24
+
}
25
+
}
+73
Sources/PterodactylKernel/Elaborator/ElabRules/Universes.swift
+73
Sources/PterodactylKernel/Elaborator/ElabRules/Universes.swift
···
1
+
// SPDX-FileCopyrightText: 2026 The Project Pterodactyl Developers
2
+
//
3
+
// SPDX-License-Identifier: MPL-2.0
4
+
5
+
import PterodactylFeedback
6
+
import PterodactylCore
7
+
8
+
extension ElabRules {
9
+
public struct UniverseType: HasProvenance, ElabType {
10
+
public let provenance: Range<Int>?
11
+
12
+
public init(provenance: Range<Int>? = nil) {
13
+
self.provenance = provenance
14
+
}
15
+
16
+
public func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
17
+
guard size == nil else {
18
+
throw ElabError(
19
+
Diagnostic(message: "The type of universes is not small.", severity: .warning, absoluteRange: provenance)
20
+
)
21
+
}
22
+
23
+
return .universeType
24
+
}
25
+
}
26
+
27
+
public struct UniverseCodes: HasProvenance, ElabType {
28
+
public let provenance: Range<Int>?
29
+
30
+
public init(provenance: Range<Int>? = nil) {
31
+
self.provenance = provenance
32
+
}
33
+
34
+
// TODO: specify the size
35
+
public func elabType(_ env: ElabEnv, size: Size<Value>?) async throws(ElabError) -> Term.Type_ {
36
+
guard size == nil else {
37
+
throw ElabError(
38
+
Diagnostic(message: "The universe of big types is not small.", severity: .warning, absoluteRange: provenance)
39
+
)
40
+
}
41
+
42
+
return .universeCodes(size: .big)
43
+
}
44
+
}
45
+
46
+
public struct Shrink: ElabTerm, HasProvenance {
47
+
public let provenance: Range<Int>?
48
+
public var type: ElabType
49
+
50
+
public init(provenance: Range<Int>? = nil, type: ElabType) {
51
+
self.provenance = provenance
52
+
self.type = type
53
+
}
54
+
55
+
public func elabTerm(_ env: ElabEnv, type goal: Value.Type_) async throws(ElabError) -> Term {
56
+
switch await goal.whnf() {
57
+
case let .universeCodes(size: size):
58
+
let itype = try await type.elabType(env, size: size)
59
+
let tsize = await env.localAnalysis.quote(size: size)
60
+
return .shrink(size: tsize, type: itype)
61
+
62
+
default:
63
+
throw ElabError(
64
+
Diagnostic(
65
+
message: "Did not expect to see a type in this position.",
66
+
severity: .warning,
67
+
absoluteRange: provenance
68
+
)
69
+
)
70
+
}
71
+
}
72
+
}
73
+
}
+16
Sources/PterodactylKernel/Elaborator/ElabSignature.swift
+16
Sources/PterodactylKernel/Elaborator/ElabSignature.swift
···
1
+
// SPDX-FileCopyrightText: 2026 The Project Pterodactyl Developers
2
+
//
3
+
// SPDX-License-Identifier: MPL-2.0
4
+
5
+
import OrderedCollections
6
+
import PterodactylCore
7
+
8
+
public struct ElabSignature: Sendable {
9
+
public let lookup: @Sendable (QName) async -> GlobalDef?
10
+
public let knownDecls: OrderedSet<QName>
11
+
12
+
public init(lookup: @escaping @Sendable (QName) async -> GlobalDef?, knownDecls: OrderedSet<QName>) {
13
+
self.lookup = lookup
14
+
self.knownDecls = knownDecls
15
+
}
16
+
}
+31
Sources/PterodactylKernel/Elaborator/ElabSink.swift
+31
Sources/PterodactylKernel/Elaborator/ElabSink.swift
···
1
+
// SPDX-FileCopyrightText: 2026 The Project Pterodactyl Developers
2
+
//
3
+
// SPDX-License-Identifier: MPL-2.0
4
+
5
+
import OrderedCollections
6
+
import PterodactylFeedback
7
+
import PterodactylCore
8
+
9
+
public struct Emission: Sendable {
10
+
public var provenance: Range<Int>?
11
+
public var def: GlobalDef
12
+
}
13
+
14
+
public actor ElabSink {
15
+
public private(set) var emitted: OrderedDictionary<QName, Emission> = [:]
16
+
public private(set) var feedbacks: [Feedback] = []
17
+
18
+
public init() {}
19
+
20
+
public func lookupEmitted(_ name: QName) -> GlobalDef? {
21
+
emitted[name]?.def
22
+
}
23
+
24
+
public func emit(name: QName, _ emission: Emission) {
25
+
emitted[name] = emission
26
+
}
27
+
28
+
public func emitFeedback(_ feedback: Feedback) {
29
+
feedbacks.append(feedback)
30
+
}
31
+
}
+2
-1
Tests/PterodactylBuildTests/Test.swift
+2
-1
Tests/PterodactylBuildTests/Test.swift
···
7
7
8
8
@testable import PterodactylBuild
9
9
@testable import PterodactylCore
10
+
@testable import PterodactylKernel
10
11
@testable import PterodactylSyntax
11
12
@testable import llbuild2fx
12
13
···
252
253
253
254
@Test
254
255
func testElab() async throws {
255
-
let signature = ElabSignature(buildContext: Context(), toplevelEnv: ToplevelEnv())
256
+
let signature = ElabSignature(lookup: { _ in nil }, knownDecls: [])
256
257
let sink = ElabSink()
257
258
let env = ElabEnv(signature: signature, sink: sink, namespace: [.user("test")])
258
259