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
5struct Evaluator {
6 struct GlobalDef {
7 var type: Term.Type_
8 var term: Term?
9 }
10
11 let globals: [Name: GlobalDef]
12 let locals: [Value]
13
14 public init(globals: [Name: GlobalDef] = [:], locals: [Value] = []) {
15 self.globals = globals
16 self.locals = locals
17 }
18
19 func extendedBy(value: Value) -> Self {
20 Self(globals: globals, locals: CollectionOfOne(value) + locals)
21 }
22
23 func close<Body>(body: Body) -> Closure<Body> {
24 Closure(evaluator: self, body: body)
25 }
26
27 func close(fieldSpec: Term.FieldSpec) -> Value.FieldSpec {
28 Value.FieldSpec(
29 type: close(body: fieldSpec.type),
30 manifest: fieldSpec.manifest.map(close(body:))
31 )
32 }
33
34 func close(fieldImpl: Term.FieldImpl) -> Value.FieldImpl {
35 Value.FieldImpl(
36 type: close(body: fieldImpl.type),
37 value: close(body: fieldImpl.value)
38 )
39 }
40
41 func evaluate(frame: Term.Frame) -> Value.Frame {
42 switch frame {
43 case let .app(arg: arg): .app(arg: evaluate(term: arg))
44 case let .proj(fieldName: fieldName): .proj(fieldName: fieldName)
45 }
46 }
47
48 func evaluate(term: Term) -> Value {
49 switch term {
50 case let .local(index: index):
51 return locals[index]
52 case let .global(name: name):
53 let neutral = Value.Neutral(
54 head: .global(name: name),
55 spine: [],
56 boundary: AsyncThunk {
57 let typedTerm = globals[name]!
58 return Value.Boundary(
59 type: evaluate(type: typedTerm.type),
60 value: typedTerm.term.map(evaluate(term:))
61 )
62 }
63 )
64 return .shift(neutral: neutral)
65 case let .cut(term: term, frame: frame):
66 return evaluate(term: term)
67 .plug(frame: evaluate(frame: frame))
68 case let .fun(dom: dom, boundName: boundName, body: body):
69 return .fun(
70 dom: AsyncThunk { await evaluate(type: dom.value()) },
71 boundName: boundName,
72 closure: close(body: body)
73 )
74 case let .record(boundName: boundName, fields: fields):
75 return .record(
76 boundName: boundName,
77 fields: fields.map(close(fieldImpl:))
78 )
79 case let .shrink(size: size, type: type):
80 return .shrink(
81 size: size.map(evaluate(term:)),
82 type: evaluate(type: type)
83 )
84 case .universeZero:
85 return .universeZero
86 case let .universeSucc(universe: universe):
87 return .universeSucc(evaluate(term: universe))
88 case let .universeLub(universe1, universe2):
89 return .universeLub(
90 evaluate(term: universe1),
91 evaluate(term: universe2)
92 )
93 }
94 }
95
96 func evaluate(type: Term.Type_) -> Value.Type_ {
97 switch type {
98 case let .funType(dom: dom, boundName: boundName, fam: fam):
99 .funType(
100 dom: evaluate(type: dom),
101 boundName: boundName,
102 fam: close(body: fam)
103 )
104
105 case let .recordType(boundName: boundName, fields: fields):
106 .recordType(boundName: boundName, fields: fields.map(close(fieldSpec:)))
107
108 case let .decode(size: size, code: code):
109 evaluate(term: code).decode(size: size)
110
111 case let .universeCodes(size: size):
112 .universeCodes(size: size.map(evaluate(term:)))
113
114 case .universeType:
115 .universeType
116 }
117 }
118}
119
120extension Value {
121 func decode(size: Size<()>) -> Value.Type_ {
122 switch self {
123 case let .shrink(_, type: type): type
124 case let .shift(neutral: neutral): .decode(size: size, code: neutral)
125 default: fatalError()
126 }
127 }
128}
129
130
131extension Closure where Body == Term {
132 func instantiate(with value: Value) -> Value {
133 evaluator.extendedBy(value: value).evaluate(term: body)
134 }
135}
136
137extension Closure where Body == Term.Type_ {
138 func instantiate(with value: Value) -> Value.Type_ {
139 evaluator.extendedBy(value: value).evaluate(type: body)
140 }
141}