From 664dcb9f91e4c9948d2bf07a77c031612b5d3246 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Wed, 12 Jun 2024 09:16:05 +0900
Subject: [PATCH 01/18] generated rbs by prototype

---
 sig/lrama/counterexamples.rbs                 |  29 ++++
 sig/lrama/counterexamples/derivation.rbs      |  33 ++++
 sig/lrama/counterexamples/example.rbs         |  47 ++++++
 sig/lrama/counterexamples/path.rbs            |  19 +++
 sig/lrama/counterexamples/production_path.rbs |  11 ++
 sig/lrama/counterexamples/start_path.rbs      |  13 ++
 sig/lrama/counterexamples/state_item.rbs      |  10 ++
 sig/lrama/counterexamples/transition_path.rbs |  11 ++
 sig/lrama/counterexamples/triple.rbs          |  20 +++
 sig/lrama/states.rbs                          | 141 ++++++++++++++++++
 10 files changed, 334 insertions(+)
 create mode 100644 sig/lrama/counterexamples.rbs
 create mode 100644 sig/lrama/counterexamples/derivation.rbs
 create mode 100644 sig/lrama/counterexamples/example.rbs
 create mode 100644 sig/lrama/counterexamples/path.rbs
 create mode 100644 sig/lrama/counterexamples/production_path.rbs
 create mode 100644 sig/lrama/counterexamples/start_path.rbs
 create mode 100644 sig/lrama/counterexamples/state_item.rbs
 create mode 100644 sig/lrama/counterexamples/transition_path.rbs
 create mode 100644 sig/lrama/counterexamples/triple.rbs
 create mode 100644 sig/lrama/states.rbs

diff --git a/sig/lrama/counterexamples.rbs b/sig/lrama/counterexamples.rbs
new file mode 100644
index 00000000..3afd894f
--- /dev/null
+++ b/sig/lrama/counterexamples.rbs
@@ -0,0 +1,29 @@
+module Lrama
+  class Counterexamples
+    @states: untyped
+    @transitions: untyped
+    @reverse_transitions: untyped
+    @productions: untyped
+    @reverse_productions: untyped
+
+    attr_reader transitions: untyped
+    attr_reader productions: untyped
+
+    def initialize: (untyped states) -> void
+    def to_s: () -> "#<Counterexamples>"
+    alias inspect to_s
+    def compute: (untyped conflict_state) -> untyped
+
+    private
+
+    def setup_transitions: () -> untyped
+    def setup_productions: () -> untyped
+    def shift_reduce_example: (untyped conflict_state, untyped conflict) -> untyped
+    def reduce_reduce_examples: (untyped conflict_state, untyped conflict) -> untyped
+    def find_shift_conflict_shortest_path: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
+    def find_shift_conflict_shortest_state_items: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
+    def build_paths_from_state_items: (untyped state_items) -> untyped
+    def shortest_path: (untyped conflict_state, untyped conflict_reduce_item, untyped conflict_term) -> (untyped | nil)
+    def follow_l: (untyped item, untyped current_l) -> untyped
+  end
+end
diff --git a/sig/lrama/counterexamples/derivation.rbs b/sig/lrama/counterexamples/derivation.rbs
new file mode 100644
index 00000000..f5fbc427
--- /dev/null
+++ b/sig/lrama/counterexamples/derivation.rbs
@@ -0,0 +1,33 @@
+module Lrama
+  class Counterexamples
+    class Derivation
+      @item: untyped
+
+      @left: untyped
+
+      @right: untyped
+
+      attr_reader item: untyped
+
+      attr_reader left: untyped
+
+      attr_reader right: untyped
+
+      attr_writer right: untyped
+
+      def initialize: (untyped item, untyped left, ?untyped? right) -> void
+
+      def to_s: () -> ::String
+
+      alias inspect to_s
+
+      def render_strings_for_report: () -> untyped
+
+      def render_for_report: () -> untyped
+
+      private
+
+      def _render_for_report: (untyped derivation, untyped offset, untyped strings, untyped index) -> untyped
+    end
+  end
+end
diff --git a/sig/lrama/counterexamples/example.rbs b/sig/lrama/counterexamples/example.rbs
new file mode 100644
index 00000000..6089724e
--- /dev/null
+++ b/sig/lrama/counterexamples/example.rbs
@@ -0,0 +1,47 @@
+module Lrama
+  class Counterexamples
+    class Example
+      @path1: untyped
+
+      @path2: untyped
+
+      @conflict: untyped
+
+      @conflict_symbol: untyped
+
+      @counterexamples: untyped
+
+      @derivations1: untyped
+
+      @derivations2: untyped
+
+      attr_reader path1: untyped
+
+      attr_reader path2: untyped
+
+      attr_reader conflict: untyped
+
+      attr_reader conflict_symbol: untyped
+
+      # path1 is shift conflict when S/R conflict
+      # path2 is always reduce conflict
+      def initialize: (untyped path1, untyped path2, untyped conflict, untyped conflict_symbol, untyped counterexamples) -> void
+
+      def type: () -> untyped
+
+      def path1_item: () -> untyped
+
+      def path2_item: () -> untyped
+
+      def derivations1: () -> untyped
+
+      def derivations2: () -> untyped
+
+      private
+
+      def _derivations: (untyped paths) -> untyped
+
+      def find_derivation_for_symbol: (untyped state_item, untyped sym) -> untyped
+    end
+  end
+end
diff --git a/sig/lrama/counterexamples/path.rbs b/sig/lrama/counterexamples/path.rbs
new file mode 100644
index 00000000..ea644650
--- /dev/null
+++ b/sig/lrama/counterexamples/path.rbs
@@ -0,0 +1,19 @@
+module Lrama
+  class Counterexamples
+    class Path
+      @from_state_item: untyped
+
+      @to_state_item: untyped
+
+      def initialize: (untyped? from_state_item, untyped to_state_item) -> void
+
+      def from: () -> untyped
+
+      def to: () -> untyped
+
+      def to_s: () -> ::String
+
+      alias inspect to_s
+    end
+  end
+end
diff --git a/sig/lrama/counterexamples/production_path.rbs b/sig/lrama/counterexamples/production_path.rbs
new file mode 100644
index 00000000..777d0804
--- /dev/null
+++ b/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
diff --git a/sig/lrama/counterexamples/start_path.rbs b/sig/lrama/counterexamples/start_path.rbs
new file mode 100644
index 00000000..a53bd144
--- /dev/null
+++ b/sig/lrama/counterexamples/start_path.rbs
@@ -0,0 +1,13 @@
+module Lrama
+  class Counterexamples
+    class StartPath < Path
+      def initialize: (untyped to_state_item) -> void
+
+      def type: () -> :start
+
+      def transition?: () -> false
+
+      def production?: () -> false
+    end
+  end
+end
diff --git a/sig/lrama/counterexamples/state_item.rbs b/sig/lrama/counterexamples/state_item.rbs
new file mode 100644
index 00000000..f32d50de
--- /dev/null
+++ b/sig/lrama/counterexamples/state_item.rbs
@@ -0,0 +1,10 @@
+module Lrama
+  class Counterexamples
+    class StateItem
+     attr_accessor state: untyped
+     attr_accessor item: untyped
+
+      def initialize: (untyped state, untyped item) -> untyped
+    end
+  end
+end
diff --git a/sig/lrama/counterexamples/transition_path.rbs b/sig/lrama/counterexamples/transition_path.rbs
new file mode 100644
index 00000000..7dd9397d
--- /dev/null
+++ b/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
diff --git a/sig/lrama/counterexamples/triple.rbs b/sig/lrama/counterexamples/triple.rbs
new file mode 100644
index 00000000..8e16898a
--- /dev/null
+++ b/sig/lrama/counterexamples/triple.rbs
@@ -0,0 +1,20 @@
+module Lrama
+  class Counterexamples
+    class Triple
+      attr_accessor s: untyped
+      attr_accessor itm: untyped
+      attr_accessor l: untyped
+
+      alias state s
+      alias item itm
+      alias precise_lookahead_set l
+
+      def initialize: (untyped s, untyped itm, untyped l) -> void
+
+      def state_item: () -> untyped
+      def inspect: () -> ::String
+
+      alias to_s inspect
+    end
+  end
+end
diff --git a/sig/lrama/states.rbs b/sig/lrama/states.rbs
new file mode 100644
index 00000000..b48d5eb6
--- /dev/null
+++ b/sig/lrama/states.rbs
@@ -0,0 +1,141 @@
+module Lrama
+  # States is passed to a template file
+  #
+  # "Efficient Computation of LALR(1) Look-Ahead Sets"
+  #   https://dl.acm.org/doi/pdf/10.1145/69622.357187
+  class States
+    @grammar: untyped
+
+    @warning: untyped
+
+    @trace_state: untyped
+
+    @states: untyped
+
+    # `DR(p, A) = {t ∈ T | p -(A)-> r -(t)-> }`
+    #   where p is state, A is nterm, t is term.
+    #
+    # `@direct_read_sets` is a hash whose
+    # key is [state.id, nterm.token_id],
+    # value is bitmap of term.
+    @direct_read_sets: untyped
+
+    # Reads relation on nonterminal transitions (pair of state and nterm)
+    # `(p, A) reads (r, C) iff p -(A)-> r -(C)-> and C =>* ε`
+    #   where p, r are state, A, C are nterm.
+    #
+    # `@reads_relation` is a hash whose
+    # key is [state.id, nterm.token_id],
+    # value is array of [state.id, nterm.token_id].
+    @reads_relation: untyped
+
+    # `@read_sets` is a hash whose
+    # key is [state.id, nterm.token_id],
+    # value is bitmap of term.
+    @read_sets: untyped
+
+    # `(p, A) includes (p', B) iff B -> βAγ, γ =>* ε, p' -(β)-> p`
+    #   where p, p' are state, A, B are nterm, β, γ is sequence of symbol.
+    #
+    # `@includes_relation` is a hash whose
+    # key is [state.id, nterm.token_id],
+    # value is array of [state.id, nterm.token_id].
+    @includes_relation: untyped
+
+    # `(q, A -> ω) lookback (p, A) iff p -(ω)-> q`
+    #   where p, q are state, A -> ω is rule, A is nterm, ω is sequence of symbol.
+    #
+    # `@lookback_relation` is a hash whose
+    # key is [state.id, rule.id],
+    # value is array of [state.id, nterm.token_id].
+    @lookback_relation: untyped
+
+    # `@follow_sets` is a hash whose
+    # key is [state.id, rule.id],
+    # value is bitmap of term.
+    @follow_sets: untyped
+
+    # `LA(q, A -> ω) = ∪{Follow(p, A) | (q, A -> ω) lookback (p, A)`
+    #
+    # `@la` is a hash whose
+    # key is [state.id, rule.id],
+    # value is bitmap of term.
+    @la: untyped
+
+    extend Forwardable
+
+    include Lrama::Report::Duration
+
+    attr_reader states: untyped
+
+    attr_reader reads_relation: untyped
+
+    attr_reader includes_relation: untyped
+
+    attr_reader lookback_relation: untyped
+
+    def initialize: (untyped grammar, untyped warning, ?trace_state: bool) -> void
+
+    def compute: () -> untyped
+
+    def reporter: () -> untyped
+
+    def states_count: () -> untyped
+
+    def direct_read_sets: () -> untyped
+
+    def read_sets: () -> untyped
+
+    def follow_sets: () -> untyped
+
+    def la: () -> untyped
+
+    private
+
+    def sr_conflicts: () -> untyped
+
+    def rr_conflicts: () -> untyped
+
+    def trace_state: () { (untyped) -> untyped } -> (untyped | nil)
+
+    def create_state: (untyped accessing_symbol, untyped kernels, untyped states_created) -> (::Array[untyped | false] | ::Array[untyped | true])
+
+    def setup_state: (untyped state) -> untyped
+
+    def enqueue_state: (untyped states, untyped state) -> untyped
+
+    def compute_lr0_states: () -> untyped
+
+    def nterm_transitions: () -> untyped
+
+    def compute_direct_read_sets: () -> untyped
+
+    def compute_reads_relation: () -> untyped
+
+    def compute_read_sets: () -> untyped
+
+    # Execute transition of state by symbols
+    # then return final state.
+    def transition: (untyped state, untyped symbols) -> untyped
+
+    def compute_includes_relation: () -> untyped
+
+    def compute_lookback_relation: () -> untyped
+
+    def compute_follow_sets: () -> untyped
+
+    def compute_look_ahead_sets: () -> untyped
+
+    def bitmap_to_terms: (untyped bit) -> untyped
+
+    def compute_conflicts: () -> untyped
+
+    def compute_shift_reduce_conflicts: () -> untyped
+
+    def compute_reduce_reduce_conflicts: () -> untyped
+
+    def compute_default_reduction: () -> untyped
+
+    def check_conflicts: () -> untyped
+  end
+end

