Add types to counterexamples

Steepfile

@@ -7,11 +7,14 @@ target :lib do
   signature "sig"
 
   check "lib/lrama/grammar"
+
+  check "lib/lrama/counterexamples"
   check "lib/lrama/lexer"
   check "lib/lrama/report"
   check "lib/lrama/state"
   check "lib/lrama/states"
   check "lib/lrama/bitmap.rb"
+  check "lib/lrama/counterexamples.rb"
   check "lib/lrama/digraph.rb"
   check "lib/lrama/grammar.rb"
   check "lib/lrama/options.rb"

lib/lrama/counterexamples.rb

@@ -32,8 +32,10 @@ def compute(conflict_state)
       conflict_state.conflicts.flat_map do |conflict|
         case conflict.type
         when :shift_reduce
+          # @type var conflict: State::ShiftReduceConflict
           shift_reduce_example(conflict_state, conflict)
         when :reduce_reduce
+          # @type var conflict: State::ReduceReduceConflict
           reduce_reduce_examples(conflict_state, conflict)
         end
       end.compact
@@ -66,6 +68,7 @@ def setup_transitions
 
             @transitions[[src_state_item, sym]] = dest_state_item
 
+            # @type var key: [StateItem, Grammar::Symbol]
             key = [dest_state_item, sym]
             @reverse_transitions[key] ||= Set.new
             @reverse_transitions[key] << src_state_item
@@ -97,6 +100,7 @@ def setup_productions
 
           sym = item.next_sym
           state_item = StateItem.new(state, item)
+          # @type var key: [State, Grammar::Symbol]
           key = [state, sym]
 
           @productions[state_item] = h[sym]
@@ -109,6 +113,7 @@ def setup_productions
 
     def shift_reduce_example(conflict_state, conflict)
       conflict_symbol = conflict.symbols.first
+      # @type var shift_conflict_item: ::Lrama::States::Item
       shift_conflict_item = conflict_state.items.find { |item| item.next_sym == conflict_symbol }
       path2 = shortest_path(conflict_state, conflict.reduce.item, conflict_symbol)
       path1 = find_shift_conflict_shortest_path(path2, conflict_state, shift_conflict_item)
