Class: Rigor::Effects::Envelope

Inherits:
Object
  • Object
show all
Defined in:
lib/rigor/effects/envelope.rb

Overview

An author-declared upper bound on one method's effect labels (ADR-103 WD1; normative in docs/type-specification/effect-labels.md § Effect envelopes).

Four facts and one seam:

  • #owner_key — the method key the envelope binds (Class#m / Class.m). A class-level envelope is read once and #rebinded onto each method of that class discovery knows.
  • #bound — the LabelSet the method's proven labels must be subsumed by. LabelSet::TOP means "no envelope": the fail-open reading a tag carrying an unknown label degrades to.
  • #source — which spelling produced it: :pure_annotation (%a{pure}), :effect_annotation (%a{rigor:v1:effect …} on the method), :class_annotation (either spelling on the class / module declaration, which is also what #rebind stamps — what matters downstream is that the bound was distributed rather than written on the method) or :config_envelope (an effects.envelopes: entry, ConfigEnvelopes). The last one survives #rebind: a configured envelope is distributed by construction, so "distributed" is not the fact worth stamping — where it was written is.
  • #location — path:line of the annotation, or .rigor.yml effects.envelopes[N] for a configured one, so the diagnostic can name where the bound was written; #spelling is the author's own text, quoted back verbatim.
  • #unknown_labels — the well-formed-but-unrecognised spellings that made this envelope read ⊤ (#384's effect.unknown-label reads it). Empty otherwise.
  • #declared_labels — every token the tag listed, in source order, recognised or not (empty for %a{pure}, whose bound is written by its spelling rather than by a list). It is what answers "was some OTHER member of this list known?", one of the four signals LabelIntent reads intent off.

mutate.local is tolerated by every envelope, %a{pure} included: a method may freely mutate what its own frame allocated and never let escape.

Constant Summary collapse

CONFIG_SOURCE =

#source for a bound written in .rigor.yml rather than on a declaration.

:config_envelope

Class Method Summary collapse

Instance Method Summary collapse

Class Method Details

.build(owner_key:, bound:, source:, location: nil, spelling: nil, unknown_labels: NO_LABELS, declared_labels: NO_LABELS) ⇒ Object 



45
46
47
48
49
50
51
52
 
# File 'lib/rigor/effects/envelope.rb', line 45

def self.build(owner_key:, bound:, source:, location: nil, spelling: nil, unknown_labels: NO_LABELS,
               declared_labels: NO_LABELS)
  new(
    owner_key: owner_key, bound: bound, source: source, location: location,
    spelling: spelling, unknown_labels: unknown_labels.uniq.sort.freeze,
    declared_labels: declared_labels.dup.freeze
  )
end

Instance Method Details

#config? ⇒ Boolean

Whether the bound was written in .rigor.yml rather than on a declaration.

Returns:

  • (Boolean) 


73
74
75
 
# File 'lib/rigor/effects/envelope.rb', line 73

def config?
  source == CONFIG_SOURCE
end

#exceeded_by(label_set) ⇒ Object

The members of label_set this envelope does NOT admit, sorted. One diagnostic per member.



66
67
68
69
70
 
# File 'lib/rigor/effects/envelope.rb', line 66

def exceeded_by(label_set)
  return NO_LABELS if top?

  label_set.to_a.reject { |label| tolerates?(label) }
end

#rebind(key) ⇒ Object

The same bound, attached to another method key — how a class-level envelope reaches each method of its class. The source becomes :class_annotation, because the distribution is the fact the diagnostic has to explain; a configured envelope keeps its own source, because for it distribution is the only mode there is and .rigor.yml is the fact worth naming.



81
82
83
 
# File 'lib/rigor/effects/envelope.rb', line 81

def rebind(key)
  config? ? with(owner_key: key) : with(owner_key: key, source: :class_annotation)
end

#tolerates?(label) ⇒ Boolean

Whether label is inside the bound. mutate.local always is.

Returns:

  • (Boolean) 


61
62
63
 
# File 'lib/rigor/effects/envelope.rb', line 61

def tolerates?(label)
  bound.admits?(label) || Summary::TRIVIAL_BOUND.admits?(label)
end

#top? ⇒ Boolean

Whether this reads as ⊤ — no bound at all. An unknown label degrades the whole tag here, so a typo suppresses findings rather than inventing them (the fail-open rule).

Returns:

  • (Boolean) 


56
57
58
 
# File 'lib/rigor/effects/envelope.rb', line 56

def top?
  bound.top?
end