Class: Ibex::Codegen::Explain

Inherits:
Object
  • Object
show all
Defined in:
lib/ibex/codegen/explain.rb,
sig/ibex/codegen/explain.rbs

Overview

Renders a selected conflict explanation from Automaton IR and counterexamples. rubocop:disable Metrics/ClassLength -- inline contracts and two stable output formats stay near selection policy.

Constant Summary collapse

SCHEMA_VERSION =

Signature:

  • Integer

Returns:

  • (Integer) 
1

Instance Method Summary collapse

Constructor Details

#initialize(automaton, state: nil, token: nil, max_tokens: LALR::Counterexample::DEFAULT_MAX_TOKENS, max_configurations: LALR::Counterexample::DEFAULT_MAX_CONFIGURATIONS) ⇒ Explain

Returns a new instance of Explain.

RBS:

  • (IR::Automaton automaton, ?state: Integer?, ?token: String?, ?max_tokens: Integer, ?max_configurations: Integer) -> void

Parameters:

  • automaton (IR::Automaton)
  • state: (Integer, nil) (defaults to: nil)
  • token: (String, nil) (defaults to: nil)
  • max_tokens: (Integer) (defaults to: LALR::Counterexample::DEFAULT_MAX_TOKENS)
  • max_configurations: (Integer) (defaults to: LALR::Counterexample::DEFAULT_MAX_CONFIGURATIONS) 


40
41
42
43
44
45
46
47
48
49
50
51
52
 
# File 'lib/ibex/codegen/explain.rb', line 40

def initialize(automaton, state: nil, token: nil, max_tokens: LALR::Counterexample::DEFAULT_MAX_TOKENS,
               max_configurations: LALR::Counterexample::DEFAULT_MAX_CONFIGURATIONS)
  @automaton = automaton
  @grammar = automaton.grammar
  @state_selector = state
  @token_query = token
  @max_tokens = max_tokens
  @max_configurations = max_configurations
  @labels = SymbolLabels.build(@grammar)
  @token_selector = resolve_token(token)
  validate_state!
  @entries = select_entries
end

Instance Method Details

#alternative_text(alternative) ⇒ String

RBS:

  • (explain_alternative alternative) -> String

Parameters:

  • alternative (explain_alternative)

Returns:

  • (String) 


335
336
337
338
339
 
# File 'lib/ibex/codegen/explain.rb', line 335

def alternative_text(alternative)
  return "shift to state #{alternative.fetch(:state)}" if alternative.fetch(:kind) == "shift"

  "reduce by production #{alternative.fetch(:production)}"
end

#append_conflict(lines, entry, number) ⇒ void

This method returns an undefined value.

RBS:

  • (Array[String] lines, explain_entry entry, Integer number) -> void

Parameters:

  • lines (Array[String])
  • entry (explain_entry)
  • number (Integer) 


276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
 
# File 'lib/ibex/codegen/explain.rb', line 276

def append_conflict(lines, entry, number)
  state = entry.fetch(:state)
  conflict = entry.fetch(:conflict)
  example = entry.fetch(:example)
  grammar = @grammar #: IR::Grammar
  token = grammar.symbol(conflict.fetch(:symbol))
  token_text = token ? token_label(token) : conflict.fetch(:symbol)
  type = conflict.fetch(:type).to_s.tr("_", "/")
  lines << "Conflict #{number}: state #{state.id}, #{type}, token #{token_text}"
  append_midrule_origins(lines, conflict)
  append_witness_steps(lines, state, conflict, example)
  append_interpretations(lines, example)
  if example.fetch(:inconclusive)
    search = example.fetch(:search)
    lines << "  Search exhausted after #{search.fetch(:explored)} configurations; classification is inconclusive."
  elsif !example.fetch(:unifying)
    lines << "  The search found no shared sentence within the configured budget; this witness is deterministic."
  end
  lines << ""
end

#append_interpretations(lines, example) ⇒ void

This method returns an undefined value.

RBS:

  • (Array[String] lines, LALR::search_counterexample example) -> void