From f5a3ba71f1773869119005c787013cee0f6ae5f1 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Tue, 18 Jun 2024 00:28:45 +0900
Subject: [PATCH 02/18] fix type error

---
 Steepfile                                |  3 +++
 lib/lrama/counterexamples/path.rb        |  4 ++++
 sig/lrama/counterexamples.rbs            |  2 +-
 sig/lrama/counterexamples/derivation.rbs |  2 +-
 sig/lrama/counterexamples/example.rbs    |  6 +++---
 sig/lrama/counterexamples/path.rbs       |  2 ++
 sig/lrama/grammar.rbs                    | 11 +++++++++++
 sig/lrama/states.rbs                     |  2 ++
 8 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/Steepfile b/Steepfile
index 2aad7a87..0c34556c 100644
--- a/Steepfile
+++ b/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"
diff --git a/lib/lrama/counterexamples/path.rb b/lib/lrama/counterexamples/path.rb
index 243b6b42..92ccf736 100644
--- a/lib/lrama/counterexamples/path.rb
+++ b/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
diff --git a/sig/lrama/counterexamples.rbs b/sig/lrama/counterexamples.rbs
index 3afd894f..5adcdca4 100644
--- a/sig/lrama/counterexamples.rbs
+++ b/sig/lrama/counterexamples.rbs
@@ -1,6 +1,6 @@
 module Lrama
   class Counterexamples
-    @states: untyped
+    @states: States
     @transitions: untyped
     @reverse_transitions: untyped
     @productions: untyped
diff --git a/sig/lrama/counterexamples/derivation.rbs b/sig/lrama/counterexamples/derivation.rbs
index f5fbc427..338dab1f 100644
--- a/sig/lrama/counterexamples/derivation.rbs
+++ b/sig/lrama/counterexamples/derivation.rbs
@@ -5,7 +5,7 @@ module Lrama
 
       @left: untyped
 
-      @right: untyped
+      @right: Derivation
 
       attr_reader item: untyped
 
