Module: Rigor::Inference::Narrowing

Defined in:
lib/rigor/inference/narrowing.rb

Overview

Control-flow predicate narrowing and type-lattice narrowing primitives.

‘Rigor::Inference::Narrowing` answers two related questions:

  1. Type-level narrowing: given a ‘Rigor::Type` value, what is its truthy fragment, its falsey fragment, its nil fragment, and its non-nil fragment? These primitives understand the value-lattice algebra (`Constant`, `Nominal`, `Singleton`, `Tuple`, `HashShape`, `Union`) and stay conservative on `Top` and `Dynamic`.

  2. Predicate-level narrowing: given a Prism predicate node and an entry scope, what are the truthy-edge scope and the falsey-edge scope? The catalogue covers truthiness, ‘nil?`, `!`, `&&`/`||`, class-membership (`is_a?`, `kind_of?`, `instance_of?`), trusted equality/inequality against static literals, `case`/`when`, regex match globals, string predicates (`start_with?` etc.), key-presence, array emptiness, numeric comparison, and `respond_to?`.

Consumed by ‘Rigor::Inference::StatementEvaluator` to refine `then`/`else` scopes of `IfNode`/`UnlessNode` and `case`/`when` branches.

The module is pure: every public function returns fresh values and MUST NOT mutate its inputs. Unrecognised predicate shapes degrade silently to “no narrowing” by returning ‘nil` from the internal analyser; the public `predicate_scopes` always returns an `[truthy_scope, falsey_scope]` pair (the entry scope twice when no rule matches).

See docs/internal-spec/inference-engine.md (Narrowing) and docs/type-specification/control-flow-analysis.md for the binding contract. rubocop:disable Metrics/ModuleLength

Constant Summary collapse

VALUE_EQUALITY_CLASSES =

Classes whose ‘===` is plain value equality, so a literal `when` pattern against a pinned `Constant` subject is exact in both directions. Anything else keeps custom-`===` semantics and stays `:maybe` in value_pattern_certainty.

[Integer, Float, Rational, Complex, String, Symbol,
TrueClass, FalseClass, NilClass].freeze

Class Method Summary collapse

Class Method Details

.analyse(node, scope) ⇒ Object

