Class: Ibex::Verify::LanguageWitness::CanonicalMachine

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

Overview

Canonical collection is intentionally built here rather than through the production construction entry point, keeping this witness independent from construction code.

Instance Method Summary collapse

Constructor Details

#initialize(grammar, max_states:, max_items:) ⇒ CanonicalMachine

Returns a new instance of CanonicalMachine.

RBS:

  • (IR::Grammar grammar, max_states: Integer, max_items: Integer) -> void

Parameters:

  • grammar (IR::Grammar)
  • max_states: (Integer)
  • max_items: (Integer) 


145
146
147
148
149
150
151
152
 
# File 'lib/ibex/verify/language_witness.rb', line 145

def initialize(grammar, max_states:, max_items:)
  collection = ReferenceCollection.new(
    grammar, max_states: max_states, max_items: max_items
  ).build(:lr1)
  @grammar = grammar
  @states = build_states(collection)
  @entry_states = grammar.starts.each_with_index.to_h
end

Instance Method Details

#build_state(collection, raw_items, state_id) ⇒ IR::AutomatonState

RBS:

  • (ReferenceCollection::Collection, Set[Array[Integer]], Integer) -> IR::AutomatonState

Parameters:

Returns:



172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
 
# File 'lib/ibex/verify/language_witness.rb', line 172

def build_state(collection, raw_items, state_id)
  item_map = Hash.new { |hash, key| hash[key] = Set.new } #: Hash[[Integer, Integer], Set[Integer]]
  raw_items.each do |raw_item|
    production = raw_item.fetch(0) #: Integer
    dot = raw_item.fetch(1) #: Integer
    lookahead = raw_item.fetch(2) #: Integer
    item_map[[production, dot]] << lookahead
  end
  items = item_map.sort.map do |(production, dot), lookaheads|
    IR::AutomatonItem.new(production: production, dot: dot, lookaheads: lookaheads.to_a)
  end
  transitions = collection.transitions.fetch(state_id)
  actions = resolve_actions(items, transitions)
  gotos = {} #: Hash[Integer, Integer]
  transitions.each do |symbol_id, target|
    gotos[symbol_id] = target if @grammar.symbol_by_id(symbol_id)&.nonterminal?
  end
  IR::AutomatonState.new(
    id: state_id, items: items, transitions: transitions,
    actions: actions, gotos: gotos
  )
end

#build_states(collection) ⇒ Array[IR::AutomatonState]

RBS:

  • (ReferenceCollection::Collection) -> Array[IR::AutomatonState]

Parameters:

Returns:



163
164
165
166
167
168
169
 
# File 'lib/ibex/verify/language_witness.rb', line 163

def build_states(collection)
  states = collection.states.each_with_index.map do |raw_items, state_id|
    build_state(collection, raw_items, state_id)
  end
  states = LALR::OnErrorReductions.apply(@grammar, states)
  LALR::DefaultReductions.apply(states, terminal_ids: @grammar.terminals.map(&:id))
end

#completed_candidates(items, candidates) ⇒ void

This method returns an undefined value.

RBS:

  • (Array[IR::AutomatonItem], Hash[Integer, Array[IR::parser_action]]) -> void

Parameters:



218
219
220
221
222
223
224
225
226
227
228
229
 
# File 'lib/ibex/verify/language_witness.rb', line 218

def completed_candidates(items, candidates)
  items.each do |item|
    next unless item.dot == rhs_for(item.production).length

    action = if item.production.negative?
               { type: :accept } #: IR::accept_action
             else
               { type: :reduce, production: item.production } #: IR::reduce_action
             end
    item.lookaheads.each { |lookahead| candidates[lookahead] << action }
  end
end

#resolve_actions(items, transitions) ⇒ Hash[Integer, IR::parser_action]

RBS:

  • (Array[IR::AutomatonItem], Hash[Integer, Integer]) -> Hash[Integer, IR::parser_action]

Parameters:

Returns:

  • (Hash[Integer, IR::parser_action]) 


196
197
198
199
200
201
202
203
204
 
# File 'lib/ibex/verify/language_witness.rb', line 196

def resolve_actions(items, transitions)
  candidates = transition_candidates(transitions)
  completed_candidates(items, candidates)
  resolver = LALR::ConflictResolver.new(@grammar)
  candidates.keys.sort.to_h do |token_id|
    action, = resolver.resolve(token_id, candidates.fetch(token_id))
    [token_id, action || { type: :error }]
  end
end

#rhs_for(production_id) ⇒ Array[Integer]

RBS:

  • (Integer production_id) -> Array[Integer]

Parameters:

  • production_id (Integer)

Returns:

  • (Array[Integer]) 


232
233
234
235
236
237
 
# File 'lib/ibex/verify/language_witness.rb', line 232

def rhs_for(production_id)
  return [@grammar.symbol(@grammar.starts.fetch(-production_id - 1)).id] if
    production_id.negative?

  @grammar.productions.fetch(production_id).rhs
end

#simulate(entry, tokens) ⇒ witness_status

RBS:

  • (String entry, Array[Integer]) -> witness_status

Parameters:

  • entry (String)
  • (Array[Integer])

Returns:

  • (witness_status) 


155
156
157
158
 
# File 'lib/ibex/verify/language_witness.rb', line 155

def simulate(entry, tokens)
  state = @entry_states.fetch(entry)
  Machine.new(@states, @grammar).simulate(state, tokens)
end

#transition_candidates(transitions) ⇒ Hash[Integer, Array[IR::parser_action]]

RBS:

  • (Hash[Integer, Integer]) -> Hash[Integer, Array[IR::parser_action]]

Parameters:

  • (Hash[Integer, Integer])

Returns:

  • (Hash[Integer, Array[IR::parser_action]]) 


207
208
209
210
211
212
213
214
215
 
# File 'lib/ibex/verify/language_witness.rb', line 207

def transition_candidates(transitions)
  candidates = Hash.new { |hash, key| hash[key] = [] } #: Hash[Integer, Array[IR::parser_action]]
  transitions.each do |symbol_id, target|
    next unless @grammar.symbol_by_id(symbol_id)&.terminal?

    candidates[symbol_id] << { type: :shift, state: target }
  end
  candidates
end