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
7struct 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 {
15 case let .funType(dom: dom, boundName: boundName, fam: fam):
16 return .funType(
17 dom: quote(type: dom),
18 boundName: boundName,
19 fam: quote(dom: AsyncThunk(value: dom), family: fam)
20 )
21
22 case let .recordType(boundName: boundName, fields: fields):
23 var fieldSpecs: [(String, Value.FieldSpec)] = []
24 var quotedFieldSpecs: [(String, Term.FieldSpec)] = []
25
26 for (key, fieldSpec) in fields.elements {
27 let dom: AsyncThunk<Value.Type_> = AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs)))
28 let quotedFieldSpec = quote(dom: dom, fieldSpec: fieldSpec)
29 fieldSpecs.append((key, fieldSpec))
30 quotedFieldSpecs.append((key, quotedFieldSpec))
31 }
32
33 return .recordType(
34 boundName: boundName,
35 fields: FieldDict(quotedFieldSpecs)
36 )
37 }
38 }
39
40 func quote(dom: AsyncThunk<Value.Type_>, fieldSpec: Value.FieldSpec) -> Term.FieldSpec {
41 return Term.FieldSpec(
42 type: quote(dom: dom, family: fieldSpec.type),
43 manifest: fieldSpec.manifest.map { quote(dom: dom, closure: $0) }
44 )
45 }
46
47 func quote(dom: AsyncThunk<Value.Type_>, fieldImpl: Value.FieldImpl) -> Term.FieldImpl {
48 return Term.FieldImpl(
49 type: quote(dom: dom, family: fieldImpl.type),
50 value: quote(dom: dom, closure: fieldImpl.value)
51 )
52 }
53
54 func quote(value: Value) -> Term {
55 switch value {
56 case let .shift(neutral: neutral):
57 return quote(neutral: neutral)
58
59 case let .fun(dom: dom, boundName: boundName, closure: closure):
60 return .fun(
61 dom: AsyncThunk { await quote(type: dom.value()) },
62 boundName: boundName,
63 body: quote(dom: dom, closure: closure)
64 )
65
66 case let .record(boundName: boundName, fields: fields):
67 var fieldSpecs: [(String, Value.FieldSpec)] = []
68 var quotedFields: [(String, Term.FieldImpl)] = []
69
70 for (key, fieldImpl) in fields.elements {
71 let fieldSpec = Value.FieldSpec(type: fieldImpl.type, manifest: fieldImpl.value)
72 let quotedFieldImpl = quote(
73 dom: AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs))),
74 fieldImpl: fieldImpl
75 )
76
77 fieldSpecs.append((key, fieldSpec))
78 quotedFields.append((key, quotedFieldImpl))
79 }
80
81 return .record(boundName: boundName, fields: FieldDict(quotedFields))
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)
102 return next.quote(value: value)
103 }
104
105 func quote(dom: AsyncThunk<Value.Type_>, family: Closure<Term.Type_>) -> Term.Type_ {
106 let x = fresh(type: dom)
107 let value = family.instantiate(with: x)
108 return next.quote(type: value)
109 }
110
111 private func quote(head: Value.Head) -> Term {
112 switch head {
113 case let .local(level: level): .local(index: depth - level - 1)
114 case let .global(name: name): .global(name: name)
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))
131 }
132 }
133}