~singpolyma/dhall-ruby

b63afc13fbad1d17124ecbe299015d459d53f6f5 — Stephen Paul Weber 3 years ago bb41559
Refactor LetBlock, allow single LetIn
3 files changed, 56 insertions(+), 37 deletions(-)

M lib/dhall/ast.rb
M lib/dhall/normalize.rb
M lib/dhall/typecheck.rb
M lib/dhall/ast.rb => lib/dhall/ast.rb +28 -20
@@ 1089,6 1089,31 @@ module Dhall
		end
	end

	class LetIn < Expression
		include(ValueSemantics.for_attributes do
			let  Let
			body Expression
		end)

		def desugar
			Application.new(
				function: Function.new(
					var:  let.var,
					type: let.type,
					body: body
				),
				argument: let.assign
			)
		end

		def eliminate
			body.substitute(
				Dhall::Variable[let.var],
				let.assign.shift(1, let.var, 0)
			).shift(-1, let.var, 0)
		end
	end

	class LetBlock < Expression
		include(ValueSemantics.for_attributes do
			lets ArrayOf(Let)


@@ 1097,30 1122,13 @@ module Dhall

		def unflatten
			lets.reverse.reduce(body) do |inside, let|
				LetBlock.new(lets: [let], body: inside)
				letin = LetIn.new(let: let, body: inside)
				block_given? ? (yield letin) : letin
			end
		end

		def desugar
			lets.reverse.reduce(body) do |inside, let|
				Application.new(
					function: Function.new(
						var:  let.var,
						type: let.type,
						body: inside
					),
					argument: let.assign
				)
			end
		end

		def eliminate
			return unflatten.eliminate if lets.length > 1

			body.substitute(
				Dhall::Variable[lets.first.var],
				lets.first.assign.shift(1, lets.first.var, 0)
			).shift(-1, lets.first.var, 0)
			unflatten(&:desugar)
		end

		def as_json

M lib/dhall/normalize.rb => lib/dhall/normalize.rb +13 -4
@@ 354,22 354,31 @@ module Dhall
	class Import
	end

	class LetBlock
	class LetIn
		def normalize
			desugar.normalize
		end

		def shift(amount, name, min_index)
			return unflatten.shift(amount, name, min_index) if lets.length > 1
			return super unless lets.first.var == name
			return super unless let.var == name

			with(
				lets: [let.first.shift(amount, name, min_index)],
				let:  let.shift(amount, name, min_index),
				body: body.shift(amount, name, min_index + 1)
			)
		end
	end

	class LetBlock
		def normalize
			desugar.normalize
		end

		def shift(amount, name, min_index)
			unflatten.shift(amount, name, min_index)
		end
	end

	class TypeAnnotation
		def normalize
			value.normalize

M lib/dhall/typecheck.rb => lib/dhall/typecheck.rb +15 -13
@@ 859,28 859,30 @@ module Dhall
			end
		end

		class LetBlock
			TypeChecker.register self, Dhall::LetBlock
		TypeChecker.register ->(blk) { LetIn.for(blk.unflatten) }, Dhall::LetBlock

			def self.for(letblock)
				if letblock.lets.first.type
					LetBlockAnnotated.new(letblock)
		class LetIn
			TypeChecker.register self, Dhall::LetIn

			def self.for(letin)
				if letin.let.type
					LetInAnnotated.new(letin)
				else
					LetBlock.new(letblock)
					LetIn.new(letin)
				end
			end

			def initialize(letblock)
				@letblock = letblock.unflatten
				@let = @letblock.lets.first
			def initialize(letin)
				@letin = letin
				@let = @letin.let
			end

			def annotate(context)
				alet = @let.with(type: assign_type(context))
				type = TypeChecker.for(@letblock.eliminate).annotate(context).type
				abody = Dhall::TypeAnnotation.new(value: @letblock.body, type: type)
				type = TypeChecker.for(@letin.eliminate).annotate(context).type
				abody = Dhall::TypeAnnotation.new(value: @letin.body, type: type)
				Dhall::TypeAnnotation.new(
					value: @letblock.with(lets: [alet], body: abody),
					value: @letin.with(let: alet, body: abody),
					type:  type
				)
			end


@@ 892,7 894,7 @@ module Dhall
			end
		end

		class LetBlockAnnotated < LetBlock
		class LetInAnnotated < LetIn
			protected

			def assign_type(context)