Parameters:

  • lines (Array[String])
  • example (LALR::search_counterexample) 


326
327
328
329
330
331
332
 
# File 'lib/ibex/codegen/explain.rb', line 326

def append_interpretations(lines, example)
  lines << "  Competing derivations:"
  example.fetch(:interpretations).each_with_index do |interpretation, index|
    lines << "    #{index + 1}. #{interpretation.fetch(:kind)}"
    append_tree(lines, interpretation.fetch(:tree), "       ", "")
  end
end

#append_midrule_origins(lines, conflict) ⇒ void

This method returns an undefined value.

RBS:

  • (Array[String] lines, IR::conflict conflict) -> void

Parameters:

  • lines (Array[String])
  • conflict (IR::conflict) 


298
299
300
301
302
303
304
305
 
# File 'lib/ibex/codegen/explain.rb', line 298

def append_midrule_origins(lines, conflict)
  origins = conflict[:midrule_origins]
  return unless origins

  origins.each do |origin|
    lines << "  Midrule action origin: #{origin.fetch(:file)}:#{origin.fetch(:line)}:#{origin.fetch(:column)}"
  end
end

#append_tree(lines, tree, prefix, connector) ⇒ void

This method returns an undefined value.

RBS:

  • (Array[String] lines, explain_tree tree, String prefix, String connector) -> void

Parameters:

  • lines (Array[String])
  • tree (explain_tree)
  • prefix (String)
  • connector (String) 


342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
 
# File 'lib/ibex/codegen/explain.rb', line 342

def append_tree(lines, tree, prefix, connector)
  unless tree.is_a?(Hash)
    lines << "#{prefix}#{connector}#{display_name(tree.to_s)}"
    return
  end

  node = tree #: explain_tree_node
  name = node[:symbol] || node[:token]
  production = node[:production] ? " (production #{node[:production]})" : ""
  lines << "#{prefix}#{connector}#{display_name(name.to_s)}#{production}"
  children = node.fetch(:children, [])
  continuation = { "" => "", "|- " => "|  " }.fetch(connector, "   ")
  child_prefix = "#{prefix}#{continuation}"
  children.each_with_index do |child, index|
    branch = index == children.length - 1 ? "`- " : "|- "
    append_tree(lines, child, child_prefix, branch)
  end
end

#append_witness_steps(lines, state, conflict, example) ⇒ void

This method returns an undefined value.

RBS:

  • (Array[String] lines, IR::AutomatonState state, IR::conflict conflict, LALR::search_counterexample example) -> void

Parameters:

  • lines (Array[String])
  • state (IR::AutomatonState)
  • conflict (IR::conflict)
  • example (LALR::search_counterexample) 


309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
 
# File 'lib/ibex/codegen/explain.rb', line 309

def append_witness_steps(lines, state, conflict, example)
  lines << "  1. Reach state #{state.id} with the witness prefix."
  sentence = example.fetch(:sentence).map { |name| display_name(name) }
  sentence.insert(example.fetch(:lookahead_index), "•")
  kind = case witness_kind(example)
         when "unifying_counterexample" then "Unifying counterexample"
         when "inconclusive" then "Inconclusive reachability witness"
         else "Nonunifying reachability witness"
         end
  lines << "     #{kind}: #{sentence.join(' ')}"
  lines << "  2. The lookahead permits these competing actions:"
  conflict_alternatives(conflict).each { |alternative| lines << "     - #{alternative_text(alternative)}" }
  resolution = conflict.fetch(:resolution)
  lines << "  3. Resolution: #{resolution.fetch(:by)} chose #{resolution.fetch(:chose)}."
end

#conflict_alternatives(conflict) ⇒ Array[explain_alternative]

RBS:

  • (IR::conflict conflict) -> Array[explain_alternative]

Parameters:

  • conflict (IR::conflict)

Returns:

  • (Array[explain_alternative]) 


211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
 
# File 'lib/ibex/codegen/explain.rb', line 211

