// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers // // SPDX-License-Identifier: MPL-2.0 struct Evaluator { struct GlobalDef { var type: Term.Type_ var term: Term? } let globals: [Name: GlobalDef] let locals: [Value] public init(globals: [Name: GlobalDef] = [:], locals: [Value] = []) { self.globals = globals self.locals = locals } func extendedBy(value: Value) -> Self { Self(globals: globals, locals: CollectionOfOne(value) + locals) } func close(body: Body) -> Closure { Closure(evaluator: self, body: body) } func close(fieldSpec: Term.FieldSpec) -> Value.FieldSpec { Value.FieldSpec( type: close(body: fieldSpec.type), manifest: fieldSpec.manifest.map(close(body:)) ) } func close(fieldImpl: Term.FieldImpl) -> Value.FieldImpl { Value.FieldImpl( type: close(body: fieldImpl.type), value: close(body: fieldImpl.value) ) } func evaluate(frame: Term.Frame) -> Value.Frame { switch frame { case let .app(arg: arg): .app(arg: evaluate(term: arg)) case let .proj(fieldName: fieldName): .proj(fieldName: fieldName) } } func evaluate(term: Term) -> Value { switch term { case let .local(index: index): return locals[index] case let .global(name: name): let neutral = Value.Neutral( head: .global(name: name), spine: [], boundary: AsyncThunk { let typedTerm = globals[name]! return Value.Boundary( type: evaluate(type: typedTerm.type), value: typedTerm.term.map(evaluate(term:)) ) } ) return .shift(neutral: neutral) case let .cut(term: term, frame: frame): return evaluate(term: term) .plug(frame: evaluate(frame: frame)) case let .fun(dom: dom, boundName: boundName, body: body): return .fun( dom: AsyncThunk { await evaluate(type: dom.value()) }, boundName: boundName, closure: close(body: body) ) case let .record(boundName: boundName, fields: fields): return .record( boundName: boundName, fields: fields.map(close(fieldImpl:)) ) case let .shrink(size: size, type: type): return .shrink( size: size.map(evaluate(term:)), type: evaluate(type: type) ) case .universeZero: return .universeZero case let .universeSucc(universe: universe): return .universeSucc(evaluate(term: universe)) case let .universeLub(universe1, universe2): return .universeLub( evaluate(term: universe1), evaluate(term: universe2) ) } } func evaluate(type: Term.Type_) -> Value.Type_ { switch type { case let .funType(dom: dom, boundName: boundName, fam: fam): .funType( dom: evaluate(type: dom), boundName: boundName, fam: close(body: fam) ) case let .recordType(boundName: boundName, fields: fields): .recordType(boundName: boundName, fields: fields.map(close(fieldSpec:))) case let .decode(size: size, code: code): evaluate(term: code).decode(size: size) case let .universeCodes(size: size): .universeCodes(size: size.map(evaluate(term:))) case .universeType: .universeType } } } extension Value { func decode(size: Size<()>) -> Value.Type_ { switch self { case let .shrink(_, type: type): type case let .shift(neutral: neutral): .decode(size: size, code: neutral) default: fatalError() } } } extension Closure where Body == Term { func instantiate(with value: Value) -> Value { evaluator.extendedBy(value: value).evaluate(term: body) } } extension Closure where Body == Term.Type_ { func instantiate(with value: Value) -> Value.Type_ { evaluator.extendedBy(value: value).evaluate(type: body) } }