Class: Rigor::Effects::LabelSet

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

Overview

An immutable, sorted, de-duplicated set of effect labels — the carrier of a summary lane and of an envelope's bound (ADR-103 WD1).

Two sentinels bracket the lattice. EMPTY is the empty set: "no effects", the reading of %a{pure} modulo mutate.local. TOP is the unbounded / unspecified reading: it admits every label, it absorbs every join, and it is what a tag carrying an unknown label degrades to (the fail-open rule). TOP is NOT the set of all registered labels and is deliberately not enumerable — top? is the only way to tell it from EMPTY through to_a.

Instances are frozen on construction and hold a frozen array, so they cross a Ractor boundary and go into a cache entry as they are.

Constant Summary collapse

TOP =

The unbounded set. Everything is subsumed by it; joining it with anything yields it.

new(NO_LABELS, top: true)
EMPTY =

The empty set — no effects at all.

new(NO_LABELS)

Instance Method Summary collapse

Constructor Details

#initialize(labels = NO_LABELS, top: false) ⇒ LabelSet

Build a set from any enumerable of label strings. Members are normalised (de-duplicated and sorted) so equality is structural and a snapshot rendering is deterministic.

Raises ArgumentError on a member that does not satisfy Rigor::Effects::Label::PATTERN: a LabelSet is a value object over the grammar, and the fail-open handling of an unrecognised spelling is the reader's job (it yields TOP), not this constructor's.

top: is internal — it exists to build TOP and is not part of the surface later slices build on.



31
32
33
34
35
36
37
38
39
40
41
42
 
# File 'lib/rigor/effects/label_set.rb', line 31

def initialize(labels = NO_LABELS, top: false)
  @top = top
  @labels = NO_LABELS
  unless top
    members = labels.to_a
    members.each do |label|
      raise ArgumentError, "not a well-formed effect label: #{label.inspect}" unless Label.valid?(label)
    end
    @labels = members.uniq.sort.freeze
  end
  freeze
end

Instance Method Details

#==(other) ⇒ Object Also known as: eql? 



118
119
120
121
122
 
# File 'lib/rigor/effects/label_set.rb', line 118

def ==(other)
  return true if equal?(other)

  other.is_a?(LabelSet) && other.top? == @top && other.to_a == @labels
end

#admits?(label) ⇒ Boolean

Whether some member of this set subsumes label. TOP admits every well-formed label.

Returns:

  • (Boolean) 


73
74
75
76
77
 
# File 'lib/rigor/effects/label_set.rb', line 73

def admits?(label)
  return Label.valid?(label) if @top

  @labels.any? { |member| Label.subsumes?(member, label) }
end

#empty? ⇒ Boolean

Whether this set records no labels. TOP is not empty: it records nothing because it stands for everything.

Returns:

  • (Boolean) 


57
58
59
 
# File 'lib/rigor/effects/label_set.rb', line 57

def empty?
  !@top && @labels.empty?
end

#excluding_subsumed_by(other) ⇒ Object

The members other does not already admit — the declared lane's rendering rule. A declared io.net.http beside a proven io.net says nothing the proven lane did not already say more strongly, so a renderer drops it rather than printing [io.net] ≤ [io.net.http], which reads as two facts where there is one. Applied where output is produced, never to the table: the lanes themselves stay raw, because a later join has to see what was actually declared.



100
101
102
103
104
105
106
107
 
# File 'lib/rigor/effects/label_set.rb', line 100

def excluding_subsumed_by(other)
  return self if @top || other.empty?

  kept = @labels.reject { |label| other.admits?(label) }
  return self if kept.length == @labels.length

  kept.empty? ? EMPTY : self.class.new(kept)
end

#hash ⇒ Object 



125
126
127
 
# File 'lib/rigor/effects/label_set.rb', line 125

def hash
  [self.class, @top, @labels].hash
end

#include?(label) ⇒ Boolean

Exact membership among the recorded labels. LabelSet.new(["io"]).include?("io.net") is false — that question is #admits?. TOP records no members, so it includes none.

Returns:

  • (Boolean) 


68
69
70
 
# File 'lib/rigor/effects/label_set.rb', line 68

def include?(label)
  @labels.include?(label)
end

#inspect ⇒ Object 



129
130
131
132
133
 
# File 'lib/rigor/effects/label_set.rb', line 129

def inspect
  return "#<Rigor::Effects::LabelSet TOP>" if @top

  "#<Rigor::Effects::LabelSet #{@labels.join(', ')}>"
end

#join(other) ⇒ Object

Union. TOP absorbs: a join involving it is TOP.

A join that adds nothing returns self without allocating. That is the common case wherever sets are joined in a loop — the propagator's fixpoint re-joins every edge on every visit — and the sets are single-digit-sized, so the containment scan is cheaper than the construction it avoids.



84
85
86
87
88
89
90
91
92
93
 
# File 'lib/rigor/effects/label_set.rb', line 84

def join(other)
  return TOP if @top || other.top?
  return other if @labels.empty?

  others = other.to_a
  return self if others.empty?
  return self if others.all? { |label| @labels.include?(label) }

  self.class.new(@labels + others)
end

#subsumed_by?(bound_set) ⇒ Boolean

Whether every member of this set is admitted by bound_set — the envelope check, modulo the policy discharge that happens at judgment time. TOP is bounded only by TOP.

Returns:

  • (Boolean) 


111
112
113
114
115
116
 
# File 'lib/rigor/effects/label_set.rb', line 111

def subsumed_by?(bound_set)
  return true if bound_set.top?
  return false if @top

  @labels.all? { |label| bound_set.admits?(label) }
end

#to_a ⇒ Object

The members, sorted, as a frozen array. TOP yields [] — consult #top? first.



62
63
64
 
# File 'lib/rigor/effects/label_set.rb', line 62

def to_a
  @labels
end

#top? ⇒ Boolean

Whether this is the unbounded sentinel TOP.

Returns:

  • (Boolean) 


51
52
53
 
# File 'lib/rigor/effects/label_set.rb', line 51

def top?
  @top
end