~singpolyma/dhall-ruby

ref: 0.2.0 dhall-ruby/test/test_typechecker.rb -rw-r--r-- 2.7 KiB View raw
a49a8991Stephen Paul Weber Customizable cache 1 year, 1 month ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
# frozen_string_literal: true

require "minitest/autorun"
require "pathname"

require "dhall"

class TestTypechecker < Minitest::Test
	DIRPATH = Pathname.new(File.dirname(__FILE__))
	TESTS = DIRPATH + "../dhall-lang/tests/typecheck/"

	Pathname.glob(TESTS + "success/**/*A.dhall").each do |path|
		test = path.relative_path_from(TESTS).to_s.sub(/A\.dhall$/, "")
		bside = TESTS + "#{test}B.dhall"

		define_method("test_#{test}") do
			parsed_a = Dhall::Parser.parse_file(path).value
			parsed_b = Dhall::Parser.parse_file(bside).value

			final_a, final_b = if test !~ /unit|simple/
				Promise.all([parsed_a, parsed_b].map { |e|
					e.resolve(
						relative_to: Dhall::Import::Path.from_string(path)
					)
				})
			else
				Promise.resolve([parsed_a, parsed_b])
			end.sync

			assert_respond_to(
				Dhall::TypeChecker.for(
					Dhall::TypeAnnotation.new(value: final_a, type: final_b)
				).annotate(Dhall::TypeChecker::Context.new),
				:type
			)
		end
	end

	Pathname.glob(TESTS + "failure/**/*.dhall").each do |path|
		test = path.relative_path_from(TESTS).to_s.sub(/.dhall$/, "")

		define_method("test_#{test}") do
			assert_raises TypeError do
				Dhall::TypeChecker.for(
					Dhall::Parser.parse_file(path).value
				).annotate(Dhall::TypeChecker::Context.new)
			end
		end
	end

	ITESTS = DIRPATH + "../dhall-lang/tests/type-inference/"

	Pathname.glob(ITESTS + "success/**/*A.dhall").each do |path|
		test = path.relative_path_from(TESTS).to_s.sub(/A\.dhall$/, "")

		define_method("test_#{test}") do
			assert_equal(
				Dhall::Parser.parse_file(ITESTS + "#{test}B.dhall").value,
				Dhall::TypeChecker.for(
					Dhall::Parser.parse_file(path).value
				).annotate(Dhall::TypeChecker::Context.new).type
			)
		end
	end

	def forall(var, type)
		Dhall::Forall.new(var: var, type: type, body: Dhall::Variable["UNKNOWN"])
	end

	def test_variable_in_context
		context =
			Dhall::TypeChecker::Context
			.new
			.add(forall("x", Dhall::Variable["Type"]))
			.add(forall("x", Dhall::Variable["Kind"]))

		assert_equal(
			Dhall::Variable["Kind"],
			Dhall::TypeChecker.for(
				Dhall::Variable["x"]
			).annotate(context).type
		)
	end

	def test_variable_in_parent_context
		context =
			Dhall::TypeChecker::Context
			.new
			.add(forall("x", Dhall::Variable["Type"]))
			.add(forall("x", Dhall::Variable["Kind"]))

		assert_equal(
			Dhall::Variable["Type"],
			Dhall::TypeChecker.for(
				Dhall::Variable["x", 1]
			).annotate(context).type
		)
	end

	def test_unknown_expression
		assert_raises TypeError do
			Dhall::TypeChecker.for(Class.new.new).annotate(
				Dhall::TypeChecker::Context.new
			)
		end
	end

	def test_unknown_builtin
		assert_raises TypeError do
			Dhall::TypeChecker.for(Class.new(Dhall::Builtin).new).annotate(
				Dhall::TypeChecker::Context.new
			)
		end
	end
end