~singpolyma/dhall-ruby

7710663f239d4dc3af55f4bd0a1e57194389ba9c — Stephen Paul Weber 3 years ago 598e05f
Refactor List typecheck
3 files changed, 62 insertions(+), 42 deletions(-)

M lib/dhall/ast.rb
M lib/dhall/binary.rb
M lib/dhall/typecheck.rb
M lib/dhall/ast.rb => lib/dhall/ast.rb +24 -13
@@ 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

M lib/dhall/binary.rb => lib/dhall/binary.rb +3 -2
@@ 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

M lib/dhall/typecheck.rb => lib/dhall/typecheck.rb +35 -27
@@ 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