~singpolyma/dhall-ruby

dhall-ruby/test/test_typechecker.rb -rw-r--r-- 3.2 KiB
7b768e2bStephen Paul Weber Fix map decode when transform_keys is not to_s 6 months 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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
# 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
			skip "duplicate union" if test =~ /UnionTypeDuplicateVariants/
			skip "duplicate record" if test =~ /RecordTypeDuplicateFields/

			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
			skip "alpha normalizing equivalences" if test =~ /AssertAlpha/

			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

	def test_enum
		union = Dhall::Enum.new(
			tag:          "red",
			alternatives: Dhall::UnionType.new(alternatives: {})
		)

		assert_equal(
			Dhall::UnionType.new(alternatives: { "red" => nil }),
			Dhall::TypeChecker.for(union).annotate(
				Dhall::TypeChecker::Context.new
			).type
		)
	end
end