this repo has no description
www.jonmsterling.com/01HC/
jonmsterling.com
1// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
2//
3// SPDX-License-Identifier: MPL-2.0
4
5import Foundation
6
7extension 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}