~singpolyma/dhall-ruby

ref: 2335534da241446a1f1b7cde96e4828995cb1103 dhall-ruby/test/test_typechecker.rb -rw-r--r-- 1.5 KiB
2335534dStephen Paul Weber Type inference/checking about half done 3 years 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
# frozen_string_literal: true

require "minitest/autorun"
require "pathname"

require "dhall/typecheck"
require "dhall/binary"

class TestNormalization < Minitest::Test
	DIRPATH = Pathname.new(File.dirname(__FILE__))
	TESTS = DIRPATH + "typechecker/"

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

		define_method("test_#{test}") do
			assert_equal(
				Dhall.from_binary((TESTS + "#{test}B.dhallb").binread),
				Dhall::TypeChecker.for(
					Dhall.from_binary(path.binread)
				).annotate(Dhall::TypeChecker::Context.new).type
			)
		end
	end

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

		define_method("test_#{test}") do
			assert_raises TypeError do
				expr = Dhall.from_binary(path.binread)
				Dhall::TypeChecker.for(
					expr
				).annotate(Dhall::TypeChecker::Context.new).type
			end
		end
	end

	def test_variable_in_context
		context =
			Dhall::TypeChecker::Context.new
				.add("x", Dhall::Variable["Type"])
				.add("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("x", Dhall::Variable["Type"])
				.add("x", Dhall::Variable["Kind"])

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