diff --git a/sig/lrama/counterexamples/example.rbs b/sig/lrama/counterexamples/example.rbs
index 6089724e..2ba4b038 100644
--- a/sig/lrama/counterexamples/example.rbs
+++ b/sig/lrama/counterexamples/example.rbs
@@ -11,9 +11,9 @@ module Lrama
 
       @counterexamples: untyped
 
-      @derivations1: untyped
+      @derivations1: Derivation
 
-      @derivations2: untyped
+      @derivations2: Derivation
 
       attr_reader path1: untyped
 
@@ -41,7 +41,7 @@ module Lrama
 
       def _derivations: (untyped paths) -> untyped
 
-      def find_derivation_for_symbol: (untyped state_item, untyped sym) -> untyped
+      def find_derivation_for_symbol: (untyped state_item, untyped sym) -> Derivation?
     end
   end
 end
diff --git a/sig/lrama/counterexamples/path.rbs b/sig/lrama/counterexamples/path.rbs
index ea644650..bb67b29f 100644
--- a/sig/lrama/counterexamples/path.rbs
+++ b/sig/lrama/counterexamples/path.rbs
@@ -14,6 +14,8 @@ module Lrama
       def to_s: () -> ::String
 
       alias inspect to_s
+
+      def type: -> bot
     end
   end
 end
diff --git a/sig/lrama/grammar.rbs b/sig/lrama/grammar.rbs
index 886cc82c..1af19fef 100644
--- a/sig/lrama/grammar.rbs
+++ b/sig/lrama/grammar.rbs
@@ -91,5 +91,16 @@ module Lrama
     def fill_sym_to_rules: () -> Array[Rule]
     def validate_rule_lhs_is_nterm!: () -> void
     def set_locations: () -> void
+
+    interface _DelegatedMethods
+    def symbols: () -> untyped
+    def terms: () -> untyped
+    def nterms: () -> untyped
+    def rules: () -> untyped
+    def accept_symbol: () -> untyped
+    def eof_symbol: () -> untyped
+    def undef_symbol: () -> untyped
+    def find_symbol_by_s_value!: () -> untyped
+    end
   end
 end
diff --git a/sig/lrama/states.rbs b/sig/lrama/states.rbs
index b48d5eb6..ca2d9f39 100644
--- a/sig/lrama/states.rbs
+++ b/sig/lrama/states.rbs
@@ -4,6 +4,8 @@ module Lrama
   # "Efficient Computation of LALR(1) Look-Ahead Sets"
   #   https://dl.acm.org/doi/pdf/10.1145/69622.357187
   class States
+    include Grammar::_DelegatedMethods
+
     @grammar: untyped
 
     @warning: untyped

From 86a2d58b2a1b60917029f52bf1c42a4eb18979fc Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Fri, 9 Aug 2024 18:05:59 +0900
Subject: [PATCH 03/18] Add types to derivation

---
 sig/lrama/counterexamples/derivation.rbs | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/sig/lrama/counterexamples/derivation.rbs b/sig/lrama/counterexamples/derivation.rbs
index 338dab1f..5a9fe249 100644
--- a/sig/lrama/counterexamples/derivation.rbs
+++ b/sig/lrama/counterexamples/derivation.rbs
@@ -1,33 +1,33 @@
 module Lrama
   class Counterexamples
     class Derivation
-      @item: untyped
+      @item: States::Item
 
-      @left: untyped
+      @left: Derivation
 
       @right: Derivation
 
-      attr_reader item: untyped
+      attr_reader item: States::Item
 
-      attr_reader left: untyped
+      attr_reader left: Derivation
 
-      attr_reader right: untyped
+      attr_reader right: Derivation?
 
-      attr_writer right: untyped
+      attr_writer right: Derivation
 
-      def initialize: (untyped item, untyped left, ?untyped? right) -> void
+      def initialize: (States::Item item, Derivation left, ?Derivation? right) -> void
 
       def to_s: () -> ::String
 
       alias inspect to_s
 
-      def render_strings_for_report: () -> untyped
+      def render_strings_for_report: () -> Array[String]
 
-      def render_for_report: () -> untyped
+      def render_for_report: () -> String
 
       private
 
-      def _render_for_report: (untyped derivation, untyped offset, untyped strings, untyped index) -> untyped
+      def _render_for_report: (Derivation derivation, Integer offset, Array[String] strings, Integer index) -> Integer
     end
   end
 end

From db62c5edebe38ff21b62feb548485d024a89a10a Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Tue, 3 Sep 2024 00:14:59 +0900
Subject: [PATCH 04/18] Add types to example.rbs and some files

---
 sig/lrama/counterexamples.rbs         |  2 +-
 sig/lrama/counterexamples/example.rbs | 36 +++++++++++++--------------
 sig/lrama/counterexamples/path.rbs    |  2 +-
 sig/lrama/counterexamples/triple.rbs  |  4 +--
 sig/lrama/states.rbs                  |  4 +--
 5 files changed, 23 insertions(+), 25 deletions(-)

diff --git a/sig/lrama/counterexamples.rbs b/sig/lrama/counterexamples.rbs
index 5adcdca4..d66ef1a2 100644
--- a/sig/lrama/counterexamples.rbs
+++ b/sig/lrama/counterexamples.rbs
@@ -23,7 +23,7 @@ module Lrama
     def find_shift_conflict_shortest_path: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
     def find_shift_conflict_shortest_state_items: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
     def build_paths_from_state_items: (untyped state_items) -> untyped
-    def shortest_path: (untyped conflict_state, untyped conflict_reduce_item, untyped conflict_term) -> (untyped | nil)
+    def shortest_path: (untyped conflict_state, untyped conflict_reduce_item, untyped conflict_term) -> [StartPath]?
     def follow_l: (untyped item, untyped current_l) -> untyped
   end
 end
diff --git a/sig/lrama/counterexamples/example.rbs b/sig/lrama/counterexamples/example.rbs
index 2ba4b038..1fe35d81 100644
--- a/sig/lrama/counterexamples/example.rbs
+++ b/sig/lrama/counterexamples/example.rbs
@@ -1,47 +1,45 @@
 module Lrama
   class Counterexamples
     class Example
-      @path1: untyped
+      @path1: (StartPath | ProductionPath | TransitionPath)
 
-      @path2: untyped
+      @path2: [StartPath]?
 
-      @conflict: untyped
+      @conflict: (State::ShiftReduceConflict | State::ReduceReduceConflict)
 
-      @conflict_symbol: untyped
+      @conflict_symbol: Grammar::Symbol
 
-      @counterexamples: untyped
+      @counterexamples: Counterexamples
 
       @derivations1: Derivation
 
       @derivations2: Derivation
 
-      attr_reader path1: untyped
+      attr_reader path1: (StartPath | ProductionPath | TransitionPath)
 
-      attr_reader path2: untyped
+      attr_reader path2: [StartPath]?
 
-      attr_reader conflict: untyped
+      attr_reader conflict: (State::ShiftReduceConflict | State::ReduceReduceConflict)
 
-      attr_reader conflict_symbol: untyped
+      attr_reader conflict_symbol: Grammar::Symbol
 
-      # path1 is shift conflict when S/R conflict
-      # path2 is always reduce conflict
-      def initialize: (untyped path1, untyped path2, untyped conflict, untyped conflict_symbol, untyped counterexamples) -> void
+      def initialize: ((StartPath | ProductionPath | TransitionPath) path1, [StartPath]? path2, (State::ShiftReduceConflict | State::ReduceReduceConflict) conflict, Grammar::Symbol conflict_symbol, Counterexamples counterexamples) -> void
 
