From d58516b09fcc8540593c723f9c99339216940966 Mon Sep 17 00:00:00 2001 From: Stephen Paul Weber Date: Wed, 10 Jul 2019 19:22:33 -0500 Subject: [PATCH] Record projection by expression / type --- lib/dhall/ast.rb | 11 +++++++++++ lib/dhall/binary.rb | 10 +++++++++- lib/dhall/normalize.rb | 12 ++++++++++++ lib/dhall/parser.rb | 2 ++ lib/dhall/typecheck.rb | 28 ++++++++++++++++++++++++++++ 5 files changed, 62 insertions(+), 1 deletion(-) diff --git a/lib/dhall/ast.rb b/lib/dhall/ast.rb index f42690d..0d934e8 100644 --- a/lib/dhall/ast.rb +++ b/lib/dhall/ast.rb @@ -810,6 +810,17 @@ module Dhall end end + class RecordProjectionByExpression < Expression + include(ValueSemantics.for_attributes do + record Expression + selector Expression + end) + + def as_json + [10, record.as_json, [selector.as_json]] + end + end + class EmptyRecordProjection < Expression include(ValueSemantics.for_attributes do record Expression diff --git a/lib/dhall/binary.rb b/lib/dhall/binary.rb index 2946d35..0c62aab 100644 --- a/lib/dhall/binary.rb +++ b/lib/dhall/binary.rb @@ -144,7 +144,15 @@ module Dhall class RecordProjection def self.decode(record, *selectors) - self.for(Dhall.decode(record), selectors) + record = Dhall.decode(record) + if selectors.length == 1 && selectors[0].is_a?(Array) + RecordProjectionByExpression.new( + record: record, + selector: Dhall.decode(selectors[0][0]) + ) + else + self.for(record, selectors) + end end end diff --git a/lib/dhall/normalize.rb b/lib/dhall/normalize.rb index d04a64e..7ac48e9 100644 --- a/lib/dhall/normalize.rb +++ b/lib/dhall/normalize.rb @@ -320,6 +320,18 @@ module Dhall end end + class RecordProjectionByExpression + def normalize + sel = selector.normalize + + if sel.is_a?(RecordType) + RecordProjection.for(record, sel.keys).normalize + else + with(record: record.normalize, selector: sel) + end + end + end + class EmptyRecordProjection def normalize EmptyRecord.new diff --git a/lib/dhall/parser.rb b/lib/dhall/parser.rb index 6edf1dc..3013392 100644 --- a/lib/dhall/parser.rb +++ b/lib/dhall/parser.rb @@ -146,6 +146,8 @@ module Dhall selectors.reduce(record) do |rec, sels| if sels.is_a?(Array) RecordProjection.for(rec, sels) + elsif sels.is_a?(Dhall::Expression) + RecordProjectionByExpression.new(record: rec, selector: sels) else RecordSelection.new(record: rec, selector: sels) end diff --git a/lib/dhall/typecheck.rb b/lib/dhall/typecheck.rb index ed212b1..21be8be 100644 --- a/lib/dhall/typecheck.rb +++ b/lib/dhall/typecheck.rb @@ -604,6 +604,34 @@ module Dhall end end + class RecordProjectionByExpression + TypeChecker.register self, Dhall::RecordProjectionByExpression + + def initialize(projection) + @selector = projection.selector.normalize + @projection = projection + end + + def annotate(context) + TypeChecker.assert @selector, Dhall::RecordType, + "RecordProjectionByExpression on #{@selector.class}" + + projection = Dhall::RecordProjection.for( + @projection.record, + @selector.keys + ) + + TypeChecker.assert_type projection, @selector.normalize, + "Type doesn't match #{@selector}", + context: context + + Dhall::TypeAnnotation.new( + value: @projection, + type: @selector + ) + end + end + class Enum TypeChecker.register self, Dhall::Enum -- 2.34.5