~singpolyma/dhall-ruby

e1dfd24714825b517fd88ae5e30995ff04f361ca — Stephen Paul Weber 3 years ago 1f819b2
Update handling of builtins

Always parse to a special value and not to variables.
Encode seperately.
M lib/dhall/ast.rb => lib/dhall/ast.rb +56 -24
@@ 114,9 114,7 @@ module Dhall
		end)

		def self.for(function:, argument:)
			if function == Variable["Some"]
				Optional.new(value: argument)
			elsif function == Variable["None"]
			if function == Builtins[:None]
				OptionalNone.new(value_type: argument)
			else
				new(function: function, argument: argument)


@@ 144,7 142,7 @@ module Dhall

	class Function < Expression
		include(ValueSemantics.for_attributes do
			var  Util::AllOf.new(::String, Util::Not.new(Util::BuiltinName))
			var  ::String
			type Either(nil, Expression) # nil is not allowed in proper Dhall
			body Expression
		end)


@@ 230,6 228,10 @@ module Dhall
		def as_json
			value
		end

		def self.as_dhall
			Builtins[:Bool]
		end
	end

	class Variable < Expression


@@ 249,8 251,6 @@ module Dhall
		def as_json
			if name == "_"
				index
			elsif index.zero?
				name
			else
				[name, index]
			end


@@ 305,9 305,13 @@ module Dhall
			end
		end

		def self.as_dhall
			Builtins[:List]
		end

		def type
			Dhall::Application.new(
				function: Dhall::Variable["List"],
				function: self.class.as_dhall,
				argument: element_type
			)
		end


@@ 317,7 321,10 @@ module Dhall
		end

		def map(type: nil, &block)
			with(elements: elements.each_with_index.map(&block), element_type: type)
			with(
				elements:     elements.each_with_index.map(&block),
				element_type: type&.as_dhall
			)
		end

		def each(&block)


@@ 422,6 429,10 @@ module Dhall
			end
		end

		def self.as_dhall
			Builtins[:Natural]
		end

		def initialize(normalized: false, **attrs)
			@normalized = normalized
			super(**attrs)


@@ 431,7 442,7 @@ module Dhall
			return unless value_type

			Dhall::Application.new(
				function: Dhall::Variable["Optional"],
				function: Builtins[:Optional],
				argument: value_type
			)
		end


@@ 458,6 469,10 @@ module Dhall
			value_type Expression
		end)

		def self.as_dhall
			Builtins[:None]
		end

		def map(type: nil)
			type.nil? ? self : with(value_type: type)
		end


@@ 471,7 486,10 @@ module Dhall
		end

		def as_json
			[0, Variable["None"].as_json, value_type.as_json]
			Application.new(
				function: self.class.as_dhall,
				argument: value_type
			).as_json
		end
	end



@@ 776,10 794,9 @@ module Dhall
		end

		def get_constructor(selector)
			var = Util::BuiltinName === selector ? "_" : selector
			type = alternatives.fetch(selector)
			body = Union.from(self, selector, Variable[var])
			Function.new(var: var, type: type, body: body)
			body = Union.from(self, selector, Variable[selector])
			Function.new(var: selector, type: type, body: body)
		end

		def constructor_types


@@ 787,8 804,7 @@ module Dhall
				ctypes[k] = if type.nil?
					self
				else
					var = Util::BuiltinName === k ? "_" : k
					Forall.new(var: var, type: type, body: self)
					Forall.new(var: k, type: type, body: self)
				end
			end
		end


@@ 889,6 905,10 @@ module Dhall
			value (0..Float::INFINITY)
		end)

		def self.as_dhall
			Builtins[:Natural]
		end

		def coerce(other)
			[other.as_dhall, self]
		end


@@ 950,6 970,10 @@ module Dhall
			value ::Integer
		end)

		def self.as_dhall
			Builtins[:Integer]
		end

		def to_s
			"#{value >= 0 ? "+" : ""}#{value}"
		end


@@ 972,6 996,10 @@ module Dhall
			value ::Float
		end)

		def self.as_dhall
			Builtins[:Double]
		end

		def to_s
			value.to_s
		end


@@ 1026,6 1054,10 @@ module Dhall
			value ::String, coerce: ->(s) { s.encode("UTF-8") }
		end)

		def self.as_dhall
			Builtins[:Double]
		end

		def <<(other)
			if other.is_a?(Text)
				with(value: value + other.value)


