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

import Testing
@testable import PterodactylKernel

struct SizeTests {
	@Test func leqIsReflexive() async throws {
		let analysis = LocalAnalysis()
		
		await #expect(throws: Never.self) {
			try await analysis.assertLeq(size1: .big, size2: .big)
		}
	}
	
	@Test func moderateIsNotSmall() async throws {
		let analysis = LocalAnalysis()
		
		await #expect(throws: LocalAnalysis.SizeError.self) {
			try await analysis.assertLeq(size1: .big, size2: .little(universe: .universeZero))
		}
	}
	
	@Test func lubIsCommutative() async throws {
		let analysis = LocalAnalysis()
		await #expect(throws: Never.self) {
			let lhs = Value.universeLub(.universeZero, .universeSucc(.universeZero))
			let rhs = Value.universeLub(.universeSucc(.universeZero), .universeZero)
			try await analysis.equate(size: .little(universe: lhs), with: .little(universe: rhs))
		}
	}
	
	@Test func lubZeroLeftUnit() async throws {
		let analysis = LocalAnalysis()
		await #expect(throws: Never.self) {
			let lhs = Value.universeLub(.universeZero, .universeSucc(.universeZero))
			let rhs = Value.universeSucc(.universeZero)
			try await analysis.equate(size: .little(universe: lhs), with: .little(universe: rhs))
		}
	}
	
	@Test func lubZeroRightUnit() async throws {
		let analysis = LocalAnalysis()
		await #expect(throws: Never.self) {
			let lhs = Value.universeLub(.universeSucc(.universeZero), .universeZero)
			let rhs = Value.universeSucc(.universeZero)
			try await analysis.equate(size: .little(universe: lhs), with: .little(universe: rhs))
		}
	}
	
	@Test func succDistributesOverLub() async throws {
		let analysis = LocalAnalysis()
		await #expect(throws: Never.self) {
			let lhs = Value.universeSucc(Value.universeLub(.universeZero, .universeSucc(.universeZero)))
			let rhs = Value.universeLub(.universeSucc(.universeSucc(.universeZero)), .universeSucc(.universeZero))
			try await analysis.equate(size: .little(universe: lhs), with: .little(universe: rhs))
		}
	}
	
}