Class: Dhall::TypeChecker::Context

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

Instance Method Summary collapse

Constructor Details

#initialize(bindings = Hash.new([])) ⇒ Context

Returns a new instance of Context.



55
56
57
58
 
# File 'lib/dhall/typecheck.rb', line 55

def initialize(bindings=Hash.new([]))
	@bindings = bindings.freeze
	freeze
end

Instance Method Details

#add(ftype) ⇒ Object 



65
66
67
68
69
 
# File 'lib/dhall/typecheck.rb', line 65

def add(ftype)
	self.class.new(@bindings.merge(
		ftype.var => [ftype.type] + @bindings[ftype.var]
	)).shift(1, ftype.var, 0)
end

#fetch(var) ⇒ Object 



60
61
62
63
 
# File 'lib/dhall/typecheck.rb', line 60

def fetch(var)
	@bindings[var.name][var.index] ||
		(raise TypeError, "Free variable: #{var}")
end

#shift(amount, name, min_index) ⇒ Object 



71
72
73
74
75
76
77
 
# File 'lib/dhall/typecheck.rb', line 71

def shift(amount, name, min_index)
	self.class.new(@bindings.merge(
		Hash[@bindings.map do |var, bindings|
			[var, bindings.map { |b| b.shift(amount, name, min_index) }]
		end]
	))
end