Continue direct->definite refactor

Tests fail, work is incomplete. Look at is_split_unstable for issues.

bootstrap/bin/hocc/attrib.ml

@@ -89,9 +89,15 @@ module T = struct
   let init_lane ~conflict_state_index ~symbol_index ~conflict ~contrib =
     {conflict_state_index; symbol_index; conflict; isucc_lr1itemset=Lr1Itemset.empty; contrib}
 
+  let to_lane_attrib {conflict_state_index; symbol_index; conflict; contrib; _} =
+    init_lane ~conflict_state_index ~symbol_index ~conflict ~contrib
+
   let is_empty {contrib; _} =
     Contrib.is_empty contrib
 
+  let is_lane_attrib {isucc_lr1itemset; _} =
+    Lr1Itemset.is_empty isucc_lr1itemset
+
   let union
       {conflict_state_index=csi0; symbol_index=s0; conflict=x0; isucc_lr1itemset=is0; contrib=c0}
       {conflict_state_index=csi1; symbol_index=s1; conflict=x1; isucc_lr1itemset=is1; contrib=c1} =

bootstrap/bin/hocc/attrib.mli

@@ -47,9 +47,15 @@ val init_lane: conflict_state_index:StateIndex.t -> symbol_index:Symbol.Index.t
 (** [init_lane ~conflict_state_index ~symbol_index ~conflict ~contrib] returns an attribution with
     key (conflict_state_index, symbol_index) that attributes [contrib] to a lane. *)
 
+val to_lane_attrib: t -> t
+(** [to_lane t] returns a derivative of [t] with empty [isucc_lr1itemset]. *)
+
 val is_empty: t -> bool
 (** [is_empty t] returns true if there are no attributions in [t]. *)
 
+val is_lane_attrib: t -> bool
+(** [is_lane t] returns true if [isucc_lr1itemset] is empty in [t]. *)
+
 val union: t -> t -> t
 (** [union t0 t1] returns an attribution with the union of attribution values in [t0] and [t1]. The
     keys must be equal. *)

bootstrap/bin/hocc/ielr1.ml

@@ -1,49 +1,41 @@
 open Basis
 open! Basis.Rudiments
 
