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.



248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
 
# File 'lib/rigor/inference/narrowing.rb', line 248

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:



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

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.



173
174
175
176
 
# File 'lib/rigor/inference/narrowing.rb', line 173

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.



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

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



184
185
186
187
 
# File 'lib/rigor/inference/narrowing.rb', line 184

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.



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

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



196
197
198
199
200
201
 
# File 'lib/rigor/inference/narrowing.rb', line 196

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

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