-      def type: () -> untyped
+      def type: () -> (:shift_reduce | :reduce_reduce)
 
-      def path1_item: () -> untyped
+      def path1_item: () -> States::Item
 
-      def path2_item: () -> untyped
+      def path2_item: () -> States::Item
 
-      def derivations1: () -> untyped
+      def derivations1: () -> Derivation
 
-      def derivations2: () -> untyped
+      def derivations2: () -> Derivation
 
       private
 
-      def _derivations: (untyped paths) -> untyped
+      def _derivations: (Array[Path] paths) -> Derivation
 
-      def find_derivation_for_symbol: (untyped state_item, untyped sym) -> Derivation?
+      def find_derivation_for_symbol: (StateItem state_item, Grammar::Symbol sym) -> Derivation?
     end
   end
 end
diff --git a/sig/lrama/counterexamples/path.rbs b/sig/lrama/counterexamples/path.rbs
index bb67b29f..2d8d8806 100644
--- a/sig/lrama/counterexamples/path.rbs
+++ b/sig/lrama/counterexamples/path.rbs
@@ -9,7 +9,7 @@ module Lrama
 
       def from: () -> untyped
 
-      def to: () -> untyped
+      def to: () -> StateItem
 
       def to_s: () -> ::String
 
diff --git a/sig/lrama/counterexamples/triple.rbs b/sig/lrama/counterexamples/triple.rbs
index 8e16898a..23a314b6 100644
--- a/sig/lrama/counterexamples/triple.rbs
+++ b/sig/lrama/counterexamples/triple.rbs
@@ -2,14 +2,14 @@ module Lrama
   class Counterexamples
     class Triple
       attr_accessor s: untyped
-      attr_accessor itm: untyped
+      attr_accessor itm: States::Item
       attr_accessor l: untyped
 
       alias state s
       alias item itm
       alias precise_lookahead_set l
 
-      def initialize: (untyped s, untyped itm, untyped l) -> void
+      def initialize: (untyped s, States::Item itm, untyped l) -> void
 
       def state_item: () -> untyped
       def inspect: () -> ::String
diff --git a/sig/lrama/states.rbs b/sig/lrama/states.rbs
index ca2d9f39..1166c779 100644
--- a/sig/lrama/states.rbs
+++ b/sig/lrama/states.rbs
@@ -12,7 +12,7 @@ module Lrama
 
     @trace_state: untyped
 
-    @states: untyped
+    @states: Array[State]
 
     # `DR(p, A) = {t ∈ T | p -(A)-> r -(t)-> }`
     #   where p is state, A is nterm, t is term.
@@ -68,7 +68,7 @@ module Lrama
 
     include Lrama::Report::Duration
 
-    attr_reader states: untyped
+    attr_reader states: Array[State]
 
     attr_reader reads_relation: untyped
 

From 4f74d51d5d175bf8e65a2c91e6d6503a7dcf7342 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Tue, 3 Sep 2024 13:18:22 +0900
Subject: [PATCH 05/18] Generate state.rbs

---
 sig/lrama/state.rbs | 82 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 82 insertions(+)
 create mode 100644 sig/lrama/state.rbs

diff --git a/sig/lrama/state.rbs b/sig/lrama/state.rbs
new file mode 100644
index 00000000..d2b5e6b9
--- /dev/null
+++ b/sig/lrama/state.rbs
@@ -0,0 +1,82 @@
+module Lrama
+  class State
+    @id: untyped
+
+    @accessing_symbol: untyped
+
+    @kernels: untyped
+
+    @items: untyped
+
+    # Manage relationships between items to state
+    # to resolve next state
+    @items_to_state: untyped
+
+    @conflicts: untyped
+
+    @resolved_conflicts: untyped
+
+    @default_reduction_rule: untyped
+
+    @closure: untyped
+
+    @nterm_transitions: untyped
+
+    @term_transitions: untyped
+
+    @transitions: untyped
+
+    attr_reader id: untyped
+
+    attr_reader accessing_symbol: untyped
+
+    attr_reader kernels: untyped
+
+    attr_reader conflicts: untyped
+
+    attr_reader resolved_conflicts: untyped
+
+    attr_reader default_reduction_rule: untyped
+
+    attr_reader closure: untyped
+
+    attr_reader items: untyped
+
+    attr_accessor shifts: untyped
+
+    attr_accessor reduces: untyped
+
+    def initialize: (untyped id, untyped accessing_symbol, untyped kernels) -> void
+
+    def closure=: (untyped closure) -> untyped
+
+    def non_default_reduces: () -> untyped
+
+    def compute_shifts_reduces: () -> untyped
+
+    def set_items_to_state: (untyped items, untyped next_state) -> untyped
+
+    def set_look_ahead: (untyped rule, untyped look_ahead) -> untyped
+
+    def nterm_transitions: () -> untyped
+
+    def term_transitions: () -> untyped
+
+    def transitions: () -> untyped
+
+    def selected_term_transitions: () -> untyped
+
+    # Move to next state by sym
+    def transition: (untyped sym) -> untyped
+
+    def find_reduce_by_item!: (untyped item) -> untyped
+
+    def default_reduction_rule=: (untyped default_reduction_rule) -> untyped
+
+    def has_conflicts?: () -> untyped
+
+    def sr_conflicts: () -> untyped
+
+    def rr_conflicts: () -> untyped
+  end
+end

From f4f2ea5f4bf75994ed86790da4208b162812c70c Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Tue, 3 Sep 2024 18:02:00 +0900
Subject: [PATCH 06/18] Modified to pass type inspection

---
 lib/lrama/counterexamples.rb             |  2 +-
 sig/lrama/counterexamples.rbs            |  2 +-
 sig/lrama/counterexamples/derivation.rbs | 10 +++++-----
 sig/lrama/counterexamples/example.rbs    | 16 ++++++++--------
 4 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/lib/lrama/counterexamples.rb b/lib/lrama/counterexamples.rb
index aaf2bb20..17185681 100644
--- a/lib/lrama/counterexamples.rb
+++ b/lib/lrama/counterexamples.rb
@@ -226,7 +226,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]))
diff --git a/sig/lrama/counterexamples.rbs b/sig/lrama/counterexamples.rbs
index d66ef1a2..5db4cbdf 100644
--- a/sig/lrama/counterexamples.rbs
+++ b/sig/lrama/counterexamples.rbs
@@ -23,7 +23,7 @@ module Lrama
     def find_shift_conflict_shortest_path: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
     def find_shift_conflict_shortest_state_items: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
     def build_paths_from_state_items: (untyped state_items) -> untyped
-    def shortest_path: (untyped conflict_state, untyped conflict_reduce_item, untyped conflict_term) -> [StartPath]?
+    def shortest_path: (State conflict_state, States::Item conflict_reduce_item, Grammar::Symbol conflict_term) -> [Path]?
     def follow_l: (untyped item, untyped current_l) -> untyped
   end
 end
diff --git a/sig/lrama/counterexamples/derivation.rbs b/sig/lrama/counterexamples/derivation.rbs
index 5a9fe249..2b2db25c 100644
--- a/sig/lrama/counterexamples/derivation.rbs
+++ b/sig/lrama/counterexamples/derivation.rbs
@@ -3,19 +3,19 @@ module Lrama
     class Derivation
       @item: States::Item
 
-      @left: Derivation
+      @left: Derivation?
 
-      @right: Derivation
+      @right: Derivation?
 
       attr_reader item: States::Item
 
-      attr_reader left: Derivation
+      attr_reader left: Derivation?
 
       attr_reader right: Derivation?
 