@@ 1111,13 1143,6 @@ module Dhall
				query     Either(nil, ::String)
			end)

			HeaderType = RecordType.new(
				record: {
					"header" => Variable["Text"],
					"value"  => Variable["Text"]
				}
			)

			def initialize(headers, authority, *path, query)
				super(
					headers:   headers,


@@ 1147,7 1172,14 @@ module Dhall
			end

			def headers
				super || EmptyList.new(element_type: HeaderType)
				header_type = RecordType.new(
					record: {
						"header" => Builtins[:Text],
						"value"  => Builtins[:Text]
					}
				)

				super || EmptyList.new(element_type: header_type)
			end

			def uri


@@ 1485,7 1517,7 @@ module Dhall

	class Let < Expression
		include(ValueSemantics.for_attributes do
			var    Util::AllOf.new(::String, Util::Not.new(Util::BuiltinName))
			var    ::String
			assign Expression
			type   Either(nil, Expression)
		end)

M lib/dhall/binary.rb => lib/dhall/binary.rb +1 -1
@@ 227,7 227,7 @@ module Dhall
		::TrueClass    => ->(e) { Bool.new(value: e) },
		::FalseClass   => ->(e) { Bool.new(value: e) },
		::Float        => ->(e) { Double.new(value: e) },
		::String       => ->(e) { Builtins::ALL[e]&.new || Variable.new(name: e) },
		::String       => ->(e) { Builtins[e.to_sym] || (raise "Unknown builtin") },
		::Integer      => ->(e) { Variable.new(index: e) },
		::Array        => lambda { |e|
			if e.length == 2 && e.first.is_a?(::String)

M lib/dhall/builtins.rb => lib/dhall/builtins.rb +78 -39
@@ 64,8 64,8 @@ module Dhall

		class Double_show < Builtin
			def call(arg)
				if arg.is_a?(Double)
					Text.new(value: arg.to_s)
				if arg.is_a?(Dhall::Double)
					Dhall::Text.new(value: arg.to_s)
				else
					super
				end


@@ 74,8 74,8 @@ module Dhall

		class Integer_show < Builtin
			def call(arg)
				if arg.is_a?(Integer)
					Text.new(value: arg.to_s)
				if arg.is_a?(Dhall::Integer)
					Dhall::Text.new(value: arg.to_s)
				else
					super
				end


@@ 84,8 84,8 @@ module Dhall

		class Integer_toDouble < Builtin
			def call(arg)
				if arg.is_a?(Integer)
					Double.new(value: arg.value.to_f)
				if arg.is_a?(Dhall::Integer)
					Dhall::Double.new(value: arg.value.to_f)
				else
					super
				end


@@ 105,20 105,20 @@ module Dhall

			def call(arg)
				arg.call(
					Variable.new(name: "Natural"),
					Natural.new,
					Function.of_arguments(
						Variable.new(name: "Natural"),
						body: Variable["_"] + Natural.new(value: 1)
						Natural.new,
						body: Variable["_"] + Dhall::Natural.new(value: 1)
					),
					Natural.new(value: 0)
					Dhall::Natural.new(value: 0)
				)
			end
		end

		class Natural_even < Builtin
			def call(nat)
				if nat.is_a?(Natural)
					Bool.new(value: nat.even?)
				if nat.is_a?(Dhall::Natural)
					Dhall::Bool.new(value: nat.even?)
				else
					super
				end


@@ 127,9 127,9 @@ module Dhall

		class Natural_fold < Builtin
			include(ValueSemantics.for_attributes do
				nat  Either(nil, Natural),    default: nil
				type Either(nil, Expression), default: nil
				f    Either(nil, Expression), default: nil
				nat  Either(nil, Dhall::Natural), default: nil
				type Either(nil, Expression),     default: nil
				f    Either(nil, Expression),     default: nil
			end)

			def call(arg)


@@ 145,8 145,8 @@ module Dhall

		class Natural_isZero < Builtin
			def call(nat)
				if nat.is_a?(Natural)
					Bool.new(value: nat.zero?)
				if nat.is_a?(Dhall::Natural)
					Dhall::Bool.new(value: nat.zero?)
				else
					super
				end


@@ 155,8 155,8 @@ module Dhall

		class Natural_odd < Builtin
			def call(nat)
				if nat.is_a?(Natural)
					Bool.new(value: nat.odd?)
				if nat.is_a?(Dhall::Natural)
					Dhall::Bool.new(value: nat.odd?)
				else
					super
				end


@@ 165,8 165,8 @@ module Dhall

		class Natural_show < Builtin
			def call(nat)
				if nat.is_a?(Natural)
					Text.new(value: nat.to_s)
				if nat.is_a?(Dhall::Natural)
					Dhall::Text.new(value: nat.to_s)
				else
					super
				end


@@ 175,8 175,8 @@ module Dhall

		class Natural_toInteger < Builtin
			def call(nat)
				if nat.is_a?(Natural)
					Integer.new(value: nat.value)
				if nat.is_a?(Dhall::Natural)
					Dhall::Integer.new(value: nat.value)
				else
					super
				end


@@ 202,7 202,7 @@ module Dhall
			def call(arg)
				fill_or_call(arg) do
					arg.call(
						Variable["List"].call(type),
						List.new.call(type),
						cons,
						EmptyList.new(element_type: type)
					)


@@ 214,8 214,8 @@ module Dhall
			def cons
				Function.of_arguments(
					type,
					Variable["List"].call(type.shift(1, "_", 0)),
					body: List.of(Variable["_", 1]).concat(Variable["_"])
					List.new.call(type.shift(1, "_", 0)),
					body: Dhall::List.of(Variable["_", 1]).concat(Variable["_"])
				)
			end
		end


@@ 242,7 242,7 @@ module Dhall

			def call(arg)
				fill_or_call(arg) do
					if arg.is_a?(List)
					if arg.is_a?(Dhall::List)
						arg.first
					else
						super


@@ 258,7 258,7 @@ module Dhall

			def call(arg)
				fill_or_call(arg) do
					if arg.is_a?(List)
					if arg.is_a?(Dhall::List)
						_call(arg)
					else
						super


@@ 272,7 272,7 @@ module Dhall
				arg.map(type: indexed_type(type)) { |x, idx|
					Record.new(
						record: {
							"index" => Natural.new(value: idx),
							"index" => Dhall::Natural.new(value: idx),
							"value" => x
						}
					)


@@ 282,7 282,7 @@ module Dhall
			def indexed_type(value_type)
				RecordType.new(
					record: {
						"index" => Variable.new(name: "Natural"),
						"index" => Natural.new,
						"value" => value_type
					}
				)


@@ 296,7 296,7 @@ module Dhall

			def call(arg)
				fill_or_call(arg) do
					if arg.is_a?(List)
					if arg.is_a?(Dhall::List)
						arg.last
					else
						super


@@ 312,8 312,8 @@ module Dhall

			def call(arg)
				fill_or_call(arg) do
					if arg.is_a?(List)
						Natural.new(value: arg.length)
					if arg.is_a?(Dhall::List)
						Dhall::Natural.new(value: arg.length)
					else
						super
					end


@@ 328,7 328,7 @@ module Dhall

			def call(arg)
				fill_or_call(arg) do
					if arg.is_a?(List)
					if arg.is_a?(Dhall::List)
						arg.reverse
					else
						super


@@ 356,7 356,7 @@ module Dhall
			def call(arg)
				fill_or_call(arg) do
					arg.call(
						Variable["Optional"].call(type),
						Optional.new.call(type),
						some,
						OptionalNone.new(value_type: type)
					)


@@ 368,7 368,7 @@ module Dhall
			def some
				Function.of_arguments(
					type,
					body: Optional.new(
					body: Dhall::Optional.new(
						value:      Variable["_"],
						value_type: type
					)


@@ 405,8 405,8 @@ module Dhall
			)

			def call(arg)
				if arg.is_a?(Text)
					Text.new(
				if arg.is_a?(Dhall::Text)
					Dhall::Text.new(
						value: "\"#{arg.value.gsub(
							/["\$\\\b\f\n\r\t\u0000-\u001F]/,
							&ENCODE


@@ 418,8 418,47 @@ module Dhall
			end
		end

		class Bool < Builtin
		end

		class Optional < Builtin
		end

		class Natural < Builtin
		end

		class Integer < Builtin
		end

		class Double < Builtin
		end

		class Text < Builtin
		end

		class List < Builtin
		end

		class None < Builtin
			def call(arg)
				OptionalNone.new(value_type: arg)
			end
		end

		class Type < Builtin
		end

		class Kind < Builtin
		end

		class Sort < Builtin
		end

		# rubocop:enable Style/ClassAndModuleCamelCase

		ALL = Hash[constants.map { |c| [c.to_s.tr("_", "/"), const_get(c)] }]
		def self.[](k)
			const = constants.find { |c| c.to_s.tr("_", "/").to_sym == k }
			const && const_get(const).new
		end
	end
end

M lib/dhall/parser.rb => lib/dhall/parser.rb +1 -1
@@ 325,7 325,7 @@ module Dhall
				return Dhall::Bool.new(value: true) if name == "True"
				return Dhall::Bool.new(value: false) if name == "False"

				(!name.quoted? && Dhall::Builtins::ALL[name]&.new) ||
				(!name.quoted? && Dhall::Builtins[name.to_sym]) ||
					Variable.new(
						name:  name,
						index: capture(:natural_literal)&.string.to_i

M lib/dhall/typecheck.rb => lib/dhall/typecheck.rb +97 -99
@@ 72,9 72,9 @@ module Dhall
		end

		KINDS = [
			Dhall::Variable["Type"],
			Dhall::Variable["Kind"],
			Dhall::Variable["Sort"]
			Builtins[:Type],
			Builtins[:Kind],
			Builtins[:Sort]
		].freeze

		class Variable


@@ 84,38 84,12 @@ module Dhall
				@var = var
			end

			BUILTIN = {
				"Type"     => Dhall::Variable["Kind"],
				"Kind"     => Dhall::Variable["Sort"],
				"Bool"     => Dhall::Variable["Type"],
				"Natural"  => Dhall::Variable["Type"],
				"Integer"  => Dhall::Variable["Type"],
				"Double"   => Dhall::Variable["Type"],
				"Text"     => Dhall::Variable["Type"],
				"List"     => Dhall::Forall.of_arguments(
					Dhall::Variable["Type"],
					body: Dhall::Variable["Type"]
				),
				"Optional" => Dhall::Forall.of_arguments(
					Dhall::Variable["Type"],
					body: Dhall::Variable["Type"]
				),
				"None"     => Dhall::Forall.new(
					var:  "A",
					type: Dhall::Variable["Type"],
					body: Dhall::Application.new(
						function: Dhall::Variable["Optional"],
						argument: Dhall::Variable["A"]
					)
				)
			}.freeze

			def annotate(context)
				raise TypeError, "Sort has no Type, Kind, or Sort" if @var.name == "Sort"

				Dhall::TypeAnnotation.new(
					value: @var,
					type:  BUILTIN.fetch(@var.name) { context.fetch(@var) }
					type:  context.fetch(@var)
				)
			end
		end


@@ 130,6 104,7 @@ module Dhall
			def initialize(lit)
				@lit = lit
				@type = Dhall::Variable[lit.class.name.split(/::/).last]
				@type = Builtins[@type.name.to_sym] || @type
			end

			def annotate(*)


@@ 170,14 145,14 @@ module Dhall
			def annotate(context)
				chunks = Chunks.new(@lit.chunks).map { |c|
					TypeChecker.for(c).annotate(context).tap do |annotated|
						TypeChecker.assert annotated.type, Dhall::Variable["Text"],
						TypeChecker.assert annotated.type, Builtins[:Text],
						                   "Cannot interpolate #{annotated.type}"
					end
				}.to_a

				Dhall::TypeAnnotation.new(
					value: @lit.with(chunks: chunks),
					type:  Dhall::Variable["Text"]
					type:  Builtins[:Text]
				)
			end
		end


@@ 194,9 169,9 @@ module Dhall

			class AnnotatedIf
				def initialize(expr, apred, athen, aelse, context:)
					TypeChecker.assert apred.type, Dhall::Variable["Bool"],
					TypeChecker.assert apred.type, Builtins[:Bool],
					                   "If must have a predicate of type Bool"
					TypeChecker.assert_type athen.type, Dhall::Variable["Type"],
					TypeChecker.assert_type athen.type, Builtins[:Type],
					                        "If branches must have types of type Type",
					                        context: context
					TypeChecker.assert aelse.type, athen.type,


@@ 225,13 200,13 @@ module Dhall

		class Operator
			{
				Dhall::Operator::And             => Dhall::Variable["Bool"],
				Dhall::Operator::Or              => Dhall::Variable["Bool"],
				Dhall::Operator::Equal           => Dhall::Variable["Bool"],
				Dhall::Operator::NotEqual        => Dhall::Variable["Bool"],
				Dhall::Operator::Plus            => Dhall::Variable["Natural"],
				Dhall::Operator::Times           => Dhall::Variable["Natural"],
				Dhall::Operator::TextConcatenate => Dhall::Variable["Text"]
				Dhall::Operator::And             => Builtins[:Bool],
				Dhall::Operator::Or              => Builtins[:Bool],
				Dhall::Operator::Equal           => Builtins[:Bool],
				Dhall::Operator::NotEqual        => Builtins[:Bool],
				Dhall::Operator::Plus            => Builtins[:Natural],
				Dhall::Operator::Times           => Builtins[:Natural],
				Dhall::Operator::TextConcatenate => Builtins[:Text]
			}.each do |node_type, type|
				TypeChecker.register self, node_type, type
			end


@@ 270,7 245,7 @@ module Dhall
			module IsList
				def self.===(other)
					other.is_a?(Dhall::Application) &&
						other.function == Dhall::Variable["List"]
						other.function == Builtins[:List]
				end
			end



@@ 387,7 362,7 @@ module Dhall
			end

			def annotate(context)
				TypeChecker.assert_type @expr.element_type, Dhall::Variable["Type"],
				TypeChecker.assert_type @expr.element_type, Builtins[:Type],
				                        "EmptyList element type not of type Type",
				                        context: context



@@ 430,7 405,7 @@ module Dhall
				                   Util::ArrayOf.new(alist.element_type),
				                   "Non-homogenous List"

				TypeChecker.assert_type alist.element_type, Dhall::Variable["Type"],
				TypeChecker.assert_type alist.element_type, Builtins[:Type],
				                        "List type not of type Type", context: context

				alist.annotation


@@ 447,7 422,7 @@ module Dhall
			def annotate(context)
				TypeChecker.assert(
					TypeChecker.for(@expr.value_type).annotate(context).type,
					Dhall::Variable["Type"],
					Builtins[:Type],
					"OptionalNone element type not of type Type"
				)



@@ 469,7 444,7 @@ module Dhall
				some = asome.with(value_type: asome.value.type)

				type_type = TypeChecker.for(some.value_type).annotate(context).type
				TypeChecker.assert type_type, Dhall::Variable["Type"],
				TypeChecker.assert type_type, Builtins[:Type],
				                   "Some type not of type Type, was: #{type_type}"

				Dhall::TypeAnnotation.new(type: some.type, value: some)


@@ 486,7 461,7 @@ module Dhall
			def annotate(*)
				Dhall::TypeAnnotation.new(
					value: @expr,
					type:  Dhall::Variable["Type"]
					type:  Builtins[:Type]
				)
			end
		end


@@ 562,7 537,7 @@ module Dhall

			class Selector
				def self.for(annotated_record)
					if annotated_record.type == Dhall::Variable["Type"]
					if annotated_record.type == Builtins[:Type]
						TypeSelector.new(annotated_record.value)
					elsif annotated_record.type.class == Dhall::RecordType
						new(annotated_record.type)


@@ 727,7 702,7 @@ module Dhall

					TypeChecker.assert(
						kind,
						Dhall::Variable["Type"],
						Builtins[:Type],
						"Merge must have kind Type"
					)



@@ 934,10 909,33 @@ module Dhall
		end

		BUILTIN_TYPES = {
			"Bool"              => Builtins[:Type],
			"Type"              => Builtins[:Kind],
			"Kind"              => Builtins[:Sort],
			"Natural"           => Builtins[:Type],
			"Integer"           => Builtins[:Type],
			"Double"            => Builtins[:Type],
			"Text"              => Builtins[:Type],
			"List"              => Dhall::Forall.of_arguments(
				Builtins[:Type],
				body: Builtins[:Type]
			),
			"Optional"          => Dhall::Forall.of_arguments(
				Builtins[:Type],
				body: Builtins[:Type]
			),
			"None"              => Dhall::Forall.new(
				var:  "A",
				type: Builtins[:Type],
				body: Dhall::Application.new(
					function: Builtins[:Optional],
					argument: Dhall::Variable["A"]
				)
			),
			"Natural/build"     => Dhall::Forall.of_arguments(
				Dhall::Forall.new(
					var:  "natural",
					type: Dhall::Variable["Type"],
					type: Builtins[:Type],
					body: Dhall::Forall.new(
						var:  "succ",
						type: Dhall::Forall.of_arguments(


@@ 951,13 949,13 @@ module Dhall
						)
					)
				),
				body: Dhall::Variable["Natural"]
				body: Builtins[:Natural]
			),
			"Natural/fold"      => Dhall::Forall.of_arguments(
				Dhall::Variable["Natural"],
				Builtins[:Natural],
				body: Dhall::Forall.new(
					var:  "natural",
					type: Dhall::Variable["Type"],
					type: Builtins[:Type],
					body: Dhall::Forall.new(
						var:  "succ",
						type: Dhall::Forall.of_arguments(


@@ 973,36 971,36 @@ module Dhall
				)
			),
			"Natural/isZero"    => Dhall::Forall.of_arguments(
				Dhall::Variable["Natural"],
				body: Dhall::Variable["Bool"]
				Builtins[:Natural],
				body: Builtins[:Bool]
			),
			"Natural/even"      => Dhall::Forall.of_arguments(
				Dhall::Variable["Natural"],
				body: Dhall::Variable["Bool"]
				Builtins[:Natural],
				body: Builtins[:Bool]
			),
			"Natural/odd"       => Dhall::Forall.of_arguments(
				Dhall::Variable["Natural"],
				body: Dhall::Variable["Bool"]
				Builtins[:Natural],
				body: Builtins[:Bool]
			),
			"Natural/toInteger" => Dhall::Forall.of_arguments(
				Dhall::Variable["Natural"],
				body: Dhall::Variable["Integer"]
				Builtins[:Natural],
				body: Builtins[:Integer]
			),
			"Natural/show"      => Dhall::Forall.of_arguments(
				Dhall::Variable["Natural"],
				body: Dhall::Variable["Text"]
				Builtins[:Natural],
				body: Builtins[:Text]
			),
			"Text/show"         => Dhall::Forall.of_arguments(
				Dhall::Variable["Text"],
				body: Dhall::Variable["Text"]
				Builtins[:Text],
				body: Builtins[:Text]
			),
			"List/build"        => Dhall::Forall.new(
				var:  "a",
				type: Dhall::Variable["Type"],
				type: Builtins[:Type],
				body: Dhall::Forall.of_arguments(
					Dhall::Forall.new(
						var:  "list",
						type: Dhall::Variable["Type"],
						type: Builtins[:Type],
						body: Dhall::Forall.new(
							var:  "cons",
							type: Dhall::Forall.of_arguments(


@@ 1018,22 1016,22 @@ module Dhall
						)
					),
					body: Dhall::Application.new(
						function: Dhall::Variable["List"],
						function: Builtins[:List],
						argument: Dhall::Variable["a"]
					)
				)
			),
			"List/fold"         => Dhall::Forall.new(
				var:  "a",
				type: Dhall::Variable["Type"],
				type: Builtins[:Type],
				body: Dhall::Forall.of_arguments(
					Dhall::Application.new(
						function: Dhall::Variable["List"],
						function: Builtins[:List],
						argument: Dhall::Variable["a"]
					),
					body: Dhall::Forall.new(
						var:  "list",
						type: Dhall::Variable["Type"],
						type: Builtins[:Type],
						body: Dhall::Forall.new(
							var:  "cons",
							type: Dhall::Forall.of_arguments(


@@ 1052,56 1050,56 @@ module Dhall
			),
			"List/length"       => Dhall::Forall.new(
				var:  "a",
				type: Dhall::Variable["Type"],
				type: Builtins[:Type],
				body: Dhall::Forall.of_arguments(
					Dhall::Application.new(
						function: Dhall::Variable["List"],
						function: Builtins[:List],
						argument: Dhall::Variable["a"]
					),
					body: Dhall::Variable["Natural"]
					body: Builtins[:Natural]
				)
			),
			"List/head"         => Dhall::Forall.new(
				var:  "a",
				type: Dhall::Variable["Type"],
				type: Builtins[:Type],
				body: Dhall::Forall.of_arguments(
					Dhall::Application.new(
						function: Dhall::Variable["List"],
						function: Builtins[:List],
						argument: Dhall::Variable["a"]
					),
					body: Dhall::Application.new(
						function: Dhall::Variable["Optional"],
						function: Builtins[:Optional],
						argument: Dhall::Variable["a"]
					)
				)
			),
			"List/last"         => Dhall::Forall.new(
				var:  "a",
				type: Dhall::Variable["Type"],
				type: Builtins[:Type],
				body: Dhall::Forall.of_arguments(
					Dhall::Application.new(
						function: Dhall::Variable["List"],
						function: Builtins[:List],
						argument: Dhall::Variable["a"]
					),
					body: Dhall::Application.new(
						function: Dhall::Variable["Optional"],
						function: Builtins[:Optional],
						argument: Dhall::Variable["a"]
					)
				)
			),
			"List/indexed"      => Dhall::Forall.new(
				var:  "a",
				type: Dhall::Variable["Type"],
				type: Builtins[:Type],
				body: Dhall::Forall.of_arguments(
					Dhall::Application.new(
						function: Dhall::Variable["List"],
						function: Builtins[:List],
						argument: Dhall::Variable["a"]
					),
					body: Dhall::Application.new(
						function: Dhall::Variable["List"],
						function: Builtins[:List],
						argument: Dhall::RecordType.new(
							record: {
								"index" => Dhall::Variable["Natural"],
								"index" => Builtins[:Natural],
								"value" => Dhall::Variable["a"]
							}
						)


@@ 1110,29 1108,29 @@ module Dhall
			),
			"List/reverse"      => Dhall::Forall.new(
				var:  "a",
				type: Dhall::Variable["Type"],
				type: Builtins[:Type],
				body: Dhall::Forall.of_arguments(
					Dhall::Application.new(
						function: Dhall::Variable["List"],
						function: Builtins[:List],
						argument: Dhall::Variable["a"]
					),
					body: Dhall::Application.new(
						function: Dhall::Variable["List"],
						function: Builtins[:List],
						argument: Dhall::Variable["a"]
					)
				)
			),
			"Optional/fold"     => Dhall::Forall.new(
				var:  "a",
				type: Dhall::Variable["Type"],
				type: Builtins[:Type],
				body: Dhall::Forall.of_arguments(
					Dhall::Application.new(
						function: Dhall::Variable["Optional"],
						function: Builtins[:Optional],
						argument: Dhall::Variable["a"]
					),
					body: Dhall::Forall.new(
						var:  "optional",
						type: Dhall::Variable["Type"],
						type: Builtins[:Type],
						body: Dhall::Forall.new(
							var:  "just",
							type: Dhall::Forall.of_arguments(


@@ 1150,11 1148,11 @@ module Dhall
			),
			"Optional/build"    => Dhall::Forall.new(
				var:  "a",
				type: Dhall::Variable["Type"],
				type: Builtins[:Type],
				body: Dhall::Forall.of_arguments(
					Dhall::Forall.new(
						var:  "optional",
						type: Dhall::Variable["Type"],
						type: Builtins[:Type],
						body: Dhall::Forall.new(
							var:  "just",
							type: Dhall::Forall.of_arguments(


@@ 1169,22 1167,22 @@ module Dhall
						)
					),
					body: Dhall::Application.new(
						function: Dhall::Variable["Optional"],
						function: Builtins[:Optional],
						argument: Dhall::Variable["a"]
					)
				)
			),
			"Integer/show"      => Dhall::Forall.of_arguments(
				Dhall::Variable["Integer"],
				body: Dhall::Variable["Text"]
				Builtins[:Integer],
				body: Builtins[:Text]
			),
			"Integer/toDouble"  => Dhall::Forall.of_arguments(
				Dhall::Variable["Integer"],
				body: Dhall::Variable["Double"]
				Builtins[:Integer],
				body: Builtins[:Double]
			),
			"Double/show"       => Dhall::Forall.of_arguments(
				Dhall::Variable["Double"],
				body: Dhall::Variable["Text"]
				Builtins[:Double],
				body: Builtins[:Text]
			)
		}.freeze


M test/test_as_dhall.rb => test/test_as_dhall.rb +10 -10
@@ 93,7 93,7 @@ class TestAsDhall < Minitest::Test
		assert_equal(
			Dhall::List.new(elements: [
				Dhall::Optional.new(value: Dhall::Natural.new(value: 1)),
				Dhall::OptionalNone.new(value_type: Dhall::Variable["Natural"])
				Dhall::OptionalNone.new(value_type: Dhall::Builtins[:Natural])
			]),
			[1, nil].as_dhall
		)


@@ 106,7 106,7 @@ class TestAsDhall < Minitest::Test
				Dhall::Optional.new(value: Dhall::Natural.new(
					value: 10000000000000000000000000000000000
				)),
				Dhall::OptionalNone.new(value_type: Dhall::Variable["Natural"])
				Dhall::OptionalNone.new(value_type: Dhall::Builtins[:Natural])
			]),
			[1, 10000000000000000000000000000000000, nil].as_dhall
		)


@@ 119,18 119,18 @@ class TestAsDhall < Minitest::Test
		           "6ff80f968ba1755d27cdf5eab3"
		union_type = Dhall::UnionType.new(
			alternatives: {
				"Natural" => Dhall::Variable["Natural"],
				"Text"    => Dhall::Variable["Text"],
				"Natural" => Dhall::Builtins[:Natural],
				"Text"    => Dhall::Builtins[:Text],
				"None"    => nil,
				"Bool"    => Dhall::Variable["Bool"],
				"Bool"    => Dhall::Builtins[:Bool],
				hash_key  => Dhall::RecordType.new(
					record: {
						"a" => Dhall::Variable["Natural"]
						"a" => Dhall::Builtins[:Natural]
					}
				),
				array_key => Dhall::Application.new(
					function: Dhall::Variable["List"],
					argument: Dhall::Variable["Natural"]
					function: Dhall::Builtins[:List],
					argument: Dhall::Builtins[:Natural]
				)
			}
		)


@@ 223,8 223,8 @@ class TestAsDhall < Minitest::Test
				value:        Dhall::TypeAnnotation.new(
					type:  Dhall::RecordType.new(
						record: {
							"a" => Dhall::Variable["Natural"],
							"b" => Dhall::Variable["Text"]
							"a" => Dhall::Builtins[:Natural],
							"b" => Dhall::Builtins[:Text]
						}
					),
					value: Dhall::Record.new(

M test/test_as_json.rb => test/test_as_json.rb +0 -1
@@ 16,7 16,6 @@ class TestAsJson < Minitest::Test
		define_method("test_#{test}") do
			skip "double as_json" if test =~ /doubleB/
			skip "deprecated syntax" if test =~ /collectionImportTypeB|annotationsB/
			skip "deprecated syntax" if test =~ /largeExpressionB/
			assert_equal(
				CBOR.decode(path.read),
				Dhall.from_binary(path.read).as_json

M test/test_binary.rb => test/test_binary.rb +1 -1
@@ 24,7 24,7 @@ class TestBinary < Minitest::Test
	def test_self_describing_cbor
		assert_equal(
			Dhall::Variable["x"],
			Dhall.from_binary(Base64.decode64("2dn3YXg"))
			Dhall.from_binary(Base64.decode64("2dn3gmF4AA"))
		)
	end
end

M test/test_readme.rb => test/test_readme.rb +12 -12
@@ 171,9 171,9 @@ class TestReadme < Minitest::Test
		assert_equal(
			Dhall::Optional.new(
				value:      Dhall::Natural.new(value: 2),
				value_type: Dhall::Variable["Natural"]
				value_type: Dhall::Builtins[:Natural]
			),
			SOME.map(type: Dhall::Variable["Natural"]) { |x| x + 1 }
			SOME.map(type: Dhall::Builtins[:Natural]) { |x| x + 1 }
		)
	end



@@ 187,15 187,15 @@ class TestReadme < Minitest::Test

	def test_none_map
		assert_equal(
			Dhall::OptionalNone.new(value_type: Dhall::Variable["Natural"]),
			Dhall::OptionalNone.new(value_type: Dhall::Builtins[:Natural]),
			NONE.map { |x| x + 1 }
		)
	end

	def test_none_map_with_type
		assert_equal(
			Dhall::OptionalNone.new(value_type: Dhall::Variable["Natural"]),
			NONE.map(type: Dhall::Variable["Natural"]) { |x| x + 1 }
			Dhall::OptionalNone.new(value_type: Dhall::Builtins[:Natural]),
			NONE.map(type: Dhall::Builtins[:Natural]) { |x| x + 1 }
		)
	end



@@ 222,8 222,8 @@ class TestReadme < Minitest::Test
			Dhall::List.new(elements: [
				Dhall::Natural.new(value: 2),
				Dhall::Natural.new(value: 3)
			], element_type: Dhall::Variable["Natural"]),
			LIST.map(type: Dhall::Variable["Natural"]) { |x| x + 1 }
			], element_type: Dhall::Builtins[:Natural]),
			LIST.map(type: Dhall::Builtins[:Natural]) { |x| x + 1 }
		)
	end



@@ 238,7 238,7 @@ class TestReadme < Minitest::Test
		assert_equal(
			Dhall::Optional.new(
				value:      Dhall::Natural.new(value: 1),
				value_type: Dhall::Variable["Natural"]
				value_type: Dhall::Builtins[:Natural]
			),
			LIST.first
		)


@@ 248,7 248,7 @@ class TestReadme < Minitest::Test
		assert_equal(
			Dhall::Optional.new(
				value:      Dhall::Natural.new(value: 2),
				value_type: Dhall::Variable["Natural"]
				value_type: Dhall::Builtins[:Natural]
			),
			LIST.last
		)


@@ 258,7 258,7 @@ class TestReadme < Minitest::Test
		assert_equal(
			Dhall::Optional.new(
				value:      Dhall::Natural.new(value: 1),
				value_type: Dhall::Variable["Natural"]
				value_type: Dhall::Builtins[:Natural]
			),
			LIST[0]
		)


@@ 266,7 266,7 @@ class TestReadme < Minitest::Test

	def test_list_index_100
		assert_equal(
			Dhall::OptionalNone.new(value_type: Dhall::Variable["Natural"]),
			Dhall::OptionalNone.new(value_type: Dhall::Builtins[:Natural]),
			LIST[100]
		)
	end


@@ 276,7 276,7 @@ class TestReadme < Minitest::Test
			Dhall::List.new(elements: [
				Dhall::Natural.new(value: 2),
				Dhall::Natural.new(value: 1)
			], element_type: Dhall::Variable["Natural"]),
			], element_type: Dhall::Builtins[:Natural]),
			LIST.reverse
		)
	end