-(* Backpropagate attribs that were directly attributed, such that all lane predecessors make
- * equivalent indirect attribs. *)
-let rec backprop_transit_attribs adjs transit_attribs lalr1_transit_attribs marks state_index =
+(* Backpropagate potential attribs, such that all lane predecessors make equivalent potential
+ * attribs. *)
+let rec backprop_transit_attribs adjs transit_attribs_potential lalr1_transit_attribs state_index =
   Array.fold ~init:lalr1_transit_attribs
     ~f:(fun lalr1_transit_attribs ipred_state_index ->
-      match Set.mem ipred_state_index marks with
+      let transit = Transit.init ~src:ipred_state_index ~dst:state_index in
+      let transit_attribs = match Ordmap.get transit lalr1_transit_attribs with
+        | None -> TransitAttribs.empty
+        | Some transit_attribs -> transit_attribs
+      in
+      let transit_attribs' = TransitAttribs.union transit_attribs_potential transit_attribs in
+      match Attribs.equal (TransitAttribs.all transit_attribs') (TransitAttribs.all transit_attribs)
+      with
       | true -> lalr1_transit_attribs
       | false -> begin
-          let transit = Transit.init ~src:ipred_state_index ~dst:state_index in
-          assert (not (Transit.cyclic transit));
-          let transit_attribs_prev = match Ordmap.get transit lalr1_transit_attribs with
-            | None -> TransitAttribs.empty
-            | Some transit_attribs_prev -> transit_attribs_prev
-          in
-          let transit_attribs_union = TransitAttribs.union transit_attribs transit_attribs_prev in
-          match Attribs.equal (TransitAttribs.all transit_attribs_union)
-            (TransitAttribs.all transit_attribs_prev) with
-          | true -> lalr1_transit_attribs
-          | false -> begin
-              let lalr1_transit_attribs = Ordmap.upsert ~k:transit ~v:transit_attribs_union
-                  lalr1_transit_attribs in
-              let marks = Set.insert ipred_state_index marks in
-              backprop_transit_attribs adjs transit_attribs lalr1_transit_attribs marks
-                ipred_state_index
-            end
+          let lalr1_transit_attribs = Ordmap.upsert ~k:transit ~v:transit_attribs'
+              lalr1_transit_attribs in
+          backprop_transit_attribs adjs transit_attribs_potential lalr1_transit_attribs
+            ipred_state_index
         end
     ) (Adjs.ipreds_of_state_index state_index adjs)
 
-let rec ipred_transit_attribs ~resolve lalr1_states adjs ~lalr1_transit_attribs marks lanectx =
+let rec ipred_transit_attribs ~resolve lalr1_states adjs ~lalr1_transit_attribs lanectx =
   (* Marking of the current lane segment spanning the start state back to the current state prevents
    * infinite recursion. It is possible for a grammar to induce a combinatorial explosion of
    * contributing lanes, but only non-redundant transition attribs lead to recursion, thus assuring
    * that each transition is recursed on only once. *)
   let state_index = State.index (LaneCtx.state lanectx) in
-  assert (not (Set.mem state_index marks));
-  let marks = Set.insert state_index marks in
   (* Accumulate transit attribs and ipred lane contexts of `lanectx`. *)
   let lalr1_transit_attribs, ipred_lanectxs =
     Array.fold ~init:(lalr1_transit_attribs, [])
       ~f:(fun (lalr1_transit_attribs, ipred_lanectxs) ipred_state_index ->
         let ipred_state = Array.get ipred_state_index lalr1_states in
         let ipred_lanectx = LaneCtx.of_ipred ipred_state lanectx in
-        let ipred_kernel_attribs = LaneCtx.kernel_attribs_all ipred_lanectx in
+        let ipred_kernel_attribs = LaneCtx.kernel_attribs ipred_lanectx in
         let transit = LaneCtx.transit ipred_lanectx in
         (* Load current transit attribs. It is possible for there to be existing attribs to other
          * conflict states. *)
@@ -61,58 +53,51 @@ let rec ipred_transit_attribs ~resolve lalr1_states adjs ~lalr1_transit_attribs
           match KernelAttribs.equal kernel_attribs' kernel_attribs with
           | true -> lalr1_transit_attribs
           | false -> begin
-              assert (not (Transit.cyclic transit));
               let lalr1_transit_attribs =
                 Ordmap.upsert ~k:transit ~v:transit_attribs' lalr1_transit_attribs in
               (* Recurse if lanes may extend to predecessors. *)
               match LaneCtx.traces_length ipred_lanectx with
               | 0L -> lalr1_transit_attribs
               | _ -> ipred_transit_attribs ~resolve lalr1_states adjs ~lalr1_transit_attribs
-                  marks ipred_lanectx
+                  ipred_lanectx
             end
         in
         let ipred_lanectxs = ipred_lanectx :: ipred_lanectxs in
         lalr1_transit_attribs, ipred_lanectxs
-      ) (Array.filter ~f:(fun ipred_state_index -> not (Set.mem ipred_state_index marks))
-        (Adjs.ipreds_of_state_index state_index adjs))
+      ) (Adjs.ipreds_of_state_index state_index adjs)
   in
