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 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),
21 boundName: boundName,
22 fam: quote(dom: AsyncThunk(value: dom), family: fam)
23 )
24
25 case let .recordType(boundName: boundName, fields: fields):
26 var fieldSpecs: [(String, Value.FieldSpec)] = []
27 var quotedFieldSpecs: [(String, Term.FieldSpec)] = []
28
29 for (key, fieldSpec) in fields.elements {
30 let dom: AsyncThunk<Value.Type_> = AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs)))
31 let quotedFieldSpec = quote(dom: dom, fieldSpec: fieldSpec)
32 fieldSpecs.append((key, fieldSpec))
33 quotedFieldSpecs.append((key, quotedFieldSpec))
34 }
35
36 return .recordType(
37 boundName: boundName,
38 fields: FieldDict(quotedFieldSpecs)
39 )
40 }
41 }
42
43 func quote(dom: AsyncThunk<Value.Type_>, fieldSpec: Value.FieldSpec) -> Term.FieldSpec {
44 return Term.FieldSpec(
45 type: quote(dom: dom, family: fieldSpec.type),
46 manifest: fieldSpec.manifest.map { quote(dom: dom, closure: $0) }
47 )
48 }
49
50 func quote(dom: AsyncThunk<Value.Type_>, fieldImpl: Value.FieldImpl) -> Term.FieldImpl {
51 return Term.FieldImpl(
52 type: quote(dom: dom, family: fieldImpl.type),
53 value: quote(dom: dom, closure: fieldImpl.value)
54 )
55 }
56
57 func quote(value: Value) -> Term {
58 switch value {
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()) },
80 boundName: boundName,
81 body: quote(dom: dom, closure: closure)
82 )
83
84 case let .record(boundName: boundName, fields: fields):
85 var fieldSpecs: [(String, Value.FieldSpec)] = []
86 var quotedFields: [(String, Term.FieldImpl)] = []
87
88 for (key, fieldImpl) in fields.elements {
89 let fieldSpec = Value.FieldSpec(type: fieldImpl.type, manifest: fieldImpl.value)
90 let quotedFieldImpl = quote(
91 dom: AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs))),
92 fieldImpl: fieldImpl
93 )
94
95 fieldSpecs.append((key, fieldSpec))
96 quotedFields.append((key, quotedFieldImpl))
97 }
98
99 return .record(boundName: boundName, fields: FieldDict(quotedFields))
100 }
101 }
102
103 func quote(dom: AsyncThunk<Value.Type_>, closure: Closure<Term>) -> Term {
104 let x = fresh(type: dom)
105 let value = closure.instantiate(with: x)
106 return next.quote(value: value)
107 }
108
109 func quote(dom: AsyncThunk<Value.Type_>, family: Closure<Term.Type_>) -> Term.Type_ {
110 let x = fresh(type: dom)
111 let value = family.instantiate(with: x)
112 return next.quote(type: value)
113 }
114
115 private func quote(head: Value.Head) -> Term {
116 switch head {
117 case let .local(level: level): .local(index: depth - level - 1)
118 case let .global(name: name): .global(name: name)
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))
135 }
136 }
137}