Class: Dhall::TypeChecker::RecordProjection

Inherits:
Object
  • Object
show all
Defined in:
lib/dhall/typecheck.rb

Instance Method Summary collapse

Constructor Details

#initialize(projection) ⇒ RecordProjection

Returns a new instance of RecordProjection.



635
636
637
638
639
 
# File 'lib/dhall/typecheck.rb', line 635

def initialize(projection)
	@projection = projection
	@record = TypeChecker.for(projection.record)
	@selectors = projection.selectors
end

Instance Method Details

#annotate(context) ⇒ Object 



641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
 
# File 'lib/dhall/typecheck.rb', line 641

def annotate(context)
	arecord = @record.annotate(context)

	TypeChecker.assert arecord.type.class.name, "Dhall::RecordType",
	                   "RecordProjection on #{arecord.type}"

	slice = arecord.type.slice(@selectors)
	TypeChecker.assert slice.keys, @selectors,
	                   "#{arecord.type} missing one of: #{@selectors}"

	Dhall::TypeAnnotation.new(
		value: @projection.with(record: arecord),
		type:  slice
	)
end