~singpolyma/dhall-ruby

f31b87ce87b240ca3b0a6e9a01b0a12ca5ab1dbc — Stephen Paul Weber 3 years ago b730651
Implement "shift" function for variable indices
2 files changed, 82 insertions(+), 1 deletions(-)

M lib/dhall/normalize.rb
M test/test_normalization.rb
M lib/dhall/normalize.rb => lib/dhall/normalize.rb +24 -1
@@ 8,6 8,10 @@ module Dhall
			map_subexpressions(&:normalize)
		end

		def shift(amount, name, min_index)
			map_subexpressions { |expr| expr.shift(amount, name, min_index) }
		end

		def fusion(*); end
	end



@@ 35,6 39,13 @@ module Dhall
	end

	class Function
		def shift(amount, name, min_index)
			return super unless var == name
			with(
				type: type.shift(amount, name, min_index),
				body: body.shift(amount, name, min_index + 1)
			)
		end
	end

	class Forall; end


@@ 43,6 54,10 @@ module Dhall
	end

	class Variable
		def shift(amount, name, min_index)
			return self if self.name != name || min_index > index
			with(index: index + amount)
		end
	end

	class Operator


@@ 274,6 289,10 @@ module Dhall

	class LetBlock
		def normalize
			desugar.normalize
		end

		def desugar
			lets.reduce(body) { |inside, let|
				Application.new(
					function: Function.new(


@@ 283,7 302,11 @@ module Dhall
					),
					arguments: [let.assign]
				)
			}.normalize
			}
		end

		def shift(amount, name, min_index)
			desugar.shift(amont, name, min_index)
		end
	end


M test/test_normalization.rb => test/test_normalization.rb +58 -0
@@ 20,4 20,62 @@ class TestParser < Minitest::Test
			)
		end
	end

	def test_shift_1_x_0_x
		assert_equal(
			Dhall::Variable.new(name: "x", index: 1),
			Dhall::Variable.new(name: "x").shift(1, "x", 0)
		)
	end

	def test_shift_1_x_1_x
		assert_equal(
			Dhall::Variable.new(name: "x", index: 0),
			Dhall::Variable.new(name: "x").shift(1, "x", 1)
		)
	end

	def test_shift_1_x_0_y
		assert_equal(
			Dhall::Variable.new(name: "y", index: 0),
			Dhall::Variable.new(name: "y").shift(1, "x", 0)
		)
	end

	def test_shift_neg1_x_0_x1
		assert_equal(
			Dhall::Variable.new(name: "x", index: 0),
			Dhall::Variable.new(name: "x", index: 1).shift(-1, "x", 0)
		)
	end

	def test_shift_closed
		assert_equal(
			Dhall::Function.new(
				var: "x",
				type: Dhall::Variable.new(name: "Type"),
				body: Dhall::Variable.new(name: "x", index: 0)
			),
			Dhall::Function.new(
				var: "x",
				type: Dhall::Variable.new(name: "Type"),
				body: Dhall::Variable.new(name: "x", index: 0)
			).shift(1, "x", 0)
		)
	end

	def test_shift_free
		assert_equal(
			Dhall::Function.new(
				var: "y",
				type: Dhall::Variable.new(name: "Type"),
				body: Dhall::Variable.new(name: "x", index: 1)
			),
			Dhall::Function.new(
				var: "y",
				type: Dhall::Variable.new(name: "Type"),
				body: Dhall::Variable.new(name: "x", index: 0)
			).shift(1, "x", 0)
		)
	end
end