-      attr_writer right: Derivation
+      attr_writer right: Derivation?
 
-      def initialize: (States::Item item, Derivation left, ?Derivation? right) -> void
+      def initialize: (States::Item item, Derivation? left, ?Derivation? right) -> void
 
       def to_s: () -> ::String
 
diff --git a/sig/lrama/counterexamples/example.rbs b/sig/lrama/counterexamples/example.rbs
index 1fe35d81..961f79f9 100644
--- a/sig/lrama/counterexamples/example.rbs
+++ b/sig/lrama/counterexamples/example.rbs
@@ -1,9 +1,9 @@
 module Lrama
   class Counterexamples
     class Example
-      @path1: (StartPath | ProductionPath | TransitionPath)
+      @path1: [Path]
 
-      @path2: [StartPath]?
+      @path2: [Path]
 
       @conflict: (State::ShiftReduceConflict | State::ReduceReduceConflict)
 
@@ -15,15 +15,15 @@ module Lrama
 
       @derivations2: Derivation
 
-      attr_reader path1: (StartPath | ProductionPath | TransitionPath)
+      attr_reader path1: [Path]
 
-      attr_reader path2: [StartPath]?
+      attr_reader path2: [Path]
 
       attr_reader conflict: (State::ShiftReduceConflict | State::ReduceReduceConflict)
 
       attr_reader conflict_symbol: Grammar::Symbol
 
-      def initialize: ((StartPath | ProductionPath | TransitionPath) path1, [StartPath]? path2, (State::ShiftReduceConflict | State::ReduceReduceConflict) conflict, Grammar::Symbol conflict_symbol, Counterexamples counterexamples) -> void
+      def initialize: ([Path]? path1, [Path]? path2, (State::ShiftReduceConflict | State::ReduceReduceConflict) conflict, Grammar::Symbol conflict_symbol, Counterexamples counterexamples) -> void
 
       def type: () -> (:shift_reduce | :reduce_reduce)
 
@@ -31,13 +31,13 @@ module Lrama
 
       def path2_item: () -> States::Item
 
-      def derivations1: () -> Derivation
+      def derivations1: () -> Derivation?
 
-      def derivations2: () -> Derivation
+      def derivations2: () -> Derivation?
 
       private
 
-      def _derivations: (Array[Path] paths) -> Derivation
+      def _derivations: (Array[Path] paths) -> Derivation?
 
       def find_derivation_for_symbol: (StateItem state_item, Grammar::Symbol sym) -> Derivation?
     end

From 2772c0e55dee153f0f1c0b0b0ea0723e1cbff4f8 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Fri, 6 Sep 2024 18:10:11 +0900
Subject: [PATCH 07/18] Define types to counterexamples directory

---
 sig/lrama/counterexamples.rbs            | 2 +-
 sig/lrama/counterexamples/path.rbs       | 8 ++++----
 sig/lrama/counterexamples/state_item.rbs | 6 +++---
 sig/lrama/counterexamples/triple.rbs     | 8 ++++----
 sig/lrama/grammar/symbol.rbs             | 2 +-
 5 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/sig/lrama/counterexamples.rbs b/sig/lrama/counterexamples.rbs
index 5db4cbdf..05126b8d 100644
--- a/sig/lrama/counterexamples.rbs
+++ b/sig/lrama/counterexamples.rbs
@@ -22,7 +22,7 @@ module Lrama
     def reduce_reduce_examples: (untyped conflict_state, untyped conflict) -> untyped
     def find_shift_conflict_shortest_path: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
     def find_shift_conflict_shortest_state_items: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
-    def build_paths_from_state_items: (untyped state_items) -> untyped
+    def build_paths_from_state_items: (Array[StateItem] state_items) -> untyped
     def shortest_path: (State conflict_state, States::Item conflict_reduce_item, Grammar::Symbol conflict_term) -> [Path]?
     def follow_l: (untyped item, untyped current_l) -> untyped
   end
diff --git a/sig/lrama/counterexamples/path.rbs b/sig/lrama/counterexamples/path.rbs
index 2d8d8806..0ef4eec6 100644
--- a/sig/lrama/counterexamples/path.rbs
+++ b/sig/lrama/counterexamples/path.rbs
@@ -1,13 +1,13 @@
 module Lrama
   class Counterexamples
     class Path
-      @from_state_item: untyped
+      @from_state_item: StateItem
 
-      @to_state_item: untyped
+      @to_state_item: StateItem
 
-      def initialize: (untyped? from_state_item, untyped to_state_item) -> void
+      def initialize: (StateItem? from_state_item, StateItem to_state_item) -> void
 
-      def from: () -> untyped
+      def from: () -> StateItem
 
       def to: () -> StateItem
 
diff --git a/sig/lrama/counterexamples/state_item.rbs b/sig/lrama/counterexamples/state_item.rbs
index f32d50de..32eab848 100644
--- a/sig/lrama/counterexamples/state_item.rbs
+++ b/sig/lrama/counterexamples/state_item.rbs
@@ -1,10 +1,10 @@
 module Lrama
   class Counterexamples
     class StateItem
-     attr_accessor state: untyped
-     attr_accessor item: untyped
+     attr_accessor state: State
+     attr_accessor item: States::Item
 
-      def initialize: (untyped state, untyped item) -> untyped
+      def initialize: (State state, States::Item item) -> void
     end
   end
 end
diff --git a/sig/lrama/counterexamples/triple.rbs b/sig/lrama/counterexamples/triple.rbs
index 23a314b6..1b3cae35 100644
--- a/sig/lrama/counterexamples/triple.rbs
+++ b/sig/lrama/counterexamples/triple.rbs
@@ -1,17 +1,17 @@
 module Lrama
   class Counterexamples
     class Triple
-      attr_accessor s: untyped
+      attr_accessor s: State
       attr_accessor itm: States::Item
-      attr_accessor l: untyped
+      attr_accessor l: Set[Grammar::Symbol]
 
       alias state s
       alias item itm
       alias precise_lookahead_set l
 
-      def initialize: (untyped s, States::Item itm, untyped l) -> void
+      def initialize: (State s, States::Item itm, Set[Grammar::Symbol] l) -> void
 
-      def state_item: () -> untyped
+      def state_item: () -> StateItem
       def inspect: () -> ::String
 
       alias to_s inspect
diff --git a/sig/lrama/grammar/symbol.rbs b/sig/lrama/grammar/symbol.rbs
index 7a84f246..32ba678a 100644
--- a/sig/lrama/grammar/symbol.rbs
+++ b/sig/lrama/grammar/symbol.rbs
@@ -13,7 +13,7 @@ module Lrama
       attr_accessor destructor: Destructor?
       attr_accessor error_token: ErrorToken
 
-      attr_accessor first_set: Set[Array[Symbol]] | Set[Symbol]
+      attr_accessor first_set: Set[Grammar::Symbol]
       attr_accessor first_set_bitmap: Integer
       attr_writer eof_symbol: bool
       attr_writer error_symbol: bool

From 68f7d6c2a76b086cd2dae65c89604c582392dd83 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Tue, 8 Oct 2024 18:24:20 +0900
Subject: [PATCH 08/18] Fix or ignore nullable error

