First cut at core syntax, semantic domain, glued NbE.

Jon Sterling 5b19b15b

+13
.gitignore
···
+
# SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
#
+
# SPDX-License-Identifier: MPL-2.0
+
+
.DS_Store
+
/.build
+
/Packages
+
xcuserdata/
+
DerivedData/
+
.swiftpm/configuration/registries.json
+
.swiftpm/xcode/package.xcworkspace/contents.xcworkspacedata
+
.netrc
+
Package.resolved
+77
.swift-format
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
{
+
"fileScopedDeclarationPrivacy" : {
+
"accessLevel" : "private"
+
},
+
"indentConditionalCompilationBlocks" : true,
+
"indentSwitchCaseLabels" : false,
+
"indentation" : {
+
"tabs" : 1
+
},
+
"lineBreakAroundMultilineExpressionChainComponents" : false,
+
"lineBreakBeforeControlFlowKeywords" : false,
+
"lineBreakBeforeEachArgument" : false,
+
"lineBreakBeforeEachGenericRequirement" : false,
+
"lineBreakBetweenDeclarationAttributes" : false,
+
"lineLength" : 200,
+
"maximumBlankLines" : 10,
+
"multiElementCollectionTrailingCommas" : false,
+
"noAssignmentInExpressions" : {
+
"allowedFunctions" : [
+
"XCTAssertNoThrow"
+
]
+
},
+
"prioritizeKeepingFunctionOutputTogether" : false,
+
"reflowMultilineStringLiterals" : "never",
+
"respectsExistingLineBreaks" : true,
+
"rules" : {
+
"AllPublicDeclarationsHaveDocumentation" : false,
+
"AlwaysUseLiteralForEmptyCollectionInit" : false,
+
"AlwaysUseLowerCamelCase" : true,
+
"AmbiguousTrailingClosureOverload" : true,
+
"AvoidRetroactiveConformances" : true,
+
"BeginDocumentationCommentWithOneLineSummary" : false,
+
"DoNotUseSemicolons" : true,
+
"DontRepeatTypeInStaticProperties" : true,
+
"FileScopedDeclarationPrivacy" : true,
+
"FullyIndirectEnum" : true,
+
"GroupNumericLiterals" : true,
+
"IdentifiersMustBeASCII" : false,
+
"NeverForceUnwrap" : false,
+
"NeverUseForceTry" : false,
+
"NeverUseImplicitlyUnwrappedOptionals" : false,
+
"NoAccessLevelOnExtensionDeclaration" : true,
+
"NoAssignmentInExpressions" : true,
+
"NoBlockComments" : false,
+
"NoCasesWithOnlyFallthrough" : true,
+
"NoEmptyLinesOpeningClosingBraces" : false,
+
"NoEmptyTrailingClosureParentheses" : true,
+
"NoLabelsInCasePatterns" : true,
+
"NoLeadingUnderscores" : false,
+
"NoParensAroundConditions" : true,
+
"NoPlaygroundLiterals" : true,
+
"NoVoidReturnOnFunctionSignature" : true,
+
"OmitExplicitReturns" : false,
+
"OneCasePerLine" : true,
+
"OneVariableDeclarationPerLine" : true,
+
"OnlyOneTrailingClosureArgument" : true,
+
"OrderedImports" : true,
+
"ReplaceForEachWithForLoop" : true,
+
"ReturnVoidInsteadOfEmptyTuple" : true,
+
"TypeNamesShouldBeCapitalized" : true,
+
"UseEarlyExits" : false,
+
"UseExplicitNilCheckInConditions" : true,
+
"UseLetInEveryBoundCaseVariable" : false,
+
"UseShorthandTypeNames" : true,
+
"UseSingleLinePropertyGetter" : true,
+
"UseSynthesizedInitializer" : true,
+
"UseTripleSlashForDocumentationComments" : true,
+
"UseWhereClausesInForLoops" : false,
+
"ValidateDocumentationComments" : false
+
},
+
"spacesAroundRangeFormationOperators" : false,
+
"spacesBeforeEndOfLineComments" : 2,
+
"version" : 1
+
}
+373
LICENSES/MPL-2.0.txt
···
+
Mozilla Public License Version 2.0
+
==================================
+
+
1. Definitions
+
--------------
+
+
1.1. "Contributor"
+
means each individual or legal entity that creates, contributes to
+
the creation of, or owns Covered Software.
+
+
1.2. "Contributor Version"
+
means the combination of the Contributions of others (if any) used
+
by a Contributor and that particular Contributor's Contribution.
+
+
1.3. "Contribution"
+
means Covered Software of a particular Contributor.
+
+
1.4. "Covered Software"
+
means Source Code Form to which the initial Contributor has attached
+
the notice in Exhibit A, the Executable Form of such Source Code
+
Form, and Modifications of such Source Code Form, in each case
+
including portions thereof.
+
+
1.5. "Incompatible With Secondary Licenses"
+
means
+
+
(a) that the initial Contributor has attached the notice described
+
in Exhibit B to the Covered Software; or
+
+
(b) that the Covered Software was made available under the terms of
+
version 1.1 or earlier of the License, but not also under the
+
terms of a Secondary License.
+
+
1.6. "Executable Form"
+
means any form of the work other than Source Code Form.
+
+
1.7. "Larger Work"
+
means a work that combines Covered Software with other material, in
+
a separate file or files, that is not Covered Software.
+
+
1.8. "License"
+
means this document.
+
+
1.9. "Licensable"
+
means having the right to grant, to the maximum extent possible,
+
whether at the time of the initial grant or subsequently, any and
+
all of the rights conveyed by this License.
+
+
1.10. "Modifications"
+
means any of the following:
+
+
(a) any file in Source Code Form that results from an addition to,
+
deletion from, or modification of the contents of Covered
+
Software; or
+
+
(b) any new file in Source Code Form that contains any Covered
+
Software.
+
+
1.11. "Patent Claims" of a Contributor
+
means any patent claim(s), including without limitation, method,
+
process, and apparatus claims, in any patent Licensable by such
+
Contributor that would be infringed, but for the grant of the
+
License, by the making, using, selling, offering for sale, having
+
made, import, or transfer of either its Contributions or its
+
Contributor Version.
+
+
1.12. "Secondary License"
+
means either the GNU General Public License, Version 2.0, the GNU
+
Lesser General Public License, Version 2.1, the GNU Affero General
+
Public License, Version 3.0, or any later versions of those
+
licenses.
+
+
1.13. "Source Code Form"
+
means the form of the work preferred for making modifications.
+
+
1.14. "You" (or "Your")
+
means an individual or a legal entity exercising rights under this
+
License. For legal entities, "You" includes any entity that
+
controls, is controlled by, or is under common control with You. For
+
purposes of this definition, "control" means (a) the power, direct
+
or indirect, to cause the direction or management of such entity,
+
whether by contract or otherwise, or (b) ownership of more than
+
fifty percent (50%) of the outstanding shares or beneficial
+
ownership of such entity.
+
+
2. License Grants and Conditions
+
--------------------------------
+
+
2.1. Grants
+
+
Each Contributor hereby grants You a world-wide, royalty-free,
+
non-exclusive license:
+
+
(a) under intellectual property rights (other than patent or trademark)
+
Licensable by such Contributor to use, reproduce, make available,
+
modify, display, perform, distribute, and otherwise exploit its
+
Contributions, either on an unmodified basis, with Modifications, or
+
as part of a Larger Work; and
+
+
(b) under Patent Claims of such Contributor to make, use, sell, offer
+
for sale, have made, import, and otherwise transfer either its
+
Contributions or its Contributor Version.
+
+
2.2. Effective Date
+
+
The licenses granted in Section 2.1 with respect to any Contribution
+
become effective for each Contribution on the date the Contributor first
+
distributes such Contribution.
+
+
2.3. Limitations on Grant Scope
+
+
The licenses granted in this Section 2 are the only rights granted under
+
this License. No additional rights or licenses will be implied from the
+
distribution or licensing of Covered Software under this License.
+
Notwithstanding Section 2.1(b) above, no patent license is granted by a
+
Contributor:
+
+
(a) for any code that a Contributor has removed from Covered Software;
+
or
+
+
(b) for infringements caused by: (i) Your and any other third party's
+
modifications of Covered Software, or (ii) the combination of its
+
Contributions with other software (except as part of its Contributor
+
Version); or
+
+
(c) under Patent Claims infringed by Covered Software in the absence of
+
its Contributions.
+
+
This License does not grant any rights in the trademarks, service marks,
+
or logos of any Contributor (except as may be necessary to comply with
+
the notice requirements in Section 3.4).
+
+
2.4. Subsequent Licenses
+
+
No Contributor makes additional grants as a result of Your choice to
+
distribute the Covered Software under a subsequent version of this
+
License (see Section 10.2) or under the terms of a Secondary License (if
+
permitted under the terms of Section 3.3).
+
+
2.5. Representation
+
+
Each Contributor represents that the Contributor believes its
+
Contributions are its original creation(s) or it has sufficient rights
+
to grant the rights to its Contributions conveyed by this License.
+
+
2.6. Fair Use
+
+
This License is not intended to limit any rights You have under
+
applicable copyright doctrines of fair use, fair dealing, or other
+
equivalents.
+
+
2.7. Conditions
+
+
Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted
+
in Section 2.1.
+
+
3. Responsibilities
+
-------------------
+
+
3.1. Distribution of Source Form
+
+
All distribution of Covered Software in Source Code Form, including any
+
Modifications that You create or to which You contribute, must be under
+
the terms of this License. You must inform recipients that the Source
+
Code Form of the Covered Software is governed by the terms of this
+
License, and how they can obtain a copy of this License. You may not
+
attempt to alter or restrict the recipients' rights in the Source Code
+
Form.
+
+
3.2. Distribution of Executable Form
+
+
If You distribute Covered Software in Executable Form then:
+
+
(a) such Covered Software must also be made available in Source Code
+
Form, as described in Section 3.1, and You must inform recipients of
+
the Executable Form how they can obtain a copy of such Source Code
+
Form by reasonable means in a timely manner, at a charge no more
+
than the cost of distribution to the recipient; and
+
+
(b) You may distribute such Executable Form under the terms of this
+
License, or sublicense it under different terms, provided that the
+
license for the Executable Form does not attempt to limit or alter
+
the recipients' rights in the Source Code Form under this License.
+
+
3.3. Distribution of a Larger Work
+
+
You may create and distribute a Larger Work under terms of Your choice,
+
provided that You also comply with the requirements of this License for
+
the Covered Software. If the Larger Work is a combination of Covered
+
Software with a work governed by one or more Secondary Licenses, and the
+
Covered Software is not Incompatible With Secondary Licenses, this
+
License permits You to additionally distribute such Covered Software
+
under the terms of such Secondary License(s), so that the recipient of
+
the Larger Work may, at their option, further distribute the Covered
+
Software under the terms of either this License or such Secondary
+
License(s).
+
+
3.4. Notices
+
+
You may not remove or alter the substance of any license notices
+
(including copyright notices, patent notices, disclaimers of warranty,
+
or limitations of liability) contained within the Source Code Form of
+
the Covered Software, except that You may alter any license notices to
+
the extent required to remedy known factual inaccuracies.
+
+
3.5. Application of Additional Terms
+
+
You may choose to offer, and to charge a fee for, warranty, support,
+
indemnity or liability obligations to one or more recipients of Covered
+
Software. However, You may do so only on Your own behalf, and not on
+
behalf of any Contributor. You must make it absolutely clear that any
+
such warranty, support, indemnity, or liability obligation is offered by
+
You alone, and You hereby agree to indemnify every Contributor for any
+
liability incurred by such Contributor as a result of warranty, support,
+
indemnity or liability terms You offer. You may include additional
+
disclaimers of warranty and limitations of liability specific to any
+
jurisdiction.
+
+
4. Inability to Comply Due to Statute or Regulation
+
---------------------------------------------------
+
+
If it is impossible for You to comply with any of the terms of this
+
License with respect to some or all of the Covered Software due to
+
statute, judicial order, or regulation then You must: (a) comply with
+
the terms of this License to the maximum extent possible; and (b)
+
describe the limitations and the code they affect. Such description must
+
be placed in a text file included with all distributions of the Covered
+
Software under this License. Except to the extent prohibited by statute
+
or regulation, such description must be sufficiently detailed for a
+
recipient of ordinary skill to be able to understand it.
+
+
5. Termination
+
--------------
+
+
5.1. The rights granted under this License will terminate automatically
+
if You fail to comply with any of its terms. However, if You become
+
compliant, then the rights granted under this License from a particular
+
Contributor are reinstated (a) provisionally, unless and until such
+
Contributor explicitly and finally terminates Your grants, and (b) on an
+
ongoing basis, if such Contributor fails to notify You of the
+
non-compliance by some reasonable means prior to 60 days after You have
+
come back into compliance. Moreover, Your grants from a particular
+
Contributor are reinstated on an ongoing basis if such Contributor
+
notifies You of the non-compliance by some reasonable means, this is the
+
first time You have received notice of non-compliance with this License
+
from such Contributor, and You become compliant prior to 30 days after
+
Your receipt of the notice.
+
+
5.2. If You initiate litigation against any entity by asserting a patent
+
infringement claim (excluding declaratory judgment actions,
+
counter-claims, and cross-claims) alleging that a Contributor Version
+
directly or indirectly infringes any patent, then the rights granted to
+
You by any and all Contributors for the Covered Software under Section
+
2.1 of this License shall terminate.
+
+
5.3. In the event of termination under Sections 5.1 or 5.2 above, all
+
end user license agreements (excluding distributors and resellers) which
+
have been validly granted by You or Your distributors under this License
+
prior to termination shall survive termination.
+
+
************************************************************************
+
* *
+
* 6. Disclaimer of Warranty *
+
* ------------------------- *
+
* *
+
* Covered Software is provided under this License on an "as is" *
+
* basis, without warranty of any kind, either expressed, implied, or *
+
* statutory, including, without limitation, warranties that the *
+
* Covered Software is free of defects, merchantable, fit for a *
+
* particular purpose or non-infringing. The entire risk as to the *
+
* quality and performance of the Covered Software is with You. *
+
* Should any Covered Software prove defective in any respect, You *
+
* (not any Contributor) assume the cost of any necessary servicing, *
+
* repair, or correction. This disclaimer of warranty constitutes an *
+
* essential part of this License. No use of any Covered Software is *
+
* authorized under this License except under this disclaimer. *
+
* *
+
************************************************************************
+
+
************************************************************************
+
* *
+
* 7. Limitation of Liability *
+
* -------------------------- *
+
* *
+
* Under no circumstances and under no legal theory, whether tort *
+
* (including negligence), contract, or otherwise, shall any *
+
* Contributor, or anyone who distributes Covered Software as *
+
* permitted above, be liable to You for any direct, indirect, *
+
* special, incidental, or consequential damages of any character *
+
* including, without limitation, damages for lost profits, loss of *
+
* goodwill, work stoppage, computer failure or malfunction, or any *
+
* and all other commercial damages or losses, even if such party *
+
* shall have been informed of the possibility of such damages. This *
+
* limitation of liability shall not apply to liability for death or *
+
* personal injury resulting from such party's negligence to the *
+
* extent applicable law prohibits such limitation. Some *
+
* jurisdictions do not allow the exclusion or limitation of *
+
* incidental or consequential damages, so this exclusion and *
+
* limitation may not apply to You. *
+
* *
+
************************************************************************
+
+
8. Litigation
+
-------------
+
+
Any litigation relating to this License may be brought only in the
+
courts of a jurisdiction where the defendant maintains its principal
+
place of business and such litigation shall be governed by laws of that
+
jurisdiction, without reference to its conflict-of-law provisions.
+
Nothing in this Section shall prevent a party's ability to bring
+
cross-claims or counter-claims.
+
+
9. Miscellaneous
+
----------------
+
+
This License represents the complete agreement concerning the subject
+
matter hereof. If any provision of this License is held to be
+
unenforceable, such provision shall be reformed only to the extent
+
necessary to make it enforceable. Any law or regulation which provides
+
that the language of a contract shall be construed against the drafter
+
shall not be used to construe this License against a Contributor.
+
+
10. Versions of the License
+
---------------------------
+
+
10.1. New Versions
+
+
Mozilla Foundation is the license steward. Except as provided in Section
+
10.3, no one other than the license steward has the right to modify or
+
publish new versions of this License. Each version will be given a
+
distinguishing version number.
+
+
10.2. Effect of New Versions
+
+
You may distribute the Covered Software under the terms of the version
+
of the License under which You originally received the Covered Software,
+
or under the terms of any subsequent version published by the license
+
steward.
+
+
10.3. Modified Versions
+
+
If you create software not governed by this License, and you want to
+
create a new license for such software, you may create and use a
+
modified version of this License if you rename the license and remove
+
any references to the name of the license steward (except to note that
+
such modified license differs from this License).
+
+
10.4. Distributing Source Code Form that is Incompatible With Secondary
+
Licenses
+
+
If You choose to distribute Source Code Form that is Incompatible With
+
Secondary Licenses under the terms of this version of the License, the
+
notice described in Exhibit B of this License must be attached.
+
+
Exhibit A - Source Code Form License Notice
+
-------------------------------------------
+
+
This Source Code Form is subject to the terms of the Mozilla Public
+
License, v. 2.0. If a copy of the MPL was not distributed with this
+
file, You can obtain one at https://mozilla.org/MPL/2.0/.
+
+
If it is not possible or desirable to put the notice in a particular
+
file, then You may include the notice in a location (such as a LICENSE
+
file in a relevant directory) where a recipient would be likely to look
+
for such a notice.
+
+
You may add additional accurate notices of copyright ownership.
+
+
Exhibit B - "Incompatible With Secondary Licenses" Notice
+
---------------------------------------------------------
+
+
This Source Code Form is "Incompatible With Secondary Licenses", as
+
defined by the Mozilla Public License, v. 2.0.
+30
Package.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
// swift-tools-version: 6.2
+
// The swift-tools-version declares the minimum version of Swift required to build this package.
+
+
import PackageDescription
+
+
let package = Package(
+
name: "PterodactylKernel",
+
products: [
+
// Products define the executables and libraries a package produces, making them visible to other packages.
+
.library(
+
name: "PterodactylKernel",
+
targets: ["PterodactylKernel"]
+
)
+
],
+
targets: [
+
// Targets are the basic building blocks of a package, defining a module or a test suite.
+
// Targets can depend on other targets in this package and products from dependencies.
+
.target(
+
name: "PterodactylKernel",
+
),
+
.testTarget(
+
name: "PterodactylKernelTests",
+
dependencies: ["PterodactylKernel"]
+
)
+
]
+
)
+29
Sources/PterodactylKernel/Control/AsyncThunk.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
import Foundation
+
+
actor AsyncThunk<Value> {
+
private var storage: Value?
+
private var thunk: (() async -> Value)?
+
+
public init(thunk: @escaping @Sendable () async -> Value) {
+
self.thunk = thunk
+
}
+
+
public init(value: Value) {
+
self.storage = value
+
}
+
+
public func value() async -> Value {
+
if let storage { return storage }
+
if let thunk {
+
let computed = await thunk()
+
self.storage = computed
+
self.thunk = nil
+
return computed
+
}
+
fatalError("AsyncThunk has neither thunk nor storage.")
+
}
+
}
+28
Sources/PterodactylKernel/Core Types/FieldDict.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
import Foundation
+
+
struct FieldDict<Value> {
+
public let elements: [(String, Value)]
+
+
init(_ dict: [(String, Value)]) {
+
self.elements = dict
+
}
+
+
subscript(key: String) -> Value? {
+
elements.first { $0.0 == key }?.1
+
}
+
}
+
+
extension FieldDict: Sendable where Value: Sendable {}
+
+
extension FieldDict {
+
func map<U>(_ f: (Value) -> U) -> FieldDict<U> {
+
let dict = elements.map { (k, v) in
+
(k, f(v))
+
}
+
return FieldDict<U>(dict)
+
}
+
}
+35
Sources/PterodactylKernel/Core Types/Term.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
typealias Name = String
+
+
indirect enum Term: Sendable {
+
case local(index: Int)
+
case global(name: Name)
+
case fun(dom: AsyncThunk<Type_>, boundName: String?, body: Term)
+
case record(boundName: String?, fields: FieldDict<FieldImpl>)
+
case cut(term: Term, frame: Frame)
+
}
+
+
extension Term {
+
indirect enum Type_: Sendable {
+
case funType(dom: Type_, boundName: String?, fam: Type_)
+
case recordType(boundName: String?, fields: FieldDict<FieldSpec>)
+
}
+
+
indirect enum Frame {
+
case app(arg: Term)
+
case proj(fieldName: String)
+
}
+
+
struct FieldSpec {
+
let type: Type_
+
let manifest: Term?
+
}
+
+
struct FieldImpl {
+
let type: Type_
+
let value: Term
+
}
+
}
+59
Sources/PterodactylKernel/Core Types/Value.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
struct Closure<Body>{
+
let evaluator: Evaluator
+
let body: Body
+
}
+
+
extension Closure: Sendable where Body: Sendable {}
+
+
indirect enum Value: Sendable {
+
case shift(neutral: Neutral)
+
case fun(dom: AsyncThunk<Type_>, boundName: String?, closure: Closure<Term>)
+
case record(boundName: String?, fields: FieldDict<FieldImpl>)
+
}
+
+
extension Value {
+
indirect enum Type_: Sendable {
+
case funType(dom: Type_, boundName: String?, fam: Closure<Term.Type_>)
+
case recordType(boundName: String?, fields: FieldDict<FieldSpec>)
+
}
+
+
struct FieldSpec {
+
let type: Closure<Term.Type_>
+
let manifest: Closure<Term>?
+
}
+
+
struct FieldImpl {
+
let type: Closure<Term.Type_>
+
let value: Closure<Term>
+
}
+
+
indirect enum Frame {
+
case app(arg: Value)
+
case proj(fieldName: String)
+
}
+
+
typealias Spine = [Frame]
+
+
enum Head {
+
case local(level: Int)
+
case global(name: Name)
+
}
+
+
struct Neutral {
+
let head: Head
+
let spine: Spine
+
let boundary: AsyncThunk<Boundary>
+
}
+
+
struct Boundary {
+
let type: Type_
+
let value: Value?
+
}
+
}
+
+
+
+85
Sources/PterodactylKernel/Evaluator.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
struct Evaluator {
+
let globals: [Name: Value]
+
let locals: [Value]
+
+
func extendedBy(value: Value) -> Self {
+
Self(globals: globals, locals: CollectionOfOne(value) + locals)
+
}
+
+
func close<Body>(body: Body) -> Closure<Body> {
+
Closure(evaluator: self, body: body)
+
}
+
+
func close(fieldSpec: Term.FieldSpec) -> Value.FieldSpec {
+
Value.FieldSpec(
+
type: close(body: fieldSpec.type),
+
manifest: fieldSpec.manifest.map(close(body:))
+
)
+
}
+
+
func close(fieldImpl: Term.FieldImpl) -> Value.FieldImpl {
+
Value.FieldImpl(
+
type: close(body: fieldImpl.type),
+
value: close(body: fieldImpl.value)
+
)
+
}
+
+
func evaluate(frame: Term.Frame) -> Value.Frame {
+
switch frame {
+
case let .app(arg: arg): .app(arg: evaluate(term: arg))
+
case let .proj(fieldName: fieldName): .proj(fieldName: fieldName)
+
}
+
}
+
+
func evaluate(term: Term) -> Value {
+
switch term {
+
case let .local(index: index):
+
return locals[index]
+
case let .global(name: name):
+
return globals[name]!
+
case let .cut(term: term, frame: frame):
+
return evaluate(term: term)
+
.plug(frame: evaluate(frame: frame))
+
case let .fun(dom: dom, boundName: boundName, body: body):
+
return .fun(
+
dom: AsyncThunk { await evaluate(type: dom.value()) },
+
boundName: boundName,
+
closure: close(body: body)
+
)
+
case let .record(boundName: boundName, fields: fields):
+
return .record(
+
boundName: boundName,
+
fields: fields.map(close(fieldImpl:))
+
)
+
}
+
}
+
+
func evaluate(type: Term.Type_) -> Value.Type_ {
+
switch type {
+
case let .funType(dom: dom, boundName: boundName, fam: fam):
+
.funType(
+
dom: evaluate(type: dom),
+
boundName: boundName,
+
fam: close(body: fam)
+
)
+
case let .recordType(boundName: boundName, fields: fields):
+
.recordType(boundName: boundName, fields: fields.map(close(fieldSpec:)))
+
}
+
}
+
}
+
+
extension Closure where Body == Term {
+
func instantiate(with value: Value) -> Value {
+
evaluator.extendedBy(value: value).evaluate(term: body)
+
}
+
}
+
+
extension Closure where Body == Term.Type_ {
+
func instantiate(with value: Value) -> Value.Type_ {
+
evaluator.extendedBy(value: value).evaluate(type: body)
+
}
+
}
+67
Sources/PterodactylKernel/Plug.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
protocol Plug {
+
func plug(frame: Value.Frame) -> Self
+
}
+
+
+
extension Plug {
+
func plug(spine: Value.Spine) -> Self {
+
spine.reduce(self) { partialResult, frame in
+
partialResult.plug(frame: frame)
+
}
+
}
+
}
+
+
extension Value: Plug {
+
func plug(frame: Frame) -> Self {
+
switch self {
+
case let .fun(_, _, closure: closure):
+
guard case let .app(arg: arg) = frame else { fatalError() }
+
return closure.instantiate(with: arg)
+
case let .record(_, fields: fields):
+
guard case let .proj(fieldName) = frame else { fatalError() }
+
guard let impl = fields[fieldName] else { fatalError() }
+
return impl.value.instantiate(with: self)
+
case let .shift(neutral: neutral):
+
return .shift(neutral: neutral.plug(frame: frame))
+
}
+
}
+
}
+
+
extension Value.Neutral: Plug {
+
// Not async now, but might need to be later.
+
func plug(boundary: Value.Boundary, frame: Value.Frame) async -> Value.Boundary {
+
switch boundary.type {
+
case let .funType(_, _, fam: fam):
+
guard case let .app(arg: arg) = frame else {
+
fatalError("Attempted to plug element of function type into invalid frame")
+
}
+
let fibre = fam.instantiate(with: arg)
+
return Value.Boundary(type: fibre, value: boundary.value?.plug(frame: frame))
+
+
case let .recordType(_, fields: fields):
+
guard case let .proj(fieldName) = frame else {
+
fatalError("Attempted to plug element of record type into invalid frame")
+
}
+
guard let field = fields[fieldName] else {
+
fatalError("Attempted to project invalid field from element of record type")
+
}
+
let fieldTypeValue = field.type.instantiate(with: .shift(neutral: self))
+
let value = boundary.value?.plug(frame: frame) ?? field.manifest.map { manifest in
+
manifest.instantiate(with: .shift(neutral: self))
+
}
+
return Value.Boundary(type: fieldTypeValue, value: value)
+
}
+
}
+
+
func plug(frame: Value.Frame) -> Self {
+
Self(
+
head: head,
+
spine: CollectionOfOne(frame) + spine,
+
boundary: AsyncThunk { await plug(boundary: boundary.value(), frame: frame) }
+
)
+
}
+
}
+3
Sources/PterodactylKernel/PterodactylKernel.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+133
Sources/PterodactylKernel/Quotation.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
import Foundation
+
+
struct Quotation {
+
let depth: Int
+
var next: Self {
+
Quotation(depth: depth + 1)
+
}
+
+
func quote(type: Value.Type_) -> Term.Type_ {
+
switch type {
+
case let .funType(dom: dom, boundName: boundName, fam: fam):
+
return .funType(
+
dom: quote(type: dom),
+
boundName: boundName,
+
fam: quote(dom: AsyncThunk(value: dom), family: fam)
+
)
+
+
case let .recordType(boundName: boundName, fields: fields):
+
var fieldSpecs: [(String, Value.FieldSpec)] = []
+
var quotedFieldSpecs: [(String, Term.FieldSpec)] = []
+
+
for (key, fieldSpec) in fields.elements {
+
let dom: AsyncThunk<Value.Type_> = AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs)))
+
let quotedFieldSpec = quote(dom: dom, fieldSpec: fieldSpec)
+
fieldSpecs.append((key, fieldSpec))
+
quotedFieldSpecs.append((key, quotedFieldSpec))
+
}
+
+
return .recordType(
+
boundName: boundName,
+
fields: FieldDict(quotedFieldSpecs)
+
)
+
}
+
}
+
+
func quote(dom: AsyncThunk<Value.Type_>, fieldSpec: Value.FieldSpec) -> Term.FieldSpec {
+
return Term.FieldSpec(
+
type: quote(dom: dom, family: fieldSpec.type),
+
manifest: fieldSpec.manifest.map { quote(dom: dom, closure: $0) }
+
)
+
}
+
+
func quote(dom: AsyncThunk<Value.Type_>, fieldImpl: Value.FieldImpl) -> Term.FieldImpl {
+
return Term.FieldImpl(
+
type: quote(dom: dom, family: fieldImpl.type),
+
value: quote(dom: dom, closure: fieldImpl.value)
+
)
+
}
+
+
func quote(value: Value) -> Term {
+
switch value {
+
case let .shift(neutral: neutral):
+
return quote(neutral: neutral)
+
+
case let .fun(dom: dom, boundName: boundName, closure: closure):
+
return .fun(
+
dom: AsyncThunk { await quote(type: dom.value()) },
+
boundName: boundName,
+
body: quote(dom: dom, closure: closure)
+
)
+
+
case let .record(boundName: boundName, fields: fields):
+
var fieldSpecs: [(String, Value.FieldSpec)] = []
+
var quotedFields: [(String, Term.FieldImpl)] = []
+
+
for (key, fieldImpl) in fields.elements {
+
let fieldSpec = Value.FieldSpec(type: fieldImpl.type, manifest: fieldImpl.value)
+
let quotedFieldImpl = quote(
+
dom: AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs))),
+
fieldImpl: fieldImpl
+
)
+
+
fieldSpecs.append((key, fieldSpec))
+
quotedFields.append((key, quotedFieldImpl))
+
}
+
+
return .record(boundName: boundName, fields: FieldDict(quotedFields))
+
}
+
}
+
+
func fresh(type: AsyncThunk<Value.Type_>) -> Value {
+
let boundary: AsyncThunk<Value.Boundary> = AsyncThunk {
+
await Value.Boundary(type: type.value(), value: nil)
+
}
+
+
return Value.shift(
+
neutral: Value.Neutral(
+
head: .local(level: depth),
+
spine: [],
+
boundary: boundary
+
)
+
)
+
}
+
+
func quote(dom: AsyncThunk<Value.Type_>, closure: Closure<Term>) -> Term {
+
let x = fresh(type: dom)
+
let value = closure.instantiate(with: x)
+
return next.quote(value: value)
+
}
+
+
func quote(dom: AsyncThunk<Value.Type_>, family: Closure<Term.Type_>) -> Term.Type_ {
+
let x = fresh(type: dom)
+
let value = family.instantiate(with: x)
+
return next.quote(type: value)
+
}
+
+
private func quote(head: Value.Head) -> Term {
+
switch head {
+
case let .local(level: level): .local(index: depth - level - 1)
+
case let .global(name: name): .global(name: name)
+
}
+
}
+
+
private func quote(frame: Value.Frame) -> Term.Frame {
+
switch frame {
+
case let .app(arg: arg):
+
return .app(arg: quote(value: arg))
+
case let .proj(fieldName: fieldName):
+
return .proj(fieldName: fieldName)
+
}
+
}
+
+
private func quote(neutral: Value.Neutral) -> Term {
+
let headTerm = quote(head: neutral.head)
+
return neutral.spine.reduce(headTerm) { term, frame in
+
.cut(term: term, frame: quote(frame: frame))
+
}
+
}
+
}
+12
Sources/PterodactylKernel/Whnf.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
extension Value {
+
func whnf() async -> Value {
+
switch self {
+
case .fun, .record : self
+
case let .shift(neutral: neutral): await neutral.boundary.value().value ?? self
+
}
+
}
+
}
+11
Tests/PterodactylKernelTests/PterodactylKernelTests.swift
···
+
// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
+
//
+
// SPDX-License-Identifier: MPL-2.0
+
+
import Testing
+
+
@testable import PterodactylKernel
+
+
@Test func example() async throws {
+
// Write your test here and use APIs like `#expect(...)` to check expected conditions.
+
}