~singpolyma/dhall-ruby

bce3b47ae39e39981dee4380c421e48ff3718bba — Stephen Paul Weber 3 years ago f31b87c
Beta normalization complete
M lib/dhall/ast.rb => lib/dhall/ast.rb +16 -0
@@ 129,6 129,14 @@ module Dhall
		def map_subexpressions(&block)
			with(var: var, type: type.nil? ? nil : block[type], body: block[body])
		end

		def call(*args)
			return super if args.length > 1
			body.substitute(
				Variable.new(name: var),
				args.first.shift(1, var, 0)
			).shift(-1, var, 0).normalize
		end
	end

	class Forall < Function; end


@@ 279,6 287,10 @@ module Dhall
		def map_subexpressions(&block)
			with(value: block[value], type: type.nil? ? type : block[type])
		end

		def reduce(_, &block)
			block[value]
		end
	end

	class OptionalNone < Optional


@@ 289,6 301,10 @@ module Dhall
		def map_subexpressions(&block)
			with(type: block[@type])
		end

		def reduce(z)
			z
		end
	end

	class Merge < Expression

M lib/dhall/builtins.rb => lib/dhall/builtins.rb +84 -0
@@ 154,6 154,10 @@ module Dhall
		end

		class List_build < Builtin
			def initialize(type=nil)
				@type = type
			end

			def fusion(*args)
				_, arg, = args
				if arg.is_a?(Application) &&


@@ 165,6 169,37 @@ module Dhall
					super
				end
			end

			def call(arg)
				if @type.nil?
					self.class.new(arg)
				else
					arg.call(
						Application.new(
							function: Variable.new(name: "List"),
							arguments: [@type]
						),
						Function.new(
							var: "_",
							type: @type,
							body: Function.new(
								var:  "_",
								type: Application.new(
									function: Variable.new(name: "List"),
									arguments: [@type.shift(1, "_", 0)]
								),
								body: Operator::ListConcatenate.new(
									lhs: List.new(
										elements: [Variable.new(name: "_", index: 1)]
									),
									rhs: Variable.new(name: "_")
								)
							),
						),
						EmptyList.new(type: @type)
					)
				end
			end
		end

		class List_fold < Builtin


@@ 249,6 284,10 @@ module Dhall
		end

		class Optional_build < Builtin
			def initialize(type=nil)
				@type = type
			end

			def fusion(*args)
				_, arg, = args
				if arg.is_a?(Application) &&


@@ 260,9 299,54 @@ module Dhall
					super
				end
			end

			def call(arg)
				if @type.nil?
					self.class.new(arg)
				else
					arg.call(
						Application.new(
							function: Variable.new(name: "Optional"),
							arguments: [@type]
						),
						Function.new(
							var: "_",
							type: @type,
							body: Optional.new(
								value: Variable.new(name: "_"),
								type: @type
							)
						),
						OptionalNone.new(type: @type)
					)
				end
			end

		end

		class Optional_fold < Builtin
			def initialize(type=nil, optional=nil, ztype=nil, f=nil)
				@type = type
				@optional = optional
				@ztype = ztype
				@f = f
			end

			def call(arg)
				if @type.nil?
					self.class.new(arg)
				elsif arg.is_a?(Optional)
					self.class.new(@type, arg)
				elsif !@optional.nil? && @ztype.nil?
					self.class.new(@type, @optional, arg)
				elsif !@optional.nil? && @f.nil?
					self.class.new(@type, @optional, @ztype, arg)
				elsif !@optional.nil?
					@optional.reduce(arg, &@f)
				else
					super
				end
			end
		end

		class Text_show < Builtin

M lib/dhall/normalize.rb => lib/dhall/normalize.rb +20 -2
@@ 12,6 12,10 @@ module Dhall
			map_subexpressions { |expr| expr.shift(amount, name, min_index) }
		end

		def substitute(var, with_expr)
			map_subexpressions { |expr| expr.substitute(var, with_expr) }
		end

		def fusion(*); end
	end



@@ 21,7 25,8 @@ module Dhall
			normalized = super
			return normalized.fuse if normalized.fuse

			if normalized.function.is_a?(Builtin)
			if normalized.function.is_a?(Builtin) ||
			   normalized.function.is_a?(Function)
				return normalized.function.call(*normalized.arguments)
			end