---
 lib/lrama/counterexamples/derivation.rb | 7 ++++---
 lib/lrama/counterexamples/example.rb    | 9 ++++++---
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/lib/lrama/counterexamples/derivation.rb b/lib/lrama/counterexamples/derivation.rb
index 423e58b8..ea339e82 100644
--- a/lib/lrama/counterexamples/derivation.rb
+++ b/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
diff --git a/lib/lrama/counterexamples/example.rb b/lib/lrama/counterexamples/example.rb
index 8dda0d17..d4840fd5 100644
--- a/lib/lrama/counterexamples/example.rb
+++ b/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
 

From c677a23607939a6349f68515c2af542616a85071 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Tue, 22 Oct 2024 10:10:45 +0900
Subject: [PATCH 09/18] Define type to StartPath#initialize and fix some types

---
 rbs_collection.lock.yaml                 | 8 ++++++++
 sig/lrama/counterexamples/path.rbs       | 4 ++--
 sig/lrama/counterexamples/start_path.rbs | 2 +-
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/rbs_collection.lock.yaml b/rbs_collection.lock.yaml
index b53cb101..bfbfce65 100644
--- a/rbs_collection.lock.yaml
+++ b/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:
diff --git a/sig/lrama/counterexamples/path.rbs b/sig/lrama/counterexamples/path.rbs
index 0ef4eec6..8a9d8b83 100644
--- a/sig/lrama/counterexamples/path.rbs
+++ b/sig/lrama/counterexamples/path.rbs
@@ -1,13 +1,13 @@
 module Lrama
   class Counterexamples
     class Path
-      @from_state_item: StateItem
+      @from_state_item: StateItem?
 
       @to_state_item: StateItem
 
       def initialize: (StateItem? from_state_item, StateItem to_state_item) -> void
 
-      def from: () -> StateItem
+      def from: () -> StateItem?
 
       def to: () -> StateItem
 
diff --git a/sig/lrama/counterexamples/start_path.rbs b/sig/lrama/counterexamples/start_path.rbs
index a53bd144..5f83a9cc 100644
--- a/sig/lrama/counterexamples/start_path.rbs
+++ b/sig/lrama/counterexamples/start_path.rbs
@@ -1,7 +1,7 @@
 module Lrama
   class Counterexamples
     class StartPath < Path
-      def initialize: (untyped to_state_item) -> void
+      def initialize: (StateItem to_state_item) -> void
 
       def type: () -> :start
 

From ca97ded8346ba84b993c0b6c3b3cbefba386815a Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Tue, 22 Oct 2024 10:16:06 +0900
Subject: [PATCH 10/18] Add types to delegated methods to grammar

---
 sig/lrama/grammar.rbs | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/sig/lrama/grammar.rbs b/sig/lrama/grammar.rbs
index 1af19fef..9042525c 100644
--- a/sig/lrama/grammar.rbs
+++ b/sig/lrama/grammar.rbs
@@ -93,14 +93,16 @@ module Lrama
     def set_locations: () -> void
 
     interface _DelegatedMethods
-    def symbols: () -> untyped
-    def terms: () -> untyped
-    def nterms: () -> untyped
-    def rules: () -> untyped
-    def accept_symbol: () -> untyped
-    def eof_symbol: () -> untyped
-    def undef_symbol: () -> untyped
-    def find_symbol_by_s_value!: () -> untyped
+    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

From 4134e7afd39bc6d041b45db8c7ff01bf96fd8a9c Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Wed, 11 Dec 2024 00:55:10 +0900
Subject: [PATCH 11/18] Fix changed nullable type information to not null

---
 sig/lrama/state/reduce_reduce_conflict.rbs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sig/lrama/state/reduce_reduce_conflict.rbs b/sig/lrama/state/reduce_reduce_conflict.rbs
index 23ced680..24a8de03 100644
--- a/sig/lrama/state/reduce_reduce_conflict.rbs
+++ b/sig/lrama/state/reduce_reduce_conflict.rbs
@@ -1,11 +1,11 @@
 module Lrama
   class State
     class ReduceReduceConflict
-      attr_accessor symbols: Array[Grammar::Symbol?]
+      attr_accessor symbols: Array[Grammar::Symbol]
       attr_accessor reduce1: State::Reduce
       attr_accessor reduce2: State::Reduce
 
-      def initialize: (?symbols: Array[Grammar::Symbol?], ?reduce1: State::Reduce, ?reduce2: State::Reduce) -> void
+      def initialize: (?symbols: Array[Grammar::Symbol], ?reduce1: State::Reduce, ?reduce2: State::Reduce) -> void
 
       def type: () -> :reduce_reduce
     end

From 0176571c554f2c85f785f42bbae4746b5edd7027 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Wed, 11 Dec 2024 01:21:26 +0900
Subject: [PATCH 12/18] Define types in and around counterexamples.rb

---
 sig/lrama/counterexamples.rbs         | 34 +++++++++++++--------------
 sig/lrama/counterexamples/example.rbs | 12 +++++-----
 sig/lrama/state.rbs                   | 16 ++++++-------
 3 files changed, 31 insertions(+), 31 deletions(-)

diff --git a/sig/lrama/counterexamples.rbs b/sig/lrama/counterexamples.rbs
index 05126b8d..c32c2488 100644
--- a/sig/lrama/counterexamples.rbs
+++ b/sig/lrama/counterexamples.rbs
@@ -1,29 +1,29 @@
 module Lrama
   class Counterexamples
     @states: States
-    @transitions: untyped
-    @reverse_transitions: untyped
-    @productions: untyped
-    @reverse_productions: untyped
+    @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: untyped
-    attr_reader productions: untyped
+    attr_reader transitions: Hash[[StateItem, Grammar::Symbol], StateItem]
+    attr_reader productions: Hash[StateItem, Set[States::Item]]
 
-    def initialize: (untyped states) -> void
+    def initialize: (States states) -> void
     def to_s: () -> "#<Counterexamples>"
     alias inspect to_s
-    def compute: (untyped conflict_state) -> untyped
+    def compute: (State conflict_state) -> Array[Example]
 
     private
 
-    def setup_transitions: () -> untyped
-    def setup_productions: () -> untyped
-    def shift_reduce_example: (untyped conflict_state, untyped conflict) -> untyped
-    def reduce_reduce_examples: (untyped conflict_state, untyped conflict) -> untyped
-    def find_shift_conflict_shortest_path: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
-    def find_shift_conflict_shortest_state_items: (untyped reduce_path, untyped conflict_state, untyped conflict_item) -> untyped
-    def build_paths_from_state_items: (Array[StateItem] state_items) -> untyped
-    def shortest_path: (State conflict_state, States::Item conflict_reduce_item, Grammar::Symbol conflict_term) -> [Path]?
-    def follow_l: (untyped item, untyped current_l) -> untyped
+    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
diff --git a/sig/lrama/counterexamples/example.rbs b/sig/lrama/counterexamples/example.rbs
index 961f79f9..ba55d46d 100644
--- a/sig/lrama/counterexamples/example.rbs
+++ b/sig/lrama/counterexamples/example.rbs
@@ -1,9 +1,9 @@
 module Lrama
   class Counterexamples
     class Example
-      @path1: [Path]
+      @path1: ::Array[StartPath | TransitionPath | ProductionPath]
 
-      @path2: [Path]
+      @path2: ::Array[StartPath | TransitionPath | ProductionPath]
 
       @conflict: (State::ShiftReduceConflict | State::ReduceReduceConflict)
 
@@ -15,15 +15,15 @@ module Lrama
 
       @derivations2: Derivation
 
-      attr_reader path1: [Path]
+      attr_reader path1: ::Array[StartPath | TransitionPath | ProductionPath]
 
