commit b7856f21730696a72f7e0e38f69958cf477ef876 · jonmsterling.com/swift-pterodactyl

+1 -1

Sources/PterodactylKernel/Control/AsyncThunk.swift

···

       4
        
       

     

       5
        
       import Foundation

     

       6
        
       

     

       7
       -
       actor AsyncThunk<Value> {

     

       8
        
       	private var storage: Value?

     

       9
        
       	private var thunk: (() async -> Value)?

     

       10

···

       4
        
       

     

       5
        
       import Foundation

     

       6
        
       

     

       7
       +
       public actor AsyncThunk<Value> {

     

       8
        
       	private var storage: Value?

     

       9
        
       	private var thunk: (() async -> Value)?

     

       10

+4 -2

Sources/PterodactylKernel/Core Types/FieldDict.swift

···

       4
        
       

     

       5
        
       import Foundation

     

       6
        
       

     

       7
       -
       struct FieldDict<Value> {

     

       0
        
       
     

       8
        
       	public let elements: [(String, Value)]

     

       0
        
       
     

       9
        
       

     

       10
        
       	init(_ dict: [(String, Value)]) {

     

       11
        
       		self.elements = dict

     
···

       14
        
       	subscript(key: String) -> Value? {

     

       15
        
       		elements.first { $0.0 == key }?.1

     

       16
        
       	}

     

       17
       -
       	

     

       18
        
       	func prefix(until: String) -> Self {

     

       19
        
       		var prefix: [(String, Value)] = []

     

       20
        
       		for (key, value) in elements {

···

       4
        
       

     

       5
        
       import Foundation

     

       6
        
       

     

       7
       +
       // TODO: This might be rewritten. The goal is to provide a dictionary that I can easily construct and traverse in order. Maybe ordered dictionaries from swift-collections?

     

       8
       +
       public struct FieldDict<Value> {

     

       9
        
       	public let elements: [(String, Value)]

     

       10
       +
       	var keys: [String] { elements.map(\.0) }

     

       11
        
       

     

       12
        
       	init(_ dict: [(String, Value)]) {

     

       13
        
       		self.elements = dict

     
···

       16
        
       	subscript(key: String) -> Value? {

     

       17
        
       		elements.first { $0.0 == key }?.1

     

       18
        
       	}

     

       19
       +
       

     

       20
        
       	func prefix(until: String) -> Self {

     

       21
        
       		var prefix: [(String, Value)] = []

     

       22
        
       		for (key, value) in elements {

+36

Sources/PterodactylKernel/Core Types/Size.swift

···

       1
       +
       // SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers

     

       2
       +
       //

     

       3
       +
       // SPDX-License-Identifier: MPL-2.0

     

       4
       +
       

     

       5
       +
       import Foundation

     

       6
       +
       

     

       7
       +
       /// Pterodactyl has two sizes of small things: little and moderate. Beyond these, we have things that are not types but rather “type schemes”.

     

       8
       +
       public enum Size<Universe> {

     

       9
       +
       	/// A “little” thing is something classified by a universe. Universes form a countable hierarchy.

     

       10
       +
       	case little(universe: Universe)

     

       11
       +
       	

     

       12
       +
       	/// A “moderate” type is something classified by `Type`.

     

       13
       +
       	case moderate

     

       14
       +
       }

     

       15
       +
       

     

       16
       +
       

     

       17
       +
       extension Size: Sendable where Universe: Sendable {}

     

       18
       +
       

     

       19
       +
       extension Size: Equatable where Universe == () {

     

       20
       +
       	public static func == (lhs: Size<Universe>, rhs: Size<Universe>) -> Bool {

     

       21
       +
       		switch (lhs, rhs) {

     

       22
       +
       		case (.little, .little): true

     

       23
       +
       		case (.moderate, .moderate): true

     

       24
       +
       		default: false

     

       25
       +
       		}

     

       26
       +
       	}

     

       27
       +
       }

     

       28
       +
       

     

       29
       +
       extension Size {

     

       30
       +
       	func map<U>(_ f: (Universe) -> U) -> Size<U> {

     

       31
       +
       		switch self {

     

       32
       +
       		case let .little(universe: universe): .little(universe: f(universe))

     

       33
       +
       		case .moderate: .moderate

     

       34
       +
       		}

     

       35
       +
       	}

     

       36
       +
       }

+28 -7

Sources/PterodactylKernel/Core Types/Term.swift

···

       2
        
       //

     

       3
        
       // SPDX-License-Identifier: MPL-2.0

     

       4
        
       

     

       5
       -
       typealias Name = String

     

       6
        
       

     

       7
       -
       indirect enum Term: Sendable {

     

       0
        
       
     

       0
        
       
     

       8
        
       	case local(index: Int)

     

       0
        
       
     

       0
        
       
     

       9
        
       	case global(name: Name)

     

       0
        
       
     

       0
        
       
     

       10
        
       	case fun(dom: AsyncThunk<Type_>, boundName: String?, body: Term)

     

       0
        
       
     

       0
        
       
     

       11
        
       	case record(boundName: String?, fields: FieldDict<FieldImpl>)

     

       0
        
       
     

       0
        
       
     

       12
        
       	case cut(term: Term, frame: Frame)

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       13
        
       }

     

       14
        
       

     

       15
        
       extension Term {

     

       16
       -
       	indirect enum Type_: Sendable {

     

       17
        
       		case funType(dom: Type_, boundName: String?, fam: Type_)

     

       18
        
       		case recordType(boundName: String?, fields: FieldDict<FieldSpec>)

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       19
        
       	}

     

       20
        
       	

     

       21
       -
       	indirect enum Frame {

     

       22
        
       		case app(arg: Term)

     

       23
        
       		case proj(fieldName: String)

     

       24
        
       	}

     

       25
        
       	

     

       26
       -
       	struct FieldSpec {

     

       27
        
       		let type: Type_

     

       28
        
       		let manifest: Term?

     

       29
        
       	}

     

       30
        
       	

     

       31
       -
       	struct TypedTerm {

     

       32
        
       		let type: Type_

     

       33
        
       		let term: Term

     

       34
        
       	}

     

       35
        
       	

     

       36
       -
       	struct FieldImpl {

     

       37
        
       		let type: Type_

     

       38
        
       		let value: Term

     

       39
        
       	}

···

       2
        
       //

     

       3
        
       // SPDX-License-Identifier: MPL-2.0

     

       4
        
       

     

       5
       +
       public typealias Name = String

     

       6
        
       

     

       7
       +
       public indirect enum Term: Sendable {

     

       8
       +
       	

     

       9
       +
       	/// A local variable, designated by a De Bruijn index.

     

       10
        
       	case local(index: Int)

     

       11
       +
       	

     

       12
       +
       	/// A global variable, designated by a `Name`.

     

       13
        
       	case global(name: Name)

     

       14
       +
       	

     

       15
       +
       	/// A (dependent) function.

     

       16
        
       	case fun(dom: AsyncThunk<Type_>, boundName: String?, body: Term)

     

       17
       +
       	

     

       18
       +
       	/// A (dependent) record.

     

       19
        
       	case record(boundName: String?, fields: FieldDict<FieldImpl>)

     

       20
       +
       	

     

       21
       +
       	/// A negative elimination-form (``Frame``) applied to a term.

     

       22
        
       	case cut(term: Term, frame: Frame)

     

       23
       +
       	

     

       24
       +
       	/// The canonical code of a small type.

     

       25
       +
       	case shrink(size: Size<Term>, type: Type_)

     

       26
       +
       	

     

       27
       +
       	case universeZero

     

       28
       +
       	case universeSucc(_ universe: Term)

     

       29
       +
       	case universeLub(_ universe1: Term, _ universe2: Term)

     

       30
        
       }

     

       31
        
       

     

       32
        
       extension Term {

     

       33
       +
       	public indirect enum Type_: Sendable {

     

       34
        
       		case funType(dom: Type_, boundName: String?, fam: Type_)

     

       35
        
       		case recordType(boundName: String?, fields: FieldDict<FieldSpec>)

     

       36
       +
       		case universeCodes(size: Size<Term>)

     

       37
       +
       		case decode(size: Size<()>, code: Term)

     

       38
       +
       		

     

       39
       +
       		case universeType

     

       40
        
       	}

     

       41
        
       	

     

       42
       +
       	public indirect enum Frame: Sendable {

     

       43
        
       		case app(arg: Term)

     

       44
        
       		case proj(fieldName: String)

     

       45
        
       	}

     

       46
        
       	

     

       47
       +
       	public struct FieldSpec: Sendable {

     

       48
        
       		let type: Type_

     

       49
        
       		let manifest: Term?

     

       50
        
       	}

     

       51
        
       	

     

       52
       +
       	public struct TypedTerm: Sendable {

     

       53
        
       		let type: Type_

     

       54
        
       		let term: Term

     

       55
        
       	}

     

       56
        
       	

     

       57
       +
       	public struct FieldImpl: Sendable {

     

       58
        
       		let type: Type_

     

       59
        
       		let value: Term

     

       60
        
       	}

+41 -12

Sources/PterodactylKernel/Core Types/Value.swift

···

       2
        
       //

     

       3
        
       // SPDX-License-Identifier: MPL-2.0

     

       4
        
       

     

       5
       -
       struct Closure<Body>{

     

       6
        
       	let evaluator: Evaluator

     

       7
        
       	let body: Body

     

       8
        
       }

     

       9
        
       

     

       10
        
       extension Closure: Sendable where Body: Sendable {}

     

       11
        
       

     

       12
       -
       indirect enum Value: Sendable {

     

       13
        
       	case shift(neutral: Neutral)

     

       14
        
       	case fun(dom: AsyncThunk<Type_>, boundName: String?, closure: Closure<Term>)

     

       15
        
       	case record(boundName: String?, fields: FieldDict<FieldImpl>)

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       16
        
       }

     

       17
        
       

     

       18
        
       extension Value {

     

       19
       -
       	indirect enum Type_: Sendable {

     

       20
        
       		case funType(dom: Type_, boundName: String?, fam: Closure<Term.Type_>)

     

       21
        
       		case recordType(boundName: String?, fields: FieldDict<FieldSpec>)

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       22
        
       	}

     

       23
       -
       	

     

       24
       -
       	struct FieldSpec {

     

       25
        
       		let type: Closure<Term.Type_>

     

       26
        
       		let manifest: Closure<Term>?

     

       27
        
       	}

     

       28
       -
       	

     

       29
       -
       	struct FieldImpl {

     

       30
        
       		let type: Closure<Term.Type_>

     

       31
        
       		let value: Closure<Term>

     

       32
        
       	}

     

       33
        
       

     

       34
       -
       	indirect enum Frame {

     

       0
        
       
     

       35
        
       		case app(arg: Value)

     

       36
        
       		case proj(fieldName: String)

     

       37
        
       	}

     

       38
        
       

     

       39
       -
       	typealias Spine = [Frame]

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       40
        
       

     

       41
       -
       	enum Head {

     

       0
        
       
     

       0
        
       
     

       42
        
       		case local(level: Int)

     

       43
        
       		case global(name: Name)

     

       44
        
       	}

     

       45
        
       

     

       46
       -
       	struct Neutral {

     

       47
        
       		let head: Head

     

       48
        
       		let spine: Spine

     

       49
        
       		let boundary: AsyncThunk<Boundary>

     
···

       56
        
       }

     

       57
        
       

     

       58
        
       

     

       59
       -
       

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0

···

       2
        
       //

     

       3
        
       // SPDX-License-Identifier: MPL-2.0

     

       4
        
       

     

       5
       +
       public struct Closure<Body> {

     

       6
        
       	let evaluator: Evaluator

     

       7
        
       	let body: Body

     

       8
        
       }

     

       9
        
       

     

       10
        
       extension Closure: Sendable where Body: Sendable {}

     

       11
        
       

     

       12
       +
       public indirect enum Value: Sendable {

     

       13
        
       	case shift(neutral: Neutral)

     

       14
        
       	case fun(dom: AsyncThunk<Type_>, boundName: String?, closure: Closure<Term>)

     

       15
        
       	case record(boundName: String?, fields: FieldDict<FieldImpl>)

     

       16
       +
       	

     

       17
       +
       	case shrink(size: Size<Value>, type: Type_)

     

       18
       +
       	

     

       19
       +
       	case universeZero

     

       20
       +
       	case universeSucc(_ universe: Value)

     

       21
       +
       	case universeLub(_ universe1: Value, _ universe2: Value)

     

       22
        
       }

     

       23
        
       

     

       24
        
       extension Value {

     

       25
       +
       	public indirect enum Type_: Sendable {

     

       26
        
       		case funType(dom: Type_, boundName: String?, fam: Closure<Term.Type_>)

     

       27
        
       		case recordType(boundName: String?, fields: FieldDict<FieldSpec>)

     

       28
       +
       		

     

       29
       +
       		/// The type of small universe levels.

     

       30
       +
       		case universeType

     

       31
       +
       		

     

       32
       +
       		/// The type of `S`-small type codes for a size `S`.

     

       33
       +
       		case universeCodes(size: Size<Value>)

     

       34
       +
       		

     

       35
       +
       		/// The decoding of a given `S`-small type code.

     

       36
       +
       		case decode(size: Size<()>, code: Neutral)

     

       37
        
       	}

     

       38
       +
       

     

       39
       +
       	public struct FieldSpec: Sendable {

     

       40
        
       		let type: Closure<Term.Type_>

     

       41
        
       		let manifest: Closure<Term>?

     

       42
        
       	}

     

       43
       +
       

     

       44
       +
       	public struct FieldImpl: Sendable {

     

       45
        
       		let type: Closure<Term.Type_>

     

       46
        
       		let value: Closure<Term>

     

       47
        
       	}

     

       48
        
       

     

       49
       +
       	// TODO: Kovacs makes the argument in an application frame lazy. Doing this would be a significant change, because it would make it necessary for the plugging operation to be asynchronous.

     

       50
       +
       	public indirect enum Frame: Sendable {

     

       51
        
       		case app(arg: Value)

     

       52
        
       		case proj(fieldName: String)

     

       53
        
       	}

     

       54
        
       

     

       55
       +
       	/// When a ``Neutral`` is plugged into a ``Frame``, the frame is enriched with further information before being placed on the spine.

     

       56
       +
       	public indirect enum RichFrame: Sendable {

     

       57
       +
       		case app(dom: AsyncThunk<Value.Type_>, arg: Value)

     

       58
       +
       		case proj(fieldName: String)

     

       59
       +
       	}

     

       60
        
       

     

       61
       +
       	public typealias Spine = [RichFrame]

     

       62
       +
       

     

       63
       +
       	public enum Head: Equatable, Sendable {

     

       64
        
       		case local(level: Int)

     

       65
        
       		case global(name: Name)

     

       66
        
       	}

     

       67
        
       

     

       68
       +
       	public struct Neutral: Sendable {

     

       69
        
       		let head: Head

     

       70
        
       		let spine: Spine

     

       71
        
       		let boundary: AsyncThunk<Boundary>

     
···

       78
        
       }

     

       79
        
       

     

       80
        
       

     

       81
       +
       extension Value.RichFrame {

     

       82
       +
       	var forget: Value.Frame {

     

       83
       +
       		switch self {

     

       84
       +
       		case let .app(dom: _, arg: arg): .app(arg: arg)

     

       85
       +
       		case let .proj(fieldName: fieldName): .proj(fieldName: fieldName)

     

       86
       +
       		}

     

       87
       +
       	}

     

       88
       +
       }

+37 -6

Sources/PterodactylKernel/Evaluator.swift

···

       5
        
       struct Evaluator {

     

       6
        
       	let globals: [Name: Term.TypedTerm]

     

       7
        
       	let locals: [Value]

     

       8
       -
       	

     

       9
       -
       	init(globals: [Name : Term.TypedTerm], locals: [Value]) {

     

       10
        
       		self.globals = globals

     

       11
        
       		self.locals = locals

     

       12
       -
       	}

     

       13
       -
       	

     

       14
       -
       	init() {

     

       15
       -
       		self.init(globals: [:], locals: [])

     

       16
        
       	}

     

       17
        
       

     

       18
        
       	func extendedBy(value: Value) -> Self {

     
···

       75
        
       				boundName: boundName,

     

       76
        
       				fields: fields.map(close(fieldImpl:))

     

       77
        
       			)

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       78
        
       		}

     

       79
        
       	}

     

       80
        
       

     
···

       86
        
       				boundName: boundName,

     

       87
        
       				fam: close(body: fam)

     

       88
        
       			)

     

       0
        
       
     

       89
        
       		case let .recordType(boundName: boundName, fields: fields):

     

       90
        
       			.recordType(boundName: boundName, fields: fields.map(close(fieldSpec:)))

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       91
        
       		}

     

       92
        
       	}

     

       93
        
       }

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       94
        
       

     

       95
        
       extension Closure where Body == Term {

     

       96
        
       	func instantiate(with value: Value) -> Value {

···

       5
        
       struct Evaluator {

     

       6
        
       	let globals: [Name: Term.TypedTerm]

     

       7
        
       	let locals: [Value]

     

       8
       +
       

     

       9
       +
       	public init(globals: [Name: Term.TypedTerm] = [:], locals: [Value] = []) {

     

       10
        
       		self.globals = globals

     

       11
        
       		self.locals = locals

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       12
        
       	}

     

       13
        
       

     

       14
        
       	func extendedBy(value: Value) -> Self {

     
···

       71
        
       				boundName: boundName,

     

       72
        
       				fields: fields.map(close(fieldImpl:))

     

       73
        
       			)

     

       74
       +
       		case let .shrink(size: size, type: type):

     

       75
       +
       			return .shrink(

     

       76
       +
       				size: size.map(evaluate(term:)),

     

       77
       +
       				type: evaluate(type: type)

     

       78
       +
       			)

     

       79
       +
       		case .universeZero:

     

       80
       +
       			return .universeZero

     

       81
       +
       		case let .universeSucc(universe: universe):

     

       82
       +
       			return .universeSucc(evaluate(term: universe))

     

       83
       +
       		case let .universeLub(universe1, universe2):

     

       84
       +
       			return .universeLub(

     

       85
       +
       				evaluate(term: universe1),

     

       86
       +
       				evaluate(term: universe2)

     

       87
       +
       			)

     

       88
        
       		}

     

       89
        
       	}

     

       90
        
       

     
···

       96
        
       				boundName: boundName,

     

       97
        
       				fam: close(body: fam)

     

       98
        
       			)

     

       99
       +
       

     

       100
        
       		case let .recordType(boundName: boundName, fields: fields):

     

       101
        
       			.recordType(boundName: boundName, fields: fields.map(close(fieldSpec:)))

     

       102
       +
       

     

       103
       +
       		case let .decode(size: size, code: code):

     

       104
       +
       			evaluate(term: code).decode(size: size)

     

       105
       +
       

     

       106
       +
       		case let .universeCodes(size: size):

     

       107
       +
       				.universeCodes(size: size.map(evaluate(term:)))

     

       108
       +
       

     

       109
       +
       		case .universeType:

     

       110
       +
       			.universeType

     

       111
        
       		}

     

       112
        
       	}

     

       113
        
       }

     

       114
       +
       

     

       115
       +
       extension Value {

     

       116
       +
       	func decode(size: Size<()>) -> Value.Type_ {

     

       117
       +
       		switch self {

     

       118
       +
       		case let .shrink(_, type: type): type

     

       119
       +
       		case let .shift(neutral: neutral): .decode(size: size, code: neutral)

     

       120
       +
       		default: fatalError()

     

       121
       +
       		}

     

       122
       +
       	}

     

       123
       +
       }

     

       124
       +
       

     

       125
        
       

     

       126
        
       extension Closure where Body == Term {

     

       127
        
       	func instantiate(with value: Value) -> Value {

+148

Sources/PterodactylKernel/Local Analysis/Equality.swift

···

       1
       +
       // SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers

     

       2
       +
       //

     

       3
       +
       // SPDX-License-Identifier: MPL-2.0

     

       4
       +
       

     

       5
       +
       import Foundation

     

       6
       +
       

     

       7
       +
       extension LocalAnalysis {

     

       8
       +
       	enum EqualityError: Error {

     

       9
       +
       		case values(lhs: Value, rhs: Value, type: Value.Type_)

     

       10
       +
       		case types(lhs: Value.Type_, rhs: Value.Type_)

     

       11
       +
       		case heads(lhs: Value.Head, rhs: Value.Head)

     

       12
       +
       		case frames(lhs: Value.RichFrame, rhs: Value.RichFrame)

     

       13
       +
       		case spines(lhs: Value.Spine, rhs: Value.Spine)

     

       14
       +
       	}

     

       15
       +
       

     

       16
       +
       	func equate(value lhs: Value, with rhs: Value, in type: Value.Type_) async throws {

     

       17
       +
       		switch await (lhs.whnf(), rhs.whnf(), type.whnf()) {

     

       18
       +
       		case (_, _, .universeType):

     

       19
       +
       			try await equate(size: .little(universe: lhs), with: .little(universe: rhs))

     

       20
       +
       

     

       21
       +
       		case let (lhs, rhs, .funType(dom: dom, boundName: _, fam: fam)):

     

       22
       +
       			let dom = AsyncThunk(value: dom)

     

       23
       +
       			let x = fresh(type: dom)

     

       24
       +
       			let frame = Value.Frame.app(arg: x)

     

       25
       +
       			let lhs = lhs.plug(frame: frame)

     

       26
       +
       			let rhs = rhs.plug(frame: frame)

     

       27
       +
       			let fibre = fam.instantiate(with: x)

     

       28
       +
       			try await next.equate(value: lhs, with: rhs, in: fibre)

     

       29
       +
       

     

       30
       +
       		case let (lhs, rhs, .recordType(boundName: boundName, fields: fields)):

     

       31
       +
       			var fieldImpls: [(String, Value.FieldImpl)] = []

     

       32
       +
       			for (key, field) in fields.elements {

     

       33
       +
       				let prefixRecord: Value = .record(boundName: boundName, fields: FieldDict(fieldImpls))

     

       34
       +
       				if field.manifest == nil {

     

       35
       +
       					let frame = Value.Frame.proj(fieldName: key)

     

       36
       +
       					let lhs = lhs.plug(frame: frame)

     

       37
       +
       					let rhs = rhs.plug(frame: frame)

     

       38
       +
       					let type = field.type.instantiate(with: prefixRecord)

     

       39
       +
       					try await equate(value: lhs, with: rhs, in: type)

     

       40
       +
       				}

     

       41
       +
       

     

       42
       +
       				let impl = Value.FieldImpl(

     

       43
       +
       					type: field.type,

     

       44
       +
       					value: Closure(

     

       45
       +
       						evaluator: Evaluator(),

     

       46
       +
       						body: .cut(

     

       47
       +
       							term: .local(index: 0),

     

       48
       +
       							frame: .proj(fieldName: key)

     

       49
       +
       						)

     

       50
       +
       					)

     

       51
       +
       				)

     

       52
       +
       				fieldImpls.append((key, impl))

     

       53
       +
       			}

     

       54
       +
       

     

       55
       +
       		case (_, _, .universeCodes):

     

       56
       +
       			try await equate(type: lhs.decode(size: .little(universe: ())), with: rhs.decode(size: .little(universe: ())))

     

       57
       +
       

     

       58
       +
       		case let (.shift(neutral: lhs), .shift(neutral: rhs), .decode):

     

       59
       +
       			try await equate(neutral: lhs, with: rhs)

     

       60
       +
       

     

       61
       +
       		default:

     

       62
       +
       			throw EqualityError.values(lhs: lhs, rhs: rhs, type: type)

     

       63
       +
       		}

     

       64
       +
       	}

     

       65
       +
       

     

       66
       +
       	func equate(type lhs: Value.Type_, with rhs: Value.Type_) async throws {

     

       67
       +
       		switch await (lhs.whnf(), rhs.whnf()) {

     

       68
       +
       

     

       69
       +
       		case let (.funType(dom: dom1, boundName: _, fam: fam1), .funType(dom: dom2, boundName: _, fam: fam2)):

     

       70
       +
       			try await equate(type: dom1, with: dom2)

     

       71
       +
       			let x = fresh(type: AsyncThunk(value: dom1))

     

       72
       +
       			let fibre1 = fam1.instantiate(with: x)

     

       73
       +
       			let fibre2 = fam2.instantiate(with: x)

     

       74
       +
       			try await next.equate(type: fibre1, with: fibre2)

     

       75
       +
       

     

       76
       +
       		case let (.recordType(boundName: boundName, fields: fields1), .recordType(boundName: _, fields: fields2)):

     

       77
       +
       			let error = EqualityError.types(lhs: lhs, rhs: rhs)

     

       78
       +
       			guard fields1.keys == fields2.keys else { throw error }

     

       79
       +
       

     

       80
       +
       			var fieldSpecs: [(String, Value.FieldSpec)] = []

     

       81
       +
       

     

       82
       +
       			for (key, field1) in fields1.elements {

     

       83
       +
       				let field2 = fields2[key]!

     

       84
       +
       				guard (field1.manifest == nil) == ((field2.manifest == nil)) else { throw error }

     

       85
       +
       

     

       86
       +
       				let prefixType: AsyncThunk<Value.Type_> = AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs)))

     

       87
       +
       				let x = fresh(type: prefixType)

     

       88
       +
       				let type1 = field1.type.instantiate(with: x)

     

       89
       +
       				let type2 = field2.type.instantiate(with: x)

     

       90
       +
       				try await next.equate(type: type1, with: type2)

     

       91
       +
       

     

       92
       +
       				if let manifest1 = field1.manifest, let manifest2 = field2.manifest {

     

       93
       +
       					let value1 = manifest1.instantiate(with: x)

     

       94
       +
       					let value2 = manifest2.instantiate(with: x)

     

       95
       +
       					try await next.equate(value: value1, with: value2, in: type1)

     

       96
       +
       				}

     

       97
       +
       

     

       98
       +
       				fieldSpecs.append((key, field1))

     

       99
       +
       			}

     

       100
       +
       

     

       101
       +
       		case (.universeType, .universeType): ()

     

       102
       +
       

     

       103
       +
       		case let (.decode(size: size1, code: neutral1), .decode(size: size2, code: neutral2)):

     

       104
       +
       			guard size1 == size2 else { throw EqualityError.types(lhs: lhs, rhs: rhs) }

     

       105
       +
       			try await equate(neutral: neutral1, with: neutral2)

     

       106
       +
       

     

       107
       +
       		case let (.universeCodes(size: lhs), .universeCodes(size: rhs)):

     

       108
       +
       			try await equate(size: lhs, with: rhs)

     

       109
       +
       

     

       110
       +
       		default:

     

       111
       +
       			throw EqualityError.types(lhs: lhs, rhs: rhs)

     

       112
       +
       		}

     

       113
       +
       	}

     

       114
       +
       

     

       115
       +
       	func equate(head lhs: Value.Head, with rhs: Value.Head) throws {

     

       116
       +
       		guard lhs == rhs else { throw EqualityError.heads(lhs: lhs, rhs: rhs) }

     

       117
       +
       	}

     

       118
       +
       

     

       119
       +
       	func equate(frame lhs: Value.RichFrame, with rhs: Value.RichFrame) async throws {

     

       120
       +
       		switch (lhs, rhs) {

     

       121
       +
       		case let (.proj(fieldName: fieldName1), .proj(fieldName: fieldName2)):

     

       122
       +
       			guard fieldName1 == fieldName2 else { throw EqualityError.frames(lhs: lhs, rhs: rhs) }

     

       123
       +
       		case let (.app(dom: dom1, arg: arg1), .app(dom: _, arg: arg2)):

     

       124
       +
       			try await equate(value: arg1, with: arg2, in: dom1.value())

     

       125
       +
       		default:

     

       126
       +
       			throw EqualityError.frames(lhs: lhs, rhs: rhs)

     

       127
       +
       		}

     

       128
       +
       	}

     

       129
       +
       

     

       130
       +
       	func equate(spine lhs: Value.Spine, with rhs: Value.Spine) async throws {

     

       131
       +
       		guard lhs.count == rhs.count else { throw EqualityError.spines(lhs: lhs, rhs: rhs) }

     

       132
       +
       

     

       133
       +
       		for (index, frame1) in lhs.enumerated() {

     

       134
       +
       			let frame2 = rhs[index]

     

       135
       +
       			try await equate(frame: frame1, with: frame2)

     

       136
       +
       		}

     

       137
       +
       	}

     

       138
       +
       

     

       139
       +
       	func equate(neutral lhs: Value.Neutral, with rhs: Value.Neutral) async throws {

     

       140
       +
       		try equate(head: lhs.head, with: rhs.head)

     

       141
       +
       		try await equate(spine: lhs.spine, with: rhs.spine)

     

       142
       +
       	}

     

       143
       +
       	

     

       144
       +
       	func equate(size lhs: Size<Value>, with rhs: Size<Value>) async throws {

     

       145
       +
       		try await assertLeq(size1: lhs, size2: rhs)

     

       146
       +
       		try await assertLeq(size1: rhs, size2: lhs)

     

       147
       +
       	}

     

       148
       +
       }

+31

Sources/PterodactylKernel/Local Analysis/LocalAnalysis.swift

···

       1
       +
       // SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers

     

       2
       +
       //

     

       3
       +
       // SPDX-License-Identifier: MPL-2.0

     

       4
       +
       

     

       5
       +
       import Foundation

     

       6
       +
       

     

       7
       +
       struct LocalAnalysis {

     

       8
       +
       	let depth: Int

     

       9
       +
       	

     

       10
       +
       	init(depth: Int = 0) {

     

       11
       +
       		self.depth = depth

     

       12
       +
       	}

     

       13
       +
       	

     

       14
       +
       	var next: Self {

     

       15
       +
       		Self(depth: depth + 1)

     

       16
       +
       	}

     

       17
       +
       	

     

       18
       +
       	func fresh(type: AsyncThunk<Value.Type_>) -> Value {

     

       19
       +
       		let boundary: AsyncThunk<Value.Boundary> = AsyncThunk {

     

       20
       +
       			await Value.Boundary(type: type.value(), value: nil)

     

       21
       +
       		}

     

       22
       +
       

     

       23
       +
       		return Value.shift(

     

       24
       +
       			neutral: Value.Neutral(

     

       25
       +
       				head: .local(level: depth),

     

       26
       +
       				spine: [],

     

       27
       +
       				boundary: boundary

     

       28
       +
       			)

     

       29
       +
       		)

     

       30
       +
       	}

     

       31
       +
       }

+33 -13

Sources/PterodactylKernel/Plug.swift

···

       10
        
       extension Plug {

     

       11
        
       	func plug(spine: Value.Spine) -> Self {

     

       12
        
       		spine.reduce(self) { partialResult, frame in

     

       13
       -
       			partialResult.plug(frame: frame)

     

       14
        
       		}

     

       15
        
       	}

     

       16
        
       }

     
···

       27
        
       			return impl.value.instantiate(with: self)

     

       28
        
       		case let .shift(neutral: neutral):

     

       29
        
       			return .shift(neutral: neutral.plug(frame: frame))

     

       0
        
       
     

       0
        
       
     

       30
        
       		}

     

       31
        
       	}

     

       32
        
       }

     

       33
        
       

     

       34
        
       extension Value.Neutral: Plug {

     

       35
       -
       	// Not async now, but might need to be later.

     

       36
        
       	func plug(boundary: Value.Boundary, frame: Value.Frame) async -> Value.Boundary {

     

       37
       -
       		switch boundary.type {

     

       0
        
       
     

       38
        
       		case let .funType(_, _, fam: fam):

     

       39
        
       			guard case let .app(arg: arg) = frame else {

     

       40
       -
       				fatalError("Attempted to plug element of function type into invalid frame")

     

       41
        
       			}

     

       42
        
       			let fibre = fam.instantiate(with: arg)

     

       43
        
       			return Value.Boundary(type: fibre, value: boundary.value?.plug(frame: frame))

     

       44
       -
       			

     

       45
        
       		case let .recordType(boundName, fields: fields):

     

       46
        
       			guard case let .proj(fieldName) = frame else {

     

       47
       -
       				fatalError("Attempted to plug element of record type into invalid frame")

     

       48
        
       			}

     

       49
        
       			guard let field = fields[fieldName] else {

     

       50
       -
       				fatalError("Attempted to project invalid field from element of record type")

     

       51
        
       			}

     

       52
        
       			let prefix = fields.prefix(until: fieldName)

     

       53
        
       			let prefixImpls = prefix.mapWithKeys { (key, spec) in

     

       54
        
       				Value.FieldImpl(

     

       55
        
       					type: spec.type,

     

       56
        
       					value: Closure(

     

       57
       -
       						evaluator: Evaluator(globals: [:], locals: [.shift(neutral: self)]),

     

       58
        
       						body: .cut(term: .local(index: 0), frame: .proj(fieldName: key))

     

       59
        
       					)

     

       60
        
       				)

     

       61
        
       			}

     

       62
        
       			let prefixRecord: Value = .record(boundName: boundName, fields: prefixImpls)

     

       63
        
       			let fieldTypeValue = field.type.instantiate(with: prefixRecord)

     

       64
       -
       			let value = boundary.value?.plug(frame: frame) ?? field.manifest.map { manifest in

     

       65
       -
       				return manifest.instantiate(with: .shift(neutral: self))

     

       66
       -
       			}

     

       67
        
       			return Value.Boundary(type: fieldTypeValue, value: value)

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       68
        
       		}

     

       69
        
       	}

     

       70
        
       

     

       71
        
       	func plug(frame: Value.Frame) -> Self {

     

       72
       -
       		Self(

     

       0
        
       
     

       73
        
       			head: head,

     

       74
       -
       			spine: CollectionOfOne(frame) + spine,

     

       75
        
       			boundary: AsyncThunk { await plug(boundary: boundary.value(), frame: frame) }

     

       76
        
       		)

     

       77
        
       	}

···

       10
        
       extension Plug {

     

       11
        
       	func plug(spine: Value.Spine) -> Self {

     

       12
        
       		spine.reduce(self) { partialResult, frame in

     

       13
       +
       			partialResult.plug(frame: frame.forget)

     

       14
        
       		}

     

       15
        
       	}

     

       16
        
       }

     
···

       27
        
       			return impl.value.instantiate(with: self)

     

       28
        
       		case let .shift(neutral: neutral):

     

       29
        
       			return .shift(neutral: neutral.plug(frame: frame))

     

       30
       +
       		default:

     

       31
       +
       			fatalError()

     

       32
        
       		}

     

       33
        
       	}

     

       34
        
       }

     

       35
        
       

     

       36
        
       extension Value.Neutral: Plug {

     

       0
        
       
     

       37
        
       	func plug(boundary: Value.Boundary, frame: Value.Frame) async -> Value.Boundary {

     

       38
       +
       		switch await boundary.type.whnf() {

     

       39
       +
       

     

       40
        
       		case let .funType(_, _, fam: fam):

     

       41
        
       			guard case let .app(arg: arg) = frame else {

     

       42
       +
       				fatalError("Attempted to plug boundary of function type into invalid frame")

     

       43
        
       			}

     

       44
        
       			let fibre = fam.instantiate(with: arg)

     

       45
        
       			return Value.Boundary(type: fibre, value: boundary.value?.plug(frame: frame))

     

       46
       +
       

     

       47
        
       		case let .recordType(boundName, fields: fields):

     

       48
        
       			guard case let .proj(fieldName) = frame else {

     

       49
       +
       				fatalError("Attempted to plug boundary of record type into invalid frame")

     

       50
        
       			}

     

       51
        
       			guard let field = fields[fieldName] else {

     

       52
       +
       				fatalError("Attempted to project invalid field from boundary of record type")

     

       53
        
       			}

     

       54
        
       			let prefix = fields.prefix(until: fieldName)

     

       55
        
       			let prefixImpls = prefix.mapWithKeys { (key, spec) in

     

       56
        
       				Value.FieldImpl(

     

       57
        
       					type: spec.type,

     

       58
        
       					value: Closure(

     

       59
       +
       						evaluator: Evaluator(),

     

       60
        
       						body: .cut(term: .local(index: 0), frame: .proj(fieldName: key))

     

       61
        
       					)

     

       62
        
       				)

     

       63
        
       			}

     

       64
        
       			let prefixRecord: Value = .record(boundName: boundName, fields: prefixImpls)

     

       65
        
       			let fieldTypeValue = field.type.instantiate(with: prefixRecord)

     

       66
       +
       			let value =

     

       67
       +
       				boundary.value?.plug(frame: frame)

     

       68
       +
       				?? field.manifest.map { $0.instantiate(with: .shift(neutral: self)) }

     

       69
        
       			return Value.Boundary(type: fieldTypeValue, value: value)

     

       70
       +
       

     

       71
       +
       		default:

     

       72
       +
       			fatalError("Boundary has unexpected type for plugging")

     

       73
       +
       		}

     

       74
       +
       	}

     

       75
       +
       

     

       76
       +
       	func enrich(frame: Value.Frame) -> Value.RichFrame {

     

       77
       +
       		switch frame {

     

       78
       +
       		case let .app(arg: arg):

     

       79
       +
       			let dom: AsyncThunk<Value.Type_> = AsyncThunk {

     

       80
       +
       				guard case let .funType(dom: dom, _, _) = await boundary.value().type.whnf() else { fatalError() }

     

       81
       +
       				return dom

     

       82
       +
       			}

     

       83
       +
       			return .app(dom: dom, arg: arg)

     

       84
       +
       

     

       85
       +
       		case let .proj(fieldName: fieldName):

     

       86
       +
       			return .proj(fieldName: fieldName)

     

       87
        
       		}

     

       88
        
       	}

     

       89
        
       

     

       90
        
       	func plug(frame: Value.Frame) -> Self {

     

       91
       +
       		let richFrame = enrich(frame: frame)

     

       92
       +
       		return Self(

     

       93
        
       			head: head,

     

       94
       +
       			spine: spine + CollectionOfOne(richFrame),

     

       95
        
       			boundary: AsyncThunk { await plug(boundary: boundary.value(), frame: frame) }

     

       96
        
       		)

     

       97
        
       	}

+27 -23

Sources/PterodactylKernel/Quotation.swift Sources/PterodactylKernel/Local Analysis/Quotation.swift

···

       4
        
       

     

       5
        
       import Foundation

     

       6
        
       

     

       7
       -
       struct Quotation {

     

       8
       -
       	let depth: Int

     

       9
       -
       	var next: Self {

     

       10
       -
       		Quotation(depth: depth + 1)

     

       11
       -
       	}

     

       12
       -
       

     

       13
        
       	func quote(type: Value.Type_) -> Term.Type_ {

     

       14
        
       		switch type {

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       15
        
       		case let .funType(dom: dom, boundName: boundName, fam: fam):

     

       16
        
       			return .funType(

     

       17
        
       				dom: quote(type: dom),

     
···

       56
        
       		case let .shift(neutral: neutral):

     

       57
        
       			return quote(neutral: neutral)

     

       58
        
       

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       59
        
       		case let .fun(dom: dom, boundName: boundName, closure: closure):

     

       60
        
       			return .fun(

     

       61
        
       				dom: AsyncThunk { await quote(type: dom.value()) },

     
···

       82
        
       		}

     

       83
        
       	}

     

       84
        
       

     

       85
       -
       	func fresh(type: AsyncThunk<Value.Type_>) -> Value {

     

       86
       -
       		let boundary: AsyncThunk<Value.Boundary> = AsyncThunk {

     

       87
       -
       			await Value.Boundary(type: type.value(), value: nil)

     

       88
       -
       		}

     

       89
       -
       

     

       90
       -
       		return Value.shift(

     

       91
       -
       			neutral: Value.Neutral(

     

       92
       -
       				head: .local(level: depth),

     

       93
       -
       				spine: [],

     

       94
       -
       				boundary: boundary

     

       95
       -
       			)

     

       96
       -
       		)

     

       97
       -
       	}

     

       98
       -
       

     

       99
        
       	func quote(dom: AsyncThunk<Value.Type_>, closure: Closure<Term>) -> Term {

     

       100
        
       		let x = fresh(type: dom)

     

       101
        
       		let value = closure.instantiate(with: x)

     
···

       115
        
       		}

     

       116
        
       	}

     

       117
        
       

     

       118
       -
       	private func quote(frame: Value.Frame) -> Term.Frame {

     

       119
        
       		switch frame {

     

       120
       -
       		case let .app(arg: arg):

     

       121
        
       			return .app(arg: quote(value: arg))

     

       122
        
       		case let .proj(fieldName: fieldName):

     

       123
        
       			return .proj(fieldName: fieldName)

     

       124
        
       		}

     

       125
        
       	}

     

       126
        
       

     

       127
       -
       	private func quote(neutral: Value.Neutral) -> Term {

     

       128
        
       		let headTerm = quote(head: neutral.head)

     

       129
        
       		return neutral.spine.reduce(headTerm) { term, frame in

     

       130
        
       			.cut(term: term, frame: quote(frame: frame))

···

       4
        
       

     

       5
        
       import Foundation

     

       6
        
       

     

       7
       +
       extension LocalAnalysis {

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       8
        
       	func quote(type: Value.Type_) -> Term.Type_ {

     

       9
        
       		switch type {

     

       10
       +
       		case .universeType: return .universeType

     

       11
       +
       

     

       12
       +
       		case let .universeCodes(size: size):

     

       13
       +
       			return .universeCodes(size: size.map(quote(value:)))

     

       14
       +
       			

     

       15
       +
       		case let .decode(size: size, code: code):

     

       16
       +
       			return .decode(size: size, code: quote(neutral: code))

     

       17
       +
       

     

       18
        
       		case let .funType(dom: dom, boundName: boundName, fam: fam):

     

       19
        
       			return .funType(

     

       20
        
       				dom: quote(type: dom),

     
···

       59
        
       		case let .shift(neutral: neutral):

     

       60
        
       			return quote(neutral: neutral)

     

       61
        
       

     

       62
       +
       		case let .shrink(size: size, type: type):

     

       63
       +
       			return .shrink(size: size.map(quote(value:)), type: quote(type: type))

     

       64
       +
       

     

       65
       +
       		case .universeZero:

     

       66
       +
       			return .universeZero

     

       67
       +
       			

     

       68
       +
       		case let .universeSucc(universe: universe):

     

       69
       +
       			return .universeSucc(quote(value: universe))

     

       70
       +
       

     

       71
       +
       		case let .universeLub(universe1, universe2):

     

       72
       +
       			return .universeLub(

     

       73
       +
       				quote(value: universe1),

     

       74
       +
       				quote(value: universe2)

     

       75
       +
       			)

     

       76
       +
       

     

       77
        
       		case let .fun(dom: dom, boundName: boundName, closure: closure):

     

       78
        
       			return .fun(

     

       79
        
       				dom: AsyncThunk { await quote(type: dom.value()) },

     
···

       100
        
       		}

     

       101
        
       	}

     

       102
        
       

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       103
        
       	func quote(dom: AsyncThunk<Value.Type_>, closure: Closure<Term>) -> Term {

     

       104
        
       		let x = fresh(type: dom)

     

       105
        
       		let value = closure.instantiate(with: x)

     
···

       119
        
       		}

     

       120
        
       	}

     

       121
        
       

     

       122
       +
       	private func quote(frame: Value.RichFrame) -> Term.Frame {

     

       123
        
       		switch frame {

     

       124
       +
       		case let .app(_, arg: arg):

     

       125
        
       			return .app(arg: quote(value: arg))

     

       126
        
       		case let .proj(fieldName: fieldName):

     

       127
        
       			return .proj(fieldName: fieldName)

     

       128
        
       		}

     

       129
        
       	}

     

       130
        
       

     

       131
       +
       	public func quote(neutral: Value.Neutral) -> Term {

     

       132
        
       		let headTerm = quote(head: neutral.head)

     

       133
        
       		return neutral.spine.reduce(headTerm) { term, frame in

     

       134
        
       			.cut(term: term, frame: quote(frame: frame))

+81

Sources/PterodactylKernel/Smallness.swift

···

       1
       +
       // SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers

     

       2
       +
       //

     

       3
       +
       // SPDX-License-Identifier: MPL-2.0

     

       4
       +
       

     

       5
       +
       import Foundation

     

       6
       +
       

     

       7
       +
       extension LocalAnalysis {

     

       8
       +
       	struct SizeError: Error { }

     

       9
       +
       

     

       10
       +
       	func assertSize(type: Value.Type_, size: Size<Value>) async throws {

     

       11
       +
       		switch await type.whnf() {

     

       12
       +
       

     

       13
       +
       		// In principle the type of universes could be small, but I am worried about about the strictness of the semilattice operations. I know how to interpret them if universeType is exoNat as in 2LTT, but in that case universeType probably should not be fibrant.

     

       14
       +
       		case .universeType, .universeCodes(size: .moderate):

     

       15
       +
       			throw SizeError()

     

       16
       +
       

     

       17
       +
       		case let .universeCodes(size: .little(universe: littleUniverse)):

     

       18
       +
       			try await assertLeq(size1: .little(universe: .universeSucc(littleUniverse)), size2: size)

     

       19
       +
       

     

       20
       +
       		case let .decode(size: _, code: code):

     

       21
       +
       			guard case let .universeCodes(size: littleSize) = await code.boundary.value().type.whnf() else { fatalError() }

     

       22
       +
       			try await assertLeq(size1: littleSize, size2: size)

     

       23
       +
       			

     

       24
       +
       		case let .funType(dom: dom, boundName: _, fam: fam):

     

       25
       +
       			try await assertSize(type: dom, size: size)

     

       26
       +
       			let domThunk = AsyncThunk(value: dom)

     

       27
       +
       			let x = fresh(type: domThunk)

     

       28
       +
       			let fibre = fam.instantiate(with: x)

     

       29
       +
       			try await next.assertSize(type: fibre, size: size)

     

       30
       +
       

     

       31
       +
       		case let .recordType(boundName: boundName, fields: fields):

     

       32
       +
       			var fieldSpecs: [(String, Value.FieldSpec)] = []

     

       33
       +
       			for (key, fieldSpec) in fields.elements {

     

       34
       +
       				if fieldSpec.manifest == nil {

     

       35
       +
       					let prefixType: AsyncThunk<Value.Type_> = AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs)))

     

       36
       +
       					let prefixRecord = fresh(type: prefixType)

     

       37
       +
       					try await next.assertSize(type: fieldSpec.type.instantiate(with: prefixRecord), size: size)

     

       38
       +
       				}

     

       39
       +
       

     

       40
       +
       				fieldSpecs.append((key, fieldSpec))

     

       41
       +
       			}

     

       42
       +
       		}

     

       43
       +
       	}

     

       44
       +
       

     

       45
       +
       	func assertSmall(type: Value.Type_, universe: Value) async throws {

     

       46
       +
       		try await assertSize(type: type, size: .little(universe: universe))

     

       47
       +
       	}

     

       48
       +
       

     

       49
       +
       	func assertLeq(size1: Size<Value>, size2: Size<Value>) async throws {

     

       50
       +
       		switch (size1, size2) {

     

       51
       +
       		case (_, .moderate): ()

     

       52
       +
       		case let (.little(universe: universe1), .little(universe: universe2)):

     

       53
       +
       			try await assertLeq(universe1: universe1, universe2: universe2)

     

       54
       +
       		default:

     

       55
       +
       			throw SizeError()

     

       56
       +
       		}

     

       57
       +
       	}

     

       58
       +
       	

     

       59
       +
       	func assertLeq(universe1: Value, universe2: Value) async throws {

     

       60
       +
       		switch await (universe1.whnf(), universe2.whnf()) {

     

       61
       +
       		case (.universeZero, _): ()

     

       62
       +
       		case let (.universeLub(universe11, universe12), _):

     

       63
       +
       			try await assertLeq(universe1: universe11, universe2: universe2)

     

       64
       +
       			try await assertLeq(universe1: universe12, universe2: universe2)

     

       65
       +
       		case let (.universeSucc(universe: universe1), .universeSucc(universe: universe2)):

     

       66
       +
       			try await assertLeq(universe1: universe1, universe2: universe2)

     

       67
       +
       		case let (_, .universeLub(universe21, universe22)):

     

       68
       +
       			do {

     

       69
       +
       				try await assertLeq(universe1: universe1, universe2: universe21)

     

       70
       +
       			} catch {

     

       71
       +
       				try await assertLeq(universe1: universe1, universe2: universe22)

     

       72
       +
       			}

     

       73
       +
       		case let (_, .universeSucc(universe: universe2)):

     

       74
       +
       			try await assertLeq(universe1: universe1, universe2: universe2)

     

       75
       +
       		case let (.shift(neutral: neutral1), .shift(neutral: neutral2)):

     

       76
       +
       			try await equate(neutral: neutral1, with: neutral2)

     

       77
       +
       		default:

     

       78
       +
       			throw SizeError()

     

       79
       +
       		}

     

       80
       +
       	}

     

       81
       +
       }

+13 -1

Sources/PterodactylKernel/Whnf.swift

···

       5
        
       extension Value {

     

       6
        
       	func whnf() async -> Value {

     

       7
        
       		switch self {

     

       8
       -
       		case .fun, .record : self

     

       9
        
       		case let .shift(neutral: neutral): await neutral.boundary.value().value ?? self

     

       10
        
       		}

     

       11
        
       	}

     

       12
        
       }

     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0
        
       
     

       0

···

       5
        
       extension Value {

     

       6
        
       	func whnf() async -> Value {

     

       7
        
       		switch self {

     

       8
       +
       		case .fun, .record, .shrink, .universeZero, .universeSucc, .universeLub: self

     

       9
        
       		case let .shift(neutral: neutral): await neutral.boundary.value().value ?? self

     

       10
        
       		}

     

       11
        
       	}

     

       12
        
       }

     

       13
       +
       

     

       14
       +
       extension Value.Type_ {

     

       15
       +
       	func whnf() async -> Self {

     

       16
       +
       		switch self {

     

       17
       +
       		case .funType, .recordType, .universeCodes, .universeType: return self

     

       18
       +
       		case let .decode(size: size, code: neutral):

     

       19
       +
       			guard let code = await neutral.boundary.value().value else { return self }

     

       20
       +
       			return code.decode(size: size)

     

       21
       +
       		}

     

       22
       +
       	}

     

       23
       +
       }

     

       24
       +

-11

Tests/PterodactylKernelTests/PterodactylKernelTests.swift

···

       1
       -
       // SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers

     

       2
       -
       //

     

       3
       -
       // SPDX-License-Identifier: MPL-2.0

     

       4
       -
       

     

       5
       -
       import Testing

     

       6
       -
       

     

       7
       -
       @testable import PterodactylKernel

     

       8
       -
       

     

       9
       -
       @Test func example() async throws {

     

       10
       -
       	// Write your test here and use APIs like `#expect(...)` to check expected conditions.

     

       11
       -
       }

+26

Tests/PterodactylKernelTests/Quotation.swift

···

       1
       +
       // SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers

     

       2
       +
       //

     

       3
       +
       // SPDX-License-Identifier: MPL-2.0

     

       4
       +
       

     

       5
       +
       import Testing

     

       6
       +
       

     

       7
       +
       @testable import PterodactylKernel

     

       8
       +
       

     

       9
       +
       struct QuotationTests {

     

       10
       +
       	@Test func quotingNeutrals() async throws {

     

       11
       +
       		let analysis = LocalAnalysis()

     

       12
       +
       		let recordType1 = Term.Type_.recordType(boundName: nil, fields: FieldDict([("foo", Term.FieldSpec(type: .universeType, manifest: nil))]))

     

       13
       +
       		let recordType2 = Term.Type_.recordType(boundName: nil, fields: FieldDict([("bar", Term.FieldSpec(type: recordType1, manifest: nil))]))

     

       14
       +
       		let recordTypeValue = Evaluator().evaluate(type: recordType2)

     

       15
       +
       		let base = Value.Neutral(head: .global(name: "X"), spine: [], boundary: AsyncThunk { Value.Boundary(type: recordTypeValue, value: nil) })

     

       16
       +
       		let bar = base.plug(frame: .proj(fieldName: "bar"))

     

       17
       +
       		let foo = bar.plug(frame: .proj(fieldName: "foo"))

     

       18
       +
       		let term = analysis.quote(neutral: foo)

     

       19
       +
       		let result =

     

       20
       +
       		switch term {

     

       21
       +
       		case .cut(term: .cut(term: .global(name: "X"), frame: .proj(fieldName: "bar")), frame: .proj(fieldName: "foo")): true

     

       22
       +
       		default: false

     

       23
       +
       		}

     

       24
       +
       		#expect(result, "Neutral incorrectly quoted as: \(term)")

     

       25
       +
       	}

     

       26
       +
       }

+61

Tests/PterodactylKernelTests/Size.swift

···

       1
       +
       // SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers

     

       2
       +
       //

     

       3
       +
       // SPDX-License-Identifier: MPL-2.0

     

       4
       +
       

     

       5
       +
       import Testing

     

       6
       +
       @testable import PterodactylKernel

     

       7
       +
       

     

       8
       +
       struct SizeTests {

     

       9
       +
       	@Test func leqIsReflexive() async throws {

     

       10
       +
       		let analysis = LocalAnalysis()

     

       11
       +
       		

     

       12
       +
       		await #expect(throws: Never.self) {

     

       13
       +
       			try await analysis.assertLeq(size1: .moderate, size2: .moderate)

     

       14
       +
       		}

     

       15
       +
       	}

     

       16
       +
       	

     

       17
       +
       	@Test func moderateIsNotSmall() async throws {

     

       18
       +
       		let analysis = LocalAnalysis()

     

       19
       +
       		

     

       20
       +
       		await #expect(throws: LocalAnalysis.SizeError.self) {

     

       21
       +
       			try await analysis.assertLeq(size1: .moderate, size2: .little(universe: .universeZero))

     

       22
       +
       		}

     

       23
       +
       	}

     

       24
       +
       	

     

       25
       +
       	@Test func lubIsCommutative() async throws {

     

       26
       +
       		let analysis = LocalAnalysis()

     

       27
       +
       		await #expect(throws: Never.self) {

     

       28
       +
       			let lhs = Value.universeLub(.universeZero, .universeSucc(.universeZero))

     

       29
       +
       			let rhs = Value.universeLub(.universeSucc(.universeZero), .universeZero)

     

       30
       +
       			try await analysis.equate(size: .little(universe: lhs), with: .little(universe: rhs))

     

       31
       +
       		}

     

       32
       +
       	}

     

       33
       +
       	

     

       34
       +
       	@Test func lubZeroLeftUnit() async throws {

     

       35
       +
       		let analysis = LocalAnalysis()

     

       36
       +
       		await #expect(throws: Never.self) {

     

       37
       +
       			let lhs = Value.universeLub(.universeZero, .universeSucc(.universeZero))

     

       38
       +
       			let rhs = Value.universeSucc(.universeZero)

     

       39
       +
       			try await analysis.equate(size: .little(universe: lhs), with: .little(universe: rhs))

     

       40
       +
       		}

     

       41
       +
       	}

     

       42
       +
       	

     

       43
       +
       	@Test func lubZeroRightUnit() async throws {

     

       44
       +
       		let analysis = LocalAnalysis()

     

       45
       +
       		await #expect(throws: Never.self) {

     

       46
       +
       			let lhs = Value.universeLub(.universeSucc(.universeZero), .universeZero)

     

       47
       +
       			let rhs = Value.universeSucc(.universeZero)

     

       48
       +
       			try await analysis.equate(size: .little(universe: lhs), with: .little(universe: rhs))

     

       49
       +
       		}

     

       50
       +
       	}

     

       51
       +
       	

     

       52
       +
       	@Test func succDistributesOverLub() async throws {

     

       53
       +
       		let analysis = LocalAnalysis()

     

       54
       +
       		await #expect(throws: Never.self) {

     

       55
       +
       			let lhs = Value.universeSucc(Value.universeLub(.universeZero, .universeSucc(.universeZero)))

     

       56
       +
       			let rhs = Value.universeLub(.universeSucc(.universeSucc(.universeZero)), .universeSucc(.universeZero))

     

       57
       +
       			try await analysis.equate(size: .little(universe: lhs), with: .little(universe: rhs))

     

       58
       +
       		}

     

       59
       +
       	}

     

       60
       +
       	

     

       61
       +
       }