From 7710663f239d4dc3af55f4bd0a1e57194389ba9c Mon Sep 17 00:00:00 2001
From: Stephen Paul Weber <singpolyma@singpolyma.net>
Date: Fri, 29 Mar 2019 21:11:54 -0500
Subject: [PATCH] Refactor List typecheck

---
 lib/dhall/ast.rb       | 37 ++++++++++++++++---------
 lib/dhall/binary.rb    |  5 ++--
 lib/dhall/typecheck.rb | 62 ++++++++++++++++++++++++------------------
 3 files changed, 62 insertions(+), 42 deletions(-)

diff --git a/lib/dhall/ast.rb b/lib/dhall/ast.rb
index 22f1a5e..5b98d20 100644
--- a/lib/dhall/ast.rb
+++ b/lib/dhall/ast.rb
@@ -266,12 +266,23 @@ module Dhall
 		include Enumerable
 
 		include(ValueSemantics.for_attributes do
-			elements Util::ArrayOf.new(Expression, min: 1)
-			type     Either(nil, Expression), default: nil
+			elements     Util::ArrayOf.new(Expression, min: 1)
+			element_type Either(nil, Expression), default: nil
 		end)
 
-		def self.of(*args)
-			List.new(elements: args)
+		def self.of(*args, type: nil)
+			if args.empty?
+				EmptyList.new(element_type: type)
+			else
+				List.new(elements: args, element_type: type)
+			end
+		end
+
+		def type
+			Dhall::Application.new(
+				function: Dhall::Variable["List"],
+				argument: element_type
+			)
 		end
 
 		def as_json
@@ -279,7 +290,7 @@ module Dhall
 		end
 
 		def map(type: nil, &block)
-			with(elements: elements.each_with_index.map(&block), type: type)
+			with(elements: elements.each_with_index.map(&block), element_type: type)
 		end
 
 		def each(&block)
@@ -296,11 +307,11 @@ module Dhall
 		end
 
 		def first
-			Optional.for(elements.first, type: type)
+			Optional.for(elements.first, type: element_type)
 		end
 
 		def last
-			Optional.for(elements.last, type: type)
+			Optional.for(elements.last, type: element_type)
 		end
 
 		def reverse
@@ -318,15 +329,15 @@ module Dhall
 
 	class EmptyList < List
 		include(ValueSemantics.for_attributes do
-			type Either(nil, Expression)
+			element_type Either(nil, Expression)
 		end)
 
 		def as_json
-			[4, type.as_json]
+			[4, element_type.as_json]
 		end
 
 		def map(type: nil)
-			type.nil? ? self : with(type: type)
+			type.nil? ? self : with(element_type: type)
 		end
 
 		def each
@@ -342,11 +353,11 @@ module Dhall
 		end
 
 		def first
-			OptionalNone.new(type: type)
+			OptionalNone.new(value_type: type)
 		end
 
 		def last
-			OptionalNone.new(type: type)
+			OptionalNone.new(value_type: type)
 		end
 
 		def reverse
@@ -366,7 +377,7 @@ module Dhall
 
 		def self.for(value, type: nil)
 			if value.nil?
-				OptionalNone.new(value_type: value_type)
+				OptionalNone.new(value_type: type)
 			else
 				Optional.new(value: value, value_type: type)
 			end
diff --git a/lib/dhall/binary.rb b/lib/dhall/binary.rb
index f4ff8c2..65a236b 100644
--- a/lib/dhall/binary.rb
+++ b/lib/dhall/binary.rb
@@ -79,10 +79,11 @@ module Dhall
 
 	class List
 		def self.decode(type, *els)
+			type = type.nil? ? nil : Dhall.decode(type)
 			if els.empty?
-				EmptyList.new(type: type.nil? ? nil : Dhall.decode(type))
+				EmptyList.new(element_type: type)
 			else
-				List.new(elements: els.map(&Dhall.method(:decode)))
+				List.new(elements: els.map(&Dhall.method(:decode)), element_type: type)
 			end
 		end
 	end
diff --git a/lib/dhall/typecheck.rb b/lib/dhall/typecheck.rb
index d577f17..0a1d893 100644
--- a/lib/dhall/typecheck.rb
+++ b/lib/dhall/typecheck.rb
@@ -11,6 +11,12 @@ module Dhall
 			end
 		end
 
+		def self.assert_type(expr, assertion, message, context:)
+			unless assertion === self.for(expr).annotate(context).type
+				raise TypeError, message
+			end
+		end
+
 		def self.for(expr)
 			case expr
 			when Dhall::Variable
@@ -385,18 +391,11 @@ module Dhall
 			end
 
 			def annotate(context)
-				type_type = TypeChecker.for(@expr.type).annotate(context).type
-				if type_type != Dhall::Variable["Type"]
-					raise TypeError, "EmptyList element type not of type Type"
-				end
+				TypeChecker.assert_type @expr.element_type, Dhall::Variable["Type"],
+				                        "EmptyList element type not of type Type",
+				                        context: context
 
-				Dhall::TypeAnnotation.new(
-					value: @expr,
-					type:  Dhall::Application.new(
-						function: Dhall::Variable["List"],
-						argument: @expr.type
-					)
-				)
+				@expr
 			end
 		end
 
@@ -405,28 +404,37 @@ module Dhall
 				@list = list
 			end
 
-			def annotate(context)
-				alist = @list.map(type: @list.type) do |el|
-					TypeChecker.for(el).annotate(context)
+			class AnnotatedList
+				def initialize(alist)
+					@alist = alist
 				end
-				list = alist.with(type: alist.first.value.type)
 
-				if (bad = alist.find { |x| x.type != list.type })
-					raise TypeError, "List #{list.type} with element #{bad}"
+				def list
+					@alist.with(element_type: element_type)
 				end
 
-				type_type = TypeChecker.for(list.type).annotate(context).type
-				if type_type != Dhall::Variable["Type"]
-					raise TypeError, "List type no of type Type, was: #{type_type}"
+				def element_type
+					@alist.first.value&.type || @alist.element_type
 				end
 
-				Dhall::TypeAnnotation.new(
-					value: list,
-					type:  Dhall::Application.new(
-						function: Dhall::Variable["List"],
-						argument: list.type
-					)
-				)
+				def element_types
+					@alist.to_a.map(&:type)
+				end
+			end
+
+			def annotate(context)
+				alist = AnnotatedList.new(@list.map(type: @list.element_type) { |el|
+					TypeChecker.for(el).annotate(context)
+				})
+
+				TypeChecker.assert alist.element_types,
+				                   Util::ArrayOf.new(alist.element_type),
+				                   "Non-homogenous List"
+
+				TypeChecker.assert_type alist.element_type, Dhall::Variable["Type"],
+				                        "List type not of type Type", context: context
+
+				alist.list
 			end
 		end
 
-- 
2.34.5