~singpolyma/dhall-ruby

afdc55804efc61ff7865651424c00060964d6830 — Stephen Paul Weber 3 years ago db074ab
Alpha normalization

Internal flag to disable for acceptance tests from the standard (which
assume beta-only normalization in some cases).  Otherwise, just always
alpha normalize as we go.
M .rubocop.yml => .rubocop.yml +3 -0
@@ 35,6 35,9 @@ Style/BlockDelimiters:
Style/MultilineBlockChain:
  Enabled: false

Style/ClassVars:
  Enabled: false

Style/Documentation:
  Enabled: false


M lib/dhall/normalize.rb => lib/dhall/normalize.rb +28 -1
@@ 45,6 45,14 @@ module Dhall
	end

	class Function
		def self.disable_alpha_normalization!
			@@alpha_normalization = false
		end

		def self.enable_alpha_normalization!
			@@alpha_normalization = true
		end

		def shift(amount, name, min_index)
			return super unless var == name



@@ 56,13 64,32 @@ module Dhall

		def substitute(svar, with_expr)
			with(
				type: type.substitute(svar, with_expr),
				type: type&.substitute(svar, with_expr),
				body: body.substitute(
					var == svar.name ? svar.with(index: svar.index + 1) : svar,
					with_expr.shift(1, var, 0)
				)
			)
		end

		def normalize
			return super unless alpha_normalize?
			with(
				var:  "_",
				type: type&.normalize,
				body: body
				      .shift(1, "_", 0)
				      .substitute(Variable[var], Variable["_"])
				      .shift(-1, var, 0)
				      .normalize
			)
		end

		protected

		def alpha_normalize?
			var != "_" && @@alpha_normalization
		end
	end

	class Forall; end

A test/normalization/alpha/FunctionBindingUnderscoreA.dhallb => test/normalization/alpha/FunctionBindingUnderscoreA.dhallb +1 -0
@@ 0,0 1,1 @@
�aAab
\ No newline at end of file

A test/normalization/alpha/FunctionBindingUnderscoreB.dhallb => test/normalization/alpha/FunctionBindingUnderscoreB.dhallb +1 -0
@@ 0,0 1,1 @@
�aAab
\ No newline at end of file

A test/normalization/alpha/FunctionBindingXA.dhallb => test/normalization/alpha/FunctionBindingXA.dhallb +1 -0
@@ 0,0 1,1 @@
�axaAax
\ No newline at end of file

A test/normalization/alpha/FunctionBindingXB.dhallb => test/normalization/alpha/FunctionBindingXB.dhallb +0 -0
A test/normalization/alpha/FunctionNestedBindingXA.dhallb => test/normalization/alpha/FunctionNestedBindingXA.dhallb +1 -0
@@ 0,0 1,1 @@
�axaA�aBax
\ No newline at end of file

A test/normalization/alpha/FunctionNestedBindingXB.dhallb => test/normalization/alpha/FunctionNestedBindingXB.dhallb +1 -0
@@ 0,0 1,1 @@
�aA�aB
\ No newline at end of file

A test/normalization/alpha/FunctionTypeBindingUnderscoreA.dhallb => test/normalization/alpha/FunctionTypeBindingUnderscoreA.dhallb +1 -0
@@ 0,0 1,1 @@
�aAaB
\ No newline at end of file

A test/normalization/alpha/FunctionTypeBindingUnderscoreB.dhallb => test/normalization/alpha/FunctionTypeBindingUnderscoreB.dhallb +1 -0
@@ 0,0 1,1 @@
�aAaB
\ No newline at end of file

A test/normalization/alpha/FunctionTypeBindingXA.dhallb => test/normalization/alpha/FunctionTypeBindingXA.dhallb +1 -0
@@ 0,0 1,1 @@
�axaAax
\ No newline at end of file

A test/normalization/alpha/FunctionTypeBindingXB.dhallb => test/normalization/alpha/FunctionTypeBindingXB.dhallb +0 -0
A test/normalization/alpha/FunctionTypeNestedBindingXA.dhallb => test/normalization/alpha/FunctionTypeNestedBindingXA.dhallb +1 -0
@@ 0,0 1,1 @@
�axaA�aBax
\ No newline at end of file

A test/normalization/alpha/FunctionTypeNestedBindingXB.dhallb => test/normalization/alpha/FunctionTypeNestedBindingXB.dhallb +1 -0
@@ 0,0 1,1 @@
�aA�aB
\ No newline at end of file

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

M test/normalization/beta/FunctionTypeNormalizeArgumentsB.dhallb => test/normalization/beta/FunctionTypeNormalizeArgumentsB.dhallb +1 -1
@@ 1,1 1,1 @@
�axaXaA
\ No newline at end of file
�aXaA
\ No newline at end of file

M test/test_normalization.rb => test/test_normalization.rb +6 -15
@@ 8,33 8,24 @@ require "dhall/binary"
require "dhall/normalize"

DIRPATH = Pathname.new(File.dirname(__FILE__))
UNIT = DIRPATH + "normalization/beta/"
STANDARD = DIRPATH + "normalization/standard/"
TESTS = DIRPATH + "normalization/"

# Tests are not the place for abstractions, but for concretions
# rubocop:disable Metrics/MethodLength
class TestNormalization < Minitest::Test
	Pathname.glob(UNIT + "*A.dhallb").each do |path|
		test = path.basename("A.dhallb").to_s
		define_method("test_#{test}") do
			assert_equal(
				Dhall.from_binary(UNIT + "#{test}B.dhallb"),
				Dhall.from_binary(path.read).normalize
			)
		end
	end

	Pathname.glob(STANDARD + "**/*A.dhallb").each do |path|
		test = path.relative_path_from(STANDARD).to_s.sub(/A\.dhallb$/, "")
	Pathname.glob(TESTS + "**/*A.dhallb").each do |path|
		test = path.relative_path_from(TESTS).to_s.sub(/A\.dhallb$/, "")
		next if test =~ /prelude\//
		next if test =~ /remoteSystems/
		next if test =~ /multiline\//

		define_method("test_#{test.gsub(/\//, "_")}") do
			Dhall::Function.disable_alpha_normalization! if test =~ /^standard\//
			assert_equal(
				Dhall.from_binary(STANDARD + "#{test}B.dhallb"),
				Dhall.from_binary(TESTS + "#{test}B.dhallb"),
				Dhall.from_binary(path.read).normalize
			)
			Dhall::Function.enable_alpha_normalization! if test =~ /^standard\//
		end
	end