//  Copyright © 2015 Rob Rix. All rights reserved.

final class ElaborationTests: XCTestCase {
	func testInfersTheTypeOfType() {
		let term: Term = .Type
		assert(try? term.elaborateType(nil, [:], [:]), ==, .Unroll(.Type(1), .Identity(.Type(0))))
	}

	func testChecksLambdasAgainstFunctionTypes() {
		let type = .Type --> .Type
		let term = .Type => { $0 }
		let elaborated = try? term.elaborateType(type, [:], [:])
		assert(elaborated?.annotation, ==, type)
	}

	func testChecksLambdasAgainstDependentFunctionTypes() {
		let type = .Type => { A in A --> A }
		let term = .Type => { A in A => { a in a } }
		let elaborated = assertNoThrow(try term.elaborateType(type, [:], [:]))
		assert(elaborated?.annotation, ==, type)
	}
}

func assertNoThrow<A>(@autoclosure test: () throws -> A, file: String = __FILE__, line: UInt = __LINE__) -> A? {
	do {
		return try test()
	} catch {
		XCTFail("\(error)", file: file, line: line)
		return nil
	}
}


import Assertions
import Manifold
import XCTest

//  Copyright © 2015 Rob Rix. All rights reserved.

final class ElaborationTests: XCTestCase {
	func testInfersTheTypeOfType() {
		let term: Term = .Type
		assert(try? term.elaborateType(nil, [:], [:]), ==, .Unroll(.Type(1), .Identity(.Type(0))))
	}

	func testChecksLambdasAgainstFunctionTypes() {
		let actual = try? Term.Lambda(.Local(0), .Type, 0).elaborateType(.Type --> .Type, [:], [:])
		let expected: AnnotatedTerm<Term> = .Unroll(.Type --> .Type, .Identity(.Lambda(.Unroll(.Type(1), .Identity(.Type(0))), .Unroll(.Type, .Abstraction(.Local(0), .Unroll(.Type, .Variable(.Local(0))))))))
		assert(actual, ==, expected)
	}

	func testChecksLambdasAgainstDependentFunctionTypes() {
		let type = .Type => { A in A --> A }
		let term = .Type => { A in A => { a in a } }
		let elaborated = assertNoThrow(try term.elaborateType(type, [:], [:]))
		assert(elaborated?.annotation, ==, type)
	}
}

func assertNoThrow<A>(@autoclosure test: () throws -> A, file: String = __FILE__, line: UInt = __LINE__) -> A? {
	do {
		return try test()
	} catch {
		XCTFail("\(error)", file: file, line: line)
		return nil
	}
}


import Assertions
import Manifold
import XCTest

--- 
+++ 
@@ -7,9 +7,10 @@
 	}
 
 	func testChecksLambdasAgainstFunctionTypes() {
-		let actual = try? Term.Lambda(.Local(0), .Type, 0).elaborateType(.Type --> .Type, [:], [:])
-		let expected: AnnotatedTerm<Term> = .Unroll(.Type --> .Type, .Identity(.Lambda(.Unroll(.Type(1), .Identity(.Type(0))), .Unroll(.Type, .Abstraction(.Local(0), .Unroll(.Type, .Variable(.Local(0))))))))
-		assert(actual, ==, expected)
+		let type = .Type --> .Type
+		let term = .Type => { $0 }
+		let elaborated = try? term.elaborateType(type, [:], [:])
+		assert(elaborated?.annotation, ==, type)
 	}
 
 	func testChecksLambdasAgainstDependentFunctionTypes() {
Change the function type elaboration test to simply test the elaborated types for equality.