@@ -153,7 +158,9 @@ def find_shift_conflict_shortest_state_items(reduce_path, conflict_state, confli
         prev_state_item = prev_path&.to
 
         if target_state_item == state_item || target_state_item.item.start_item?
-          result.concat(reversed_reduce_path[_j..-1].map(&:to))
+          result.concat(
+            reversed_reduce_path[_j..-1] #: Array[StartPath|TransitionPath|ProductionPath]
+              .map(&:to))
           break
         end
 
@@ -174,15 +181,17 @@ def find_shift_conflict_shortest_state_items(reduce_path, conflict_state, confli
             end
 
             if si.item.beginning_of_rule?
+              # @type var key: [State, Grammar::Symbol]
               key = [si.state, si.item.lhs]
               @reverse_productions[key].each do |item|
                 state_item = StateItem.new(si.state, item)
                 queue << (sis + [state_item])
               end
             else
+              # @type var key: [StateItem, Grammar::Symbol]
               key = [si, si.item.previous_sym]
               @reverse_transitions[key].each do |prev_target_state_item|
-                next if prev_target_state_item.state != prev_state_item.state
+                next if prev_target_state_item.state != prev_state_item&.state
                 sis.shift
                 result.concat(sis)
                 result << prev_target_state_item
@@ -195,9 +204,10 @@ def find_shift_conflict_shortest_state_items(reduce_path, conflict_state, confli
           end
         else
           # Find reverse transition
+          # @type var key: [StateItem, Grammar::Symbol]
           key = [target_state_item, target_state_item.item.previous_sym]
           @reverse_transitions[key].each do |prev_target_state_item|
-            next if prev_target_state_item.state != prev_state_item.state
+            next if prev_target_state_item.state != prev_state_item&.state
             result << prev_target_state_item
             target_state_item = prev_target_state_item
             i = j
@@ -226,7 +236,7 @@ def shortest_path(conflict_state, conflict_reduce_item, conflict_term)
       # queue: is an array of [Triple, [Path]]
       queue = []
       visited = {}
-      start_state = @states.states.first
+      start_state = @states.states.first #: Lrama::State
       raise "BUG: Start state should be just one kernel." if start_state.kernels.count != 1
 
       start = Triple.new(start_state, start_state.kernels.first, Set.new([@states.eof_symbol]))

lib/lrama/counterexamples/derivation.rb

@@ -51,11 +51,12 @@ def _render_for_report(derivation, offset, strings, index)
         end
 
         if derivation.right&.left
-          length = _render_for_report(derivation.right.left, str.length, strings, index + 1)
-          str << "#{item.symbols_after_dot[1..-1].map(&:display_name).join(" ")} "
+          left = derivation.right&.left #: Derivation
+          length = _render_for_report(left, str.length, strings, index + 1)
+          str << "#{item.symbols_after_dot[1..-1].map(&:display_name).join(" ")} " # steep:ignore
           str << " " * (length - str.length) if length > str.length
         elsif item.next_next_sym
-          str << "#{item.symbols_after_dot[1..-1].map(&:display_name).join(" ")} "
+          str << "#{item.symbols_after_dot[1..-1].map(&:display_name).join(" ")} " # steep:ignore
         end
 
         return str.length

lib/lrama/counterexamples/example.rb

@@ -38,9 +38,10 @@ def derivations2
       private
 
       def _derivations(paths)
-        derivation = nil
+        derivation = nil #: Derivation?
         current = :production
-        lookahead_sym = paths.last.to.item.end_of_rule? ? @conflict_symbol : nil
+        last_path = paths.last #: Path
+        lookahead_sym = last_path.to.item.end_of_rule? ? @conflict_symbol : nil
 
         paths.reverse_each do |path|
           item = path.to.item
@@ -57,12 +58,14 @@ def _derivations(paths)
             when ProductionPath
               derivation = Derivation.new(item, derivation)
               current = :production
+            else
+              return nil
             end
 
             if lookahead_sym && item.next_next_sym && item.next_next_sym.first_set.include?(lookahead_sym)
               state_item = @counterexamples.transitions[[path.to, item.next_sym]]
               derivation2 = find_derivation_for_symbol(state_item, lookahead_sym)
-              derivation.right = derivation2
+              derivation.right = derivation2 # steep:ignore
               lookahead_sym = nil
             end
 

lib/lrama/counterexamples/path.rb

@@ -20,6 +20,10 @@ def to_s
         "#<Path(#{type})>"
       end
       alias :inspect :to_s
+
+      def type
+        raise NoMethodError
+      end
     end
   end
 end

rbs_collection.lock.yaml

@@ -1,6 +1,14 @@
 ---
 path: ".gem_rbs_collection"
 gems:
+- name: diff-lcs
+  version: '1.5'
+  source:
+    type: git
+    name: ruby/gem_rbs_collection
+    revision: 218cf130d31f63e110e350efc3fa265311b0f238
+    remote: https://github.com/ruby/gem_rbs_collection.git
+    repo_dir: gems
 - name: erb
   version: '0'
   source:

sig/lrama/counterexamples.rbs

@@ -0,0 +1,29 @@
+module Lrama
+  class Counterexamples
+    @states: States
+    @transitions: Hash[[StateItem, Grammar::Symbol], StateItem]
+    @reverse_transitions: Hash[[StateItem, Grammar::Symbol], Set[StateItem]]
+    @productions: Hash[StateItem, Set[States::Item]]
+    @reverse_productions: Hash[[State, Grammar::Symbol], Set[States::Item]]
+
+    attr_reader transitions: Hash[[StateItem, Grammar::Symbol], StateItem]
+    attr_reader productions: Hash[StateItem, Set[States::Item]]
+
+    def initialize: (States states) -> void
+    def to_s: () -> "#<Counterexamples>"
+    alias inspect to_s
+    def compute: (State conflict_state) -> Array[Example]
+
+    private
+
+    def setup_transitions: () -> void
+    def setup_productions: () -> void
+    def shift_reduce_example: (State conflict_state, State::ShiftReduceConflict conflict) -> Example
+    def reduce_reduce_examples: (State conflict_state, State::ReduceReduceConflict conflict) -> Example
+    def find_shift_conflict_shortest_path: (::Array[StartPath|TransitionPath|ProductionPath]? reduce_path, State conflict_state, States::Item conflict_item) -> ::Array[StartPath|TransitionPath|ProductionPath]
+    def find_shift_conflict_shortest_state_items: (::Array[StartPath|TransitionPath|ProductionPath]? reduce_path, State conflict_state, States::Item conflict_item) -> Array[StateItem]
+    def build_paths_from_state_items: (Array[StateItem] state_items) -> ::Array[StartPath|TransitionPath|ProductionPath]
+    def shortest_path: (State conflict_state, States::Item conflict_reduce_item, Grammar::Symbol conflict_term) -> ::Array[StartPath|TransitionPath|ProductionPath]?
+    def follow_l: (States::Item item, Set[Grammar::Symbol] current_l) -> Set[Grammar::Symbol]
+  end
+end

sig/lrama/counterexamples/derivation.rbs

@@ -0,0 +1,33 @@
+module Lrama
+  class Counterexamples
+    class Derivation
+      @item: States::Item
+
+      @left: Derivation?
+
+      @right: Derivation?
+
+      attr_reader item: States::Item
+
+      attr_reader left: Derivation?
+
+      attr_reader right: Derivation?
+
+      attr_writer right: Derivation?
+
+      def initialize: (States::Item item, Derivation? left, ?Derivation? right) -> void
+
+      def to_s: () -> ::String
+
+      alias inspect to_s
+
+      def render_strings_for_report: () -> Array[String]
+
+      def render_for_report: () -> String
+
+      private
+
+      def _render_for_report: (Derivation derivation, Integer offset, Array[String] strings, Integer index) -> Integer
+    end
+  end
+end

sig/lrama/counterexamples/example.rbs

@@ -0,0 +1,45 @@
+module Lrama
+  class Counterexamples
+    class Example
+      @path1: ::Array[StartPath | TransitionPath | ProductionPath]
+
+      @path2: ::Array[StartPath | TransitionPath | ProductionPath]
+
+      @conflict: (State::ShiftReduceConflict | State::ReduceReduceConflict)
+
+      @conflict_symbol: Grammar::Symbol
+
+      @counterexamples: Counterexamples
+
+      @derivations1: Derivation
+
+      @derivations2: Derivation
+
+      attr_reader path1: ::Array[StartPath | TransitionPath | ProductionPath]
+
+      attr_reader path2: ::Array[StartPath | TransitionPath | ProductionPath]
+
+      attr_reader conflict: (State::ShiftReduceConflict | State::ReduceReduceConflict)
+
+      attr_reader conflict_symbol: Grammar::Symbol
+
+      def initialize: (::Array[StartPath | TransitionPath | ProductionPath]? path1, ::Array[StartPath | TransitionPath | ProductionPath]? path2, (State::ShiftReduceConflict | State::ReduceReduceConflict) conflict, Grammar::Symbol conflict_symbol, Counterexamples counterexamples) -> void
+
+      def type: () -> (:shift_reduce | :reduce_reduce)
+
+      def path1_item: () -> States::Item
+
+      def path2_item: () -> States::Item
+
+      def derivations1: () -> Derivation?
+
+      def derivations2: () -> Derivation?
+
+      private
+
+      def _derivations: (::Array[StartPath | TransitionPath | ProductionPath] paths) -> Derivation?
+
+      def find_derivation_for_symbol: (StateItem state_item, Grammar::Symbol sym) -> Derivation?
+    end
+  end
+end

sig/lrama/counterexamples/path.rbs

@@ -0,0 +1,21 @@
+module Lrama
+  class Counterexamples
+    class Path
+      @from_state_item: StateItem?
+
+      @to_state_item: StateItem
+
+      def initialize: (StateItem? from_state_item, StateItem to_state_item) -> void
+
+      def from: () -> StateItem?
+
+      def to: () -> StateItem
+
+      def to_s: () -> ::String
+
+      alias inspect to_s
+
+      def type: -> bot
+    end
+  end
+end

sig/lrama/counterexamples/production_path.rbs

@@ -0,0 +1,11 @@
+module Lrama
+  class Counterexamples
+    class ProductionPath < Path
+      def type: () -> :production
+
+      def transition?: () -> false
+
+      def production?: () -> true
+    end
+  end
+end

sig/lrama/counterexamples/start_path.rbs

@@ -0,0 +1,13 @@
+module Lrama
+  class Counterexamples
+    class StartPath < Path
+      def initialize: (StateItem to_state_item) -> void
+
+      def type: () -> :start
+
+      def transition?: () -> false
+
+      def production?: () -> false
+    end
+  end
+end

sig/lrama/counterexamples/state_item.rbs

@@ -0,0 +1,10 @@
+module Lrama
+  class Counterexamples
+    class StateItem
+     attr_accessor state: State
+     attr_accessor item: States::Item
+
+      def initialize: (State state, States::Item item) -> void
+    end
+  end
+end

sig/lrama/counterexamples/transition_path.rbs

@@ -0,0 +1,11 @@
+module Lrama
+  class Counterexamples
+    class TransitionPath < Path
+      def type: () -> :transition
+
+      def transition?: () -> true
+
+      def production?: () -> false
+    end
+  end
+end

sig/lrama/counterexamples/triple.rbs

@@ -0,0 +1,20 @@
+module Lrama
+  class Counterexamples
+    class Triple
+      attr_accessor s: State
+      attr_accessor itm: States::Item
+      attr_accessor l: Set[Grammar::Symbol]
+
+      alias state s
+      alias item itm
+      alias precise_lookahead_set l
+
+      def initialize: (State s, States::Item itm, Set[Grammar::Symbol] l) -> void
+
+      def state_item: () -> StateItem
+      def inspect: () -> ::String
+
+      alias to_s inspect
+    end
+  end
+end

sig/lrama/grammar.rbs

@@ -91,5 +91,18 @@ module Lrama
     def fill_sym_to_rules: () -> Array[Rule]
     def validate_rule_lhs_is_nterm!: () -> void
     def set_locations: () -> void
+
+    interface _DelegatedMethods
+    def rules: () -> Array[Rule]
+    def accept_symbol: () -> Grammar::Symbol
+    def eof_symbol: () -> Grammar::Symbol
+    def undef_symbol: () -> Grammar::Symbol
+
+    # delegate to @symbols_resolver
+    def symbols: () -> Array[Grammar::Symbol]
+    def terms: () -> Array[Grammar::Symbol]
+    def nterms: () -> Array[Grammar::Symbol]
+    def find_symbol_by_s_value!: (Grammar::Symbol s_value) -> Grammar::Symbol
+    end
   end
 end