-      attr_reader path2: [Path]
+      attr_reader path2: ::Array[StartPath | TransitionPath | ProductionPath]
 
       attr_reader conflict: (State::ShiftReduceConflict | State::ReduceReduceConflict)
 
       attr_reader conflict_symbol: Grammar::Symbol
 
-      def initialize: ([Path]? path1, [Path]? path2, (State::ShiftReduceConflict | State::ReduceReduceConflict) conflict, Grammar::Symbol conflict_symbol, Counterexamples counterexamples) -> void
+      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)
 
@@ -37,7 +37,7 @@ module Lrama
 
       private
 
-      def _derivations: (Array[Path] paths) -> Derivation?
+      def _derivations: (::Array[StartPath | TransitionPath | ProductionPath] paths) -> Derivation?
 
       def find_derivation_for_symbol: (StateItem state_item, Grammar::Symbol sym) -> Derivation?
     end
diff --git a/sig/lrama/state.rbs b/sig/lrama/state.rbs
index d2b5e6b9..e462709c 100644
--- a/sig/lrama/state.rbs
+++ b/sig/lrama/state.rbs
@@ -6,13 +6,13 @@ module Lrama
 
     @kernels: untyped
 
-    @items: untyped
+    @items: Array[States::Item]
 
     # Manage relationships between items to state
     # to resolve next state
     @items_to_state: untyped
 
-    @conflicts: untyped
+    @conflicts: Array[State::ShiftReduceConflict|State::ReduceReduceConflict]
 
     @resolved_conflicts: untyped
 
@@ -24,7 +24,7 @@ module Lrama
 
     @term_transitions: untyped
 
-    @transitions: untyped
+    @transitions: Array[[Shift, State]]
 
     attr_reader id: untyped
 
@@ -32,7 +32,7 @@ module Lrama
 
     attr_reader kernels: untyped
 
-    attr_reader conflicts: untyped
+    attr_reader conflicts: Array[State::ShiftReduceConflict|State::ReduceReduceConflict]
 
     attr_reader resolved_conflicts: untyped
 
@@ -40,13 +40,13 @@ module Lrama
 
     attr_reader closure: untyped
 
-    attr_reader items: untyped
+    attr_reader items: Array[States::Item]
 
-    attr_accessor shifts: untyped
+    attr_accessor shifts: Array[Shift]
 
     attr_accessor reduces: untyped
 
-    def initialize: (untyped id, untyped accessing_symbol, untyped kernels) -> void
+    def initialize: (untyped id, untyped accessing_symbol, Array[States::Item] kernels) -> void
 
     def closure=: (untyped closure) -> untyped
 
@@ -62,7 +62,7 @@ module Lrama
 
     def term_transitions: () -> untyped
 
-    def transitions: () -> untyped
+    def transitions: () -> Array[[Shift, State]]
 
     def selected_term_transitions: () -> untyped
 

From 7105dc74fed32d0732eac730793d52c3513a0997 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Sat, 14 Dec 2024 00:08:37 +0900
Subject: [PATCH 13/18] Add type definition and fix method calls from var that
 may be null

---
 lib/lrama/counterexamples.rb | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/lib/lrama/counterexamples.rb b/lib/lrama/counterexamples.rb
index 17185681..11076478 100644
--- a/lib/lrama/counterexamples.rb
+++ b/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

From 2f18c94593f011e56de6b64c3eb9cd22bb1fd435 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Fri, 20 Dec 2024 14:00:58 +0900
Subject: [PATCH 14/18] Run rbs collection update

---
 rbs_collection.lock.yaml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/rbs_collection.lock.yaml b/rbs_collection.lock.yaml
index 2e642e97..cc74a7fd 100644
--- a/rbs_collection.lock.yaml
+++ b/rbs_collection.lock.yaml
@@ -6,7 +6,7 @@ gems:
   source:
     type: git
     name: ruby/gem_rbs_collection
-    revision: f2fa96be08e0f7fe5237a45d2b69d9d7a5d0b416
+    revision: 71fb7ae83789ae150bdee1cd8a7cd3035b5d79e2
     remote: https://github.com/ruby/gem_rbs_collection.git
     repo_dir: gems
 - name: erb
@@ -26,7 +26,7 @@ gems:
   source:
     type: git
     name: ruby/gem_rbs_collection
-    revision: f2fa96be08e0f7fe5237a45d2b69d9d7a5d0b416
+    revision: 71fb7ae83789ae150bdee1cd8a7cd3035b5d79e2
     remote: https://github.com/ruby/gem_rbs_collection.git
     repo_dir: gems
 - name: stackprof
@@ -34,7 +34,7 @@ gems:
   source:
     type: git
     name: ruby/gem_rbs_collection
-    revision: f2fa96be08e0f7fe5237a45d2b69d9d7a5d0b416
+    revision: 71fb7ae83789ae150bdee1cd8a7cd3035b5d79e2
     remote: https://github.com/ruby/gem_rbs_collection.git
     repo_dir: gems
 - name: strscan

From 12c75e35cd39d888c615d8814001b0c6bfc207d1 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Fri, 20 Dec 2024 18:42:29 +0900
Subject: [PATCH 15/18] Fix Ruby::UnannotatedEmptyCollection error

---
 lib/lrama/counterexamples.rb            | 10 +++++-----
 lib/lrama/counterexamples/derivation.rb |  2 +-
 lib/lrama/counterexamples/example.rb    |  2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/lib/lrama/counterexamples.rb b/lib/lrama/counterexamples.rb
index 11076478..ee2b5d59 100644
--- a/lib/lrama/counterexamples.rb
+++ b/lib/lrama/counterexamples.rb
@@ -50,7 +50,7 @@ def setup_transitions
       @reverse_transitions = {}
 
       @states.states.each do |src_state|
-        trans = {}
+        trans = {} #: Hash[Grammar::Symbol, State]
 
         src_state.transitions.each do |shift, next_state|
           trans[shift.next_sym] = next_state
@@ -85,7 +85,7 @@ def setup_productions
 
       @states.states.each do |state|
         # LHS => Set(Item)
-        h = {}
+        h = {} #: Hash[Grammar::Symbol, Set[States::Item]]
 
         state.closure.each do |item|
           sym = item.lhs
