New functions [production_index] and [find_production] in the incremental API.

TODO

@@ -19,6 +19,7 @@
       force_reduction
       input_needed
       feed (inspection API)
+      production numbers (production_index, find_production)
     menhirLib: possibly incompatible change of type 'a env
 
 * Implementing may_reduce by looping over the action table may be too
@@ -50,14 +51,12 @@
         allows exposing current state even when it is an initial state?
         meta-initial state with transition to the real initial states?
       remonter aussi la fonction element: 'a checkpoint -> int -> element de CompCert
-      ajouter la bijection entre production et int (i2p, p2i)
 
 * Suite des patchs de Frédéric Bour.
     API d'inspection complète.
       Documenter loop_handle_undo, loop_test (let it just return an option), acceptable.
       Exposer le nombre d'états (pour la mémoisation).
       Idem pour les productions.
-      Fonctions d'affichage pour les types terminal, nonterminal, etc.?
       Fonctions d'isomorphisme entre token et 'a terminal * 'a?
 
 * BUG: the warning "this production is never reduced" is sound but incomplete.

src/Engine.ml

@@ -23,8 +23,9 @@ open EngineTypes
 
 module Make (T : TABLE) = struct
 
-  (* This propagates type and exception definitions. The function [number],
-     too, is defined by this [include] declaration. *)
+  (* This propagates type and exception definitions. The functions [number],
+     [production_index], [find_production], too, are defined by this [include]
+     declaration. *)
 
   include T
 

src/EngineTypes.ml

@@ -142,6 +142,9 @@ module type TABLE = sig
 
   type production
 
+  val production_index: production -> int
+  val find_production: int -> production
+
   (* If a state [s] has a default reduction on production [prod], then, upon
      entering [s], the automaton should reduce [prod] without consulting the
      lookahead token. The following function allows determining which states

src/IncrementalEngine.ml

@@ -226,6 +226,13 @@ module type INCREMENTAL_ENGINE = sig
 
   val number: _ lr1state -> int
 
+  (* Productions are numbered. *)
+
+  (* [find_production i] requires the index [i] to be valid. Use with care. *)
+
+  val production_index: production -> int
+  val find_production: int -> production
+
   (* [find_default_reduction s] returns [Some prod] if the state [s] has a
      default reduction of production [prod], and returns [None] otherwise. *)
 

src/TableInterpreter.ml

@@ -65,6 +65,19 @@ module MakeEngineTable (T : TableFormat.TABLES) = struct
   type production =
       int
 
+  (* In principle, only non-start productions are exposed to the user,
+     at type [production] or at type [int]. This is checked dynamically. *)
+  let non_start_production i =
+    assert (T.start <= i && i - T.start < Array.length T.semantic_action)
+
+  let production_index i =
+    non_start_production i;
+    i
+
+  let find_production i =
+    non_start_production i;
+    i
+
   let default_reduction state defred nodefred env =
     let code = PackedIntArray.get T.default_reduction state in
     if code = 0 then

src/referenceInterpreter.ml

@@ -57,6 +57,9 @@ module T = struct
   type production =
       Production.index
 
+  let production_index = Production.p2i
+  let find_production  = Production.i2p
+
   let default_reduction (s : state) defred nodefred env =
     match Invariant.has_default_reduction s with
     | Some (prod, _) ->