From b63afc13fbad1d17124ecbe299015d459d53f6f5 Mon Sep 17 00:00:00 2001 From: Stephen Paul Weber Date: Sun, 31 Mar 2019 19:29:13 -0500 Subject: [PATCH] Refactor LetBlock, allow single LetIn --- lib/dhall/ast.rb | 48 ++++++++++++++++++++++++------------------ lib/dhall/normalize.rb | 17 +++++++++++---- lib/dhall/typecheck.rb | 28 ++++++++++++------------ 3 files changed, 56 insertions(+), 37 deletions(-) diff --git a/lib/dhall/ast.rb b/lib/dhall/ast.rb index 05686ac..8a8f7ea 100644 --- a/lib/dhall/ast.rb +++ b/lib/dhall/ast.rb @@ -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 diff --git a/lib/dhall/normalize.rb b/lib/dhall/normalize.rb index 4c74655..e033bb9 100644 --- a/lib/dhall/normalize.rb +++ b/lib/dhall/normalize.rb @@ -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 diff --git a/lib/dhall/typecheck.rb b/lib/dhall/typecheck.rb index dda7a26..36f6ad6 100644 --- a/lib/dhall/typecheck.rb +++ b/lib/dhall/typecheck.rb @@ -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) -- 2.34.5