~singpolyma/dhall-ruby

06fb351f4b8016f048e402f086e32b8937442fab — Stephen Paul Weber 1 year, 2 months ago 2d11985
Implement dependent types, assert : A === B
5 files changed, 84 insertions(+), 8 deletions(-)

M dhall-lang
M lib/dhall/ast.rb
M lib/dhall/binary.rb
M lib/dhall/parser.rb
M lib/dhall/typecheck.rb
M dhall-lang => dhall-lang +1 -1
@@ 1,1 1,1 @@
Subproject commit 9f259cd68870b912fbf2f2a08cd63dc3ccba9dc3
Subproject commit 1ed98c33ce5078161109885f0b16b3828958f4e2

M lib/dhall/ast.rb => lib/dhall/ast.rb +17 -1
@@ 104,6 104,10 @@ module Dhall
			end
		end

		def annotate(type)
			TypeAnnotation.new(value: self, type: type)
		end

		def to_s
			inspect
		end


@@ 394,13 398,15 @@ module Dhall
		end
		class RecursiveRecordTypeMerge < Operator; end
		class ImportFallback < Operator; end
		class Equivalent < Operator; end

		OPERATORS = [
			Or, And, Equal, NotEqual,
			Plus, Times,
			TextConcatenate, ListConcatenate,
			RecursiveRecordMerge, RightBiasedRecordMerge, RecursiveRecordTypeMerge,
			ImportFallback
			ImportFallback,
			Equivalent
		].freeze
	end



@@ 1842,4 1848,14 @@ module Dhall
			[26, value.as_json, type.as_json]
		end
	end

	class Assertion < Expression
		include(ValueSemantics.for_attributes do
			type Expression
		end)

		def as_json
			[19, type.as_json]
		end
	end
end

M lib/dhall/binary.rb => lib/dhall/binary.rb +7 -1
@@ 213,6 213,12 @@ module Dhall
		end
	end

	class Assertion
		def self.decode(type)
			new(type: Dhall.decode(type))
		end
	end

	class Import
		class IntegrityCheck
			def self.decode(integrity_check)


@@ 335,7 341,7 @@ module Dhall
		Integer,
		nil,
		TextLiteral,
		nil,
		Assertion,
		nil,
		nil,
		nil,

M lib/dhall/parser.rb => lib/dhall/parser.rb +7 -2
@@ 24,7 24,7 @@ module Dhall
				return list if string =~ /\A\[\s*\]/

				key =
					[:let_binding, :lambda, :forall, :arrow, :if, :merge, :tomap]
					[:let_binding, :lambda, :forall, :arrow, :if, :merge, :tomap, :assert]
					.find { |k| captures.key?(k) }

				key ? public_send(key) : super


@@ 87,6 87,10 @@ module Dhall
					type:   capture(:application_expression).value
				)
			end

			def assert
				Assertion.new(type: capture(:expression).value)
			end
		end

		OPERATORS = {


@@ 101,7 105,8 @@ module Dhall
			combine_types_expression: :RecursiveRecordTypeMerge,
			times_expression:         :Times,
			equal_expression:         :Equal,
			not_equal_expression:     :NotEqual
			not_equal_expression:     :NotEqual,
			equivalent_expression:    :Equivalent
		}.freeze

		OPERATORS.to_a.zip(

M lib/dhall/typecheck.rb => lib/dhall/typecheck.rb +52 -3
@@ 20,7 20,9 @@ module Dhall
		def self.assert_types_match(a, b, message, context:)
			atype = self.for(a).annotate(context).type
			btype = self.for(b).annotate(context).type
			raise TypeError, "#{message}: #{atype}, #{btype}" unless atype == btype
			unless atype.normalize == btype.normalize
				raise TypeError, "#{message}: #{atype}, #{btype}"
			end
			atype
		end



@@ 237,6 239,31 @@ module Dhall
			end
		end

		class OperatorEquivalent
			TypeChecker.register self, Dhall::Operator::Equivalent

			def initialize(expr)
				@expr = expr
				@lhs = expr.lhs
				@rhs = expr.rhs
			end

			def annotate(context)
				type = TypeChecker.assert_types_match @lhs, @rhs,
				                                      "arguments do not match",
				                                      context: context

				TypeChecker.assert_type type, Builtins[:Type],
				                        "arguments are not terms",
				                        context: context

				Dhall::TypeAnnotation.new(
					value: @expr.with(lhs: @lhs.annotate(type), rhs: @rhs.annotate(type)),
					type:  Builtins[:Type]
				)
			end
		end

		class OperatorListConcatenate
			TypeChecker.register self, Dhall::Operator::ListConcatenate



@@ 842,8 869,6 @@ module Dhall
						raise TypeError, "FunctionType part of this is a term"
					end

					raise TypeError, "Dependent types are not allowed" if outkind > inkind

					if outkind.zero?
						Term.new
					else


@@ 996,6 1021,30 @@ module Dhall
			end
		end

		class Assertion
			TypeChecker.register self, Dhall::Assertion

			def initialize(expr)
				@expr = expr
				@type = expr.type
			end

			def annotate(context)
				TypeChecker.assert @type, Dhall::Operator::Equivalent,
				                   "assert expected === got: #{@type.class}"

				TypeChecker.assert_type @type, Builtins[:Type],
				                        "=== expected to have type Type",
				                        context: context

				TypeChecker.assert @type.lhs.normalize.to_binary,
				                   @type.rhs.normalize.to_binary,
				                   "assert equivalence not equivalent"

				@expr
			end
		end

		BUILTIN_TYPES = {
			"Bool"              => Builtins[:Type],
			"Type"              => Builtins[:Kind],