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

import Foundation

extension LocalAnalysis {
	struct SizeError: Error { }

	func assertSize(type: Value.Type_, size: Size<Value>) async throws {
		switch await type.whnf() {

		// In principle the type of universes could be small, but I am worried about about the strictness of the semilattice operations. I know how to interpret them if universeType is exoNat as in 2LTT, but in that case universeType probably should not be fibrant.
		case .universeType, .universeCodes(size: .big):
			throw SizeError()

		case let .universeCodes(size: .little(universe: littleUniverse)):
			try await assertLeq(size1: .little(universe: .universeSucc(littleUniverse)), size2: size)

		case let .decode(size: _, code: code):
			guard case let .universeCodes(size: littleSize) = await code.boundary.value().type.whnf() else { fatalError() }
			try await assertLeq(size1: littleSize, size2: size)
			
		case let .funType(dom: dom, boundName: _, fam: fam):
			try await assertSize(type: dom, size: size)
			let domThunk = AsyncThunk(value: dom)
			let x = fresh(type: domThunk)
			let fibre = fam.instantiate(with: x)
			try await next.assertSize(type: fibre, size: size)

		case let .recordType(boundName: boundName, fields: fields):
			var fieldSpecs: [(String, Value.FieldSpec)] = []
			for (key, fieldSpec) in fields.elements {
				if fieldSpec.manifest == nil {
					let prefixType: AsyncThunk<Value.Type_> = AsyncThunk(value: .recordType(boundName: boundName, fields: FieldDict(fieldSpecs)))
					let prefixRecord = fresh(type: prefixType)
					try await next.assertSize(type: fieldSpec.type.instantiate(with: prefixRecord), size: size)
				}

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

	func assertSmall(type: Value.Type_, universe: Value) async throws {
		try await assertSize(type: type, size: .little(universe: universe))
	}

	func assertLeq(size1: Size<Value>, size2: Size<Value>) async throws {
		switch (size1, size2) {
		case (_, .big): ()
		case let (.little(universe: universe1), .little(universe: universe2)):
			try await assertLeq(universe1: universe1, universe2: universe2)
		default:
			throw SizeError()
		}
	}
	
	func assertLeq(universe1: Value, universe2: Value) async throws {
		switch await (universe1.whnf(), universe2.whnf()) {
		case (.universeZero, _): ()
		case let (.universeLub(universe11, universe12), _):
			try await assertLeq(universe1: universe11, universe2: universe2)
			try await assertLeq(universe1: universe12, universe2: universe2)
		case let (.universeSucc(universe: universe1), .universeSucc(universe: universe2)):
			try await assertLeq(universe1: universe1, universe2: universe2)
		case let (_, .universeLub(universe21, universe22)):
			do {
				try await assertLeq(universe1: universe1, universe2: universe21)
			} catch {
				try await assertLeq(universe1: universe1, universe2: universe22)
			}
		case let (_, .universeSucc(universe: universe2)):
			try await assertLeq(universe1: universe1, universe2: universe2)
		case let (.shift(neutral: neutral1), .shift(neutral: neutral2)):
			try await equate(neutral: neutral1, with: neutral2)
		default:
			throw SizeError()
		}
	}
}