Class: Steep::Subtyping::Constraints

Inherits:
Object
  • Object
show all
Defined in:
lib/steep/subtyping/constraints.rb

Defined Under Namespace

Classes: UnsatisfiableConstraint, UnsatisfiedInvariantError

Constant Summary collapse

Context = 
_ = Struct.new(:variance, :self_type, :instance_type, :class_type, keyword_init: true)

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(unknowns:) ⇒ Constraints

Returns a new instance of Constraints.



78
79
80
81
82
83
84
85
 
# File 'lib/steep/subtyping/constraints.rb', line 78

def initialize(unknowns:)
  @dictionary = {}
  @vars = Set.new

  unknowns.each do |var|
    dictionary[var] = [Set.new, Set.new, Set.new]
  end
end

Instance Attribute Details

#dictionary ⇒ Object (readonly)

Returns the value of attribute dictionary.



75
76
77
 
# File 'lib/steep/subtyping/constraints.rb', line 75

def dictionary
  @dictionary
end

#vars ⇒ Object (readonly)

Returns the value of attribute vars.



76
77
78
 
# File 'lib/steep/subtyping/constraints.rb', line 76

def vars
  @vars
end

Class Method Details

.empty ⇒ Object 



87
88
89
 
# File 'lib/steep/subtyping/constraints.rb', line 87

def self.empty
  new(unknowns: [])
end

Instance Method Details

#add(var, sub_type: nil, super_type: nil, skip: false) ⇒ Object 



104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
 
# File 'lib/steep/subtyping/constraints.rb', line 104

def add(var, sub_type: nil, super_type: nil, skip: false)
  subs, supers, skips = dictionary.fetch(var)

  if sub_type.is_a?(AST::Types::Logic::Base)
    sub_type = AST::Builtin.bool_type
  end

  if super_type.is_a?(AST::Types::Logic::Base)
    super_type = AST::Builtin.bool_type
  end

  if super_type && !super_type.is_a?(AST::Types::Top)
    type = eliminate_variable(super_type, to: AST::Types::Top.instance)
    supers << type
    skips << type if skip
  end

  if sub_type && !sub_type.is_a?(AST::Types::Bot)
    type = eliminate_variable(sub_type, to: AST::Types::Bot.instance)
    subs << type
    skips << type if skip
  end

  super_fvs = supers.each_with_object(Set.new) do |type, fvs|
    fvs.merge(type.free_variables)
  end
  sub_fvs = subs.each_with_object(Set.new) do |type, fvs|
    fvs.merge(type.free_variables)
  end

  unless super_fvs.disjoint?(unknowns) || sub_fvs.disjoint?(unknowns)
    raise UnsatisfiedInvariantError.new(
      reason: UnsatisfiedInvariantError::UnknownsFreeVariableNotDisjoint.new(
        var: var,
        lower_bound: sub_type,
        upper_bound: super_type
      ),
      constraints: self
    )
  end
end

#add_var(*vars) ⇒ Object 



91
92
93
94
95
96
97
98
99
100
101
102
 
# File 'lib/steep/subtyping/constraints.rb', line 91

def add_var(*vars)
  vars.each do |var|
    self.vars << var
  end

  unless Set.new(vars).disjoint?(unknowns)
    raise UnsatisfiedInvariantError.new(
      reason: UnsatisfiedInvariantError::VariablesUnknownsNotDisjoint.new(vars: vars),
      constraints: self
    )
  end
end

#each ⇒ Object 



304
305
306
307
308
309
310
311
312
 
# File 'lib/steep/subtyping/constraints.rb', line 304

def each
  if block_given?
    dictionary.each_key do |var|
      yield [var, lower_bound(var), upper_bound(var)]
    end
  else
    enum_for :each
  end
end

#eliminate_variable(type, to:) ⇒ Object 



146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
 
# File 'lib/steep/subtyping/constraints.rb', line 146

def eliminate_variable(type, to:)
  case type
  when AST::Types::Name::Instance, AST::Types::Name::Alias, AST::Types::Name::Interface
    type.args.map do |ty|
      eliminate_variable(ty, to: AST::Types::Any.instance)
    end.yield_self do |args|
      type.class.new(name: type.name, args: args)
    end
  when AST::Types::Union
    type.types.map do |ty|
      eliminate_variable(ty, to: AST::Types::Any.instance)
    end.yield_self do |types|
      AST::Types::Union.build(types: types)
    end
  when AST::Types::Intersection
    type.types.map do |ty|
      eliminate_variable(ty, to: AST::Types::Any.instance)
    end.yield_self do |types|
      AST::Types::Intersection.build(types: types)
    end
  when AST::Types::Var
    if vars.member?(type.name)
      to
    else
      type
    end
  when AST::Types::Tuple
    AST::Types::Tuple.new(
      types: type.types.map {|ty| eliminate_variable(ty, to: AST::Builtin.any_type) }
    )
  when AST::Types::Record
    type.map_type { eliminate_variable(_1, to: AST::Builtin.any_type) }
  when AST::Types::Proc
    type.map_type {|ty| eliminate_variable(ty, to: AST::Builtin.any_type) }
  else
    type
  end
