Class: Ibex::Verify::LanguageWitness

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

Overview

Compares canonical and submitted parser acceptance over a bounded set of terminal sequences. This is a semantic witness, not a proof of language equivalence: the reference collection is complete within its budgets and the token enumeration is deliberately finite.

Defined Under Namespace

Classes: CanonicalMachine, Difference, Machine, Result

Instance Method Summary collapse

Constructor Details

#initialize(grammar, target, max_tokens: 6, max_cases: 10_000, max_states: 100_000, max_items: 1_000_000) ⇒ LanguageWitness

Returns a new instance of LanguageWitness.

Raises:

  • (ArgumentError) 


61
62
63
64
65
66
67
68
69
70
71
72
73
 
# File 'lib/ibex/verify/language_witness.rb', line 61

def initialize(grammar, target, max_tokens: 6, max_cases: 10_000, max_states: 100_000,
               max_items: 1_000_000)
  raise ArgumentError, "max_tokens must be nonnegative" if max_tokens.negative?
  raise ArgumentError, "max_cases must be positive" unless max_cases.positive?

  @grammar = grammar
  @target = target
  @max_tokens = max_tokens
  @max_cases = max_cases
  @canonical = CanonicalMachine.new(
    grammar, max_states: max_states, max_items: max_items
  )
end

Instance Method Details

#verify ⇒ Object 



76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
 
# File 'lib/ibex/verify/language_witness.rb', line 76

def verify
  differences = [] #: Array[Difference]
  explored = 0
  truncated = false
  token_ids = input_tokens.map(&:id)

  @grammar.starts.each do |entry|
    explored, truncated = verify_entry(entry, token_ids, differences, explored)
    break if truncated
  end

  Result.new(
    differences: differences.freeze, explored: explored, truncated: truncated,
    max_tokens: @max_tokens, max_cases: @max_cases
  )
end