def conflict_alternatives(conflict)
  case conflict[:type]
  when :shift_reduce
    shift = { kind: "shift", state: conflict.fetch(:shift_to) } # @type var shift: explain_alternative
    reduce = { kind: "reduce", production: conflict.fetch(:reduce) } # @type var reduce: explain_alternative
    [shift, reduce]
  when :reduce_reduce
    reduce_reduce = conflict #: IR::reduce_reduce_conflict
    reduce_reduce[:reductions].map do |production|
      { kind: "reduce", production: production }
    end #: Array[explain_alternative]
  else
    []
  end
end

#conflict_document(entry) ⇒ Hash[Symbol, Object?]

RBS:

  • (explain_entry entry) -> Hash[Symbol, Object?]

Parameters:

  • entry (explain_entry)

Returns:

  • (Hash[Symbol, Object?]) 


169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
 
# File 'lib/ibex/codegen/explain.rb', line 169

def conflict_document(entry)
  state = entry.fetch(:state)
  conflict = entry.fetch(:conflict)
  example = entry.fetch(:example)
  document = {
    state: state.id,
    type: conflict.fetch(:type).to_s,
    token: symbol_reference(conflict.fetch(:symbol)),
    alternatives: conflict_alternatives(conflict),
    resolution: string_values(conflict.fetch(:resolution)),
    witness: {
      kind: witness_kind(example),
      sentence: example.fetch(:sentence).map { |name| symbol_reference(name) },
      lookahead_index: example.fetch(:lookahead_index),
      symbol_path: example.fetch(:symbol_path).map { |name| symbol_reference(name) },
      search: search_document(example.fetch(:search)),
      interpretations: example.fetch(:interpretations).map { |item| interpretation_document(item) }
    }
  } #: Hash[Symbol, Object?]
  document[:midrule_origins] = conflict[:midrule_origins] if conflict[:midrule_origins]
  document
end

#display_name(name) ⇒ String

RBS:

  • (String name) -> String

Parameters:

  • name (String)

Returns:

  • (String) 


372
373
374
375
376
 
# File 'lib/ibex/codegen/explain.rb', line 372

def display_name(name)
  grammar = @grammar #: IR::Grammar
  labels = @labels #: Hash[Integer, String]
  grammar.symbol(name)&.then { |symbol| labels.fetch(symbol.id, symbol.name) } || name
end

#interpretation_document(interpretation) ⇒ explain_interpretation

RBS:

  • (IR::interpretation interpretation) -> explain_interpretation

Parameters:

  • interpretation (IR::interpretation)

Returns:

  • (explain_interpretation) 


228
229
230
231
232
233
234
235
236
 
# File 'lib/ibex/codegen/explain.rb', line 228

def interpretation_document(interpretation)
  kind = interpretation.fetch(:kind) #: Symbol
  tree = interpretation.fetch(:tree) #: explain_tree
  value = { kind: kind.to_s,
            tree: tree_document(tree) } # @type var value: explain_interpretation
  value[:state] = interpretation[:state] if interpretation.key?(:state)
  value[:production] = interpretation[:production] if interpretation.key?(:production)
  value
end

#render_text ⇒ String

RBS:

  • () -> String

Returns:

  • (String) 


80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
 
# File 'lib/ibex/codegen/explain.rb', line 80

def render_text
  automaton = @automaton #: IR::Automaton
  entries = @entries #: Array[explain_entry]
  state_selector = @state_selector #: Integer?
  token_selector = @token_selector #: IR::GrammarSymbol?
  lines = [
    "Ibex conflict explanation v#{SCHEMA_VERSION}",
    "Algorithm: #{automaton.algorithm}",
    "State selector: #{state_selector || 'all'}",
    "Token selector: #{token_selector ? token_label(token_selector, query: @token_query) : 'all'}",
    "Search budget: #{@max_tokens} tokens, #{@max_configurations} configurations",
    "Matched conflicts: #{entries.length}",
    ""
  ]
  if entries.empty?
    lines << "No conflicts matched the selectors."
  else
    entries.each_with_index { |entry, index| append_conflict(lines, entry, index + 1) }
  end
  "#{lines.join("\n")}\n"
