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

import Foundation

extension LocalAnalysis {
	enum EqualityError: Error {
		case values(lhs: Value, rhs: Value, type: Value.Type_)
		case types(lhs: Value.Type_, rhs: Value.Type_)
		case heads(lhs: Value.Head, rhs: Value.Head)
		case frames(lhs: Value.RichFrame, rhs: Value.RichFrame)
		case spines(lhs: Value.Spine, rhs: Value.Spine)
	}

	func equate(value lhs: Value, with rhs: Value, in type: Value.Type_) async throws {
		switch await (lhs.whnf(), rhs.whnf(), type.whnf()) {
		case (_, _, .universeType):
			try await equate(size: .little(universe: lhs), with: .little(universe: rhs))

		case let (lhs, rhs, .funType(dom: dom, boundName: _, fam: fam)):
			let dom = AsyncThunk(value: dom)
			let x = fresh(type: dom)
			let frame = Value.Frame.app(arg: x)
			let lhs = lhs.plug(frame: frame)
			let rhs = rhs.plug(frame: frame)
			let fibre = fam.instantiate(with: x)
			try await next.equate(value: lhs, with: rhs, in: fibre)

		case let (lhs, rhs, .recordType(boundName: boundName, fields: fields)):
			var fieldImpls: [(String, Value.FieldImpl)] = []
			for (key, field) in fields.elements {
				let prefixRecord: Value = .record(boundName: boundName, fields: FieldDict(fieldImpls))
				if field.manifest == nil {
					let frame = Value.Frame.proj(fieldName: key)
					let lhs = lhs.plug(frame: frame)
					let rhs = rhs.plug(frame: frame)
					let type = field.type.instantiate(with: prefixRecord)
					try await equate(value: lhs, with: rhs, in: type)
				}

				let impl = Value.FieldImpl(
					type: field.type,
					value: Closure(
						evaluator: Evaluator(),
						body: .cut(
							term: .local(index: 0),
							frame: .proj(fieldName: key)
						)
					)
				)
				fieldImpls.append((key, impl))
			}

		case (_, _, .universeCodes):
			try await equate(type: lhs.decode(size: .little(universe: ())), with: rhs.decode(size: .little(universe: ())))

		case let (.shift(neutral: lhs), .shift(neutral: rhs), .decode):
			try await equate(neutral: lhs, with: rhs)

		default:
			throw EqualityError.values(lhs: lhs, rhs: rhs, type: type)
		}
	}

	func equate(type lhs: Value.Type_, with rhs: Value.Type_) async throws {
		switch await (lhs.whnf(), rhs.whnf()) {

		case let (.funType(dom: dom1, boundName: _, fam: fam1), .funType(dom: dom2, boundName: _, fam: fam2)):
			try await equate(type: dom1, with: dom2)
			let x = fresh(type: AsyncThunk(value: dom1))
			let fibre1 = fam1.instantiate(with: x)
			let fibre2 = fam2.instantiate(with: x)
			try await next.equate(type: fibre1, with: fibre2)

		case let (.recordType(boundName: boundName, fields: fields1), .recordType(boundName: _, fields: fields2)):
			let error = EqualityError.types(lhs: lhs, rhs: rhs)
			guard fields1.keys == fields2.keys else { throw error }

			var fieldSpecs: [(String, Value.FieldSpec)] = []

			for (key, field1) in fields1.elements {
				let field2 = fields2[key]!
				guard (field1.manifest == nil) == ((field2.manifest == nil)) else { throw error }

				let prefixType: AsyncThunk<Value.Type_> = AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs)))
				let x = fresh(type: prefixType)
				let type1 = field1.type.instantiate(with: x)
				let type2 = field2.type.instantiate(with: x)
				try await next.equate(type: type1, with: type2)

				if let manifest1 = field1.manifest, let manifest2 = field2.manifest {
					let value1 = manifest1.instantiate(with: x)
					let value2 = manifest2.instantiate(with: x)
					try await next.equate(value: value1, with: value2, in: type1)
				}

				fieldSpecs.append((key, field1))
			}

		case (.universeType, .universeType): ()

		case let (.decode(size: size1, code: neutral1), .decode(size: size2, code: neutral2)):
			guard size1 == size2 else { throw EqualityError.types(lhs: lhs, rhs: rhs) }
			try await equate(neutral: neutral1, with: neutral2)

		case let (.universeCodes(size: lhs), .universeCodes(size: rhs)):
			try await equate(size: lhs, with: rhs)

		default:
			throw EqualityError.types(lhs: lhs, rhs: rhs)
		}
	}

	func equate(head lhs: Value.Head, with rhs: Value.Head) throws {
		guard lhs == rhs else { throw EqualityError.heads(lhs: lhs, rhs: rhs) }
	}

	func equate(frame lhs: Value.RichFrame, with rhs: Value.RichFrame) async throws {
		switch (lhs, rhs) {
		case let (.proj(fieldName: fieldName1), .proj(fieldName: fieldName2)):
			guard fieldName1 == fieldName2 else { throw EqualityError.frames(lhs: lhs, rhs: rhs) }
		case let (.app(dom: dom1, arg: arg1), .app(dom: _, arg: arg2)):
			try await equate(value: arg1, with: arg2, in: dom1.value())
		default:
			throw EqualityError.frames(lhs: lhs, rhs: rhs)
		}
	}

	func equate(spine lhs: Value.Spine, with rhs: Value.Spine) async throws {
		guard lhs.count == rhs.count else { throw EqualityError.spines(lhs: lhs, rhs: rhs) }

		for (index, frame1) in lhs.enumerated() {
			let frame2 = rhs[index]
			try await equate(frame: frame1, with: frame2)
		}
	}

	func equate(neutral lhs: Value.Neutral, with rhs: Value.Neutral) async throws {
		try equate(head: lhs.head, with: rhs.head)
		try await equate(spine: lhs.spine, with: rhs.spine)
	}
	
	func equate(size lhs: Size<Value>, with rhs: Size<Value>) async throws {
		try await assertLeq(size1: lhs, size2: rhs)
		try await assertLeq(size1: rhs, size2: lhs)
	}
}