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
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