Internal analyser. Returns ‘[truthy_scope, falsey_scope]` when the predicate shape is recognised, or `nil` to signal “no narrowing” so the public surface can fall back to the entry scope.



469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
 
# File 'lib/rigor/inference/narrowing.rb', line 469

def analyse(node, scope)
  case node
  when Prism::ParenthesesNode
    analyse_parentheses(node, scope)
  when Prism::StatementsNode
    analyse_statements(node, scope)
  when Prism::LocalVariableReadNode
    analyse_local_read(node, scope)
  when Prism::LocalVariableWriteNode
    analyse_local_write(node, scope)
  when Prism::InstanceVariableReadNode, Prism::InstanceVariableWriteNode
    analyse_ivar(node, scope)
  when Prism::ClassVariableWriteNode
    analyse_cvar_write(node, scope)
  when Prism::GlobalVariableWriteNode
    analyse_global_write(node, scope)
  when Prism::CallNode
    analyse_call(node, scope)
  when Prism::AndNode
    analyse_and(node, scope)
  when Prism::OrNode
    analyse_or(node, scope)
  when Prism::MatchWriteNode
    analyse_match_write(node, scope)
  end
end

.apply_when_regex_globals(conditions, scope) ⇒ Object

When the clause has exactly one ‘RegularExpressionNode` literal condition, narrow the match-data globals on the body edge (same rule as `analyse_regex_match_predicate`’s truthy edge). With multiple regex conditions (‘when /a/, /b/`) the body is reachable through any of them, so only `$~`/`$&` are safely non-nil; numbered groups whose presence differs per alternative stay `String | nil`. With no regex condition the entry scope passes through unchanged.



451
452
453
454
455
456
457
458
459
460
461
462
463
 
# File 'lib/rigor/inference/narrowing.rb', line 451

def apply_when_regex_globals(conditions, scope)
  regexes = conditions.grep(Prism::RegularExpressionNode)
  return scope if regexes.empty?

  unconditional =
    if regexes.size == 1
      unconditional_capture_groups(regexes.first.unescaped)
    else
      Set.new
    end
  truthy, = regex_match_predicate_scopes(scope, unconditional)
  truthy
end

.case_when_scopes(subject, conditions, scope) ⇒ Array(Rigor::Scope, Rigor::Scope)

Slice 7 phase 5 — ‘case`/`when` narrowing.

Given the subject of a ‘case` (the expression after the `case` keyword) and an array of `when`-clause condition nodes (`when_clause.conditions`), returns a pair of scopes:

  • ‘body_scope`: the scope under which the body of the `when` clause MUST be evaluated. The subject local is narrowed by the union of every condition’s truthy edge so the body sees the most specific type compatible with “any of the conditions matched”.

  • ‘falsey_scope`: the scope under which the next branch (the next `when` or the `else`) MUST be evaluated. The subject is narrowed by the conjunction of every condition’s falsey edge.

The narrowing is best-effort: if the subject is not a ‘Prism::LocalVariableReadNode` or none of the condition shapes are recognised, both returned scopes equal the input scope. The catalogue mirrors case_equality_target_class: static class/module constants narrow as `is_a?`; integer/float-endpoint ranges narrow to `Numeric`; string-endpoint ranges and regexp literals narrow to `String`.

Parameters:

  • subject (Prism::Node, nil) —

    the ‘case` subject.

  • conditions (Array<Prism::Node>) —

    the ‘when` clause’s ‘conditions` array.

  • scope (Rigor::Scope)

Returns:



423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
 
# File 'lib/rigor/inference/narrowing.rb', line 423

def case_when_scopes(subject, conditions, scope)
  # C1 — `case x when /re/` runs `/re/ === x`, which sets the
  # regex match-data globals exactly as a successful `=~` does.
  # Narrow `$~`/`$&`/`$1..$N` on the clause body (the match
  # edge); the falsey scope keeps the entry globals because a
  # later clause may match a different regex. Applied even when
  # the subject is not a narrowable local read.
  body_scope = apply_when_regex_globals(conditions, scope)

  return [body_scope, scope] unless subject.is_a?(Prism::LocalVariableReadNode)

  local_name = subject.name
  current = scope.local(local_name)
  return [body_scope, scope] if current.nil?

  truthy, = accumulate_case_when_scopes(body_scope, local_name, current, conditions)
  _, falsey = accumulate_case_when_scopes(scope, local_name, current, conditions)
  [truthy, falsey]
end

.class_pattern_certainty(subject_type, class_name, environment:) ⇒ Object

Three-valued certainty of ‘C === subject` for a class / module `when` pattern, derived from narrow_class / narrow_not_class: `:no` when no inhabitant of the subject matches, `:yes` when every inhabitant matches, `:maybe` otherwise. The value-side counterpart of the scope narrowing case_when_scopes performs for the same condition shape, kept here so the branch a `case` expression’s type drops and the clause whose body scope goes dead derive from one judgment.



155
156
157
158
159
160
161
162
163
 
# File 'lib/rigor/inference/narrowing.rb', line 155

def class_pattern_certainty(subject_type, class_name, environment:)
  truthy_bot = narrow_class(subject_type, class_name, environment: environment).is_a?(Type::Bot)
  falsey_bot = narrow_not_class(subject_type, class_name, environment: environment).is_a?(Type::Bot)

  return :no if truthy_bot && !falsey_bot
  return :yes if !truthy_bot && falsey_bot

  :maybe
end

.narrow_class(type, class_name, exact: false, environment: Environment.default) ⇒ Object

Class-membership fragment of ‘type`: the subset whose inhabitants are instances of `class_name` (or its subclasses when `exact: false`). `class_name` is the qualified name of the class as it appears in source (`“Integer”`, `“Foo::Bar”`). Slice 6 phase 2 sub-phase 1 narrows the `if x.is_a?©` / `if x.kind_of?©` / `if x.instance_of?©` truthy edge.

Nominal narrowing is hierarchy-aware through the analyzer environment: when the bound type is a supertype of ‘class_name` the result narrows DOWN to `Nominal` (e.g., `Numeric & Integer = Integer`); when the bound type is already a subtype it is preserved; disjoint hierarchies collapse to `Bot`. Classes the environment cannot resolve fall back to the conservative answer (the type unchanged) so the analyzer never asserts narrowing it cannot prove.



288
289
290
291
 
# File 'lib/rigor/inference/narrowing.rb', line 288

def narrow_class(type, class_name, exact: false, environment: Environment.default)
  context = ClassNarrowingContext.new(exact: exact, polarity: :positive, environment: environment)
  narrow_class_dispatch(type, class_name, context)
end

.narrow_equal(type, literal) ⇒ Object

Equality fragment of ‘type` against a trusted literal.

String/Symbol/Integer equality narrows only when the current domain is already a finite union of trusted literals. Nil and booleans are singleton values, so they can be extracted from a mixed union such as ‘Integer | nil` without manufacturing a new positive domain from the comparison alone.



191
192
193
194
195
196
197
198
199
200
201
 
# File 'lib/rigor/inference/narrowing.rb', line 191

def narrow_equal(type, literal)
  return type unless trusted_equality_literal?(literal)

  if singleton_literal?(literal)
    narrow_singleton_equal(type, literal)
  elsif finite_trusted_literal_domain?(type)
    narrow_finite_equal(type, literal)
  else
    type
  end
end

.narrow_falsey(type) ⇒ Object

Falsey fragment of ‘type`: the subset whose inhabitants are `nil` or `false`. Carriers that cannot inhabit a falsey value collapse to `Bot`.



81
82
83
84
85
86
87
88
 
# File 'lib/rigor/inference/narrowing.rb', line 81

def narrow_falsey(type)
  case type
  when Type::Constant then falsey_value?(type.value) ? type : Type::Combinator.bot
  when Type::Nominal then falsey_nominal?(type) ? type : Type::Combinator.bot
  when Type::Union then Type::Combinator.union(*type.members.map { |m| narrow_falsey(m) })
  else narrow_falsey_other(type)
  end
end

.narrow_for_fact(current, fact, environment) ⇒ Object

ADR-7 § “Slice 4-A” — public Fact-shaped narrowing entry. Distinguishes a ‘Nominal`-typed Fact (uses `narrow_class` / `narrow_not_class` for hierarchy-aware narrowing) from a refinement-shaped Fact (refined types, IntegerRange, Difference, …). The implementation lives next to its sibling helpers `narrow_class` and `narrow_not_refinement`; consumers outside `Narrowing` (today: `StatementEvaluator`’s post-return assertion path) reach for it via ‘Rigor::Inference::Narrowing.narrow_for_fact`.



365
366
367
368
369
370
371
372
373
374
375
376
 
# File 'lib/rigor/inference/narrowing.rb', line 365

def narrow_for_fact(current, fact, environment)
  if fact.type.is_a?(Type::Nominal) && fact.type.type_args.empty?
    class_name = fact.type.class_name
    return narrow_not_class(current, class_name, exact: false, environment: environment) if fact.negative?

    return narrow_class(current, class_name, exact: false, environment: environment)
  end

  return narrow_not_refinement(current, fact.type) if fact.negative?

  fact.type
end

.narrow_integer_comparison(type, comparator, bound) ⇒ Object

Integer-comparison fragment of ‘type` against an Integer literal `bound`. Narrows the receiver of `x < n`, `x <= n`, `x > n`, `x >= n` (and the reversed forms) to the subset of the existing domain that satisfies the comparison. Hooks in:

  • ‘Constant<Integer>` is preserved when it satisfies the comparison, otherwise collapsed to `Bot`.

  • ‘IntegerRange` becomes the intersection with the half-line implied by the comparison; an empty intersection collapses to `Bot`, a single-point intersection collapses to `Constant<Integer>`.

  • ‘Nominal` becomes the half-line itself (e.g. `x > 0` on `Nominal` is `positive_int`).

  • ‘Union` narrows each member independently.

  • Other carriers (Float, String, Top, Dynamic) flow through unchanged: the analyzer does not have a Float-range carrier today, and no other carrier participates in numeric ordering.



234
235
236
237
238
 
# File 'lib/rigor/inference/narrowing.rb', line 234

def narrow_integer_comparison(type, comparator, bound)
  return type unless bound.is_a?(Integer) && %i[< <= > >=].include?(comparator)

  narrow_integer_comparison_dispatch(type, comparator, bound)
end

.narrow_integer_equal(type, value) ⇒ Object

Equality fragment of ‘type` against an Integer `value`. `Constant<Integer>` is preserved when it equals `value`, otherwise collapses to `Bot`. `IntegerRange` covers? `value` narrows to `Constant`; an out-of-range comparison collapses to `Bot`. `Nominal` narrows to `Constant`. `Union` narrows each member.



246
247
248
249
250
 
# File 'lib/rigor/inference/narrowing.rb', line 246

def narrow_integer_equal(type, value)
  return type unless value.is_a?(Integer)

  narrow_integer_equal_dispatch(type, value)
end

.narrow_integer_not_equal(type, value) ⇒ Object

Complement of narrow_integer_equal. Removes a single integer value from the domain when one endpoint of an ‘IntegerRange` is exactly that value (so the result stays a contiguous range). Domains where the value sits strictly between the endpoints stay unchanged: punching a hole would require a two-piece carrier the lattice does not yet model.



258
259
260
261
262
263
264
265
266
267
268
269
270
271
 
# File 'lib/rigor/inference/narrowing.rb', line 258

def narrow_integer_not_equal(type, value)
  return type unless value.is_a?(Integer)

  case type
  when Type::Constant
    type.value == value ? Type::Combinator.bot : type
  when Type::IntegerRange
    narrow_integer_range_not_equal(type, value)
  when Type::Union
    Type::Combinator.union(*type.members.map { |m| narrow_integer_not_equal(m, value) })
  else
    type
  end
end

.narrow_nil(type) ⇒ Object

Nil fragment of ‘type`: the subset whose inhabitants are `nil`. Used by `nil?` predicate narrowing. `Top`/`Dynamic` narrow to the canonical `Constant` so downstream dispatch resolves through `NilClass`; carriers that never inhabit `nil` (`Singleton`, `Tuple`, `HashShape`) collapse to `Bot`. `Bot` is its own nil fragment.



96
97
98
99
100
101
102
103
 
# File 'lib/rigor/inference/narrowing.rb', line 96

def narrow_nil(type)
  case type
  when Type::Constant then type.value.nil? ? type : Type::Combinator.bot
  when Type::Nominal then type.class_name == "NilClass" ? type : Type::Combinator.bot
  when Type::Union then Type::Combinator.union(*type.members.map { |m| narrow_nil(m) })
  else narrow_nil_other(type)
  end
end

.narrow_non_nil(type) ⇒ Object

Non-nil fragment of ‘type`: the subset whose inhabitants are not `nil`. Mirror of narrow_nil for the falsey edge of `x.nil?`.



108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
 
# File 'lib/rigor/inference/narrowing.rb', line 108

def narrow_non_nil(type)
  case type
  when Type::Constant
    type.value.nil? ? Type::Combinator.bot : type
  when Type::Nominal
    type.class_name == "NilClass" ? Type::Combinator.bot : type
  when Type::Union
    Type::Combinator.union(*type.members.map { |m| narrow_non_nil(m) })
  else
    # Top, Dynamic, Singleton, Tuple, HashShape, Bot: there is
    # no nil contribution to remove, so the type is its own
    # non-nil fragment.
    type
  end
end

.narrow_not_class(type, class_name, exact: false, environment: Environment.default) ⇒ Object

Mirror of narrow_class for the falsey edge of ‘is_a?`/`kind_of?`/`instance_of?`. Inhabitants that DO satisfy the predicate are removed; inhabitants that do not are preserved. Conservative on Top/Dynamic/Bot (preserved unchanged) because the analyzer cannot prove the negative without a richer carrier.



299
300
301
302
 
# File 'lib/rigor/inference/narrowing.rb', line 299

def narrow_not_class(type, class_name, exact: false, environment: Environment.default)
  context = ClassNarrowingContext.new(exact: exact, polarity: :negative, environment: environment)
  narrow_class_dispatch(type, class_name, context)
end

.narrow_not_equal(type, literal) ⇒ Object

Complement of narrow_equal. Negative facts are domain-relative: they remove a literal from an already-known domain but do not create an unbounded difference type when the domain is broad or dynamic.



206
207
208
209
210
211
212
213
214
215
216
 
# File 'lib/rigor/inference/narrowing.rb', line 206

def narrow_not_equal(type, literal)
  return type unless trusted_equality_literal?(literal)

  if singleton_literal?(literal)
    narrow_singleton_not_equal(type, literal)
  elsif finite_trusted_literal_domain?(type)
    narrow_finite_not_equal(type, literal)
  else
    type
  end
end

.narrow_not_refinement(current_type, refinement_type) ⇒ Object

Negation pair for ‘assert_value is ~refinement` / `predicate-if-* … is ~refinement` directives. Computes the complement of `refinement` within the current local’s domain ‘current_type`.

Carrier-by-carrier rules:

  • ‘Difference[base, Constant]`. Complement of `base \ v` within `current_type`. Walk the current type’s union members, keep each part disjoint from ‘base`, and add the removed-value Constant once when any current member covers it. `assert s is ~non-empty-string` over `s: String | nil` narrows to `Constant | NilClass`.

  • ‘IntegerRange[a, b]` (v0.0.5+ slice). Complement is the two open halves `int<min, a-1>` and `int<b+1, max>`, each intersected with the integer-domain parts of `current_type`. Non-integer parts (nil, String, …) of a Union receiver survive unchanged. `assert n is ~int<5, 10>` over `n: Integer | nil` narrows to `int<min, 4> | int<11, max> | NilClass`.

  • ‘Type::Intersection[M1, M2, …]` (v0.0.5+ slice). De Morgan: `D \ (M1 ∩ M2) = (D \ M1) ∪ (D \ M2)`. Each member’s complement is computed independently within ‘current_type` and the results are unioned. Members the algebra cannot complement (Refined, non-Constant Difference, …) contribute `current_type` itself, so the union widens the answer to `current_type` —sound but imprecise.

  • ‘Refined[base, predicate]`. Predicate complements are not reducible to a finite carrier without a richer shape (e.g. `~lowercase-string` is “uppercase OR mixed-case”); `current_type` is returned unchanged.



338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
 
# File 'lib/rigor/inference/narrowing.rb', line 338

def narrow_not_refinement(current_type, refinement_type)
  case refinement_type
  when Type::Difference
    return current_type unless refinement_type.removed.is_a?(Type::Constant)

    complement_difference(current_type, refinement_type)
  when Type::IntegerRange
    complement_integer_range(current_type, refinement_type)
  when Type::Intersection
    complement_intersection(current_type, refinement_type)
  when Type::Refined
    complement_refined(current_type, refinement_type)
  else
    current_type
  end
end

.narrow_truthy(type) ⇒ Object

Truthy fragment of ‘type`: the subset whose inhabitants are truthy in Ruby’s sense (anything other than ‘nil` and `false`).

‘Top`, `Dynamic`, `Bot`, `Singleton`, `Tuple`, and `HashShape*` flow through unchanged: Top/Dynamic stay conservative because the analyzer cannot express the difference type without a richer carrier and Dynamic must preserve its provenance under the value-lattice algebra; the remaining carriers are already truthy by inhabitance.



65
66
67
68
69
70
71
72
73
74
75
76
 
# File 'lib/rigor/inference/narrowing.rb', line 65

def narrow_truthy(type)
  case type
  when Type::Constant
    falsey_value?(type.value) ? Type::Combinator.bot : type
  when Type::Nominal
    falsey_nominal?(type) ? Type::Combinator.bot : type
  when Type::Union
    Type::Combinator.union(*type.members.map { |m| narrow_truthy(m) })
  else
    type
  end
end

.predicate_certainty(type) ⇒ Object

Three-valued truthiness certainty of a predicate’s type, derived from the truthy / falsey fragments above: ‘:truthy` when no inhabitant is falsey (the falsey fragment is `Bot`), `:falsey` when no inhabitant is truthy, nil when both fragments are inhabited — or when the type itself is nil / `Bot` (dead code is not a certainty claim). This is the single owner of the judgment both branch-elision consumers read (`ExpressionTyper#elide_or_union` on the value side, `StatementEvaluator#live_branch_for_if` on the scope side), so the type a dead branch is elided from and the scope that stops flowing through it can never disagree.



135
136
137
138
139
140
141
142
143
144
145
 
# File 'lib/rigor/inference/narrowing.rb', line 135

def predicate_certainty(type)
  return nil if type.nil? || type.is_a?(Type::Bot)

  truthy_bot = narrow_truthy(type).is_a?(Type::Bot)
  falsey_bot = narrow_falsey(type).is_a?(Type::Bot)

  return :falsey if truthy_bot && !falsey_bot
  return :truthy if !truthy_bot && falsey_bot

  nil
end

.predicate_scopes(node, scope) ⇒ Array(Rigor::Scope, Rigor::Scope)

Public predicate analyser. Returns ‘[truthy_scope, falsey_scope]`, always; when no narrowing rule matches the predicate node both entries are the receiver scope unchanged.

Parameters:

Returns:



385
386
387
388
389
390
 
# File 'lib/rigor/inference/narrowing.rb', line 385

def predicate_scopes(node, scope)
  return [scope, scope] if node.nil?

  result = analyse(node, scope)
  result || [scope, scope]
end

.value_pattern_certainty(subject_type, pattern_value) ⇒ Object

Three-valued certainty of ‘<literal> === subject` for a value-equality literal pattern: exact (`:yes` / `:no`) only when the subject is itself a pinned `Constant` of a value-equality class; `:maybe` otherwise (the runtime value isn’t pinned, or ‘===` may be user-defined).



177
178
179
180
181
182
 
# File 'lib/rigor/inference/narrowing.rb', line 177

def value_pattern_certainty(subject_type, pattern_value)
  return :maybe unless subject_type.is_a?(Type::Constant)
  return :maybe unless VALUE_EQUALITY_CLASSES.any? { |klass| subject_type.value.is_a?(klass) }

  pattern_value == subject_type.value ? :yes : :no
end