-  (* Finish computing direct attributions for `lanectx`. This is done post-order to detect
+  (* Finish computing definite attributions for `lanectx`. This is done post-order to detect
    * attributions for which there is a relevant kernel item in `lanectx`, but no relevant item in
    * any of its ipreds' lane contexts. *)
   let lanectx = LaneCtx.post_init ipred_lanectxs lanectx in
-  (* Accumulate direct attributions. *)
+  (* Accumulate definite attributions. *)
   let transit = LaneCtx.transit lanectx in
   let lane_attribs_definite = LaneCtx.lane_attribs_definite lanectx in
   let lalr1_transit_attribs = match Attribs.is_empty lane_attribs_definite with
     | true -> lalr1_transit_attribs
     | false -> begin
-        (* Backpropagate. *)
-        let transit_attribs = TransitAttribs.of_lane_attribs lane_attribs_definite in
-        let lalr1_transit_attribs = backprop_transit_attribs adjs transit_attribs
-            lalr1_transit_attribs marks state_index in
-        let lalr1_transit_attribs = match Transit.cyclic transit with
-          | true -> lalr1_transit_attribs
-          | false -> begin
-              let transit_attribs_direct =
-                TransitAttribs.of_lane_attribs_definite lane_attribs_definite in
-              Ordmap.amend transit ~f:(function
-                | None -> Some transit_attribs_direct
-                | Some transit_attribs_existing ->
-                  Some (TransitAttribs.union transit_attribs_direct transit_attribs_existing)
-              ) lalr1_transit_attribs
-            end
+        (* Merge definite attribs before backpropagating. If there are relevant cycles incorporating
+         * this state, recursion will (in the worst case) terminate upon reaching this state. *)
+        let transit_attribs_definite =
+          TransitAttribs.of_attribs_definite lane_attribs_definite in
+        let lalr1_transit_attribs = Ordmap.amend transit ~f:(function
+          | None -> Some transit_attribs_definite
+          | Some transit_attribs_existing ->
+            Some (TransitAttribs.union transit_attribs_definite transit_attribs_existing)
+        ) lalr1_transit_attribs
         in
-        lalr1_transit_attribs
+        (* Backpropagate. *)
+        let transit_attribs_potential = TransitAttribs.of_attribs_potential lane_attribs_definite in
+        backprop_transit_attribs adjs transit_attribs_potential lalr1_transit_attribs state_index
       end
   in
   lalr1_transit_attribs
 
 let gather_transit_attribs ~resolve symbols prods lalr1_states adjs ~lalr1_transit_attribs
     conflict_state_index =
-  let marks = Set.empty (module State.Index) in
   let conflict_state = Array.get conflict_state_index lalr1_states in
   let lanectx = LaneCtx.of_conflict_state ~resolve symbols prods conflict_state in
-  ipred_transit_attribs ~resolve lalr1_states adjs ~lalr1_transit_attribs marks lanectx
+  ipred_transit_attribs ~resolve lalr1_states adjs ~lalr1_transit_attribs lanectx
 
 let filter_transits_relevant lalr1_transit_attribs transits ~conflict_state_index symbol_index =
   (* Filter in/out transits lacking a relevant {conflict_state, symbol} attrib. *)
@@ -192,8 +177,10 @@ let close_transit_attribs io adjs lalr1_transit_attribs =
                       ~f:(fun (io, lalr1_transit_attribs, workq) out_transit ->
                         let transit_attribs =
                           Ordmap.get_hlt out_transit lalr1_transit_attribs in
-                        let transit_attribs' = TransitAttribs.merge_definite ~conflict_state_index
-                            ~symbol_index ~conflict ~contrib:in_contrib_common transit_attribs in
+                        let lane_attrib = Attrib.init_lane ~conflict_state_index ~symbol_index
+                            ~conflict ~contrib:in_contrib_common in
+                        let transit_attribs' =
+                          TransitAttribs.merge_definite lane_attrib transit_attribs in
                         match Attribs.equal (TransitAttribs.definite transit_attribs')
                           (TransitAttribs.definite transit_attribs) with
                         | true -> io, lalr1_transit_attribs, workq

bootstrap/bin/hocc/laneCtx.ml

@@ -235,7 +235,7 @@ let kernel_lr1itemset_of_prod_index prods state symbol_index prod_index =
   let prod = Prods.prod_of_prod_index prod_index prods in
   kernel_lr1itemset_of_prod state symbol_index prod
 
-let kernel_attribs_all {conflict_state; traces; _} =
+let kernel_attribs {conflict_state; traces; _} =
   let conflict_state_index = State.index conflict_state in
   Ordmap.fold ~init:KernelAttribs.empty
     ~f:(fun kernel_attribs (TraceKey.{symbol_index; conflict; action}, kernel_isuccs) ->
@@ -260,7 +260,7 @@ let lane_attribs_all ({lane_attribs_definite; _} as t) =
         Attribs.insert attrib lane_attribs
       ) attribs
     |> Attribs.union lane_attribs
-  ) (kernel_attribs_all t)
+  ) (kernel_attribs t)
   |> Attribs.union lane_attribs_definite
 
 let lane_attribs_definite {lane_attribs_definite; _} =

bootstrap/bin/hocc/laneCtx.mli

@@ -68,9 +68,9 @@ val post_init: t list -> t -> t
 (** [post_init ipred_lanectxs t] finishes initializing definite lane conflict attributions, given
     all (acyclic) ipreds' contexts and returns a derivative of [t]. *)
 
-val kernel_attribs_all: t -> KernelAttribs.t
-(** [kernel_attribs_all t] returns a map of the conflict attributions attributable to the lane(s)
-    encompassing [t], i.e. both definite and potential conflict attributions. *)
+val kernel_attribs: t -> KernelAttribs.t
+(** [kernel_attribs t] returns a map of the conflict attributions directly attributable to the
+    lane(s) encompassing [t], i.e. both definite and potential conflict attributions. *)
 
 val lane_attribs_all: t -> Attribs.t
 (** [lane_attribs_all t] returns a map of the merged lane conflict attributions attributable to

bootstrap/bin/hocc/transitAttribs.ml

@@ -2,10 +2,12 @@ open Basis
 open! Basis.Rudiments
 
 type t = {
-  (* Union of conflict attributions in `kernel_attribs`. *)
+  (* Union of conflict attributions in `definite` and any conflict attributions introduced via
+   * `{of_attribs,merge}_potential`. *)
   all: Attribs.t;
 
-  (* Definite conflict attributions, whether shift (conflict state only) or reduce. *)
+  (* Union of conflict attributions in `kernel_attribs`, whether shift (conflict state only) or
+   * reduce, and any conflict attributions introduced via `{of_attribs,merge}_definite`. *)
   definite: Attribs.t;
 
   (* Per kernel item reduce conflict attributions. Shift attributions are omitted since it is
@@ -76,36 +78,36 @@ let definite {definite; _} =
 let kernel_attribs {kernel_attribs; _} =
   kernel_attribs
 
-let merge ~conflict_state_index ~symbol_index ~conflict ~contrib ({all; _} as t) =
-  let attrib = Attrib.init_lane ~conflict_state_index ~symbol_index ~conflict ~contrib in
-  let all = Attribs.insert attrib all in
+let merge_potential lane_attrib ({all; _} as t) =
+  assert (Attrib.is_lane_attrib lane_attrib);
+  let all = Attribs.insert lane_attrib all in
   {t with all}
 
-let of_lane_attribs lane_attribs =
+let of_attribs_potential lane_attribs =
   Attribs.fold ~init:empty
-    ~f:(fun t Attrib.{conflict_state_index; symbol_index; conflict; contrib; _} ->
-      merge ~conflict_state_index ~symbol_index ~conflict ~contrib t
+    ~f:(fun t lane_attrib ->
+      merge_potential lane_attrib t
     ) lane_attribs
 
-let merge_definite ~conflict_state_index ~symbol_index ~conflict ~contrib ({definite; _} as t) =
-  let t = merge ~conflict_state_index ~symbol_index ~conflict ~contrib t in
-  let attrib = Attrib.init_lane ~conflict_state_index ~symbol_index ~conflict ~contrib in
-  let definite = Attribs.insert attrib definite in
+let merge_definite lane_attrib ({definite; _} as t) =
+  assert (Attrib.is_lane_attrib lane_attrib);
+  let t = merge_potential lane_attrib t in
+  let definite = Attribs.insert lane_attrib definite in
   {t with definite}
 
-let of_lane_attribs_definite lane_attribs_definite =
+let of_attribs_definite lane_attribs =
   Attribs.fold ~init:empty
-    ~f:(fun t Attrib.{conflict_state_index; symbol_index; conflict; contrib; _} ->
-      merge_definite ~conflict_state_index ~symbol_index ~conflict ~contrib t
-    ) lane_attribs_definite
+    ~f:(fun t attrib_definite ->
+      merge_definite attrib_definite t
+    ) lane_attribs
 
 let insert_kernel_attribs kernel_attribs t =
   KernelAttribs.fold ~init:t
     ~f:(fun ({kernel_attribs; _} as t) (item, attribs) ->
-      let t = Attribs.fold ~init:t
-          ~f:(fun t Attrib.{conflict_state_index; symbol_index; conflict; contrib; _} ->
-            merge ~conflict_state_index ~symbol_index ~conflict ~contrib t
-          ) attribs in
+      let t = Attribs.fold ~init:t ~f:(fun t attrib ->
+        let lane_attrib = Attrib.to_lane_attrib attrib in
+        merge_definite lane_attrib t
+      ) attribs in
       let kernel_attribs = KernelAttribs.insert item attribs kernel_attribs in
       {t with kernel_attribs}
     ) kernel_attribs

bootstrap/bin/hocc/transitAttribs.mli

@@ -19,48 +19,45 @@ val empty: t
 val is_empty: t -> bool
 (** [is_empty t] returns true if there are no attribs in [t]. *)
 
-val of_lane_attribs: Attribs.t -> t
-(** [of_lane_attribs lane_attribs] initializes a {type:t} by inserting [lane_attribs]. *)
+val of_attribs_potential: Attribs.t -> t
+(** [of_attribs_potential lane_attribs] initializes a {type:t} by inserting [lane_attribs] as
+    potential conflict attributions into the set of all conflict attributions. *)
 
-val of_lane_attribs_definite: Attribs.t -> t
-(** [of_lane_attribs_definite lane_attribs_definite] initializes a {type:t} by inserting
-    [lane_attribs_definite] as definite conflict attributions. *)
+val of_attribs_definite: Attribs.t -> t
+(** [of_attribs_definite lane_attribs] initializes a {type:t} by inserting [lane_attribs] as
+    definite conflict attributions into the set of definite conflict attributions, as well as into
+    the set of all conflict attributions. *)
 
 val reindex: (StateIndex.t, StateIndex.t, StateIndex.cmper_witness) Map.t -> t -> t
 (** [reindex index_map t] creates kernel attribs with all LR(1) item set closure and state nub
     indexes translated according to [index_map], where keys are the original indexes, and values are
     the reindexed indexes. *)
 
 val all: t -> Attribs.t
-(** [all t] returns the union of all conflict attributions in [t]. *)
+(** [all t] returns the union of all potential and definite conflict attributions in [t]. *)
 
 val definite: t -> Attribs.t
 (** [definite t] returns the union of definite conflict attributions made by all kernel items, as
-    well as any definite conflict attributions introduced via [merge_definite]. *)
+    well as any definite conflict attributions introduced via [of_attribs_definite] and/or
+    [merge_definite]. *)
 
 val kernel_attribs: t -> KernelAttribs.t
 (** [kernel_attribs t] returns the per kernel item (definite) reduce conflict attributions in [t].
     Shift attributions are omitted since it is irrelevant which kernel item has a shift attribution,
     whether definite or potential. *)
 
-(* XXX Not used externally. Remove from interface? *)
-val merge: conflict_state_index:StateIndex.t -> symbol_index:Symbol.Index.t -> conflict:Contrib.t
-  -> contrib:Contrib.t -> t -> t
-(** [merge ~conflict_state_index ~symbol_index ~conflict ~contrib t] merges attribution of the
-    conflict contribution [contrib] to state [conflict_state_index] on symbol [symbol_index] into
-    the set of all conflict attributions. *)
+val merge_potential: Attrib.t -> t -> t
+(** [merge_potential lane_attrib t] merges [lane_attrib] into the set of all conflict attributions.
+*)
 
-val merge_definite: conflict_state_index:StateIndex.t -> symbol_index:Symbol.Index.t
-  -> conflict:Contrib.t -> contrib:Contrib.t -> t -> t
-(** [merge_definite ~conflict_state_index ~symbol_index ~conflict ~contrib t] merges attribution of
-    the conflict contribution [contrib] to state [conflict_state_index] on symbol [symbol_index]
-    into the set of definite conflict attributions, as well as into the set of all conflict
-    attributions. *)
+val merge_definite: Attrib.t -> t -> t
+(** [merge_definite lane_attrib t] merges [lane_attrib] into the set of definite conflict
+    attributions, as well as into the set of all conflict attributions. *)
 
 val insert_kernel_attribs: KernelAttribs.t -> t -> t
 (** [insert_kernel_attribs kernel_attribs t] inserts the conflict attributions in [kernel_attribs]
-    into the conflict attributions, and merging [kernel_attribs] into the set of all conflict
-    attributions. *)
+    into the set of kernel attribs, as well as into the set of definite conflict attributions and
+    the set of all conflict attributions. *)
 
 val union: t -> t -> t
 (** [union t0 t1] returns the union of transit conflict attributions in [t0] and [t1]. *)