class TypedRb::Types::Polymorphism::Unification
Implements a unification algorithm for variable types with support for subtyping and restrictions on variable types.
Attributes
constraints[R]
graph[R]
Public Class Methods
new(constraints, options = {})
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 352 def initialize(constraints, options = {}) @allow_unbound_receivers = options[:allow_unbound_receivers] || false @constraints = canonical_form(constraints) @constraints = expand_constraints @gt_constraints = @constraints.select { |(_, t, _r)| t == :gt }.sort do |(_, _, r1), (_, _, r2)| -(r1 <=> r2) || 0 rescue 0 end @lt_constraints = @constraints.select { |(_, t, _r)| t == :lt }.sort do |(_, _, r1), (_, _, r2)| (r1 <=> r2) || 0 rescue 0 end @send_constraints = @constraints.select { |(_, t, _r)| t == :send } @graph = Topography.new(@constraints) @to_bubble = [] end
Public Instance Methods
bindings()
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 432 def bindings graph.vars end
bindings_map()
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 436 def bindings_map graph.vars.each_with_object({}) do |var, acc| acc[var.variable] = var if var.bound end end
bubble_send_constraints()
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 420 def bubble_send_constraints @to_bubble.each do |(var, constraint)| return_var = constraint[:return] message = constraint[:message] args = constraint[:args] lower_type = @graph[return_var][:lower_type] upper_type = @graph[return_var][:upper_type] fresh_return_var = var.add_message_constraint(message, args) Types::TypingContext.add_constraint(fresh_return_var.variable, :lt, lower_type) if lower_type Types::TypingContext.add_constraint(fresh_return_var.variable, :gt, upper_type) if upper_type end end
canonical_form(constraints)
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 383 def canonical_form(constraints) disambiguation = {} constraints.inject([]) do |acc, (l, t, r)| next acc if r.nil? || (r.respond_to?(:ruby_type) && r.ruby_type == NilClass) || r.is_a?(Types::TyDynamic) if l.is_a?(TypeVariable) l = disambiguation[l.variable] || l disambiguation[l.variable] = l end if r.is_a?(TypeVariable) r = disambiguation[r.variable] || r disambiguation[r.variable] = r end if l.is_a?(TypeVariable) && r.is_a?(TypeVariable) && t == :lt acc << [r, :gt, l] else acc << [l, t, r] end end end
expand_constraint(element)
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 374 def expand_constraint(element) expanded = [] if element.is_a?(TypeVariable) && element.bound.nil? expanded << [element, :gt, element.lower_bound] if element.lower_bound expanded << [element, :lt, element.upper_bound] if element.upper_bound end expanded end
expand_constraints()
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 367 def expand_constraints expanded = constraints.reduce([]) do |acc, (l,_,r)| acc + expand_constraint(l) + expand_constraint(r) end expanded + @constraints end
print_constraints()
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 442 def print_constraints text = StringIO.new text << "Running unification on #{constraints.size} constraints:\n" @gt_constraints.each do |(l, _t, r)| l = if l.is_a?(Hash) l.keys.map(&:to_s).join(',') else l.to_s end text << "#{l} :gt #{r}\n" end @lt_constraints.each do |(l, _t, r)| l = if l.is_a?(Hash) l.keys.map(&:to_s).join(',') else l.to_s end text << "#{l} :lt #{r}\n" end @send_constraints.each do |(l, _t, send)| return_type = send[:return] arg_types = send[:args].map(&:to_s) message = send[:message] l = if l.is_a?(Hash) l.keys.map(&:to_s).join(',') else l.to_s end text << "#{l} :send #{message}[ #{arg_types.join(',')} -> #{return_type}]\n" end TypedRb.log binding, :debug, text.string end
run(bind_variables = true)
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 404 def run(bind_variables = true) print_constraints unify(@gt_constraints) # we create links between vars in unify, we need to fold groups afterwards # this just references to vars in the same group, by the group itself # in the remaining @lt constraints @lt_constraints = graph.replace_groups(@lt_constraints) unify(@lt_constraints) graph.check_bindings unify(@send_constraints) graph.check_bindings graph.print_groups bubble_send_constraints graph.do_bindings! if bind_variables self end
Protected Instance Methods
check_constraint(l, t, r, bind = true)
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 498 def check_constraint(l, t, r, bind = true) # ONE BOUND value_l = if t == :lt graph[l][:lower_type] elsif t == :gt graph[l][:upper_type] else graph[l] end # value_r = r value_r = if r.is_a?(Hash) && t != :send if t == :lt graph[r][:lower_type] elsif t == :gt graph[r][:upper_type] else graph[r] end else r end # this will throw an exception if types no compatible compatible_type = compatible_type?(value_l, t, value_r) if t == :lt graph[l][:lower_type] = compatible_type if bind elsif t == :gt graph[l][:upper_type] = compatible_type if bind end # # OTHER BOUND # # value_l = if t == :lt # graph[l][:upper_type] # elsif t == :gt # graph[l][:lower_type] # else # graph[l] # end # #value_r = r # value_r = if r.is_a?(Hash) # if t == :lt # graph[r][:upper_type] # elsif t == :gt # graph[r][:lower_type] # else # graph[r] # end # else # r # end # # # this will throw an exception if types no compatible # compatible_type = compatible_type?(value_l, (t == :gt ? :lt : :gt), value_r) # if t == :lt # graph[l][:upper_type] = compatible_type if bind # elsif t == :gt # graph[l][:lower_type] = compatible_type if bind # end end
unify(constraints)
click to toggle source
# File lib/typed/types/polymorphism/unification.rb, line 477 def unify(constraints) return if constraints.empty? (l, t, r) = constraints.first rest = constraints.drop(1) if l == r unify(rest) else if r.is_a?(TypeVariable) # this is only going to happen in the first invocation to unify graph.merge(l, r) else # - In the first invocation to unify, l must always be a TypeVar # t :gt and r a type variable or a type, # - In the second invocation to unify, l must always be a group # t :lt and r a type variable, check_constraint(l, t, r, t != :send) # we don't bind if constraint is send end unify(rest) end end