From f31b87ce87b240ca3b0a6e9a01b0a12ca5ab1dbc Mon Sep 17 00:00:00 2001
From: Stephen Paul Weber <singpolyma@singpolyma.net>
Date: Thu, 7 Mar 2019 23:46:22 -0500
Subject: [PATCH] Implement "shift" function for variable indices

---
 lib/dhall/normalize.rb     | 25 +++++++++++++++-
 test/test_normalization.rb | 58 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 82 insertions(+), 1 deletion(-)

diff --git a/lib/dhall/normalize.rb b/lib/dhall/normalize.rb
index 89afda7..fe6cd84 100644
--- a/lib/dhall/normalize.rb
+++ b/lib/dhall/normalize.rb
@@ -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
 
diff --git a/test/test_normalization.rb b/test/test_normalization.rb
index f49f4d1..f8d4ceb 100644
--- a/test/test_normalization.rb
+++ b/test/test_normalization.rb
@@ -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
-- 
2.38.4