@@ -165,7 +165,7 @@ def find_shift_conflict_shortest_state_items(reduce_path, conflict_state, confli
         end
 
         if target_state_item.item.beginning_of_rule?
-          queue = []
+          queue = [] #: Array[Array[StateItem]]
           queue << [target_state_item]
 
           # Find reverse production
@@ -234,8 +234,8 @@ def build_paths_from_state_items(state_items)
 
     def shortest_path(conflict_state, conflict_reduce_item, conflict_term)
       # queue: is an array of [Triple, [Path]]
-      queue = []
-      visited = {}
+      queue = [] #: Array[[Triple, Array[StartPath|TransitionPath|ProductionPath]]]
+      visited = {} #: Hash[Triple, true]
       start_state = @states.states.first #: Lrama::State
       raise "BUG: Start state should be just one kernel." if start_state.kernels.count != 1
 
diff --git a/lib/lrama/counterexamples/derivation.rb b/lib/lrama/counterexamples/derivation.rb
index 436b2b79..368d7f10 100644
--- a/lib/lrama/counterexamples/derivation.rb
+++ b/lib/lrama/counterexamples/derivation.rb
@@ -18,7 +18,7 @@ def to_s
       alias :inspect :to_s
 
       def render_strings_for_report
-        result = []
+        result = [] #: Array[String]
         _render_for_report(self, 0, result, 0)
         result.map(&:rstrip)
       end
diff --git a/lib/lrama/counterexamples/example.rb b/lib/lrama/counterexamples/example.rb
index d4840fd5..01995abe 100644
--- a/lib/lrama/counterexamples/example.rb
+++ b/lib/lrama/counterexamples/example.rb
@@ -92,7 +92,7 @@ def _derivations(paths)
       end
 
       def find_derivation_for_symbol(state_item, sym)
-        queue = []
+        queue = [] #: Array[Array[StateItem]]
         queue << [state_item]
 
         while (sis = queue.shift)

From a35a747dbef268ae40dc2498c90402d615da99e2 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Sat, 21 Dec 2024 20:15:47 +0900
Subject: [PATCH 16/18] Remove comments from generated rbs files

---
 sig/lrama/state.rbs  |  3 ---
 sig/lrama/states.rbs | 42 ------------------------------------------
 2 files changed, 45 deletions(-)

diff --git a/sig/lrama/state.rbs b/sig/lrama/state.rbs
index e462709c..13b5de66 100644
--- a/sig/lrama/state.rbs
+++ b/sig/lrama/state.rbs
@@ -8,8 +8,6 @@ module Lrama
 
     @items: Array[States::Item]
 
-    # Manage relationships between items to state
-    # to resolve next state
     @items_to_state: untyped
 
     @conflicts: Array[State::ShiftReduceConflict|State::ReduceReduceConflict]
@@ -66,7 +64,6 @@ module Lrama
 
     def selected_term_transitions: () -> untyped
 
-    # Move to next state by sym
     def transition: (untyped sym) -> untyped
 
     def find_reduce_by_item!: (untyped item) -> untyped
diff --git a/sig/lrama/states.rbs b/sig/lrama/states.rbs
index 1166c779..fda9c2d2 100644
--- a/sig/lrama/states.rbs
+++ b/sig/lrama/states.rbs
@@ -1,8 +1,4 @@
 module Lrama
-  # States is passed to a template file
-  #
-  # "Efficient Computation of LALR(1) Look-Ahead Sets"
-  #   https://dl.acm.org/doi/pdf/10.1145/69622.357187
   class States
     include Grammar::_DelegatedMethods
 
@@ -14,54 +10,18 @@ module Lrama
 
     @states: Array[State]
 
-    # `DR(p, A) = {t ∈ T | p -(A)-> r -(t)-> }`
-    #   where p is state, A is nterm, t is term.
-    #
-    # `@direct_read_sets` is a hash whose
-    # key is [state.id, nterm.token_id],
-    # value is bitmap of term.
     @direct_read_sets: untyped
 
-    # Reads relation on nonterminal transitions (pair of state and nterm)
-    # `(p, A) reads (r, C) iff p -(A)-> r -(C)-> and C =>* ε`
-    #   where p, r are state, A, C are nterm.
-    #
-    # `@reads_relation` is a hash whose
-    # key is [state.id, nterm.token_id],
-    # value is array of [state.id, nterm.token_id].
     @reads_relation: untyped
 
-    # `@read_sets` is a hash whose
-    # key is [state.id, nterm.token_id],
-    # value is bitmap of term.
     @read_sets: untyped
 
-    # `(p, A) includes (p', B) iff B -> βAγ, γ =>* ε, p' -(β)-> p`
-    #   where p, p' are state, A, B are nterm, β, γ is sequence of symbol.
-    #
-    # `@includes_relation` is a hash whose
-    # key is [state.id, nterm.token_id],
-    # value is array of [state.id, nterm.token_id].
     @includes_relation: untyped
 
-    # `(q, A -> ω) lookback (p, A) iff p -(ω)-> q`
-    #   where p, q are state, A -> ω is rule, A is nterm, ω is sequence of symbol.
-    #
-    # `@lookback_relation` is a hash whose
-    # key is [state.id, rule.id],
-    # value is array of [state.id, nterm.token_id].
     @lookback_relation: untyped
 
-    # `@follow_sets` is a hash whose
-    # key is [state.id, rule.id],
-    # value is bitmap of term.
     @follow_sets: untyped
 
-    # `LA(q, A -> ω) = ∪{Follow(p, A) | (q, A -> ω) lookback (p, A)`
-    #
-    # `@la` is a hash whose
-    # key is [state.id, rule.id],
-    # value is bitmap of term.
     @la: untyped
 
     extend Forwardable
@@ -116,8 +76,6 @@ module Lrama
 
     def compute_read_sets: () -> untyped
 
-    # Execute transition of state by symbols
-    # then return final state.
     def transition: (untyped state, untyped symbols) -> untyped
 
     def compute_includes_relation: () -> untyped

From 8668c403b0a47471fe1c1c2cbd2eb5e068ee228e Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Sat, 21 Dec 2024 20:17:53 +0900
Subject: [PATCH 17/18] Fix returned error to NotImplementedError

---
 lib/lrama/counterexamples/path.rb | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/lrama/counterexamples/path.rb b/lib/lrama/counterexamples/path.rb
index 92ccf736..0a5823dd 100644
--- a/lib/lrama/counterexamples/path.rb
+++ b/lib/lrama/counterexamples/path.rb
@@ -22,7 +22,7 @@ def to_s
       alias :inspect :to_s
 
       def type
-        raise NoMethodError
+        raise NotImplementedError
       end
     end
   end

From 613c68ebd0d490ed7caa00d629e1fcfc3c88fd38 Mon Sep 17 00:00:00 2001
From: Little_Rubyist <contact@little-rubyist.com>
Date: Sat, 21 Dec 2024 20:23:38 +0900
Subject: [PATCH 18/18] Fix _derivations to be non-null

Co-authored-by: yui-knk <spiketeika@gmail.com>
---
 lib/lrama/counterexamples/example.rb  | 4 ++--
 sig/lrama/counterexamples/example.rbs | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/lib/lrama/counterexamples/example.rb b/lib/lrama/counterexamples/example.rb
index 01995abe..bb08428f 100644
--- a/lib/lrama/counterexamples/example.rb
+++ b/lib/lrama/counterexamples/example.rb
@@ -38,7 +38,7 @@ def derivations2
       private
 
       def _derivations(paths)
-        derivation = nil #: Derivation?
+        derivation = nil #: Derivation
         current = :production
         last_path = paths.last #: Path
         lookahead_sym = last_path.to.item.end_of_rule? ? @conflict_symbol : nil
@@ -59,7 +59,7 @@ def _derivations(paths)
               derivation = Derivation.new(item, derivation)
               current = :production
             else
-              return nil
+              raise "Unexpected. #{path}"
             end
 
             if lookahead_sym && item.next_next_sym && item.next_next_sym.first_set.include?(lookahead_sym)
diff --git a/sig/lrama/counterexamples/example.rbs b/sig/lrama/counterexamples/example.rbs
index ba55d46d..fae1a98b 100644
--- a/sig/lrama/counterexamples/example.rbs
+++ b/sig/lrama/counterexamples/example.rbs
@@ -31,13 +31,13 @@ module Lrama
 
       def path2_item: () -> States::Item
 
-      def derivations1: () -> Derivation?
+      def derivations1: () -> Derivation
 
-      def derivations2: () -> Derivation?
+      def derivations2: () -> Derivation
 
       private
 
-      def _derivations: (::Array[StartPath | TransitionPath | ProductionPath] paths) -> Derivation?
+      def _derivations: (::Array[StartPath | TransitionPath | ProductionPath] paths) -> Derivation
 
       def find_derivation_for_symbol: (StateItem state_item, Grammar::Symbol sym) -> Derivation?
     end