end

#empty? ⇒ Boolean

Returns:

  • (Boolean) 


199
200
201
 
# File 'lib/steep/subtyping/constraints.rb', line 199

def empty?
  dictionary.keys.empty?
end

#has_constraint?(var) ⇒ Boolean

Returns:

  • (Boolean) 


300
301
302
 
# File 'lib/steep/subtyping/constraints.rb', line 300

def has_constraint?(var)
  !upper_bound_types(var).empty? || !lower_bound_types(var).empty?
end

#lower_bound(var, skip: false) ⇒ Object 



220
221
222
223
224
225
226
227
228
229
230
231
 
# File 'lib/steep/subtyping/constraints.rb', line 220

def lower_bound(var, skip: false)
  lower_bound = lower_bound_types(var)

  case lower_bound.size
  when 0
    AST::Types::Bot.instance
  when 1
    lower_bound.first || raise
  else
    AST::Types::Union.build(types: lower_bound.to_a)
  end
end

#lower_bound_types(var_name) ⇒ Object 



322
323
324
325
 
# File 'lib/steep/subtyping/constraints.rb', line 322

def lower_bound_types(var_name)
  lower, _, _ = dictionary.fetch(var_name)
  lower
end

#solution(checker, variance: nil, variables:, self_type: nil, instance_type: nil, class_type: nil, context: nil) ⇒ Object 



235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
 
# File 'lib/steep/subtyping/constraints.rb', line 235

def solution(checker, variance: nil, variables:, self_type: nil, instance_type: nil, class_type: nil, context: nil)
  if context
    raise if variance
    raise if self_type
    raise if instance_type
    raise if class_type

    variance = context.variance
    self_type = context.self_type
    instance_type = context.instance_type
    class_type = context.class_type
  end

  vars = [] #: Array[Symbol]
  types = [] #: Array[AST::Types::t]

  dictionary.each_key do |var|
    if variables.include?(var)
      if has_constraint?(var)
        relation = Relation.new(
          sub_type: lower_bound(var, skip: false),
          super_type: upper_bound(var, skip: false)
        )

        checker.check(relation, self_type: self_type, instance_type: instance_type, class_type: class_type, constraints: self.class.empty).yield_self do |result|
          if result.success?
            vars << var

            upper_bound = upper_bound(var, skip: true)
            lower_bound = lower_bound(var, skip: true)

            type =
              case
              when variance.contravariant?(var)
                upper_bound
              when variance.covariant?(var)
                lower_bound
              else
                if lower_bound.level.join > upper_bound.level.join
                  upper_bound
                else
                  lower_bound
                end
              end

            types << type
          else
            raise UnsatisfiableConstraint.new(
              var: var,
              sub_type: result.relation.sub_type,
              super_type: result.relation.super_type,
              result: result
            )
          end
        end
      else
        vars << var
        types << AST::Types::Any.instance
      end
    end
  end

  Interface::Substitution.build(vars, types)
end

#to_s ⇒ Object 



314
315
316
317
318
319
320
 
# File 'lib/steep/subtyping/constraints.rb', line 314

def to_s
  strings = each.map do |var, lower_bound, upper_bound|
    "#{lower_bound} <: #{var} <: #{upper_bound}"
  end

  "#{unknowns.to_a.join(",")}/#{vars.to_a.join(",")} |- { #{strings.join(", ")} }"
end

#unknown!(var) ⇒ Object 



193
194
195
196
197
 
# File 'lib/steep/subtyping/constraints.rb', line 193

def unknown!(var)
  unless unknown?(var)
    dictionary[var] = [Set.new, Set.new, Set.new]
  end
end

#unknown?(var) ⇒ Boolean

Returns:

  • (Boolean) 


185
186
187
 
# File 'lib/steep/subtyping/constraints.rb', line 185

def unknown?(var)
  dictionary.key?(var)
end

#unknowns ⇒ Object 



189
190
191
 
# File 'lib/steep/subtyping/constraints.rb', line 189

def unknowns
  Set.new(dictionary.keys)
end

#upper_bound(var, skip: false) ⇒ Object 



203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
 
# File 'lib/steep/subtyping/constraints.rb', line 203

def upper_bound(var, skip: false)
  if skip
    upper_bound = upper_bound_types(var)
  else
    _, upper_bound, _ = dictionary.fetch(var)
  end

  case upper_bound.size
  when 0
    AST::Types::Top.instance
  when 1
    upper_bound.first || raise
  else
    AST::Types::Intersection.build(types: upper_bound.to_a)
  end
end

#upper_bound_types(var_name) ⇒ Object 



327
328
329
330
331
332
333
334
335
336
337
338
 
# File 'lib/steep/subtyping/constraints.rb', line 327

def upper_bound_types(var_name)
  _, upper, skips = dictionary.fetch(var_name)

  case
  when upper.empty?
    skips
  when skips.empty?
    upper
  else
    upper - skips
  end
end