end

#resolve_token(query) ⇒ IR::GrammarSymbol?

RBS:

  • (String? query) -> IR::GrammarSymbol?

Parameters:

  • query (String, nil)

Returns:



105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
 
# File 'lib/ibex/codegen/explain.rb', line 105

def resolve_token(query)
  return unless query

  grammar = @grammar #: IR::Grammar
  canonical = grammar.terminals.find { |symbol| symbol.name == query }
  return canonical if canonical

  displayed = grammar.terminals.select { |symbol| symbol.display_name == query }
  return displayed.first if displayed.one?

  if displayed.length > 1
    names = displayed.map(&:name).sort.join(", ")
    raise Ibex::Error, "(cli):1:1: token display name #{query.inspect} is ambiguous; use one of: #{names}"
  end

  raise Ibex::Error,
        "(cli):1:1: unknown token #{query.inspect}; use a grammar token name or an exact display name"
end

#search_document(outcome) ⇒ explain_search

RBS:

  • (LALR::search_outcome outcome) -> explain_search

Parameters:

  • outcome (LALR::search_outcome)

Returns:

  • (explain_search) 


201
202
203
204
205
206
207
208
 
# File 'lib/ibex/codegen/explain.rb', line 201

def search_document(outcome)
  {
    status: outcome.fetch(:status).to_s,
    explored: outcome.fetch(:explored),
    exhausted: outcome.fetch(:exhausted),
    bounds: outcome.fetch(:bounds)
  }
end

#select_entries ⇒ Array[explain_entry]

RBS:

  • () -> Array[explain_entry]

Returns:

  • (Array[explain_entry]) 


135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
 
# File 'lib/ibex/codegen/explain.rb', line 135

def select_entries
  selections = selected_conflicts
  return [] if selections.empty?

  automaton = @automaton #: IR::Automaton
  counterexamples = LALR::Counterexample.new(
    automaton, max_tokens: @max_tokens, max_configurations: @max_configurations
  )
  selections.map do |selection|
    state = selection.fetch(:state)
    {
      state: state,
      conflict: selection.fetch(:conflict),
      example: counterexamples.for_conflict(state.id, selection.fetch(:conflict_index))
    }
  end
end

#selected_conflicts ⇒ Array[explain_selection]

RBS:

  • () -> Array[explain_selection]

Returns:

  • (Array[explain_selection]) 


154
155
156
157
158
159
160
161
162
163
164
165
166
 
# File 'lib/ibex/codegen/explain.rb', line 154

def selected_conflicts
  automaton = @automaton #: IR::Automaton
  state_selector = @state_selector #: Integer?
  token_selector = @token_selector #: IR::GrammarSymbol?
  automaton.states.flat_map do |state|
    state.conflicts.each_with_index.filter_map do |conflict, conflict_index|
      next if state_selector && state.id != state_selector
      next if token_selector && conflict[:symbol] != token_selector.name

      { state: state, conflict: conflict, conflict_index: conflict_index }
    end
  end
end

#string_values(value) ⇒ Hash[Symbol, string_value]

RBS:

  • (Hash[Symbol, string_value] value) -> Hash[Symbol, string_value]

Parameters:

  • value (Hash[Symbol, string_value])

Returns:

  • (Hash[Symbol, string_value]) 


252
253
254
255
 
# File 'lib/ibex/codegen/explain.rb', line 252

def string_values(value)
  values = value #: Hash[Symbol, string_value]
  values.transform_values { |item| item.is_a?(Symbol) ? item.to_s : item }
end

#symbol_reference(name) ⇒ explain_token

RBS:

  • (String name) -> explain_token

Parameters:

  • name (String)

Returns:

  • (explain_token) 


258
259
260
261
262
263
264
 
# File 'lib/ibex/codegen/explain.rb', line 258

def symbol_reference(name)
  grammar = @grammar #: IR::Grammar
  symbol = grammar.symbol(name)
  return { name: name, display_name: nil, label: name } unless symbol

  token_reference(symbol)
end

#to_h ⇒ Hash[Symbol, Object?]

