Refactors, out_transits filtering fix, possible StateNub.goto reg…

…ression

bootstrap/bin/hocc/contribs.ml

@@ -149,6 +149,21 @@ let union t0 t1 =
     | false -> Ordmap.insert_hlt ~k:conflict_state_index ~v:attribs t
   ) t0 t1
 
+let inter t0 t1 =
+  Ordmap.fold2 ~init:empty ~f:(fun t state_symbol_contrib_opt0 state_symbol_contrib_opt1 ->
+    let conflict_state_index, attribs =
+      match state_symbol_contrib_opt0, state_symbol_contrib_opt1 with
+      | Some (conflict_state_index, _), None
+      | None, Some (conflict_state_index, _) -> conflict_state_index, Attribs.empty
+      | Some (conflict_state_index, attribs0), Some (_, attribs1) ->
+        conflict_state_index, Attribs.inter attribs0 attribs1
+      | None, None -> not_reached ()
+    in
+    match Attribs.is_empty attribs with
+    | true -> t
+    | false -> Ordmap.insert_hlt ~k:conflict_state_index ~v:attribs t
+  ) t0 t1
+
 let diff t0 t1 =
   Ordmap.fold2 ~init:empty ~f:(fun t state_symbol_contrib_opt0 state_symbol_contrib_opt1 ->
     let conflict_state_index, attribs =

bootstrap/bin/hocc/contribs.mli

@@ -43,6 +43,9 @@ val insert: conflict_state_index:StateIndex.t -> Symbol.Index.t -> Contrib.t ->
 val union: t -> t -> t
 (** [union t0 t1] returns the union of conflict contributions in [t0] and [t1]. *)
 
+val inter: t -> t -> t
+(** [inter t0 t1] returns the intersection of conflict contributions in [t0] and [t1]. *)
+
 val diff: t -> t -> t
 (** [diff t0 t1] returns the difference of [t0] relative to [t1]; that is, the set of contribs
     present in [t0] but not in [t1]. *)

bootstrap/bin/hocc/isocores.ml

@@ -93,10 +93,10 @@ let insert symbols gotonub transit_contribs ({isocores; statenubs_map; _} as t)
       index, {t with isocores=isocores'; statenubs_map=statenubs_map'}
     end
 
-let merge symbols gotonub merge_index ({statenubs_map; _} as t) =
+let merge symbols gotonub transit_contribs merge_index ({statenubs_map; _} as t) =
   (* Merge into existing LR(1) item set closure. *)
   let merge_statenub = Ordmap.get_hlt merge_index statenubs_map in
-  let merged, merge_statenub' = StateNub.merge symbols gotonub merge_statenub in
+  let merged, merge_statenub' = StateNub.merge symbols gotonub transit_contribs merge_statenub in
   match merged with
   | false -> begin
 (*

bootstrap/bin/hocc/isocores.mli

@@ -38,11 +38,11 @@ val insert: Symbols.t -> GotoNub.t -> Contribs.t -> t -> StateNub.Index.t * t
     [gotonub] and [transit_contribs], inserts it into an incremental derivative of [t], and returns
     its index along with the derivative of [t]. *)
 
-val merge: Symbols.t -> GotoNub.t -> StateNub.Index.t -> t -> bool * t
-(** [merge symbols gotonub statenub_index t] merges the LR(1) item set closure of [gotonub] into the
-    state nub with given [statenub_index]. If the resulting state nub is distinct from the input,
-    true is returned along with a derivative of [t] with the resulting state nub; [false, t]
-    otherwise. *)
+val merge: Symbols.t -> GotoNub.t -> Contribs.t -> StateNub.Index.t -> t -> bool * t
+(** [merge symbols gotonub transit_contribs statenub_index t] merges the LR(1) item set closure of
+    [gotonub] into the state nub with given [statenub_index] and merges conflict contributions from
+    [gotonub] and [transit_contribs]. If the resulting state nub is distinct from the input, true is
+    returned along with a derivative of [t] with the resulting state nub; [false, t] otherwise. *)
 
 val length: t -> uns
 (** [length t] returns the number of state nubs in [t] (greater than or equal to the number of

bootstrap/bin/hocc/spec.ml

@@ -932,15 +932,8 @@ let rec isocores_init algorithm ~resolve io symbols prods reductions =
               ) (Antes.antes_of_state_index state_index antes) in
             let out_transits = Array.fold ~init:(Ordset.empty (module Transit))
               ~f:(fun out_transits ergo_state_index ->
-                (* Filter out transitions to stable states. Such states may be outside any lanes,
-                 * for which the following code would fail. But even stable ergo states within lanes
-                 * cannot impact split-stability, so universal filtering is appropriate. *)
-                match Set.mem ergo_state_index stable with
-                | true -> out_transits
-                | false -> begin
-                    let transit = Transit.init ~src:state_index ~dst:ergo_state_index in
-                    Ordset.insert transit out_transits
-                  end
+                let transit = Transit.init ~src:state_index ~dst:ergo_state_index in
+                Ordset.insert transit out_transits
               ) (Ergos.ergos_of_state_index state_index ergos) in
             (* Gather the union of conflict states contributed to by all in/out-transitions. *)
             let conflict_state_indexes = Ordset.fold ~init:(Ordset.empty (module State.Index))
@@ -1353,79 +1346,77 @@ let rec isocores_init algorithm ~resolve io symbols prods reductions =
     isocores, workq
   end in
   (* Iteratively process the work queue until no work remains. *)
-  let rec close_gotonubs io symbols prods ~transit_contribs_of_statenub_gotonub ~stable isocores
-      ~workq ~reported_isocores_length = begin
-    match Workq.is_empty workq with
-    | true -> io, isocores
-    | false -> begin
-        let index, workq' = Workq.pop workq in
-        let statenub = Isocores.statenub index isocores in
-        let io, isocores', workq', reported_isocores_length = Ordset.fold
-            ~init:(io, isocores, workq', reported_isocores_length)
-            ~f:(fun (io, isocores, workq, reported_isocores_length) symbol_index ->
-              let symbol = Symbols.symbol_of_symbol_index symbol_index symbols in
-              let gotonub = StateNub.goto symbol statenub in
-              (* Do not propagate contribs across transitions to split-stable states (i.e.
-               * initialize split-stable states with empty contribs). Split-stable states propagate
-               * only constant transition contribs. *)
-              let gotonub, transit_contribs = match stable gotonub with
-                | false -> gotonub, transit_contribs_of_statenub_gotonub statenub gotonub
-                | true -> GotoNub.init ~goto:gotonub.goto ~contribs:Contribs.empty, Contribs.empty
-              in
-              let io, isocores, workq = match Isocores.get gotonub transit_contribs isocores with
-                | None -> begin
-                    let io =
-                      io.log
-                      |> Fmt.fmt (match (Isocores.mem (GotoNub.core gotonub) isocores) with
-                        | false -> "+"
-                        | true -> "*"
-                      )
-                      |> Io.with_log io
-                    in
-                    let index, isocores' =
-                      Isocores.insert symbols gotonub transit_contribs isocores in
-                    let workq' = Workq.push_back index workq in
-                    io, isocores', workq'
-                  end
-                | Some merge_index -> begin
-                    match Isocores.merge symbols gotonub merge_index isocores with
-                    | false, _ -> io, isocores, workq
-                    | true, isocores' -> begin
-                        let io = io.log |> Fmt.fmt "." |> Io.with_log io in
-                        let workq' = match Workq.mem merge_index workq with
-                          | true -> workq
-                          | false -> Workq.push merge_index workq
-                        in
-                        io, isocores', workq'
-                      end
-                  end
-              in
-              let isocores_length = Isocores.length isocores in
-              let io, reported_isocores_length =
-                match (isocores_length % 100L) = 0L && isocores_length > reported_isocores_length
-                with
-                | false -> io, reported_isocores_length
-                | true -> begin
-                    let io =
-                      io.log
-                      |> Fmt.fmt "["
-                      |> Uns.pp (Workq.length workq)
-                      |> Fmt.fmt "/"
-                      |> Uns.pp isocores_length
-                      |> Fmt.fmt "]"
-                      |> Io.with_log io
-                    in
-                    io, isocores_length
-                  end
-              in
-              io, isocores, workq, reported_isocores_length
-            ) (StateNub.next statenub)
-        in
-        close_gotonubs io symbols prods ~transit_contribs_of_statenub_gotonub ~stable isocores'
-          ~workq:workq' ~reported_isocores_length
-      end
-  end in
-  let io, transit_contribs_of_statenub_gotonub, stable, manifestation = match algorithm with
+  let rec close_gotonubs io symbols prods ~transit_contribs_of_statenub_gotonub
+      ~transit_contribs_mask_of_statenub_gotonub isocores ~workq ~reported_isocores_length =
+    begin
+      match Workq.is_empty workq with
+      | true -> io, isocores
+      | false -> begin
+          let index, workq' = Workq.pop workq in
+          let statenub = Isocores.statenub index isocores in
+          let io, isocores', workq', reported_isocores_length = Ordset.fold
+              ~init:(io, isocores, workq', reported_isocores_length)
+              ~f:(fun (io, isocores, workq, reported_isocores_length) symbol_index ->
+                let symbol = Symbols.symbol_of_symbol_index symbol_index symbols in
+                let gotonub =
+                  StateNub.goto ~transit_contribs_mask_of_statenub_gotonub symbol statenub in
+                let transit_contribs = transit_contribs_of_statenub_gotonub statenub gotonub in
+                let io, isocores, workq = match Isocores.get gotonub transit_contribs isocores with
+                  | None -> begin
+                      let io =
+                        io.log
+                        |> Fmt.fmt (match (Isocores.mem (GotoNub.core gotonub) isocores) with
+                          | false -> "+"
+                          | true -> "*"
+                        )
+                        |> Io.with_log io
+                      in
+                      let index, isocores' =
+                        Isocores.insert symbols gotonub transit_contribs isocores in
+                      let workq' = Workq.push_back index workq in
+                      io, isocores', workq'
+                    end
+                  | Some merge_index -> begin
+                      match Isocores.merge symbols gotonub transit_contribs merge_index isocores with
+                      | false, _ -> io, isocores, workq
+                      | true, isocores' -> begin
+                          let io = io.log |> Fmt.fmt "." |> Io.with_log io in
+                          let workq' = match Workq.mem merge_index workq with
+                            | true -> workq
+                            | false -> Workq.push merge_index workq
+                          in
+                          io, isocores', workq'
+                        end
+                    end
+                in
+                let isocores_length = Isocores.length isocores in
+                let io, reported_isocores_length =
+                  match (isocores_length % 100L) = 0L && isocores_length > reported_isocores_length
+                  with
+                  | false -> io, reported_isocores_length
+                  | true -> begin
+                      let io =
+                        io.log
+                        |> Fmt.fmt "["
+                        |> Uns.pp (Workq.length workq)
+                        |> Fmt.fmt "/"
+                        |> Uns.pp isocores_length
+                        |> Fmt.fmt "]"
+                        |> Io.with_log io
+                      in
+                      io, isocores_length
+                    end
+                in
+                io, isocores, workq, reported_isocores_length
+              ) (StateNub.next statenub)
+          in
+          close_gotonubs io symbols prods ~transit_contribs_of_statenub_gotonub
+            ~transit_contribs_mask_of_statenub_gotonub isocores' ~workq:workq'
+            ~reported_isocores_length
+        end
+    end in
+  let io, transit_contribs_of_statenub_gotonub, transit_contribs_mask_of_statenub_gotonub, stable,
+    manifestation = match algorithm with
     | Conf.Ielr1 -> begin
         (* Create lookup function for contribs that closes on the prerequisite LALR(1) inadequacy
          * analysis. *)
@@ -1438,18 +1429,31 @@ let rec isocores_init algorithm ~resolve io symbols prods reductions =
           (* src and dst may be the same when Isocores is looking up an existing state, in which
            * case returning empty contribs is correct. *)
           let transit = Transit.init ~src ~dst in
-          let ret =
-            match Map.get transit lalr1_transit_contribs with
-            | None -> Contribs.empty
-            | Some contribs -> begin
-                (* Omit transit contribs from split-unstable states. A subset of the contribs flow
-                 * through split states. *)
-                match Array.get src lalr1_isocores_stable with
-                | false -> Contribs.empty
-                | true -> contribs
-              end
-          in
-          ret
+          match Map.get transit lalr1_transit_contribs with
+          | None -> Contribs.empty
+          | Some contribs -> begin
+              (* Do not propagate contribs from split-unstable states or to split-stable states. *)
+              match Array.get src lalr1_isocores_stable
+                    && not (Array.get dst lalr1_isocores_stable) with
+              | false -> Contribs.empty
+              | true -> contribs
+            end
+        end in
+        let transit_contribs_mask_of_statenub_gotonub statenub gotonub = begin
+          let src = Isocores.get_core_hlt (Lr1Itemset.core
+              StateNub.(statenub.lr1itemsetclosure.kernel)) lalr1_isocores in
+          let dst = Isocores.get_core_hlt (GotoNub.core gotonub) lalr1_isocores in
+          (* src and dst may be the same when Isocores is looking up an existing state, in which
+           * case returning empty contribs is correct. *)
+          let transit = Transit.init ~src ~dst in
+          match Map.get transit lalr1_transit_contribs with
+          | None -> Contribs.empty
+          | Some contribs -> begin
+              (* Do not propagate contribs to split-stable states. *)
+              match Array.get dst lalr1_isocores_stable with
+              | true -> Contribs.empty
+              | false -> contribs
+            end
         end in
         let stable gotonub = begin
           let statenub_index = Isocores.get_core_hlt (GotoNub.core gotonub) lalr1_isocores in
@@ -1459,9 +1463,11 @@ let rec isocores_init algorithm ~resolve io symbols prods reductions =
           let manifestations = Array.get conflict_state_index lalr1_state_conflict_manifestations in
           Map.get_hlt symbol_index manifestations
         end in
-        io, transit_contribs_of_statenub_gotonub, stable, manifestation
+        io, transit_contribs_of_statenub_gotonub, transit_contribs_mask_of_statenub_gotonub, stable,
+        manifestation
       end
-    | _ -> io, (fun _statenub _gotonub -> Contribs.empty), (fun _gotonub -> false),
+    | _ -> io, (fun _statenub _gotonub -> Contribs.empty),
+      (fun _statenub _gotonub -> Contribs.empty), (fun _gotonub -> false),
       (fun _symbol_index _conflict_state_index -> Contrib.empty)
   in
   let io, compat = compat_init algorithm ~resolve io symbols prods
@@ -1473,7 +1479,8 @@ let rec isocores_init algorithm ~resolve io symbols prods reductions =
     |> Io.with_log io
   in
   let io, isocores =
-    close_gotonubs io symbols prods ~transit_contribs_of_statenub_gotonub ~stable isocores ~workq
+    close_gotonubs io symbols prods ~transit_contribs_of_statenub_gotonub
+      ~transit_contribs_mask_of_statenub_gotonub isocores ~workq
       ~reported_isocores_length:0L in
   let io = io.log |> Fmt.fmt "\n" |> Io.with_log io in
   io, isocores, transit_contribs_of_statenub_gotonub

bootstrap/bin/hocc/stateNub.ml

@@ -202,17 +202,21 @@ let init symbols ~index GotoNub.{goto; contribs=goto_contribs} transit_contribs
 let index {lr1itemsetclosure; _} =
   lr1itemsetclosure.index
 
-let merge symbols GotoNub.{goto; contribs=goto_contribs} {lr1itemsetclosure; contribs} =
+let merge symbols GotoNub.{goto; contribs=goto_contribs} transit_contribs
+  {lr1itemsetclosure; contribs} =
   let merged, lr1itemsetclosure' = Lr1ItemsetClosure.merge symbols goto lr1itemsetclosure in
-  let contribs' = Contribs.union goto_contribs contribs in
+  let contribs' = contribs |> Contribs.union goto_contribs |> Contribs.union transit_contribs in
   merged, {lr1itemsetclosure=lr1itemsetclosure'; contribs=contribs'}
 
 let next {lr1itemsetclosure; _} =
   Lr1ItemsetClosure.next lr1itemsetclosure
 
-let goto symbol {lr1itemsetclosure; contribs} =
+let goto ~transit_contribs_mask_of_statenub_gotonub symbol ({lr1itemsetclosure; contribs} as t) =
   let goto = Lr1ItemsetClosure.goto symbol lr1itemsetclosure in
-  GotoNub.init ~goto ~contribs
+  let gotonub = GotoNub.init ~goto ~contribs in
+  (* XXX Masking causes state explosion in `Gawk`/`Gpic`. *)
+  let transit_contribs_mask = transit_contribs_mask_of_statenub_gotonub t gotonub in
+  GotoNub.init ~goto:gotonub.goto ~contribs:(Contribs.inter gotonub.contribs transit_contribs_mask)
 
 let actions symbols {lr1itemsetclosure; contribs} =
   Lr1ItemsetClosure.actions symbols lr1itemsetclosure

bootstrap/bin/hocc/stateNub.mli

@@ -41,17 +41,20 @@ val init: Symbols.t -> index:Index.t -> GotoNub.t -> Contribs.t -> t
 val index: t -> Index.t
 (** [index t] returns the index of the contained unique LR(1) item set closure. *)
 
-val merge: Symbols.t -> GotoNub.t -> t -> bool * t
-(** [merge symbols gotonub t] merges the kernel represented by [gotonub] into [t]'s kernel and
-    creates the closure of the merged kernel, as well as merging contribs. The boolean result
-    indicates whether items were merged into the kernel. *)
+val merge: Symbols.t -> GotoNub.t -> Contribs.t -> t -> bool * t
+(** [merge symbols gotonub transit_contribs t] merges the kernel represented by [gotonub] into [t]'s
+    kernel and creates the closure of the merged kernel, as well as merging conflict contributions
+    from [gotonub] and [transit_contribs. The boolean result indicates whether items were merged
+    into the kernel. *)
 
 val next: t -> (Symbol.Index.t, Symbol.Index.cmper_witness) Ordset.t
 (** [next t] returns the set of symbol indexes that may appear next, i.e. the symbol indexes
     corresponding to the symbols for which [goto] returns a non-empty set. *)
 
-val goto: Symbol.t -> t -> GotoNub.t
-(** [goto symbol t] computes the kernel of the goto set reachable from [t], given [symbol]. *)
+val goto: transit_contribs_mask_of_statenub_gotonub:(t -> GotoNub.t -> Contribs.t) -> Symbol.t -> t
+  -> GotoNub.t
+(** [goto ~transit_contribs_mask_of_statenub_gotonub symbol t] computes the kernel of the goto set
+    reachable from [t], given [symbol]. *)
 
 val actions: Symbols.t -> t -> (Symbol.Index.t, Actionset.t, Symbol.Index.cmper_witness) Ordmap.t
 (** [actions symbols t] computes the map of per symbol actions for [t]. *)