// SPDX-FileCopyrightText: 2025 The Project Pterodactyl Developers
//
// SPDX-License-Identifier: MPL-2.0

import Foundation

extension LocalAnalysis {
	func quote(type: Value.Type_) -> Term.Type_ {
		switch type {
		case .universeType: return .universeType

		case let .universeCodes(size: size):
			return .universeCodes(size: size.map(quote(value:)))
			
		case let .decode(size: size, code: code):
			return .decode(size: size, code: quote(neutral: code))

		case let .funType(dom: dom, boundName: boundName, fam: fam):
			return .funType(
				dom: quote(type: dom),
				boundName: boundName,
				fam: quote(dom: AsyncThunk(value: dom), family: fam)
			)

		case let .recordType(boundName: boundName, fields: fields):
			var fieldSpecs: [(String, Value.FieldSpec)] = []
			var quotedFieldSpecs: [(String, Term.FieldSpec)] = []

			for (key, fieldSpec) in fields.elements {
				let dom: AsyncThunk<Value.Type_> = AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs)))
				let quotedFieldSpec = quote(dom: dom, fieldSpec: fieldSpec)
				fieldSpecs.append((key, fieldSpec))
				quotedFieldSpecs.append((key, quotedFieldSpec))
			}

			return .recordType(
				boundName: boundName,
				fields: FieldDict(quotedFieldSpecs)
			)
		}
	}

	func quote(dom: AsyncThunk<Value.Type_>, fieldSpec: Value.FieldSpec) -> Term.FieldSpec {
		return Term.FieldSpec(
			type: quote(dom: dom, family: fieldSpec.type),
			manifest: fieldSpec.manifest.map { quote(dom: dom, closure: $0) }
		)
	}

	func quote(dom: AsyncThunk<Value.Type_>, fieldImpl: Value.FieldImpl) -> Term.FieldImpl {
		return Term.FieldImpl(
			type: quote(dom: dom, family: fieldImpl.type),
			value: quote(dom: dom, closure: fieldImpl.value)
		)
	}

	func quote(value: Value) -> Term {
		switch value {
		case let .shift(neutral: neutral):
			return quote(neutral: neutral)

		case let .shrink(size: size, type: type):
			return .shrink(size: size.map(quote(value:)), type: quote(type: type))

		case .universeZero:
			return .universeZero
			
		case let .universeSucc(universe: universe):
			return .universeSucc(quote(value: universe))

		case let .universeLub(universe1, universe2):
			return .universeLub(
				quote(value: universe1),
				quote(value: universe2)
			)

		case let .fun(dom: dom, boundName: boundName, closure: closure):
			return .fun(
				dom: AsyncThunk { await quote(type: dom.value()) },
				boundName: boundName,
				body: quote(dom: dom, closure: closure)
			)

		case let .record(boundName: boundName, fields: fields):
			var fieldSpecs: [(String, Value.FieldSpec)] = []
			var quotedFields: [(String, Term.FieldImpl)] = []

			for (key, fieldImpl) in fields.elements {
				let fieldSpec = Value.FieldSpec(type: fieldImpl.type, manifest: fieldImpl.value)
				let quotedFieldImpl = quote(
					dom: AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs))),
					fieldImpl: fieldImpl
				)

				fieldSpecs.append((key, fieldSpec))
				quotedFields.append((key, quotedFieldImpl))
			}

			return .record(boundName: boundName, fields: FieldDict(quotedFields))
		}
	}

	func quote(dom: AsyncThunk<Value.Type_>, closure: Closure<Term>) -> Term {
		let x = fresh(type: dom)
		let value = closure.instantiate(with: x)
		return next.quote(value: value)
	}

	func quote(dom: AsyncThunk<Value.Type_>, family: Closure<Term.Type_>) -> Term.Type_ {
		let x = fresh(type: dom)
		let value = family.instantiate(with: x)
		return next.quote(type: value)
	}

	private func quote(head: Value.Head) -> Term {
		switch head {
		case let .local(level: level): .local(index: depth - level - 1)
		case let .global(name: name): .global(name: name)
		}
	}

	private func quote(frame: Value.RichFrame) -> Term.Frame {
		switch frame {
		case let .app(_, arg: arg):
			return .app(arg: quote(value: arg))
		case let .proj(fieldName: fieldName):
			return .proj(fieldName: fieldName)
		}
	}

	public func quote(neutral: Value.Neutral) -> Term {
		let headTerm = quote(head: neutral.head)
		return neutral.spine.reduce(headTerm) { term, frame in
			.cut(term: term, frame: quote(frame: frame))
		}
	}
}