@@ 46,6 51,15 @@ module Dhall
				body: body.shift(amount, name, min_index + 1)
			)
		end

		def substitute(svar, with_expr)
			with_expr = with_expr.shift(1, var, 0)
			if var == svar.name
				super(svar.with(index: svar.index + 1), with_expr)
			else
				super(svar, with_expr)
			end
		end
	end

	class Forall; end


@@ 58,6 72,10 @@ module Dhall
			return self if self.name != name || min_index > index
			with(index: index + amount)
		end

		def substitute(var, with_expr)
			self == var ? with_expr : self
		end
	end

	class Operator


@@ 293,7 311,7 @@ module Dhall
		end

		def desugar
			lets.reduce(body) { |inside, let|
			lets.reverse.reduce(body) { |inside, let|
				Application.new(
					function: Function.new(
						var: let.var,

A test/normalization/beta/FunctionApplicationCaptureA.dhallb => test/normalization/beta/FunctionApplicationCaptureA.dhallb +0 -0
A test/normalization/beta/FunctionApplicationCaptureB.dhallb => test/normalization/beta/FunctionApplicationCaptureB.dhallb +1 -0
@@ 0,0 1,1 @@
�e5.0.0ax
\ No newline at end of file

A test/normalization/beta/FunctionApplicationNoSubstituteA.dhallb => test/normalization/beta/FunctionApplicationNoSubstituteA.dhallb +0 -0
A test/normalization/beta/FunctionApplicationNoSubstituteB.dhallb => test/normalization/beta/FunctionApplicationNoSubstituteB.dhallb +1 -0
@@ 0,0 1,1 @@
�e5.0.0ay
\ No newline at end of file

A test/normalization/beta/FunctionApplicationNormalizeArgumentsA.dhallb => test/normalization/beta/FunctionApplicationNormalizeArgumentsA.dhallb +0 -0
A test/normalization/beta/FunctionApplicationNormalizeArgumentsB.dhallb => test/normalization/beta/FunctionApplicationNormalizeArgumentsB.dhallb +0 -0
A test/normalization/beta/FunctionApplicationSubstituteA.dhallb => test/normalization/beta/FunctionApplicationSubstituteA.dhallb +0 -0
A test/normalization/beta/FunctionApplicationSubstituteB.dhallb => test/normalization/beta/FunctionApplicationSubstituteB.dhallb +1 -0
@@ 0,0 1,1 @@
�e5.0.0ay
\ No newline at end of file

A test/normalization/beta/FunctionNormalizeArgumentsA.dhallb => test/normalization/beta/FunctionNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
�e5.0.0�ax��aXaY��axay
\ No newline at end of file

A test/normalization/beta/FunctionNormalizeArgumentsB.dhallb => test/normalization/beta/FunctionNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
�e5.0.0�axaXax
\ No newline at end of file

A test/normalization/beta/FunctionTypeNormalizeArgumentsA.dhallb => test/normalization/beta/FunctionTypeNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
�e5.0.0�ax��aXaY��aAaB
\ No newline at end of file

A test/normalization/beta/FunctionTypeNormalizeArgumentsB.dhallb => test/normalization/beta/FunctionTypeNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
�e5.0.0�axaXaA
\ No newline at end of file

M test/test_normalization.rb => test/test_normalization.rb +30 -0
@@ 78,4 78,34 @@ class TestParser < Minitest::Test
			).shift(1, "x", 0)
		)
	end

	def test_substitute_variable
		assert_equal(
			Dhall::Natural.new(value: 1),
			Dhall::Variable.new(name: "x", index: 0).substitute(
				Dhall::Variable.new(name: "x", index: 0),
				Dhall::Natural.new(value: 1)
			)
		)
	end

	def test_substitute_variable_different_name
		assert_equal(
			Dhall::Variable.new(name: "y", index: 0),
			Dhall::Variable.new(name: "y", index: 0).substitute(
				Dhall::Variable.new(name: "x", index: 0),
				Dhall::Natural.new(value: 1)
			)
		)
	end

	def test_substitute_variable_different_index
		assert_equal(
			Dhall::Variable.new(name: "x", index: 1),
			Dhall::Variable.new(name: "x", index: 1).substitute(
				Dhall::Variable.new(name: "x", index: 0),
				Dhall::Natural.new(value: 1)
			)
		)
	end
end