RBS:

  • () -> Hash[Symbol, Object?]

Returns:

  • (Hash[Symbol, Object?]) 


55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
 
# File 'lib/ibex/codegen/explain.rb', line 55

def to_h
  entries = @entries #: Array[explain_entry]
  automaton = @automaton #: IR::Automaton
  unifying = entries.count { |entry| entry.fetch(:example).fetch(:unifying) }
  inconclusive = entries.count { |entry| entry.fetch(:example).fetch(:inconclusive) }
  {
    ibex_explain: "conflicts",
    schema_version: SCHEMA_VERSION,
    algorithm: automaton.algorithm,
    selectors: {
      state: @state_selector,
      token: @token_selector && token_reference(@token_selector, query: @token_query)
    },
    search: { max_tokens: @max_tokens, max_configurations: @max_configurations },
    summary: {
      matched_conflicts: entries.length,
      unifying_counterexamples: unifying,
      nonunifying_witnesses: entries.length - unifying - inconclusive,
      inconclusive_searches: inconclusive
    },
    conflicts: entries.map { |entry| conflict_document(entry) }
  }
end

#token_label(symbol, query: nil) ⇒ String

RBS:

  • (IR::GrammarSymbol symbol, ?query: String?) -> String

Parameters:

Returns:

  • (String) 


362
363
364
365
366
367
368
369
 
# File 'lib/ibex/codegen/explain.rb', line 362

def token_label(symbol, query: nil)
  label = if symbol.display_name && symbol.display_name != symbol.name
            "#{symbol.name} (display #{symbol.display_name.inspect})"
          else
            symbol.name
          end
  query && query != symbol.name ? "#{label}, selected by #{query.inspect}" : label
end

#token_reference(symbol, query: nil) ⇒ explain_token

RBS:

  • (IR::GrammarSymbol symbol, ?query: String?) -> explain_token

Parameters:

Returns:

  • (explain_token) 


267
268
269
270
271
272
273
 
# File 'lib/ibex/codegen/explain.rb', line 267

def token_reference(symbol, query: nil)
  labels = @labels #: Hash[Integer, String]
  value = { name: symbol.name, display_name: symbol.display_name,
            label: labels.fetch(symbol.id, symbol.name) } # @type var value: explain_token
  value[:query] = query if query
  value
end

#tree_document(tree) ⇒ explain_tree

RBS:

  • (explain_tree tree) -> explain_tree

Parameters:

  • tree (explain_tree)

Returns:

  • (explain_tree) 


239
240
241
242
243
244
245
246
247
248
249
 
# File 'lib/ibex/codegen/explain.rb', line 239

def tree_document(tree)
  return symbol_reference(tree.to_s) unless tree.is_a?(Hash)

  node = tree #: explain_tree_node
  value = {} # @type var value: explain_tree_node
  value[:symbol] = symbol_reference(node[:symbol].to_s) if node[:symbol]
  value[:token] = symbol_reference(node[:token].to_s) if node[:token]
  value[:production] = node[:production] if node[:production]
  value[:children] = node[:children].map { |child| tree_document(child) } if node[:children]
  value
end

#validate_state! ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



125
126
127
128
129
130
131
132
 
# File 'lib/ibex/codegen/explain.rb', line 125

def validate_state!
  state_selector = @state_selector #: Integer?
  automaton = @automaton #: IR::Automaton
  return unless state_selector
  return if state_selector >= 0 && automaton.states.any? { |state| state.id == state_selector }

  raise Ibex::Error, "(cli):1:1: unknown automaton state #{state_selector}"
end

#witness_kind(example) ⇒ String

RBS:

  • (LALR::search_counterexample example) -> String

Parameters:

  • example (LALR::search_counterexample)

Returns:

  • (String) 


193
194
195
196
197
198
 
# File 'lib/ibex/codegen/explain.rb', line 193

def witness_kind(example)
  return "unifying_counterexample" if example.fetch(:unifying)
  return "inconclusive" if example.fetch(:inconclusive)

  "nonunifying_witness"
end