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 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: .big):
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 (_, .big): ()
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}