Module: Rigor::Inference::Narrowing

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

Overview

Slice 6 phase 1 minimal narrowing surface.

‘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`, where the analyzer cannot prove the boundary either way.

  2. Predicate-level narrowing: given a Prism predicate node and an entry scope, what are the truthy-edge scope and the falsey-edge scope after the predicate has been evaluated? The phase 1 catalogue covers truthiness on ‘LocalVariableReadNode`, `nil?` against a local, the unary `!` inverter, parenthesised predicates, and short-circuiting `&&` / `||` chains.

Predicate-level narrowing is consumed by ‘Rigor::Inference::StatementEvaluator` to refine the `then` and `else` scopes of `IfNode`/`UnlessNode`. Phase 1 narrows local bindings on truthiness and `nil?`; phase 2 extends the catalogue with class-membership predicates (`is_a?`, `kind_of?`, `instance_of?`) and trusted equality/inequality checks against static literals.

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 (Slice 6 — Narrowing) and docs/type-specification/control-flow-analysis.md for the binding contract. rubocop:disable Metrics/ModuleLength

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.



355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
 
# File 'lib/rigor/inference/narrowing.rb', line 355

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::CallNode
    analyse_call(node, scope)
  when Prism::AndNode
    analyse_and(node, scope)
  when Prism::OrNode
    analyse_or(node, scope)
  end
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:



341
342
343
344
345
346
347
348
349
 
# File 'lib/rigor/inference/narrowing.rb', line 341

def case_when_scopes(subject, conditions, scope)
  return [scope, scope] unless subject.is_a?(Prism::LocalVariableReadNode)

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

  accumulate_case_when_scopes(scope, local_name, current, conditions)
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.



229
230
231
232
 
# File 'lib/rigor/inference/narrowing.rb', line 229

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.



132
133
134
135
136
137
138
139
140
141
142
 
# File 'lib/rigor/inference/narrowing.rb', line 132

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



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

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



175
176
177
178
179
 
# File 'lib/rigor/inference/narrowing.rb', line 175

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.



187
188
189
190
191
 
# File 'lib/rigor/inference/narrowing.rb', line 187

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.



199
200
201
202
203
204
205
206
207
208
209
210
211
212
 
# File 'lib/rigor/inference/narrowing.rb', line 199

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.



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

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?`.



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

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.



240
241
242
243
 
# File 'lib/rigor/inference/narrowing.rb', line 240

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.



147
148
149
150
151
152
153
154
155
156
157
 
# File 'lib/rigor/inference/narrowing.rb', line 147

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.



279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
 
# File 'lib/rigor/inference/narrowing.rb', line 279

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.



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

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



303
304
305
306
307
308
 
# File 'lib/rigor/inference/narrowing.rb', line 303

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

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